diff --git a/src/geometry/manifold/instances/sphere.lean b/src/geometry/manifold/instances/sphere.lean
index 3bcf4e1df5c3a..96b30a99a9f9b 100644
--- a/src/geometry/manifold/instances/sphere.lean
+++ b/src/geometry/manifold/instances/sphere.lean
@@ -167,7 +167,7 @@ begin
 end
 
 lemma continuous_stereo_inv_fun (hv : ∥v∥ = 1) : continuous (stereo_inv_fun hv) :=
-continuous_induced_rng (cont_diff_stereo_inv_fun_aux.continuous.comp continuous_subtype_coe)
+continuous_induced_rng.2 (cont_diff_stereo_inv_fun_aux.continuous.comp continuous_subtype_coe)
 
 variables [complete_space E]
 
@@ -386,7 +386,7 @@ lemma cont_mdiff.cod_restrict_sphere {n : ℕ} [fact (finrank ℝ E = n + 1)]
   cont_mdiff I (𝓡 n) m (set.cod_restrict _ _ hf' : M → (sphere (0:E) 1)) :=
 begin
   rw cont_mdiff_iff_target,
-  refine ⟨continuous_induced_rng hf.continuous, _⟩,
+  refine ⟨continuous_induced_rng.2 hf.continuous, _⟩,
   intros v,
   let U := -- Again, removing type ascription... Weird that this helps!
     (orthonormal_basis.from_orthogonal_span_singleton n (ne_zero_of_mem_unit_sphere (-v))).repr,
diff --git a/src/topology/algebra/constructions.lean b/src/topology/algebra/constructions.lean
index 8b739689ad7da..cf61c93cbee10 100644
--- a/src/topology/algebra/constructions.lean
+++ b/src/topology/algebra/constructions.lean
@@ -34,7 +34,7 @@ variables [topological_space M]
 continuous_induced_dom
 
 @[continuity, to_additive] lemma continuous_op : continuous (op : M → Mᵐᵒᵖ) :=
-continuous_induced_rng continuous_id
+continuous_induced_rng.2 continuous_id
 
 @[to_additive] instance [t2_space M] : t2_space Mᵐᵒᵖ :=
 ⟨λ x y h, separated_by_continuous mul_opposite.continuous_unop $ unop_injective.ne h⟩
diff --git a/src/topology/algebra/group.lean b/src/topology/algebra/group.lean
index 1f4ffbbee6dd9..3b4404977f83b 100644
--- a/src/topology/algebra/group.lean
+++ b/src/topology/algebra/group.lean
@@ -279,7 +279,7 @@ variables {ι' : Sort*} [has_inv G]
 @[to_additive] lemma has_continuous_inv_Inf {ts : set (topological_space G)}
   (h : Π t ∈ ts, @has_continuous_inv G t _) :
   @has_continuous_inv G (Inf ts) _ :=
-{ continuous_inv := continuous_Inf_rng (λ t ht, continuous_Inf_dom ht
+{ continuous_inv := continuous_Inf_rng.2 (λ t ht, continuous_Inf_dom ht
   (@has_continuous_inv.continuous_inv G t _ (h t ht))) }
 
 @[to_additive] lemma has_continuous_inv_infi {ts' : ι' → topological_space G}
@@ -1145,7 +1145,7 @@ variables [group G] [topological_space G] [topological_group G] {Γ : subgroup G
 @[to_additive]
 instance quotient_group.has_continuous_const_smul : has_continuous_const_smul G (G ⧸ Γ) :=
 { continuous_const_smul := λ g₀, begin
-    apply continuous_coinduced_dom,
+    apply continuous_coinduced_dom.2,
     change continuous (λ g : G, quotient_group.mk (g₀ * g)),
     exact continuous_coinduced_rng.comp (continuous_mul_left g₀),
   end }
@@ -1181,7 +1181,7 @@ variables [monoid α] [topological_space α] [has_continuous_mul α] [monoid β]
   [has_continuous_mul β]
 
 @[to_additive] instance : topological_group αˣ :=
-{ continuous_inv := continuous_induced_rng ((continuous_unop.comp
+{ continuous_inv := continuous_induced_rng.2 ((continuous_unop.comp
     (@continuous_embed_product α _ _).snd).prod_mk (continuous_op.comp continuous_coe)) }
 
 /-- The topological group isomorphism between the units of a product of two monoids, and the product
@@ -1191,21 +1191,21 @@ def homeomorph.prod_units : homeomorph (α × β)ˣ (αˣ × βˣ) :=
   begin
     show continuous (λ i : (α × β)ˣ, (map (monoid_hom.fst α β) i, map (monoid_hom.snd α β) i)),
     refine continuous.prod_mk _ _,
-    { refine continuous_induced_rng ((continuous_fst.comp units.continuous_coe).prod_mk _),
+    { refine continuous_induced_rng.2 ((continuous_fst.comp units.continuous_coe).prod_mk _),
       refine mul_opposite.continuous_op.comp (continuous_fst.comp _),
       simp_rw units.inv_eq_coe_inv,
       exact units.continuous_coe.comp continuous_inv, },
-    { refine continuous_induced_rng ((continuous_snd.comp units.continuous_coe).prod_mk _),
+    { refine continuous_induced_rng.2 ((continuous_snd.comp units.continuous_coe).prod_mk _),
       simp_rw units.coe_map_inv,
       exact continuous_op.comp (continuous_snd.comp (units.continuous_coe.comp continuous_inv)), }
   end,
   continuous_inv_fun :=
   begin
-    refine continuous_induced_rng (continuous.prod_mk _ _),
+    refine continuous_induced_rng.2 (continuous.prod_mk _ _),
     { exact (units.continuous_coe.comp continuous_fst).prod_mk
         (units.continuous_coe.comp continuous_snd), },
     { refine continuous_op.comp
-        (units.continuous_coe.comp $ continuous_induced_rng $ continuous.prod_mk _ _),
+        (units.continuous_coe.comp $ continuous_induced_rng.2 $ continuous.prod_mk _ _),
       { exact (units.continuous_coe.comp (continuous_inv.comp continuous_fst)).prod_mk
           (units.continuous_coe.comp (continuous_inv.comp continuous_snd)) },
       { exact continuous_op.comp ((units.continuous_coe.comp continuous_fst).prod_mk
diff --git a/src/topology/algebra/module/basic.lean b/src/topology/algebra/module/basic.lean
index bb904422b5525..bb3892b157efd 100644
--- a/src/topology/algebra/module/basic.lean
+++ b/src/topology/algebra/module/basic.lean
@@ -139,7 +139,7 @@ lemma has_continuous_smul_induced :
 { continuous_smul :=
     begin
       letI : topological_space M₁ := t.induced f,
-      refine continuous_induced_rng _,
+      refine continuous_induced_rng.2 _,
       simp_rw [function.comp, f.map_smul],
       refine continuous_fst.smul (continuous_induced_dom.comp continuous_snd)
     end }
diff --git a/src/topology/algebra/module/weak_dual.lean b/src/topology/algebra/module/weak_dual.lean
index 4090ee974c7d7..81c938b9b92d8 100644
--- a/src/topology/algebra/module/weak_dual.lean
+++ b/src/topology/algebra/module/weak_dual.lean
@@ -104,7 +104,7 @@ lemma eval_continuous (y : F) : continuous (λ x : weak_bilin B, B x y) :=
 
 lemma continuous_of_continuous_eval [topological_space α] {g : α → weak_bilin B}
   (h : ∀ y, continuous (λ a, B (g a) y)) : continuous g :=
-continuous_induced_rng (continuous_pi_iff.mpr h)
+continuous_induced_rng.2 (continuous_pi_iff.mpr h)
 
 /-- The coercion `(λ x y, B x y) : E → (F → 𝕜)` is an embedding. -/
 lemma embedding {B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜} (hB : function.injective B) :
@@ -118,7 +118,7 @@ by rw [← tendsto_pi_nhds, embedding.tendsto_nhds_iff (embedding hB)]
 /-- Addition in `weak_space B` is continuous. -/
 instance [has_continuous_add 𝕜] : has_continuous_add (weak_bilin B) :=
 begin
-  refine ⟨continuous_induced_rng _⟩,
+  refine ⟨continuous_induced_rng.2 _⟩,
   refine cast (congr_arg _ _) (((coe_fn_continuous B).comp continuous_fst).add
     ((coe_fn_continuous B).comp continuous_snd)),
   ext,
@@ -128,7 +128,7 @@ end
 /-- Scalar multiplication by `𝕜` on `weak_bilin B` is continuous. -/
 instance [has_continuous_smul 𝕜 𝕜] : has_continuous_smul 𝕜 (weak_bilin B) :=
 begin
-  refine ⟨continuous_induced_rng _⟩,
+  refine ⟨continuous_induced_rng.2 _⟩,
   refine cast (congr_arg _ _) (continuous_fst.smul ((coe_fn_continuous B).comp continuous_snd)),
   ext,
   simp only [function.comp_app, pi.smul_apply, linear_map.map_smulₛₗ, ring_hom.id_apply,
@@ -149,7 +149,7 @@ continuous. -/
 instance [has_continuous_add 𝕜] : topological_add_group (weak_bilin B) :=
 { to_has_continuous_add := by apply_instance,
   continuous_neg := begin
-    refine continuous_induced_rng (continuous_pi_iff.mpr (λ y, _)),
+    refine continuous_induced_rng.2 (continuous_pi_iff.mpr (λ y, _)),
     refine cast (congr_arg _ _) (eval_continuous B (-y)),
     ext,
     simp only [map_neg, function.comp_app, linear_map.neg_apply],
@@ -217,14 +217,14 @@ continuous_linear_map.module
 
 instance (M) [monoid M] [distrib_mul_action M 𝕜] [smul_comm_class 𝕜 M 𝕜]
   [has_continuous_const_smul M 𝕜] : has_continuous_const_smul M (weak_dual 𝕜 E) :=
-⟨λ m, continuous_induced_rng $ (weak_bilin.coe_fn_continuous (top_dual_pairing 𝕜 E)).const_smul m⟩
+⟨λ m, continuous_induced_rng.2 $ (weak_bilin.coe_fn_continuous (top_dual_pairing 𝕜 E)).const_smul m⟩
 
 /-- If a monoid `M` distributively continuously acts on `𝕜` and this action commutes with
 multiplication on `𝕜`, then it continuously acts on `weak_dual 𝕜 E`. -/
 instance (M) [monoid M] [distrib_mul_action M 𝕜] [smul_comm_class 𝕜 M 𝕜]
   [topological_space M] [has_continuous_smul M 𝕜] :
   has_continuous_smul M (weak_dual 𝕜 E) :=
-⟨continuous_induced_rng $ continuous_fst.smul ((weak_bilin.coe_fn_continuous
+⟨continuous_induced_rng.2 $ continuous_fst.smul ((weak_bilin.coe_fn_continuous
                           (top_dual_pairing 𝕜 E)).comp continuous_snd)⟩
 
 lemma coe_fn_continuous : continuous (λ (x : weak_dual 𝕜 E) y, x y) :=
@@ -235,7 +235,7 @@ continuous_pi_iff.mp coe_fn_continuous y
 
 lemma continuous_of_continuous_eval [topological_space α] {g : α → weak_dual 𝕜 E}
   (h : ∀ y, continuous (λ a, (g a) y)) : continuous g :=
-continuous_induced_rng (continuous_pi_iff.mpr h)
+continuous_induced_rng.2 (continuous_pi_iff.mpr h)
 
 end weak_dual
 
diff --git a/src/topology/algebra/monoid.lean b/src/topology/algebra/monoid.lean
index d051728edc171..646fdbe5dc952 100644
--- a/src/topology/algebra/monoid.lean
+++ b/src/topology/algebra/monoid.lean
@@ -565,7 +565,7 @@ variables {ι' : Sort*} [has_mul M]
 @[to_additive] lemma has_continuous_mul_Inf {ts : set (topological_space M)}
   (h : Π t ∈ ts, @has_continuous_mul M t _) :
   @has_continuous_mul M (Inf ts) _ :=
-{ continuous_mul := continuous_Inf_rng (λ t ht, continuous_Inf_dom₂ ht ht
+{ continuous_mul := continuous_Inf_rng.2 (λ t ht, continuous_Inf_dom₂ ht ht
   (@has_continuous_mul.continuous_mul M t _ (h t ht))) }
 
 @[to_additive] lemma has_continuous_mul_infi {ts : ι' → topological_space M}
diff --git a/src/topology/algebra/mul_action.lean b/src/topology/algebra/mul_action.lean
index 60959fe853285..b5719e3c8d659 100644
--- a/src/topology/algebra/mul_action.lean
+++ b/src/topology/algebra/mul_action.lean
@@ -154,7 +154,7 @@ variables {ι : Sort*} {M X : Type*} [topological_space M] [has_smul M X]
 { continuous_smul :=
   begin
     rw ← @Inf_singleton _ _ ‹topological_space M›,
-    exact continuous_Inf_rng (λ t ht, continuous_Inf_dom₂ (eq.refl _) ht
+    exact continuous_Inf_rng.2 (λ t ht, continuous_Inf_dom₂ (eq.refl _) ht
       (@has_continuous_smul.continuous_smul _ _ _ _ t (h t ht)))
   end }
 
diff --git a/src/topology/algebra/ring.lean b/src/topology/algebra/ring.lean
index 80fd313e9bbb8..46d628aabc25e 100644
--- a/src/topology/algebra/ring.lean
+++ b/src/topology/algebra/ring.lean
@@ -160,7 +160,7 @@ open mul_opposite
 
 instance [non_unital_non_assoc_semiring α] [topological_space α] [has_continuous_add α] :
   has_continuous_add αᵐᵒᵖ :=
-{ continuous_add := continuous_induced_rng $ (@continuous_add α _ _ _).comp
+{ continuous_add := continuous_induced_rng.2 $ (@continuous_add α _ _ _).comp
   (continuous_unop.prod_map continuous_unop) }
 
 instance [non_unital_non_assoc_semiring α] [topological_space α] [topological_semiring α] :
@@ -168,7 +168,7 @@ instance [non_unital_non_assoc_semiring α] [topological_space α] [topological_
 
 instance [non_unital_non_assoc_ring α] [topological_space α] [has_continuous_neg α] :
   has_continuous_neg αᵐᵒᵖ :=
-{ continuous_neg := continuous_induced_rng $ (@continuous_neg α _ _ _).comp continuous_unop }
+{ continuous_neg := continuous_induced_rng.2 $ (@continuous_neg α _ _ _).comp continuous_unop }
 
 instance [non_unital_non_assoc_ring α] [topological_space α] [topological_ring α] :
   topological_ring αᵐᵒᵖ := {}
@@ -379,7 +379,7 @@ let Inf_S' := Inf (to_topological_space '' S) in
 { to_topological_space := Inf_S',
   continuous_add       :=
   begin
-    apply continuous_Inf_rng,
+    apply continuous_Inf_rng.2,
     rintros _ ⟨⟨t, tr⟩, haS, rfl⟩, resetI,
     have h := continuous_Inf_dom (set.mem_image_of_mem to_topological_space haS) continuous_id,
     have h_continuous_id := @continuous.prod_map _ _ _ _ t t Inf_S' Inf_S' _ _ h h,
@@ -387,7 +387,7 @@ let Inf_S' := Inf (to_topological_space '' S) in
   end,
   continuous_mul       :=
   begin
-    apply continuous_Inf_rng,
+    apply continuous_Inf_rng.2,
     rintros _ ⟨⟨t, tr⟩, haS, rfl⟩, resetI,
     have h := continuous_Inf_dom (set.mem_image_of_mem to_topological_space haS) continuous_id,
     have h_continuous_id := @continuous.prod_map _ _ _ _ t t Inf_S' Inf_S' _ _ h h,
@@ -395,7 +395,7 @@ let Inf_S' := Inf (to_topological_space '' S) in
   end,
   continuous_neg       :=
   begin
-    apply continuous_Inf_rng,
+    apply continuous_Inf_rng.2,
     rintros _ ⟨⟨t, tr⟩, haS, rfl⟩, resetI,
     have h := continuous_Inf_dom (set.mem_image_of_mem to_topological_space haS) continuous_id,
     exact @continuous.comp _ _ _ (id _) (id _) t _ _ continuous_neg h,
diff --git a/src/topology/algebra/star.lean b/src/topology/algebra/star.lean
index 687cd33e7810e..6ee222f3fcde4 100644
--- a/src/topology/algebra/star.lean
+++ b/src/topology/algebra/star.lean
@@ -84,6 +84,6 @@ instance [has_star R] [topological_space R] [has_continuous_star R] : has_contin
 
 instance [monoid R] [star_semigroup R] [topological_space R] [has_continuous_star R] :
   has_continuous_star Rˣ :=
-⟨continuous_induced_rng units.continuous_embed_product.star⟩
+⟨continuous_induced_rng.2 units.continuous_embed_product.star⟩
 
 end instances
diff --git a/src/topology/constructions.lean b/src/topology/constructions.lean
index c7f021430b549..7164c8bcc540a 100644
--- a/src/topology/constructions.lean
+++ b/src/topology/constructions.lean
@@ -230,7 +230,7 @@ hf.comp continuous_at_snd
 
 @[continuity] lemma continuous.prod_mk {f : γ → α} {g : γ → β}
   (hf : continuous f) (hg : continuous g) : continuous (λx, (f x, g x)) :=
-continuous_inf_rng (continuous_induced_rng hf) (continuous_induced_rng hg)
+continuous_inf_rng.2 ⟨continuous_induced_rng.2 hf, continuous_induced_rng.2 hg⟩
 
 @[continuity] lemma continuous.prod.mk (a : α) : continuous (λ b : β, (a, b)) :=
 continuous_const.prod_mk continuous_id'
@@ -626,11 +626,8 @@ continuous_sup_rng_right continuous_coinduced_rng
 
 @[continuity] lemma continuous.sum_elim {f : α → γ} {g : β → γ}
   (hf : continuous f) (hg : continuous g) : continuous (sum.elim f g) :=
-begin
-  apply continuous_sup_dom;
-  rw continuous_def at hf hg ⊢;
-  assumption
-end
+by simp only [continuous_sup_dom, continuous_coinduced_dom, sum.elim_comp_inl, sum.elim_comp_inr,
+  true_and, *]
 
 @[continuity] lemma continuous.sum_map {f : α → β} {g : γ → δ}
   (hf : continuous f) (hg : continuous g) : continuous (sum.map f g) :=
@@ -760,7 +757,7 @@ lemma is_closed.closed_embedding_subtype_coe {s : set α} (hs : is_closed s) :
 
 @[continuity] lemma continuous_subtype_mk {f : β → α}
   (hp : ∀x, p (f x)) (h : continuous f) : continuous (λx, (⟨f x, hp x⟩ : subtype p)) :=
-continuous_induced_rng h
+continuous_induced_rng.2 h
 
 lemma continuous_inclusion {s t : set α} (h : s ⊆ t) : continuous (inclusion h) :=
 continuous_subtype_mk _ continuous_subtype_coe
@@ -850,7 +847,7 @@ continuous_coinduced_rng
 
 @[continuity] lemma continuous_quot_lift {f : α → β} (hr : ∀ a b, r a b → f a = f b)
   (h : continuous f) : continuous (quot.lift f hr : quot r → β) :=
-continuous_coinduced_dom h
+continuous_coinduced_dom.2 h
 
 lemma quotient_map_quotient_mk : quotient_map (@quotient.mk α s) :=
 quotient_map_quot_mk
@@ -860,11 +857,11 @@ continuous_coinduced_rng
 
 lemma continuous_quotient_lift {f : α → β} (hs : ∀ a b, a ≈ b → f a = f b)
   (h : continuous f) : continuous (quotient.lift f hs : quotient s → β) :=
-continuous_coinduced_dom h
+continuous_coinduced_dom.2 h
 
 lemma continuous_quotient_lift_on' {f : α → β} (hs : ∀ a b, a ≈ b → f a = f b)
   (h : continuous f) : continuous (λ x, quotient.lift_on' x f hs : quotient s → β) :=
-continuous_coinduced_dom h
+continuous_coinduced_dom.2 h
 
 end quotient
 
@@ -874,7 +871,7 @@ variables {ι : Type*} {π : ι → Type*}
 @[continuity]
 lemma continuous_pi [topological_space α] [∀i, topological_space (π i)] {f : α → Πi:ι, π i}
   (h : ∀i, continuous (λa, f a i)) : continuous f :=
-continuous_infi_rng $ assume i, continuous_induced_rng $ h i
+continuous_infi_rng.2 $ assume i, continuous_induced_rng.2 $ h i
 
 @[continuity]
 lemma continuous_apply [∀i, topological_space (π i)] (i : ι) :
@@ -1135,7 +1132,7 @@ end
 @[continuity]
 lemma continuous_sigma [topological_space β] {f : sigma σ → β}
   (h : ∀ i, continuous (λ a, f ⟨i, a⟩)) : continuous f :=
-continuous_supr_dom (λ i, continuous_coinduced_dom (h i))
+continuous_supr_dom.2 (λ i, continuous_coinduced_dom.2 (h i))
 
 @[continuity]
 lemma continuous_sigma_map {κ : Type*} {τ : κ → Type*} [Π k, topological_space (τ k)]
@@ -1201,7 +1198,7 @@ continuous_induced_dom
 
 @[continuity] lemma continuous_ulift_up [topological_space α] :
   continuous (ulift.up : α → ulift.{v u} α) :=
-continuous_induced_rng continuous_id
+continuous_induced_rng.2 continuous_id
 
 end ulift
 
diff --git a/src/topology/continuous_function/units.lean b/src/topology/continuous_function/units.lean
index 5719fe40939aa..6552ba5f8a04d 100644
--- a/src/topology/continuous_function/units.lean
+++ b/src/topology/continuous_function/units.lean
@@ -35,7 +35,7 @@ def units_lift : C(X, Mˣ) ≃ C(X, M)ˣ :=
   inv_fun := λ f,
   { to_fun := λ x, ⟨f x, f⁻¹ x, continuous_map.congr_fun f.mul_inv x,
                                 continuous_map.congr_fun f.inv_mul x⟩,
-    continuous_to_fun := continuous_induced_rng $ continuous.prod_mk (f : C(X, M)).continuous
+    continuous_to_fun := continuous_induced_rng.2 $ continuous.prod_mk (f : C(X, M)).continuous
       $ mul_opposite.continuous_op.comp (↑f⁻¹ : C(X, M)).continuous },
   left_inv := λ f, by { ext, refl },
   right_inv := λ f, by { ext, refl } }
@@ -49,7 +49,7 @@ variables [normed_ring R] [complete_space R]
 lemma _root_.normed_ring.is_unit_unit_continuous {f : C(X, R)} (h : ∀ x, is_unit (f x)) :
   continuous (λ x, (h x).unit) :=
 begin
-  refine continuous_induced_rng (continuous.prod_mk f.continuous
+  refine continuous_induced_rng.2 (continuous.prod_mk f.continuous
     (mul_opposite.continuous_op.comp (continuous_iff_continuous_at.mpr (λ x, _)))),
   have := normed_ring.inverse_continuous_at (h x).unit,
   simp only [←ring.inverse_unit, is_unit.unit_spec, ←function.comp_apply] at this ⊢,
diff --git a/src/topology/order.lean b/src/topology/order.lean
index acf5ed5cf61bc..a1377c4cfd675 100644
--- a/src/topology/order.lean
+++ b/src/topology/order.lean
@@ -595,6 +595,10 @@ lemma nhds_inf {t₁ t₂ : topological_space α} {a : α} :
 
 lemma nhds_top {a : α} : @nhds α ⊤ a = ⊤ := (gc_nhds a).u_top
 
+lemma is_open_sup {t₁ t₂ : topological_space α} {s : set α} :
+  @is_open α (t₁ ⊔ t₂) s ↔ @is_open α t₁ s ∧ @is_open α t₂ s :=
+iff.rfl
+
 local notation `cont` := @continuous _ _
 local notation `tspace` := topological_space
 open topological_space
@@ -617,29 +621,16 @@ continuous_iff_coinduced_le.2 $ le_generate_from h
 lemma continuous_induced_dom {t : tspace β} : cont (induced f t) t f :=
 by { rw continuous_def, assume s h, exact ⟨_, h, rfl⟩ }
 
-lemma continuous_induced_rng {g : γ → α} {t₂ : tspace β} {t₁ : tspace γ}
-  (h : cont t₁ t₂ (f ∘ g)) : cont t₁ (induced f t₂) g :=
-begin
-  rw continuous_def,
-  rintros s ⟨t, ht, s_eq⟩,
-  simpa [← s_eq] using continuous_def.1 h t ht,
-end
-
-lemma continuous_induced_rng' [topological_space α] [topological_space β] [topological_space γ]
-  {g : γ → α} (f : α → β) (H : ‹topological_space α› = ‹topological_space β›.induced f)
-  (h : continuous (f ∘ g)) : continuous g :=
-H.symm ▸ continuous_induced_rng h
+lemma continuous_induced_rng {g : γ → α} {t₂ : tspace β} {t₁ : tspace γ} :
+  cont t₁ (induced f t₂) g ↔ cont t₁ t₂ (f ∘ g) :=
+by simp only [continuous_iff_le_induced, induced_compose]
 
 lemma continuous_coinduced_rng {t : tspace α} : cont t (coinduced f t) f :=
 by { rw continuous_def, assume s h, exact h }
 
-lemma continuous_coinduced_dom {g : β → γ} {t₁ : tspace α} {t₂ : tspace γ}
-  (h : cont t₁ t₂ (g ∘ f)) : cont (coinduced f t₁) t₂ g :=
-begin
-  rw continuous_def at h ⊢,
-  assume s hs,
-  exact h _ hs
-end
+lemma continuous_coinduced_dom {g : β → γ} {t₁ : tspace α} {t₂ : tspace γ} :
+  cont (coinduced f t₁) t₂ g ↔ cont t₁ t₂ (g ∘ f) :=
+by simp only [continuous_iff_coinduced_le, coinduced_compose]
 
 lemma continuous_le_dom {t₁ t₂ : tspace α} {t₃ : tspace β}
   (h₁ : t₂ ≤ t₁) (h₂ : cont t₁ t₃ f) : cont t₂ t₃ f :=
@@ -657,13 +648,9 @@ begin
   exact h₂ s (h₁ s h)
 end
 
-lemma continuous_sup_dom {t₁ t₂ : tspace α} {t₃ : tspace β}
-  (h₁ : cont t₁ t₃ f) (h₂ : cont t₂ t₃ f) : cont (t₁ ⊔ t₂) t₃ f :=
-begin
-  rw continuous_def at h₁ h₂ ⊢,
-  assume s h,
-  exact ⟨h₁ s h, h₂ s h⟩
-end
+lemma continuous_sup_dom {t₁ t₂ : tspace α} {t₃ : tspace β} :
+  cont (t₁ ⊔ t₂) t₃ f ↔ cont t₁ t₃ f ∧ cont t₂ t₃ f :=
+by simp only [continuous_iff_le_induced, sup_le_iff]
 
 lemma continuous_sup_rng_left {t₁ : tspace α} {t₃ t₂ : tspace β} :
   cont t₁ t₂ f → cont t₁ (t₂ ⊔ t₃) f :=
@@ -673,27 +660,25 @@ lemma continuous_sup_rng_right {t₁ : tspace α} {t₃ t₂ : tspace β} :
   cont t₁ t₃ f → cont t₁ (t₂ ⊔ t₃) f :=
 continuous_le_rng le_sup_right
 
-lemma continuous_Sup_dom {t₁ : set (tspace α)} {t₂ : tspace β}
-  (h : ∀t∈t₁, cont t t₂ f) : cont (Sup t₁) t₂ f :=
-continuous_iff_le_induced.2 $ Sup_le $ assume t ht, continuous_iff_le_induced.1 $ h t ht
+lemma continuous_Sup_dom {T : set (tspace α)} {t₂ : tspace β} :
+  cont (Sup T) t₂ f ↔ ∀ t ∈ T, cont t t₂ f :=
+by simp only [continuous_iff_le_induced, Sup_le_iff]
 
 lemma continuous_Sup_rng {t₁ : tspace α} {t₂ : set (tspace β)} {t : tspace β}
   (h₁ : t ∈ t₂) (hf : cont t₁ t f) : cont t₁ (Sup t₂) f :=
 continuous_iff_coinduced_le.2 $ le_Sup_of_le h₁ $ continuous_iff_coinduced_le.1 hf
 
-lemma continuous_supr_dom {t₁ : ι → tspace α} {t₂ : tspace β}
-  (h : ∀i, cont (t₁ i) t₂ f) : cont (supr t₁) t₂ f :=
-continuous_Sup_dom $ assume t ⟨i, (t_eq : t₁ i = t)⟩, t_eq ▸ h i
+lemma continuous_supr_dom {t₁ : ι → tspace α} {t₂ : tspace β} :
+  cont (supr t₁) t₂ f ↔  ∀ i, cont (t₁ i) t₂ f :=
+by simp only [continuous_iff_le_induced, supr_le_iff]
 
 lemma continuous_supr_rng {t₁ : tspace α} {t₂ : ι → tspace β} {i : ι}
   (h : cont t₁ (t₂ i) f) : cont t₁ (supr t₂) f :=
 continuous_Sup_rng ⟨i, rfl⟩ h
 
-lemma continuous_inf_rng {t₁ : tspace α} {t₂ t₃ : tspace β}
-  (h₁ : cont t₁ t₂ f) (h₂ : cont t₁ t₃ f) : cont t₁ (t₂ ⊓ t₃) f :=
-continuous_iff_coinduced_le.2 $ le_inf
-  (continuous_iff_coinduced_le.1 h₁)
-  (continuous_iff_coinduced_le.1 h₂)
+lemma continuous_inf_rng {t₁ : tspace α} {t₂ t₃ : tspace β} :
+  cont t₁ (t₂ ⊓ t₃) f ↔ cont t₁ t₂ f ∧ cont t₁ t₃ f :=
+by simp only [continuous_iff_coinduced_le, le_inf_iff]
 
 lemma continuous_inf_dom_left {t₁ t₂ : tspace α} {t₃ : tspace β} :
   cont t₁ t₃ f → cont (t₁ ⊓ t₂) t₃ f :=
@@ -707,17 +692,17 @@ lemma continuous_Inf_dom {t₁ : set (tspace α)} {t₂ : tspace β} {t : tspace
   cont t t₂ f → cont (Inf t₁) t₂ f :=
 continuous_le_dom $ Inf_le h₁
 
-lemma continuous_Inf_rng {t₁ : tspace α} {t₂ : set (tspace β)}
-  (h : ∀t∈t₂, cont t₁ t f) : cont t₁ (Inf t₂) f :=
-continuous_iff_coinduced_le.2 $ le_Inf $ assume b hb, continuous_iff_coinduced_le.1 $ h b hb
+lemma continuous_Inf_rng {t₁ : tspace α} {T : set (tspace β)} :
+  cont t₁ (Inf T) f ↔ ∀ t ∈ T, cont t₁ t f :=
+by simp only [continuous_iff_coinduced_le, le_Inf_iff]
 
 lemma continuous_infi_dom {t₁ : ι → tspace α} {t₂ : tspace β} {i : ι} :
   cont (t₁ i) t₂ f → cont (infi t₁) t₂ f :=
 continuous_le_dom $ infi_le _ _
 
-lemma continuous_infi_rng {t₁ : tspace α} {t₂ : ι → tspace β}
-  (h : ∀i, cont t₁ (t₂ i) f) : cont t₁ (infi t₂) f :=
-continuous_iff_coinduced_le.2 $ le_infi $ assume i, continuous_iff_coinduced_le.1 $ h i
+lemma continuous_infi_rng {t₁ : tspace α} {t₂ : ι → tspace β} :
+  cont t₁ (infi t₂) f ↔ ∀ i, cont t₁ (t₂ i) f :=
+by simp only [continuous_iff_coinduced_le, le_infi_iff]
 
 @[continuity] lemma continuous_bot {t : tspace β} : cont ⊥ t f :=
 continuous_iff_le_induced.2 $ bot_le