feat: miscellaneous grind golfs (#29700)

Author: kim-em

Mathlib/Algebra/Order/Floor/Ring.lean

@@ -315,8 +315,7 @@ theorem fract_sub_self (a : R) : fract a - a = -⌊a⌋ :=
 theorem fract_add (a b : R) : ∃ z : ℤ, fract (a + b) - fract a - fract b = z :=
   ⟨⌊a⌋ + ⌊b⌋ - ⌊a + b⌋, by
     unfold fract
-    simp only [sub_eq_add_neg, neg_add_rev, neg_neg, cast_add, cast_neg]
-    abel⟩
+    grind⟩
 
 variable [IsStrictOrderedRing R]
 

Mathlib/Algebra/Polynomial/Derivative.lean

@@ -255,9 +255,7 @@ theorem derivative_mul {f g : R[X]} : derivative (f * g) = derivative f * g + f
   | succ m =>
   cases n with
   | zero => simp only [add_zero, Nat.cast_zero, mul_zero, map_zero]
-  | succ n =>
-  simp only [Nat.add_succ_sub_one, add_tsub_cancel_right]
-  rw [add_assoc, add_comm n 1]
+  | succ n => grind
 
 theorem derivative_eval (p : R[X]) (x : R) :
     p.derivative.eval x = p.sum fun n a => a * n * x ^ (n - 1) := by

Mathlib/Combinatorics/Matroid/Map.lean

@@ -162,9 +162,7 @@ def comap (N : Matroid β) (f : α → β) : Matroid α :=
 @[simp] lemma comap_dep_iff :
     (N.comap f).Dep I ↔ N.Dep (f '' I) ∨ (N.Indep (f '' I) ∧ ¬ InjOn f I) := by
   rw [Dep, comap_indep_iff, not_and, comap_ground_eq, Dep, image_subset_iff]
-  refine ⟨fun ⟨hi, h⟩ ↦ ?_, ?_⟩
-  · rw [and_iff_left h, ← imp_iff_not_or]
-    exact fun hI ↦ ⟨hI, hi hI⟩
+  refine ⟨by grind, ?_⟩
   rintro (⟨hI, hIE⟩ | hI)
   · exact ⟨fun h ↦ (hI h).elim, hIE⟩
   rw [iff_true_intro hI.1, iff_true_intro hI.2, implies_true, true_and]
@@ -459,9 +457,7 @@ lemma map_comap {f : α → β} (h_range : N.E ⊆ range f) (hf : InjOn f (f ⁻
     (N.comap f).map f hf = N := by
   refine ext_indep (by simpa [image_preimage_eq_iff]) ?_
   simp only [map_ground, comap_ground_eq, map_indep_iff, comap_indep_iff, forall_subset_image_iff]
-  refine fun I hI ↦ ⟨fun ⟨I₀, ⟨hI₀, _⟩, hII₀⟩ ↦ ?_, fun h ↦ ⟨_, ⟨h, hf.mono hI⟩, rfl⟩⟩
-  suffices h : I₀ ⊆ f ⁻¹' N.E by rw [InjOn.image_eq_image_iff hf hI h] at hII₀; rwa [hII₀]
-  exact (subset_preimage_image f I₀).trans <| preimage_mono (f := f) hI₀.subset_ground
+  exact fun I hI ↦ ⟨by grind, fun h ↦ ⟨_, ⟨h, hf.mono hI⟩, rfl⟩⟩
 
 lemma comap_map {f : α → β} (hf : f.Injective) : (M.map f hf.injOn).comap f = M := by
   simp [ext_iff_indep, preimage_image_eq _ hf, and_iff_left hf.injOn,

Mathlib/Data/Int/Init.lean

@@ -107,7 +107,7 @@ where
   neg : ∀ n : ℕ, motive (b + -[n+1])
   | 0 => pred _ Int.le_rfl zero
   | n + 1 => by
-    refine cast (by rw [Int.add_sub_assoc]; rfl) (pred _ (Int.le_of_lt ?_) (neg n))
+    refine cast (by cutsat) (pred _ (Int.le_of_lt ?_) (neg n))
     cutsat
 
 variable {z b zero succ pred}
@@ -143,13 +143,7 @@ end inductionOn'
 @[elab_as_elim]
 protected lemma le_induction {m : ℤ} {motive : ∀ n, m ≤ n → Prop} (base : motive m m.le_refl)
     (succ : ∀ n hmn, motive n hmn → motive (n + 1) (le_add_one hmn)) : ∀ n hmn, motive n hmn := by
-  refine fun n ↦ Int.inductionOn' n m ?_ ?_ ?_
-  · intro
-    exact base
-  · intro k hle hi _
-    exact succ k hle (hi hle)
-  · intro k hle _ hle'
-    cutsat
+  refine fun n ↦ Int.inductionOn' n m ?_ ?_ ?_ <;> grind
 
 /-- See `Int.inductionOn'` for an induction in both directions. -/
 @[elab_as_elim]

Mathlib/Data/Nat/Bits.lean

@@ -3,12 +3,12 @@ Copyright (c) 2022 Praneeth Kolichala. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Praneeth Kolichala
 -/
-import Mathlib.Data.Nat.Basic
 import Mathlib.Data.Nat.BinaryRec
 import Mathlib.Data.List.Defs
 import Mathlib.Tactic.Convert
 import Mathlib.Tactic.GeneralizeProofs
 import Mathlib.Tactic.Says
+import Mathlib.Util.AssertExists
 
 /-!
 # Additional properties of binary recursion on `Nat`
@@ -101,6 +101,7 @@ lemma bodd_add_div2 : ∀ n, (bodd n).toNat + 2 * div2 n = n
     · simp
     · simp; cutsat
 
+@[grind =]
 lemma div2_val (n) : div2 n = n / 2 := by
   refine Nat.eq_of_mul_eq_mul_left (by decide)
     (Nat.add_left_cancel (Eq.trans ?_ (Nat.mod_add_div n 2).symm))
@@ -138,12 +139,7 @@ lemma shiftLeft'_false : ∀ n, shiftLeft' false m n = m <<< n
 @[simp] lemma shiftLeft_eq' (m n : Nat) : shiftLeft m n = m <<< n := rfl
 @[simp] lemma shiftRight_eq (m n : Nat) : shiftRight m n = m >>> n := rfl
 
-lemma binaryRec_decreasing (h : n ≠ 0) : div2 n < n := by
-  rw [div2_val]
-  apply (div_lt_iff_lt_mul <| succ_pos 1).2
-  have := Nat.mul_lt_mul_of_pos_left (lt_succ_self 1)
-    (lt_of_le_of_ne n.zero_le h.symm)
-  rwa [Nat.mul_one] at this
+lemma binaryRec_decreasing (h : n ≠ 0) : div2 n < n := by grind
 
 /-- `size n` : Returns the size of a natural number in
 bits i.e. the length of its binary representation -/

Mathlib/Data/Nat/Digits/Lemmas.lean

@@ -28,7 +28,7 @@ theorem ofDigits_eq_sum_mapIdx_aux (b : ℕ) (l : List ℕ) :
     l.zipWith (fun a i : ℕ => a * b ^ (i + 1)) (List.range l.length) =
       l.zipWith (fun a i=> b * (a * b ^ i)) (List.range l.length)
     by simp [this]
-  congr; ext; simp [pow_succ]; ring
+  congr; ext; ring
 
 theorem ofDigits_eq_sum_mapIdx (b : ℕ) (L : List ℕ) :
     ofDigits b L = (L.mapIdx fun i a => a * b ^ i).sum := by

Mathlib/Data/Nat/Size.lean

@@ -6,6 +6,7 @@ Authors: Floris van Doorn, Leonardo de Moura, Jeremy Avigad, Mario Carneiro
 import Mathlib.Algebra.Group.Nat.Defs
 import Mathlib.Algebra.Group.Basic
 import Mathlib.Data.Nat.Bits
+import Mathlib.Data.Nat.Basic
 
 /-! Lemmas about `size`. -/
 

Mathlib/Data/PEquiv.lean

@@ -386,17 +386,7 @@ instance [DecidableEq α] [DecidableEq β] : SemilatticeInf (α ≃. β) :=
           have hf := @mem_iff_mem _ _ f a b
           have hg := @mem_iff_mem _ _ g a b
           simp only [Option.mem_def] at *
-          split_ifs with h1 h2 h2 <;> try simp [hf]
-          · contrapose! h2
-            rw [h2]
-            rw [← h1, hf, h2] at hg
-            simp only [true_iff] at hg
-            rw [hg]
-          · contrapose! h1
-            rw [h1] at hf h2
-            rw [← h2] at hg
-            simp only [iff_true] at hf hg
-            rw [hf, hg] }
+          grind }
     inf_le_left := fun _ _ _ _ => by simp only [coe_mk, mem_def]; split_ifs <;> simp [*]
     inf_le_right := fun _ _ _ _ => by simp only [coe_mk, mem_def]; split_ifs <;> simp [*]
     le_inf := fun f g h fg gh a b => by

Mathlib/MeasureTheory/Constructions/Cylinders.lean

@@ -122,9 +122,7 @@ theorem comap_eval_le_generateFrom_squareCylinders_singleton
       convert ht
       simp only [cast_heq]
     · simp only [hji, not_false_iff, dif_neg, MeasurableSet.univ]
-  · simp only [eq_mpr_eq_cast, ← h]
-    ext1 x
-    simp only [Function.eval, cast_eq, dite_eq_ite, ite_true, mem_preimage]
+  · grind
 
 /-- The square cylinders formed from measurable sets generate the product σ-algebra. -/
 theorem generateFrom_squareCylinders [∀ i, MeasurableSpace (α i)] :

Mathlib/MeasureTheory/PiSystem.lean

@@ -407,17 +407,8 @@ theorem isPiSystem_piiUnionInter (π : ι → Set (Set α)) (hpi : ∀ x, IsPiSy
     rw [ht1_eq, ht2_eq]
     simp_rw [← Set.inf_eq_inter]
     ext1 x
-    simp only [g, inf_eq_inter, mem_inter_iff, mem_iInter, Finset.mem_union]
-    refine ⟨fun h i _ => ?_, fun h => ⟨fun i hi1 => ?_, fun i hi2 => ?_⟩⟩
-    · split_ifs with h_1 h_2 h_2
-      exacts [⟨h.1 i h_1, h.2 i h_2⟩, ⟨h.1 i h_1, Set.mem_univ _⟩, ⟨Set.mem_univ _, h.2 i h_2⟩,
-        ⟨Set.mem_univ _, Set.mem_univ _⟩]
-    · specialize h i (Or.inl hi1)
-      rw [if_pos hi1] at h
-      exact h.1
-    · specialize h i (Or.inr hi2)
-      rw [if_pos hi2] at h
-      exact h.2
+    simp only [inf_eq_inter, mem_inter_iff, mem_iInter]
+    grind
   refine ⟨fun n hn => ?_, h_inter_eq⟩
   simp only [g]
   split_ifs with hn1 hn2 h
@@ -427,8 +418,7 @@ theorem isPiSystem_piiUnionInter (π : ι → Set (Set α)) (hpi : ∀ x, IsPiSy
       (Set.not_nonempty_iff_eq_empty.mpr h_empty) h_nonempty
     refine le_antisymm (Set.iInter_subset_of_subset n ?_) (Set.empty_subset _)
     refine Set.iInter_subset_of_subset hn ?_
-    simp_rw [g, if_pos hn1, if_pos hn2]
-    exact h.subset
+    grind
   · simp [hf1m n hn1]
   · simp [hf2m n h]
   · exact absurd hn (by simp [hn1, h])