From 4861d6364fc16cc12d6a64d772d5c26532466239 Mon Sep 17 00:00:00 2001
From: "Yury G. Kudryashov" <urkud@urkud.name>
Date: Sat, 13 Apr 2024 17:32:44 -0500
Subject: [PATCH 1/3] chore(*Set): golf
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

- Golf `Directed.exists_mem_subset_of_finset_subset_biUnion`
  using Lean 4 `induction` tactic.
- Reduce abuse of `Set α = α → Prop` defeq.
---
 Mathlib/Data/Fintype/Powerset.lean       |  5 ++---
 Mathlib/Data/Set/Basic.lean              |  8 ++++----
 Mathlib/Data/Set/Finite.lean             | 18 +++++++-----------
 Mathlib/Data/Set/Intervals/Disjoint.lean |  4 ++--
 4 files changed, 15 insertions(+), 20 deletions(-)

diff --git a/Mathlib/Data/Fintype/Powerset.lean b/Mathlib/Data/Fintype/Powerset.lean
index 63d6e40da8857..047eb24026861 100644
--- a/Mathlib/Data/Fintype/Powerset.lean
+++ b/Mathlib/Data/Fintype/Powerset.lean
@@ -59,12 +59,11 @@ theorem Fintype.card_finset_len [Fintype α] (k : ℕ) :
 #align fintype.card_finset_len Fintype.card_finset_len
 
 instance Set.fintype [Fintype α] : Fintype (Set α) :=
-  ⟨(@Finset.univ α _).powerset.map ⟨(↑), coe_injective⟩, fun s => by
+  ⟨(@Finset.univ α _).powerset.map coeEmb.1, fun s => by
     classical
       refine' mem_map.2 ⟨Finset.univ.filter s, Finset.mem_powerset.2 (Finset.subset_univ _), _⟩
       apply (coe_filter _ _).trans
-      simp
-      rfl⟩
+      simp⟩
 #align set.fintype Set.fintype
 
 -- Not to be confused with `Set.Finite`, the predicate
diff --git a/Mathlib/Data/Set/Basic.lean b/Mathlib/Data/Set/Basic.lean
index 75f0196029d24..25113229c19a6 100644
--- a/Mathlib/Data/Set/Basic.lean
+++ b/Mathlib/Data/Set/Basic.lean
@@ -1425,12 +1425,12 @@ theorem sep_false : { x ∈ s | False } = ∅ :=
 
 --Porting note (#10618): removed `simp` attribute because `simp` can prove it
 theorem sep_empty (p : α → Prop) : { x ∈ (∅ : Set α) | p x } = ∅ :=
-  empty_inter p
+  empty_inter {x | p x}
 #align set.sep_empty Set.sep_empty
 
 --Porting note (#10618): removed `simp` attribute because `simp` can prove it
 theorem sep_univ : { x ∈ (univ : Set α) | p x } = { x | p x } :=
-  univ_inter p
+  univ_inter {x | p x}
 #align set.sep_univ Set.sep_univ
 
 @[simp]
@@ -1440,12 +1440,12 @@ theorem sep_union : { x | (x ∈ s ∨ x ∈ t) ∧ p x } = { x ∈ s | p x } 
 
 @[simp]
 theorem sep_inter : { x | (x ∈ s ∧ x ∈ t) ∧ p x } = { x ∈ s | p x } ∩ { x ∈ t | p x } :=
-  inter_inter_distrib_right s t p
+  inter_inter_distrib_right s t {x | p x}
 #align set.sep_inter Set.sep_inter
 
 @[simp]
 theorem sep_and : { x ∈ s | p x ∧ q x } = { x ∈ s | p x } ∩ { x ∈ s | q x } :=
-  inter_inter_distrib_left s p q
+  inter_inter_distrib_left s {x | p x} {x | q x}
 #align set.sep_and Set.sep_and
 
 @[simp]
diff --git a/Mathlib/Data/Set/Finite.lean b/Mathlib/Data/Set/Finite.lean
index 2d6c950c46ca3..89712ac93ba5b 100644
--- a/Mathlib/Data/Set/Finite.lean
+++ b/Mathlib/Data/Set/Finite.lean
@@ -1758,17 +1758,13 @@ lemma Set.finite_diff_iUnion_Ioo' (s : Set α) : (s \ ⋃ x : s × s, Ioo x.1 x.
 lemma Directed.exists_mem_subset_of_finset_subset_biUnion {α ι : Type*} [Nonempty ι]
     {f : ι → Set α} (h : Directed (· ⊆ ·) f) {s : Finset α} (hs : (s : Set α) ⊆ ⋃ i, f i) :
     ∃ i, (s : Set α) ⊆ f i := by
-  classical
-  revert hs
-  refine s.induction_on ?_ ?_
-  · simp
-  intro b t _hbt htc hbtc
-  obtain ⟨i : ι, hti : (t : Set α) ⊆ f i⟩ := htc (Set.Subset.trans (t.subset_insert b) hbtc)
-  obtain ⟨j, hbj⟩ : ∃ j, b ∈ f j := by simpa [Set.mem_iUnion₂] using hbtc (t.mem_insert_self b)
-  rcases h j i with ⟨k, hk, hk'⟩
-  use k
-  rw [Finset.coe_insert, Set.insert_subset_iff]
-  exact ⟨hk hbj, _root_.trans hti hk'⟩
+  induction s using Finset.cons_induction_on with
+  | h₁ => exact ⟨hn.some, by simp only [coe_empty, Set.empty_subset]⟩
+  | h₂ hbt iht =>
+    simp only [coe_cons, Set.insert_subset_iff, Set.mem_iUnion] at hs ⊢
+    rcases hs.imp_right iht with ⟨⟨i, hi⟩, j, hj⟩
+    rcases h i j with ⟨k, hik, hjk⟩
+    exact ⟨k, hik hi, hj.trans hjk⟩
 #align directed.exists_mem_subset_of_finset_subset_bUnion Directed.exists_mem_subset_of_finset_subset_biUnion
 
 theorem DirectedOn.exists_mem_subset_of_finset_subset_biUnion {α ι : Type*} {f : ι → Set α}
diff --git a/Mathlib/Data/Set/Intervals/Disjoint.lean b/Mathlib/Data/Set/Intervals/Disjoint.lean
index be7d22fbcd269..a8527eac61800 100644
--- a/Mathlib/Data/Set/Intervals/Disjoint.lean
+++ b/Mathlib/Data/Set/Intervals/Disjoint.lean
@@ -43,12 +43,12 @@ theorem Iio_disjoint_Ici (h : a ≤ b) : Disjoint (Iio a) (Ici b) :=
 
 @[simp]
 theorem Iic_disjoint_Ioc (h : a ≤ b) : Disjoint (Iic a) (Ioc b c) :=
-  (Iic_disjoint_Ioi h).mono le_rfl fun _ => And.left
+  (Iic_disjoint_Ioi h).mono le_rfl Ioc_subset_Ioi_self
 #align set.Iic_disjoint_Ioc Set.Iic_disjoint_Ioc
 
 @[simp]
 theorem Ioc_disjoint_Ioc_same : Disjoint (Ioc a b) (Ioc b c) :=
-  (Iic_disjoint_Ioc (le_refl b)).mono (fun _ => And.right) le_rfl
+  (Iic_disjoint_Ioc le_rfl).mono Ioc_subset_Iic_self le_rfl
 #align set.Ioc_disjoint_Ioc_same Set.Ioc_disjoint_Ioc_same
 
 @[simp]

From 441c67b70b6d4d0aa175fc824bd8e15619877f78 Mon Sep 17 00:00:00 2001
From: "Yury G. Kudryashov" <urkud@urkud.name>
Date: Sat, 13 Apr 2024 18:11:16 -0500
Subject: [PATCH 2/3] Fix

---
 Mathlib/Data/Fintype/Powerset.lean | 7 +++----
 1 file changed, 3 insertions(+), 4 deletions(-)

diff --git a/Mathlib/Data/Fintype/Powerset.lean b/Mathlib/Data/Fintype/Powerset.lean
index 047eb24026861..18b42cbde5822 100644
--- a/Mathlib/Data/Fintype/Powerset.lean
+++ b/Mathlib/Data/Fintype/Powerset.lean
@@ -59,11 +59,10 @@ theorem Fintype.card_finset_len [Fintype α] (k : ℕ) :
 #align fintype.card_finset_len Fintype.card_finset_len
 
 instance Set.fintype [Fintype α] : Fintype (Set α) :=
-  ⟨(@Finset.univ α _).powerset.map coeEmb.1, fun s => by
+  ⟨(@Finset.univ (Finset α) _).map coeEmb.1, fun s => by
     classical
-      refine' mem_map.2 ⟨Finset.univ.filter s, Finset.mem_powerset.2 (Finset.subset_univ _), _⟩
-      apply (coe_filter _ _).trans
-      simp⟩
+    refine mem_map.2 ⟨Finset.univ.filter (· ∈ s), Finset.mem_univ _, (coe_filter _ _).trans ?_⟩
+    simp⟩
 #align set.fintype Set.fintype
 
 -- Not to be confused with `Set.Finite`, the predicate

From 04caa66c1a169f79006bb550aa18bec865c25246 Mon Sep 17 00:00:00 2001
From: "Yury G. Kudryashov" <urkud@urkud.name>
Date: Sat, 13 Apr 2024 18:21:27 -0500
Subject: [PATCH 3/3] Fix

---
 Mathlib/Data/Set/Finite.lean | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/Mathlib/Data/Set/Finite.lean b/Mathlib/Data/Set/Finite.lean
index 89712ac93ba5b..88df426f58963 100644
--- a/Mathlib/Data/Set/Finite.lean
+++ b/Mathlib/Data/Set/Finite.lean
@@ -1758,10 +1758,10 @@ lemma Set.finite_diff_iUnion_Ioo' (s : Set α) : (s \ ⋃ x : s × s, Ioo x.1 x.
 lemma Directed.exists_mem_subset_of_finset_subset_biUnion {α ι : Type*} [Nonempty ι]
     {f : ι → Set α} (h : Directed (· ⊆ ·) f) {s : Finset α} (hs : (s : Set α) ⊆ ⋃ i, f i) :
     ∃ i, (s : Set α) ⊆ f i := by
-  induction s using Finset.cons_induction_on with
-  | h₁ => exact ⟨hn.some, by simp only [coe_empty, Set.empty_subset]⟩
-  | h₂ hbt iht =>
-    simp only [coe_cons, Set.insert_subset_iff, Set.mem_iUnion] at hs ⊢
+  induction s using Finset.cons_induction with
+  | empty => simp
+  | cons hbt iht =>
+    simp only [Finset.coe_cons, Set.insert_subset_iff, Set.mem_iUnion] at hs ⊢
     rcases hs.imp_right iht with ⟨⟨i, hi⟩, j, hj⟩
     rcases h i j with ⟨k, hik, hjk⟩
     exact ⟨k, hik hi, hj.trans hjk⟩