awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Ordinal (goal)
Goal:
x_1 y_1 x y : ZFSet.{u}
IH :
  ∀ (a₂ b₂ : ZFSet.{u}),
    Sym2.GameAdd (fun (x1 x2 : ZFSet.{u}) ↦ x1 ∈ x2) s(a₂, b₂) s(x, y) →
      ∀ (hx : a₂.IsOrdinal) (hy : b₂.IsOrdinal), a₂ ∉ b₂ → b₂ ⊆ a₂
hx : x.IsOrdinal
hy : y.IsOrdinal
hyx : x ∉ y
z : ZFSet.{u}
hzy : z ∈ y
⊢ z ∈ x
have by_contra : ∀ (hzx : z ∉ x), False
Tactic: by_contra hzx
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Ordinal (goal)
Goal:
x y : ZFSet.{u}
hx : x.IsOrdinal
hy : y.IsOrdinal
⊢ ¬x ⊆ y ↔ y ∈ x
have rw : y ∉ x ↔ x ⊆ y
Tactic: rw [not_iff_comm, notMem_iff_subset hy hx]
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Ordinal (goal)
Goal:
x y : ZFSet.{u}
hx : x.IsOrdinal
hy : y.IsOrdinal
rw : y ∉ x ↔ x ⊆ y
⊢ ¬x ⊆ y ↔ y ∈ x
have rw₁ : x ⊆ y ↔ x ⊆ y
Tactic: rw [not_iff_comm, notMem_iff_subset hy hx]
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Ordinal (goal)
Goal:
x y : ZFSet.{u}
hx : x.IsOrdinal
hy : y.IsOrdinal
⊢ x ∈ y ∨ y ⊆ x
have rw : y ⊆ x → y ⊆ x
Tactic: rw [or_iff_not_imp_left, notMem_iff_subset hx hy]
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Ordinal (goal)
Goal:
x y : ZFSet.{u}
hx : x.IsOrdinal
hy : y.IsOrdinal
⊢ x ⊆ y ∨ y ⊆ x
have inl : ∀ (h : x ∈ y), x ⊆ y ∨ y ⊆ x
Tactic: obtain h | h := mem_or_subset hx hy
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Ordinal (goal)
Goal:
x y : ZFSet.{u}
hx : x.IsOrdinal
hy : y.IsOrdinal
inl : ∀ (h : x ∈ y), x ⊆ y ∨ y ⊆ x
⊢ x ⊆ y ∨ y ⊆ x
have inr : ∀ (h : y ⊆ x), x ⊆ y ∨ y ⊆ x
Tactic: obtain h | h := mem_or_subset hx hy
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Ordinal (goal)
Goal:
x y : ZFSet.{u}
hx : x.IsOrdinal
hy : y.IsOrdinal
⊢ x ∈ y ∨ x = y ∨ y ∈ x
have rw : x ∈ y ∨ y ⊆ x
Tactic: rw [eq_comm, ← subset_iff_eq_or_mem hy hx]
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Ordinal (goal)
Goal:
x : ZFSet.{u}
h : x.IsOrdinal
a : ZFSet.{u}
ha : a ∈ x
⊢ ∀ {b : ↥x},
    Subrel (fun (x1 x2 : ZFSet.{u}) ↦ x1 ∈ x2) (fun (x_1 : ZFSet.{u}) ↦ x_1 ∈ x)
        (Subtype.mk (p := fun (x_1 : ZFSet.{u}) ↦ x_1 ∈ x) a ha) b ∨
      Subtype.mk (p := fun (x_1 : ZFSet.{u}) ↦ x_1 ∈ x) a ha = b ∨
        Subrel (fun (x1 x2 : ZFSet.{u}) ↦ x1 ∈ x2) (fun (x_1 : ZFSet.{u}) ↦ x_1 ∈ x) b
          (Subtype.mk (p := fun (x_1 : ZFSet.{u}) ↦ x_1 ∈ x) a ha)
have this : ∀ (b : ZFSet.{u}) (hb : b ∈ x),
  Subrel (fun (x1 x2 : ZFSet.{u}) ↦ x1 ∈ x2) (fun (x_1 : ZFSet.{u}) ↦ x_1 ∈ x)
      (Subtype.mk (p := fun (x_1 : ZFSet.{u}) ↦ x_1 ∈ x) a ha)
      (Subtype.mk (p := fun (x_1 : ZFSet.{u}) ↦ x_1 ∈ x) b hb) ∨
    Subtype.mk (p := fun (x_1 : ZFSet.{u}) ↦ x_1 ∈ x) a ha = Subtype.mk (p := fun (x_1 : ZFSet.{u}) ↦ x_1 ∈ x) b hb ∨
      Subrel (fun (x1 x2 : ZFSet.{u}) ↦ x1 ∈ x2) (fun (x_1 : ZFSet.{u}) ↦ x_1 ∈ x)
        (Subtype.mk (p := fun (x_1 : ZFSet.{u}) ↦ x_1 ∈ x) b hb)
        (Subtype.mk (p := fun (x_1 : ZFSet.{u}) ↦ x_1 ∈ x) a ha)
Tactic: ⟨b, hb⟩
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Ordinal (goal)
Goal:
x : ZFSet.{u}
h₁ : x.IsTransitive
h₂ : Std.Trichotomous.{u + 2} (α := ↥x) (Subrel (fun (x1 x2 : ZFSet.{u}) ↦ x1 ∈ x2) fun (x_1 : ZFSet.{u}) ↦ x_1 ∈ x)
⊢ x.IsOrdinal
have rw : x.IsTransitive ∧ IsTrans.{u + 2} (↥x) (Subrel (fun (x1 x2 : ZFSet.{u}) ↦ x1 ∈ x2) fun (x_1 : ZFSet.{u}) ↦ x_1 ∈ x)
Tactic: rw [isOrdinal_iff_isTrans]
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Ordinal (goal)
Goal:
x : ZFSet.{u}
h₁ : x.IsTransitive
h₂ : Std.Trichotomous.{u + 2} (α := ↥x) (Subrel (fun (x1 x2 : ZFSet.{u}) ↦ x1 ∈ x2) fun (x_1 : ZFSet.{u}) ↦ x_1 ∈ x)
⊢ x.IsTransitive ∧ IsTrans.{u + 2} (↥x) (Subrel (fun (x1 x2 : ZFSet.{u}) ↦ x1 ∈ x2) fun (x_1 : ZFSet.{u}) ↦ x_1 ∈ x)
have refine : ∀ (y z w : ↥x) (hyz : Subrel (fun (x1 x2 : ZFSet.{u}) ↦ x1 ∈ x2) (fun (x_1 : ZFSet.{u}) ↦ x_1 ∈ x) y z)
  (hzw : Subrel (fun (x1 x2 : ZFSet.{u}) ↦ x1 ∈ x2) (fun (x_1 : ZFSet.{u}) ↦ x_1 ∈ x) z w),
  Subrel (fun (x1 x2 : ZFSet.{u}) ↦ x1 ∈ x2) (fun (x_1 : ZFSet.{u}) ↦ x_1 ∈ x) y w
Tactic: refine ⟨h₁, ⟨@fun y z w hyz hzw ↦ ?_⟩⟩
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Ordinal (goal)
Goal:
x : ZFSet.{u}
h₁ : x.IsTransitive
h₂ : Std.Trichotomous.{u + 2} (α := ↥x) (Subrel (fun (x1 x2 : ZFSet.{u}) ↦ x1 ∈ x2) fun (x_1 : ZFSet.{u}) ↦ x_1 ∈ x)
y z w : ↥x
hyz : Subrel (fun (x1 x2 : ZFSet.{u}) ↦ x1 ∈ x2) (fun (x_1 : ZFSet.{u}) ↦ x_1 ∈ x) y z
hzw : Subrel (fun (x1 x2 : ZFSet.{u}) ↦ x1 ∈ x2) (fun (x_1 : ZFSet.{u}) ↦ x_1 ∈ x) z w
⊢ Subrel (fun (x1 x2 : ZFSet.{u}) ↦ x1 ∈ x2) (fun (x_1 : ZFSet.{u}) ↦ x_1 ∈ x) y w
have inl : ∀ (hyw : Subrel (fun (x1 x2 : ZFSet.{u}) ↦ x1 ∈ x2) (fun (x_1 : ZFSet.{u}) ↦ x_1 ∈ x) y w),
  Subrel (fun (x1 x2 : ZFSet.{u}) ↦ x1 ∈ x2) (fun (x_1 : ZFSet.{u}) ↦ x_1 ∈ x) y w
Tactic: obtain hyw | rfl | hwy := trichotomous_of (Subrel (· ∈ ·) (· ∈ x)) y w
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Ordinal (goal)
Goal:
x : ZFSet.{u}
h₁ : x.IsTransitive
h₂ : Std.Trichotomous.{u + 2} (α := ↥x) (Subrel (fun (x1 x2 : ZFSet.{u}) ↦ x1 ∈ x2) fun (x_1 : ZFSet.{u}) ↦ x_1 ∈ x)
y z w : ↥x
hyz : Subrel (fun (x1 x2 : ZFSet.{u}) ↦ x1 ∈ x2) (fun (x_1 : ZFSet.{u}) ↦ x_1 ∈ x) y z
hzw : Subrel (fun (x1 x2 : ZFSet.{u}) ↦ x1 ∈ x2) (fun (x_1 : ZFSet.{u}) ↦ x_1 ∈ x) z w
inl :
  ∀ (hyw : Subrel (fun (x1 x2 : ZFSet.{u}) ↦ x1 ∈ x2) (fun (x_1 : ZFSet.{u}) ↦ x_1 ∈ x) y w),
    Subrel (fun (x1 x2 : ZFSet.{u}) ↦ x1 ∈ x2) (fun (x_1 : ZFSet.{u}) ↦ x_1 ∈ x) y w
⊢ Subrel (fun (x1 x2 : ZFSet.{u}) ↦ x1 ∈ x2) (fun (x_1 : ZFSet.{u}) ↦ x_1 ∈ x) y w
have inr : ∀ (hzw : Subrel (fun (x1 x2 : ZFSet.{u}) ↦ x1 ∈ x2) (fun (x_1 : ZFSet.{u}) ↦ x_1 ∈ x) z y),
  Subrel (fun (x1 x2 : ZFSet.{u}) ↦ x1 ∈ x2) (fun (x_1 : ZFSet.{u}) ↦ x_1 ∈ x) y y
Tactic: obtain hyw | rfl | hwy := trichotomous_of (Subrel (· ∈ ·) (· ∈ x)) y w
Cleared hypotheses: w, hzw
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Ordinal (goal)
Goal:
x : ZFSet.{u}
h₁ : x.IsTransitive
h₂ : Std.Trichotomous.{u + 2} (α := ↥x) (Subrel (fun (x1 x2 : ZFSet.{u}) ↦ x1 ∈ x2) fun (x_1 : ZFSet.{u}) ↦ x_1 ∈ x)
y z w : ↥x
hyz : Subrel (fun (x1 x2 : ZFSet.{u}) ↦ x1 ∈ x2) (fun (x_1 : ZFSet.{u}) ↦ x_1 ∈ x) y z
hzw : Subrel (fun (x1 x2 : ZFSet.{u}) ↦ x1 ∈ x2) (fun (x_1 : ZFSet.{u}) ↦ x_1 ∈ x) z w
inl :
  ∀ (hyw : Subrel (fun (x1 x2 : ZFSet.{u}) ↦ x1 ∈ x2) (fun (x_1 : ZFSet.{u}) ↦ x_1 ∈ x) y w),
    Subrel (fun (x1 x2 : ZFSet.{u}) ↦ x1 ∈ x2) (fun (x_1 : ZFSet.{u}) ↦ x_1 ∈ x) y w
inr :
  ∀ (hzw : Subrel (fun (x1 x2 : ZFSet.{u}) ↦ x1 ∈ x2) (fun (x_1 : ZFSet.{u}) ↦ x_1 ∈ x) z y),
    Subrel (fun (x1 x2 : ZFSet.{u}) ↦ x1 ∈ x2) (fun (x_1 : ZFSet.{u}) ↦ x_1 ∈ x) y y
⊢ Subrel (fun (x1 x2 : ZFSet.{u}) ↦ x1 ∈ x2) (fun (x_1 : ZFSet.{u}) ↦ x_1 ∈ x) y w
have inr₁ : ∀ (hwy : Subrel (fun (x1 x2 : ZFSet.{u}) ↦ x1 ∈ x2) (fun (x_1 : ZFSet.{u}) ↦ x_1 ∈ x) w y),
  Subrel (fun (x1 x2 : ZFSet.{u}) ↦ x1 ∈ x2) (fun (x_1 : ZFSet.{u}) ↦ x_1 ∈ x) y w
Tactic: obtain hyw | rfl | hwy := trichotomous_of (Subrel (· ∈ ·) (· ∈ x)) y w
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Ordinal (goal)
Goal:
x : ZFSet.{u}
⊢ x.IsOrdinal ↔
    x.IsTransitive ∧
      IsWellOrder.{u + 1} (↥x) (Subrel (fun (x1 x2 : ZFSet.{u}) ↦ x1 ∈ x2) fun (x_1 : ZFSet.{u}) ↦ x_1 ∈ x)
have mpr : x.IsTransitive ∧ IsWellOrder.{u + 1} (↥x) (Subrel (fun (x1 x2 : ZFSet.{u}) ↦ x1 ∈ x2) fun (x_1 : ZFSet.{u}) ↦ x_1 ∈ x) →
  x.IsOrdinal
Tactic: use fun h ↦ ⟨h.isTransitive, h.isWellOrder⟩
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Ordinal (goal)
Goal:
x : ZFSet.{u}
h₁ : x.IsTransitive
h₂ : IsWellOrder.{u + 1} (↥x) (Subrel (fun (x1 x2 : ZFSet.{u}) ↦ x1 ∈ x2) fun (x_1 : ZFSet.{u}) ↦ x_1 ∈ x)
⊢ x.IsOrdinal
have mpr : IsTrans.{u + 2} (↥x) (Subrel (fun (x1 x2 : ZFSet.{u}) ↦ x1 ∈ x2) fun (x_1 : ZFSet.{u}) ↦ x_1 ∈ x)
Tactic: refine isOrdinal_iff_isTrans.2 ⟨h₁, ?_⟩
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Ordinal (goal)
Goal:
x y : ZFSet.{u_1}
hx : x.IsOrdinal
hy : y.IsOrdinal
⊢ x.rank < y.rank ↔ x ∈ y
have refine : ∀ (h : x.rank < y.rank), x ∈ y
Tactic: refine ⟨fun h ↦ ?_, rank_lt_of_mem⟩
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Ordinal (goal)
Goal:
x y : ZFSet.{u_1}
hx : x.IsOrdinal
hy : y.IsOrdinal
h : x.rank < y.rank
⊢ x ∈ y
have rw : ¬y ⊆ x
Tactic: rw [← hy.not_subset_iff_mem hx]
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Ordinal (goal)
Goal:
x y : ZFSet.{u_1}
hx : x.IsOrdinal
hy : y.IsOrdinal
⊢ x.rank ≤ y.rank ↔ x ⊆ y
have rw : x.rank ≤ y.rank ↔ y ∉ x
Tactic: rw [← notMem_iff_subset hy hx, ← rank_lt_iff_mem hy hx, not_lt]
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Ordinal (goal)
Goal:
x y : ZFSet.{u_1}
hx : x.IsOrdinal
hy : y.IsOrdinal
rw : x.rank ≤ y.rank ↔ y ∉ x
⊢ x.rank ≤ y.rank ↔ x ⊆ y
have rw₁ : x.rank ≤ y.rank ↔ ¬y.rank < x.rank
Tactic: rw [← notMem_iff_subset hy hx, ← rank_lt_iff_mem hy hx, not_lt]
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Ordinal (goal)
Goal:
x y : ZFSet.{u_1}
hx : x.IsOrdinal
hy : y.IsOrdinal
rw : x.rank ≤ y.rank ↔ y ∉ x
rw₁ : x.rank ≤ y.rank ↔ ¬y.rank < x.rank
⊢ x.rank ≤ y.rank ↔ x ⊆ y
have rw₂ : x.rank ≤ y.rank ↔ x.rank ≤ y.rank
Tactic: rw [← notMem_iff_subset hy hx, ← rank_lt_iff_mem hy hx, not_lt]
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Ordinal (goal)
Goal:
x y : ZFSet.{u_1}
hx : x.IsOrdinal
hy : y.IsOrdinal
⊢ x.rank = y.rank ↔ x = y
have rw : x.rank ≤ y.rank ∧ y.rank ≤ x.rank ↔ x = y
Tactic: rw [le_antisymm_iff, subset_antisymm_iff, rank_le_iff_subset hx hy, rank_le_iff_subset hy hx]
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Ordinal (goal)
Goal:
x y : ZFSet.{u_1}
hx : x.IsOrdinal
hy : y.IsOrdinal
rw : x.rank ≤ y.rank ∧ y.rank ≤ x.rank ↔ x = y
⊢ x.rank = y.rank ↔ x = y
have rw₁ : x.rank ≤ y.rank ∧ y.rank ≤ x.rank ↔ x ⊆ y ∧ y ⊆ x
Tactic: rw [le_antisymm_iff, subset_antisymm_iff, rank_le_iff_subset hx hy, rank_le_iff_subset hy hx]
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Ordinal (goal)
Goal:
x y : ZFSet.{u_1}
hx : x.IsOrdinal
hy : y.IsOrdinal
rw : x.rank ≤ y.rank ∧ y.rank ≤ x.rank ↔ x = y
rw₁ : x.rank ≤ y.rank ∧ y.rank ≤ x.rank ↔ x ⊆ y ∧ y ⊆ x
⊢ x.rank = y.rank ↔ x = y
have rw₂ : x ⊆ y ∧ y.rank ≤ x.rank ↔ x ⊆ y ∧ y ⊆ x
Tactic: rw [le_antisymm_iff, subset_antisymm_iff, rank_le_iff_subset hx hy, rank_le_iff_subset hy hx]
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Ordinal (goal)
Goal:
x y : ZFSet.{u_1}
hx : x.IsOrdinal
hy : y.IsOrdinal
rw : x.rank ≤ y.rank ∧ y.rank ≤ x.rank ↔ x = y
rw₁ : x.rank ≤ y.rank ∧ y.rank ≤ x.rank ↔ x ⊆ y ∧ y ⊆ x
rw₂ : x ⊆ y ∧ y.rank ≤ x.rank ↔ x ⊆ y ∧ y ⊆ x
⊢ x.rank = y.rank ↔ x = y
have rw₃ : x ⊆ y ∧ y ⊆ x ↔ x ⊆ y ∧ y ⊆ x
Tactic: rw [le_antisymm_iff, subset_antisymm_iff, rank_le_iff_subset hx hy, rank_le_iff_subset hy hx]
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Ordinal (goal)
Goal:
x : ZFSet.{u_1}
h : x.IsOrdinal
⊢ IsOrdinal.{u_1} (insert x x)
have refine_1 : ∀ (y : ZFSet.{u_1}) (hy : y ∈ insert x x), y ⊆ insert x x
Tactic: refine ⟨fun y hy ↦ ?_, @fun y z w hyz hzw hw ↦ ?_⟩
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Ordinal (goal)
Goal:
x : ZFSet.{u_1}
h : x.IsOrdinal
refine_1 : ∀ (y : ZFSet.{u_1}) (hy : y ∈ insert x x), y ⊆ insert x x
⊢ IsOrdinal.{u_1} (insert x x)
have refine_2 : ∀ (y z w : ZFSet.{u_1}) (hyz : y ∈ z) (hzw : z ∈ w) (hw : w ∈ insert x x), y ∈ w
Tactic: refine ⟨fun y hy ↦ ?_, @fun y z w hyz hzw hw ↦ ?_⟩
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Ordinal (goal)
Goal:
x : ZFSet.{u_1}
h : x.IsOrdinal
y : ZFSet.{u_1}
hy : y ∈ insert x x
⊢ y ⊆ insert x x
have refine_1 : ∀ (h : y.IsOrdinal) (hy : y ∈ insert y y), y ⊆ insert y y
Tactic: obtain rfl | hy := mem_insert_iff.1 hy
Cleared hypotheses: x, h, hy
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Ordinal (goal)
Goal:
x : ZFSet.{u_1}
h : x.IsOrdinal
y : ZFSet.{u_1}
hy : y ∈ insert x x
refine_1 : ∀ (h : y.IsOrdinal) (hy : y ∈ insert y y), y ⊆ insert y y
⊢ y ⊆ insert x x
have refine_1₁ : ∀ (hy : y ∈ x), y ⊆ insert x x
Tactic: obtain rfl | hy := mem_insert_iff.1 hy
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Ordinal (goal)
Goal:
x : ZFSet.{u_1}
h : x.IsOrdinal
y : ZFSet.{u_1}
hy_1 : y ∈ insert x x
hy : y ∈ x
⊢ y ⊆ insert x x
have refine_1 : x ⊆ insert x x
Tactic: apply (h.subset_of_mem hy).trans
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Ordinal (goal)
Goal:
x : ZFSet.{u_1}
h : x.IsOrdinal
y : ZFSet.{u_1}
hy_1 : y ∈ insert x x
hy : y ∈ x
⊢ y ⊆ insert x x
have refine_1 : x ⊆ insert x x
Tactic: on_goal 2 => apply (h.subset_of_mem hy).trans
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Ordinal (goal)
Goal:
x : ZFSet.{u_1}
h : x.IsOrdinal
y z w : ZFSet.{u_1}
hyz : y ∈ z
hzw : z ∈ w
hw : w ∈ insert x x
⊢ y ∈ w
have refine_2 : ∀ (h : w.IsOrdinal) (hw : w ∈ insert w w), y ∈ w
Tactic: obtain rfl | hw := mem_insert_iff.1 hw
Cleared hypotheses: x, h, hw
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Ordinal (goal)
Goal:
x : ZFSet.{u_1}
h : x.IsOrdinal
y z w : ZFSet.{u_1}
hyz : y ∈ z
hzw : z ∈ w
hw : w ∈ insert x x
refine_2 : ∀ (h : w.IsOrdinal) (hw : w ∈ insert w w), y ∈ w
⊢ y ∈ w
have refine_2₁ : ∀ (hw : w ∈ x), y ∈ w
Tactic: obtain rfl | hw := mem_insert_iff.1 hw
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Ordinal (goal)
Goal:
o : Ordinal.{u_1}
⊢ o.toPSet.Type = o.ToType
have rw : (PSet.mk o.ToType fun (a : o.ToType) ↦ (↑a.toOrd : Ordinal.{u_1}).toPSet).Type = o.ToType
Tactic: rw [toPSet]
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Ordinal (goal)
Goal:
o : Ordinal.{u_1}
x : PSet.{u_1}
⊢ x ∈ o.toPSet ↔ ∃ a < o, x.Equiv a.toPSet
have rw : (∃ (b : (PSet.mk o.ToType fun (a : o.ToType) ↦ (↑a.toOrd : Ordinal.{u_1}).toPSet).Type),
    x.Equiv ((PSet.mk o.ToType fun (a : o.ToType) ↦ (↑a.toOrd : Ordinal.{u_1}).toPSet).Func b)) ↔
  ∃ a < o, x.Equiv a.toPSet
Tactic: rw [toPSet, PSet.mem_def]
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Ordinal (goal)
Goal:
o : Ordinal.{u_1}
⊢ o.toPSet.rank = o
have rw : ⨆ (a : o.ToType), Order.succ (↑a.toOrd : Ordinal.{u_1}).toPSet.rank = o
Tactic: rw [toPSet, PSet.rank]
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Ordinal (goal)
Goal:
o : Ordinal.{u_1}
| o
have rw : ⨆ (a : (↑(Iio o) : Type (u_1 + 1))), Order.succ (↑a : Ordinal.{u_1})
Tactic: rw [← _root_.iSup_succ o]
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Ordinal (goal)
Goal:
o : Ordinal.{u_1}
⊢ ⨆ (a : o.ToType), Order.succ (↑a.toOrd : Ordinal.{u_1}).toPSet.rank = o
have conv_rhs : Eq.{u_1 + 2} (α := Ordinal.{u_1}) (⨆ (a : o.ToType), Order.succ (↑a.toOrd : Ordinal.{u_1}).toPSet.rank)
  (⨆ (a : (↑(Iio o) : Type (u_1 + 1))), Order.succ (↑a : Ordinal.{u_1}))
Tactic: conv_rhs => rw [← _root_.iSup_succ o]
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Ordinal (goal)
Goal:
o : Ordinal.{u_1}
⊢ Eq.{u_1 + 2} (α := Ordinal.{u_1}) (⨆ (a : o.ToType), Order.succ (↑a.toOrd : Ordinal.{u_1}).toPSet.rank)
    (⨆ (a : (↑(Iio o) : Type (u_1 + 1))), Order.succ (↑a : Ordinal.{u_1}))
have h : ∀ (x : (↑(Iio o) : Type (u_1 + 1))), (↑x : Ordinal.{u_1}) = (↑x : Ordinal.{u_1}).toPSet.rank
Tactic: convert! ToType.mk.symm.iSup_comp (g := fun x ↦ Order.succ x.1.toPSet.rank)
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Ordinal (goal)
Goal:
o : Ordinal.{u_1}
x : (↑(Iio o) : Type (u_1 + 1))
⊢ (↑x : Ordinal.{u_1}) = (↑x : Ordinal.{u_1}).toPSet.rank
have h : (↑x : Ordinal.{u_1}) = (↑x : Ordinal.{u_1})
Tactic: rw [rank_toPSet]
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Ordinal (goal)
Goal:
o : Ordinal.{u_1}
x : ZFSet.{u_1}
⊢ x ∈ o.toZFSet ↔ ∃ a < o, a.toZFSet = x
have a : ∀ (a : PSet.{u_1}), ⟦a⟧ ∈ o.toZFSet ↔ ∃ a_1 < o, a_1.toZFSet = ⟦a⟧
Tactic: induction x using Quotient.ind
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Ordinal (goal)
Goal:
o : Ordinal.{u_1}
a : PSet.{u_1}
⊢ ⟦a⟧ ∈ o.toZFSet ↔ ∃ a_1 < o, a_1.toZFSet = ⟦a⟧
have a : (∃ a_1 < o, a.Equiv a_1.toPSet) ↔ ∃ a_1 < o, a_1.toZFSet = mk a
Tactic: rw [toZFSet, mk_eq, ZFSet.mk_mem_iff, mem_toPSet_iff]
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Ordinal (goal)
Goal:
o : Ordinal.{u_1}
a : PSet.{u_1}
⊢ (∃ a_1 < o, a.Equiv a_1.toPSet) ↔ ∃ a_1 < o, a_1.toZFSet = mk a
have a : ∀ (x : Ordinal.{u_1}), a.Equiv x.toPSet ↔ x.toZFSet = mk a
Tactic: congr!
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Ordinal (goal)
Goal:
o : Ordinal.{u_1}
a : PSet.{u_1}
x : Ordinal.{u_1}
⊢ a.Equiv x.toPSet ↔ x.toZFSet = mk a
have a : a.Equiv x.toPSet ↔ mk x.toPSet = mk a
Tactic: rw [toZFSet, eq, PSet.Equiv.comm]
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Ordinal (goal)
Goal:
o : Ordinal.{u_1}
a_1 : PSet.{u_1}
x : Ordinal.{u_1}
a : a_1.Equiv x.toPSet ↔ mk x.toPSet = mk a_1
⊢ a_1.Equiv x.toPSet ↔ x.toZFSet = mk a_1
have a₁ : a_1.Equiv x.toPSet ↔ x.toPSet.Equiv a_1
Tactic: rw [toZFSet, eq, PSet.Equiv.comm]
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Ordinal (goal)
Goal:
o : Ordinal.{u_1}
a_1 : PSet.{u_1}
x : Ordinal.{u_1}
a : a_1.Equiv x.toPSet ↔ mk x.toPSet = mk a_1
a₁ : a_1.Equiv x.toPSet ↔ x.toPSet.Equiv a_1
⊢ a_1.Equiv x.toPSet ↔ x.toZFSet = mk a_1
have a₂ : x.toPSet.Equiv a_1 ↔ x.toPSet.Equiv a_1
Tactic: rw [toZFSet, eq, PSet.Equiv.comm]
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Ordinal (goal)
Goal:
o : Ordinal.{u_1}
⊢ (↑o.toZFSet : Set ZFSet.{u_1}) = toZFSet '' Iio o
have h : ∀ (x : ZFSet.{u_1}), x ∈ (↑o.toZFSet : Set ZFSet.{u_1}) ↔ x ∈ toZFSet '' Iio o
Tactic: ext
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Ordinal (goal)
Goal:
a b : Ordinal.{u_1}
h : a < b
⊢ a.toZFSet ∈ b.toZFSet
have rw : ∃ a_1 < b, a_1.toZFSet = a.toZFSet
Tactic: rw [mem_toZFSet_iff]
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Ordinal (goal)
Goal:
a b : Ordinal.{u_1}
h : a ≤ b
x : ZFSet.{u_1}
hx : x ∈ a.toZFSet
⊢ x ∈ b.toZFSet
have obtain : ∀ (c : Ordinal.{u_1}) (hc : c < a) (hx : c.toZFSet ∈ a.toZFSet), c.toZFSet ∈ b.toZFSet
Tactic: obtain ⟨c, hc, rfl⟩ := mem_toZFSet_iff.1 hx
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Ordinal (goal)
Goal:
a b : Ordinal.{u_1}
⊢ a.toZFSet ∈ b.toZFSet ↔ a < b
have refine : a.toZFSet ∈ b.toZFSet → a < b
Tactic: refine ⟨?_, toZFSet_mem_toZFSet_of_lt⟩
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Ordinal (goal)
Goal:
a b : Ordinal.{u_1}
⊢ a.toZFSet ∈ b.toZFSet → a < b
have contrapose! : b ≤ a → a.toZFSet ∉ b.toZFSet
Tactic: contrapose!
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Ordinal (goal)
Goal:
a b : Ordinal.{u_1}
⊢ a.toZFSet ⊆ b.toZFSet ↔ a ≤ b
have refine : a.toZFSet ⊆ b.toZFSet → a ≤ b
Tactic: refine ⟨?_, fun h ↦ toZFSet_monotone h⟩
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Ordinal (goal)
Goal:
a b : Ordinal.{u_1}
⊢ a.toZFSet ⊆ b.toZFSet → a ≤ b
have contrapose! : b < a → ¬a.toZFSet ⊆ b.toZFSet
Tactic: contrapose!
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Ordinal (goal)
Goal:
⊢ toZFSet 0 = ∅
have a : ∀ (z : ZFSet.{u_1}), z ∈ toZFSet 0 ↔ Membership.mem (γ := ZFSet.{u_1}) ∅ z
Tactic: ext
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Ordinal (goal)
Goal:
o : Ordinal.{u_1}
⊢ IsOrdinal.{u_1} o.toZFSet
have refine_1 : ∀ (x : ZFSet.{u_1}) (hx : x ∈ o.toZFSet) (y : ZFSet.{u_1}) (hy : y ∈ x), y ∈ o.toZFSet
Tactic: refine ⟨fun x hx y hy ↦ ?_, fun {z y x} hz hy hx ↦ ?_⟩
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Ordinal (goal)
Goal:
o : Ordinal.{u_1}
refine_1 : ∀ (x : ZFSet.{u_1}) (hx : x ∈ o.toZFSet) (y : ZFSet.{u_1}) (hy : y ∈ x), y ∈ o.toZFSet
⊢ IsOrdinal.{u_1} o.toZFSet
have refine_2 : ∀ {z y x : ZFSet.{u_1}} (hz : z ∈ y) (hy : y ∈ x) (hx : x ∈ o.toZFSet), z ∈ x
Tactic: refine ⟨fun x hx y hy ↦ ?_, fun {z y x} hz hy hx ↦ ?_⟩
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Ordinal (goal)
Goal:
o : Ordinal.{u_1}
x : ZFSet.{u_1}
hx : x ∈ o.toZFSet
y : ZFSet.{u_1}
hy : y ∈ x
⊢ y ∈ o.toZFSet
have refine_1 : ∀ (a : Ordinal.{u_1}) (ha : a < o) (hx : a.toZFSet ∈ o.toZFSet) (hy : y ∈ a.toZFSet), y ∈ o.toZFSet
Tactic: obtain ⟨a, ha, rfl⟩ := mem_toZFSet_iff.1 hx
Cleared hypotheses: x, hx, hy
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Ordinal (goal)
Goal:
o : Ordinal.{u_1}
y : ZFSet.{u_1}
a : Ordinal.{u_1}
ha : a < o
hx : a.toZFSet ∈ o.toZFSet
hy : y ∈ a.toZFSet
⊢ y ∈ o.toZFSet
have refine_1 : ∀ (b : Ordinal.{u_1}) (hb : b < a) (hy : b.toZFSet ∈ a.toZFSet), b.toZFSet ∈ o.toZFSet
Tactic: obtain ⟨b, hb, rfl⟩ := mem_toZFSet_iff.1 hy
Cleared hypotheses: y, hy
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Ordinal (goal)
Goal:
o : Ordinal.{u_1}
z y x : ZFSet.{u_1}
hz : z ∈ y
hy : y ∈ x
hx : x ∈ o.toZFSet
⊢ z ∈ x
have refine_2 : ∀ (a : Ordinal.{u_1}) (ha : a < o) (hy : y ∈ a.toZFSet) (hx : a.toZFSet ∈ o.toZFSet), z ∈ a.toZFSet
Tactic: obtain ⟨a, ha, rfl⟩ := mem_toZFSet_iff.1 hx
Cleared hypotheses: x, hy, hx
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Ordinal (goal)
Goal:
o : Ordinal.{u_1}
z y : ZFSet.{u_1}
hz : z ∈ y
a : Ordinal.{u_1}
ha : a < o
hy : y ∈ a.toZFSet
hx : a.toZFSet ∈ o.toZFSet
⊢ z ∈ a.toZFSet
have refine_2 : ∀ (b : Ordinal.{u_1}) (hb : b < a) (hz : z ∈ b.toZFSet) (hy : b.toZFSet ∈ a.toZFSet), z ∈ a.toZFSet
Tactic: obtain ⟨b, hb, rfl⟩ := mem_toZFSet_iff.1 hy
Cleared hypotheses: y, hz, hy
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Ordinal (goal)
Goal:
o : Ordinal.{u_1}
z : ZFSet.{u_1}
a : Ordinal.{u_1}
ha : a < o
hx : a.toZFSet ∈ o.toZFSet
b : Ordinal.{u_1}
hb : b < a
hz : z ∈ b.toZFSet
hy : b.toZFSet ∈ a.toZFSet
⊢ z ∈ a.toZFSet
have refine_2 : ∀ (c : Ordinal.{u_1}) (hc : c < b) (hz : c.toZFSet ∈ b.toZFSet), c.toZFSet ∈ a.toZFSet
Tactic: obtain ⟨c, hc, rfl⟩ := mem_toZFSet_iff.1 hz
Cleared hypotheses: z, hz
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Ordinal (goal)
Goal:
x : ZFSet.{u}
⊢ x.IsOrdinal ↔ x ∈ Set.range toZFSet
have refine_1 : ∀ (h : x.IsOrdinal), x ∈ Set.range toZFSet
Tactic: refine ⟨fun h ↦ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Ordinal (goal)
Goal:
x : ZFSet.{u}
refine_1 : ∀ (h : x.IsOrdinal), x ∈ Set.range toZFSet
⊢ x.IsOrdinal ↔ x ∈ Set.range toZFSet
have refine_2 : x ∈ Set.range toZFSet → x.IsOrdinal
Tactic: refine ⟨fun h ↦ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.Ordinal (goal)
Goal:
x : ZFSet.{u}
h : x.IsOrdinal
⊢ x ∈ Set.range toZFSet
have refine_1 : x.rank.toZFSet ∈ Set.range toZFSet
Tactic: rw [← h.toZFSet_rank_eq]
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.PSet (goal)
Goal:
x y z : PSet.{u_1}
hxy : x ⊆ y
hyz : y ⊆ z
a : x.Type
⊢ ∃ (b : z.Type), Equiv.{u_1, u_1} (x.Func a) (z.Func b)
have obtain : ∀ (b : y.Type) (hb : Equiv.{u_1, u_1} (x.Func a) (y.Func b)), ∃ (b : z.Type), Equiv.{u_1, u_1} (x.Func a) (z.Func b)
Tactic: obtain ⟨b, hb⟩ := hxy a
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.PSet (goal)
Goal:
x y z : PSet.{u_1}
hxy : x ⊆ y
hyz : y ⊆ z
a : x.Type
b : y.Type
hb : Equiv.{u_1, u_1} (x.Func a) (y.Func b)
⊢ ∃ (b : z.Type), Equiv.{u_1, u_1} (x.Func a) (z.Func b)
have obtain : ∀ (c : z.Type) (hc : Equiv.{u_1, u_1} (y.Func b) (z.Func c)), ∃ (b : z.Type), Equiv.{u_1, u_1} (x.Func a) (z.Func b)
Tactic: obtain ⟨c, hc⟩ := hyz b
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.PSet (goal)
Goal:
α : Type u
A : α → PSet.{u}
β : Type u
B : β → PSet.{u}
H : Equiv.{u, u} (mk α A) (mk β B)
γ : Type u
C : γ → PSet.{u}
b : (mk β B).Type
hc : Equiv.{u, u} (mk γ C) ((mk β B).Func b)
⊢ Acc (fun (x1 x2 : PSet.{u}) ↦ x1 ∈ x2) (mk γ C)
have obtain : ∀ (a : (mk α A).Type) (ha : Equiv.{u, u} ((mk α A).Func a) ((mk β B).Func b)),
  Acc (fun (x1 x2 : PSet.{u}) ↦ x1 ∈ x2) (mk γ C)
Tactic: obtain ⟨a, ha⟩ := H.exists_right b
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.PSet (hypothesis)
Goal:
α : Type u
A : α → PSet.{u}
β : Type u
B : β → PSet.{u}
H : Equiv.{u, u} (mk α A) (mk β B)
γ : Type u
C : γ → PSet.{u}
b : (mk β B).Type
hc : Equiv.{u, u} (mk γ C) ((mk β B).Func b)
a : (mk α A).Type
ha : Equiv.{u, u} ((mk α A).Func a) ((mk β B).Func b)
⊢ Acc (fun (x1 x2 : PSet.{u}) ↦ x1 ∈ x2) (mk γ C)
have H₁ : Equiv.{u, u} ((mk α A).Func a) (mk γ C)
Tactic: have H := ha.trans hc.symm
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.PSet (hypothesis)
Goal:
α : Type u
A : α → PSet.{u}
β : Type u
B : β → PSet.{u}
H_1 : Equiv.{u, u} (mk α A) (mk β B)
γ : Type u
C : γ → PSet.{u}
b : (mk β B).Type
hc : Equiv.{u, u} (mk γ C) ((mk β B).Func b)
a : (mk α A).Type
ha : Equiv.{u, u} ((mk α A).Func a) ((mk β B).Func b)
H : Equiv.{u, u} ((mk α A).Func a) (mk γ C)
⊢ Acc (fun (x1 x2 : PSet.{u}) ↦ x1 ∈ x2) (mk γ C)
have H₁ : Equiv.{u, u} (A a) (mk γ C)
Tactic: rw [mk_func] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.SetTheory.ZFC.PSet (goal)
Goal:
α : Type u
A : α → PSet.{u}
y : PSet.{u}
h : y ∈ ⋃₀ mk α A
a : (mk α A).Type
c : ((mk α A).Func a).Type
e : y.Equiv ((A a).Func c)
this : (A a).Func c ∈ mk (A a).Type (A a).Func
⊢ (A a).Func c ∈ A a
have rwa : ∀ (this : (A a).Func c ∈ A a), (A a).Func c ∈ A a
Tactic: rwa [eta] at this