feat: lemmas for paths-up-to-homotopy (#31574)

We introduce `Path.Homotopic.Quotient.mk` as the normal form (rather than `_root_.Quotient.mk`) for constructing a path-up-to-homotopy from a path. This enables us to work more easily in the quotient. We add simp lemmas corresponding to the basic homotopies relating `refl` / `symm` / `trans` / `cast`.

Author: kim-em

Mathlib/AlgebraicTopology/FundamentalGroupoid/Basic.lean

@@ -163,6 +163,69 @@ end Assoc
 
 end Homotopy
 
+namespace Homotopic
+
+theorem refl_trans (p : Path x₀ x₁) :
+    ((Path.refl x₀).trans p).Homotopic p :=
+  ⟨Homotopy.reflTrans p⟩
+
+theorem trans_refl (p : Path x₀ x₁) :
+    (p.trans (Path.refl x₁)).Homotopic p :=
+  ⟨Homotopy.transRefl p⟩
+
+theorem trans_symm (p : Path x₀ x₁) :
+    (p.trans p.symm).Homotopic (Path.refl x₀) :=
+  ⟨(Homotopy.reflTransSymm p).symm⟩
+
+theorem symm_trans (p : Path x₀ x₁) :
+    (p.symm.trans p).Homotopic (Path.refl x₁) :=
+  ⟨(Homotopy.reflSymmTrans p).symm⟩
+
+theorem trans_assoc {x₀ x₁ x₂ x₃ : X} (p : Path x₀ x₁) (q : Path x₁ x₂) (r : Path x₂ x₃) :
+    ((p.trans q).trans r).Homotopic (p.trans (q.trans r)) :=
+  ⟨Homotopy.transAssoc p q r⟩
+
+namespace Quotient
+
+@[simp, grind =]
+theorem refl_trans (γ : Homotopic.Quotient x₀ x₁) :
+    trans (refl x₀) γ = γ := by
+  induction γ using Quotient.ind with | mk γ =>
+  simpa [← mk_trans, ← mk_refl, eq] using Homotopic.refl_trans γ
+
+@[simp, grind =]
+theorem trans_refl (γ : Homotopic.Quotient x₀ x₁) :
+    trans γ (refl x₁) = γ := by
+  induction γ using Quotient.ind with | mk γ =>
+  simpa [← mk_trans, ← mk_refl, eq] using Homotopic.trans_refl γ
+
+@[simp, grind =]
+theorem trans_symm (γ : Homotopic.Quotient x₀ x₁) :
+    trans γ (symm γ) = refl x₀ := by
+  induction γ using Quotient.ind with | mk γ =>
+  simpa [← mk_trans, ← mk_symm, ← mk_refl, eq] using Homotopic.trans_symm γ
+
+@[simp, grind =]
+theorem symm_trans (γ : Homotopic.Quotient x₀ x₁) :
+    trans (symm γ) γ = refl x₁ := by
+  induction γ using Quotient.ind with | mk γ =>
+  simpa [← mk_trans, ← mk_symm, ← mk_refl, eq] using Homotopic.symm_trans γ
+
+@[simp, grind _=_]
+theorem trans_assoc {x₀ x₁ x₂ x₃ : X}
+    (γ₀ : Homotopic.Quotient x₀ x₁)
+    (γ₁ : Homotopic.Quotient x₁ x₂)
+    (γ₂ : Homotopic.Quotient x₂ x₃) :
+    trans (trans γ₀ γ₁) γ₂ = trans γ₀ (trans γ₁ γ₂) := by
+  induction γ₀ using Quotient.ind with | mk γ₀ =>
+  induction γ₁ using Quotient.ind with | mk γ₁ =>
+  induction γ₂ using Quotient.ind with | mk γ₂ =>
+  simpa [← mk_trans, eq] using Homotopic.trans_assoc γ₀ γ₁ γ₂
+
+end Quotient
+
+end Homotopic
+
 end Path
 
 /-- The fundamental groupoid of a space `X` is defined to be a wrapper around `X`, and we
@@ -218,22 +281,22 @@ instance {X : Type*} [Inhabited X] : Inhabited (FundamentalGroupoid X) :=
 instance : Groupoid (FundamentalGroupoid X) where
   Hom x y := Path.Homotopic.Quotient x.as y.as
   id x := ⟦Path.refl x.as⟧
-  comp := Path.Homotopic.Quotient.comp
+  comp := Path.Homotopic.Quotient.trans
   id_comp := by rintro _ _ ⟨f⟩; exact Quotient.sound ⟨Path.Homotopy.reflTrans f⟩
   comp_id := by rintro _ _ ⟨f⟩; exact Quotient.sound ⟨Path.Homotopy.transRefl f⟩
   assoc := by rintro _ _ _ _ ⟨f⟩ ⟨g⟩ ⟨h⟩; exact Quotient.sound ⟨Path.Homotopy.transAssoc f g h⟩
   inv := Quotient.lift (fun f ↦ ⟦f.symm⟧) (by rintro a b ⟨h⟩; exact Quotient.sound ⟨h.symm₂⟩)
   inv_comp := by rintro _ _ ⟨f⟩; exact Quotient.sound ⟨(Path.Homotopy.reflSymmTrans f).symm⟩
   comp_inv := by rintro _ _ ⟨f⟩; exact Quotient.sound ⟨(Path.Homotopy.reflTransSymm f).symm⟩
 
-theorem comp_eq (x y z : FundamentalGroupoid X) (p : x ⟶ y) (q : y ⟶ z) : p ≫ q = p.comp q := rfl
+theorem comp_eq (x y z : FundamentalGroupoid X) (p : x ⟶ y) (q : y ⟶ z) : p ≫ q = p.trans q := rfl
 
 theorem id_eq_path_refl (x : FundamentalGroupoid X) : 𝟙 x = ⟦Path.refl x.as⟧ := rfl
 
 /-- The functor on fundamental groupoid induced by a continuous map. -/
 @[simps] def map (f : C(X, Y)) : FundamentalGroupoid X ⥤ FundamentalGroupoid Y where
   obj x := ⟨f x.as⟩
-  map p := p.mapFn f
+  map p := p.map f
   map_id _ := rfl
   map_comp := by rintro _ _ _ ⟨p⟩ ⟨q⟩; exact congr_arg Quotient.mk'' (p.map_trans q f.continuous)
 
@@ -253,7 +316,7 @@ scoped notation "πₓ" => FundamentalGroupoid.fundamentalGroupoidFunctor.obj
 scoped notation "πₘ" => FundamentalGroupoid.fundamentalGroupoidFunctor.map
 
 theorem map_eq {X Y : TopCat} {x₀ x₁ : X} (f : C(X, Y)) (p : Path.Homotopic.Quotient x₀ x₁) :
-    (πₘ (TopCat.ofHom f)).map p = p.mapFn f := rfl
+    (πₘ (TopCat.ofHom f)).map p = p.map f := rfl
 
 /-- Help the typechecker by converting a point in a groupoid back to a point in
 the underlying topological space. -/

Mathlib/AlgebraicTopology/FundamentalGroupoid/InducedMaps.lean

@@ -84,8 +84,10 @@ include hfg
 /-- If `f(p(t) = g(q(t))` for two paths `p` and `q`, then the induced path homotopy classes
 `f(p)` and `g(p)` are the same as well, despite having a priori different types -/
 theorem heq_path_of_eq_image :
-    (πₘ (TopCat.ofHom f)).map ⟦p⟧ ≍ (πₘ (TopCat.ofHom g)).map ⟦q⟧ := by
-  simp only [map_eq, ← Path.Homotopic.map_lift]; apply Path.Homotopic.hpath_hext; exact hfg
+    (πₘ (TopCat.ofHom f)).map ⟦p⟧ ≍ (πₘ (TopCat.ofHom g)).map (Path.Homotopic.Quotient.mk q) := by
+  simp only [map_eq, ← Path.Homotopic.Quotient.mk_map]
+  apply Path.Homotopic.hpath_hext
+  exact hfg
 
 private theorem start_path : f x₀ = g x₂ := by convert hfg 0 <;> simp only [Path.source]
 

Mathlib/AlgebraicTopology/FundamentalGroupoid/Product.lean

@@ -56,7 +56,7 @@ def piToPiTop : (∀ i, πₓ (X i)) ⥤ πₓ (TopCat.of (∀ i, X i)) where
   obj g := ⟨fun i => (g i).as⟩
   map p := Path.Homotopic.pi p
   map_id x := by
-    change (Path.Homotopic.pi fun i => ⟦_⟧) = _
+    change (Path.Homotopic.pi fun i => Path.Homotopic.Quotient.mk _) = _
     simp only [Path.Homotopic.pi_lift]
     rfl
   map_comp f g := (Path.Homotopic.comp_pi_eq_pi_comp f g).symm

Mathlib/Topology/Homotopy/Lifting.lean

@@ -346,11 +346,12 @@ theorem liftPath_apply_one_eq_of_homotopicRel {γ₀ γ₁ : C(I, X)}
 /-- A covering map induces an injection on all Hom-sets of the fundamental groupoid,
   in particular on the fundamental group. -/
 lemma injective_path_homotopic_mapFn (e₀ e₁ : E) :
-    Function.Injective fun γ : Path.Homotopic.Quotient e₀ e₁ ↦ γ.mapFn ⟨p, cov.continuous⟩ := by
+    Function.Injective fun γ : Path.Homotopic.Quotient e₀ e₁ ↦ γ.map ⟨p, cov.continuous⟩ := by
   refine Quotient.ind₂ fun γ₀ γ₁ ↦ ?_
   dsimp only
-  simp_rw [← Path.Homotopic.map_lift]
-  iterate 2 rw [Quotient.eq]
+  simp only [Path.Homotopic.Quotient.mk''_eq_mk]
+  simp_rw [← Path.Homotopic.Quotient.mk_map]
+  iterate 2 rw [Path.Homotopic.Quotient.eq]
   exact (cov.homotopicRel_iff_comp ⟨0, .inl rfl, γ₀.source.trans γ₁.source.symm⟩).mpr
 
 /-- A map `f` from a simply-connected, locally path-connected space `A` to another space `X` lifts

Mathlib/Topology/Homotopy/Path.lean

@@ -240,6 +240,9 @@ theorem refl (p : Path x₀ x₁) : p.Homotopic p :=
 theorem symm ⦃p₀ p₁ : Path x₀ x₁⦄ (h : p₀.Homotopic p₁) : p₁.Homotopic p₀ :=
   h.map Homotopy.symm
 
+theorem symm₂ {p q : Path x₀ x₁} (h : p.Homotopic q) : p.symm.Homotopic q.symm :=
+  h.map Homotopy.symm₂
+
 @[trans]
 theorem trans ⦃p₀ p₁ p₂ : Path x₀ x₁⦄ (h₀ : p₀.Homotopic p₁) (h₁ : p₁.Homotopic p₂) :
     p₀.Homotopic p₂ :=
@@ -278,23 +281,123 @@ attribute [local instance] Homotopic.setoid
 instance : Inhabited (Homotopic.Quotient () ()) :=
   ⟨Quotient.mk' <| Path.refl ()⟩
 
+namespace Quotient
+
+/--
+The canonical map from `Path x₀ x₁` to `Path.Homotopic.Quotient x₀ x₁`.
+
+We prefer this as the normal form, rather than generic `_root_.Quotient.mk'`,
+to have better control of simp lemmas.
+-/
+def mk (p : Path x₀ x₁) : Path.Homotopic.Quotient x₀ x₁ :=
+  _root_.Quotient.mk' p
+
+/-- `Path.Homotopic.Quotient.mk` is the simp normal form. -/
+@[simp] theorem mk'_eq_mk (p : Path x₀ x₁) : Quotient.mk' p = mk p := rfl
+@[simp] theorem mk''_eq_mk (p : Path x₀ x₁) : Quotient.mk'' p = mk p := rfl
+
+theorem exact {p q : Path x₀ x₁} (h : Quotient.mk p = Quotient.mk q) :
+    Homotopic p q := by
+  exact _root_.Quotient.exact h
+
+theorem eq {p q : Path x₀ x₁} : mk p = mk q ↔ Homotopic p q :=
+  _root_.Quotient.eq
+
+/--
+A reasoning principle for quotients that allows proofs about quotients to assume that all values are
+constructed with `Quotient.mk`.
+-/
+@[induction_eliminator]
+protected theorem ind {x y : X} {motive : Homotopic.Quotient x y → Prop} :
+    (mk : (a : Path x y) → motive (Quotient.mk a)) → (q : Homotopic.Quotient x y) → motive q :=
+  Quot.ind
+
+/--
+A reasoning principle for quotients that allows proofs about quotients to assume that all values are
+constructed with `Quotient.mk`. This is the two-variable version of `ind`.
+-/
+@[elab_as_elim]
+protected theorem ind₂ {Y : Type*} [TopologicalSpace Y] {x₀ y₀ : X} {x₁ y₁ : Y}
+    {motive : Homotopic.Quotient x₀ y₀ → Path.Homotopic.Quotient x₁ y₁ → Prop}
+    (mk : (a : Path x₀ y₀) → (b : Path x₁ y₁) → motive (Quotient.mk a) (Quotient.mk b))
+    (q₀ : Homotopic.Quotient x₀ y₀) (q₁ : Path.Homotopic.Quotient x₁ y₁) : motive q₀ q₁ := by
+  induction q₀ using Quot.ind with | mk a =>
+  induction q₁ using Quot.ind with | mk b =>
+  exact mk a b
+
+/-- The constant path homotopy class at a point. This is `Path.refl` descended to the quotient. -/
+def refl (x : X) : Path.Homotopic.Quotient x x :=
+  mk (Path.refl x)
+
+@[simp, grind =]
+theorem mk_refl (x : X) : mk (Path.refl x) = refl x :=
+  rfl
+
+/-- The reverse of a path homotopy class. This is `Path.symm` descended to the quotient. -/
+def symm (P : Path.Homotopic.Quotient x₀ x₁) : Path.Homotopic.Quotient x₁ x₀ :=
+  _root_.Quotient.map Path.symm (fun _ _ h => Homotopic.symm₂ h) P
+
+@[simp, grind =]
+theorem mk_symm (P : Path x₀ x₁) : mk P.symm = symm (mk P) :=
+  rfl
+
+/-- Cast a path homotopy class using equalities of endpoints. -/
+def cast {x y : X} (γ : Homotopic.Quotient x y) {x' y'} (hx : x' = x) (hy : y' = y) :
+    Homotopic.Quotient x' y' :=
+  _root_.Quotient.map (fun p => p.cast hx hy)
+    (fun _ _ h => Nonempty.map (fun F => F.cast (by simp) (by simp)) h) γ
+
+@[simp, grind =]
+theorem mk_cast {x y : X} (P : Path x y) {x' y'} (hx : x' = x) (hy : y' = y) :
+    mk (P.cast hx hy) = (mk P).cast hx hy :=
+  rfl
+
+@[simp, grind =]
+theorem cast_rfl_rfl {x y : X} (γ : Homotopic.Quotient x y) : γ.cast rfl rfl = γ := by
+  induction γ using Quotient.ind with | mk γ =>
+  rfl
+
+@[simp, grind =]
+theorem cast_cast {x y : X} (γ : Homotopic.Quotient x y) {x' y'} (hx : x' = x) (hy : y' = y)
+    {x'' y''} (hx' : x'' = x') (hy' : y'' = y') :
+    (γ.cast hx hy).cast hx' hy' = γ.cast (hx'.trans hx) (hy'.trans hy) := by
+  induction γ using Quotient.ind with | mk γ =>
+  rfl
+
 /-- The composition of path homotopy classes. This is `Path.trans` descended to the quotient. -/
-def Quotient.comp (P₀ : Path.Homotopic.Quotient x₀ x₁) (P₁ : Path.Homotopic.Quotient x₁ x₂) :
+def trans (P₀ : Path.Homotopic.Quotient x₀ x₁) (P₁ : Path.Homotopic.Quotient x₁ x₂) :
     Path.Homotopic.Quotient x₀ x₂ :=
   Quotient.map₂ Path.trans (fun (_ : Path x₀ x₁) _ hp (_ : Path x₁ x₂) _ hq => hcomp hp hq) P₀ P₁
 
-theorem comp_lift (P₀ : Path x₀ x₁) (P₁ : Path x₁ x₂) : ⟦P₀.trans P₁⟧ = Quotient.comp ⟦P₀⟧ ⟦P₁⟧ :=
+@[deprecated (since := "2025-11-13")]
+noncomputable alias _root_.Path.Homotopic.comp := Quotient.trans
+
+@[simp, grind =]
+theorem mk_trans (P₀ : Path x₀ x₁) (P₁ : Path x₁ x₂) :
+    mk (P₀.trans P₁) = Quotient.trans (mk P₀) (mk P₁) :=
   rfl
 
+@[deprecated (since := "2025-11-13")]
+noncomputable alias _root_.Path.Homotopic.comp_lift := Quotient.mk_trans
+
 /-- The image of a path homotopy class `P₀` under a map `f`.
 This is `Path.map` descended to the quotient. -/
-def Quotient.mapFn (P₀ : Path.Homotopic.Quotient x₀ x₁) (f : C(X, Y)) :
+def map (P₀ : Path.Homotopic.Quotient x₀ x₁) (f : C(X, Y)) :
     Path.Homotopic.Quotient (f x₀) (f x₁) :=
-  Quotient.map (fun q : Path x₀ x₁ => q.map f.continuous) (fun _ _ h => Path.Homotopic.map h f) P₀
+  _root_.Quotient.map
+    (fun q : Path x₀ x₁ => q.map f.continuous) (fun _ _ h => Path.Homotopic.map h f) P₀
 
-theorem map_lift (P₀ : Path x₀ x₁) (f : C(X, Y)) : ⟦P₀.map f.continuous⟧ = Quotient.mapFn ⟦P₀⟧ f :=
+@[deprecated (since := "2025-11-13")]
+noncomputable alias _root_.Path.Homotopic.mapFn := Quotient.map
+
+theorem mk_map (P₀ : Path x₀ x₁) (f : C(X, Y)) : mk (P₀.map f.continuous) = map (mk P₀) f :=
   rfl
 
+@[deprecated (since := "2025-11-13")]
+noncomputable alias _root_.Path.Homotopic.map_lift := Quotient.mk_map
+
+end Quotient
+
 -- Porting note: we didn't previously need the `α := ...` and `β := ...` hints.
 theorem hpath_hext {p₁ : Path x₀ x₁} {p₂ : Path x₂ x₃} (hp : ∀ t, p₁ t = p₂ t) :
     HEq (α := Path.Homotopic.Quotient _ _) ⟦p₁⟧ (β := Path.Homotopic.Quotient _ _) ⟦p₂⟧ := by

Mathlib/Topology/Homotopy/Product.lean

@@ -98,7 +98,7 @@ end ContinuousMap
 
 namespace Path.Homotopic
 
-local infixl:70 " ⬝ " => Quotient.comp
+local infixl:70 " ⬝ " => Quotient.trans
 
 section Pi
 
@@ -111,38 +111,40 @@ def piHomotopy (γ₀ γ₁ : ∀ i, Path (as i) (bs i)) (H : ∀ i, Path.Homoto
 
 /-- The product of a family of path homotopy classes. -/
 def pi (γ : ∀ i, Path.Homotopic.Quotient (as i) (bs i)) : Path.Homotopic.Quotient as bs :=
-  (Quotient.map Path.pi fun x y hxy =>
+  (_root_.Quotient.map Path.pi fun x y hxy =>
     Nonempty.map (piHomotopy x y) (Classical.nonempty_pi.mpr hxy)) (Quotient.choice γ)
 
 theorem pi_lift (γ : ∀ i, Path (as i) (bs i)) :
-    (Path.Homotopic.pi fun i => ⟦γ i⟧) = ⟦Path.pi γ⟧ := by unfold pi; simp
+    (Path.Homotopic.pi fun i => (Quotient.mk (γ i))) = Quotient.mk (Path.pi γ) := by
+  simp_rw [← Quotient.mk'_eq_mk, Quotient.mk', pi, Quotient.choice_eq, Quotient.map_mk]
 
 /-- Composition and products commute.
   This is `Path.trans_pi_eq_pi_trans` descended to path homotopy classes. -/
 theorem comp_pi_eq_pi_comp (γ₀ : ∀ i, Path.Homotopic.Quotient (as i) (bs i))
     (γ₁ : ∀ i, Path.Homotopic.Quotient (bs i) (cs i)) : pi γ₀ ⬝ pi γ₁ = pi fun i ↦ γ₀ i ⬝ γ₁ i := by
   induction γ₁ using Quotient.induction_on_pi with | _ a =>
   induction γ₀ using Quotient.induction_on_pi
-  simp only [pi_lift]
-  rw [← Path.Homotopic.comp_lift, Path.trans_pi_eq_pi_trans, ← pi_lift]
+  simp only [Quotient.mk''_eq_mk, pi_lift]
+  rw [← Path.Homotopic.Quotient.mk_trans, Path.trans_pi_eq_pi_trans, ← pi_lift]
   rfl
 
 /-- Abbreviation for projection onto the ith coordinate. -/
 abbrev proj (i : ι) (p : Path.Homotopic.Quotient as bs) : Path.Homotopic.Quotient (as i) (bs i) :=
-  p.mapFn ⟨_, continuous_apply i⟩
+  p.map ⟨_, continuous_apply i⟩
 
 /-- Lemmas showing projection is the inverse of pi. -/
 @[simp]
 theorem proj_pi (i : ι) (paths : ∀ i, Path.Homotopic.Quotient (as i) (bs i)) :
     proj i (pi paths) = paths i := by
   induction paths using Quotient.induction_on_pi
-  rw [proj, pi_lift, ← Path.Homotopic.map_lift]
+  simp only [Quotient.mk''_eq_mk]
+  rw [proj, pi_lift]
   congr
 
 @[simp]
 theorem pi_proj (p : Path.Homotopic.Quotient as bs) : (pi fun i => proj i p) = p := by
   induction p using Quotient.inductionOn
-  simp_rw [proj, ← Path.Homotopic.map_lift]
+  simp_rw [Quotient.mk''_eq_mk, proj, ← Path.Homotopic.Quotient.mk_map]
   erw [pi_lift]
   congr
 
@@ -167,46 +169,46 @@ def prod (q₁ : Path.Homotopic.Quotient a₁ a₂) (q₂ : Path.Homotopic.Quoti
 
 variable (p₁ p₁' p₂ p₂')
 
-theorem prod_lift : prod ⟦p₁⟧ ⟦p₂⟧ = ⟦p₁.prod p₂⟧ :=
+theorem prod_lift : prod (Quotient.mk p₁) (Quotient.mk p₂) = Quotient.mk (p₁.prod p₂) :=
   rfl
 
 variable (r₁ : Path.Homotopic.Quotient a₂ a₃) (r₂ : Path.Homotopic.Quotient b₂ b₃)
 
 /-- Products commute with path composition.
 This is `trans_prod_eq_prod_trans` descended to the quotient. -/
 theorem comp_prod_eq_prod_comp : prod q₁ q₂ ⬝ prod r₁ r₂ = prod (q₁ ⬝ r₁) (q₂ ⬝ r₂) := by
-  induction q₁, q₂ using Quotient.inductionOn₂
-  induction r₁, r₂ using Quotient.inductionOn₂
-  simp only [prod_lift, ← Path.Homotopic.comp_lift, Path.trans_prod_eq_prod_trans]
+  induction q₁, q₂ using Path.Homotopic.Quotient.ind₂
+  induction r₁, r₂ using Path.Homotopic.Quotient.ind₂
+  simp only [prod_lift, ← Path.Homotopic.Quotient.mk_trans, Path.trans_prod_eq_prod_trans]
 
 variable {c₁ c₂ : α × β}
 
 /-- Abbreviation for projection onto the left coordinate of a path class. -/
 abbrev projLeft (p : Path.Homotopic.Quotient c₁ c₂) : Path.Homotopic.Quotient c₁.1 c₂.1 :=
-  p.mapFn ⟨_, continuous_fst⟩
+  p.map ⟨_, continuous_fst⟩
 
 /-- Abbreviation for projection onto the right coordinate of a path class. -/
 abbrev projRight (p : Path.Homotopic.Quotient c₁ c₂) : Path.Homotopic.Quotient c₁.2 c₂.2 :=
-  p.mapFn ⟨_, continuous_snd⟩
+  p.map ⟨_, continuous_snd⟩
 
 /-- Lemmas showing projection is the inverse of product. -/
 @[simp]
 theorem projLeft_prod : projLeft (prod q₁ q₂) = q₁ := by
-  induction q₁, q₂ using Quotient.inductionOn₂
-  rw [projLeft, prod_lift, ← Path.Homotopic.map_lift]
+  induction q₁, q₂ using Path.Homotopic.Quotient.ind₂
+  rw [projLeft, prod_lift, ← Path.Homotopic.Quotient.mk_map]
   congr
 
 @[simp]
 theorem projRight_prod : projRight (prod q₁ q₂) = q₂ := by
-  induction q₁, q₂ using Quotient.inductionOn₂
-  rw [projRight, prod_lift, ← Path.Homotopic.map_lift]
+  induction q₁, q₂ using Path.Homotopic.Quotient.ind₂
+  rw [projRight, prod_lift, ← Path.Homotopic.Quotient.mk_map]
   congr
 
 @[simp]
 theorem prod_projLeft_projRight (p : Path.Homotopic.Quotient (a₁, b₁) (a₂, b₂)) :
     prod (projLeft p) (projRight p) = p := by
-  induction p using Quotient.inductionOn
-  simp only [projLeft, projRight, ← Path.Homotopic.map_lift]
+  induction p using Path.Homotopic.Quotient.ind
+  simp only [projLeft, projRight, ← Path.Homotopic.Quotient.mk_map]
   congr
 
 end Prod