feat(Topology/Path): prove Path.extend_symm (#23980)

Author: urkud

Mathlib/Order/Interval/Set/ProjIcc.lean

@@ -62,7 +62,6 @@ theorem projIic_of_le (hx : b ≤ x) : projIic b x = ⟨b, le_rfl⟩ := Subtype.
 theorem projIcc_of_le_left (hx : x ≤ a) : projIcc a b h x = ⟨a, left_mem_Icc.2 h⟩ := by
   simp [projIcc, hx, hx.trans h]
 
-
 theorem projIcc_of_right_le (hx : b ≤ x) : projIcc a b h x = ⟨b, right_mem_Icc.2 h⟩ := by
   simp [projIcc, hx, h]
 

Mathlib/Topology/Path.lean

@@ -146,13 +146,8 @@ theorem refl_symm {a : X} : (Path.refl a).symm = Path.refl a := by
   rfl
 
 @[simp]
-theorem symm_range {a b : X} (γ : Path a b) : range γ.symm = range γ := by
-  ext x
-  simp only [mem_range, Path.symm, DFunLike.coe, unitInterval.symm, SetCoe.exists, comp_apply,
-    Subtype.coe_mk]
-  constructor <;> rintro ⟨y, hy, hxy⟩ <;> refine ⟨1 - y, mem_iff_one_sub_mem.mp hy, ?_⟩ <;>
-    convert hxy
-  simp
+theorem symm_range {a b : X} (γ : Path a b) : range γ.symm = range γ :=
+  symm_involutive.surjective.range_comp γ
 
 /-! #### Space of paths -/
 
@@ -227,6 +222,13 @@ theorem extend_of_one_le {a b : X} (γ : Path a b) {t : ℝ}
 theorem refl_extend {a : X} : (Path.refl a).extend = fun _ => a :=
   rfl
 
+theorem extend_symm_apply (γ : Path x y) (t : ℝ) : γ.symm.extend t = γ.extend (1 - t) :=
+  congrArg γ <| symm_projIcc _
+
+@[simp]
+theorem extend_symm (γ : Path x y) : γ.symm.extend = (γ.extend <| 1 - ·) :=
+  funext γ.extend_symm_apply
+
 /-- The path obtained from a map defined on `ℝ` by restriction to the unit interval. -/
 def ofLine {f : ℝ → X} (hf : ContinuousOn f I) (h₀ : f 0 = x) (h₁ : f 1 = y) : Path x y where
   toFun := f ∘ ((↑) : unitInterval → ℝ)
@@ -237,6 +239,11 @@ def ofLine {f : ℝ → X} (hf : ContinuousOn f I) (h₀ : f 0 = x) (h₁ : f 1
 theorem ofLine_mem {f : ℝ → X} (hf : ContinuousOn f I) (h₀ : f 0 = x) (h₁ : f 1 = y) :
     ∀ t, ofLine hf h₀ h₁ t ∈ f '' I := fun ⟨t, t_in⟩ => ⟨t, t_in, rfl⟩
 
+@[simp]
+theorem ofLine_extend (γ : Path x y) : ofLine (by fun_prop) (extend_zero γ) (extend_one γ) = γ := by
+  ext t
+  simp [ofLine]
+
 attribute [local simp] Iic_def
 
 /-- Concatenation of two paths from `x` to `y` and from `y` to `z`, putting the first

Mathlib/Topology/UnitInterval.lean

@@ -107,6 +107,17 @@ theorem symm_bijective : Function.Bijective (symm : I → I) := symm_involutive.
 theorem coe_symm_eq (x : I) : (σ x : ℝ) = 1 - x :=
   rfl
 
+@[simp]
+theorem symm_projIcc (x : ℝ) :
+    symm (projIcc 0 1 zero_le_one x) = projIcc 0 1 zero_le_one (1 - x) := by
+  ext
+  rcases le_total x 0 with h₀ | h₀
+  · simp [projIcc_of_le_left, projIcc_of_right_le, h₀]
+  · rcases le_total x 1 with h₁ | h₁
+    · lift x to I using ⟨h₀, h₁⟩
+      simp_rw [← coe_symm_eq, projIcc_val]
+    · simp [projIcc_of_le_left, projIcc_of_right_le, h₁]
+
 @[continuity, fun_prop]
 theorem continuous_symm : Continuous σ :=
   Continuous.subtype_mk (by fun_prop) _