feat: grind golfing in Topology/Path (#31305)

This is not as exhaustive as I would have liked; there's plenty more cleanup to do here. But I need to pause on this for now and I think it's an improvement.

Author: kim-em

Mathlib/Algebra/Order/Interval/Set/Instances.lean

@@ -64,11 +64,11 @@ theorem coe_zero : ↑(0 : Icc (0 : R) 1) = (0 : R) :=
 theorem coe_one : ↑(1 : Icc (0 : R) 1) = (1 : R) :=
   rfl
 
-@[simp]
+@[simp, grind =]
 theorem mk_zero (h : (0 : R) ∈ Icc (0 : R) 1) : (⟨0, h⟩ : Icc (0 : R) 1) = 0 :=
   rfl
 
-@[simp]
+@[simp, grind =]
 theorem mk_one (h : (1 : R) ∈ Icc (0 : R) 1) : (⟨1, h⟩ : Icc (0 : R) 1) = 1 :=
   rfl
 
@@ -169,7 +169,7 @@ instance instZero [Nontrivial R] : Zero (Ico (0 : R) 1) where zero := ⟨0, by s
 theorem coe_zero [Nontrivial R] : ↑(0 : Ico (0 : R) 1) = (0 : R) :=
   rfl
 
-@[simp]
+@[simp, grind =]
 theorem mk_zero [Nontrivial R] (h : (0 : R) ∈ Ico (0 : R) 1) : (⟨0, h⟩ : Ico (0 : R) 1) = 0 :=
   rfl
 
@@ -225,7 +225,7 @@ instance instOne : One (Ioc (0 : R) 1) where one := ⟨1, ⟨zero_lt_one, le_ref
 theorem coe_one : ↑(1 : Ioc (0 : R) 1) = (1 : R) :=
   rfl
 
-@[simp]
+@[simp, grind =]
 theorem mk_one (h : (1 : R) ∈ Ioc (0 : R) 1) : (⟨1, h⟩ : Ioc (0 : R) 1) = 1 :=
   rfl
 

Mathlib/AlgebraicTopology/FundamentalGroupoid/Basic.lean

@@ -38,36 +38,19 @@ def reflTransSymmAux (x : I × I) : ℝ :=
   if (x.2 : ℝ) ≤ 1 / 2 then x.1 * 2 * x.2 else x.1 * (2 - 2 * x.2)
 
 @[continuity, fun_prop]
-theorem continuous_reflTransSymmAux : Continuous reflTransSymmAux := by
-  refine continuous_if_le ?_ ?_ (Continuous.continuousOn ?_) (Continuous.continuousOn ?_) ?_
-  iterate 4 fun_prop
-  intro x hx
-  norm_num [hx, mul_assoc]
+theorem continuous_reflTransSymmAux : Continuous reflTransSymmAux :=
+  continuous_if_le (by fun_prop) (by fun_prop) (by fun_prop) (by fun_prop) (by grind)
 
 theorem reflTransSymmAux_mem_I (x : I × I) : reflTransSymmAux x ∈ I := by
   dsimp only [reflTransSymmAux]
   split_ifs
   · constructor
-    · apply mul_nonneg
-      · apply mul_nonneg
-        · unit_interval
-        · simp
-      · unit_interval
+    · apply mul_nonneg <;> grind
     · rw [mul_assoc]
-      apply mul_le_one₀
-      · unit_interval
-      · apply mul_nonneg
-        · simp
-        · unit_interval
-      · linarith
+      apply mul_le_one₀ <;> grind
   · constructor
-    · apply mul_nonneg
-      · unit_interval
-      linarith [unitInterval.nonneg x.2, unitInterval.le_one x.2]
-    · apply mul_le_one₀
-      · unit_interval
-      · linarith [unitInterval.nonneg x.2, unitInterval.le_one x.2]
-      · linarith [unitInterval.nonneg x.2, unitInterval.le_one x.2]
+    · apply mul_nonneg <;> grind
+    · apply mul_le_one₀ <;> grind
 
 /-- For any path `p` from `x₀` to `x₁`, we have a homotopy from the constant path based at `x₀` to
   `p.trans p.symm`. -/
@@ -78,10 +61,10 @@ def reflTransSymm (p : Path x₀ x₁) : Homotopy (Path.refl x₀) (p.trans p.sy
   map_one_left x := by
     simp only [reflTransSymmAux, Path.trans]
     cases le_or_gt (x : ℝ) 2⁻¹ with
-    | inl hx => simp [hx, ← extend_extends]
+    | inl hx => simp [hx, ← extend_apply]
     | inr hx =>
       have : p.extend (2 - 2 * ↑x) = p.extend (1 - (2 * ↑x - 1)) := by ring_nf
-      simpa [hx.not_ge, ← extend_extends]
+      simpa [hx.not_ge, ← extend_apply]
   prop' t := by norm_num [reflTransSymmAux]
 
 /-- For any path `p` from `x₀` to `x₁`, we have a homotopy from the constant path based at `x₁` to
@@ -98,11 +81,8 @@ def transReflReparamAux (t : I) : ℝ :=
   if (t : ℝ) ≤ 1 / 2 then 2 * t else 1
 
 @[continuity, fun_prop]
-theorem continuous_transReflReparamAux : Continuous transReflReparamAux := by
-  refine continuous_if_le ?_ ?_ (Continuous.continuousOn ?_) (Continuous.continuousOn ?_) ?_ <;>
-    [fun_prop; fun_prop; fun_prop; fun_prop; skip]
-  intro x hx
-  simp [hx]
+theorem continuous_transReflReparamAux : Continuous transReflReparamAux :=
+  continuous_if_le (by fun_prop) (by fun_prop) (by fun_prop) (by fun_prop) (by grind)
 
 theorem transReflReparamAux_mem_I (t : I) : transReflReparamAux t ∈ I := by
   unfold transReflReparamAux
@@ -120,12 +100,8 @@ theorem trans_refl_reparam (p : Path x₀ x₁) :
         (Subtype.ext transReflReparamAux_zero) (Subtype.ext transReflReparamAux_one) := by
   ext
   unfold transReflReparamAux
-  simp only [Path.trans_apply, coe_reparam, Function.comp_apply, one_div, Path.refl_apply]
-  split_ifs
-  · rfl
-  · rfl
-  · simp
-  · simp
+  simp only [coe_reparam]
+  grind
 
 /-- For any path `p` from `x₀` to `x₁`, we have a homotopy from `p.trans (Path.refl x₁)` to `p`. -/
 def transRefl (p : Path x₀ x₁) : Homotopy (p.trans (Path.refl x₁)) p :=
@@ -147,15 +123,10 @@ def transAssocReparamAux (t : I) : ℝ :=
   if (t : ℝ) ≤ 1 / 4 then 2 * t else if (t : ℝ) ≤ 1 / 2 then t + 1 / 4 else 1 / 2 * (t + 1)
 
 @[continuity, fun_prop]
-theorem continuous_transAssocReparamAux : Continuous transAssocReparamAux := by
-  refine continuous_if_le ?_ ?_ (Continuous.continuousOn ?_)
-    (continuous_if_le ?_ ?_
-      (Continuous.continuousOn ?_) (Continuous.continuousOn ?_) ?_).continuousOn
-      ?_ <;>
-    [fun_prop; fun_prop; fun_prop; fun_prop; fun_prop; fun_prop; fun_prop; skip;
-      skip] <;>
-    · intro x hx
-      norm_num [hx]
+theorem continuous_transAssocReparamAux : Continuous transAssocReparamAux :=
+  continuous_if_le (by fun_prop) (by fun_prop) (by fun_prop)
+    (continuous_if_le (by fun_prop) (by fun_prop) (by fun_prop) (by fun_prop)
+      (by grind)).continuousOn (by grind)
 
 theorem transAssocReparamAux_mem_I (t : I) : transAssocReparamAux t ∈ I := by
   unfold transAssocReparamAux
@@ -173,16 +144,12 @@ theorem trans_assoc_reparam {x₀ x₁ x₂ x₃ : X} (p : Path x₀ x₁) (q :
         (fun t => ⟨transAssocReparamAux t, transAssocReparamAux_mem_I t⟩) (by fun_prop)
         (Subtype.ext transAssocReparamAux_zero) (Subtype.ext transAssocReparamAux_one) := by
   ext x
-  simp only [transAssocReparamAux, Path.trans_apply, Function.comp_apply, mul_ite, Path.coe_reparam]
-  -- TODO: why does split_ifs not reduce the ifs??????
-  split_ifs with h₁ h₂ h₃ h₄ h₅
-  · rfl
-  iterate 6 exfalso; linarith
-  · have h : 2 * (2 * (x : ℝ)) - 1 = 2 * (2 * (↑x + 1 / 4) - 1) := by linarith
-    simp [h]
-  iterate 6 exfalso; linarith
-  · congr
-    ring
+  simp only [transAssocReparamAux, Path.trans_apply, Function.comp_apply, Path.coe_reparam]
+  split_ifs
+  iterate 12 grind
+  · linarith
+  · linarith
+  · grind
 
 /-- For paths `p q r`, we have a homotopy from `(p.trans q).trans r` to `p.trans (q.trans r)`. -/
 def transAssoc {x₀ x₁ x₂ x₃ : X} (p : Path x₀ x₁) (q : Path x₁ x₂) (r : Path x₂ x₃) :

Mathlib/Topology/Homotopy/Path.lean

@@ -67,6 +67,7 @@ theorem target (F : Homotopy p₀ p₁) (t : I) : F (t, 1) = x₁ :=
 
 /-- Evaluating a path homotopy at an intermediate point, giving us a `Path`.
 -/
+@[simps]
 def eval (F : Homotopy p₀ p₁) (t : I) : Path x₀ x₁ where
   toFun := F.toHomotopy.curry t
   source' := by simp
@@ -75,12 +76,12 @@ def eval (F : Homotopy p₀ p₁) (t : I) : Path x₀ x₁ where
 @[simp]
 theorem eval_zero (F : Homotopy p₀ p₁) : F.eval 0 = p₀ := by
   ext t
-  simp [eval]
+  simp
 
 @[simp]
 theorem eval_one (F : Homotopy p₀ p₁) : F.eval 1 = p₁ := by
   ext t
-  simp [eval]
+  simp
 
 end
 
@@ -163,7 +164,7 @@ theorem hcomp_apply (F : Homotopy p₀ q₀) (G : Homotopy p₁ q₁) (x : I ×
       else
         G.eval x.1
           ⟨2 * x.2 - 1, unitInterval.two_mul_sub_one_mem_iff.2 ⟨(not_le.1 h).le, x.2.2.2⟩⟩ :=
-  show ite _ _ _ = _ by split_ifs <;> exact Path.extend_extends _ _
+  show ite _ _ _ = _ by split_ifs <;> exact Path.extend_apply _ _
 
 theorem hcomp_half (F : Homotopy p₀ q₀) (G : Homotopy p₁ q₁) (t : I) :
     F.hcomp G (t, ⟨1 / 2, by norm_num, by norm_num⟩) = x₁ :=

Mathlib/Topology/Path.lean

@@ -66,7 +66,7 @@ instance Path.instFunLike : FunLike (Path x y) I X where
 instance Path.continuousMapClass : ContinuousMapClass (Path x y) I X where
   map_continuous γ := show Continuous γ.toContinuousMap by fun_prop
 
-@[ext]
+@[ext, grind ext]
 protected theorem Path.ext : ∀ {γ₁ γ₂ : Path x y}, (γ₁ : I → X) = γ₂ → γ₁ = γ₂ := by
   rintro ⟨⟨x, h11⟩, h12, h13⟩ ⟨⟨x, h21⟩, h22, h23⟩ rfl
   rfl
@@ -87,11 +87,11 @@ variable (γ : Path x y)
 protected theorem continuous : Continuous γ :=
   γ.continuous_toFun
 
-@[simp]
+@[simp, grind =]
 protected theorem source : γ 0 = x :=
   γ.source'
 
-@[simp]
+@[simp, grind =]
 protected theorem target : γ 1 = y :=
   γ.target'
 
@@ -123,16 +123,16 @@ instance instHasUncurryPath {α : Type*} {x y : α → X} :
     HasUncurry (∀ a : α, Path (x a) (y a)) (α × I) X :=
   ⟨fun φ p => φ p.1 p.2⟩
 
-@[simp high]
+@[simp high, grind! .]
 lemma source_mem_range (γ : Path x y) : x ∈ range ⇑γ :=
   ⟨0, Path.source γ⟩
 
-@[simp high]
+@[simp high, grind! .]
 lemma target_mem_range (γ : Path x y) : y ∈ range ⇑γ :=
   ⟨1, Path.target γ⟩
 
 /-- The constant path from a point to itself -/
-@[refl, simps!]
+@[refl, simps! (attr := grind =)]
 def refl (x : X) : Path x x where
   toContinuousMap  := .const I x
   source' := rfl
@@ -142,18 +142,15 @@ def refl (x : X) : Path x x where
 theorem refl_range {a : X} : range (Path.refl a) = {a} := range_const
 
 /-- The reverse of a path from `x` to `y`, as a path from `y` to `x` -/
-@[symm, simps]
+@[symm, simps (attr := grind =)]
 def symm (γ : Path x y) : Path y x where
   toFun := γ ∘ σ
   continuous_toFun := by fun_prop
   source' := by simp
   target' := by simp
 
 @[simp]
-theorem symm_symm (γ : Path x y) : γ.symm.symm = γ := by
-  ext t
-  change γ (σ (σ t)) = γ t
-  rw [unitInterval.symm_symm]
+theorem symm_symm (γ : Path x y) : γ.symm.symm = γ := by grind
 
 theorem symm_bijective : Function.Bijective (Path.symm : Path x y → Path y x) :=
   Function.bijective_iff_has_inverse.mpr ⟨_, symm_symm, symm_symm⟩
@@ -218,11 +215,14 @@ theorem _root_.ContinuousAt.pathExtend {g : Y → ℝ} {l r : Y → X} (γ : ∀
 @[deprecated (since := "2025-05-02")]
 alias _root_.ContinuousAt.path_extend := ContinuousAt.pathExtend
 
-@[simp]
-theorem extend_extends {a b : X} (γ : Path a b) {t : ℝ}
+@[simp, grind =]
+theorem extend_apply {a b : X} (γ : Path a b) {t : ℝ}
     (ht : t ∈ (Icc 0 1 : Set ℝ)) : γ.extend t = γ ⟨t, ht⟩ :=
   IccExtend_of_mem _ γ ht
 
+@[deprecated (since := "2025-11-05")]
+alias extend_extends := extend_apply
+
 theorem extend_zero : γ.extend 0 = x := by simp
 
 theorem extend_one : γ.extend 1 = y := by simp
@@ -289,11 +289,12 @@ def trans (γ : Path x y) (γ' : Path y z) : Path x z where
   source' := by simp
   target' := by norm_num
 
+@[grind =]
 theorem trans_apply (γ : Path x y) (γ' : Path y z) (t : I) :
     (γ.trans γ') t =
       if h : (t : ℝ) ≤ 1 / 2 then γ ⟨2 * t, (mul_pos_mem_iff zero_lt_two).2 ⟨t.2.1, h⟩⟩
       else γ' ⟨2 * t - 1, two_mul_sub_one_mem_iff.2 ⟨(not_le.1 h).le, t.2.2⟩⟩ :=
-  show ite _ _ _ = _ by split_ifs <;> rw [extend_extends]
+  show ite _ _ _ = _ by split_ifs <;> rw [extend_apply]
 
 @[simp]
 theorem trans_symm (γ : Path x y) (γ' : Path y z) : (γ.trans γ').symm = γ'.symm.trans γ.symm := by
@@ -314,7 +315,7 @@ theorem extend_trans_of_le_half (γ₁ : Path x y) (γ₂ : Path y z) {t : ℝ}
     (γ₁.trans γ₂).extend t = γ₁.extend (2 * t) := by
   obtain _ | ht₀ := le_total t 0
   · repeat rw [extend_of_le_zero _ (by linarith)]
-  · rwa [extend_extends _ ⟨ht₀, by linarith⟩, trans_apply, dif_pos, extend_extends]
+  · rwa [extend_apply _ ⟨ht₀, by linarith⟩, trans_apply, dif_pos, extend_apply]
 
 theorem extend_trans_of_half_le (γ₁ : Path x y) (γ₂ : Path y z) {t : ℝ} (ht : 1 / 2 ≤ t) :
     (γ₁.trans γ₂).extend t = γ₂.extend (2 * t - 1) := by
@@ -349,7 +350,7 @@ def map' (γ : Path x y) {f : X → Y} (h : ContinuousOn f (range γ)) : Path (f
 def map (γ : Path x y) {f : X → Y} (h : Continuous f) :
     Path (f x) (f y) := γ.map' h.continuousOn
 
-@[simp]
+@[simp, grind =]
 theorem map_coe (γ : Path x y) {f : X → Y} (h : Continuous f) :
     (γ.map h : I → Y) = f ∘ γ := by
   ext t
@@ -364,8 +365,8 @@ theorem map_symm (γ : Path x y) {f : X → Y} (h : Continuous f) :
 theorem map_trans (γ : Path x y) (γ' : Path y z) {f : X → Y}
     (h : Continuous f) : (γ.trans γ').map h = (γ.map h).trans (γ'.map h) := by
   ext t
-  rw [trans_apply, map_coe, Function.comp_apply, trans_apply]
-  split_ifs <;> rfl
+  rw [trans_apply, map_coe, Function.comp_apply, trans_apply, map_coe, map_coe]
+  grind
 
 @[simp]
 theorem map_id (γ : Path x y) : γ.map continuous_id = γ := by
@@ -478,19 +479,18 @@ protected def prod (γ₁ : Path a₁ a₂) (γ₂ : Path b₁ b₂) : Path (a
   source' := by simp
   target' := by simp
 
-@[simp]
+@[simp, grind =]
 theorem prod_coe (γ₁ : Path a₁ a₂) (γ₂ : Path b₁ b₂) :
     ⇑(γ₁.prod γ₂) = fun t => (γ₁ t, γ₂ t) :=
   rfl
 
 /-- Path composition commutes with products -/
 theorem trans_prod_eq_prod_trans (γ₁ : Path a₁ a₂) (δ₁ : Path a₂ a₃) (γ₂ : Path b₁ b₂)
     (δ₂ : Path b₂ b₃) : (γ₁.prod γ₂).trans (δ₁.prod δ₂) = (γ₁.trans δ₁).prod (γ₂.trans δ₂) := by
+  unfold Path.trans
   ext t <;>
-  unfold Path.trans <;>
-  simp only [Path.coe_mk_mk, Path.prod_coe, Function.comp_apply] <;>
-  split_ifs <;>
-  rfl
+  · simp only [Path.coe_mk_mk, Path.prod_coe]
+    grind
 
 end Prod
 
@@ -505,7 +505,7 @@ protected def pi (γ : ∀ i, Path (as i) (bs i)) : Path as bs where
   source' := by simp
   target' := by simp
 
-@[simp]
+@[simp, grind =]
 theorem pi_coe (γ : ∀ i, Path (as i) (bs i)) : ⇑(Path.pi γ) = fun t i => γ i t :=
   rfl
 
@@ -515,7 +515,9 @@ theorem trans_pi_eq_pi_trans (γ₀ : ∀ i, Path (as i) (bs i)) (γ₁ : ∀ i,
   ext t i
   unfold Path.trans
   simp only [Path.coe_mk_mk, Function.comp_apply, pi_coe]
-  split_ifs <;> rfl
+  split_ifs
+  · rfl
+  · rfl
 
 end Pi
 

Mathlib/Topology/UnitInterval.lean

@@ -69,23 +69,23 @@ def symm : I → I := fun t => ⟨1 - t, Icc.mem_iff_one_sub_mem.mp t.prop⟩
 @[inherit_doc]
 scoped notation "σ" => unitInterval.symm
 
-@[simp]
+@[simp, grind =]
 theorem symm_zero : σ 0 = 1 :=
   Subtype.ext <| by simp [symm]
 
-@[simp]
+@[simp, grind =]
 theorem symm_one : σ 1 = 0 :=
   Subtype.ext <| by simp [symm]
 
-@[simp]
+@[simp, grind =]
 theorem symm_symm (x : I) : σ (σ x) = x :=
   Subtype.ext <| by simp [symm]
 
 theorem symm_involutive : Function.Involutive (symm : I → I) := symm_symm
 
 theorem symm_bijective : Function.Bijective (symm : I → I) := symm_involutive.bijective
 
-@[simp]
+@[simp, grind =]
 theorem coe_symm_eq (x : I) : (σ x : ℝ) = 1 - x :=
   rfl