chore: golf using grind and add grind annotation

Author: euprunin

Mathlib/GroupTheory/GroupAction/MultipleTransitivity.lean

@@ -583,19 +583,10 @@ theorem isMultiplyPretransitive (n : ℕ) :
       · obtain ⟨i, rfl⟩ := hb
         use x i
         simp only [ψ, x.injective.extend_apply]
-      · rw [← Set.mem_compl_iff] at hb
-        use φ.invFun ⟨b, hb⟩
+      · use φ.invFun ⟨b, hb⟩
         simp only [ψ]
-        rw [Function.extend_apply' _ _ _ ?_]
-        · simp only [φ']
-          set a : α := (φ.invFun ⟨b, hb⟩ : α)
-          have ha : a ∈ (range x)ᶜ := Subtype.coe_prop (φ.invFun ⟨b, hb⟩)
-          rw [← Subtype.coe_mk a ha]
-          simp [a]
-        · rintro ⟨i, hi⟩
-          apply Subtype.coe_prop (φ.invFun ⟨b, hb⟩)
-          rw [← hi]
-          exact mem_range_self i
+        simp only [invFun_as_coe]
+        grind [Function.extend_apply', Function.extend_val_apply]
   use Equiv.ofBijective ψ this
   ext i
   simp [ψ, x.injective.extend_apply]

Mathlib/GroupTheory/Perm/Support.lean

@@ -78,7 +78,7 @@ theorem disjoint_one_right (f : Perm α) : Disjoint f 1 := fun _ => Or.inr rfl
 theorem disjoint_iff_eq_or_eq : Disjoint f g ↔ ∀ x : α, f x = x ∨ g x = x :=
   Iff.rfl
 
-@[simp]
+@[simp, grind =]
 theorem disjoint_refl_iff : Disjoint f f ↔ f = 1 := by
   refine ⟨fun h => ?_, fun h => h.symm ▸ disjoint_one_left 1⟩
   ext x
@@ -136,13 +136,7 @@ theorem disjoint_prod_perm {l₁ l₂ : List (Perm α)} (hl : l₁.Pairwise Disj
 
 theorem nodup_of_pairwise_disjoint {l : List (Perm α)} (h1 : (1 : Perm α) ∉ l)
     (h2 : l.Pairwise Disjoint) : l.Nodup := by
-  refine List.Pairwise.imp_of_mem ?_ h2
-  intro τ σ h_mem _ h_disjoint _
-  subst τ
-  suffices (σ : Perm α) = 1 by
-    rw [this] at h_mem
-    exact h1 h_mem
-  exact ext fun a => or_self_iff.mp (h_disjoint a)
+  grind [List.nodup_iff_sublist]
 
 theorem pow_apply_eq_self_of_apply_eq_self {x : α} (hfx : f x = x) : ∀ n : ℕ, (f ^ n) x = x
   | 0 => rfl

Mathlib/NumberTheory/LucasLehmer.lean

@@ -643,14 +643,7 @@ theorem sModNat_eq_sMod (p k : ℕ) (hp : 2 ≤ p) : (sModNat (2 ^ p - 1) k : 
     simp [h2]
   | succ k ih =>
     rw [sModNat, sMod, ← ih]
-    have h3 : 2 ≤ 2 ^ p - 1 := by
-      zify [h2]
-      calc (2 : ℤ)
-        _ ≤ 4 - 1 := by simp
-        _ ≤ 2 ^ p - 1 := by zify at h1; exact Int.sub_le_sub_right h1 _
-    zify [h2, h3]
-    rw [← add_sub_assoc, sub_eq_add_neg, add_assoc, add_comm _ (-2), ← add_assoc,
-      Int.add_emod_right, ← sub_eq_add_neg]
+    grind [Int.emod_eq_emod_iff_emod_sub_eq_zero, Int.add_emod, Int.emod_eq_add_self_emod]
 
 /-- Tail-recursive version of `sModNat`. -/
 meta def sModNatTR (q k : ℕ) : ℕ :=

Mathlib/Probability/Kernel/IonescuTulcea/Maps.lean

@@ -188,15 +188,7 @@ lemma _root_.IicProdIoc_preimage {a b : ι} (hab : a ≤ b) (s : (i : Iic b) →
       (Set.univ.pi <| frestrictLe₂ (π := (fun n ↦ Set (X n))) hab s) ×ˢ
         (Set.univ.pi <| restrict₂ (π := (fun n ↦ Set (X n))) Ioc_subset_Iic_self s) := by
   ext x
-  simp only [Set.mem_preimage, Set.mem_pi, Set.mem_univ, IicProdIoc_def, forall_const,
-    Subtype.forall, mem_Iic, Set.mem_prod, frestrictLe₂_apply, restrict₂, mem_Ioc]
-  refine ⟨fun h ↦ ⟨fun i hi ↦ ?_, fun i ⟨hi1, hi2⟩ ↦ ?_⟩, fun ⟨h1, h2⟩ i hi ↦ ?_⟩
-  · convert h i (hi.trans hab)
-    rw [dif_pos hi]
-  · convert h i hi2
-    rw [dif_neg (not_le.2 hi1)]
-  · split_ifs with hi3
-    · exact h1 i hi3
-    · exact h2 i ⟨not_le.1 hi3, hi⟩
+  simp only [Set.mem_preimage, Set.mem_pi, IicProdIoc_def, Subtype.forall, mem_Iic]
+  grind
 
 end Lemmas