awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
x_1 y_1 z_1 x y : ZFSet.{u}
hxy : x.toSet = y.toSet
z : ZFSet.{u}
⊢ z ∈ x.toSet ↔ z ∈ y.toSet

Tactic:
congr(z ∈ $hxy)

Premises used: congrArg, Membership.mem, id, iff_of_eq
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
x_1 y_1 z_1 x y : ZFSet.{u}
hxy : x.toSet = y.toSet
z : ZFSet.{u}
⊢ z ∈ x.toSet ↔ z ∈ y.toSet

Tactic:
exact congr(z ∈ $hxy)
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
x y : PSet.{u_1}
⊢ mk x ∈ mk y ↔ x ∈ y

Tactic:
Iff.rfl

Premises used: PSet.Mem, Set.Mem, Iff.rfl, setOf, ZFSet.toSet
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
x y : ZFSet.{u}
⊢ (∀ (z : ZFSet.{u}), z ∈ x ↔ z ∈ y) → x = y

Tactic:
ext_aux

Premises used: Set.Mem, _private.0.ZFSet.ext_aux
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
x_1 y z x : ZFSet.{u}
a : PSet.{u}
f : (i : a.Type) → ↥(mk a) := fun (i : a.Type) ↦ Subtype.mk (p := fun (x : ZFSet.{u}) ↦ x ∈ mk a) (mk (a.Func i)) ⋯
this : Function.Surjective f
⊢ Small.{u, u + 1} ↥(⟦a⟧)

Tactic:
small_of_surjective this

Premises used: small_of_surjective
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
x_1 y z x : ZFSet.{u}
a : PSet.{u}
f : (i : a.Type) → ↥(mk a) := fun (i : a.Type) ↦ Subtype.mk (p := fun (x : ZFSet.{u}) ↦ x ∈ mk a) (mk (a.Func i)) ⋯
this : Function.Surjective f
⊢ Small.{u, u + 1} ↥(⟦a⟧)

Tactic:
exact small_of_surjective this

Premises used: small_of_surjective
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
x_1 y z x : ZFSet.{u}
a : PSet.{u}
f : (i : a.Type) → ↥(mk a) := fun (i : a.Type) ↦ Subtype.mk (p := fun (x : ZFSet.{u}) ↦ x ∈ mk a) (mk (a.Func i)) ⋯
suffices : Function.Surjective f
⊢ Small.{u, u + 1} ↥(⟦a⟧)

Tactic:
suffices Function.Surjective f by exact small_of_surjective this
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
x_1 y_1 z x : ZFSet.{u}
a : PSet.{u}
f : (i : a.Type) → ↥(mk a) := fun (i : a.Type) ↦ Subtype.mk (p := fun (x : ZFSet.{u}) ↦ x ∈ mk a) (mk (a.Func i)) ⋯
y : ZFSet.{u}
hb : y ∈ mk a
h :
  ∀ (a_1 : PSet.{u}) (hb : ⟦a_1⟧ ∈ mk a),
    ∃ (a_2 : a.Type), f a_2 = Subtype.mk (p := fun (x : ZFSet.{u}) ↦ x ∈ mk a) ⟦a_1⟧ hb
⊢ ∃ (a_1 : a.Type), f a_1 = Subtype.mk (p := fun (x : ZFSet.{u}) ↦ x ∈ mk a) y hb

Tactic:
induction y using Quotient.inductionOn
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
x_1 y z x : ZFSet.{u}
a : PSet.{u}
f : (i : a.Type) → ↥(mk a) := fun (i : a.Type) ↦ Subtype.mk (p := fun (x : ZFSet.{u}) ↦ x ∈ mk a) (mk (a.Func i)) ⋯
a_1 : PSet.{u}
hb : ⟦a_1⟧ ∈ mk a
h :
  ∀ (i : a.Type) (h : a_1.Equiv (a.Func i)),
    ∃ (a_2 : a.Type), f a_2 = Subtype.mk (p := fun (x : ZFSet.{u}) ↦ x ∈ mk a) ⟦a_1⟧ ⋯
⊢ ∃ (a_2 : a.Type), f a_2 = Subtype.mk (p := fun (x : ZFSet.{u}) ↦ x ∈ mk a) ⟦a_1⟧ hb

Tactic:
obtain ⟨i, h⟩ := hb
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
x_1 y z x : ZFSet.{u}
a : PSet.{u}
f : (i : a.Type) → ↥(mk a) := fun (i : a.Type) ↦ Subtype.mk (p := fun (x : ZFSet.{u}) ↦ x ∈ mk a) (mk (a.Func i)) ⋯
a_1 : PSet.{u}
i : a.Type
h : a_1.Equiv (a.Func i)
⊢ ∃ (a_2 : a.Type), f a_2 = Subtype.mk (p := fun (x : ZFSet.{u}) ↦ x ∈ mk a) ⟦a_1⟧ ⋯

Tactic:
⟨i, Subtype.coe_injective (Quotient.sound h.symm)⟩

Premises used: Subtype.coe_injective, PSet.Equiv.symm, Exists.intro, Quotient.sound
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
x_1 y z x : ZFSet.{u}
a : PSet.{u}
f : (i : a.Type) → ↥(mk a) := fun (i : a.Type) ↦ Subtype.mk (p := fun (x : ZFSet.{u}) ↦ x ∈ mk a) (mk (a.Func i)) ⋯
a_1 : PSet.{u}
i : a.Type
h : a_1.Equiv (a.Func i)
⊢ ∃ (a_2 : a.Type), f a_2 = Subtype.mk (p := fun (x : ZFSet.{u}) ↦ x ∈ mk a) ⟦a_1⟧ ⋯

Tactic:
exact ⟨i, Subtype.coe_injective (Quotient.sound h.symm)⟩
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
u : ZFSet.{u_1}
⊢ u.Nonempty ↔ ∃ (x : ZFSet.{u_1}), x ∈ u

Tactic:
Iff.rfl

Premises used: Iff.rfl, Set.Nonempty, ZFSet.Nonempty
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
x u : ZFSet.{u_1}
h : x ∈ u
⊢ u.Nonempty

Tactic:
⟨x, h⟩

Premises used: Set.Nonempty, Exists.intro, ZFSet.Nonempty
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
x : ZFSet.{u}
⊢ (↑x : Set ZFSet.{u}).Nonempty ↔ x.Nonempty

Tactic:
.rfl

Premises used: Iff.rfl, ZFSet.Nonempty
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
x y : ZFSet.{u}
⊢ x ≤ y ↔ x ⊆ y

Tactic:
.rfl

Premises used: Iff.rfl, ZFSet.Subset
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
x y : ZFSet.{u}
⊢ x < y ↔ x ⊂ y

Tactic:
.rfl

Premises used: Iff.rfl
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
x y : ZFSet.{u}
⊢ x ⊆ y ↔ ∀ ⦃z : ZFSet.{u}⦄, z ∈ x → z ∈ y

Tactic:
Iff.rfl

Premises used: Iff.rfl, ZFSet.Subset
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
x y z : ZFSet.{u}
⊢ Std.Refl fun (x1 x2 : ZFSet.{u_1}) ↦ x1 ⊆ x2

Tactic:
⟨fun _ _ => id⟩

Premises used: Std.Refl.mk, id
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
x y z : ZFSet.{u}
⊢ IsTrans ZFSet.{u_1} fun (x1 x2 : ZFSet.{u_1}) ↦ x1 ⊆ x2

Tactic:
⟨fun _ _ _ hxy hyz _ ha => hyz (hxy ha)⟩

Premises used: IsTrans.mk
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
x y : ZFSet.{u}
⊢ (↑x : Set ZFSet.{u}) ⊆ (↑y : Set ZFSet.{u}) ↔ x ⊆ y

Tactic:
simp
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
x y z : ZFSet.{u}
⊢ Std.Antisymm fun (x1 x2 : ZFSet.{u_1}) ↦ x1 ⊆ x2

Tactic:
⟨@le_antisymm ZFSet _⟩

Premises used: le_antisymm, Std.Antisymm.mk
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
x y z : ZFSet.{u}
⊢ IsNonstrictStrictOrder ZFSet.{u_1} (fun (x1 x2 : ZFSet.{u_1}) ↦ x1 ⊆ x2) fun (x1 x2 : ZFSet.{u_1}) ↦ x1 ⊂ x2

Tactic:
⟨fun _ _ ↦ Iff.rfl⟩

Premises used: Iff.rfl, IsNonstrictStrictOrder.mk
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
x : ZFSet.{u}
⊢ x ∉ ∅

Tactic:
Quotient.inductionOn x PSet.notMem_empty

Premises used: Quotient.inductionOn
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
h : ∀ (x : ZFSet.{u}), x ∈ (↑∅ : Set ZFSet.{u}) ↔ Membership.mem (γ := Set ZFSet.{u}) ∅ x
⊢ (↑∅ : Set ZFSet.{u}) = ∅

Tactic:
ext
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
x : ZFSet.{u}
⊢ x ∈ (↑∅ : Set ZFSet.{u}) ↔ Membership.mem (γ := Set ZFSet.{u}) ∅ x

Tactic:
simp
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
x : ZFSet.{u}
⊢ ∅ ⊆ x

Tactic:
Quotient.inductionOn x fun y => subset_iff.2 <| PSet.empty_subset y

Premises used: Quotient.inductionOn
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
⊢ ¬ZFSet.Nonempty.{u_1} ∅

Tactic:
simp [ZFSet.Nonempty]

Premises used: ZFSet.Nonempty
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
x : PSet.{u_1}
⊢ ZFSet.Nonempty.{u_1} (mk x) ↔ x.Nonempty

Tactic:
⟨?_, fun ⟨a, h⟩ => ⟨mk a, h⟩⟩

Premises used: ZFSet.mk, Iff.intro, Exists.intro, _private.0.ZFSet.nonempty_mk_iff.match_1, ZFSet.Nonempty
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
x : PSet.{u_1}
refine : ZFSet.Nonempty.{u_1} (mk x) → x.Nonempty
⊢ ZFSet.Nonempty.{u_1} (mk x) ↔ x.Nonempty

Tactic:
refine ⟨?_, fun ⟨a, h⟩ => ⟨mk a, h⟩⟩
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
x : PSet.{u_1}
a : ZFSet.{u_1}
h : a ∈ (↑(mk x) : Set ZFSet.{u_1})
h₁ : ∀ (a : PSet.{u_1}) (h : ⟦a⟧ ∈ (↑(mk x) : Set ZFSet.{u_1})), x.Nonempty
⊢ x.Nonempty

Tactic:
induction a using Quotient.inductionOn
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
x a : PSet.{u_1}
h : ⟦a⟧ ∈ (↑(mk x) : Set ZFSet.{u_1})
⊢ x.Nonempty

Tactic:
⟨_, h⟩

Premises used: PSet.Nonempty, Set.Nonempty, Exists.intro
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
x a : PSet.{u_1}
h : ⟦a⟧ ∈ (↑(mk x) : Set ZFSet.{u_1})
⊢ x.Nonempty

Tactic:
exact ⟨_, h⟩
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
x : ZFSet.{u}
⊢ x = ∅ ↔ ∀ (y : ZFSet.{u}), y ∉ x

Tactic:
simp [ZFSet.ext_iff]

Premises used: ZFSet.ext_iff
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
u : ZFSet.{u_1}
rw : (¬∃ (x : ZFSet.{u_1}), x ∈ u) ∨ u.Nonempty
⊢ u = ∅ ∨ u.Nonempty

Tactic:
rw [eq_empty, ← not_exists]

Premises used: ZFSet.eq_empty, not_exists
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
u : ZFSet.{u_1}
⊢ (¬∃ (x : ZFSet.{u_1}), x ∈ u) ∨ u.Nonempty

Tactic:
apply em'

Premises used: em'
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
x y z : ZFSet.{u}
⊢ LawfulSingleton ZFSet.{u_1} ZFSet.{u_1}

Tactic:
⟨fun _ => rfl⟩

Premises used: LawfulSingleton.mk, rfl
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
x y z : ZFSet.{u}
⊢ x ∈ insert y z ↔ x = y ∨ x ∈ z

Tactic:
Quotient.inductionOn₃ x y z fun _ _ _ => PSet.mem_insert_iff.trans (or_congr_left eq.symm)

Premises used: Quotient.inductionOn₃
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
x y : ZFSet.{u_1}
⊢ x ∈ insert x y

Tactic:
mem_insert_iff.2 <| Or.inl rfl

Premises used: Iff.mpr, ZFSet.mem_insert_iff, Or.inl, rfl
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
y z x : ZFSet.{u_1}
h : z ∈ y
⊢ z ∈ insert x y

Tactic:
mem_insert_iff.2 <| Or.inr h

Premises used: Iff.mpr, ZFSet.mem_insert_iff, Or.inr
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
x y : ZFSet.{u_1}
h : ∀ (x_1 : ZFSet.{u_1}), x_1 ∈ (↑(insert x y) : Set ZFSet.{u_1}) ↔ x_1 ∈ insert x (↑y : Set ZFSet.{u_1})
⊢ (↑(insert x y) : Set ZFSet.{u_1}) = insert x (↑y : Set ZFSet.{u_1})

Tactic:
ext
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
x y x_1 : ZFSet.{u_1}
⊢ x_1 ∈ (↑(insert x y) : Set ZFSet.{u_1}) ↔ x_1 ∈ insert x (↑y : Set ZFSet.{u_1})

Tactic:
simp
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
x y : ZFSet.{u}
⊢ Membership.mem (γ := ZFSet.{u}) {y} x ↔ x = y

Tactic:
Quotient.inductionOn₂ x y fun _ _ => PSet.mem_singleton.trans eq.symm

Premises used: Quotient.inductionOn₂
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
x y : ZFSet.{u}
⊢ x ∉ {y} ↔ x ≠ y

Tactic:
mem_singleton.not

Premises used: Iff.not, ZFSet.mem_singleton
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
x : ZFSet.{u_1}
h : ∀ (x_1 : ZFSet.{u_1}), x_1 ∈ (↑{x} : Set ZFSet.{u_1}) ↔ Membership.mem (γ := Set ZFSet.{u_1}) {x} x_1
⊢ (↑{x} : Set ZFSet.{u_1}) = {x}

Tactic:
ext
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
x x_1 : ZFSet.{u_1}
⊢ x_1 ∈ (↑{x} : Set ZFSet.{u_1}) ↔ Membership.mem (γ := Set ZFSet.{u_1}) {x} x_1

Tactic:
simp
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
u v : ZFSet.{u_1}
⊢ ZFSet.Nonempty.{u_1} (insert u v)

Tactic:
⟨u, mem_insert u v⟩

Premises used: Set.Nonempty, Exists.intro, ZFSet.Nonempty, ZFSet.mem_insert
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
u : ZFSet.{u_1}
⊢ ZFSet.Nonempty.{u_1} {u}

Tactic:
insert_nonempty u ∅

Premises used: ZFSet.insert_nonempty, EmptyCollection.emptyCollection
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
x y z : ZFSet.{u}
⊢ Membership.mem (γ := ZFSet.{u}) {y, z} x ↔ x = y ∨ x = z

Tactic:
simp
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
x : ZFSet.{u_1}
a : ∀ (z : ZFSet.{u_1}), Membership.mem (γ := ZFSet.{u_1}) {x, x} z ↔ Membership.mem (γ := ZFSet.{u_1}) {x} z
⊢ Eq (α := ZFSet.{u_1}) {x, x} {x}

Tactic:
ext
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
x z : ZFSet.{u_1}
⊢ Membership.mem (γ := ZFSet.{u_1}) {x, x} z ↔ Membership.mem (γ := ZFSet.{u_1}) {x} z

Tactic:
simp
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
x y z : ZFSet.{u_1}
⊢ Eq (α := ZFSet.{u_1}) {x, y} {z} ↔ x = z ∧ y = z

Tactic:
⟨fun h ↦ ?_, ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
x y z : ZFSet.{u_1}
refine_1 : ∀ (h : Eq (α := ZFSet.{u_1}) {x, y} {z}), x = z ∧ y = z
refine_2 : x = z ∧ y = z → Eq (α := ZFSet.{u_1}) {x, y} {z}
⊢ Eq (α := ZFSet.{u_1}) {x, y} {z} ↔ x = z ∧ y = z

Tactic:
refine ⟨fun h ↦ ?_, ?_⟩
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
x y z : ZFSet.{u_1}
h : Eq (α := ZFSet.{u_1}) {x, y} {z}
refine_1 : Membership.mem (γ := ZFSet.{u_1}) {z} x ∧ Membership.mem (γ := ZFSet.{u_1}) {z} y
⊢ x = z ∧ y = z

Tactic:
rw [← mem_singleton, ← mem_singleton]

Premises used: ZFSet.mem_singleton
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
x y z : ZFSet.{u_1}
h : Eq (α := ZFSet.{u_1}) {x, y} {z}
⊢ Membership.mem (γ := ZFSet.{u_1}) {z} x ∧ Membership.mem (γ := ZFSet.{u_1}) {z} y

Tactic:
simp [← h]
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
y : ZFSet.{u_1}
⊢ Eq (α := ZFSet.{u_1}) {y, y} {y}

Tactic:
pair_eq_singleton y

Premises used: ZFSet.pair_eq_singleton
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
y : ZFSet.{u_1}
⊢ Eq (α := ZFSet.{u_1}) {y, y} {y}

Tactic:
exact pair_eq_singleton y

Premises used: ZFSet.pair_eq_singleton
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
x y z : ZFSet.{u_1}
rw : y = x ∧ z = x ↔ x = y ∧ x = z
⊢ Eq (α := ZFSet.{u_1}) {x} {y, z} ↔ x = y ∧ x = z

Tactic:
rw [eq_comm, pair_eq_singleton_iff]

Premises used: ZFSet.pair_eq_singleton_iff, eq_comm
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
x y z : ZFSet.{u_1}
⊢ y = x ∧ z = x ↔ x = y ∧ x = z

Tactic:
simp_rw [eq_comm]

Premises used: eq_comm
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
⊢ ∅ ∈ omega

Tactic:
⟨⟨0⟩, Equiv.rfl⟩

Premises used: PSet.Mem, Set.Mem, setOf, PSet.Equiv.rfl, ZFSet.toSet, Exists.intro, OfNat.ofNat, ULift.up
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
n_1 : ZFSet.{u}
x : PSet.{u}
h_1 : ⟦x⟧ ∈ omega
n : ℕ
h : x.Equiv (PSet.omega.Func { down := n : ULift.{u, 0} ℕ })
rw :
  insert (mk (PSet.omega.Func { down := n : ULift.{u, 0} ℕ })) (mk (PSet.omega.Func { down := n : ULift.{u, 0} ℕ })) =
    insert (mk (ofNat n)) (mk (ofNat n))
⊢ insert (mk x) (mk x) = insert (mk (ofNat n)) (mk (ofNat n))

Tactic:
rw [ZFSet.sound h]

Premises used: ZFSet.sound
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
n_1 : ZFSet.{u}
x : PSet.{u}
h_1 : ⟦x⟧ ∈ omega
n : ℕ
h : x.Equiv (PSet.omega.Func { down := n : ULift.{u, 0} ℕ })
⊢ insert (mk (PSet.omega.Func { down := n : ULift.{u, 0} ℕ })) (mk (PSet.omega.Func { down := n : ULift.{u, 0} ℕ })) =
    insert (mk (ofNat n)) (mk (ofNat n))

Tactic:
rfl
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
x y z : ZFSet.{u}
p : ZFSet.{u_1} → Prop
x_1 x_2 : PSet.{u_1}
α : Type u_1
A : α → PSet.{u_1}
β : Type u_1
B : β → PSet.{u_1}
h : PSet.mk α A ≈ PSet.mk β B
αβ : ∀ (a : α), ∃ (b : β), PSet.Equiv.{u_1, u_1} (A a) (B b)
βα : ∀ (b : β), ∃ (a : α), PSet.Equiv.{u_1, u_1} (A a) (B b)
x_3 : { a : (PSet.mk α A).Type // (fun (y : PSet.{u_1}) ↦ p (mk y)) ((PSet.mk α A).Func a) }
a : (PSet.mk α A).Type
pa : (fun (y : PSet.{u_1}) ↦ p (mk y)) ((PSet.mk α A).Func a)
b : β
hb : PSet.Equiv.{u_1, u_1} (A a) (B b)
⊢ (fun (y : PSet.{u_1}) ↦ p (mk y)) ((PSet.mk β B).Func b)

Tactic:
simpa only [mk_func, ← ZFSet.sound hb]

Premises used: ZFSet.sound, PSet.mk_func
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
x y z : ZFSet.{u}
p : ZFSet.{u_1} → Prop
x_1 x_2 : PSet.{u_1}
α : Type u_1
A : α → PSet.{u_1}
β : Type u_1
B : β → PSet.{u_1}
h : PSet.mk α A ≈ PSet.mk β B
αβ : ∀ (a : α), ∃ (b : β), PSet.Equiv.{u_1, u_1} (A a) (B b)
βα : ∀ (b : β), ∃ (a : α), PSet.Equiv.{u_1, u_1} (A a) (B b)
x_3 : { a : (PSet.mk β B).Type // (fun (y : PSet.{u_1}) ↦ p (mk y)) ((PSet.mk β B).Func a) }
b : (PSet.mk β B).Type
pb : (fun (y : PSet.{u_1}) ↦ p (mk y)) ((PSet.mk β B).Func b)
a : α
ha : PSet.Equiv.{u_1, u_1} (A a) (B b)
⊢ (fun (y : PSet.{u_1}) ↦ p (mk y)) ((PSet.mk α A).Func a)

Tactic:
simpa only [mk_func, ZFSet.sound ha]

Premises used: ZFSet.sound, PSet.mk_func
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
p : ZFSet.{u} → Prop
x y : ZFSet.{u}
⊢ y ∈ ZFSet.sep p x ↔ y ∈ x ∧ p y

Tactic:
Quotient.inductionOn₂ x y fun _ _ =>
    PSet.mem_sep (p := p ∘ mk) fun _ _ h => (Quotient.sound h).subst

Premises used: Quotient.inductionOn₂
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
p : ZFSet.{u_1} → Prop
⊢ ZFSet.sep p ∅ = ∅

Tactic:
(eq_empty _).mpr fun _ h ↦ notMem_empty _ (mem_sep.mp h).1

Premises used: Iff.mpr, ZFSet.mem_sep, ZFSet.notMem_empty, ZFSet.eq_empty, And.left, Iff.mp
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
x : ZFSet.{u_1}
p : ZFSet.{u_1} → Prop
⊢ ZFSet.sep p x ⊆ x

Tactic:
fun _ h => (mem_sep.1 h).1

Premises used: ZFSet.mem_sep, And.left, Iff.mp, ZFSet.Subset
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
a : ZFSet.{u_1}
p : ZFSet.{u_1} → Prop
h :
  ∀ (x : ZFSet.{u_1}),
    x ∈ (↑(ZFSet.sep p a) : Set ZFSet.{u_1}) ↔ Membership.mem (γ := Set ZFSet.{u_1}) {x : ZFSet.{u_1} | x ∈ a ∧ p x} x
⊢ (↑(ZFSet.sep p a) : Set ZFSet.{u_1}) = {x : ZFSet.{u_1} | x ∈ a ∧ p x}

Tactic:
ext
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
a : ZFSet.{u_1}
p : ZFSet.{u_1} → Prop
x : ZFSet.{u_1}
⊢ x ∈ (↑(ZFSet.sep p a) : Set ZFSet.{u_1}) ↔ Membership.mem (γ := Set ZFSet.{u_1}) {x : ZFSet.{u_1} | x ∈ a ∧ p x} x

Tactic:
simp
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
x y : ZFSet.{u}
⊢ y ∈ x.powerset ↔ y ⊆ x

Tactic:
Quotient.inductionOn₂ x y fun _ _ => PSet.mem_powerset.trans subset_iff.symm

Premises used: Quotient.inductionOn₂
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
α β : Type u
A : α → PSet.{u}
B : β → PSet.{u}
αβ : ∀ (a : α), ∃ (b : β), PSet.Equiv.{u, u} (A a) (B b)
a : (PSet.mk α A).Type
c : ((PSet.mk α A).Func a).Type
let :
  ∀ (b : β) (hb : PSet.Equiv.{u, u} (A a) (B b)),
    ∃ (b : (⋃₀ PSet.mk β B).Type),
      PSet.Equiv.{u, u}
        ((⋃₀ PSet.mk α A).Func (Sigma.mk (β := fun (x : (PSet.mk α A).Type) ↦ ((PSet.mk α A).Func x).Type) a c))
        ((⋃₀ PSet.mk β B).Func b)
⊢ ∃ (b : (⋃₀ PSet.mk β B).Type),
    PSet.Equiv.{u, u}
      ((⋃₀ PSet.mk α A).Func (Sigma.mk (β := fun (x : (PSet.mk α A).Type) ↦ ((PSet.mk α A).Func x).Type) a c))
      ((⋃₀ PSet.mk β B).Func b)

Tactic:
let ⟨b, hb⟩ := αβ a
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
α β : Type u
A : α → PSet.{u}
B : β → PSet.{u}
αβ : ∀ (a : α), ∃ (b : β), PSet.Equiv.{u, u} (A a) (B b)
a : (PSet.mk α A).Type
c : ((PSet.mk α A).Func a).Type
b : β
hb : PSet.Equiv.{u, u} (A a) (B b)
mk :
  ∀ (γ : Type u) (Γ : γ → PSet.{u}),
    (∀ (a_1 : γ) (ea : A a = Γ a_1),
        ∃ (b : (⋃₀ PSet.mk β B).Type),
          PSet.Equiv.{u, u}
            ((⋃₀ PSet.mk α A).Func (Sigma.mk (β := fun (x : (PSet.mk α A).Type) ↦ ((PSet.mk α A).Func x).Type) a c))
            ((⋃₀ PSet.mk β B).Func b)) →
      ∀ (ea : A a = PSet.mk γ Γ),
        ∃ (b : (⋃₀ PSet.mk β B).Type),
          PSet.Equiv.{u, u}
            ((⋃₀ PSet.mk α A).Func (Sigma.mk (β := fun (x : (PSet.mk α A).Type) ↦ ((PSet.mk α A).Func x).Type) a c))
            ((⋃₀ PSet.mk β B).Func b)
⊢ ∃ (b : (⋃₀ PSet.mk β B).Type),
    PSet.Equiv.{u, u}
      ((⋃₀ PSet.mk α A).Func (Sigma.mk (β := fun (x : (PSet.mk α A).Type) ↦ ((PSet.mk α A).Func x).Type) a c))
      ((⋃₀ PSet.mk β B).Func b)

Tactic:
induction ea : A a with | _ γ Γ
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
α β : Type u
A : α → PSet.{u}
B : β → PSet.{u}
αβ : ∀ (a : α), ∃ (b : β), PSet.Equiv.{u, u} (A a) (B b)
a : (PSet.mk α A).Type
c : ((PSet.mk α A).Func a).Type
b : β
hb : PSet.Equiv.{u, u} (A a) (B b)
γ : Type u
Γ : γ → PSet.{u}
A_ih :
  ∀ (a_1 : γ) (ea : A a = Γ a_1),
    ∃ (b : (⋃₀ PSet.mk β B).Type),
      PSet.Equiv.{u, u}
        ((⋃₀ PSet.mk α A).Func (Sigma.mk (β := fun (x : (PSet.mk α A).Type) ↦ ((PSet.mk α A).Func x).Type) a c))
        ((⋃₀ PSet.mk β B).Func b)
ea : A a = PSet.mk γ Γ
mk :
  ∀ (δ : Type u) (Δ : δ → PSet.{u}),
    (∀ (a_1 : δ) (eb : B b = Δ a_1),
        ∃ (b : (⋃₀ PSet.mk β B).Type),
          PSet.Equiv.{u, u}
            ((⋃₀ PSet.mk α A).Func (Sigma.mk (β := fun (x : (PSet.mk α A).Type) ↦ ((PSet.mk α A).Func x).Type) a c))
            ((⋃₀ PSet.mk β B).Func b)) →
      ∀ (eb : B b = PSet.mk δ Δ),
        ∃ (b : (⋃₀ PSet.mk β B).Type),
          PSet.Equiv.{u, u}
            ((⋃₀ PSet.mk α A).Func (Sigma.mk (β := fun (x : (PSet.mk α A).Type) ↦ ((PSet.mk α A).Func x).Type) a c))
            ((⋃₀ PSet.mk β B).Func b)
⊢ ∃ (b : (⋃₀ PSet.mk β B).Type),
    PSet.Equiv.{u, u}
      ((⋃₀ PSet.mk α A).Func (Sigma.mk (β := fun (x : (PSet.mk α A).Type) ↦ ((PSet.mk α A).Func x).Type) a c))
      ((⋃₀ PSet.mk β B).Func b)

Tactic:
induction eb : B b with | _ δ Δ
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
α β : Type u
A : α → PSet.{u}
B : β → PSet.{u}
αβ : ∀ (a : α), ∃ (b : β), PSet.Equiv.{u, u} (A a) (B b)
a : (PSet.mk α A).Type
c : ((PSet.mk α A).Func a).Type
b : β
hb : PSet.Equiv.{u, u} (A a) (B b)
γ : Type u
Γ : γ → PSet.{u}
A_ih :
  ∀ (a_1 : γ) (ea : A a = Γ a_1),
    ∃ (b : (⋃₀ PSet.mk β B).Type),
      PSet.Equiv.{u, u}
        ((⋃₀ PSet.mk α A).Func (Sigma.mk (β := fun (x : (PSet.mk α A).Type) ↦ ((PSet.mk α A).Func x).Type) a c))
        ((⋃₀ PSet.mk β B).Func b)
ea : A a = PSet.mk γ Γ
δ : Type u
Δ : δ → PSet.{u}
A_ih_1 :
  ∀ (a_1 : δ) (eb : B b = Δ a_1),
    ∃ (b : (⋃₀ PSet.mk β B).Type),
      PSet.Equiv.{u, u}
        ((⋃₀ PSet.mk α A).Func (Sigma.mk (β := fun (x : (PSet.mk α A).Type) ↦ ((PSet.mk α A).Func x).Type) a c))
        ((⋃₀ PSet.mk β B).Func b)
eb : B b = PSet.mk δ Δ
mk :
  (∀ (a_1 : γ) (ea : A a = Γ a_1),
      ∃ (b : (⋃₀ PSet.mk β B).Type),
        PSet.Equiv.{u, u}
          ((⋃₀ PSet.mk α A).Func (Sigma.mk (β := fun (x : (PSet.mk α A).Type) ↦ ((PSet.mk α A).Func x).Type) a c))
          ((⋃₀ PSet.mk β B).Func b)) →
    ∀ (ea : A a = PSet.mk γ Γ) (δ : Type u) (Δ : δ → PSet.{u}) (hb : PSet.Equiv.{u, u} (PSet.mk γ Γ) (PSet.mk δ Δ)),
      (∀ (a_1 : δ) (eb : B b = Δ a_1),
          ∃ (b : (⋃₀ PSet.mk β B).Type),
            PSet.Equiv.{u, u}
              ((⋃₀ PSet.mk α A).Func (Sigma.mk (β := fun (x : (PSet.mk α A).Type) ↦ ((PSet.mk α A).Func x).Type) a c))
              ((⋃₀ PSet.mk β B).Func b)) →
        ∀ (eb : B b = PSet.mk δ Δ),
          ∃ (b : (⋃₀ PSet.mk β B).Type),
            PSet.Equiv.{u, u}
              ((⋃₀ PSet.mk α A).Func (Sigma.mk (β := fun (x : (PSet.mk α A).Type) ↦ ((PSet.mk α A).Func x).Type) a c))
              ((⋃₀ PSet.mk β B).Func b)
⊢ ∃ (b : (⋃₀ PSet.mk β B).Type),
    PSet.Equiv.{u, u}
      ((⋃₀ PSet.mk α A).Func (Sigma.mk (β := fun (x : (PSet.mk α A).Type) ↦ ((PSet.mk α A).Func x).Type) a c))
      ((⋃₀ PSet.mk β B).Func b)

Tactic:
rw [ea, eb] at hb
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
α β : Type u
A : α → PSet.{u}
B : β → PSet.{u}
αβ : ∀ (a : α), ∃ (b : β), PSet.Equiv.{u, u} (A a) (B b)
a : (PSet.mk α A).Type
c : ((PSet.mk α A).Func a).Type
b : β
γ : Type u
Γ : γ → PSet.{u}
A_ih :
  ∀ (a_1 : γ) (ea : A a = Γ a_1),
    ∃ (b : (⋃₀ PSet.mk β B).Type),
      PSet.Equiv.{u, u}
        ((⋃₀ PSet.mk α A).Func (Sigma.mk (β := fun (x : (PSet.mk α A).Type) ↦ ((PSet.mk α A).Func x).Type) a c))
        ((⋃₀ PSet.mk β B).Func b)
ea : A a = PSet.mk γ Γ
δ : Type u
Δ : δ → PSet.{u}
hb : PSet.Equiv.{u, u} (PSet.mk γ Γ) (PSet.mk δ Δ)
A_ih_1 :
  ∀ (a_1 : δ) (eb : B b = Δ a_1),
    ∃ (b : (⋃₀ PSet.mk β B).Type),
      PSet.Equiv.{u, u}
        ((⋃₀ PSet.mk α A).Func (Sigma.mk (β := fun (x : (PSet.mk α A).Type) ↦ ((PSet.mk α A).Func x).Type) a c))
        ((⋃₀ PSet.mk β B).Func b)
eb : B b = PSet.mk δ Δ
⊢ ∀ (a : γ), ∃ (b : δ), PSet.Equiv.{u, u} (Γ a) (Δ b)

Tactic:
obtain ⟨γδ, δγ⟩ := hb
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
α β : Type u
A : α → PSet.{u}
B : β → PSet.{u}
αβ : ∀ (a : α), ∃ (b : β), PSet.Equiv.{u, u} (A a) (B b)
a : (PSet.mk α A).Type
c : ((PSet.mk α A).Func a).Type
b : β
γ : Type u
Γ : γ → PSet.{u}
A_ih :
  ∀ (a_1 : γ) (ea : A a = Γ a_1),
    ∃ (b : (⋃₀ PSet.mk β B).Type),
      PSet.Equiv.{u, u}
        ((⋃₀ PSet.mk α A).Func (Sigma.mk (β := fun (x : (PSet.mk α A).Type) ↦ ((PSet.mk α A).Func x).Type) a c))
        ((⋃₀ PSet.mk β B).Func b)
ea : A a = PSet.mk γ Γ
δ : Type u
Δ : δ → PSet.{u}
hb : PSet.Equiv.{u, u} (PSet.mk γ Γ) (PSet.mk δ Δ)
A_ih_1 :
  ∀ (a_1 : δ) (eb : B b = Δ a_1),
    ∃ (b : (⋃₀ PSet.mk β B).Type),
      PSet.Equiv.{u, u}
        ((⋃₀ PSet.mk α A).Func (Sigma.mk (β := fun (x : (PSet.mk α A).Type) ↦ ((PSet.mk α A).Func x).Type) a c))
        ((⋃₀ PSet.mk β B).Func b)
eb : B b = PSet.mk δ Δ
γδ : ∀ (a : γ), ∃ (b : δ), PSet.Equiv.{u, u} (Γ a) (Δ b)
⊢ ∀ (b : δ), ∃ (a : γ), PSet.Equiv.{u, u} (Γ a) (Δ b)

Tactic:
obtain ⟨γδ, δγ⟩ := hb
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
α β : Type u
A : α → PSet.{u}
B : β → PSet.{u}
αβ : ∀ (a : α), ∃ (b : β), PSet.Equiv.{u, u} (A a) (B b)
a : (PSet.mk α A).Type
c_1 : ((PSet.mk α A).Func a).Type
b : β
γ : Type u
Γ : γ → PSet.{u}
A_ih :
  ∀ (a_1 : γ) (ea : A a = Γ a_1),
    ∃ (b : (⋃₀ PSet.mk β B).Type),
      PSet.Equiv.{u, u}
        ((⋃₀ PSet.mk α A).Func (Sigma.mk (β := fun (x : (PSet.mk α A).Type) ↦ ((PSet.mk α A).Func x).Type) a c_1))
        ((⋃₀ PSet.mk β B).Func b)
ea : A a = PSet.mk γ Γ
δ : Type u
Δ : δ → PSet.{u}
A_ih_1 :
  ∀ (a_1 : δ) (eb : B b = Δ a_1),
    ∃ (b : (⋃₀ PSet.mk β B).Type),
      PSet.Equiv.{u, u}
        ((⋃₀ PSet.mk α A).Func (Sigma.mk (β := fun (x : (PSet.mk α A).Type) ↦ ((PSet.mk α A).Func x).Type) a c_1))
        ((⋃₀ PSet.mk β B).Func b)
eb : B b = PSet.mk δ Δ
γδ : ∀ (a : γ), ∃ (b : δ), PSet.Equiv.{u, u} (Γ a) (Δ b)
δγ : ∀ (b : δ), ∃ (a : γ), PSet.Equiv.{u, u} (Γ a) (Δ b)
c : (A a).Type := c_1
rwa rwa₁ rwa₂ rwa₃ : (c : (PSet.mk γ Γ).Type) → γ
⊢ γ

Tactic:
rwa [ea] at c