awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.SetTheory.ZFC.Class
Goal:
x : Class.{u_1}
y : ZFSet.{u_1}
mp : (⋃₀ x) y → ∃ (z : ZFSet.{u_1}), x z ∧ y ∈ z
mpr : (∃ (z : ZFSet.{u_1}), x z ∧ y ∈ z) → (⋃₀ x) y
⊢ (⋃₀ x) y ↔ ∃ (z : ZFSet.{u_1}), x z ∧ y ∈ z

Tactic:
constructor
-- Module: Mathlib.SetTheory.ZFC.Class
Goal:
x : Class.{u_1}
y z : ZFSet.{u_1}
hxz : x z
hyz : y ∈ (↑z : Class.{u_1})
⊢ ∃ (z : ZFSet.{u_1}), x z ∧ y ∈ z

Tactic:
⟨z, hxz, hyz⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.SetTheory.ZFC.Class
Goal:
x : Class.{u_1}
y z : ZFSet.{u_1}
hxz : x z
hyz : y ∈ (↑z : Class.{u_1})
⊢ ∃ (z : ZFSet.{u_1}), x z ∧ y ∈ z

Tactic:
exact ⟨z, hxz, hyz⟩
-- Module: Mathlib.SetTheory.ZFC.Class
Goal:
x : Class.{u_1}
y : ZFSet.{u_1}
⊢ (∃ (z : ZFSet.{u_1}), x z ∧ y ∈ z) → (⋃₀ x) y

Tactic:
fun ⟨z, hxz, hyz⟩ => ⟨_, coe_mem.2 hxz, hyz⟩

Premises used: Iff.mpr, Class.ofSet, Class.coe_mem, _private.0.Class.sUnion_apply.match_1, And.intro, Exists.intro, Class.sUnion
-- Module: Mathlib.SetTheory.ZFC.Class
Goal:
x : Class.{u_1}
y : ZFSet.{u_1}
⊢ (∃ (z : ZFSet.{u_1}), x z ∧ y ∈ z) → (⋃₀ x) y

Tactic:
exact fun ⟨z, hxz, hyz⟩ => ⟨_, coe_mem.2 hxz, hyz⟩
-- Module: Mathlib.SetTheory.ZFC.Class
Goal:
x y : ZFSet.{u}
⊢ (∃ (z : ZFSet.{u}), (↑x : Class.{u}) z ∧ y ∈ z) ↔ ∃ z ∈ x, y ∈ z

Tactic:
rfl
-- Module: Mathlib.SetTheory.ZFC.Class
Goal:
x y : Class.{u}
mp : y ∈ ⋃₀ x → ∃ z ∈ x, y ∈ z
mpr : (∃ z ∈ x, y ∈ z) → y ∈ ⋃₀ x
⊢ y ∈ ⋃₀ x ↔ ∃ z ∈ x, y ∈ z

Tactic:
constructor
-- Module: Mathlib.SetTheory.ZFC.Class
Goal:
x : Class.{u}
w : ZFSet.{u}
z : Set ZFSet.{u}
hzx : z ∈ x.classToCong
hwz : w ∈ z
⊢ ∃ z ∈ x, (↑w : Class.{u}) ∈ z

Tactic:
⟨z, hzx, coe_mem.2 hwz⟩

Premises used: Iff.mpr, Class.coe_mem, And.intro, Exists.intro
-- Module: Mathlib.SetTheory.ZFC.Class
Goal:
x : Class.{u}
w : ZFSet.{u}
z : Set ZFSet.{u}
hzx : z ∈ x.classToCong
hwz : w ∈ z
⊢ ∃ z ∈ x, (↑w : Class.{u}) ∈ z

Tactic:
exact ⟨z, hzx, coe_mem.2 hwz⟩
-- Module: Mathlib.SetTheory.ZFC.Class
Goal:
x w : Class.{u}
hwx : w ∈ x
z : ZFSet.{u}
hwz : w z
⊢ (↑z : Class.{u}) ∈ ⋃₀ x

Tactic:
⟨z, rfl, w, hwx, hwz⟩

Premises used: Class.Mem, Class.ToSet, And.intro, Exists.intro, rfl
-- Module: Mathlib.SetTheory.ZFC.Class
Goal:
x w : Class.{u}
hwx : w ∈ x
z : ZFSet.{u}
hwz : w z
⊢ (↑z : Class.{u}) ∈ ⋃₀ x

Tactic:
exact ⟨z, rfl, w, hwx, hwz⟩
-- Module: Mathlib.SetTheory.ZFC.Class
Goal:
x : Class.{u}
y : ZFSet.{u}
⊢ (⋂₀ x) y ↔ ∀ (z : ZFSet.{u}), x z → y ∈ z

Tactic:
⟨fun hxy z hxz => hxy _ ⟨z, rfl, hxz⟩, ?_⟩

Premises used: SetLike.coe, And.intro, Iff.intro, Exists.intro, rfl
-- Module: Mathlib.SetTheory.ZFC.Class
Goal:
x : Class.{u}
y : ZFSet.{u}
refine : (∀ (z : ZFSet.{u}), x z → y ∈ z) → (⋂₀ x) y
⊢ (⋂₀ x) y ↔ ∀ (z : ZFSet.{u}), x z → y ∈ z

Tactic:
refine ⟨fun hxy z hxz => hxy _ ⟨z, rfl, hxz⟩, ?_⟩
-- Module: Mathlib.SetTheory.ZFC.Class
Goal:
x : Class.{u}
y : ZFSet.{u}
H : ∀ (z : ZFSet.{u}), x z → y ∈ z
z : ZFSet.{u}
hxz : x z
⊢ y ∈ (↑z : Class.{u})

Tactic:
H _ hxz

Premises used: Class.ofSet, Set.Mem, setOf, ZFSet.toSet
-- Module: Mathlib.SetTheory.ZFC.Class
Goal:
x : Class.{u}
y : ZFSet.{u}
H : ∀ (z : ZFSet.{u}), x z → y ∈ z
z : ZFSet.{u}
hxz : x z
⊢ y ∈ (↑z : Class.{u})

Tactic:
exact H _ hxz
-- Module: Mathlib.SetTheory.ZFC.Class
Goal:
x : ZFSet.{u}
h : x.Nonempty
⊢ (↑(⋂₀ x) : Class.{u}) = ⋂₀ (↑x : Class.{u})

Tactic:
Set.ext fun _ => (ZFSet.mem_sInter h).trans sInter_apply.symm

Premises used: Set.ext, Class.sInter_apply, Class, Iff.trans, Iff.symm, ZFSet.mem_sInter
-- Module: Mathlib.SetTheory.ZFC.Class
Goal:
x y z : Class.{u_1}
hy : y ∈ ⋂₀ x
hz : z ∈ x
obtain : ∀ (w : ZFSet.{u_1}) (hw : (⋂₀ x) w), (↑w : Class.{u_1}) ∈ z
⊢ y ∈ z

Tactic:
obtain ⟨w, rfl, hw⟩ := hy

Premises used: rfl
-- Module: Mathlib.SetTheory.ZFC.Class
Goal:
x z : Class.{u_1}
hz : z ∈ x
w : ZFSet.{u_1}
hw : (⋂₀ x) w
⊢ (↑w : Class.{u_1}) ∈ z

Tactic:
coe_mem.2 (hw z hz)

Premises used: Iff.mpr, Class.coe_mem
-- Module: Mathlib.SetTheory.ZFC.Class
Goal:
x z : Class.{u_1}
hz : z ∈ x
w : ZFSet.{u_1}
hw : (⋂₀ x) w
⊢ (↑w : Class.{u_1}) ∈ z

Tactic:
exact coe_mem.2 (hw z hz)

Premises used: Iff.mpr, Class.coe_mem
-- Module: Mathlib.SetTheory.ZFC.Class
Goal:
x y : Class.{u}
h : Set.Nonempty x
⊢ y ∈ ⋂₀ x ↔ ∀ z ∈ x, y ∈ z

Tactic:
⟨fun hy z => mem_of_mem_sInter hy, fun H => ?_⟩

Premises used: Class.mem_of_mem_sInter, Iff.intro
-- Module: Mathlib.SetTheory.ZFC.Class
Goal:
x y : Class.{u}
h : Set.Nonempty x
refine : ∀ (H : ∀ z ∈ x, y ∈ z), y ∈ ⋂₀ x
⊢ y ∈ ⋂₀ x ↔ ∀ z ∈ x, y ∈ z

Tactic:
refine ⟨fun hy z => mem_of_mem_sInter hy, fun H => ?_⟩
-- Module: Mathlib.SetTheory.ZFC.Class
Goal:
x y : Class.{u}
h : Set.Nonempty x
H : ∀ z ∈ x, y ∈ z
simp_rw : ∃ (x_1 : ZFSet.{u}), (↑x_1 : Class.{u}) = y ∧ ∀ (z : ZFSet.{u}), x z → x_1 ∈ z
⊢ y ∈ ⋂₀ x

Tactic:
simp_rw [mem_def, sInter_apply]

Premises used: Class.sInter_apply, Class.mem_def
-- Module: Mathlib.SetTheory.ZFC.Class
Goal:
x y : Class.{u}
h : Set.Nonempty x
H : ∀ z ∈ x, y ∈ z
obtain : ∀ (z : ZFSet.{u}) (hz : z ∈ x), ∃ (x_1 : ZFSet.{u}), (↑x_1 : Class.{u}) = y ∧ ∀ (z : ZFSet.{u}), x z → x_1 ∈ z
⊢ ∃ (x_1 : ZFSet.{u}), (↑x_1 : Class.{u}) = y ∧ ∀ (z : ZFSet.{u}), x z → x_1 ∈ z

Tactic:
obtain ⟨z, hz⟩ := h
-- Module: Mathlib.SetTheory.ZFC.Class
Goal:
x y : Class.{u}
H : ∀ z ∈ x, y ∈ z
z : ZFSet.{u}
hz : z ∈ x
obtain :
  ∀ (y : ZFSet.{u}),
    (↑z : Class.{u}) y →
      ∀ (H : ∀ z ∈ x, (↑y : Class.{u}) ∈ z),
        ∃ (x_1 : ZFSet.{u}), (↑x_1 : Class.{u}) = (↑y : Class.{u}) ∧ ∀ (z : ZFSet.{u}), x z → x_1 ∈ z
⊢ ∃ (x_1 : ZFSet.{u}), (↑x_1 : Class.{u}) = y ∧ ∀ (z : ZFSet.{u}), x z → x_1 ∈ z

Tactic:
obtain ⟨y, rfl, _⟩ := H z (coe_mem.2 hz)

Premises used: Iff.mpr, Class.ofSet, Class.coe_mem, rfl
-- Module: Mathlib.SetTheory.ZFC.Class
Goal:
x : Class.{u}
z : ZFSet.{u}
hz : z ∈ x
y : ZFSet.{u}
right : (↑z : Class.{u}) y
H : ∀ z ∈ x, (↑y : Class.{u}) ∈ z
⊢ ∃ (x_1 : ZFSet.{u}), (↑x_1 : Class.{u}) = (↑y : Class.{u}) ∧ ∀ (z : ZFSet.{u}), x z → x_1 ∈ z

Tactic:
⟨y, rfl, fun w hxw => ?_⟩

Premises used: And.intro, Exists.intro, rfl
-- Module: Mathlib.SetTheory.ZFC.Class
Goal:
x : Class.{u}
z : ZFSet.{u}
hz : z ∈ x
y : ZFSet.{u}
right : (↑z : Class.{u}) y
H : ∀ z ∈ x, (↑y : Class.{u}) ∈ z
refine : ∀ (w : ZFSet.{u}) (hxw : x w), y ∈ w
⊢ ∃ (x_1 : ZFSet.{u}), (↑x_1 : Class.{u}) = (↑y : Class.{u}) ∧ ∀ (z : ZFSet.{u}), x z → x_1 ∈ z

Tactic:
refine ⟨y, rfl, fun w hxw => ?_⟩
-- Module: Mathlib.SetTheory.ZFC.Class
Goal:
x : Class.{u}
z : ZFSet.{u}
hz : z ∈ x
y : ZFSet.{u}
right : (↑z : Class.{u}) y
H : ∀ z ∈ x, (↑y : Class.{u}) ∈ z
w : ZFSet.{u}
hxw : x w
⊢ y ∈ w

Tactic:
simpa only [coe_mem, coe_apply] using H w (coe_mem.2 hxw)

Premises used: Iff.mpr, Class.ofSet, Class.coe_mem, Class.coe_apply
-- Module: Mathlib.SetTheory.ZFC.Class
Goal:
a : ∀ (z : ZFSet.{u}), (⋃₀ ∅) z ↔ ∅ z
⊢ ⋃₀ ∅ = ∅

Tactic:
ext
-- Module: Mathlib.SetTheory.ZFC.Class
Goal:
z : ZFSet.{u}
⊢ (⋃₀ ∅) z ↔ ∅ z

Tactic:
simp
-- Module: Mathlib.SetTheory.ZFC.Class
Goal:
⊢ ⋂₀ ∅ = univ

Tactic:
simp [sInter, Top.top]

Premises used: Top.top, Class.sInter
-- Module: Mathlib.SetTheory.ZFC.Class
Goal:
A : Class.{u_1}
hA : A.powerset ⊆ A
by_contra! : ∀ (hnA : ∃ (x : ZFSet.{u_1}), ¬A x), False
⊢ ∀ (x : ZFSet.{u_1}), A x

Tactic:
by_contra! hnA
-- Module: Mathlib.SetTheory.ZFC.Class
Goal:
A : Class.{u_1}
hA : A.powerset ⊆ A
hnA : ∃ (x : ZFSet.{u_1}), ¬A x
⊢ False

Tactic:
WellFounded.min_mem ZFSet.mem_wf _ hnA
          (hA fun x hx =>
            Classical.not_not.1 fun hB =>
              WellFounded.not_lt_min ZFSet.mem_wf _ hB <| coe_apply.1 hx)

Premises used: WellFounded.min_mem, Classical.not_not, Class.coe_apply, ZFSet.mem_wf, Iff.mp, WellFounded.not_lt_min
-- Module: Mathlib.SetTheory.ZFC.Class
Goal:
A : Class.{u_1}
hA : A.powerset ⊆ A
hnA : ∃ (x : ZFSet.{u_1}), ¬A x
⊢ False

Tactic:
exact
        WellFounded.min_mem ZFSet.mem_wf _ hnA
          (hA fun x hx =>
            Classical.not_not.1 fun hB =>
              WellFounded.not_lt_min ZFSet.mem_wf _ hB <| coe_apply.1 hx)

Premises used: WellFounded.min_mem, Classical.not_not, Class.coe_apply, ZFSet.mem_wf, Iff.mp, WellFounded.not_lt_min
-- Module: Mathlib.SetTheory.ZFC.Class
Goal:
A : Class.{u_1}
x : ZFSet.{u_1}
H : ∀ (y : ZFSet.{u_1}), A y ↔ y = x
y : ZFSet.{u_1}
h_1 : A.iota y
x' : ZFSet.{u_1}
h : {x : ZFSet.{u_1} | ∀ (y : ZFSet.{u_1}), A y ↔ y = x} x'
yx' : y ∈ (↑x' : Class.{u_1})
rwa rwa₁ rwa₂ rwa₃ : (↑x' : Class.{u_1}) y
⊢ (↑x : Class.{u_1}) y

Tactic:
rwa [← (H x').1 <| (h x').2 rfl]

Premises used: Iff.mpr, Iff.mp, rfl
-- Module: Mathlib.SetTheory.ZFC.Class
Goal:
A : Class.{u}
⊢ A.iota ∈ univ

Tactic:
mem_univ.2 <|
    Or.elim (Classical.em <| ∃ x, ∀ y, A y ↔ y = x) (fun ⟨x, h⟩ => ⟨x, Eq.symm <| iota_val A x h⟩)
      fun hn =>
      ⟨∅, ext fun _ => coe_empty.symm ▸ ⟨False.rec, fun ⟨_, ⟨x, rfl, H⟩, _⟩ => hn ⟨x, H⟩⟩⟩

Premises used: Iff.mpr, Class.ofSet, Class.iota_val, Class.mem_univ, Class.ext, _private.0.Class.iota_ex.match_1, Class.iota, Exists, Eq.rec, Class.coe_empty, _private.0.Class.iota_val.match_1, Iff.intro, Classical.em, Exists.intro, False.rec, EmptyCollection.emptyCollection, Or.elim, Eq.symm, Eq
-- Module: Mathlib.SetTheory.ZFC.Class
Goal:
F A : Class.{u}
⊢ F ′ A ∈ univ

Tactic:
iota_ex _

Premises used: Class.iota_ex, Class.fval
-- Module: Mathlib.SetTheory.ZFC.Class
Goal:
f : ZFSet.{u} → ZFSet.{u}
inst : Definable₁ f
x y : ZFSet.{u}
h : y ∈ x
z : ZFSet.{u}
rw : (∃ z_1 ∈ x, z_1.pair (f z_1) = y.pair z) ↔ z = f y
⊢ Class.ToSet.{u} (fun (x_1 : ZFSet.{u}) ↦ (↑(map f x) : Class.{u}) (x_1.pair z)) (↑y : Class.{u}) ↔ z = f y

Tactic:
rw [Class.toSet_of_ZFSet, Class.coe_apply, mem_map]

Premises used: Class.coe_apply, Class.toSet_of_ZFSet, ZFSet.mem_map
-- Module: Mathlib.SetTheory.ZFC.Class
Goal:
f : ZFSet.{u} → ZFSet.{u}
inst : Definable₁ f
x y : ZFSet.{u}
h : y ∈ x
z : ZFSet.{u}
h_1 : ∃ z_1 ∈ x, z_1.pair (f z_1) = y.pair z
w : ZFSet.{u}
left : w ∈ x
pr : w.pair (f w) = y.pair z
⊢ w = y

Tactic:
let ⟨wy, fw⟩ := ZFSet.pair_injective pr
-- Module: Mathlib.SetTheory.ZFC.Class
Goal:
f : ZFSet.{u} → ZFSet.{u}
inst : Definable₁ f
x y : ZFSet.{u}
h : y ∈ x
z : ZFSet.{u}
h_1 : ∃ z_1 ∈ x, z_1.pair (f z_1) = y.pair z
w : ZFSet.{u}
left : w ∈ x
pr : w.pair (f w) = y.pair z
wy : w = y
⊢ f w = z

Tactic:
let ⟨wy, fw⟩ := ZFSet.pair_injective pr
-- Module: Mathlib.SetTheory.ZFC.Class
Goal:
f : ZFSet.{u} → ZFSet.{u}
inst : Definable₁ f
x y : ZFSet.{u}
h : y ∈ x
z : ZFSet.{u}
h_1 : ∃ z_1 ∈ x, z_1.pair (f z_1) = y.pair z
w : ZFSet.{u}
left : w ∈ x
pr : w.pair (f w) = y.pair z
wy : w = y
fw : f w = z
rw : f w = f y
rw₁ rw₂ : f y = f y
⊢ z = f y

Tactic:
rw [← fw, wy]
-- Module: Mathlib.SetTheory.ZFC.Class
Goal:
f : ZFSet.{u} → ZFSet.{u}
inst : Definable₁ f
x y : ZFSet.{u}
h : y ∈ x
z : ZFSet.{u}
e : z = f y
subst : ∃ z ∈ x, z.pair (f z) = y.pair (f y)
⊢ ∃ z_1 ∈ x, z_1.pair (f z_1) = y.pair z

Tactic:
subst e
-- Module: Mathlib.SetTheory.ZFC.Class
Goal:
f : ZFSet.{u} → ZFSet.{u}
inst : Definable₁ f
x y : ZFSet.{u}
h : y ∈ x
⊢ ∃ z ∈ x, z.pair (f z) = y.pair (f y)

Tactic:
⟨_, h, rfl⟩

Premises used: And.intro, Exists.intro, rfl
-- Module: Mathlib.SetTheory.ZFC.Class
Goal:
f : ZFSet.{u} → ZFSet.{u}
inst : Definable₁ f
x y : ZFSet.{u}
h : y ∈ x
⊢ ∃ z ∈ x, z.pair (f z) = y.pair (f y)

Tactic:
exact ⟨_, h, rfl⟩
-- Module: Mathlib.SetTheory.ZFC.Class
Goal:
f : ZFSet.{u} → ZFSet.{u}
inst : Definable₁ f
x y : ZFSet.{u}
h : y ∈ x
z : ZFSet.{u}
⊢ (∃ z_1 ∈ x, z_1.pair (f z_1) = y.pair z) ↔ z = f y

Tactic:
exact
      ⟨fun ⟨w, _, pr⟩ => by
        let ⟨wy, fw⟩ := ZFSet.pair_injective pr
        rw [← fw, wy], fun e => by
        subst e
        exact ⟨_, h, rfl⟩⟩
-- Module: Mathlib.SetTheory.ZFC.Class
Goal:
x : ZFSet.{u}
h : ∅ ∉ x
y : ZFSet.{u}
yx : y ∈ x
n : ¬∃ (y_1 : ZFSet.{u}), y_1 ∈ y
rwa rwa₁ rwa₂ rwa₃ : y ∈ x
⊢ ∅ ∈ x

Tactic:
rwa [← (eq_empty y).2 fun z zx => n ⟨z, zx⟩]

Premises used: Iff.mpr, ZFSet.eq_empty, Exists.intro
-- Module: Mathlib.SetTheory.ZFC.Class
Goal:
x : ZFSet.{u}
h : ∅ ∉ x
⊢ x.IsFunc (⋃₀ x) x.choice

Tactic:
(@map_isFunc _ (Classical.allZFSetDefinable _) _ _).2 fun y yx =>
    mem_sUnion.2 ⟨y, yx, choice_mem_aux x h y yx⟩

Premises used: Iff.mpr, ZFSet.map_isFunc, ZFSet.mem_sUnion, And.intro, Exists.intro, ZFSet.choice, ZFSet.choice_mem_aux
-- Module: Mathlib.SetTheory.ZFC.Class
Goal:
x : ZFSet.{u}
h : ∅ ∉ x
y : ZFSet.{u}
yx : y ∈ x
rw : (Classical.epsilon fun (z : ZFSet.{u}) ↦ z ∈ y) ∈ y
⊢ (↑(map (fun (y : ZFSet.{u}) ↦ Classical.epsilon fun (z : ZFSet.{u}) ↦ z ∈ y) x) : Class.{u}) ′ (↑y : Class.{u}) ∈
    (↑y : Class.{u})

Tactic:
rw [@map_fval _ (Classical.allZFSetDefinable _) x y yx, Class.coe_mem, Class.coe_apply]

Premises used: Class.coe_mem, Class.coe_apply, ZFSet.map_fval
-- Module: Mathlib.SetTheory.ZFC.Class
Goal:
x : ZFSet.{u}
h : ∅ ∉ x
y : ZFSet.{u}
yx : y ∈ x
⊢ (Classical.epsilon fun (z : ZFSet.{u}) ↦ z ∈ y) ∈ y

Tactic:
choice_mem_aux x h y yx

Premises used: ZFSet.choice_mem_aux
-- Module: Mathlib.SetTheory.ZFC.Class
Goal:
x : ZFSet.{u}
h : ∅ ∉ x
y : ZFSet.{u}
yx : y ∈ x
⊢ (Classical.epsilon fun (z : ZFSet.{u}) ↦ z ∈ y) ∈ y

Tactic:
exact choice_mem_aux x h y yx

Premises used: ZFSet.choice_mem_aux
-- Module: Mathlib.SetTheory.ZFC.Class
Goal:
s : Set ZFSet.{u}
hs : Small.{u, u + 1} (↑s : Type (u + 1))
h :
  ∀ (x : ZFSet.{u}),
    x ∈
        (↑(mk
              (PSet.mk (Shrink.{u, u + 1} (↑s : Type (u + 1))) fun (x : Shrink.{u, u + 1} (↑s : Type (u + 1))) ↦
                Quotient.out (s := PSet.setoid)
                  (↑((Equiv.symm (equivShrink (↑s : Type (u + 1))) :
                          (a : Shrink.{u, u + 1} (↑s : Type (u + 1))) → (↑s : Type (u + 1)))
                        x) :
                    ZFSet.{u}))) :
          Set ZFSet.{u}) ↔
      x ∈ s
⊢ (↑(mk
          (PSet.mk (Shrink.{u, u + 1} (↑s : Type (u + 1))) fun (x : Shrink.{u, u + 1} (↑s : Type (u + 1))) ↦
            Quotient.out (s := PSet.setoid)
              (↑((Equiv.symm (equivShrink (↑s : Type (u + 1))) :
                      (a : Shrink.{u, u + 1} (↑s : Type (u + 1))) → (↑s : Type (u + 1)))
                    x) :
                ZFSet.{u}))) :
      Set ZFSet.{u}) =
    s

Tactic:
ext x
-- Module: Mathlib.SetTheory.ZFC.Class
Goal:
s : Set ZFSet.{u}
hs : Small.{u, u + 1} (↑s : Type (u + 1))
x : ZFSet.{u}
h :
  (Quotient.out x ∈
      PSet.mk (Shrink.{u, u + 1} (↑s : Type (u + 1))) fun (x : Shrink.{u, u + 1} (↑s : Type (u + 1))) ↦
        Quotient.out (s := PSet.setoid)
          (↑((Equiv.symm (equivShrink (↑s : Type (u + 1))) :
                  (a : Shrink.{u, u + 1} (↑s : Type (u + 1))) → (↑s : Type (u + 1)))
                x) :
            ZFSet.{u})) ↔
    x ∈ s
⊢ x ∈
      (↑(mk
            (PSet.mk (Shrink.{u, u + 1} (↑s : Type (u + 1))) fun (x : Shrink.{u, u + 1} (↑s : Type (u + 1))) ↦
              Quotient.out (s := PSet.setoid)
                (↑((Equiv.symm (equivShrink (↑s : Type (u + 1))) :
                        (a : Shrink.{u, u + 1} (↑s : Type (u + 1))) → (↑s : Type (u + 1)))
                      x) :
                  ZFSet.{u}))) :
        Set ZFSet.{u}) ↔
    x ∈ s

Tactic:
rw [SetLike.mem_coe, ← mk_out x, mk_mem_iff, mk_out]

Premises used: ZFSet.mk_out, ZFSet.mk_mem_iff, SetLike.mem_coe
-- Module: Mathlib.SetTheory.ZFC.Class
Goal:
s : Set ZFSet.{u}
hs : Small.{u, u + 1} (↑s : Type (u + 1))
x : ZFSet.{u}
⊢ (Quotient.out x ∈
      PSet.mk (Shrink.{u, u + 1} (↑s : Type (u + 1))) fun (x : Shrink.{u, u + 1} (↑s : Type (u + 1))) ↦
        Quotient.out (s := PSet.setoid)
          (↑((Equiv.symm (equivShrink (↑s : Type (u + 1))) :
                  (a : Shrink.{u, u + 1} (↑s : Type (u + 1))) → (↑s : Type (u + 1)))
                x) :
            ZFSet.{u})) ↔
    x ∈ s

Tactic:
⟨?_, fun xs ↦ ⟨equivShrink s (Subtype.mk x xs), ?_⟩⟩

Premises used: Set.Elem, Subtype.mk, Iff.intro, Exists.intro, equivShrink, DFunLike.coe
-- Module: Mathlib.SetTheory.ZFC.Class
Goal:
s : Set ZFSet.{u}
hs : Small.{u, u + 1} (↑s : Type (u + 1))
x : ZFSet.{u}
h :
  (Quotient.out x ∈
      PSet.mk (Shrink.{u, u + 1} (↑s : Type (u + 1))) fun (x : Shrink.{u, u + 1} (↑s : Type (u + 1))) ↦
        Quotient.out (s := PSet.setoid)
          (↑((Equiv.symm (equivShrink (↑s : Type (u + 1))) :
                  (a : Shrink.{u, u + 1} (↑s : Type (u + 1))) → (↑s : Type (u + 1)))
                x) :
            ZFSet.{u})) →
    x ∈ s
h₁ :
  ∀ (xs : x ∈ s),
    PSet.Equiv.{u, u} (Quotient.out x)
      ((PSet.mk (Shrink.{u, u + 1} (↑s : Type (u + 1))) fun (x : Shrink.{u, u + 1} (↑s : Type (u + 1))) ↦
            Quotient.out (s := PSet.setoid)
              (↑((Equiv.symm (equivShrink (↑s : Type (u + 1))) :
                      (a : Shrink.{u, u + 1} (↑s : Type (u + 1))) → (↑s : Type (u + 1)))
                    x) :
                ZFSet.{u})).Func
        ((equivShrink (↑s : Type (u + 1)) : (a : (↑s : Type (u + 1))) → Shrink.{u, u + 1} (↑s : Type (u + 1)))
          (Subtype.mk (p := fun (x : ZFSet.{u}) ↦ x ∈ s) x xs)))
⊢ (Quotient.out x ∈
      PSet.mk (Shrink.{u, u + 1} (↑s : Type (u + 1))) fun (x : Shrink.{u, u + 1} (↑s : Type (u + 1))) ↦
        Quotient.out (s := PSet.setoid)
          (↑((Equiv.symm (equivShrink (↑s : Type (u + 1))) :
                  (a : Shrink.{u, u + 1} (↑s : Type (u + 1))) → (↑s : Type (u + 1)))
                x) :
            ZFSet.{u})) ↔
    x ∈ s

Tactic:
refine ⟨?_, fun xs ↦ ⟨equivShrink s (Subtype.mk x xs), ?_⟩⟩
-- Module: Mathlib.SetTheory.ZFC.Class
Goal:
s : Set ZFSet.{u}
hs : Small.{u, u + 1} (↑s : Type (u + 1))
x : ZFSet.{u}
b :
  (PSet.mk (Shrink.{u, u + 1} (↑s : Type (u + 1))) fun (x : Shrink.{u, u + 1} (↑s : Type (u + 1))) ↦
      Quotient.out (s := PSet.setoid)
        (↑((Equiv.symm (equivShrink (↑s : Type (u + 1))) :
                (a : Shrink.{u, u + 1} (↑s : Type (u + 1))) → (↑s : Type (u + 1)))
              x) :
          ZFSet.{u})).Type
h2 :
  PSet.Equiv.{u, u} (Quotient.out x)
    ((PSet.mk (Shrink.{u, u + 1} (↑s : Type (u + 1))) fun (x : Shrink.{u, u + 1} (↑s : Type (u + 1))) ↦
          Quotient.out (s := PSet.setoid)
            (↑((Equiv.symm (equivShrink (↑s : Type (u + 1))) :
                    (a : Shrink.{u, u + 1} (↑s : Type (u + 1))) → (↑s : Type (u + 1)))
                  x) :
              ZFSet.{u})).Func
      b)
⊢ x =
    mk
      ((PSet.mk (Shrink.{u, u + 1} (↑s : Type (u + 1))) fun (x : Shrink.{u, u + 1} (↑s : Type (u + 1))) ↦
            Quotient.out (s := PSet.setoid)
              (↑((Equiv.symm (equivShrink (↑s : Type (u + 1))) :
                      (a : Shrink.{u, u + 1} (↑s : Type (u + 1))) → (↑s : Type (u + 1)))
                    x) :
                ZFSet.{u})).Func
        b)

Tactic:
rw [← ZFSet.eq, ZFSet.mk_out] at h2

Premises used: ZFSet.mk_out, ZFSet.eq
-- Module: Mathlib.SetTheory.ZFC.Class
Goal:
s : Set ZFSet.{u}
hs : Small.{u, u + 1} (↑s : Type (u + 1))
x : ZFSet.{u}
b :
  (PSet.mk (Shrink.{u, u + 1} (↑s : Type (u + 1))) fun (x : Shrink.{u, u + 1} (↑s : Type (u + 1))) ↦
      Quotient.out (s := PSet.setoid)
        (↑((Equiv.symm (equivShrink (↑s : Type (u + 1))) :
                (a : Shrink.{u, u + 1} (↑s : Type (u + 1))) → (↑s : Type (u + 1)))
              x) :
          ZFSet.{u})).Type
h2 :
  x =
    mk
      ((PSet.mk (Shrink.{u, u + 1} (↑s : Type (u + 1))) fun (x : Shrink.{u, u + 1} (↑s : Type (u + 1))) ↦
            Quotient.out (s := PSet.setoid)
              (↑((Equiv.symm (equivShrink (↑s : Type (u + 1))) :
                      (a : Shrink.{u, u + 1} (↑s : Type (u + 1))) → (↑s : Type (u + 1)))
                    x) :
                ZFSet.{u})).Func
        b)
⊢ x ∈ s

Tactic:
simp [h2]
-- Module: Mathlib.SetTheory.ZFC.Class
Goal:
s : Set ZFSet.{u}
hs : Small.{u, u + 1} (↑s : Type (u + 1))
x : ZFSet.{u}
xs : x ∈ s
⊢ PSet.Equiv.{u, u} (Quotient.out x)
    ((PSet.mk (Shrink.{u, u + 1} (↑s : Type (u + 1))) fun (x : Shrink.{u, u + 1} (↑s : Type (u + 1))) ↦
          Quotient.out (s := PSet.setoid)
            (↑((Equiv.symm (equivShrink (↑s : Type (u + 1))) :
                    (a : Shrink.{u, u + 1} (↑s : Type (u + 1))) → (↑s : Type (u + 1)))
                  x) :
              ZFSet.{u})).Func
      ((equivShrink (↑s : Type (u + 1)) : (a : (↑s : Type (u + 1))) → Shrink.{u, u + 1} (↑s : Type (u + 1)))
        (Subtype.mk (p := fun (x : ZFSet.{u}) ↦ x ∈ s) x xs)))

Tactic:
simp [PSet.Equiv.refl]

Premises used: PSet.Equiv.refl
-- Module: Mathlib.SetTheory.ZFC.Class
Goal:
x a₁ : ZFSet.{u}
_ :
  ∀ ⦃a₂ : ZFSet.{u}⦄,
    Eq.{u + 2} (α := { s : Set ZFSet.{u} // Small.{u, u + 1} (↑s : Type (u + 1)) })
        ((fun (x : ZFSet.{u}) ↦
            (Subtype.mk (p := fun (s : Set ZFSet.{u}) ↦ Small.{u, u + 1} (↑s : Type (u + 1))) (↑x : Set ZFSet.{u}) ⋯ :
              { s : Set ZFSet.{u} // Small.{u, u + 1} (↑s : Type (u + 1)) }))
          a₁)
        ((fun (x : ZFSet.{u}) ↦
            (Subtype.mk (p := fun (s : Set ZFSet.{u}) ↦ Small.{u, u + 1} (↑s : Type (u + 1))) (↑x : Set ZFSet.{u}) ⋯ :
              { s : Set ZFSet.{u} // Small.{u, u + 1} (↑s : Type (u + 1)) }))
          a₂) →
      a₁ = a₂
⊢ ∀ ⦃a₂ : ZFSet.{u}⦄,
    Eq.{u + 2} (α := { s : Set ZFSet.{u} // Small.{u, u + 1} (↑s : Type (u + 1)) })
        ((fun (x : ZFSet.{u}) ↦
            (Subtype.mk (p := fun (s : Set ZFSet.{u}) ↦ Small.{u, u + 1} (↑s : Type (u + 1))) (↑x : Set ZFSet.{u}) ⋯ :
              { s : Set ZFSet.{u} // Small.{u, u + 1} (↑s : Type (u + 1)) }))
          a₁)
        ((fun (x : ZFSet.{u}) ↦
            (Subtype.mk (p := fun (s : Set ZFSet.{u}) ↦ Small.{u, u + 1} (↑s : Type (u + 1))) (↑x : Set ZFSet.{u}) ⋯ :
              { s : Set ZFSet.{u} // Small.{u, u + 1} (↑s : Type (u + 1)) }))
          a₂) →
      a₁ = a₂

Tactic:
_
-- Module: Mathlib.SetTheory.ZFC.Class
Goal:
x a₁ a₂ : ZFSet.{u}
⊢ Eq.{u + 2} (α := { s : Set ZFSet.{u} // Small.{u, u + 1} (↑s : Type (u + 1)) })
      ((fun (x : ZFSet.{u}) ↦
          (Subtype.mk (p := fun (s : Set ZFSet.{u}) ↦ Small.{u, u + 1} (↑s : Type (u + 1))) (↑x : Set ZFSet.{u}) ⋯ :
            { s : Set ZFSet.{u} // Small.{u, u + 1} (↑s : Type (u + 1)) }))
        a₁)
      ((fun (x : ZFSet.{u}) ↦
          (Subtype.mk (p := fun (s : Set ZFSet.{u}) ↦ Small.{u, u + 1} (↑s : Type (u + 1))) (↑x : Set ZFSet.{u}) ⋯ :
            { s : Set ZFSet.{u} // Small.{u, u + 1} (↑s : Type (u + 1)) }))
        a₂) →
    a₁ = a₂

Tactic:
simp
-- Module: Mathlib.SetTheory.ZFC.Class
Goal:
x : ZFSet.{u}
hx : (↑x : Class.{u}) = IsOrdinal
this : x.IsOrdinal
apply : (↑x : Class.{u}) ∈ (↑x : Class.{u})
⊢ False

Tactic:
apply Class.mem_irrefl x

Premises used: Class.ofSet, Class.mem_irrefl
-- Module: Mathlib.SetTheory.ZFC.Class
Goal:
x : ZFSet.{u}
hx : (↑x : Class.{u}) = IsOrdinal
this : x.IsOrdinal
rwa : (↑x : Class.{u}) x
rwa₁ rwa₂ rwa₃ rwa₄ : x.IsOrdinal
⊢ (↑x : Class.{u}) ∈ (↑x : Class.{u})

Tactic:
rwa [Class.coe_mem, hx]

Premises used: Class.coe_mem
-- Module: Mathlib.SetTheory.ZFC.Class
Goal:
x : ZFSet.{u}
hx : (↑x : Class.{u}) = IsOrdinal
suffices : x.IsOrdinal
⊢ False

Tactic:
suffices IsOrdinal x by
    apply Class.mem_irrefl x
    rwa [Class.coe_mem, hx]
-- Module: Mathlib.SetTheory.ZFC.Class
Goal:
x : ZFSet.{u}
hx : (↑x : Class.{u}) = IsOrdinal
⊢ x.IsOrdinal

Tactic:
⟨fun y hy z hz ↦ ?_, fun hyz hzw hwx ↦ ?_⟩

Premises used: ZFSet.IsOrdinal.mk
-- Module: Mathlib.SetTheory.ZFC.Class
Goal:
x : ZFSet.{u}
hx : (↑x : Class.{u}) = IsOrdinal
refine_1 : ∀ (y : ZFSet.{u}) (hy : y ∈ x) (z : ZFSet.{u}) (hz : z ∈ y), z ∈ x
refine_2 : ∀ {y z w : ZFSet.{u}} (hyz : y ∈ z) (hzw : z ∈ w) (hwx : w ∈ x), y ∈ w
⊢ x.IsOrdinal

Tactic:
refine ⟨fun y hy z hz ↦ ?_, fun hyz hzw hwx ↦ ?_⟩
-- Module: Mathlib.SetTheory.ZFC.Class
Goal:
x : ZFSet.{u}
hx : (↑x : Class.{u}) = IsOrdinal
y : ZFSet.{u}
hy : y ∈ x
z : ZFSet.{u}
hz : z ∈ y
refine_1 :
  ∀ (hx : IsOrdinal = IsOrdinal) (y : ZFSet.{u}) (hy : y.IsOrdinal) (z : ZFSet.{u}) (hz : (↑y : Class.{u}) z),
    z.IsOrdinal
⊢ z ∈ x

Tactic:
rw [← Class.coe_apply, hx] at *

Premises used: Class.coe_apply
-- Module: Mathlib.SetTheory.ZFC.Class
Goal:
x : ZFSet.{u}
hx : (↑x : Class.{u}) = IsOrdinal
y z w : ZFSet.{u}
hyz : y ∈ z
hzw : z ∈ w
hwx : w ∈ x
refine_2 :
  ∀ (hx : IsOrdinal = IsOrdinal) {y z w : ZFSet.{u}} (hyz : (↑z : Class.{u}) y) (hzw : (↑w : Class.{u}) z)
    (hwx : w.IsOrdinal), (↑w : Class.{u}) y
⊢ y ∈ w

Tactic:
rw [← Class.coe_apply, hx] at *

Premises used: Class.coe_apply
-- Module: Mathlib.SetTheory.ZFC.Class
Goal:
x : ZFSet.{u}
hx : IsOrdinal = IsOrdinal
y : ZFSet.{u}
hy : y.IsOrdinal
z : ZFSet.{u}
hz : (↑y : Class.{u}) z
⊢ z.IsOrdinal

Tactic:
hy.mem hz

Premises used: ZFSet.IsOrdinal.mem