From 668c203df3f8d86d815f31cc2feccc3ef9710eea Mon Sep 17 00:00:00 2001
From: qawbecrdtey <qawbecrdtey@kaist.ac.kr>
Date: Wed, 27 Nov 2024 00:33:44 +0900
Subject: [PATCH 1/6] Added congruence about subtypes.

---
 Mathlib/Data/Finset/Image.lean | 21 +++++++++++++++++++++
 Mathlib/Data/Set/Basic.lean    | 14 ++++++++++++++
 2 files changed, 35 insertions(+)

diff --git a/Mathlib/Data/Finset/Image.lean b/Mathlib/Data/Finset/Image.lean
index 5b0af20456dff..5a6ba136833e6 100644
--- a/Mathlib/Data/Finset/Image.lean
+++ b/Mathlib/Data/Finset/Image.lean
@@ -767,4 +767,25 @@ theorem finsetCongr_toEmbedding (e : α ≃ β) :
     e.finsetCongr.toEmbedding = (Finset.mapEmbedding e.toEmbedding).toEmbedding :=
   rfl
 
+/-- Given a predicate `p : Finset α → Prop`, produces an equivalence between
+  `{S : Finset (Finset α) // ∀ s ∈ S, p s}` and `Finset {s : Finset α // p s}`. -/
+protected def finsetSubtypeCongr (p : Finset α → Prop) :
+    {S : Finset (Finset α) // ∀ s ∈ S, p s} ≃ (Finset {s : Finset α // p s}) where
+  toFun S := S.val.attach.map (Subtype.impEmbedding _ _ S.property)
+  invFun S := ⟨S.map ⟨fun s ↦ s.val, Subtype.val_injective⟩, fun s h ↦
+    have ⟨v, _, h⟩ := Embedding.coeFn_mk _ _ ▸ mem_map.mp h
+    h ▸ v.property⟩
+  left_inv S := by
+    ext s; constructor <;> intro h <;>
+    simp only [Finset.mem_map, Finset.mem_attach, true_and, Subtype.exists, Embedding.coeFn_mk,
+      exists_and_right, exists_eq_right, Subtype.impEmbedding, Subtype.mk.injEq] at *
+    · rcases h with ⟨_, _, h₁, h₂⟩; exact h₂ ▸ h₁
+    · use S.property _ h, s
+  right_inv S := by
+    ext s; constructor <;> intro h <;>
+    simp only [Finset.mem_map, Finset.mem_attach, true_and, Subtype.exists, Embedding.coeFn_mk,
+      exists_and_right, exists_eq_right, Subtype.impEmbedding, Subtype.mk.injEq] at *
+    · rcases h with ⟨_, ⟨_, h₁⟩, h₂⟩; exact h₂ ▸ h₁
+    · use s, ⟨s.property, h⟩
+
 end Equiv
diff --git a/Mathlib/Data/Set/Basic.lean b/Mathlib/Data/Set/Basic.lean
index 8d28bac27f0b0..1e69169da898f 100644
--- a/Mathlib/Data/Set/Basic.lean
+++ b/Mathlib/Data/Set/Basic.lean
@@ -2168,4 +2168,18 @@ end Disjoint
 @[simp] theorem Prop.compl_singleton (p : Prop) : ({p}ᶜ : Set Prop) = {¬p} :=
   ext fun q ↦ by simpa [@Iff.comm q] using not_iff
 
+namespace Equiv
+
+/-- Given a predicate `p : Set α → Prop`, produces an equivalence between
+  `{S : Set (Set α) // ∀ s ∈ S, p s}` and `Set {s : Set α // p s}`. -/
+protected def setSubtypeCongr {α : Type*} (p : Set α → Prop) :
+    Equiv {S : Set (Set α) // ∀ s ∈ S, p s} (Set {s : Set α // p s}) where
+  toFun S s := S.val s
+  invFun S := ⟨fun s ↦ ∃ h : p s, S ⟨s, h⟩, fun _ h ↦ h.1⟩
+  left_inv S := by ext; exact ⟨fun h ↦ h.2, fun h ↦ ⟨S.property _ h, h⟩⟩
+  right_inv S := by ext s; exact ⟨fun h ↦ h.2, fun h ↦ ⟨s.property, h⟩⟩
+
+
+end Equiv
+
 set_option linter.style.longFile 2300

From d0498e7127bd0eca4bda72be6e1134fd6a0fd503 Mon Sep 17 00:00:00 2001
From: qawbecrdtey <qawbecrdtey@kaist.ac.kr>
Date: Wed, 27 Nov 2024 14:34:42 +0900
Subject: [PATCH 2/6] Applied suggestion: Generalized Set a to a.

---
 Mathlib/Data/Finset/Image.lean | 23 +++++++++++------------
 Mathlib/Data/Set/Basic.lean    | 12 ++++++------
 2 files changed, 17 insertions(+), 18 deletions(-)

diff --git a/Mathlib/Data/Finset/Image.lean b/Mathlib/Data/Finset/Image.lean
index 5a6ba136833e6..28cf94c37f723 100644
--- a/Mathlib/Data/Finset/Image.lean
+++ b/Mathlib/Data/Finset/Image.lean
@@ -769,23 +769,22 @@ theorem finsetCongr_toEmbedding (e : α ≃ β) :
 
 /-- Given a predicate `p : Finset α → Prop`, produces an equivalence between
   `{S : Finset (Finset α) // ∀ s ∈ S, p s}` and `Finset {s : Finset α // p s}`. -/
-protected def finsetSubtypeCongr (p : Finset α → Prop) :
-    {S : Finset (Finset α) // ∀ s ∈ S, p s} ≃ (Finset {s : Finset α // p s}) where
-  toFun S := S.val.attach.map (Subtype.impEmbedding _ _ S.property)
-  invFun S := ⟨S.map ⟨fun s ↦ s.val, Subtype.val_injective⟩, fun s h ↦
-    have ⟨v, _, h⟩ := Embedding.coeFn_mk _ _ ▸ mem_map.mp h
-    h ▸ v.property⟩
-  left_inv S := by
-    ext s; constructor <;> intro h <;>
+protected def finsetSubtypeCongr (p : α → Prop) :
+    {s : Finset α // ∀ a ∈ s, p a} ≃ (Finset {a : α // p a}) where
+  toFun s := s.val.attach.map (Subtype.impEmbedding _ _ s.property)
+  invFun s := ⟨s.map ⟨fun a ↦ a.val, Subtype.val_injective⟩, fun _ h ↦
+    have ⟨v, _, h⟩ := Embedding.coeFn_mk _ _ ▸ mem_map.mp h; h ▸ v.property⟩
+  left_inv s := by
+    ext a; constructor <;> intro h <;>
     simp only [Finset.mem_map, Finset.mem_attach, true_and, Subtype.exists, Embedding.coeFn_mk,
       exists_and_right, exists_eq_right, Subtype.impEmbedding, Subtype.mk.injEq] at *
     · rcases h with ⟨_, _, h₁, h₂⟩; exact h₂ ▸ h₁
-    · use S.property _ h, s
-  right_inv S := by
-    ext s; constructor <;> intro h <;>
+    · use s.property _ h, a
+  right_inv s := by
+    ext a; constructor <;> intro h <;>
     simp only [Finset.mem_map, Finset.mem_attach, true_and, Subtype.exists, Embedding.coeFn_mk,
       exists_and_right, exists_eq_right, Subtype.impEmbedding, Subtype.mk.injEq] at *
     · rcases h with ⟨_, ⟨_, h₁⟩, h₂⟩; exact h₂ ▸ h₁
-    · use s, ⟨s.property, h⟩
+    · use a, ⟨a.property, h⟩
 
 end Equiv
diff --git a/Mathlib/Data/Set/Basic.lean b/Mathlib/Data/Set/Basic.lean
index 1e69169da898f..a86f0ac8ce432 100644
--- a/Mathlib/Data/Set/Basic.lean
+++ b/Mathlib/Data/Set/Basic.lean
@@ -2172,12 +2172,12 @@ namespace Equiv
 
 /-- Given a predicate `p : Set α → Prop`, produces an equivalence between
   `{S : Set (Set α) // ∀ s ∈ S, p s}` and `Set {s : Set α // p s}`. -/
-protected def setSubtypeCongr {α : Type*} (p : Set α → Prop) :
-    Equiv {S : Set (Set α) // ∀ s ∈ S, p s} (Set {s : Set α // p s}) where
-  toFun S s := S.val s
-  invFun S := ⟨fun s ↦ ∃ h : p s, S ⟨s, h⟩, fun _ h ↦ h.1⟩
-  left_inv S := by ext; exact ⟨fun h ↦ h.2, fun h ↦ ⟨S.property _ h, h⟩⟩
-  right_inv S := by ext s; exact ⟨fun h ↦ h.2, fun h ↦ ⟨s.property, h⟩⟩
+protected def setSubtypeCongr {α : Type*} (p : α → Prop) :
+    {s : Set α // ∀ a ∈ s, p a} ≃ (Set {a : α // p a}) where
+  toFun s a := s.val a
+  invFun s := ⟨fun a ↦ ∃ h : p a, s ⟨a, h⟩, fun _ h ↦ h.1⟩
+  left_inv s := by ext; exact ⟨fun h ↦ h.2, fun h ↦ ⟨s.property _ h, h⟩⟩
+  right_inv s := by ext a; exact ⟨fun h ↦ h.2, fun h ↦ ⟨a.property, h⟩⟩
 
 
 end Equiv

From 8d469784b9d0b50ee5cb895369733313ccb49831 Mon Sep 17 00:00:00 2001
From: qawbecrdtey <qawbecrdtey@kaist.ac.kr>
Date: Wed, 27 Nov 2024 16:17:56 +0900
Subject: [PATCH 3/6] Fixed comment.

---
 Mathlib/Data/Finset/Image.lean | 4 ++--
 Mathlib/Data/Set/Basic.lean    | 4 ++--
 2 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/Mathlib/Data/Finset/Image.lean b/Mathlib/Data/Finset/Image.lean
index 28cf94c37f723..9f45cb712bcf6 100644
--- a/Mathlib/Data/Finset/Image.lean
+++ b/Mathlib/Data/Finset/Image.lean
@@ -767,8 +767,8 @@ theorem finsetCongr_toEmbedding (e : α ≃ β) :
     e.finsetCongr.toEmbedding = (Finset.mapEmbedding e.toEmbedding).toEmbedding :=
   rfl
 
-/-- Given a predicate `p : Finset α → Prop`, produces an equivalence between
-  `{S : Finset (Finset α) // ∀ s ∈ S, p s}` and `Finset {s : Finset α // p s}`. -/
+/-- Given a predicate `p : α → Prop`, produces an equivalence between
+  `{s : Finset α // ∀ a ∈ s, p a}` and `Finset {a : α // p a}`. -/
 protected def finsetSubtypeCongr (p : α → Prop) :
     {s : Finset α // ∀ a ∈ s, p a} ≃ (Finset {a : α // p a}) where
   toFun s := s.val.attach.map (Subtype.impEmbedding _ _ s.property)
diff --git a/Mathlib/Data/Set/Basic.lean b/Mathlib/Data/Set/Basic.lean
index a86f0ac8ce432..5138f0cd59ec2 100644
--- a/Mathlib/Data/Set/Basic.lean
+++ b/Mathlib/Data/Set/Basic.lean
@@ -2170,8 +2170,8 @@ end Disjoint
 
 namespace Equiv
 
-/-- Given a predicate `p : Set α → Prop`, produces an equivalence between
-  `{S : Set (Set α) // ∀ s ∈ S, p s}` and `Set {s : Set α // p s}`. -/
+/-- Given a predicate `p : α → Prop`, produces an equivalence between
+  `{s : Set α // ∀ a ∈ s, p a}` and `Set {a : α // p a}`. -/
 protected def setSubtypeCongr {α : Type*} (p : α → Prop) :
     {s : Set α // ∀ a ∈ s, p a} ≃ (Set {a : α // p a}) where
   toFun s a := s.val a

From 4cccbab226a20fbe62ff0966970e5ad79ef2036d Mon Sep 17 00:00:00 2001
From: qawbecrdtey <qawbecrdtey@kaist.ac.kr>
Date: Thu, 28 Nov 2024 04:48:17 +0900
Subject: [PATCH 4/6] Applied suggestions.

---
 Mathlib/Data/Finset/Image.lean | 17 +++++++++--------
 Mathlib/Data/Set/Basic.lean    | 14 +++++++-------
 2 files changed, 16 insertions(+), 15 deletions(-)

diff --git a/Mathlib/Data/Finset/Image.lean b/Mathlib/Data/Finset/Image.lean
index 9f45cb712bcf6..54be6182a289a 100644
--- a/Mathlib/Data/Finset/Image.lean
+++ b/Mathlib/Data/Finset/Image.lean
@@ -768,23 +768,24 @@ theorem finsetCongr_toEmbedding (e : α ≃ β) :
   rfl
 
 /-- Given a predicate `p : α → Prop`, produces an equivalence between
-  `{s : Finset α // ∀ a ∈ s, p a}` and `Finset {a : α // p a}`. -/
+  `Finset {a : α // p a}` and `{s : Finset α // ∀ a ∈ s, p a}`. -/
+@[simps]
 protected def finsetSubtypeCongr (p : α → Prop) :
-    {s : Finset α // ∀ a ∈ s, p a} ≃ (Finset {a : α // p a}) where
-  toFun s := s.val.attach.map (Subtype.impEmbedding _ _ s.property)
-  invFun s := ⟨s.map ⟨fun a ↦ a.val, Subtype.val_injective⟩, fun _ h ↦
+    Finset {a : α // p a} ≃ {s : Finset α // ∀ a ∈ s, p a} where
+  toFun s := ⟨s.map ⟨fun a ↦ a.val, Subtype.val_injective⟩, fun _ h ↦
     have ⟨v, _, h⟩ := Embedding.coeFn_mk _ _ ▸ mem_map.mp h; h ▸ v.property⟩
+  invFun s := s.val.attach.map (Subtype.impEmbedding _ _ s.property)
   left_inv s := by
     ext a; constructor <;> intro h <;>
     simp only [Finset.mem_map, Finset.mem_attach, true_and, Subtype.exists, Embedding.coeFn_mk,
       exists_and_right, exists_eq_right, Subtype.impEmbedding, Subtype.mk.injEq] at *
-    · rcases h with ⟨_, _, h₁, h₂⟩; exact h₂ ▸ h₁
-    · use s.property _ h, a
+    · rcases h with ⟨_, ⟨_, h₁⟩, h₂⟩; exact h₂ ▸ h₁
+    · use a, ⟨a.property, h⟩
   right_inv s := by
     ext a; constructor <;> intro h <;>
     simp only [Finset.mem_map, Finset.mem_attach, true_and, Subtype.exists, Embedding.coeFn_mk,
       exists_and_right, exists_eq_right, Subtype.impEmbedding, Subtype.mk.injEq] at *
-    · rcases h with ⟨_, ⟨_, h₁⟩, h₂⟩; exact h₂ ▸ h₁
-    · use a, ⟨a.property, h⟩
+    · rcases h with ⟨_, _, h₁, h₂⟩; exact h₂ ▸ h₁
+    · use s.property _ h, a
 
 end Equiv
diff --git a/Mathlib/Data/Set/Basic.lean b/Mathlib/Data/Set/Basic.lean
index 5138f0cd59ec2..cb8ba8791dc30 100644
--- a/Mathlib/Data/Set/Basic.lean
+++ b/Mathlib/Data/Set/Basic.lean
@@ -2171,14 +2171,14 @@ end Disjoint
 namespace Equiv
 
 /-- Given a predicate `p : α → Prop`, produces an equivalence between
-  `{s : Set α // ∀ a ∈ s, p a}` and `Set {a : α // p a}`. -/
+  `Set {a : α // p a}` and `{s : Set α // ∀ a ∈ s, p a}`. -/
+@[simps]
 protected def setSubtypeCongr {α : Type*} (p : α → Prop) :
-    {s : Set α // ∀ a ∈ s, p a} ≃ (Set {a : α // p a}) where
-  toFun s a := s.val a
-  invFun s := ⟨fun a ↦ ∃ h : p a, s ⟨a, h⟩, fun _ h ↦ h.1⟩
-  left_inv s := by ext; exact ⟨fun h ↦ h.2, fun h ↦ ⟨s.property _ h, h⟩⟩
-  right_inv s := by ext a; exact ⟨fun h ↦ h.2, fun h ↦ ⟨a.property, h⟩⟩
-
+    Set {a : α // p a} ≃ {s : Set α // ∀ a ∈ s, p a} where
+  toFun s := ⟨fun a ↦ ∃ h : p a, s ⟨a, h⟩, fun _ h ↦ h.1⟩
+  invFun s a := s.val a
+  left_inv s := by ext a; exact ⟨fun h ↦ h.2, fun h ↦ ⟨a.property, h⟩⟩
+  right_inv s := by ext; exact ⟨fun h ↦ h.2, fun h ↦ ⟨s.property _ h, h⟩⟩
 
 end Equiv
 

From a3c1ee0df5094a684deb7c3547b7f72237dc718d Mon Sep 17 00:00:00 2001
From: qawbecrdtey <qawbecrdtey@kaist.ac.kr>
Date: Fri, 29 Nov 2024 13:32:20 +0900
Subject: [PATCH 5/6] Added comments on generated lemmas.

---
 Mathlib/Data/Finset/Image.lean | 16 +++++++++++++++-
 Mathlib/Data/Set/Basic.lean    | 14 +++++++++++++-
 2 files changed, 28 insertions(+), 2 deletions(-)

diff --git a/Mathlib/Data/Finset/Image.lean b/Mathlib/Data/Finset/Image.lean
index 54be6182a289a..7a7e4a9ef1c44 100644
--- a/Mathlib/Data/Finset/Image.lean
+++ b/Mathlib/Data/Finset/Image.lean
@@ -768,7 +768,20 @@ theorem finsetCongr_toEmbedding (e : α ≃ β) :
   rfl
 
 /-- Given a predicate `p : α → Prop`, produces an equivalence between
-  `Finset {a : α // p a}` and `{s : Finset α // ∀ a ∈ s, p a}`. -/
+  `Finset {a : α // p a}` and `{s : Finset α // ∀ a ∈ s, p a}`.
+
+  Theorems generated by simps:
+  
+  @[simp]
+  protected lemma finsetSubtypeCongr_apply_coe (p : α → Prop) (s : Finset {a // p a}) :
+    (Equiv.finsetSubtypeCongr p) s = s.map ⟨Subtype.val, Subtype.val_injective⟩
+
+  @[simp]
+  protected lemma finsetSubtypeCongr_symm_apply (p : α → Prop) (s : { s // ∀ a ∈ s, p a }) :
+    (Equiv.finsetSubtypeCongr p).symm s =
+      s.val.attach.map (Subtype.impEmbedding (Membership.mem s.val) p fun _ ↦ s.property _)
+  -/
+
 @[simps]
 protected def finsetSubtypeCongr (p : α → Prop) :
     Finset {a : α // p a} ≃ {s : Finset α // ∀ a ∈ s, p a} where
@@ -789,3 +802,4 @@ protected def finsetSubtypeCongr (p : α → Prop) :
     · use s.property _ h, a
 
 end Equiv
+
diff --git a/Mathlib/Data/Set/Basic.lean b/Mathlib/Data/Set/Basic.lean
index cb8ba8791dc30..a7158d7cf6b77 100644
--- a/Mathlib/Data/Set/Basic.lean
+++ b/Mathlib/Data/Set/Basic.lean
@@ -2171,7 +2171,19 @@ end Disjoint
 namespace Equiv
 
 /-- Given a predicate `p : α → Prop`, produces an equivalence between
-  `Set {a : α // p a}` and `{s : Set α // ∀ a ∈ s, p a}`. -/
+  `Set {a : α // p a}` and `{s : Set α // ∀ a ∈ s, p a}`.
+
+  Theorems generated by simps:
+
+  @[simp]
+  protected lemma setSubtypeCongr_apply_coe (p : α → Prop) (s : Set {a // p a}) (a : α) :
+    (Equiv.setSubtypeCongr p) s a = ∃ (h : p a), s ⟨a, h⟩
+
+  @[simp]
+  protected lemma setSubtypeCongr_symm_apply
+      (p : α → Prop) (s : {s // ∀ a ∈ s, p a}) (a : {a // p a}) :
+    (Equiv.setSubtypeCongr p).symm s a = s.val a.val
+  -/
 @[simps]
 protected def setSubtypeCongr {α : Type*} (p : α → Prop) :
     Set {a : α // p a} ≃ {s : Set α // ∀ a ∈ s, p a} where

From 192e81ddbc26bb2ba54c176e3a4523fef9ee9a06 Mon Sep 17 00:00:00 2001
From: qawbecrdtey <40463813+qawbecrdtey@users.noreply.github.com>
Date: Fri, 29 Nov 2024 13:35:14 +0900
Subject: [PATCH 6/6] Update Mathlib/Data/Finset/Image.lean

Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
---
 Mathlib/Data/Finset/Image.lean | 1 -
 1 file changed, 1 deletion(-)

diff --git a/Mathlib/Data/Finset/Image.lean b/Mathlib/Data/Finset/Image.lean
index 7a7e4a9ef1c44..f1437e7138084 100644
--- a/Mathlib/Data/Finset/Image.lean
+++ b/Mathlib/Data/Finset/Image.lean
@@ -771,7 +771,6 @@ theorem finsetCongr_toEmbedding (e : α ≃ β) :
   `Finset {a : α // p a}` and `{s : Finset α // ∀ a ∈ s, p a}`.
 
   Theorems generated by simps:
-  
   @[simp]
   protected lemma finsetSubtypeCongr_apply_coe (p : α → Prop) (s : Finset {a // p a}) :
     (Equiv.finsetSubtypeCongr p) s = s.map ⟨Subtype.val, Subtype.val_injective⟩