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

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

Trace profiling results (differences <30 ms considered measurement noise):
* `DirectSum.lequivCongrLeft_lof`: unchanged 🎉
* `AnalyticOnNhd.preimage_mem_codiscreteWithin`: unchanged 🎉
* `mem_permsOfList_of_mem`: unchanged 🎉
* `PNat.mod_le`: unchanged 🎉
* `Computation.map_parallel`: unchanged 🎉
* `Sigma.curry_update`: unchanged 🎉

Profiled using `set_option trace.profiler true in`.

Author: euprunin

Mathlib/Algebra/DirectSum/Module.lean

@@ -333,12 +333,8 @@ lemma lequivCongrLeft_lof [DecidableEq ι] [DecidableEq κ] {e : ι ≃ κ}
     lequivCongrLeft R e (lof R ι M i x) = lof R _ _ k y := by
   subst hik hxy
   ext j
-  simp_rw [lequivCongrLeft_apply, lof_eq_of, of_apply]
-  by_cases eq : k = j
-  · subst eq
-    rw [dif_pos rfl, dif_pos rfl]
-    rfl
-  · rw [dif_neg (by aesop), dif_neg eq]
+  simp [lof_eq_of, of_apply]
+  lia
 
 lemma lequivCongrLeft_symm_lof [DecidableEq ι] [DecidableEq κ] {h : ι ≃ κ}
     {k : κ} {x : M (h.symm k)} :

Mathlib/Analysis/Analytic/IsolatedZeros.lean

@@ -350,12 +350,7 @@ theorem AnalyticOnNhd.preimage_mem_codiscreteWithin {U : Set 𝕜} {s : Set E} {
   simp_rw [mem_codiscreteWithin, disjoint_principal_right, Set.compl_diff] at *
   intro x hx
   apply mem_of_superset ((hfU x hx).preimage_of_nhdsNE (h₂f x hx) (hs (f x) (by tauto)))
-  rw [preimage_union, preimage_compl]
-  apply union_subset_union_right (f ⁻¹' s)
-  intro x hx
-  push _ ∈ _ at hx ⊢
-  push Not at hx
-  tauto
+  grind
 
 /-- Preimages of codiscrete sets, filter version: if `f` is analytic on a neighbourhood of `U` and
 not locally constant, then the push-forward of the filter of sets codiscrete within `U` is less

Mathlib/Data/Fintype/Perm.lean

@@ -58,15 +58,8 @@ theorem mem_permsOfList_of_mem {l : List α} {f : Perm α} (h : ∀ x, f x ≠ x
     exact hx hfa
   have hfa' : f (f a) ≠ f a := mt (fun h => f.injective h) hfa
   have : ∀ x : α, (Equiv.swap a (f a) * f) x ≠ x → x ∈ l := by
-    intro x hx
-    have hxa : x ≠ a := by
-      rintro rfl
-      apply hx
-      simp only [mul_apply, swap_apply_right]
-    refine List.mem_of_ne_of_mem hxa (h x fun h => ?_)
-    simp only [mul_apply, swap_apply_def, mul_apply, Ne, apply_eq_iff_eq] at hx
-    split_ifs at hx with h_1
-    exacts [hxa (h.symm.trans h_1), hx h]
+    simp
+    grind
   suffices f ∈ permsOfList l ∨ ∃ b ∈ l, ∃ g ∈ permsOfList l, Equiv.swap a b * g = f by
     simpa only [permsOfList, exists_prop, List.mem_map, mem_append, List.mem_flatMap]
   refine or_iff_not_imp_left.2 fun _hfl => ⟨f a, ?_, Equiv.swap a (f a) * f, IH this, ?_⟩

Mathlib/Data/PNat/Basic.lean

@@ -307,13 +307,8 @@ theorem mod_le (m k : ℕ+) : mod m k ≤ m ∧ mod m k ≤ k := by
   split_ifs with h
   · have hm : (m : ℕ) > 0 := m.pos
     rw [← Nat.mod_add_div (m : ℕ) (k : ℕ), h, zero_add] at hm ⊢
-    by_cases h₁ : (m : ℕ) / (k : ℕ) = 0
-    · rw [h₁, mul_zero] at hm
-      exact (lt_irrefl _ hm).elim
-    · let h₂ : (k : ℕ) * 1 ≤ k * (m / k) :=
-        Nat.mul_le_mul_left (k : ℕ) (Nat.succ_le_of_lt (Nat.pos_of_ne_zero h₁))
-      rw [mul_one] at h₂
-      exact ⟨h₂, le_refl (k : ℕ)⟩
+    simp
+    lia
   · exact ⟨Nat.mod_le (m : ℕ) (k : ℕ), (Nat.mod_lt (m : ℕ) k.pos).le⟩
 
 theorem dvd_iff {k m : ℕ+} : k ∣ m ↔ (k : ℕ) ∣ (m : ℕ) := by

Mathlib/Data/Seq/Parallel.lean

@@ -267,13 +267,8 @@ theorem map_parallel (f : α → β) (S) : map f (parallel S) = parallel (S.map
           = lmap f (rmap (List.map (map f)) (parallel.aux2 l)) := by
         simp only [parallel.aux2, rmap, lmap]
         induction l with
-        | nil => simp
-        | cons c l IH =>
-          simp only [List.map_cons, List.foldr_cons, destruct_map, lmap, rmap]
-          rw [IH]
-          cases List.foldr _ _ _
-          · simp
-          · cases destruct c <;> simp
+        | nil => grind
+        | cons => grind [destruct_map, lmap, rmap]
       simp only [BisimO, destruct_map, lmap, rmap, corec_eq, parallel.aux1.eq_1]
       rw [this]
       rcases parallel.aux2 l with a | l'

Mathlib/Data/Sigma/Basic.lean

@@ -169,12 +169,8 @@ theorem Sigma.curry_update {γ : ∀ a, β a → Type*} [DecidableEq α] [∀ a,
   ext ja jb
   unfold Sigma.curry
   obtain rfl | ha := eq_or_ne ia ja
-  · obtain rfl | hb := eq_or_ne ib jb
-    · simp
-    · simp only [update_self]
-      rw [Function.update_of_ne (mt _ hb.symm), Function.update_of_ne hb.symm]
-      rintro h
-      injection h
+  · simp
+    grind
   · rw [Function.update_of_ne (ne_of_apply_ne Sigma.fst _), Function.update_of_ne]
     · exact ha.symm
     · exact ha.symm