chore: golf using grind (leanprover-community#33286)

The goal of this golfing PR is to decrease the number of times lemmas are called explicitly (replacing calls to lemmas with calls to tactics). Any decrease in compilation time is a welcome side effect, although it is not a primary objective.

Trace profiling results (shown if ≥10 ms before or after):
* `AkraBazziRecurrence.GrowsPolynomially.eventually_atTop_nonneg_or_nonpos`: 1208 ms before, 917 ms after  🎉
* `Equiv.Perm.support_congr`: <10 ms before, 38 ms after
* `Equiv.Perm.subtypeCongr.trans`: 13 ms before, 35 ms after
* `preCantorSet_antitone`: 766 ms before, 371 ms after  🎉

This golfing PR is batched under the following guidelines:
* Up to ~5 changed files per PR
* Up to ~25 changed declarations per PR
* Up to ~100 changed lines per PR

Author: euprunin

Mathlib/Computability/AkraBazzi/GrowsPolynomially.lean

@@ -189,45 +189,14 @@ lemma eventually_atTop_nonneg_or_nonpos (hf : GrowsPolynomially f) :
       rw [eventually_atTop]
       refine ⟨max n₀ 2, ?_⟩
       refine Real.induction_Ico_mul _ 2 (by norm_num) (by positivity) ?base ?step
-      case base =>
-        intro x ⟨hxlb, hxub⟩
-        have h₁ := calc n₀ ≤ 1 * max n₀ 2 := by simp
-                        _ ≤ 2 * max n₀ 2 := by gcongr; norm_num
-        have h₂ := hn₀ (2 * max n₀ 2) h₁ (max n₀ 2) ⟨by simp, by linarith⟩
-        rw [h₂]
-        exact hn₀ (2 * max n₀ 2) h₁ x ⟨by simp [hxlb], le_of_lt hxub⟩
+      case base => grind
       case step =>
-        intro n hn hyp_ind z hz
-        have z_nonneg : 0 ≤ z := by
-          calc (0 : ℝ) ≤ (2 : ℝ) ^ n * max n₀ 2 := by
-                        exact mul_nonneg (pow_nonneg (by norm_num) _) (by norm_num)
-                  _ ≤ z := by exact_mod_cast hz.1
+        intro n _ _ z _
         have le_2n : max n₀ 2 ≤ (2 : ℝ) ^ n * max n₀ 2 := by
-          nth_rewrite 1 [← one_mul (max n₀ 2)]
-          gcongr
-          exact one_le_pow₀ (by norm_num : (1 : ℝ) ≤ 2)
-        have n₀_le_z : n₀ ≤ z := by
-          calc n₀ ≤ max n₀ 2 := by simp
-                _ ≤ (2 : ℝ) ^ n * max n₀ 2 := le_2n
-                _ ≤ _ := by exact_mod_cast hz.1
-        have fz_eq_c₂fz : f z = c₂ * f z := hn₀ z n₀_le_z z ⟨by linarith, le_rfl⟩
-        have z_to_half_z' : f (1 / 2 * z) = c₂ * f z :=
-          hn₀ z n₀_le_z (1 / 2 * z) ⟨le_rfl, by linarith⟩
-        have z_to_half_z : f (1 / 2 * z) = f z := by rwa [← fz_eq_c₂fz] at z_to_half_z'
+          simp [one_le_pow₀ (show (1 : ℝ) ≤ 2 by norm_num1)]
         have half_z_to_base : f (1 / 2 * z) = f (max n₀ 2) := by
-          refine hyp_ind (1 / 2 * z) ⟨?lb, ?ub⟩
-          case lb =>
-            calc max n₀ 2 ≤ (1 / 2 : ℝ) * (2 : ℝ) ^ 1 * max n₀ 2 := by simp
-                        _ ≤ (1 / 2 : ℝ) * (2 : ℝ) ^ n * max n₀ 2 := by gcongr; norm_num
-                        _ ≤ _ := by rw [mul_assoc]; gcongr; exact_mod_cast hz.1
-          case ub =>
-            have h₁ : (2 : ℝ) ^ n = (1 / 2 : ℝ) * (2 : ℝ) ^ (n + 1) := by
-              rw [one_div, pow_add, pow_one]
-              ring
-            rw [h₁, mul_assoc]
-            gcongr
-            exact_mod_cast hz.2
-        rw [← z_to_half_z, half_z_to_base]
+          grind [mul_assoc]
+        grind
     obtain ⟨c, hc⟩ := hmain
     cases le_or_gt 0 c with
     | inl hpos =>

Mathlib/GroupTheory/Perm/Support.lean

@@ -290,11 +290,7 @@ theorem support_refl : support (Equiv.refl α) = ∅ :=
   support_one
 
 theorem support_congr (h : f.support ⊆ g.support) (h' : ∀ x ∈ g.support, f x = g x) : f = g := by
-  ext x
-  by_cases hx : x ∈ g.support
-  · exact h' x hx
-  · rw [notMem_support.mp hx, ← notMem_support]
-    exact fun H => hx (h H)
+  grind [notMem_support]
 
 /-- If g and c commute, then g stabilizes the support of c -/
 theorem mem_support_iff_of_commute {g c : Perm α} (hgc : Commute g c) (x : α) :

Mathlib/Logic/Equiv/Basic.lean

@@ -97,12 +97,7 @@ theorem Perm.subtypeCongr.symm : (ep.subtypeCongr en).symm = Perm.subtypeCongr e
 theorem Perm.subtypeCongr.trans :
     (ep.subtypeCongr en).trans (ep'.subtypeCongr en')
     = Perm.subtypeCongr (ep.trans ep') (en.trans en') := by
-  ext x
-  by_cases h : p x
-  · have : p (ep ⟨x, h⟩) := Subtype.property _
-    simp [h, this]
-  · have : ¬p (en ⟨x, h⟩) := Subtype.property (en _)
-    simp [h, this]
+  grind [eq_def, coe_trans]
 
 end subtypeCongr
 

Mathlib/Topology/Instances/CantorSet.lean

@@ -88,16 +88,9 @@ lemma zero_mem_preCantorSet (n : ℕ) : 0 ∈ preCantorSet n := by
 theorem zero_mem_cantorSet : 0 ∈ cantorSet := by simp [cantorSet, zero_mem_preCantorSet]
 
 theorem preCantorSet_antitone : Antitone preCantorSet := by
-  apply antitone_nat_of_succ_le
-  intro m
-  simp only [Set.le_eq_subset, preCantorSet_succ, Set.union_subset_iff]
-  induction m with
-  | zero =>
-    simp only [preCantorSet_zero]
-    constructor <;> intro x <;>
-      simp only [Set.mem_image, Set.mem_Icc, forall_exists_index, and_imp] <;>
-      intro y _ _ _ <;> constructor <;> linarith
-  | succ m ih => grind [preCantorSet_succ, Set.image_union]
+  refine antitone_nat_of_succ_le fun m ↦ ?_
+  simp only [Set.le_eq_subset]
+  induction m with grind [preCantorSet_zero, preCantorSet_succ]
 
 lemma preCantorSet_subset_unitInterval {n : ℕ} : preCantorSet n ⊆ Set.Icc 0 1 := by
   rw [← preCantorSet_zero]