fix(SetTheory/ZFC/Basic): fix diamond for Membership ZFSet ZFSet (leanprover-community#36734)

This PR removes the manual instance of `Membership ZFSet ZFSet` in favour of the instance that comes from the `SetLike` instance. The two instances are not defeq in `implicit_reducible` transparency, hence causing a diamond (it relies on the defeq of `{x | x ∈ s}` with `s`).

This change also helps remove a lot of the `respectTransparency` options. I've extended the PR with a little more defeq-abuse cleanup.

Author: JovanGerb

Mathlib/SetTheory/ZFC/Basic.lean

@@ -167,32 +167,30 @@ theorem sound {x y : PSet} (h : PSet.Equiv x y) : mk x = mk y :=
 theorem exact {x y : PSet} : mk x = mk y → PSet.Equiv x y :=
   Quotient.exact
 
-/-- The membership relation for ZFC sets is inherited from the membership relation for pre-sets. -/
-protected def Mem : ZFSet → ZFSet → Prop :=
-  Quotient.lift₂ (· ∈ ·) fun _ _ _ _ hx hy =>
-    propext ((Mem.congr_left hx).trans (Mem.congr_right hy))
+/-- Convert a ZFC set into a `Set` of ZFC sets -/
+def toSet (x : ZFSet) : Set ZFSet :=
+  {y | Quotient.lift₂ (· ∈ ·) (fun _ _ _ _ hx hy =>
+    propext ((Mem.congr_left hx).trans (Mem.congr_right hy))) y x}
+
+private lemma ext_aux : (∀ z : ZFSet.{u}, z ∈ x.toSet ↔ z ∈ y.toSet) → x = y :=
+  Quotient.inductionOn₂ x y fun _ _ h => Quotient.sound (Mem.ext fun w => h ⟦w⟧)
+
+instance : SetLike ZFSet.{u} ZFSet.{u} where
+  coe := toSet
+  coe_injective' x y hxy := by apply ext_aux; intro z; exact congr(z ∈ $hxy)
 
-instance : Membership ZFSet ZFSet where
-  mem t s := ZFSet.Mem s t
+/-- The membership relation for ZFC sets is inherited from the membership relation for pre-sets. -/
+@[deprecated "use `∈` notation" (since := "2026-03-16")]
+protected def Mem : ZFSet → ZFSet → Prop := (· ∈ ·)
 
 @[simp]
 theorem mk_mem_iff {x y : PSet} : mk x ∈ mk y ↔ x ∈ y :=
   Iff.rfl
 
-@[ext] lemma ext : (∀ z : ZFSet.{u}, z ∈ x ↔ z ∈ y) → x = y :=
-  Quotient.inductionOn₂ x y fun _ _ h => Quotient.sound (Mem.ext fun w => h ⟦w⟧)
-
-instance : SetLike ZFSet.{u} ZFSet.{u} where
-  coe x := {y | y ∈ x}
-  coe_injective' x y hxy := by ext z; exact congr(z ∈ $hxy)
+@[ext] lemma ext : (∀ z : ZFSet.{u}, z ∈ x ↔ z ∈ y) → x = y := ext_aux
 
 instance : PartialOrder ZFSet.{u} := .ofSetLike ZFSet.{u} ZFSet.{u}
 
-/-- Convert a ZFC set into a `Set` of ZFC sets -/
-@[deprecated SetLike.coe (since := "2025-11-05")]
-def toSet (u : ZFSet.{u}) : Set ZFSet.{u} :=
-  { x | x ∈ u }
-
 @[deprecated SetLike.mem_coe (since := "2025-11-05")]
 theorem mem_toSet (a u : ZFSet.{u}) : a ∈ (u : Set ZFSet.{u}) ↔ a ∈ u :=
   Iff.rfl
@@ -279,7 +277,6 @@ instance : Inhabited ZFSet :=
 theorem notMem_empty (x) : x ∉ (∅ : ZFSet.{u}) :=
   Quotient.inductionOn x PSet.notMem_empty
 
-set_option backward.isDefEq.respectTransparency false in
 @[simp, norm_cast] lemma coe_empty : ((∅ : ZFSet.{u}) : Set ZFSet.{u}) = ∅ := by ext; simp
 
 @[deprecated (since := "2025-11-05")] alias toSet_empty := coe_empty
@@ -341,7 +338,6 @@ theorem mem_insert (x y : ZFSet) : x ∈ insert x y :=
 theorem mem_insert_of_mem {y z : ZFSet} (x) (h : z ∈ y) : z ∈ insert x y :=
   mem_insert_iff.2 <| Or.inr h
 
-set_option backward.isDefEq.respectTransparency false in
 @[simp, norm_cast]
 lemma coe_insert (x y : ZFSet) : ↑(insert x y) = (insert x ↑y : Set ZFSet) := by ext; simp
 
@@ -354,7 +350,6 @@ theorem mem_singleton {x y : ZFSet.{u}} : x ∈ ({y} : ZFSet.{u}) ↔ x = y :=
 theorem notMem_singleton {x y : ZFSet.{u}} : x ∉ ({y} : ZFSet.{u}) ↔ x ≠ y :=
   mem_singleton.not
 
-set_option backward.isDefEq.respectTransparency false in
 @[simp, norm_cast]
 lemma coe_singleton (x : ZFSet) : (({x} : ZFSet) : Set ZFSet) = {x} := by ext; simp
 
@@ -432,7 +427,6 @@ theorem sep_empty (p : ZFSet → Prop) : (∅ : ZFSet).sep p = ∅ :=
 theorem sep_subset {x p} : ZFSet.sep p x ⊆ x :=
   fun _ h => (mem_sep.1 h).1
 
-set_option backward.isDefEq.respectTransparency false in
 @[simp, norm_cast]
 lemma coe_sep (a : ZFSet) (p : ZFSet → Prop) : (ZFSet.sep p a : Set ZFSet) = {x ∈ a | p x} := by
   ext
@@ -534,15 +528,13 @@ theorem sUnion_singleton {x : ZFSet.{u}} : ⋃₀ ({x} : ZFSet) = x :=
 theorem sInter_singleton {x : ZFSet.{u}} : ⋂₀ ({x} : ZFSet) = x :=
   ext fun y => by simp_rw [mem_sInter (singleton_nonempty x), mem_singleton, forall_eq]
 
-set_option backward.isDefEq.respectTransparency false in
 @[simp, norm_cast]
 lemma coe_sUnion (x : ZFSet.{u}) : (⋃₀ x : Set ZFSet) = ⋃₀ (SetLike.coe '' (x : Set ZFSet)) := by
   ext
   simp
 
 @[deprecated (since := "2025-11-05")] alias toSet_sUnion := coe_sUnion
 
-set_option backward.isDefEq.respectTransparency false in
 @[simp, norm_cast]
 lemma coe_sInter (h : x.Nonempty) : (⋂₀ x : Set ZFSet) = ⋂₀ (SetLike.coe '' (x : Set ZFSet)) := by
   ext
@@ -590,19 +582,16 @@ instance : SDiff ZFSet :=
 
 @[deprecated (since := "2025-11-06")] alias mem_diff := mem_sdiff
 
-set_option backward.isDefEq.respectTransparency false in
 @[simp, norm_cast]
 lemma coe_union (x y : ZFSet.{u}) : ↑(x ∪ y) = (↑x ∪ ↑y : Set ZFSet) := by ext; simp
 
 @[deprecated (since := "2025-11-05")] alias toSet_union := coe_union
 
-set_option backward.isDefEq.respectTransparency false in
 @[simp, norm_cast]
 lemma coe_inter (x y : ZFSet.{u}) : ↑(x ∩ y) = (↑x ∩ ↑y : Set ZFSet) := by ext; simp
 
 @[deprecated (since := "2025-11-05")] alias toSet_inter := coe_inter
 
-set_option backward.isDefEq.respectTransparency false in
 @[simp, norm_cast]
 lemma coe_sdiff (x y : ZFSet.{u}) : ↑(x \ y) = (↑x \ ↑y : Set ZFSet) := by ext; simp
 
@@ -611,7 +600,6 @@ lemma coe_sdiff (x y : ZFSet.{u}) : ↑(x \ y) = (↑x \ ↑y : Set ZFSet) := by
 @[simp] lemma inter_eq_left_of_subset (hxy : x ⊆ y) : x ∩ y = x := by ext; simpa using @hxy _
 @[simp] lemma inter_eq_right_of_subset (hyx : y ⊆ x) : x ∩ y = y := by ext; simpa using @hyx _
 
-set_option backward.isDefEq.respectTransparency false in
 /-- `ZFSet.powerset` is equivalent to `Set.powerset`. -/
 def powersetEquiv (x : ZFSet.{u}) : x.powerset ≃ 𝒫 (x : Set ZFSet) where
   toFun y := ⟨y.1, Set.mem_powerset (mem_powerset.1 y.2)⟩
@@ -681,7 +669,6 @@ theorem mem_image {f : ZFSet.{u} → ZFSet.{u}} [Definable₁ f] {x y : ZFSet.{u
     ⟨fun ⟨a, ya⟩ => ⟨⟦A a⟧, Mem.mk A a, ((Quotient.sound ya).trans Definable₁.mk_out).symm⟩,
       fun ⟨_, hz, e⟩ => e ▸ image.mk _ _ hz⟩
 
-set_option backward.isDefEq.respectTransparency false in
 @[simp, norm_cast]
 lemma coe_image (f : ZFSet → ZFSet) [Definable₁ f] (x : ZFSet) :
     (image f x : Set ZFSet) = f '' x := by ext; simp
@@ -706,7 +693,6 @@ theorem mem_range {f : α → ZFSet.{u}} {x : ZFSet.{u}} : x ∈ range f ↔ ∃
       use equivShrink α z
       simpa [hz] using PSet.Equiv.symm (Quotient.mk_out y)
 
-set_option backward.isDefEq.respectTransparency false in
 @[simp, norm_cast]
 lemma coe_range (f : α → ZFSet.{u}) : (range f : Set ZFSet) = .range f := by ext; simp
 
@@ -724,7 +710,6 @@ noncomputable def iUnion (f : α → ZFSet.{u}) : ZFSet.{u} :=
 theorem mem_iUnion {f : α → ZFSet.{u}} {x : ZFSet.{u}} : x ∈ ⋃ i, f i ↔ ∃ i, x ∈ f i := by
   simp [iUnion]
 
-set_option backward.isDefEq.respectTransparency false in
 @[simp, norm_cast]
 lemma coe_iUnion (f : α → ZFSet.{u}) : ↑(⋃ i, f i) = ⋃ i, (f i : Set ZFSet) := by
   ext

Mathlib/SetTheory/ZFC/Cardinal.lean

@@ -39,18 +39,15 @@ theorem cardinalMk_coe_sort : #x = lift.{u + 1, u} (card x) := by
 theorem card_mono (h : x ⊆ y) : card x ≤ card y := by
   simpa [cardinalMk_coe_sort] using mk_le_mk_of_subset (coe_subset_coe.2 h)
 
-set_option backward.isDefEq.respectTransparency false in
 @[simp]
 theorem card_empty : card ∅ = 0 := by
   rw [← lift_inj, ← cardinalMk_coe_sort]
   simp
 
-set_option backward.isDefEq.respectTransparency false in
 theorem card_insert_le : card (insert x y) ≤ card y + 1 := by
   rw [← lift_le.{u + 1}]
   simpa [← cardinalMk_coe_sort] using mk_insert_le
 
-set_option backward.isDefEq.respectTransparency false in
 theorem card_insert (h : x ∉ y) : card (insert x y) = card y + 1 := by
   rw [← lift_inj.{u, u + 1}]
   simpa [← cardinalMk_coe_sort] using mk_insert (SetLike.mem_coe.not.2 h)
@@ -63,7 +60,6 @@ theorem card_pair_of_ne (h : x ≠ y) : card {x, y} = 2 := by
   convert card_insert (notMem_singleton.2 h)
   rw [card_singleton, one_add_one_eq_two]
 
-set_option backward.isDefEq.respectTransparency false in
 theorem card_union_le : card (x ∪ y) ≤ card x + card y := by
   rw [← lift_le.{u + 1}]
   simpa [← cardinalMk_coe_sort] using mk_union_le (x : Set ZFSet) y

Mathlib/SetTheory/ZFC/Class.lean

@@ -62,6 +62,10 @@ instance : Coe ZFSet Class :=
 def univ : Class :=
   Set.univ
 
+instance : Top Class := ⟨univ⟩
+
+deriving instance CompleteLattice for Class
+
 /-- Assert that `A` is a ZFC set satisfying `B` -/
 def ToSet (B : Class.{u}) (A : Class.{u}) : Prop :=
   ∃ x : ZFSet, ↑x = A ∧ B x
@@ -148,15 +152,15 @@ def powerset (x : Class) : Class :=
 /-- The union of a class is the class of all members of ZFC sets in the class. Uses `⋃₀` notation,
 scoped under the `Class` namespace. -/
 def sUnion (x : Class) : Class :=
-  ⋃₀ classToCong x
+  sSup (classToCong x)
 
 @[inherit_doc]
 scoped prefix:110 "⋃₀ " => Class.sUnion
 
 /-- The intersection of a class is the class of all members of ZFC sets in the class .
 Uses `⋂₀` notation, scoped under the `Class` namespace. -/
 def sInter (x : Class) : Class :=
-  ⋂₀ classToCong x
+  sInf (classToCong x)
 
 @[inherit_doc]
 scoped prefix:110 "⋂₀ " => Class.sInter
@@ -263,10 +267,9 @@ theorem sUnion_empty : ⋃₀ (∅ : Class.{u}) = (∅ : Class.{u}) := by
   ext
   simp
 
-set_option backward.isDefEq.respectTransparency false in
 @[simp]
 theorem sInter_empty : ⋂₀ (∅ : Class.{u}) = univ := by
-  rw [sInter, classToCong_empty, Set.sInter_empty, univ]
+  simp [sInter, Top.top]
 
 /-- An induction principle for sets. If every subset of a class is a member, then the class is
   universal. -/
@@ -345,8 +348,6 @@ theorem choice_mem (h : ∅ ∉ x) (y : ZFSet.{u}) (yx : y ∈ x) :
   rw [@map_fval _ (Classical.allZFSetDefinable _) x y yx, Class.coe_mem, Class.coe_apply]
   exact choice_mem_aux x h y yx
 
-set_option backward.isDefEq.respectTransparency false in
-set_option backward.privateInPublic true in
 private lemma coe_equiv_aux {s : Set ZFSet.{u}} (hs : Small.{u} s) :
     (mk <| PSet.mk (Shrink s) fun x ↦ ((equivShrink s).symm x).1.out) = s := by
   ext x
@@ -357,16 +358,14 @@ private lemma coe_equiv_aux {s : Set ZFSet.{u}} (hs : Small.{u} s) :
     simp [h2]
   · simp [PSet.Equiv.refl]
 
-set_option backward.privateInPublic true in
-set_option backward.privateInPublic.warn false in
 /-- `SetLike.coe` as an equivalence. -/
 @[simps apply_coe]
 noncomputable def coeEquiv : ZFSet.{u} ≃ {s : Set ZFSet.{u} // Small.{u, u+1} s} where
   toFun x := ⟨x, x.small_coe⟩
   invFun := fun ⟨s, _⟩ ↦ mk <| PSet.mk (Shrink s) fun x ↦ ((equivShrink.{u, u + 1} s).symm x).1.out
-  left_inv := Function.rightInverse_of_injective_of_leftInverse (by intro _ _; simp)
+  left_inv := private Function.rightInverse_of_injective_of_leftInverse (by intro _ _; simp)
     fun s ↦ Subtype.coe_injective <| coe_equiv_aux s.2
-  right_inv s := Subtype.coe_injective <| coe_equiv_aux s.2
+  right_inv s := private Subtype.coe_injective <| coe_equiv_aux s.2
 
 @[deprecated (since := "2025-11-05")] alias toSet_equiv := coeEquiv
 

Mathlib/SetTheory/ZFC/Ordinal.lean

@@ -321,7 +321,6 @@ theorem mem_toZFSet_iff {o : Ordinal} {x : ZFSet} : x ∈ o.toZFSet ↔ ∃ a <
 theorem rank_toZFSet (o : Ordinal) : o.toZFSet.rank = o :=
   rank_toPSet o
 
-set_option backward.isDefEq.respectTransparency false in
 @[simp]
 theorem coe_toZFSet {o : Ordinal} : o.toZFSet = toZFSet '' Iio o := by
   ext