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

Author: euprunin

Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean

@@ -62,9 +62,7 @@ the product over `s`, as long as `a` is in `s` or `f a = 1`. -/
 the sum over `s`, as long as `a` is in `s` or `f a = 0`. -/]
 theorem prod_insert_of_eq_one_if_notMem [DecidableEq ι] (h : a ∉ s → f a = 1) :
     ∏ x ∈ insert a s, f x = ∏ x ∈ s, f x := by
-  by_cases hm : a ∈ s
-  · simp_rw [insert_eq_of_mem hm]
-  · rw [prod_insert hm, h hm, one_mul]
+  by_cases a ∈ s <;> grind
 
 /-- The product of `f` over `insert a s` is the same as
 the product over `s`, as long as `f a = 1`. -/

Mathlib/Data/Finset/Sym.lean

@@ -87,9 +87,7 @@ theorem sym2_univ [Fintype α] (inst : Fintype (Sym2 α) := Sym2.instFintype) :
 
 @[simp, mono]
 theorem sym2_mono (h : s ⊆ t) : s.sym2 ⊆ t.sym2 := by
-  rw [← val_le_iff, sym2_val, sym2_val]
-  apply Multiset.sym2_mono
-  rwa [val_le_iff]
+  grind
 
 theorem monotone_sym2 : Monotone (Finset.sym2 : Finset α → _) := fun _ _ => sym2_mono
 

Mathlib/Data/Finsupp/Defs.lean

@@ -255,9 +255,7 @@ theorem support_onFinset [DecidableEq M] {s : Finset α} {f : α → M}
 @[simp]
 theorem support_onFinset_subset {s : Finset α} {f : α → M} {hf} :
     (onFinset s f hf).support ⊆ s := by
-  classical
-  rw [support_onFinset]
-  exact filter_subset (f · ≠ 0) s
+  grind
 
 grind_pattern support_onFinset_subset => onFinset s f hf
 

Mathlib/Order/Disjoint.lean

@@ -144,7 +144,7 @@ theorem top_disjoint : Disjoint ⊤ a ↔ a = ⊥ :=
 
 @[to_dual]
 theorem Disjoint.ne_top_of_ne_bot (h : Disjoint a b) (ha : a ≠ ⊥) : b ≠ ⊤ := by
-  rintro rfl; exact ha <| by simpa using h
+  grind
 
 @[deprecated ne_bot_of_ne_top (since := "2025-11-07")]
 lemma Codisjoint.ne_bot_of_ne_top' (h : Codisjoint a b) (hb : b ≠ ⊤) : a ≠ ⊥ :=