feat(Topology): more API for ZerothHomotopy (leanprover-community#38201)

This PR introduces a very basic API for `ZerothHomotopy`. As it was not very well typed, the generic constructor `⟦x⟧` for quotients is replaced by a specific constructor `ZerothHomotopy.mk`.

Author: joelriou

Mathlib/Topology/Connected/LocPathConnected.lean

@@ -126,7 +126,7 @@ def connectedComponentsEquivZerothHomotopy : ConnectedComponents X ≃ ZerothHom
 
 @[simp]
 lemma connectedComponentsEquivZerothHomotopy_apply (x : X) :
-    connectedComponentsEquivZerothHomotopy ⟦x⟧ = ⟦x⟧ :=
+    connectedComponentsEquivZerothHomotopy ⟦x⟧ = (.mk x) :=
   rfl
 
 @[simp]
@@ -135,7 +135,7 @@ lemma coe_connectedComponentsEquivZerothHomotopy_symm :
   rfl
 
 lemma connectedComponentsEquivZerothHomotopy_symm_apply (x : X) :
-    connectedComponentsEquivZerothHomotopy.symm ⟦x⟧ = ⟦x⟧ :=
+    connectedComponentsEquivZerothHomotopy.symm (.mk x) = ⟦x⟧ :=
   rfl
 
 theorem pathConnected_subset_basis {U : Set X} (h : IsOpen U) (hx : x ∈ U) :
@@ -262,19 +262,12 @@ instance AlexandrovDiscrete.locPathConnectedSpace [AlexandrovDiscrete X] :
   symm
   apply hy.joinedIn <;> rewrite [mem_nhdsKer_singleton] <;> [assumption; rfl]
 
-set_option backward.isDefEq.respectTransparency false in
 /-- If a space is locally path-connected, the topology of its path components is discrete. -/
 instance : DiscreteTopology <| ZerothHomotopy X := by
   refine discreteTopology_iff_isOpen_singleton.mpr fun c ↦ ?_
-  obtain ⟨x, rfl⟩ := Quotient.mk_surjective c
-  rw [← isQuotientMap_quotient_mk'.isOpen_preimage]
-  #adaptation_note /-- Before https://github.com/leanprover/lean4/pull/13166
-  (replacing grind's canonicalizer with a type-directed normalizer), `grind` closed this goal.
-  It is not yet clear whether this is due to defeq abuse in Mathlib or a problem in the new
-  canonicalizer; a minimization would help. The original proof was:
-  `grind [ZerothHomotopy.preimage_singleton_eq_pathComponent, IsOpen.pathComponent]` -/
-  rw [ZerothHomotopy.preimage_singleton_eq_pathComponent]
-  exact IsOpen.pathComponent x
+  obtain ⟨x, rfl⟩ := ZerothHomotopy.mk_surjective c
+  rw [← ZerothHomotopy.isQuotientMap_mk.isOpen_preimage]
+  grind [ZerothHomotopy.preimage_singleton_eq_pathComponent, IsOpen.pathComponent]
 
 /-- A locally path-connected compact space has finitely many path components. -/
 instance [CompactSpace X] : Finite <| ZerothHomotopy X :=

Mathlib/Topology/Connected/PathConnected.lean

@@ -108,13 +108,52 @@ def pathSetoid : Setoid X where
 def ZerothHomotopy :=
   Quotient (pathSetoid X)
 
+namespace ZerothHomotopy
+
+variable {X}
+
+/-- The map `X → ZerothHomotopy X`. -/
+def mk (x : X) : ZerothHomotopy X := Quotient.mk _ x
+
+lemma mk_surjective : Function.Surjective (mk (X := X)) := by
+  rintro ⟨x⟩
+  exact ⟨x, rfl⟩
+
+@[elab_as_elim, induction_eliminator, cases_eliminator]
+lemma rec {motive : ZerothHomotopy X → Prop}
+    (mk : ∀ (x : X), motive (.mk x)) (x : ZerothHomotopy X) :
+    motive x := by
+  obtain ⟨x, rfl⟩ := mk_surjective x
+  exact mk x
+
+lemma sound {x y : X} (p : Path x y) : mk x = mk y :=
+  Quotient.sound ⟨p⟩
+
 /-- The quotient topology on path components. -/
 instance : TopologicalSpace <| ZerothHomotopy X :=
   inferInstanceAs <| TopologicalSpace <| Quotient _
 
-instance ZerothHomotopy.inhabited : Inhabited (ZerothHomotopy ℝ) :=
+lemma isQuotientMap_mk : IsQuotientMap (ZerothHomotopy.mk (X := X)) :=
+  isQuotientMap_quotient_mk'
+
+instance inhabited : Inhabited (ZerothHomotopy ℝ) :=
   ⟨@Quotient.mk' ℝ (pathSetoid ℝ) 0⟩
 
+section
+
+variable {T : Type*} (f : X → T) (hf : ∀ ⦃x y : X⦄ (_ : Path x y), f x = f y)
+
+/-- Constructor for maps from `ZerothHomotopy X`. -/
+def lift : ZerothHomotopy X → T :=
+  Quotient.lift f fun _ _ ⟨p⟩ ↦ hf p
+
+@[simp]
+lemma lift_mk (x : X) : lift f hf (.mk x) = f x := rfl
+
+end
+
+end ZerothHomotopy
+
 variable {X}
 
 /-! ### Being joined by a path inside a set -/
@@ -278,8 +317,8 @@ def ZerothHomotopy.toConnectedComponents : ZerothHomotopy X → ConnectedCompone
   Quotient.map id fun x _ h ↦ connectedComponent_eq <| pathComponent_subset_component x h
 
 @[simp]
-theorem ZerothHomotopy.toConnectedComponents_apply (x : X) : toConnectedComponents ⟦x⟧ = ⟦x⟧ :=
-  rfl
+theorem ZerothHomotopy.toConnectedComponents_apply (x : X) :
+    toConnectedComponents (.mk x) = ⟦x⟧ := rfl
 
 /-- There are at least as many path connected components as there are connected components -/
 theorem ZerothHomotopy.toConnectedComponents_surjective :
@@ -598,7 +637,7 @@ end PathConnectedSpace
 /-- The preimage of a singleton in `ZerothHomotopy` is the path component of an element in the
 equivalence class. -/
 theorem ZerothHomotopy.preimage_singleton_eq_pathComponent (x : X) :
-    Quotient.mk' (s := pathSetoid X) ⁻¹' {⟦x⟧} = pathComponent x := by
+    ZerothHomotopy.mk ⁻¹' {.mk x} = pathComponent x := by
   ext y
   rw [mem_preimage, mem_singleton_iff, eq_comm, mem_pathComponent_iff]
   exact Quotient.eq