chore(topology/homeomorph): add more simp lemmas (#5069)

Also use implicit arguments in some `iff` lemmas.

src/topology/algebra/module.lean

@@ -769,14 +769,14 @@ protected lemma continuous_within_at (e : M ≃L[R] M₂) {s : set M} {x : M} :
 e.continuous.continuous_within_at
 
 lemma comp_continuous_on_iff
-  {α : Type*} [topological_space α] (e : M ≃L[R] M₂) (f : α → M) (s : set α) :
+  {α : Type*} [topological_space α] (e : M ≃L[R] M₂) {f : α → M} {s : set α} :
   continuous_on (e ∘ f) s ↔ continuous_on f s :=
 e.to_homeomorph.comp_continuous_on_iff _ _
 
 lemma comp_continuous_iff
-  {α : Type*} [topological_space α] (e : M ≃L[R] M₂) (f : α → M) :
+  {α : Type*} [topological_space α] (e : M ≃L[R] M₂) {f : α → M} :
   continuous (e ∘ f) ↔ continuous f :=
-e.to_homeomorph.comp_continuous_iff _
+e.to_homeomorph.comp_continuous_iff
 
 /-- An extensionality lemma for `R ≃L[R] M`. -/
 lemma ext₁ [topological_space R] {f g : R ≃L[R] M} (h : f 1 = g 1) : f = g :=

src/topology/homeomorph.lean

@@ -52,6 +52,16 @@ rfl
 @[continuity]
 protected lemma continuous (h : α ≃ₜ β) : continuous h := h.continuous_to_fun
 
+@[simp] lemma apply_symm_apply (h : α ≃ₜ β) (x : β) : h (h.symm x) = x :=
+h.to_equiv.apply_symm_apply x
+
+@[simp] lemma symm_apply_apply (h : α ≃ₜ β) (x : α) : h.symm (h x) = x :=
+h.to_equiv.symm_apply_apply x
+
+protected lemma bijective (h : α ≃ₜ β) : function.bijective h := h.to_equiv.bijective
+protected lemma injective (h : α ≃ₜ β) : function.injective h := h.to_equiv.injective
+protected lemma surjective (h : α ≃ₜ β) : function.surjective h := h.to_equiv.surjective
+
 /-- Change the homeomorphism `f` to make the inverse function definitionally equal to `g`. -/
 def change_inv (f : α ≃ₜ β) (g : β → α) (hg : function.right_inverse g f) : α ≃ₜ β :=
 have g = f.symm, from funext (λ x, calc g x = f.symm (f (g x)) : (f.left_inv (g x)).symm
@@ -63,14 +73,14 @@ have g = f.symm, from funext (λ x, calc g x = f.symm (f (g x)) : (f.left_inv (g
   continuous_to_fun := f.continuous,
   continuous_inv_fun := by convert f.symm.continuous }
 
-lemma symm_comp_self (h : α ≃ₜ β) : ⇑h.symm ∘ ⇑h = id :=
-funext $ assume a, h.to_equiv.left_inv a
+@[simp] lemma symm_comp_self (h : α ≃ₜ β) : ⇑h.symm ∘ ⇑h = id :=
+funext h.symm_apply_apply
 
-lemma self_comp_symm (h : α ≃ₜ β) : ⇑h ∘ ⇑h.symm = id :=
-funext $ assume a, h.to_equiv.right_inv a
+@[simp] lemma self_comp_symm (h : α ≃ₜ β) : ⇑h ∘ ⇑h.symm = id :=
+funext h.apply_symm_apply
 
-lemma range_coe (h : α ≃ₜ β) : range h = univ :=
-eq_univ_of_forall $ assume b, ⟨h.symm b, congr_fun h.self_comp_symm b⟩
+@[simp] lemma range_coe (h : α ≃ₜ β) : range h = univ :=
+h.surjective.range_eq
 
 lemma image_symm (h : α ≃ₜ β) : image h.symm = preimage h :=
 funext h.symm.to_equiv.image_eq_preimage
@@ -147,21 +157,20 @@ def homeomorph_of_continuous_open (e : α ≃ β) (h₁ : continuous e) (h₂ :
   end,
   .. e }
 
-lemma comp_continuous_on_iff (h : α ≃ₜ β) (f : γ → α) (s : set γ) :
+@[simp] lemma comp_continuous_on_iff (h : α ≃ₜ β) (f : γ → α) (s : set γ) :
   continuous_on (h ∘ f) s ↔ continuous_on f s :=
-begin
-  split,
-  { assume H,
-    have : continuous_on (h.symm ∘ (h ∘ f)) s :=
-      h.symm.continuous.comp_continuous_on H,
-    rwa [← function.comp.assoc h.symm h f, symm_comp_self h] at this },
-  { exact λ H, h.continuous.comp_continuous_on H }
-end
+⟨λ H, by simpa only [(∘), h.symm_apply_apply] using h.symm.continuous.comp_continuous_on H,
+  λ H, h.continuous.comp_continuous_on H⟩
 
-lemma comp_continuous_iff (h : α ≃ₜ β) (f : γ → α) :
+@[simp] lemma comp_continuous_iff (h : α ≃ₜ β) {f : γ → α} :
   continuous (h ∘ f) ↔ continuous f :=
 by simp [continuous_iff_continuous_on_univ, comp_continuous_on_iff]
 
+@[simp] lemma comp_continuous_iff' (h : α ≃ₜ β) {f : β → γ} :
+  continuous (f ∘ h) ↔ continuous f :=
+⟨λ H, by simpa only [(∘), h.apply_symm_apply] using H.comp h.symm.continuous,
+  λ H, H.comp h.continuous⟩
+
 protected lemma quotient_map (h : α ≃ₜ β) : quotient_map h :=
 ⟨h.to_equiv.surjective, h.coinduced_eq.symm⟩
 
@@ -175,41 +184,41 @@ def set_congr {s t : set α} (h : s = t) : s ≃ₜ t :=
 def sum_congr (h₁ : α ≃ₜ β) (h₂ : γ ≃ₜ δ) : α ⊕ γ ≃ₜ β ⊕ δ :=
 { continuous_to_fun  :=
   begin
-    convert continuous_sum_rec (continuous_inl.comp h₁.continuous) (continuous_inr.comp h₂.continuous),
+    convert continuous_sum_rec (continuous_inl.comp h₁.continuous)
+      (continuous_inr.comp h₂.continuous),
     ext x, cases x; refl,
   end,
   continuous_inv_fun :=
   begin
-    convert continuous_sum_rec (continuous_inl.comp h₁.symm.continuous) (continuous_inr.comp h₂.symm.continuous),
+    convert continuous_sum_rec (continuous_inl.comp h₁.symm.continuous)
+      (continuous_inr.comp h₂.symm.continuous),
     ext x, cases x; refl
   end,
   .. h₁.to_equiv.sum_congr h₂.to_equiv }
 
 /-- Product of two homeomorphisms. -/
 def prod_congr (h₁ : α ≃ₜ β) (h₂ : γ ≃ₜ δ) : α × γ ≃ₜ β × δ :=
-{ continuous_to_fun  :=
-    continuous.prod_mk (h₁.continuous.comp continuous_fst) (h₂.continuous.comp continuous_snd),
-  continuous_inv_fun :=
-    continuous.prod_mk (h₁.symm.continuous.comp continuous_fst) (h₂.symm.continuous.comp continuous_snd),
+{ continuous_to_fun  := (h₁.continuous.comp continuous_fst).prod_mk
+    (h₂.continuous.comp continuous_snd),
+  continuous_inv_fun := (h₁.symm.continuous.comp continuous_fst).prod_mk
+    (h₂.symm.continuous.comp continuous_snd),
   .. h₁.to_equiv.prod_congr h₂.to_equiv }
 
 section
 variables (α β γ)
 
 /-- `α × β` is homeomorphic to `β × α`. -/
 def prod_comm : α × β ≃ₜ β × α :=
-{ continuous_to_fun  := continuous.prod_mk continuous_snd continuous_fst,
-  continuous_inv_fun := continuous.prod_mk continuous_snd continuous_fst,
+{ continuous_to_fun  := continuous_snd.prod_mk continuous_fst,
+  continuous_inv_fun := continuous_snd.prod_mk continuous_fst,
   .. equiv.prod_comm α β }
 
 /-- `(α × β) × γ` is homeomorphic to `α × (β × γ)`. -/
 def prod_assoc : (α × β) × γ ≃ₜ α × (β × γ) :=
-{ continuous_to_fun  :=
-    continuous.prod_mk (continuous_fst.comp continuous_fst)
-      (continuous.prod_mk (continuous_snd.comp continuous_fst) continuous_snd),
-  continuous_inv_fun := continuous.prod_mk
-      (continuous.prod_mk continuous_fst (continuous_fst.comp continuous_snd))
-      (continuous_snd.comp continuous_snd),
+{ continuous_to_fun  := (continuous_fst.comp continuous_fst).prod_mk
+    ((continuous_snd.comp continuous_fst).prod_mk continuous_snd),
+  continuous_inv_fun := (continuous_fst.prod_mk (continuous_fst.comp continuous_snd)).prod_mk
+    (continuous_snd.comp continuous_snd),
   .. equiv.prod_assoc α β γ }
 
 end
@@ -248,9 +257,9 @@ def sigma_prod_distrib : ((Σ i, σ i) × β) ≃ₜ (Σ i, (σ i × β)) :=
 homeomorph.symm $
 homeomorph_of_continuous_open (equiv.sigma_prod_distrib σ β).symm
   (continuous_sigma $ λ i,
-    continuous.prod_mk (continuous_sigma_mk.comp continuous_fst) continuous_snd)
+    (continuous_sigma_mk.comp continuous_fst).prod_mk continuous_snd)
   (is_open_map_sigma $ λ i,
-    (open_embedding.prod open_embedding_sigma_mk open_embedding_id).is_open_map)
+    (open_embedding_sigma_mk.prod open_embedding_id).is_open_map)
 
 end distrib