From fdc159aad2b93c5ed316804d216d99acff9d3ebf Mon Sep 17 00:00:00 2001
From: euprunin <euprunin@users.noreply.github.com>
Date: Tue, 19 Aug 2025 07:10:21 +0200
Subject: [PATCH] chore(Order/BooleanAlgebra): golf entire
 `diff_insert_of_notMem`, `insert_diff_of_mem`, `insert_diff_of_notMem` and
 `subset_insert_iff` using `grind`

---
 Mathlib/Order/BooleanAlgebra/Set.lean | 18 ++++--------------
 1 file changed, 4 insertions(+), 14 deletions(-)

diff --git a/Mathlib/Order/BooleanAlgebra/Set.lean b/Mathlib/Order/BooleanAlgebra/Set.lean
index f2d25bb8942266..4e3e21117fce4a 100644
--- a/Mathlib/Order/BooleanAlgebra/Set.lean
+++ b/Mathlib/Order/BooleanAlgebra/Set.lean
@@ -401,23 +401,16 @@ lemma subset_insert_diff_singleton (x : α) (s : Set α) : s ⊆ insert x (s \ {
   rw [← diff_singleton_subset_iff]
 
 lemma diff_insert_of_notMem (h : a ∉ s) : s \ insert a t = s \ t := by
-  refine Subset.antisymm (diff_subset_diff (refl _) (subset_insert ..)) fun y hy ↦ ?_
-  simp only [mem_diff, mem_insert_iff, not_or] at hy ⊢
-  exact ⟨hy.1, fun hxy ↦ h <| hxy ▸ hy.1, hy.2⟩
+  grind
 
 @[deprecated (since := "2025-05-23")] alias diff_insert_of_not_mem := diff_insert_of_notMem
 
 @[simp]
 lemma insert_diff_of_mem (s) (h : a ∈ t) : insert a s \ t = s \ t := by
-  ext
-  constructor <;> simp +contextual [or_imp, h]
+  grind
 
 lemma insert_diff_of_notMem (s) (h : a ∉ t) : insert a s \ t = insert a (s \ t) := by
-  classical
-  ext x
-  by_cases h' : x ∈ t
-  · simp [h', ne_of_mem_of_not_mem h' h]
-  · simp [h']
+  grind
 
 @[deprecated (since := "2025-05-23")] alias insert_diff_of_not_mem := insert_diff_of_notMem
 
@@ -464,10 +457,7 @@ lemma mem_diff_singleton_empty {t : Set (Set α)} : s ∈ t \ {∅} ↔ s ∈ t
   mem_diff_singleton.trans <| and_congr_right' nonempty_iff_ne_empty.symm
 
 lemma subset_insert_iff : s ⊆ insert a t ↔ s ⊆ t ∨ (a ∈ s ∧ s \ {a} ⊆ t) := by
-  rw [← diff_singleton_subset_iff]
-  by_cases hx : a ∈ s
-  · rw [and_iff_right hx, or_iff_right_of_imp diff_subset.trans]
-  rw [diff_singleton_eq_self hx, or_iff_left_of_imp And.right]
+  grind
 
 lemma pair_diff_left (hab : a ≠ b) : ({a, b} : Set α) \ {a} = {b} := by
   rw [insert_diff_of_mem _ (mem_singleton a), diff_singleton_eq_self (by simpa)]