diff --git a/Mathlib/Data/Finset/BooleanAlgebra.lean b/Mathlib/Data/Finset/BooleanAlgebra.lean
index 0c7a2a5c9eb0a2..8827770b6ff547 100644
--- a/Mathlib/Data/Finset/BooleanAlgebra.lean
+++ b/Mathlib/Data/Finset/BooleanAlgebra.lean
@@ -231,8 +231,7 @@ theorem univ_filter_exists (f : α → β) [Fintype β] [DecidablePred fun y =>
 /-- Note this is a special case of `(Finset.image_preimage f univ _).symm`. -/
 theorem univ_filter_mem_range (f : α → β) [Fintype β] [DecidablePred fun y => y ∈ Set.range f]
     [DecidableEq β] : (Finset.univ.filter fun y => y ∈ Set.range f) = Finset.univ.image f := by
-  letI : DecidablePred (fun y => ∃ x, f x = y) := by simpa using ‹_›
-  exact univ_filter_exists f
+  grind
 
 theorem coe_filter_univ (p : α → Prop) [DecidablePred p] :
     (univ.filter p : Set α) = { x | p x } := by simp
diff --git a/Mathlib/Data/Finset/Erase.lean b/Mathlib/Data/Finset/Erase.lean
index a80d79b53726e9..fbe3889ec1d055 100644
--- a/Mathlib/Data/Finset/Erase.lean
+++ b/Mathlib/Data/Finset/Erase.lean
@@ -99,9 +99,7 @@ theorem coe_erase (a : α) (s : Finset α) : ↑(erase s a) = (s \ {a} : Set α)
 theorem erase_idem {a : α} {s : Finset α} : erase (erase s a) a = erase s a := by simp
 
 theorem erase_right_comm {a b : α} {s : Finset α} : erase (erase s a) b = erase (erase s b) a := by
-  ext x
-  simp only [mem_erase, ← and_assoc]
-  rw [@and_comm (x ≠ a)]
+  grind
 
 theorem erase_inj {x y : α} (s : Finset α) (hx : x ∈ s) : s.erase x = s.erase y ↔ x = y := by
   grind [eq_of_mem_of_notMem_erase]
diff --git a/Mathlib/Data/Finset/Powerset.lean b/Mathlib/Data/Finset/Powerset.lean
index 3db19e3ef71df9..a2be7885f80493 100644
--- a/Mathlib/Data/Finset/Powerset.lean
+++ b/Mathlib/Data/Finset/Powerset.lean
@@ -306,11 +306,7 @@ theorem powersetCard_map {β : Type*} (f : α ↪ β) (n : ℕ) (s : Finset α)
     constructor
     · classical
       intro h
-      have : map f (filter (fun x => (f x ∈ t)) s) = t := by
-        ext x
-        simp only [mem_map, mem_filter]
-        exact ⟨fun ⟨_y, ⟨_hy₁, hy₂⟩, hy₃⟩ => hy₃ ▸ hy₂,
-          fun hx => let ⟨y, hy⟩ := mem_map.1 (h.1 hx); ⟨y, ⟨hy.1, hy.2 ▸ hx⟩, hy.2⟩⟩
+      have : map f (filter (fun x => (f x ∈ t)) s) = t := by grind
       refine ⟨_, ?_, this⟩
       rw [← card_map f, this, h.2]; simp
     · rintro ⟨a, ⟨has, rfl⟩, rfl⟩
diff --git a/Mathlib/Data/Finset/Prod.lean b/Mathlib/Data/Finset/Prod.lean
index aba5ca332d8a74..c2569b85d436d5 100644
--- a/Mathlib/Data/Finset/Prod.lean
+++ b/Mathlib/Data/Finset/Prod.lean
@@ -313,8 +313,7 @@ theorem offDiag_empty : (∅ : Finset α).offDiag = ∅ :=
 
 @[simp]
 theorem diag_union_offDiag : s.diag ∪ s.offDiag = s ×ˢ s := by
-  conv_rhs => rw [← filter_union_filter_neg_eq (fun a => a.1 = a.2) (s ×ˢ s)]
-  rfl
+  grind
 
 @[simp]
 theorem disjoint_diag_offDiag : Disjoint s.diag s.offDiag :=