chore(Topology): restack paths_discrete dependencies

Author: kim-em

Mathlib/AlgebraicTopology/FundamentalGroupoid/SemilocallySimplyConnected.lean

@@ -339,19 +339,11 @@ lemma PathInTube.subpathOn_range_subset {X : Type*} [TopologicalSpace X] {x y :
       (part.h_mono.monotone i.castSucc_lt_succ.le)) ⊆ T.U i := by
   intro z hz
   obtain ⟨t, rfl⟩ := hz
-  apply hγ.stays_in_U i
   have h_mono : (part.t i.castSucc : ℝ) ≤ part.t i.succ :=
     part.h_mono.monotone i.castSucc_lt_succ.le
-  constructor
-  · apply le_add_of_nonneg_right
-    apply mul_nonneg t.2.1
-    linarith
-  · calc (part.t i.castSucc : ℝ) + t * (part.t i.succ - part.t i.castSucc)
-        ≤ part.t i.castSucc + 1 * (part.t i.succ - part.t i.castSucc) := by
-          apply add_le_add_right
-          apply mul_le_mul_of_nonneg_right t.2.2
-          linarith
-      _ = part.t i.succ := by ring
+  simpa [Path.subpathOn_apply] using
+    hγ.stays_in_U i (Set.Icc.convexCombo (part.t i.castSucc) (part.t i.succ) t)
+      ⟨Set.Icc.le_convexCombo h_mono t, Set.Icc.convexCombo_le h_mono t⟩
 
 /-- Convert TubeData with partition to the set of paths in the tube -/
 def TubeData.toSet {X : Type*} [TopologicalSpace X] {x y : X} {n : ℕ}
@@ -390,10 +382,12 @@ theorem Path.exists_partition_in_slsc_neighborhoods (hX : SemilocallySimplyConne
     have hγ_in_inter : γ (t j) ∈ U_inter := by
       simp only [U_inter, Set.mem_iInter]
       intro i hi
-      apply hU_contains i (t j)
+      refine hU_contains i ?_
       cases hi with
-      | inl h => constructor <;> apply h_mono.monotone <;> simp [h, Fin.le_def]
-      | inr h => constructor <;> apply h_mono.monotone <;> simp [h, Fin.le_def, Fin.succ]
+      | inl h =>
+          constructor <;> apply h_mono.monotone <;> simp [h, Fin.le_def]
+      | inr h =>
+          constructor <;> apply h_mono.monotone <;> simp [h, Fin.le_def, Fin.succ]
     -- Take the path component of γ(t_j) in the intersection
     refine ⟨pathComponentIn U_inter (γ (t j)),
       ?_, isPathConnected_pathComponentIn hγ_in_inter,
@@ -1014,10 +1008,11 @@ theorem Path.Homotopic.Quotient.discreteTopology
   induction a using Quotient.inductionOn with
   | h p =>
     -- The preimage of {⟦p⟧} is the homotopy class {p' | Homotopic p' p}, which is open
-    rw [isOpen_coinduced]
+    change IsOpen ((Path.Homotopic.Quotient.mk : Path x y → Path.Homotopic.Quotient x y) ⁻¹'
+      ({⟦p⟧} : Set (Path.Homotopic.Quotient x y)))
     convert isOpen_setOf_homotopic hX p
     ext p'
-    simp only [Set.mem_preimage, Set.mem_singleton_iff, Set.mem_setOf_eq]
+    simp only [Set.mem_preimage, Set.mem_setOf_eq]
     exact Path.Homotopic.Quotient.eq
 
 end

Mathlib/Topology/Homotopy/Path.lean

@@ -472,7 +472,7 @@ variable {X : Type*} [TopologicalSpace X] {x y : X}
 
 /-- Extract a subpath from γ on the interval [a, b] ⊆ [0, 1].
 This is γ reparametrized via the affine map t ↦ a + t(b - a). -/
-def subpathOn (γ : Path x y) (a b : unitInterval) (hab : a ≤ b) : Path (γ a) (γ b) where
+def subpathOn (γ : Path x y) (a b : unitInterval) (_hab : a ≤ b) : Path (γ a) (γ b) where
   toFun t := γ (convexCombo a b t)
   source' := by simp
   target' := by simp

Mathlib/Topology/UnitInterval.lean

@@ -49,9 +49,6 @@ theorem mul_mem {x y : ℝ} (hx : x ∈ I) (hy : y ∈ I) : x * y ∈ I :=
 theorem div_mem {x y : ℝ} (hx : 0 ≤ x) (hy : 0 ≤ y) (hxy : x ≤ y) : x / y ∈ I :=
   ⟨div_nonneg hx hy, div_le_one_of_le₀ hxy hy⟩
 
-/-- The midpoint of the unit interval. -/
-def half : I := ⟨1 / 2, by constructor <;> linarith⟩
-
 theorem fract_mem (x : ℝ) : fract x ∈ I :=
   ⟨fract_nonneg _, (fract_lt_one _).le⟩
 
@@ -337,7 +334,7 @@ theorem convexCombo_eq {a b : ℝ} (x : Icc a b) (t : unitInterval) : convexComb
 
 @[simp, grind =]
 theorem convexCombo_same {a b : ℝ} (x : Icc a b) (t : unitInterval) : convexCombo x x t = x := by
-  convexCombo_eq x t
+  simp [convexCombo_eq]
 
 /-- Convex combination of the endpoints of the unit interval gives the parameter. -/
 @[simp]
@@ -477,12 +474,6 @@ theorem eq_convexCombo {a b : ℝ} {x y z : Icc a b} (hxy : x ≤ y) (hyz : y 
   · field_simp
     ring_nf
 
-theorem continuous_convexCombo {a b : ℝ} :
-    Continuous (fun (p : Icc a b × Icc a b × unitInterval) => convexCombo p.1 p.2.1 p.2.2) := by
-  apply Continuous.subtype_mk
-  fun_prop
-
-
 end Set.Icc
 
 open scoped unitInterval
@@ -735,122 +726,6 @@ lemma exists_strictMono_Icc_subset_open_cover_unitInterval {ι} {c : ι → Set
   · ext; exact ht0
   · ext; exact htn
 
-lemma exists_monotone_Icc_subset_open_cover_unitInterval_prod_self {ι} {c : ι → Set (I × I)}
-    (hc₁ : ∀ i, IsOpen (c i)) (hc₂ : univ ⊆ ⋃ i, c i) :
-    ∃ t : ℕ → I, t 0 = 0 ∧ Monotone t ∧ (∃ n, ∀ m ≥ n, t m = 1) ∧
-      ∀ n m, ∃ i, Icc (t n) (t (n + 1)) ×ˢ Icc (t m) (t (m + 1)) ⊆ c i := by
-  obtain ⟨δ, δ_pos, ball_subset⟩ := lebesgue_number_lemma_of_metric isCompact_univ hc₁ hc₂
-  have hδ := half_pos δ_pos
-  simp_rw [Subtype.ext_iff]
-  have h : (0 : ℝ) ≤ 1 := zero_le_one
-  refine ⟨addNSMul h (δ/2), addNSMul_zero h,
-    monotone_addNSMul h hδ.le, addNSMul_eq_right h hδ, fun n m ↦ ?_⟩
-  obtain ⟨i, hsub⟩ := ball_subset (addNSMul h (δ / 2) n, addNSMul h (δ / 2) m) trivial
-  exact ⟨i, fun t ht ↦ hsub (Metric.mem_ball.mpr <| (max_le (abs_sub_addNSMul_le h hδ.le n ht.1) <|
-    abs_sub_addNSMul_le h hδ.le m ht.2).trans_lt <| half_lt_self δ_pos)⟩
-
-/-- Finite partition variant: Any open cover of `[a, b]` can be refined to a finite partition
-with strictly monotone partition points indexed by `Fin (n + 1)`. -/
-lemma exists_strictMono_Icc_subset_open_cover_Icc {ι} {a b : ℝ} (h : a ≤ b) {c : ι → Set (Icc a b)}
-    (hc₁ : ∀ i, IsOpen (c i)) (hc₂ : univ ⊆ ⋃ i, c i) :
-    ∃ (n : ℕ) (t : Fin (n + 1) → Icc a b),
-      StrictMono t ∧ t 0 = a ∧ t (Fin.last n) = b ∧
-      ∀ i : Fin n, ∃ j : ι, Icc (t i.castSucc) (t i.succ) ⊆ c j := by
-  -- Get Lebesgue number
-  obtain ⟨δ, δ_pos, hδ⟩ := lebesgue_number_lemma_of_metric isCompact_univ hc₁ hc₂
-  -- Pick n: if a = b then n = 0, otherwise pick n large enough so that (b - a) / n < δ
-  by_cases hab : a = b
-  · -- Case a = b: take n = 0 with single partition point
-    subst hab
-    exact ⟨0, fun _ => ⟨a, by simp⟩, Subsingleton.strictMono (α := Fin 1) _, rfl, rfl,
-      fun i => i.elim0⟩
-  · -- Case a < b: pick n with (b - a) / n < δ
-    have hab_pos : 0 < b - a := sub_pos.mpr (Ne.lt_of_le hab h)
-    obtain ⟨n, hn_pos, hn_small⟩ : ∃ n : ℕ, 0 < n ∧ (b - a) / n < δ := by
-      obtain ⟨n, hn⟩ := exists_nat_gt ((b - a) / δ)
-      have hn_pos : 0 < n := by
-        have h1 : 0 < (b - a) / δ := div_pos hab_pos δ_pos
-        have h2 : (0 : ℝ) < n := by linarith
-        exact Nat.cast_pos.mp h2
-      refine ⟨n, hn_pos, ?_⟩
-      have hn_pos' : (0 : ℝ) < n := Nat.cast_pos.mpr hn_pos
-      -- From (b - a) / δ < n, multiply both sides by δ to get b - a < n * δ
-      have h_mul : b - a < n * δ := calc
-        b - a = (b - a) / δ * δ := by field_simp [δ_pos.ne']
-        _ < n * δ := by nlinarith [δ_pos]
-      calc (b - a) / n < (n * δ) / n := by gcongr
-        _ = δ := by field_simp
-    -- Define partition: t k = a + k * (b - a) / n
-    let t : Fin (n + 1) → Icc a b := fun k => ⟨a + k * (b - a) / n, by
-      constructor
-      · linarith [mul_nonneg (Nat.cast_nonneg (k : ℕ)) (sub_nonneg.mpr h),
-          div_nonneg (mul_nonneg (Nat.cast_nonneg (k : ℕ)) (sub_nonneg.mpr h)) (Nat.cast_nonneg n)]
-      · have hk : (k : ℝ) ≤ n := Nat.cast_le.mpr (Nat.lt_succ_iff.mp k.is_lt)
-        have hn_pos' : (0 : ℝ) < n := Nat.cast_pos.mpr hn_pos
-        calc a + k * (b - a) / n ≤ a + n * (b - a) / n := by {
-              have : k * (b - a) ≤ n * (b - a) := by nlinarith
-              linarith [div_le_div_of_nonneg_right this hn_pos'.le] }
-          _ = b := by field_simp [hn_pos'.ne']; ring⟩
-    have ht_strict : StrictMono t := by
-      intro i j hij
-      change (t i : ℝ) < (t j : ℝ)
-      simp only [t]
-      have hij' : (i : ℝ) < (j : ℝ) := Nat.cast_lt.mpr hij
-      have hn_pos' : (0 : ℝ) < n := Nat.cast_pos.mpr hn_pos
-      have : i * (b - a) < j * (b - a) := by nlinarith [hab_pos]
-      linarith [div_lt_div_of_pos_right this hn_pos']
-    refine ⟨n, t, ht_strict, ?_, ?_, ?_⟩
-    · -- t 0 = a
-      simp [t]
-    · -- t (Fin.last n) = b
-      simp [t]
-      field_simp [Nat.cast_pos.mpr hn_pos]
-      ring
-    · -- Covering property
-      intro i
-      -- Use StrictMono to get that t i.castSucc < t i.succ
-      have h_mono : (t i.castSucc : ℝ) < (t i.succ : ℝ) := ht_strict i.castSucc_lt_succ
-      -- Define the midpoint
-      let m : Icc a b := ⟨((t i.castSucc : ℝ) + (t i.succ : ℝ)) / 2, by
-        constructor
-        · linarith [(t i.castSucc).2.1, (t i.succ).2.1]
-        · linarith [(t i.castSucc).2.2, (t i.succ).2.2]⟩
-      -- The segment is contained in ball m δ
-      have h_subset : Icc (t i.castSucc) (t i.succ) ⊆ Metric.ball m δ := by
-        intro x hx
-        simp only [Metric.ball, mem_setOf_eq]
-        have segment_len : (t i.succ : ℝ) - (t i.castSucc : ℝ) = (b - a) / n := by
-          simp [t]
-          field_simp
-          ring
-        -- x is in the segment, so its distance from midpoint is at most (b-a)/(2n) < δ
-        have hx_bounds : (t i.castSucc : ℝ) ≤ (x : ℝ) ∧ (x : ℝ) ≤ (t i.succ : ℝ) := ⟨hx.1, hx.2⟩
-        have dist_bound : dist (x : ℝ) (m : ℝ) ≤ ((b - a) / n) / 2 := by
-          rw [dist_comm, Real.dist_eq]
-          simp only [m, abs_sub_le_iff]
-          constructor <;>
-          · linarith [hx_bounds.1, hx_bounds.2, segment_len]
-        -- Since (b-a)/n < δ, we have (b-a)/(2n) < δ/2 < δ
-        calc dist (x : ℝ) (m : ℝ) ≤ ((b - a) / n) / 2 := dist_bound
-          _ < δ / 2 := by linarith [hn_small]
-          _ < δ := by linarith [δ_pos]
-      -- Apply Lebesgue number property to get the covering set
-      obtain ⟨j, hj⟩ := hδ m trivial
-      exact ⟨j, Subset.trans h_subset hj⟩
-
-/-- Finite partition variant: Any open cover of the unit interval can be refined to a finite
-partition with strictly monotone partition points indexed by `Fin (n + 1)`. -/
-lemma exists_strictMono_Icc_subset_open_cover_unitInterval {ι} {c : ι → Set I}
-    (hc₁ : ∀ i, IsOpen (c i)) (hc₂ : univ ⊆ ⋃ i, c i) :
-    ∃ (n : ℕ) (t : Fin (n + 1) → I),
-      StrictMono t ∧ t 0 = 0 ∧ t (Fin.last n) = 1 ∧
-      ∀ i : Fin n, ∃ j : ι, Icc (t i.castSucc) (t i.succ) ⊆ c j := by
-  obtain ⟨n, t, ht_strict, ht0, htn, ht_cover⟩ :=
-    exists_strictMono_Icc_subset_open_cover_Icc zero_le_one hc₁ hc₂
-  refine ⟨n, t, ht_strict, ?_, ?_, ht_cover⟩
-  · ext; exact ht0
-  · ext; exact htn
-
 end partition
 
 @[simp]