feat: port Topology.Homotopy.Equiv (#2919)

Misc changes:

- rename `Homeomorph.symm_comp_to_continuousMap` to `Homeomorph.symm_comp_toContinuousMap`;
- rename `Homeomorph.to_continuousMap_comp_symm` to `Homeomorph.toContinuousMap_comp_symm`;
- add `CoeFun` instance for `Homeomorph`; otherwise, `toFun_eq_coe` was stuck trying to coerce `h` to a function.

Mathlib.lean

@@ -1467,6 +1467,7 @@ import Mathlib.Topology.GDelta
 import Mathlib.Topology.Hom.Open
 import Mathlib.Topology.Homeomorph
 import Mathlib.Topology.Homotopy.Basic
+import Mathlib.Topology.Homotopy.Equiv
 import Mathlib.Topology.Inseparable
 import Mathlib.Topology.Instances.ENNReal
 import Mathlib.Topology.Instances.EReal

Mathlib/Topology/ContinuousFunction/Basic.lean

@@ -452,14 +452,14 @@ theorem coe_trans : (f.trans g : C(α, γ)) = (g : C(β, γ)).comp f :=
 
 /-- Left inverse to a continuous map from a homeomorphism, mirroring `Equiv.symm_comp_self`. -/
 @[simp]
-theorem symm_comp_to_continuousMap : (f.symm : C(β, α)).comp (f : C(α, β)) = ContinuousMap.id α :=
+theorem symm_comp_toContinuousMap : (f.symm : C(β, α)).comp (f : C(α, β)) = ContinuousMap.id α :=
   by rw [← coe_trans, self_trans_symm, coe_refl]
-#align homeomorph.symm_comp_to_continuous_map Homeomorph.symm_comp_to_continuousMap
+#align homeomorph.symm_comp_to_continuous_map Homeomorph.symm_comp_toContinuousMap
 
 /-- Right inverse to a continuous map from a homeomorphism, mirroring `Equiv.self_comp_symm`. -/
 @[simp]
-theorem to_continuousMap_comp_symm : (f : C(α, β)).comp (f.symm : C(β, α)) = ContinuousMap.id β :=
+theorem toContinuousMap_comp_symm : (f : C(α, β)).comp (f.symm : C(β, α)) = ContinuousMap.id β :=
   by rw [← coe_trans, symm_trans_self, coe_refl]
-#align homeomorph.to_continuous_map_comp_symm Homeomorph.to_continuousMap_comp_symm
+#align homeomorph.to_continuous_map_comp_symm Homeomorph.toContinuousMap_comp_symm
 
 end Homeomorph

Mathlib/Topology/Homeomorph.lean

@@ -65,6 +65,8 @@ instance : EquivLike (α ≃ₜ β) α β where
   right_inv := fun h => h.right_inv
   coe_injective' := fun _ _ H _ => toEquiv_injective <| FunLike.ext' H
 
+instance : CoeFun (α ≃ₜ β) fun _ ↦ α → β := ⟨FunLike.coe⟩
+
 @[simp]
 theorem homeomorph_mk_coe (a : Equiv α β) (b c) : (Homeomorph.mk a b c : α → β) = a :=
   rfl

Mathlib/Topology/Homotopy/Equiv.lean

@@ -0,0 +1,191 @@
+/-
+Copyright (c) 2021 Shing Tak Lam. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Shing Tak Lam
+
+! This file was ported from Lean 3 source module topology.homotopy.equiv
+! leanprover-community/mathlib commit 3d7987cda72abc473c7cdbbb075170e9ac620042
+! Please do not edit these lines, except to modify the commit id
+! if you have ported upstream changes.
+-/
+import Mathlib.Topology.Homotopy.Basic
+
+/-!
+
+# Homotopy equivalences between topological spaces
+
+In this file, we define homotopy equivalences between topological spaces `X` and `Y` as a pair of
+functions `f : C(X, Y)` and `g : C(Y, X)` such that `f.comp g` and `g.comp f` are both homotopic
+to `ContinuousMap.id`.
+
+## Main definitions
+
+- `ContinuousMap.HomotopyEquiv` is the type of homotopy equivalences between topological spaces.
+
+## Notation
+
+We introduce the notation `X ≃ₕ Y` for `ContinuousMap.HomotopyEquiv X Y` in the `ContinuousMap`
+locale.
+
+-/
+
+
+universe u v w
+
+variable {X : Type u} {Y : Type v} {Z : Type w}
+
+variable [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z]
+
+namespace ContinuousMap
+
+/-- A homotopy equivalence between topological spaces `X` and `Y` are a pair of functions
+`toFun : C(X, Y)` and `invFun : C(Y, X)` such that `toFun.comp invFun` and `invFun.comp toFun`
+are both homotopic to corresponding identity maps.
+-/
+@[ext]
+structure HomotopyEquiv (X : Type u) (Y : Type v) [TopologicalSpace X] [TopologicalSpace Y] where
+  toFun : C(X, Y)
+  invFun : C(Y, X)
+  left_inv : (invFun.comp toFun).Homotopic (ContinuousMap.id X)
+  right_inv : (toFun.comp invFun).Homotopic (ContinuousMap.id Y)
+#align continuous_map.homotopy_equiv ContinuousMap.HomotopyEquiv
+
+-- mathport name: continuous_map.homotopy_equiv
+scoped infixl:25 " ≃ₕ " => ContinuousMap.HomotopyEquiv
+
+namespace HomotopyEquiv
+
+/-- Coercion of a `HomotopyEquiv` to function. While the Lean 4 way is to unfold coercions, this
+auxiliary definition will make porting of Lean 3 code easier.
+
+Porting note: TODO: drop this definition. -/
+@[coe] def toFun' (e : X ≃ₕ Y) : X → Y := e.toFun
+
+instance : CoeFun (X ≃ₕ Y) fun _ => X → Y := ⟨toFun'⟩
+
+@[simp]
+theorem toFun_eq_coe (h : HomotopyEquiv X Y) : (h.toFun : X → Y) = h :=
+  rfl
+#align continuous_map.homotopy_equiv.to_fun_eq_coe ContinuousMap.HomotopyEquiv.toFun_eq_coe
+
+@[continuity]
+theorem continuous (h : HomotopyEquiv X Y) : Continuous h :=
+  h.toFun.continuous
+#align continuous_map.homotopy_equiv.continuous ContinuousMap.HomotopyEquiv.continuous
+
+end HomotopyEquiv
+
+end ContinuousMap
+
+open ContinuousMap
+
+namespace Homeomorph
+
+/-- Any homeomorphism is a homotopy equivalence.
+-/
+def toHomotopyEquiv (h : X ≃ₜ Y) : X ≃ₕ Y where
+  toFun := h
+  invFun := h.symm
+  left_inv := by rw [symm_comp_toContinuousMap]
+  right_inv := by rw [toContinuousMap_comp_symm]
+#align homeomorph.to_homotopy_equiv Homeomorph.toHomotopyEquiv
+
+@[simp]
+theorem coe_toHomotopyEquiv (h : X ≃ₜ Y) : (h.toHomotopyEquiv : X → Y) = h :=
+  rfl
+#align homeomorph.coe_to_homotopy_equiv Homeomorph.coe_toHomotopyEquiv
+
+end Homeomorph
+
+namespace ContinuousMap
+
+namespace HomotopyEquiv
+
+/-- If `X` is homotopy equivalent to `Y`, then `Y` is homotopy equivalent to `X`.
+-/
+def symm (h : X ≃ₕ Y) : Y ≃ₕ X where
+  toFun := h.invFun
+  invFun := h.toFun
+  left_inv := h.right_inv
+  right_inv := h.left_inv
+#align continuous_map.homotopy_equiv.symm ContinuousMap.HomotopyEquiv.symm
+
+@[simp]
+theorem coe_invFun (h : HomotopyEquiv X Y) : (⇑h.invFun : Y → X) = ⇑h.symm :=
+  rfl
+#align continuous_map.homotopy_equiv.coe_inv_fun ContinuousMap.HomotopyEquiv.coe_invFun
+
+/-- See Note [custom simps projection]. We need to specify this projection explicitly in this case,
+because it is a composition of multiple projections. -/
+def Simps.apply (h : X ≃ₕ Y) : X → Y :=
+  h
+#align continuous_map.homotopy_equiv.simps.apply ContinuousMap.HomotopyEquiv.Simps.apply
+
+/-- See Note [custom simps projection]. We need to specify this projection explicitly in this case,
+because it is a composition of multiple projections. -/
+def Simps.symm_apply (h : X ≃ₕ Y) : Y → X :=
+  h.symm
+#align continuous_map.homotopy_equiv.simps.symm_apply ContinuousMap.HomotopyEquiv.Simps.symm_apply
+
+initialize_simps_projections HomotopyEquiv (toFun_toFun → apply, invFun_toFun → symm_apply,
+  -toFun, -invFun)
+
+/-- Any topological space is homotopy equivalent to itself.
+-/
+@[simps!]
+def refl (X : Type u) [TopologicalSpace X] : X ≃ₕ X :=
+  (Homeomorph.refl X).toHomotopyEquiv
+#align continuous_map.homotopy_equiv.refl ContinuousMap.HomotopyEquiv.refl
+#align continuous_map.homotopy_equiv.refl_apply ContinuousMap.HomotopyEquiv.refl_apply
+#align continuous_map.homotopy_equiv.refl_symm_apply ContinuousMap.HomotopyEquiv.refl_symm_apply
+
+instance : Inhabited (HomotopyEquiv Unit Unit) :=
+  ⟨refl Unit⟩
+
+/--
+If `X` is homotopy equivalent to `Y`, and `Y` is homotopy equivalent to `Z`, then `X` is homotopy
+equivalent to `Z`.
+-/
+@[simps!]
+def trans (h₁ : X ≃ₕ Y) (h₂ : Y ≃ₕ Z) : X ≃ₕ Z where
+  toFun := h₂.toFun.comp h₁.toFun
+  invFun := h₁.invFun.comp h₂.invFun
+  left_inv := by
+    refine Homotopic.trans ?_ h₁.left_inv
+    exact ((Homotopic.refl _).hcomp h₂.left_inv).hcomp (Homotopic.refl _)
+  right_inv := by
+    refine Homotopic.trans ?_ h₂.right_inv
+    exact ((Homotopic.refl _).hcomp h₁.right_inv).hcomp (Homotopic.refl _)
+#align continuous_map.homotopy_equiv.trans ContinuousMap.HomotopyEquiv.trans
+#align continuous_map.homotopy_equiv.trans_apply ContinuousMap.HomotopyEquiv.trans_apply
+#align continuous_map.homotopy_equiv.trans_symm_apply ContinuousMap.HomotopyEquiv.trans_symm_apply
+
+theorem symm_trans (h₁ : X ≃ₕ Y) (h₂ : Y ≃ₕ Z) : (h₁.trans h₂).symm = h₂.symm.trans h₁.symm := rfl
+#align continuous_map.homotopy_equiv.symm_trans ContinuousMap.HomotopyEquiv.symm_trans
+
+end HomotopyEquiv
+
+end ContinuousMap
+
+open ContinuousMap
+
+namespace Homeomorph
+
+@[simp]
+theorem refl_toHomotopyEquiv (X : Type u) [TopologicalSpace X] :
+    (Homeomorph.refl X).toHomotopyEquiv = HomotopyEquiv.refl X :=
+  rfl
+#align homeomorph.refl_to_homotopy_equiv Homeomorph.refl_toHomotopyEquiv
+
+@[simp]
+theorem symm_toHomotopyEquiv (h : X ≃ₜ Y) : h.symm.toHomotopyEquiv = h.toHomotopyEquiv.symm :=
+  rfl
+#align homeomorph.symm_to_homotopy_equiv Homeomorph.symm_toHomotopyEquiv
+
+@[simp]
+theorem trans_toHomotopyEquiv (h₀ : X ≃ₜ Y) (h₁ : Y ≃ₜ Z) :
+    (h₀.trans h₁).toHomotopyEquiv = h₀.toHomotopyEquiv.trans h₁.toHomotopyEquiv :=
+  rfl
+#align homeomorph.trans_to_homotopy_equiv Homeomorph.trans_toHomotopyEquiv
+
+end Homeomorph