awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
α : Type u_1
inst : Small.{u, u_1} α
f : α → ZFSet.{u}
x : ZFSet.{u}
⊢ x ∈ (↑(range f) : Set ZFSet.{u}) ↔ x ∈ Set.range f

Tactic:
simp
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
α : Type u_1
inst : Small.{u, u_1} α
f : α → ZFSet.{u}
a : α
⊢ f a ∈ range f

Tactic:
simp
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
α : Type u_1
inst : Small.{u, u_1} α
f : α → ZFSet.{u}
x : ZFSet.{u}
⊢ x ∈ ⋃ (i : α), f i ↔ ∃ (i : α), x ∈ f i

Tactic:
simp [iUnion]

Premises used: ZFSet.iUnion
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
α : Type u_1
inst : Small.{u, u_1} α
f : α → ZFSet.{u}
h :
  ∀ (x : ZFSet.{u}),
    x ∈ (↑(⋃ (i : α), f i) : Set ZFSet.{u}) ↔
      Membership.mem (γ := Set ZFSet.{u}) (⋃ (i : α), (↑(f i) : Set ZFSet.{u})) x
⊢ (↑(⋃ (i : α), f i) : Set ZFSet.{u}) = ⋃ (i : α), (↑(f i) : Set ZFSet.{u})

Tactic:
ext
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
α : Type u_1
inst : Small.{u, u_1} α
f : α → ZFSet.{u}
x : ZFSet.{u}
⊢ x ∈ (↑(⋃ (i : α), f i) : Set ZFSet.{u}) ↔ Membership.mem (γ := Set ZFSet.{u}) (⋃ (i : α), (↑(f i) : Set ZFSet.{u})) x

Tactic:
simp
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
α : Type u_1
inst : Small.{u, u_1} α
f : α → ZFSet.{u}
i : α
x : ZFSet.{u}
hx : x ∈ f i
⊢ x ∈ ⋃ (i : α), f i

Tactic:
simpa using ⟨i, hx⟩
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
x y : ZFSet.{u}
⊢ (↑(x.pair y) : Set ZFSet.{u}) = {{x}, {x, y}}

Tactic:
simp [pair]

Premises used: ZFSet.pair
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
p : ZFSet.{u} → ZFSet.{u} → Prop
x y z : ZFSet.{u}
⊢ z ∈ pairSep p x y ↔ ∃ a ∈ x, ∃ b ∈ y, z = a.pair b ∧ p a b

Tactic:
mem_sep.trans ⟨And.right, fun e => ⟨?_, e⟩⟩

Premises used: ZFSet.mem_sep, Set.Mem, ZFSet.pairSep, And.right, And.intro, Iff.intro, Iff.trans
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
p : ZFSet.{u} → ZFSet.{u} → Prop
x y z : ZFSet.{u}
refine : ∀ (e : ∃ a ∈ x, ∃ b ∈ y, z = a.pair b ∧ p a b), z ∈ (x ∪ y).powerset.powerset
⊢ z ∈ pairSep p x y ↔ ∃ a ∈ x, ∃ b ∈ y, z = a.pair b ∧ p a b

Tactic:
refine mem_sep.trans ⟨And.right, fun e => ⟨?_, e⟩⟩

Premises used: ZFSet.mem_sep, And.right, And.intro, Iff.intro, Iff.trans
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
p : ZFSet.{u} → ZFSet.{u} → Prop
x y z : ZFSet.{u}
e : ∃ a ∈ x, ∃ b ∈ y, z = a.pair b ∧ p a b
⊢ z ∈ (x ∪ y).powerset.powerset

Tactic:
grind [mem_pair, mem_powerset, mem_singleton, mem_union, pair, subset_def]

Premises used: ZFSet.subset_def, ZFSet.mem_powerset, ZFSet.mem_pair, ZFSet.pair, ZFSet.mem_singleton, ZFSet.mem_union
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
x x' y y' : ZFSet.{u_1}
H : x.pair y = x'.pair y'
⊢ ∀ (z : ZFSet.{u_1}), z = {x} ∨ z = {x, y} ↔ z = {x'} ∨ z = {x', y'}

Tactic:
simp_rw [ZFSet.ext_iff, pair, mem_pair] at H

Premises used: ZFSet.mem_pair, ZFSet.pair, ZFSet.ext_iff
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
x x' y y' : ZFSet.{u_1}
H : ∀ (z : ZFSet.{u_1}), z = {x} ∨ z = {x, y} ↔ z = {x'} ∨ z = {x', y'}
⊢ x = x' ∧ (x = x' ∨ x = y')

Tactic:
simpa [or_and_left] using (H {x}).1 (Or.inl rfl)

Premises used: or_and_left, Iff.mp, Or.inl, Singleton.singleton, rfl
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
x x' y y' : ZFSet.{u_1}
H : ∀ (z : ZFSet.{u_1}), z = {x} ∨ z = {x, y} ↔ z = {x'} ∨ z = {x', y'}
obtain : ∀ (H : ∀ (z : ZFSet.{u_1}), z = {x} ∨ z = {x, y} ↔ z = {x} ∨ z = {x, y'}), x = x ∧ y = y'
⊢ x = x' ∧ y = y'

Tactic:
obtain rfl : x = x' := And.left <| by simpa [or_and_left] using (H {x}).1 (Or.inl rfl)

Premises used: And.left, rfl
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
y y' : ZFSet.{u_1}
H : ∀ (z : ZFSet.{u_1}), z = {y} ∨ z = {y, y} ↔ z = {y} ∨ z = {y, y'}
⊢ y = y'

Tactic:
simpa [eq_comm] using H {y, y'}

Premises used: Insert.insert, eq_comm, Singleton.singleton
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
x y y' : ZFSet.{u_1}
H : ∀ (z : ZFSet.{u_1}), z = {x} ∨ z = {x, y} ↔ z = {x} ∨ z = {x, y'}
⊢ y = x → y = y'

Tactic:
have he : y = x → y = y' := by
    rintro rfl
    simpa [eq_comm] using H {y, y'}
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
x y y' : ZFSet.{u_1}
H : ∀ (z : ZFSet.{u_1}), z = {x} ∨ z = {x, y} ↔ z = {x} ∨ z = {x, y'}
he : y = x → y = y'
⊢ Eq (α := ZFSet.{u_1}) {x, y} {x} ∨ Eq (α := ZFSet.{u_1}) {x, y} {x, y} ↔
    Eq (α := ZFSet.{u_1}) {x, y} {x} ∨ Eq (α := ZFSet.{u_1}) {x, y} {x, y'}

Tactic:
have hx := H {x, y}
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
x y y' : ZFSet.{u_1}
H : ∀ (z : ZFSet.{u_1}), z = {x} ∨ z = {x, y} ↔ z = {x} ∨ z = {x, y'}
he : y = x → y = y'
hx :
  Eq (α := ZFSet.{u_1}) {x, y} {x} ∨ Eq (α := ZFSet.{u_1}) {x, y} {x, y} ↔
    Eq (α := ZFSet.{u_1}) {x, y} {x} ∨ Eq (α := ZFSet.{u_1}) {x, y} {x, y'}
⊢ y = x ∨ Eq (α := ZFSet.{u_1}) {x, y} {x, y'}

Tactic:
simp_rw [pair_eq_singleton_iff, true_and, or_true, true_iff] at hx

Premises used: ZFSet.pair_eq_singleton_iff, true_iff, or_true, true_and
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
x y y' : ZFSet.{u_1}
H : ∀ (z : ZFSet.{u_1}), z = {x} ∨ z = {x, y} ↔ z = {x} ∨ z = {x, y'}
he : y = x → y = y'
hx : y = x ∨ Eq (α := ZFSet.{u_1}) {x, y} {x, y'}
⊢ x = x ∧ y = y'

Tactic:
⟨rfl, hx.elim he fun hy ↦ Or.elim ?_ he id⟩

Premises used: id, And.intro, Or.elim, rfl
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
x y y' : ZFSet.{u_1}
H : ∀ (z : ZFSet.{u_1}), z = {x} ∨ z = {x, y} ↔ z = {x} ∨ z = {x, y'}
he : y = x → y = y'
hx : y = x ∨ Eq (α := ZFSet.{u_1}) {x, y} {x, y'}
refine : ∀ (hy : Eq (α := ZFSet.{u_1}) {x, y} {x, y'}), y = x ∨ y = y'
⊢ x = x ∧ y = y'

Tactic:
refine ⟨rfl, hx.elim he fun hy ↦ Or.elim ?_ he id⟩
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
x y y' : ZFSet.{u_1}
H : ∀ (z : ZFSet.{u_1}), z = {x} ∨ z = {x, y} ↔ z = {x} ∨ z = {x, y'}
he : y = x → y = y'
hx : y = x ∨ Eq (α := ZFSet.{u_1}) {x, y} {x, y'}
hy : Eq (α := ZFSet.{u_1}) {x, y} {x, y'}
⊢ y = x ∨ y = y'

Tactic:
simpa using ZFSet.ext_iff.1 hy y

Premises used: Iff.mp, ZFSet.ext_iff
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
x y x' y' : ZFSet.{u_1}
⊢ x.pair y = x'.pair y' ↔ x = x' ∧ y = y'

Tactic:
pair_injective.eq_iff

Premises used: ZFSet.pair_injective, Function.Injective2.eq_iff
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
x y z : ZFSet.{u}
⊢ z ∈ x.prod y ↔ ∃ a ∈ x, ∃ b ∈ y, z = a.pair b

Tactic:
simp [prod]

Premises used: ZFSet.prod
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
x y a b : ZFSet.{u}
⊢ a.pair b ∈ x.prod y ↔ a ∈ x ∧ b ∈ y

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

Tactic:
simp [funs, IsFunc]

Premises used: ZFSet.funs, ZFSet.IsFunc
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
f : ZFSet.{u_1} → ZFSet.{u_1}
inst : Definable₁ f
x y : ZFSet.{u_1}
⊢ y ∈ map f x ↔ ∃ z ∈ x, z.pair (f z) = y

Tactic:
mem_image

Premises used: Set.Mem, ZFSet.mem_image, ZFSet.map
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
f : ZFSet.{u} → ZFSet.{u}
inst : Definable₁ f
x z : ZFSet.{u}
zx : z ∈ x
y : ZFSet.{u}
yx : (fun (w : ZFSet.{u}) ↦ z.pair w ∈ map f x) y
let : ∀ w ∈ x, ∀ (we : w.pair (f w) = z.pair y), y = f z
⊢ y = f z

Tactic:
let ⟨w, _, we⟩ := mem_image.1 yx
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
f : ZFSet.{u} → ZFSet.{u}
inst : Definable₁ f
x z : ZFSet.{u}
zx : z ∈ x
y : ZFSet.{u}
yx : (fun (w : ZFSet.{u}) ↦ z.pair w ∈ map f x) y
w : ZFSet.{u}
left : w ∈ x
we : w.pair (f w) = z.pair y
⊢ w = z

Tactic:
let ⟨wz, fy⟩ := pair_injective we
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
f : ZFSet.{u} → ZFSet.{u}
inst : Definable₁ f
x z : ZFSet.{u}
zx : z ∈ x
y : ZFSet.{u}
yx : (fun (w : ZFSet.{u}) ↦ z.pair w ∈ map f x) y
w : ZFSet.{u}
left : w ∈ x
we : w.pair (f w) = z.pair y
wz : w = z
⊢ f w = y

Tactic:
let ⟨wz, fy⟩ := pair_injective we
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
f : ZFSet.{u} → ZFSet.{u}
inst : Definable₁ f
x z : ZFSet.{u}
zx : z ∈ x
y : ZFSet.{u}
yx : (fun (w : ZFSet.{u}) ↦ z.pair w ∈ map f x) y
w : ZFSet.{u}
left : w ∈ x
we : w.pair (f w) = z.pair y
wz : w = z
fy : f w = y
rw : f w = f z
rw₁ rw₂ : f z = f z
⊢ y = f z

Tactic:
rw [← fy, wz]
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
f : ZFSet.{u_1} → ZFSet.{u_1}
inst : Definable₁ f
x y : ZFSet.{u_1}
⊢ x.IsFunc y (map f x) ↔ ∀ z ∈ x, f z ∈ y

Tactic:
⟨fun ⟨ss, h⟩ z zx =>
    let ⟨_, t1, t2⟩ := h z zx
    (t2 (f z) (image.mk _ _ zx)).symm ▸ (pair_mem_prod.1 (ss t1)).right,
    fun h =>
    ⟨fun _ yx =>
      let ⟨z, zx, ze⟩ := mem_image.1 yx
      ze ▸ pair_mem_prod.2 ⟨zx, h z zx⟩,
      fun _ => map_unique⟩⟩

Premises used: Iff.mpr, _private.0.ZFSet.map_isFunc.match_2, ZFSet.pair_mem_prod, Membership.mem, Eq.rec, ZFSet.prod, ZFSet.map_unique, ZFSet.pair, And.right, _private.0.ZFSet.map_isFunc.match_1, And.intro, Iff.intro, Iff.mp, _private.0.ZFSet.map_isFunc.match_3, ZFSet.mem_image, Eq.symm, ZFSet.image.mk
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
p : ZFSet.{u} → Prop
x : ZFSet.{u}
rw rw₁ : Hereditarily p x ↔ Hereditarily p x
⊢ Hereditarily p x ↔ p x ∧ ∀ y ∈ x, Hereditarily p y

Tactic:
rw [← Hereditarily]

Premises used: ZFSet.Hereditarily
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
p : ZFSet.{u} → Prop
x : ZFSet.{u}
h : Hereditarily p x
⊢ p x

Tactic:
h.def.1

Premises used: ZFSet.Hereditarily.def, And.left
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
p : ZFSet.{u} → Prop
x y : ZFSet.{u}
h : Hereditarily p x
hy : y ∈ x
⊢ Hereditarily p y

Tactic:
h.def.2 _ hy

Premises used: ZFSet.Hereditarily.def, And.right
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
p : ZFSet.{u} → Prop
x : ZFSet.{u}
apply : ∀ (x : ZFSet.{u}), (∀ y ∈ x, Hereditarily p y → p ∅) → Hereditarily p x → p ∅
⊢ Hereditarily p x → p ∅

Tactic:
apply @ZFSet.inductionOn _ x

Premises used: ZFSet.inductionOn
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
p : ZFSet.{u} → Prop
x y : ZFSet.{u}
IH : ∀ y_1 ∈ y, Hereditarily p y_1 → p ∅
h : Hereditarily p y
inl :
  ∀ (IH : ∀ (y : ZFSet.{u}), Membership.mem (γ := ZFSet.{u}) ∅ y → Hereditarily p y → p ∅) (h : Hereditarily p ∅), p ∅
inr : ∀ (a : ZFSet.{u}) (ha : a ∈ (↑y : Set ZFSet.{u})), p ∅
⊢ p ∅

Tactic:
rcases ZFSet.eq_empty_or_nonempty y with (rfl | ⟨a, ha⟩)

Premises used: ZFSet.eq_empty_or_nonempty, rfl
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
p : ZFSet.{u} → Prop
x : ZFSet.{u}
IH : ∀ (y : ZFSet.{u}), Membership.mem (γ := ZFSet.{u}) ∅ y → Hereditarily p y → p ∅
h : Hereditarily p ∅
⊢ p ∅

Tactic:
h.self

Premises used: ZFSet.Hereditarily.self
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
p : ZFSet.{u} → Prop
x : ZFSet.{u}
IH : ∀ (y : ZFSet.{u}), Membership.mem (γ := ZFSet.{u}) ∅ y → Hereditarily p y → p ∅
h : Hereditarily p ∅
⊢ p ∅

Tactic:
exact h.self

Premises used: ZFSet.Hereditarily.self
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
p : ZFSet.{u} → Prop
x y : ZFSet.{u}
IH : ∀ y_1 ∈ y, Hereditarily p y_1 → p ∅
h : Hereditarily p y
a : ZFSet.{u}
ha : a ∈ (↑y : Set ZFSet.{u})
⊢ p ∅

Tactic:
IH a ha (h.mem ha)

Premises used: ZFSet.Hereditarily.mem
-- Module: Mathlib.SetTheory.ZFC.Basic
Goal:
p : ZFSet.{u} → Prop
x y : ZFSet.{u}
IH : ∀ y_1 ∈ y, Hereditarily p y_1 → p ∅
h : Hereditarily p y
a : ZFSet.{u}
ha : a ∈ (↑y : Set ZFSet.{u})
⊢ p ∅

Tactic:
exact IH a ha (h.mem ha)

Premises used: ZFSet.Hereditarily.mem
-- Module: Mathlib.SetTheory.ZFC.Cardinal
Goal:
x : ZFSet.{u}
rw : #↥x = lift.{u + 1, u} #(Shrink.{u, u + 1} ↥x)
rw₁ rw₂ : #↥x = #↥x
⊢ #↥x = lift.{u + 1, u} x.card

Tactic:
rw [card, lift_mk_shrink'']

Premises used: Cardinal.lift_mk_shrink'', ZFSet.card
-- Module: Mathlib.SetTheory.ZFC.Cardinal
Goal:
x y : ZFSet.{u}
h : x ⊆ y
⊢ x.card ≤ y.card

Tactic:
simpa [cardinalMk_coe_sort] using mk_le_mk_of_subset (coe_subset_coe.2 h)

Premises used: Iff.mpr, ZFSet.coe_subset_coe, Cardinal.mk_le_mk_of_subset, ZFSet.cardinalMk_coe_sort
-- Module: Mathlib.SetTheory.ZFC.Cardinal
Goal:
rw : #↥∅ = lift.{u_1 + 1, u_1} 0
⊢ card ∅ = 0

Tactic:
rw [← lift_inj, ← cardinalMk_coe_sort]

Premises used: Cardinal.lift_inj, ZFSet.cardinalMk_coe_sort
-- Module: Mathlib.SetTheory.ZFC.Cardinal
Goal:
⊢ #↥∅ = lift.{u_1 + 1, u_1} 0

Tactic:
simp
-- Module: Mathlib.SetTheory.ZFC.Cardinal
Goal:
x y : ZFSet.{u}
rw : lift.{u + 1, u} (insert x y).card ≤ lift.{u + 1, u} (y.card + 1)
⊢ (insert x y).card ≤ y.card + 1

Tactic:
rw [← lift_le.{u + 1}]
-- Module: Mathlib.SetTheory.ZFC.Cardinal
Goal:
x y : ZFSet.{u}
⊢ lift.{u + 1, u} (insert x y).card ≤ lift.{u + 1, u} (y.card + 1)

Tactic:
simpa [← cardinalMk_coe_sort] using mk_insert_le

Premises used: Cardinal.mk_insert_le, ZFSet.cardinalMk_coe_sort
-- Module: Mathlib.SetTheory.ZFC.Cardinal
Goal:
x y : ZFSet.{u}
h : x ∉ y
rw : lift.{u + 1, u} (insert x y).card = lift.{u + 1, u} (y.card + 1)
⊢ (insert x y).card = y.card + 1

Tactic:
rw [← lift_inj.{u, u + 1}]
-- Module: Mathlib.SetTheory.ZFC.Cardinal
Goal:
x y : ZFSet.{u}
h : x ∉ y
⊢ lift.{u + 1, u} (insert x y).card = lift.{u + 1, u} (y.card + 1)

Tactic:
simpa [← cardinalMk_coe_sort] using mk_insert (SetLike.mem_coe.not.2 h)

Premises used: Iff.mpr, Iff.not, SetLike.mem_coe, Cardinal.mk_insert, ZFSet.cardinalMk_coe_sort
-- Module: Mathlib.SetTheory.ZFC.Cardinal
Goal:
x : ZFSet.{u}
⊢ card {x} = 1

Tactic:
simpa [notMem_singleton] using card_insert (notMem_empty x)

Premises used: ZFSet.notMem_empty, ZFSet.notMem_singleton, ZFSet.card_insert
-- Module: Mathlib.SetTheory.ZFC.Cardinal
Goal:
x y : ZFSet.{u}
h : x ≠ y
⊢ card {x, y} = card {y} + 1

Tactic:
card_insert (notMem_singleton.2 h)

Premises used: Iff.mpr, ZFSet.notMem_singleton, ZFSet.card_insert
-- Module: Mathlib.SetTheory.ZFC.Cardinal
Goal:
x y : ZFSet.{u}
h : x ≠ y
h₁ : 2 = card {y} + 1
⊢ card {x, y} = 2

Tactic:
convert! card_insert (notMem_singleton.2 h)

Premises used: Iff.mpr, ZFSet.notMem_singleton, ZFSet.card_insert
-- Module: Mathlib.SetTheory.ZFC.Cardinal
Goal:
x y : ZFSet.{u}
h : x ≠ y
h₁ : 2 = HAdd.hAdd (α := Cardinal.{u}) 1 1
h₂ h₃ : Eq.{u + 2} (α := Cardinal.{u}) 2 2
⊢ 2 = card {y} + 1

Tactic:
rw [card_singleton, one_add_one_eq_two]

Premises used: ZFSet.card_singleton, one_add_one_eq_two
-- Module: Mathlib.SetTheory.ZFC.Cardinal
Goal:
x y : ZFSet.{u}
rw : lift.{u + 1, u} (x ∪ y).card ≤ lift.{u + 1, u} (x.card + y.card)
⊢ (x ∪ y).card ≤ x.card + y.card

Tactic:
rw [← lift_le.{u + 1}]
-- Module: Mathlib.SetTheory.ZFC.Cardinal
Goal:
x y : ZFSet.{u}
⊢ lift.{u + 1, u} (x ∪ y).card ≤ lift.{u + 1, u} (x.card + y.card)

Tactic:
simpa [← cardinalMk_coe_sort] using mk_union_le (x : Set ZFSet) y

Premises used: SetLike.coe, ZFSet.cardinalMk_coe_sort, Cardinal.mk_union_le
-- Module: Mathlib.SetTheory.ZFC.Cardinal
Goal:
x : ZFSet.{u}
rw : lift.{u + 1, u} x.powerset.card = lift.{u + 1, u} (HPow.hPow (α := Cardinal.{u}) 2 x.card)
⊢ x.powerset.card = HPow.hPow (α := Cardinal.{u}) 2 x.card

Tactic:
rw [← lift_inj.{u, u + 1}]
-- Module: Mathlib.SetTheory.ZFC.Cardinal
Goal:
x : ZFSet.{u}
⊢ lift.{u + 1, u} x.powerset.card = lift.{u + 1, u} (HPow.hPow (α := Cardinal.{u}) 2 x.card)

Tactic:
simpa [← cardinalMk_coe_sort] using mk_congr (powersetEquiv x)

Premises used: ZFSet.cardinalMk_coe_sort, ZFSet.powersetEquiv, Cardinal.mk_congr
-- Module: Mathlib.SetTheory.ZFC.Cardinal
Goal:
x : ZFSet.{u}
f : ZFSet.{u} → ZFSet.{u}
inst : Definable₁ f
⊢ (image f x).card ≤ x.card

Tactic:
simpa [cardinalMk_coe_sort, ← coe_image, -mem_image] using mk_image_le (f := f) (s := x)

Premises used: ZFSet.coe_image, Cardinal.mk_image_le, ZFSet.mem_image, ZFSet.cardinalMk_coe_sort
-- Module: Mathlib.SetTheory.ZFC.Cardinal
Goal:
α : Type u
inst : Small.{v, u} α
f : α → ZFSet.{v}
rw : lift.{max u (v + 1), max u v} (lift.{u, v} (range f).card) ≤ lift.{v + 1, u} #α
⊢ lift.{u, v} (range f).card ≤ lift.{v, u} #α

Tactic:
rw [← lift_le.{max u (v + 1)}, lift_lift.{v}, lift_umax.{u, v + 1}]
-- Module: Mathlib.SetTheory.ZFC.Cardinal
Goal:
α : Type u
inst : Small.{v, u} α
f : α → ZFSet.{v}
⊢ lift.{max u (v + 1), max u v} (lift.{u, v} (range f).card) ≤ lift.{v + 1, u} #α

Tactic:
simpa [cardinalMk_coe_sort, ← coe_range, -mem_range] using mk_range_le_lift (f := f)

Premises used: ZFSet.coe_range, ZFSet.cardinalMk_coe_sort, ZFSet.mem_range, Cardinal.mk_range_le_lift
-- Module: Mathlib.SetTheory.ZFC.Cardinal
Goal:
α : Type u
inst : Small.{v, u} α
f : α → ZFSet.{v}
⊢ ⨆ (i : α), (f i).card ≤ (⋃ (i : α), f i).card

Tactic:
simpa [cardinalMk_coe_sort, ← coe_iUnion, ← lift_iSup bddAbove_of_small, -mem_iUnion] using
    iSup_mk_le_mk_iUnion (f := SetLike.coe ∘ f)

Premises used: Cardinal.lift_iSup, ZFSet.mem_iUnion, ZFSet.coe_iUnion, Cardinal.bddAbove_of_small, ZFSet.cardinalMk_coe_sort, Cardinal.iSup_mk_le_mk_iUnion
-- Module: Mathlib.SetTheory.ZFC.Cardinal
Goal:
α : Type u
inst : Small.{v, u} α
f : α → ZFSet.{v}
rw :
  lift.{v + 1, max u v} (lift.{u, v} (⋃ (i : α), f i).card) ≤
    lift.{v + 1, max u v} (sum.{u, v} fun (i : α) ↦ (f i).card)
⊢ lift.{u, v} (⋃ (i : α), f i).card ≤ sum.{u, v} fun (i : α) ↦ (f i).card

Tactic:
rw [← lift_le.{max u (v + 1)}, lift_umax.{max u v, v + 1}]
-- Module: Mathlib.SetTheory.ZFC.Cardinal
Goal:
α : Type u
inst : Small.{v, u} α
f : α → ZFSet.{v}
⊢ lift.{v + 1, max u v} (lift.{u, v} (⋃ (i : α), f i).card) ≤
    lift.{v + 1, max u v} (sum.{u, v} fun (i : α) ↦ (f i).card)

Tactic:
simpa [cardinalMk_coe_sort, ← coe_iUnion, -mem_iUnion] using
    mk_iUnion_le_sum_mk_lift (f := SetLike.coe ∘ f)

Premises used: Cardinal.mk_iUnion_le_sum_mk_lift, ZFSet.mem_iUnion, ZFSet.coe_iUnion, ZFSet.cardinalMk_coe_sort
-- Module: Mathlib.SetTheory.ZFC.Class
Goal:
x y : Class.{u}
⊢ (∀ (z : ZFSet.{u}), x z ↔ y z) → x = y

Tactic:
Set.ext

Premises used: Set.ext, Set.Mem, Class
-- Module: Mathlib.SetTheory.ZFC.Class
Goal:
A B : Class.{u}
⊢ A ∈ B ↔ ∃ (x : ZFSet.{u}), (↑x : Class.{u}) = A ∧ B x

Tactic:
Iff.rfl

Premises used: Iff.rfl, Class.Mem, Class.ToSet
-- Module: Mathlib.SetTheory.ZFC.Class
Goal:
x : Class.{u}
⊢ x ∉ ∅

Tactic:
fun ⟨_, _, h⟩ => h

Premises used: False, _private.0.Class.notMem_empty.match_1, Not
-- Module: Mathlib.SetTheory.ZFC.Class
Goal:
x : ZFSet.{u}
⊢ ¬∅ x

Tactic:
id

Premises used: id, Not
-- Module: Mathlib.SetTheory.ZFC.Class
Goal:
A : Class.{u}
⊢ A ∈ univ ↔ ∃ (x : ZFSet.{u}), (↑x : Class.{u}) = A

Tactic:
exists_congr fun _ => iff_of_eq (and_true _)

Premises used: Class.ofSet, and_true, Class.Mem, exists_congr, Class.ToSet, Eq, iff_of_eq
-- Module: Mathlib.SetTheory.ZFC.Class
Goal:
x : ZFSet.{u}
⊢ univ x

Tactic:
trivial

Premises used: trivial, Set.univ, setOf, Class.univ
-- Module: Mathlib.SetTheory.ZFC.Class
Goal:
A : Class.{u}
⊢ A = univ ↔ ∀ (x : ZFSet.{u}), A x

Tactic:
Set.eq_univ_iff_forall

Premises used: Set.Mem, Set.eq_univ_iff_forall, Class, Class.univ
-- Module: Mathlib.SetTheory.ZFC.Class
Goal:
A : Class.{u}
⊢ (∀ (x : ZFSet.{u}), A x) → A = univ

Tactic:
Set.eq_univ_of_forall

Premises used: Set.Mem, Set.eq_univ_of_forall, Class, Class.univ
-- Module: Mathlib.SetTheory.ZFC.Class
Goal:
⊢ ∀ (x : ZFSet.{u}), Acc (fun (x1 x2 : Class.{u}) ↦ x1 ∈ x2) (↑x : Class.{u})

Tactic:
fun a => ZFSet.inductionOn a fun x IH => ⟨_, ?_⟩

Premises used: ZFSet.inductionOn
-- Module: Mathlib.SetTheory.ZFC.Class
Goal:
refine :
  ∀ (a x : ZFSet.{u}) (IH : ∀ y ∈ x, Acc (fun (x1 x2 : Class.{u}) ↦ x1 ∈ x2) (↑y : Class.{u})),
    ∀ y ∈ (↑x : Class.{u}), Acc (fun (x1 x2 : Class.{u}) ↦ x1 ∈ x2) y
⊢ ∀ (x : ZFSet.{u}), Acc (fun (x1 x2 : Class.{u}) ↦ x1 ∈ x2) (↑x : Class.{u})

Tactic:
refine fun a => ZFSet.inductionOn a fun x IH => ⟨_, ?_⟩
-- Module: Mathlib.SetTheory.ZFC.Class
Goal:
a x : ZFSet.{u}
IH : ∀ y ∈ x, Acc (fun (x1 x2 : Class.{u}) ↦ x1 ∈ x2) (↑y : Class.{u})
z : ZFSet.{u}
hz : (↑x : Class.{u}) z
⊢ Acc (fun (x1 x2 : Class.{u}) ↦ x1 ∈ x2) (↑z : Class.{u})

Tactic:
IH z hz
-- Module: Mathlib.SetTheory.ZFC.Class
Goal:
a x : ZFSet.{u}
IH : ∀ y ∈ x, Acc (fun (x1 x2 : Class.{u}) ↦ x1 ∈ x2) (↑y : Class.{u})
z : ZFSet.{u}
hz : (↑x : Class.{u}) z
⊢ Acc (fun (x1 x2 : Class.{u}) ↦ x1 ∈ x2) (↑z : Class.{u})

Tactic:
exact IH z hz
-- Module: Mathlib.SetTheory.ZFC.Class
Goal:
⊢ ∀ (x : ZFSet.{u}), Acc (fun (x1 x2 : Class.{u}) ↦ x1 ∈ x2) (↑x : Class.{u})

Tactic:
have H : ∀ x : ZFSet.{u}, @Acc Class.{u} (· ∈ ·) ↑x := by
      refine fun a => ZFSet.inductionOn a fun x IH => ⟨_, ?_⟩
      rintro A ⟨z, rfl, hz⟩
      exact IH z hz
-- Module: Mathlib.SetTheory.ZFC.Class
Goal:
H : ∀ (x : ZFSet.{u}), Acc (fun (x1 x2 : Class.{u}) ↦ x1 ∈ x2) (↑x : Class.{u})
⊢ ∀ (a : Class.{u}), Acc (fun (x1 x2 : Class.{u}) ↦ x1 ∈ x2) a

Tactic:
fun A => ⟨A, ?_⟩

Premises used: Acc.intro
-- Module: Mathlib.SetTheory.ZFC.Class
Goal:
H : ∀ (x : ZFSet.{u}), Acc (fun (x1 x2 : Class.{u}) ↦ x1 ∈ x2) (↑x : Class.{u})
refine : ∀ (A y : Class.{u}), y ∈ A → Acc (fun (x1 x2 : Class.{u}) ↦ x1 ∈ x2) y
⊢ ∀ (a : Class.{u}), Acc (fun (x1 x2 : Class.{u}) ↦ x1 ∈ x2) a

Tactic:
refine fun A => ⟨A, ?_⟩
-- Module: Mathlib.SetTheory.ZFC.Class
Goal:
H : ∀ (x : ZFSet.{u}), Acc (fun (x1 x2 : Class.{u}) ↦ x1 ∈ x2) (↑x : Class.{u})
A : Class.{u}
x : ZFSet.{u}
right : A x
⊢ Acc (fun (x1 x2 : Class.{u}) ↦ x1 ∈ x2) (↑x : Class.{u})

Tactic:
H x
-- Module: Mathlib.SetTheory.ZFC.Class
Goal:
H : ∀ (x : ZFSet.{u}), Acc (fun (x1 x2 : Class.{u}) ↦ x1 ∈ x2) (↑x : Class.{u})
A : Class.{u}
x : ZFSet.{u}
right : A x
⊢ Acc (fun (x1 x2 : Class.{u}) ↦ x1 ∈ x2) (↑x : Class.{u})

Tactic:
exact H x
-- Module: Mathlib.SetTheory.ZFC.Class
Goal:
⊢ IsWellFounded Class.{u_1} fun (x1 x2 : Class.{u_1}) ↦ x1 ∈ x2

Tactic:
⟨mem_wf⟩

Premises used: IsWellFounded.mk, Class.mem_wf
-- Module: Mathlib.SetTheory.ZFC.Class
Goal:
x y : Class.{u_1}
⊢ x ∈ y → y ∉ x

Tactic:
asymm_of (· ∈ ·)

Premises used: asymm_of, Membership.mem
-- Module: Mathlib.SetTheory.ZFC.Class
Goal:
x : Class.{u_1}
⊢ x ∉ x

Tactic:
irrefl_of (· ∈ ·) x

Premises used: irrefl_of, Membership.mem
-- Module: Mathlib.SetTheory.ZFC.Class
Goal:
⊢ univ ∉ univ

Tactic:
mem_irrefl _

Premises used: Class.mem_irrefl
-- Module: Mathlib.SetTheory.ZFC.Class
Goal:
⊢ congToClass ∅ = ∅

Tactic:
rfl
-- Module: Mathlib.SetTheory.ZFC.Class
Goal:
⊢ classToCong ∅ = ∅

Tactic:
simp [classToCong]

Premises used: Class.classToCong
-- Module: Mathlib.SetTheory.ZFC.Class
Goal:
x y : ZFSet.{u}
h : (↑x : Class.{u}) = (↑y : Class.{u})
z : ZFSet.{u}
rw rw₁ : (↑y : Class.{u}) z ↔ (↑y : Class.{u}) z
⊢ (↑x : Class.{u}) z ↔ (↑y : Class.{u}) z

Tactic:
rw [h]
-- Module: Mathlib.SetTheory.ZFC.Class
Goal:
A : Class.{u}
x : ZFSet.{u}
h : A.ToSet (↑x : Class.{u})
y : ZFSet.{u}
yx : (↑y : Class.{u}) = (↑x : Class.{u})
py : A y
rwa rwa₁ rwa₂ rwa₃ : ∀ (py : A x), A x
⊢ A x

Tactic:
rwa [ofSet.inj yx] at py

Premises used: Class.ofSet.inj
-- Module: Mathlib.SetTheory.ZFC.Class
Goal:
x : ZFSet.{u}
A : Class.{u}
⊢ (↑x : Class.{u}) ∈ A ↔ A x

Tactic:
toSet_of_ZFSet _ _

Premises used: Class.Mem, Class.toSet_of_ZFSet, Class.ToSet
-- Module: Mathlib.SetTheory.ZFC.Class
Goal:
x y : ZFSet.{u}
⊢ (↑y : Class.{u}) x ↔ x ∈ y

Tactic:
Iff.rfl

Premises used: Class.ofSet, Iff.rfl, setOf
-- Module: Mathlib.SetTheory.ZFC.Class
Goal:
x y : ZFSet.{u}
⊢ (↑x : Class.{u}) ⊆ (↑y : Class.{u}) ↔ x ⊆ y

Tactic:
Iff.rfl

Premises used: Class.ofSet, Set.Mem, Iff.rfl, setOf, Set.Subset, ZFSet.toSet, ZFSet.Subset
-- Module: Mathlib.SetTheory.ZFC.Class
Goal:
p : Class.{u}
x : ZFSet.{u}
⊢ (↑(ZFSet.sep p x) : Class.{u}) = {y : ZFSet.{u} | y ∈ x ∧ p y}

Tactic:
ext fun _ => ZFSet.mem_sep

Premises used: ZFSet.mem_sep, Class.ext
-- Module: Mathlib.SetTheory.ZFC.Class
Goal:
⊢ (↑∅ : Class.{u}) = ∅

Tactic:
ext fun y => iff_false _ ▸ ZFSet.notMem_empty y

Premises used: Class.ofSet, ZFSet.notMem_empty, iff_false, Class.ext, Eq.rec, EmptyCollection.emptyCollection, Eq.symm
-- Module: Mathlib.SetTheory.ZFC.Class
Goal:
x y : ZFSet.{u}
⊢ (↑(insert x y) : Class.{u}) = insert x (↑y : Class.{u})

Tactic:
ext fun _ => ZFSet.mem_insert_iff

Premises used: Class.ext, ZFSet.mem_insert_iff
-- Module: Mathlib.SetTheory.ZFC.Class
Goal:
x y : ZFSet.{u}
⊢ (↑(x ∪ y) : Class.{u}) = (↑x : Class.{u}) ∪ (↑y : Class.{u})

Tactic:
ext fun _ => ZFSet.mem_union

Premises used: Class.ext, ZFSet.mem_union
-- Module: Mathlib.SetTheory.ZFC.Class
Goal:
x y : ZFSet.{u}
⊢ (↑(x ∩ y) : Class.{u}) = (↑x : Class.{u}) ∩ (↑y : Class.{u})

Tactic:
ext fun _ => ZFSet.mem_inter

Premises used: Class.ext, ZFSet.mem_inter
-- Module: Mathlib.SetTheory.ZFC.Class
Goal:
x y : ZFSet.{u}
⊢ (↑(x \ y) : Class.{u}) = (↑x : Class.{u}) \ (↑y : Class.{u})

Tactic:
ext fun _ => ZFSet.mem_sdiff

Premises used: Class.ext, ZFSet.mem_sdiff
-- Module: Mathlib.SetTheory.ZFC.Class
Goal:
x : ZFSet.{u}
⊢ (↑x.powerset : Class.{u}) = (↑x : Class.{u}).powerset

Tactic:
ext fun _ => ZFSet.mem_powerset

Premises used: Class.ext, ZFSet.mem_powerset
-- Module: Mathlib.SetTheory.ZFC.Class
Goal:
A : Class.{u}
x : ZFSet.{u}
⊢ A.powerset x ↔ (↑x : Class.{u}) ⊆ A

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.powerset, Class.congToClass, Class.powerset