extract lemmas and golf

Mathlib/Topology/Covering/FundamentalGroupCircle.lean

@@ -31,14 +31,14 @@ variable (p : ℝ)
 /-- The loop in `AddCircle p` based at `x` that winds `n` times, defined as
 `t ↦ n • (t * p) + x`. -/
 def zsmulLoop (x : ℝ) (n : ℤ) : Path (x : AddCircle p) x where
-  toFun t := ((n • ((t : ℝ) * p) + x : ℝ) : AddCircle p)
+  toFun t := n • (t * p : ℝ) + x
   source' := by simp
   target' := by simp [coe_period]
   continuous_toFun := by fun_prop
 
 @[simp]
 theorem zsmulLoop_apply (x : ℝ) (n : ℤ) (t : I) :
-    zsmulLoop p x n t = ((n • ((t : ℝ) * p) + x : ℝ) : AddCircle p) :=
+    zsmulLoop p x n t = n • (t * p : ℝ) + x :=
   rfl
 
 variable {p} [hp : Fact (0 < p)]
@@ -58,35 +58,23 @@ noncomputable def windingNumber {x : AddCircle p} (γ : FundamentalGroup (AddCir
 
 /-- The winding number of a loop in `AddCircle p` is `(f 1 - f 0) / p`, for any continuous lift
 `f` of the loop to `ℝ`. -/
-theorem windingNumber_eq_div {x : AddCircle p} (γ : Path x x) (f : C(I, ℝ))
-    (hf : ∀ t, (f t : AddCircle p) = γ t) :
-    (windingNumber (FundamentalGroup.fromPath (.mk γ)) : ℝ) = (f 1 - f 0) / p := by
-  have h0 : ((f 0 : ℝ) : AddCircle p) = x := (hf 0).trans γ.source
+theorem windingNumber_eq_div {x : AddCircle p} (γ : Path x x) (f : C(I, ℝ)) (hf : (↑) ∘ f = γ) :
+    (windingNumber (.mk γ) : ℝ) = (f 1 - f 0) / p := by
+  have h0 : (f 0 : AddCircle p) = x := congr($hf 0).trans γ.source
   obtain ⟨n, hn⟩ : ∃ n : ℤ, n • p = f 1 - f 0 :=
     AddSubgroup.mem_zmultiples_iff.mp <| QuotientAddGroup.eq_iff_sub_mem.mp <|
-      (hf 1).trans <| γ.target.trans h0.symm
-  have hlift : (isCoveringMap_coe p).liftPath γ (f 0) (γ.source.trans h0.symm) = f :=
-    (((isCoveringMap_coe p).eq_liftPath_iff' _).mpr ⟨funext hf, rfl⟩).symm
-  have hmono : ((isCoveringMap_coe p).monodromy (.mk γ) ⟨f 0, h0⟩ : ℝ) = f 1 := by
-    rw [IsCoveringMap.coe_monodromy_mk, hlift]
-  have h : (isAddQuotientCoveringMap_coe p).fundamentalGroupEquiv (x := x) ⟨f 0, h0⟩
-      (FundamentalGroup.fromPath (.mk γ)) =
-      MulOpposite.op (Multiplicative.ofAdd
-        (⟨n • p, AddSubgroup.zsmul_mem_zmultiples p n⟩ : AddSubgroup.zmultiples p)) :=
-    (IsAddQuotientCoveringMap.fundamentalGroupToMulOpposite_apply_eq_Iff
-      (isAddQuotientCoveringMap_coe p)).mpr <| by
-      simp [hmono, AddSubgroup.vadd_def, vadd_eq_add, hn]
-  have hw : windingNumber (FundamentalGroup.fromPath (.mk γ)) = n := by
-    simp only [windingNumber, windingNumberIso,
-      (isAddQuotientCoveringMap_coe p).fundamentalGroupEquiv_eq _ ⟨f 0, h0⟩,
-      MulEquiv.trans_apply, h, MulOpposite.coe_symm_opMulEquiv, MulOpposite.unop_op]
-    exact AddSubgroup.zmultiplesEquivInt_apply_zsmul hp.out.ne' n
-  rw [hw, eq_div_iff hp.out.ne', ← zsmul_eq_mul, hn]
+      congr($hf 1).trans <| γ.target.trans h0.symm
+  have h : (isAddQuotientCoveringMap_coe p).fundamentalGroupEquiv (x := x) ⟨f 0, h0⟩ (.mk γ) =
+      .op (.ofAdd ⟨n • p, n, rfl⟩) :=
+    (isAddQuotientCoveringMap_coe p).fundamentalGroupToMulOpposite_apply_mk_eq hf rfl (by simp [hn])
+  simp [windingNumber, windingNumberIso, AddSubgroup.zmultiplesEquivInt_apply_zsmul hp.out.ne' n,
+    (isAddQuotientCoveringMap_coe p).fundamentalGroupEquiv_eq _ ⟨f 0, h0⟩, h,
+    eq_div_iff hp.out.ne', ← zsmul_eq_mul, ← hn]
 
 /-- The loop `t ↦ n • (t * p) + x` has winding number `n`. -/
 theorem windingNumber_zsmulLoop (x : ℝ) (n : ℤ) :
-    windingNumber (FundamentalGroup.fromPath (.mk (zsmulLoop p x n))) = n := by
+    windingNumber (x := x) (.mk (zsmulLoop p x n)) = n := by
   simpa [hp.out.ne'] using windingNumber_eq_div (zsmulLoop p x n)
-    ⟨fun t ↦ n • ((t : ℝ) * p) + x, by fun_prop⟩ fun _ ↦ rfl
+    ⟨fun t ↦ n • (t * p) + x, by fun_prop⟩ rfl
 
 end AddCircle

Mathlib/Topology/Homotopy/Lifting.lean

@@ -396,6 +396,11 @@ theorem coe_monodromy_mk {x y : X} (γ : Path x y) (e : p ⁻¹' {x}) :
     (cov.monodromy (.mk γ) e : E) = cov.liftPath γ e (γ.source.trans e.2.symm) 1 :=
   rfl
 
+lemma monodromy_eq_apply_one {x y : X} {γ : Path x y} {e : p ⁻¹' {x}} {Γ : C(I, E)}
+    (hpΓ : p ∘ Γ = γ) (Γ_0 : Γ 0 = e) : cov.monodromy (.mk γ) e = Γ 1 := by
+  rw [show Γ = cov.liftPath γ e (γ.source.trans e.2.symm) from (eq_liftPath_iff' ..).mpr ⟨hpΓ, Γ_0⟩,
+    coe_monodromy_mk]
+
 /-- Lift a homotopy class of paths to a covering space. -/
 def liftPathQuotient {x y : X} (γ : Path.Homotopic.Quotient x y) (e : p ⁻¹' {x}) :
     Path.Homotopic.Quotient e.1 (cov.monodromy γ e) :=
@@ -651,6 +656,13 @@ theorem fundamentalGroupToMulOpposite_apply_eq_Iff {g : Gᵐᵒᵖ} :
   have := hp.isCancelSMul.right_cancel'
   aesop
 
+variable {e} in
+theorem fundamentalGroupToMulOpposite_apply_mk_eq {γ : Path x x} {g : G} {Γ : C(I, E)}
+    (hpΓ : p ∘ Γ = γ) (Γ_0 : Γ 0 = e) (Γ_1 : Γ 1 = g • e) :
+    hp.fundamentalGroupToMulOpposite e (.mk γ) = .op g :=
+  hp.fundamentalGroupToMulOpposite_apply_eq_Iff.mpr <| by
+    simp [hp.isCoveringMap.monodromy_eq_apply_one hpΓ Γ_0, Γ_1]
+
 variable {e} in
 theorem unop_fundamentalGroupToMulOpposite_smul :
     (hp.fundamentalGroupToMulOpposite e γ).unop • e.1 = hp.isCoveringMap.monodromy γ e := by
@@ -774,6 +786,13 @@ theorem fundamentalGroupToMulOpposite_apply_eq_Iff {g : (Multiplicative G)ᵐᵒ
     hp.fundamentalGroupToMulOpposite e γ = g ↔ g.unop • e.1 = hp.isCoveringMap.monodromy γ e :=
   hp.toMultiplicative.fundamentalGroupToMulOpposite_apply_eq_Iff
 
+variable {e} in
+theorem fundamentalGroupToMulOpposite_apply_mk_eq {γ : Path x x} {g : Multiplicative G} {Γ : C(I, E)}
+    (hpΓ : p ∘ Γ = γ) (Γ_0 : Γ 0 = e) (Γ_1 : Γ 1 = g • e) :
+    hp.fundamentalGroupToMulOpposite e (.mk γ) = .op g :=
+  hp.fundamentalGroupToMulOpposite_apply_eq_Iff.mpr <| by
+    rw [hp.isCoveringMap.monodromy_eq_apply_one hpΓ Γ_0, Γ_1]; rfl
+
 variable {e} in
 theorem unop_fundamentalGroupToMulOpposite_smul :
     (hp.fundamentalGroupToMulOpposite e γ).unop • e.1 = hp.isCoveringMap.monodromy γ e :=