awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.SetTheory.ZFC.Rank
Goal:
x y w : ZFSet.{u_1}
left : w ∈ x
right : y ∈ w
⊢ y ∈ w

Tactic:
assumption
-- Module: Mathlib.SetTheory.ZFC.Rank
Goal:
x y w : ZFSet.{u_1}
left : w ∈ x
right : y ∈ w
⊢ w ∈ x

Tactic:
assumption
-- Module: Mathlib.SetTheory.ZFC.Rank
Goal:
x : ZFSet.{u_1}
rw : x.rank ≤ (⋃₀ x).powerset.rank
⊢ x.rank ≤ succ (⋃₀ x).rank

Tactic:
rw [← rank_powerset]

Premises used: ZFSet.rank_powerset
-- Module: Mathlib.SetTheory.ZFC.Rank
Goal:
x : ZFSet.{u_1}
h : x ⊆ (⋃₀ x).powerset
⊢ x.rank ≤ (⋃₀ x).powerset.rank

Tactic:
apply rank_mono

Premises used: ZFSet.rank_mono
-- Module: Mathlib.SetTheory.ZFC.Rank
Goal:
x z : ZFSet.{u_1}
h : z ∈ x → z ∈ (⋃₀ x).powerset
⊢ z ∈ x → z ∈ (⋃₀ x).powerset

Tactic:
_
-- Module: Mathlib.SetTheory.ZFC.Rank
Goal:
x z : ZFSet.{u_1}
h_1 : z ∈ x
h : z ⊆ ⋃₀ x
⊢ z ∈ (⋃₀ x).powerset

Tactic:
rw [mem_powerset]

Premises used: ZFSet.mem_powerset
-- Module: Mathlib.SetTheory.ZFC.Rank
Goal:
x z : ZFSet.{u_1}
h_1 : z ∈ x
z_1 : ZFSet.{u_1}
h : z_1 ∈ z → z_1 ∈ ⋃₀ x
⊢ z_1 ∈ z → z_1 ∈ ⋃₀ x

Tactic:
_
-- Module: Mathlib.SetTheory.ZFC.Rank
Goal:
x z : ZFSet.{u_1}
h_1 : z ∈ x
z_1 : ZFSet.{u_1}
h_2 : z_1 ∈ z
h : ∃ z ∈ x, z_1 ∈ z
⊢ z_1 ∈ ⋃₀ x

Tactic:
rw [mem_sUnion]

Premises used: ZFSet.mem_sUnion
-- Module: Mathlib.SetTheory.ZFC.Rank
Goal:
x z : ZFSet.{u_1}
h_1 : z ∈ x
z_1 : ZFSet.{u_1}
h_2 : z_1 ∈ z
h h₁ : z ∈ x ∧ z_1 ∈ z
⊢ ∃ z ∈ x, z_1 ∈ z

Tactic:
exists z
-- Module: Mathlib.SetTheory.ZFC.Rank
Goal:
α : Type u_1
inst : Small.{u, u_1} α
f : α → ZFSet.{u}
apply : (range f).rank ≤ ⨆ (i : α), succ (f i).rank
apply₁ : ∀ (i : α), succ (f i).rank ≤ (range f).rank
⊢ (range f).rank = ⨆ (i : α), succ (f i).rank

Tactic:
apply (Ordinal.iSup_le _).antisymm'

Premises used: LE.le.antisymm', Ordinal.iSup_le
-- Module: Mathlib.SetTheory.ZFC.Rank
Goal:
α : Type u_1
inst : Small.{u, u_1} α
f : α → ZFSet.{u}
⊢ (range f).rank ≤ ⨆ (i : α), succ (f i).rank

Tactic:
simpa [rank_le_iff, ← add_one_le_iff] using Ordinal.le_iSup _

Premises used: Order.add_one_le_iff, Ordinal.le_iSup, ZFSet.rank_le_iff
-- Module: Mathlib.SetTheory.ZFC.Rank
Goal:
α : Type u_1
inst : Small.{u, u_1} α
f : α → ZFSet.{u}
⊢ ∀ (i : α), succ (f i).rank ≤ (range f).rank

Tactic:
simp [rank_lt_of_mem]

Premises used: ZFSet.rank_lt_of_mem
-- Module: Mathlib.SetTheory.ZFC.Rank
Goal:
α : Type u_1
inst : Small.{u, u_1} α
f : α → ZFSet.{u}
a : (⋃ (i : α), f i).rank ≤ ⨆ (i : α), (f i).rank
a₁ : ⨆ (i : α), (f i).rank ≤ (⋃ (i : α), f i).rank
⊢ (⋃ (i : α), f i).rank = ⨆ (i : α), (f i).rank

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.SetTheory.ZFC.Rank
Goal:
α : Type u_1
inst : Small.{u, u_1} α
f : α → ZFSet.{u}
a : ∀ ⦃y : ZFSet.{u}⦄, (∃ (i : α), y ∈ f i) → y.rank < ⨆ (i : α), (f i).rank
⊢ (⋃ (i : α), f i).rank ≤ ⨆ (i : α), (f i).rank

Tactic:
simp_rw [rank_le_iff, mem_iUnion]

Premises used: ZFSet.mem_iUnion, ZFSet.rank_le_iff
-- Module: Mathlib.SetTheory.ZFC.Rank
Goal:
α : Type u_1
inst : Small.{u, u_1} α
f : α → ZFSet.{u}
y : ZFSet.{u}
a : ∀ (i : α) (hy : y ∈ f i), y.rank < ⨆ (i : α), (f i).rank
⊢ (∃ (i : α), y ∈ f i) → y.rank < ⨆ (i : α), (f i).rank

Tactic:
⟨i, hy⟩
-- Module: Mathlib.SetTheory.ZFC.Rank
Goal:
α : Type u_1
inst : Small.{u, u_1} α
f : α → ZFSet.{u}
y : ZFSet.{u}
i : α
hy : y ∈ f i
⊢ y.rank < ⨆ (i : α), (f i).rank

Tactic:
(rank_lt_of_mem hy).trans_le (Ordinal.le_iSup _ _)

Premises used: Ordinal.le_iSup, LT.lt.trans_le, ZFSet.rank_lt_of_mem
-- Module: Mathlib.SetTheory.ZFC.Rank
Goal:
α : Type u_1
inst : Small.{u, u_1} α
f : α → ZFSet.{u}
y : ZFSet.{u}
i : α
hy : y ∈ f i
⊢ y.rank < ⨆ (i : α), (f i).rank

Tactic:
exact (rank_lt_of_mem hy).trans_le (Ordinal.le_iSup _ _)
-- Module: Mathlib.SetTheory.ZFC.Rank
Goal:
α : Type u_1
inst : Small.{u, u_1} α
f : α → ZFSet.{u}
⊢ ⨆ (i : α), (f i).rank ≤ (⋃ (i : α), f i).rank

Tactic:
Ordinal.iSup_le fun i => rank_mono (subset_iUnion f i)

Premises used: Ordinal.iSup_le, ZFSet.rank_mono, ZFSet.subset_iUnion
-- Module: Mathlib.SetTheory.ZFC.Rank
Goal:
α : Type u_1
inst : Small.{u, u_1} α
f : α → ZFSet.{u}
⊢ ⨆ (i : α), (f i).rank ≤ (⋃ (i : α), f i).rank

Tactic:
exact Ordinal.iSup_le fun i => rank_mono (subset_iUnion f i)

Premises used: Ordinal.iSup_le, ZFSet.rank_mono, ZFSet.subset_iUnion
-- Module: Mathlib.SetTheory.ZFC.Rank
Goal:
x : ZFSet.{u}
h :
  ∀ (x : ZFSet.{u}) (ih : ∀ y ∈ x, lift.{u + 1, u} y.rank = IsWellFounded.rank (fun (x1 x2 : ZFSet.{u}) ↦ x1 ∈ x2) y),
    lift.{u + 1, u} x.rank = IsWellFounded.rank (fun (x1 x2 : ZFSet.{u}) ↦ x1 ∈ x2) x
⊢ lift.{u + 1, u} x.rank = IsWellFounded.rank (fun (x1 x2 : ZFSet.{u}) ↦ x1 ∈ x2) x

Tactic:
induction x using inductionOn with | _ x ih
-- Module: Mathlib.SetTheory.ZFC.Rank
Goal:
x_1 x : ZFSet.{u}
ih : ∀ y ∈ x, lift.{u + 1, u} y.rank = IsWellFounded.rank (fun (x1 x2 : ZFSet.{u}) ↦ x1 ∈ x2) y
h : lift.{u + 1, u} x.rank = ⨆ (b : ↥x), succ (IsWellFounded.rank (fun (x1 x2 : ZFSet.{u}) ↦ x1 ∈ x2) (↑b : ZFSet.{u}))
⊢ lift.{u + 1, u} x.rank = IsWellFounded.rank (fun (x1 x2 : ZFSet.{u}) ↦ x1 ∈ x2) x

Tactic:
rw [IsWellFounded.rank_eq]

Premises used: IsWellFounded.rank_eq
-- Module: Mathlib.SetTheory.ZFC.Rank
Goal:
x_1 x : ZFSet.{u}
ih : ∀ y ∈ x, lift.{u + 1, u} y.rank = IsWellFounded.rank (fun (x1 x2 : ZFSet.{u}) ↦ x1 ∈ x2) y
h : lift.{u + 1, u} x.rank = ⨆ (b : ↥x), succ (lift.{u + 1, u} (↑b : ZFSet.{u}).rank)
⊢ lift.{u + 1, u} x.rank = ⨆ (b : ↥x), succ (IsWellFounded.rank (fun (x1 x2 : ZFSet.{u}) ↦ x1 ∈ x2) (↑b : ZFSet.{u}))

Tactic:
simp_rw [← fun y : { y // y ∈ x } => ih y y.2]

Premises used: Subtype.val, Subtype.property
-- Module: Mathlib.SetTheory.ZFC.Rank
Goal:
x_1 x : ZFSet.{u}
ih : ∀ y ∈ x, lift.{u + 1, u} y.rank = IsWellFounded.rank (fun (x1 x2 : ZFSet.{u}) ↦ x1 ∈ x2) y
apply : ∀ c < lift.{u + 1, u} x.rank, c < ⨆ (i : ↥x), succ (lift.{u + 1, u} (↑i : ZFSet.{u}).rank)
apply₁ : ∀ (i : ↥x), succ (lift.{u + 1, u} (↑i : ZFSet.{u}).rank) ≤ lift.{u + 1, u} x.rank
⊢ lift.{u + 1, u} x.rank = ⨆ (b : ↥x), succ (lift.{u + 1, u} (↑b : ZFSet.{u}).rank)

Tactic:
apply (le_of_forall_lt _).antisymm (Ordinal.iSup_le _)

Premises used: Ordinal.iSup_le, LE.le.antisymm, le_of_forall_lt
-- Module: Mathlib.SetTheory.ZFC.Rank
Goal:
x_1 x : ZFSet.{u}
ih : ∀ y ∈ x, lift.{u + 1, u} y.rank = IsWellFounded.rank (fun (x1 x2 : ZFSet.{u}) ↦ x1 ∈ x2) y
h : Ordinal.{u + 1}
rw : (∃ a' < x.rank, lift.{u + 1, u} a' = h) → h < ⨆ (i : ↥x), succ (lift.{u + 1, u} (↑i : ZFSet.{u}).rank)
⊢ h < lift.{u + 1, u} x.rank → h < ⨆ (i : ↥x), succ (lift.{u + 1, u} (↑i : ZFSet.{u}).rank)

Tactic:
rw [lt_lift_iff]

Premises used: Ordinal.lt_lift_iff
-- Module: Mathlib.SetTheory.ZFC.Rank
Goal:
x_1 x : ZFSet.{u}
ih : ∀ y ∈ x, lift.{u + 1, u} y.rank = IsWellFounded.rank (fun (x1 x2 : ZFSet.{u}) ↦ x1 ∈ x2) y
o : Ordinal.{u}
h : o < x.rank
⊢ lift.{u + 1, u} o < ⨆ (i : ↥x), succ (lift.{u + 1, u} (↑i : ZFSet.{u}).rank)

Tactic:
simpa [Ordinal.lt_iSup_iff] using lt_rank_iff.1 h

Premises used: ZFSet.lt_rank_iff, Ordinal.lt_iSup_iff, Iff.mp
-- Module: Mathlib.SetTheory.ZFC.Rank
Goal:
x_1 x : ZFSet.{u}
ih : ∀ y ∈ x, lift.{u + 1, u} y.rank = IsWellFounded.rank (fun (x1 x2 : ZFSet.{u}) ↦ x1 ∈ x2) y
h : ↥x
⊢ succ (lift.{u + 1, u} (↑h : ZFSet.{u}).rank) ≤ lift.{u + 1, u} x.rank

Tactic:
simpa using rank_lt_of_mem h.2

Premises used: ZFSet.rank_lt_of_mem, Subtype.property
-- Module: Mathlib.SetTheory.ZFC.VonNeumann
Goal:
o : Ordinal.{u}
a : (↑(Set.Iio o) : Type (u + 1))
⊢ (↑a : Ordinal.{u}) < o

Tactic:
a.2

Premises used: Set.Mem, setOf, Set.Iio, Subtype.property
-- Module: Mathlib.SetTheory.ZFC.VonNeumann
Goal:
o : Ordinal.{u}
a : (↑(Set.Iio o) : Type (u + 1))
⊢ (↑a : Ordinal.{u}) < o

Tactic:
exact a.2

Premises used: Subtype.property
-- Module: Mathlib.SetTheory.ZFC.VonNeumann
Goal:
o : Ordinal.{u}
a : (↑(Set.Iio o) : Type (u + 1))
⊢ (↑a : Ordinal.{u}) < o

Tactic:
decreasing_by exact a.2

Premises used: Subtype.property
-- Module: Mathlib.SetTheory.ZFC.VonNeumann
Goal:
o : Ordinal.{u}
x : ZFSet.{u}
rw : x ∈ ⋃ (a : (↑(Set.Iio o) : Type (u + 1))), (V_ (↑a : Ordinal.{u})).powerset ↔ ∃ a < o, x ⊆ V_ a
⊢ x ∈ V_ o ↔ ∃ a < o, x ⊆ V_ a

Tactic:
rw [vonNeumann]

Premises used: ZFSet.vonNeumann
-- Module: Mathlib.SetTheory.ZFC.VonNeumann
Goal:
o : Ordinal.{u}
x : ZFSet.{u}
⊢ x ∈ ⋃ (a : (↑(Set.Iio o) : Type (u + 1))), (V_ (↑a : Ordinal.{u})).powerset ↔ ∃ a < o, x ⊆ V_ a

Tactic:
simp
-- Module: Mathlib.SetTheory.ZFC.VonNeumann
Goal:
o : Ordinal.{u_1}
rw : IsTransitive.{u_1} (⋃ (a : (↑(Set.Iio o) : Type (u_1 + 1))), (V_ (↑a : Ordinal.{u_1})).powerset)
⊢ IsTransitive.{u_1} (V_ o)

Tactic:
rw [vonNeumann]

Premises used: ZFSet.vonNeumann
-- Module: Mathlib.SetTheory.ZFC.VonNeumann
Goal:
o : Ordinal.{u_1}
⊢ IsTransitive.{u_1} (⋃ (a : (↑(Set.Iio o) : Type (u_1 + 1))), (V_ (↑a : Ordinal.{u_1})).powerset)

Tactic:
.iUnion fun ⟨a, _⟩ => (isTransitive_vonNeumann a).powerset

Premises used: ZFSet.IsTransitive, ZFSet.vonNeumann, _private.0.ZFSet.isTransitive_vonNeumann.match_1, ZFSet.IsTransitive.powerset, ZFSet.IsTransitive.iUnion, ZFSet.powerset, Subtype.val
-- Module: Mathlib.SetTheory.ZFC.VonNeumann
Goal:
o : Ordinal.{u_1}
⊢ IsTransitive.{u_1} (⋃ (a : (↑(Set.Iio o) : Type (u_1 + 1))), (V_ (↑a : Ordinal.{u_1})).powerset)

Tactic:
exact .iUnion fun ⟨a, _⟩ => (isTransitive_vonNeumann a).powerset
-- Module: Mathlib.SetTheory.ZFC.VonNeumann
Goal:
a b : Ordinal.{u}
h : a < b
rw : V_ a ∈ ⋃ (a : (↑(Set.Iio b) : Type (u + 1))), (V_ (↑a : Ordinal.{u})).powerset
⊢ V_ a ∈ V_ b

Tactic:
rw [vonNeumann]

Premises used: ZFSet.vonNeumann
-- Module: Mathlib.SetTheory.ZFC.VonNeumann
Goal:
a b : Ordinal.{u}
h : a < b
⊢ V_ a ∈ ⋃ (a : (↑(Set.Iio b) : Type (u + 1))), (V_ (↑a : Ordinal.{u})).powerset

Tactic:
aesop
-- Module: Mathlib.SetTheory.ZFC.VonNeumann
Goal:
a b : Ordinal.{u}
h : a ≤ b
⊢ ∀ (h : a = b), V_ a ⊆ V_ b

Tactic:
simp_all
-- Module: Mathlib.SetTheory.ZFC.VonNeumann
Goal:
o : Ordinal.{u_1}
x : ZFSet.{u_1}
rw : x ⊆ V_ o ↔ ∀ ⦃y : ZFSet.{u_1}⦄, y ∈ x → y.rank < o
⊢ x ⊆ V_ o ↔ x.rank ≤ o

Tactic:
rw [rank_le_iff]

Premises used: ZFSet.rank_le_iff
-- Module: Mathlib.SetTheory.ZFC.VonNeumann
Goal:
o : Ordinal.{u_1}
x : ZFSet.{u_1}
mp : x ⊆ V_ o → ∀ ⦃y : ZFSet.{u_1}⦄, y ∈ x → y.rank < o
mpr : (∀ ⦃y : ZFSet.{u_1}⦄, y ∈ x → y.rank < o) → x ⊆ V_ o
⊢ x ⊆ V_ o ↔ ∀ ⦃y : ZFSet.{u_1}⦄, y ∈ x → y.rank < o

Tactic:
constructor
-- Module: Mathlib.SetTheory.ZFC.VonNeumann
Goal:
o : Ordinal.{u_1}
x : ZFSet.{u_1}
hx : x ⊆ V_ o
y : ZFSet.{u_1}
hy : y ∈ x
mp : (V_ o).rank ≤ o
⊢ y.rank < o

Tactic:
apply (rank_lt_of_mem (hx hy)).trans_le

Premises used: LT.lt.trans_le, ZFSet.rank_lt_of_mem
-- Module: Mathlib.SetTheory.ZFC.VonNeumann
Goal:
o : Ordinal.{u_1}
x : ZFSet.{u_1}
hx : x ⊆ V_ o
y : ZFSet.{u_1}
hy : y ∈ x
mp : ∀ ⦃y : ZFSet.{u_1}⦄, (∃ a < o, y ⊆ V_ a) → y.rank < o
⊢ (V_ o).rank ≤ o

Tactic:
simp_rw [rank_le_iff, mem_vonNeumann']

Premises used: ZFSet.mem_vonNeumann', ZFSet.rank_le_iff
-- Module: Mathlib.SetTheory.ZFC.VonNeumann
Goal:
o : Ordinal.{u_1}
x : ZFSet.{u_1}
hx : x ⊆ V_ o
y : ZFSet.{u_1}
hy : y ∈ x
z : ZFSet.{u_1}
a : Ordinal.{u_1}
ha : a < o
hz : z ⊆ V_ a
⊢ z.rank < o

Tactic:
(subset_vonNeumann.1 hz).trans_lt ha

Premises used: Iff.mp, LE.le.trans_lt
-- Module: Mathlib.SetTheory.ZFC.VonNeumann
Goal:
o : Ordinal.{u_1}
x : ZFSet.{u_1}
hx : x ⊆ V_ o
y : ZFSet.{u_1}
hy : y ∈ x
z : ZFSet.{u_1}
a : Ordinal.{u_1}
ha : a < o
hz : z ⊆ V_ a
⊢ z.rank < o

Tactic:
exact (subset_vonNeumann.1 hz).trans_lt ha

Premises used: Iff.mp, LE.le.trans_lt
-- Module: Mathlib.SetTheory.ZFC.VonNeumann
Goal:
o : Ordinal.{u_1}
x : ZFSet.{u_1}
hx : ∀ ⦃y : ZFSet.{u_1}⦄, y ∈ x → y.rank < o
y : ZFSet.{u_1}
hy : y ∈ x
mpr : ∃ a < o, y ⊆ V_ a
⊢ y ∈ V_ o

Tactic:
rw [mem_vonNeumann']

Premises used: ZFSet.mem_vonNeumann'
-- Module: Mathlib.SetTheory.ZFC.VonNeumann
Goal:
o : Ordinal.{u_1}
x : ZFSet.{u_1}
hx : ∀ ⦃y : ZFSet.{u_1}⦄, y ∈ x → y.rank < o
y : ZFSet.{u_1}
hy : y ∈ x
⊢ y.rank < o

Tactic:
have := hx hy
-- Module: Mathlib.SetTheory.ZFC.VonNeumann
Goal:
o : Ordinal.{u_1}
x : ZFSet.{u_1}
hx : ∀ ⦃y : ZFSet.{u_1}⦄, y ∈ x → y.rank < o
y : ZFSet.{u_1}
hy : y ∈ x
this : y.rank < o
⊢ ∃ a < o, y ⊆ V_ a

Tactic:
⟨_, this, subset_vonNeumann.2 le_rfl⟩

Premises used: Iff.mpr, le_rfl, And.intro, Exists.intro
-- Module: Mathlib.SetTheory.ZFC.VonNeumann
Goal:
o : Ordinal.{u_1}
x : ZFSet.{u_1}
hx : ∀ ⦃y : ZFSet.{u_1}⦄, y ∈ x → y.rank < o
y : ZFSet.{u_1}
hy : y ∈ x
this : y.rank < o
⊢ ∃ a < o, y ⊆ V_ a

Tactic:
exact ⟨_, this, subset_vonNeumann.2 le_rfl⟩
-- Module: Mathlib.SetTheory.ZFC.VonNeumann
Goal:
x : ZFSet.{u_1}
⊢ x ⊆ V_ x.rank

Tactic:
simp [subset_vonNeumann]

Premises used: ZFSet.subset_vonNeumann
-- Module: Mathlib.SetTheory.ZFC.VonNeumann
Goal:
o : Ordinal.{u}
x : ZFSet.{u}
simp_rw : (∃ a < o, x.rank ≤ a) ↔ x.rank < o
⊢ x ∈ V_ o ↔ x.rank < o

Tactic:
simp_rw [mem_vonNeumann', subset_vonNeumann]

Premises used: ZFSet.subset_vonNeumann, ZFSet.mem_vonNeumann'
-- Module: Mathlib.SetTheory.ZFC.VonNeumann
Goal:
o : Ordinal.{u}
x : ZFSet.{u}
⊢ x.rank < o → ∃ a < o, x.rank ≤ a

Tactic:
aesop
-- Module: Mathlib.SetTheory.ZFC.VonNeumann
Goal:
o : Ordinal.{u}
x : ZFSet.{u}
⊢ (∃ a < o, x.rank ≤ a) ↔ x.rank < o

Tactic:
exact ⟨fun ⟨a, h₁, h₂⟩ ↦ h₂.trans_lt h₁, by aesop⟩
-- Module: Mathlib.SetTheory.ZFC.VonNeumann
Goal:
x : ZFSet.{u_1}
⊢ x ∈ V_ (succ x.rank)

Tactic:
simp [mem_vonNeumann]

Premises used: ZFSet.mem_vonNeumann
-- Module: Mathlib.SetTheory.ZFC.VonNeumann
Goal:
x : ZFSet.{u_1}
⊢ ∃ (o : Ordinal.{u_1}), x ∈ V_ o

Tactic:
⟨_, mem_vonNeumann_succ x⟩

Premises used: ZFSet.mem_vonNeumann_succ, Exists.intro
-- Module: Mathlib.SetTheory.ZFC.VonNeumann
Goal:
o : Ordinal.{u_1}
rw rw₁ : V_ o ⊆ V_ o
⊢ (V_ o).rank ≤ o

Tactic:
rw [← subset_vonNeumann]

Premises used: ZFSet.subset_vonNeumann
-- Module: Mathlib.SetTheory.ZFC.VonNeumann
Goal:
a b : Ordinal.{u}
⊢ V_ a ∈ V_ b ↔ a < b

Tactic:
simp [mem_vonNeumann]

Premises used: ZFSet.mem_vonNeumann
-- Module: Mathlib.SetTheory.ZFC.VonNeumann
Goal:
a b : Ordinal.{u}
⊢ V_ a ⊆ V_ b ↔ a ≤ b

Tactic:
simp [subset_vonNeumann]

Premises used: ZFSet.subset_vonNeumann
-- Module: Mathlib.SetTheory.ZFC.VonNeumann
Goal:
o : Ordinal.{u}
x y : ZFSet.{u}
h : x ⊆ y
hy : y ∈ V_ o
rw : ∀ (hy : y.rank < o), x.rank < o
⊢ x ∈ V_ o

Tactic:
rw [mem_vonNeumann] at *

Premises used: ZFSet.mem_vonNeumann
-- Module: Mathlib.SetTheory.ZFC.VonNeumann
Goal:
o : Ordinal.{u}
x y : ZFSet.{u}
h : x ⊆ y
hy : y.rank < o
⊢ x.rank < o

Tactic:
(rank_mono h).trans_lt hy

Premises used: ZFSet.rank_mono, LE.le.trans_lt
-- Module: Mathlib.SetTheory.ZFC.VonNeumann
Goal:
o : Ordinal.{u}
x y : ZFSet.{u}
h : x ⊆ y
hy : y.rank < o
⊢ x.rank < o

Tactic:
exact (rank_mono h).trans_lt hy

Premises used: ZFSet.rank_mono, LE.le.trans_lt
-- Module: Mathlib.SetTheory.ZFC.VonNeumann
Goal:
⊢ ∀ (x y : Ordinal.{u_1}), x ≤ y ↔ V_ x ≤ V_ y

Tactic:
simp
-- Module: Mathlib.SetTheory.ZFC.VonNeumann
Goal:
⊢ Function.Injective V_

Tactic:
vonNeumann_strictMono.injective

Premises used: ZFSet.vonNeumann_strictMono, StrictMono.injective
-- Module: Mathlib.SetTheory.ZFC.VonNeumann
Goal:
a b : Ordinal.{u}
⊢ V_ a = V_ b ↔ a = b

Tactic:
vonNeumann_injective.eq_iff

Premises used: Function.Injective.eq_iff, ZFSet.vonNeumann_injective
-- Module: Mathlib.SetTheory.ZFC.VonNeumann
Goal:
⊢ ∀ (y : ZFSet.{u_1}), y ∉ V_ 0

Tactic:
simp [mem_vonNeumann]

Premises used: ZFSet.mem_vonNeumann
-- Module: Mathlib.SetTheory.ZFC.VonNeumann
Goal:
o : Ordinal.{u_1}
z : ZFSet.{u_1}
rw : z.rank < o + 1 ↔ z ∈ (V_ o).powerset
rw₁ : z.rank < o + 1 ↔ z ⊆ V_ o
rw₂ : z.rank < o + 1 ↔ z.rank ≤ o
rw₃ rw₄ : z.rank ≤ o ↔ z.rank ≤ o
⊢ z ∈ V_ (o + 1) ↔ z ∈ (V_ o).powerset

Tactic:
rw [mem_vonNeumann, mem_powerset, subset_vonNeumann, lt_add_one_iff]

Premises used: ZFSet.subset_vonNeumann, ZFSet.mem_powerset, Order.lt_add_one_iff, ZFSet.mem_vonNeumann
-- Module: Mathlib.SetTheory.ZFC.VonNeumann
Goal:
o : Ordinal.{u_1}
⊢ V_ (succ o) = (V_ o).powerset

Tactic:
vonNeumann_add_one o

Premises used: Order.succ, ZFSet.vonNeumann_add_one
-- Module: Mathlib.SetTheory.ZFC.VonNeumann
Goal:
o : Ordinal.{u}
h : IsSuccPrelimit o
z : ZFSet.{u}
⊢ z ∈ V_ o ↔ z ∈ ⋃ (a : (↑(Set.Iio o) : Type (u + 1))), V_ (↑a : Ordinal.{u})

Tactic:
simpa [mem_vonNeumann] using h.lt_iff_exists_lt

Premises used: Order.IsSuccPrelimit.lt_iff_exists_lt, ZFSet.mem_vonNeumann
-- Module: Mathlib.SetTheory.ZFC.VonNeumann
Goal:
⊢ ⋃ (o : Ordinal.{u_1}), (↑(V_ o) : Class.{u_1}) = Class.univ

Tactic:
Class.eq_univ_of_forall fun x ↦ Set.mem_iUnion.2 <| exists_mem_vonNeumann x

Premises used: Iff.mpr, ZFSet.exists_mem_vonNeumann, Set.mem_iUnion, Class.eq_univ_of_forall, Class
-- Module: Mathlib.SetTheory.ZFC.VonNeumann
Goal:
o : Ordinal.{u_1}
⊢ o.toZFSet ⊆ V_ o

Tactic:
simp [subset_vonNeumann]

Premises used: ZFSet.subset_vonNeumann
-- Module: Mathlib.SetTheory.ZFC.VonNeumann
Goal:
o : Ordinal.{u_1}
⊢ o.card ≤ (V_ o).card

Tactic:
simpa using card_mono o.toZFSet_subset_vonNeumann

Premises used: Ordinal.toZFSet_subset_vonNeumann, ZFSet.card_mono
-- Module: Mathlib.SetTheory.ZFC.VonNeumann
Goal:
⊢ (V_ 0).card = preBeth 0

Tactic:
simp
-- Module: Mathlib.SetTheory.ZFC.VonNeumann
Goal:
o : Ordinal.{u}
ih : (V_ o).card = preBeth o
⊢ (V_ (o + 1)).card = preBeth (o + 1)

Tactic:
simp [ih]
-- Module: Mathlib.SetTheory.ZFC.VonNeumann
Goal:
o : Ordinal.{u}
ho : IsSuccLimit o
ih : ∀ o' < o, (V_ o').card = preBeth o'
limit :
  (⋃ (a : (↑(Set.Iio o) : Type (u + 1))), V_ (↑a : Ordinal.{u})).card =
    ⨆ (a : (↑(Set.Iio o) : Type (u + 1))), (V_ (↑a : Ordinal.{u})).card
⊢ (V_ o).card = preBeth o

Tactic:
simp_rw [preBeth_limit ho.isSuccPrelimit, ← fun i : Set.Iio o => ih i i.2,
      vonNeumann_of_isSuccPrelimit ho.isSuccPrelimit]

Premises used: Cardinal.preBeth_limit, Order.IsSuccLimit.isSuccPrelimit, ZFSet.vonNeumann_of_isSuccPrelimit, Subtype.val, Subtype.property
-- Module: Mathlib.SetTheory.ZFC.VonNeumann
Goal:
o : Ordinal.{u}
ho : IsSuccLimit o
ih : ∀ o' < o, (V_ o').card = preBeth o'
limit :
  (⋃ (i : (↑(Set.Iio o) : Type (u + 1))), V_ (↑i : Ordinal.{u})).card ≤
    ⨆ (i : (↑(Set.Iio o) : Type (u + 1))), (V_ (↑i : Ordinal.{u})).card
⊢ (⋃ (a : (↑(Set.Iio o) : Type (u + 1))), V_ (↑a : Ordinal.{u})).card =
    ⨆ (a : (↑(Set.Iio o) : Type (u + 1))), (V_ (↑a : Ordinal.{u})).card

Tactic:
apply iSup_card_le_card_iUnion.antisymm'

Premises used: LE.le.antisymm', ZFSet.iSup_card_le_card_iUnion
-- Module: Mathlib.SetTheory.ZFC.VonNeumann
Goal:
o : Ordinal.{u}
ho : IsSuccLimit o
ih : ∀ o' < o, (V_ o').card = preBeth o'
limit :
  lift.{u + 1, u} (⋃ (i : (↑(Set.Iio o) : Type (u + 1))), V_ (↑i : Ordinal.{u})).card ≤
    lift.{u + 1, u} (⨆ (i : (↑(Set.Iio o) : Type (u + 1))), (V_ (↑i : Ordinal.{u})).card)
⊢ (⋃ (i : (↑(Set.Iio o) : Type (u + 1))), V_ (↑i : Ordinal.{u})).card ≤
    ⨆ (i : (↑(Set.Iio o) : Type (u + 1))), (V_ (↑i : Ordinal.{u})).card

Tactic:
rw [← lift_le.{u + 1}]
-- Module: Mathlib.SetTheory.ZFC.VonNeumann
Goal:
o : Ordinal.{u}
ho : IsSuccLimit o
ih : ∀ o' < o, (V_ o').card = preBeth o'
limit :
  (sum fun (i : (↑(Set.Iio o) : Type (u + 1))) ↦ (V_ (↑i : Ordinal.{u})).card) ≤
    lift.{u + 1, u} (⨆ (i : (↑(Set.Iio o) : Type (u + 1))), (V_ (↑i : Ordinal.{u})).card)
⊢ lift.{u + 1, u} (⋃ (i : (↑(Set.Iio o) : Type (u + 1))), V_ (↑i : Ordinal.{u})).card ≤
    lift.{u + 1, u} (⨆ (i : (↑(Set.Iio o) : Type (u + 1))), (V_ (↑i : Ordinal.{u})).card)

Tactic:
apply lift_card_iUnion_le_sum_card.trans

Premises used: ZFSet.lift_card_iUnion_le_sum_card, LE.le.trans
-- Module: Mathlib.SetTheory.ZFC.VonNeumann
Goal:
o : Ordinal.{u}
ho : IsSuccLimit o
ih : ∀ o' < o, (V_ o').card = preBeth o'
⊢ (sum fun (i : (↑(Set.Iio o) : Type (u + 1))) ↦ (V_ (↑i : Ordinal.{u})).card) ≤
    lift.{u + 1, u} (⨆ (i : (↑(Set.Iio o) : Type (u + 1))), (V_ (↑i : Ordinal.{u})).card)

Tactic:
(sum_eq_lift_iSup_of_lift_mk_le_lift_iSup ?_ ?_).le

Premises used: Cardinal.sum_eq_lift_iSup_of_lift_mk_le_lift_iSup, Eq.le
-- Module: Mathlib.SetTheory.ZFC.VonNeumann
Goal:
o : Ordinal.{u}
ho : IsSuccLimit o
ih : ∀ o' < o, (V_ o').card = preBeth o'
limit : ℵ₀ ≤ #(↑(Set.Iio o) : Type (u + 1))
limit₁ :
  lift.{u, u + 1} #(↑(Set.Iio o) : Type (u + 1)) ≤
    lift.{u + 1, u} (⨆ (i : (↑(Set.Iio o) : Type (u + 1))), (V_ (↑i : Ordinal.{u})).card)
⊢ (sum fun (i : (↑(Set.Iio o) : Type (u + 1))) ↦ (V_ (↑i : Ordinal.{u})).card) ≤
    lift.{u + 1, u} (⨆ (i : (↑(Set.Iio o) : Type (u + 1))), (V_ (↑i : Ordinal.{u})).card)

Tactic:
refine (sum_eq_lift_iSup_of_lift_mk_le_lift_iSup ?_ ?_).le

Premises used: Cardinal.sum_eq_lift_iSup_of_lift_mk_le_lift_iSup, Eq.le
-- Module: Mathlib.SetTheory.ZFC.VonNeumann
Goal:
o : Ordinal.{u}
ho : IsSuccLimit o
ih : ∀ o' < o, (V_ o').card = preBeth o'
limit : Ordinal.omega0 ≤ o
⊢ ℵ₀ ≤ #(↑(Set.Iio o) : Type (u + 1))

Tactic:
rw [mk_Iio_ordinal, ← lift_aleph0.{u + 1, u}, lift_le, Ordinal.aleph0_le_card]

Premises used: Cardinal.mk_Iio_ordinal, Ordinal.aleph0_le_card, Cardinal.lift_le
-- Module: Mathlib.SetTheory.ZFC.VonNeumann
Goal:
o : Ordinal.{u}
ho : IsSuccLimit o
ih : ∀ o' < o, (V_ o').card = preBeth o'
⊢ Ordinal.omega0 ≤ o

Tactic:
Ordinal.omega0_le_of_isSuccLimit ho

Premises used: Ordinal.omega0_le_of_isSuccLimit
-- Module: Mathlib.SetTheory.ZFC.VonNeumann
Goal:
o : Ordinal.{u}
ho : IsSuccLimit o
ih : ∀ o' < o, (V_ o').card = preBeth o'
⊢ Ordinal.omega0 ≤ o

Tactic:
exact Ordinal.omega0_le_of_isSuccLimit ho

Premises used: Ordinal.omega0_le_of_isSuccLimit
-- Module: Mathlib.SetTheory.ZFC.VonNeumann
Goal:
o : Ordinal.{u}
ho : IsSuccLimit o
ih : ∀ o' < o, (V_ o').card = preBeth o'
limit : o.card ≤ ⨆ (i : (↑(Set.Iio o) : Type (u + 1))), (V_ (↑i : Ordinal.{u})).card
⊢ lift.{u, u + 1} #(↑(Set.Iio o) : Type (u + 1)) ≤
    lift.{u + 1, u} (⨆ (i : (↑(Set.Iio o) : Type (u + 1))), (V_ (↑i : Ordinal.{u})).card)

Tactic:
rw [mk_Iio_ordinal, lift_lift, lift_le]

Premises used: Cardinal.lift_lift, Cardinal.mk_Iio_ordinal, Cardinal.lift_le
-- Module: Mathlib.SetTheory.ZFC.VonNeumann
Goal:
o : Ordinal.{u}
ho : IsSuccLimit o
ih : ∀ o' < o, (V_ o').card = preBeth o'
limit : ∀ (h : ⨆ (i : (↑(Set.Iio o) : Type (u + 1))), (V_ (↑i : Ordinal.{u})).card < o.card), False
⊢ o.card ≤ ⨆ (i : (↑(Set.Iio o) : Type (u + 1))), (V_ (↑i : Ordinal.{u})).card

Tactic:
by_contra! h
-- Module: Mathlib.SetTheory.ZFC.VonNeumann
Goal:
o : Ordinal.{u}
ho : IsSuccLimit o
ih : ∀ o' < o, (V_ o').card = preBeth o'
h : ⨆ (i : (↑(Set.Iio o) : Type (u + 1))), (V_ (↑i : Ordinal.{u})).card < o.card
⊢ False

Tactic:
(⨆ i : Set.Iio o, (V_ ↑i).card).card_ord.not_lt <|
        (Ordinal.card_le_card_vonNeumann _).trans_lt <| (cantor _).trans_le ?_

Premises used: iSup, ZFSet.vonNeumann, Cardinal.cantor, LT.lt.trans_le, Cardinal.card_ord, Ordinal.card_le_card_vonNeumann, Eq.not_lt, ZFSet.card, Subtype.val, LE.le.trans_lt
-- Module: Mathlib.SetTheory.ZFC.VonNeumann
Goal:
o : Ordinal.{u}
ho : IsSuccLimit o
ih : ∀ o' < o, (V_ o').card = preBeth o'
h : ⨆ (i : (↑(Set.Iio o) : Type (u + 1))), (V_ (↑i : Ordinal.{u})).card < o.card
limit :
  HPow.hPow (α := Cardinal.{u}) 2
      (V_ (ord (⨆ (i : (↑(Set.Iio o) : Type (u + 1))), (V_ (↑i : Ordinal.{u})).card))).card ≤
    ⨆ (i : (↑(Set.Iio o) : Type (u + 1))), (V_ (↑i : Ordinal.{u})).card
⊢ False

Tactic:
refine (⨆ i : Set.Iio o, (V_ ↑i).card).card_ord.not_lt <|
        (Ordinal.card_le_card_vonNeumann _).trans_lt <| (cantor _).trans_le ?_

Premises used: iSup, ZFSet.vonNeumann, Cardinal.cantor, LT.lt.trans_le, Cardinal.card_ord, Ordinal.card_le_card_vonNeumann, Eq.not_lt, ZFSet.card, Subtype.val, LE.le.trans_lt
-- Module: Mathlib.SetTheory.ZFC.VonNeumann
Goal:
o : Ordinal.{u}
ho : IsSuccLimit o
ih : ∀ o' < o, (V_ o').card = preBeth o'
h : ⨆ (i : (↑(Set.Iio o) : Type (u + 1))), (V_ (↑i : Ordinal.{u})).card < o.card
limit :
  (V_ (succ (ord (⨆ (i : (↑(Set.Iio o) : Type (u + 1))), (V_ (↑i : Ordinal.{u})).card)))).card ≤
    ⨆ (i : (↑(Set.Iio o) : Type (u + 1))), (V_ (↑i : Ordinal.{u})).card
⊢ HPow.hPow (α := Cardinal.{u}) 2
      (V_ (ord (⨆ (i : (↑(Set.Iio o) : Type (u + 1))), (V_ (↑i : Ordinal.{u})).card))).card ≤
    ⨆ (i : (↑(Set.Iio o) : Type (u + 1))), (V_ (↑i : Ordinal.{u})).card

Tactic:
rw [← card_powerset, ← vonNeumann_succ]

Premises used: ZFSet.card_powerset, ZFSet.vonNeumann_succ