awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Aleph (goal)
Goal:
o : Ordinal.{u_1}
ho : IsSuccLimit o
a : Ordinal.{u_1}
ha : ∀ b < o, (preOmega : (a : Ordinal.{u_1}) → Ordinal.{u_1}) b ≤ a
b : Ordinal.{u_1}
hb : b < o
⊢ card ((preOmega : (a : Ordinal.{u_1}) → Ordinal.{u_1}) b) <
    card ((preOmega : (a : Ordinal.{u_1}) → Ordinal.{u_1}) (succ b))
have rw : b < succ b
Tactic: rw [(isInitial_preOmega _).card_lt_card, preOmega_lt_preOmega]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Aleph (goal)
Goal:
x : Ordinal.{u_1}
⊢ Membership.mem (γ := Set Ordinal.{u_1}) (range (ι := Ordinal.{u_1}) (⇑preOmega : (a : Ordinal.{u_1}) → Ordinal.{u_1}))
      x ↔
    x.IsInitial
have rw : Membership.mem (γ := Set Ordinal.{u_1}) {x : Ordinal.{u_1} | x.IsInitial} x ↔ x.IsInitial
Tactic: rw [range_preOmega, mem_setOf]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Aleph (goal)
Goal:
x : Ordinal.{u_1}
rw : Membership.mem (γ := Set Ordinal.{u_1}) {x : Ordinal.{u_1} | x.IsInitial} x ↔ x.IsInitial
⊢ Membership.mem (γ := Set Ordinal.{u_1}) (range (ι := Ordinal.{u_1}) (⇑preOmega : (a : Ordinal.{u_1}) → Ordinal.{u_1}))
      x ↔
    x.IsInitial
have rw₁ : x.IsInitial ↔ x.IsInitial
Tactic: rw [range_preOmega, mem_setOf]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Aleph (goal)
Goal:
⊢ (preOmega : (a : Ordinal.{u_1}) → Ordinal.{u_1}) ω = ω
have simp_rw : ⨆ (n : ℕ), (preOmega : (a : Ordinal.{u_1}) → Ordinal.{u_1}) (↑n : Ordinal.{u_1}) = ω
Tactic: simp_rw [← apply_omega0_of_isNormal isNormal_preOmega, preOmega_natCast, iSup_natCast]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Aleph (goal)
Goal:
simp_rw : ⨆ (n : ℕ), (preOmega : (a : Ordinal.{u_1}) → Ordinal.{u_1}) (↑n : Ordinal.{u_1}) = ω
⊢ (preOmega : (a : Ordinal.{u_1}) → Ordinal.{u_1}) ω = ω
have simp_rw₁ : ⨆ (n : ℕ), (↑n : Ordinal.{u_1}) = ω
Tactic: simp_rw [← apply_omega0_of_isNormal isNormal_preOmega, preOmega_natCast, iSup_natCast]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Aleph (goal)
Goal:
x : Ordinal.{u_1}
| ω ≤ (preOmega : (a : Ordinal.{u_1}) → Ordinal.{u_1}) x
have rw : ω ≤ x
Tactic: rw [← preOmega_omega0, preOmega_le_preOmega]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Aleph (goal)
Goal:
x : Ordinal.{u_1}
⊢ ω ≤ (preOmega : (a : Ordinal.{u_1}) → Ordinal.{u_1}) x ↔ ω ≤ x
have conv_lhs : ω ≤ (preOmega : (a : Ordinal.{u_1}) → Ordinal.{u_1}) x ↔ ω ≤ x
Tactic: conv_lhs => rw [← preOmega_omega0, preOmega_le_preOmega]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Aleph (goal)
Goal:
x : Ordinal.{u_1}
conv_lhs : ω ≤ (preOmega : (a : Ordinal.{u_1}) → Ordinal.{u_1}) x ↔ ω ≤ x
⊢ ω ≤ (preOmega : (a : Ordinal.{u_1}) → Ordinal.{u_1}) x ↔ ω ≤ x
have conv_lhs₁ : ω ≤ x ↔ ω ≤ x
Tactic: conv_lhs => rw [← preOmega_omega0, preOmega_le_preOmega]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Aleph (goal)
Goal:
x : Ordinal.{u_1}
| ω < (preOmega : (a : Ordinal.{u_1}) → Ordinal.{u_1}) x
have rw : ω < x
Tactic: rw [← preOmega_omega0, preOmega_lt_preOmega]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Aleph (goal)
Goal:
x : Ordinal.{u_1}
⊢ ω < (preOmega : (a : Ordinal.{u_1}) → Ordinal.{u_1}) x ↔ ω < x
have conv_lhs : ω < (preOmega : (a : Ordinal.{u_1}) → Ordinal.{u_1}) x ↔ ω < x
Tactic: conv_lhs => rw [← preOmega_omega0, preOmega_lt_preOmega]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Aleph (goal)
Goal:
x : Ordinal.{u_1}
conv_lhs : ω < (preOmega : (a : Ordinal.{u_1}) → Ordinal.{u_1}) x ↔ ω < x
⊢ ω < (preOmega : (a : Ordinal.{u_1}) → Ordinal.{u_1}) x ↔ ω < x
have conv_lhs₁ : ω < x ↔ ω < x
Tactic: conv_lhs => rw [← preOmega_omega0, preOmega_lt_preOmega]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Aleph (goal)
Goal:
⊢ (ω_ : (a : Ordinal.{u_1}) → Ordinal.{u_1}) 0 = ω
have rw : (preOmega : (a : Ordinal.{u_1}) → Ordinal.{u_1}) (ω + 0) = ω
Tactic: rw [omega_eq_preOmega, add_zero, preOmega_omega0]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Aleph (goal)
Goal:
rw : (preOmega : (a : Ordinal.{u_1}) → Ordinal.{u_1}) (ω + 0) = ω
⊢ (ω_ : (a : Ordinal.{u_1}) → Ordinal.{u_1}) 0 = ω
have rw₁ : (preOmega : (a : Ordinal.{u_1}) → Ordinal.{u_1}) ω = ω
Tactic: rw [omega_eq_preOmega, add_zero, preOmega_omega0]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Aleph (goal)
Goal:
rw : (preOmega : (a : Ordinal.{u_1}) → Ordinal.{u_1}) (ω + 0) = ω
rw₁ : (preOmega : (a : Ordinal.{u_1}) → Ordinal.{u_1}) ω = ω
⊢ (ω_ : (a : Ordinal.{u_1}) → Ordinal.{u_1}) 0 = ω
have rw₂ : ω = ω
Tactic: rw [omega_eq_preOmega, add_zero, preOmega_omega0]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Aleph (goal)
Goal:
o : Ordinal.{u_1}
⊢ ω ≤ (ω_ : (a : Ordinal.{u_1}) → Ordinal.{u_1}) o
have rw : 0 ≤ o
Tactic: rw [← omega_zero, omega_le_omega]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Aleph (goal)
Goal:
⊢ ω < (ω_ : (a : Ordinal.{u_1}) → Ordinal.{u_1}) 1
have rw : LT.lt.{u_1 + 1} (α := Ordinal.{u_1}) 0 1
Tactic: rw [← omega_zero, omega_lt_omega]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Aleph (goal)
Goal:
⊢ Eq (α := Set Ordinal.{u_1}) (range (ι := Ordinal.{u_1}) (⇑ω_ : (a : Ordinal.{u_1}) → Ordinal.{u_1}))
    {x : Ordinal.{u_1} | ω ≤ x ∧ x.IsInitial}
have h : ∀ (x : Ordinal.{u_1}),
  Membership.mem (γ := Set Ordinal.{u_1}) (range (ι := Ordinal.{u_1}) (⇑ω_ : (a : Ordinal.{u_1}) → Ordinal.{u_1})) x ↔
    Membership.mem (γ := Set Ordinal.{u_1}) {x : Ordinal.{u_1} | ω ≤ x ∧ x.IsInitial} x
Tactic: ext x
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Aleph (goal)
Goal:
x : Ordinal.{u_1}
⊢ Membership.mem (γ := Set Ordinal.{u_1}) (range (ι := Ordinal.{u_1}) (⇑ω_ : (a : Ordinal.{u_1}) → Ordinal.{u_1})) x ↔
    Membership.mem (γ := Set Ordinal.{u_1}) {x : Ordinal.{u_1} | ω ≤ x ∧ x.IsInitial} x
have h : Membership.mem (γ := Set Ordinal.{u_1}) (range (ι := Ordinal.{u_1}) (⇑ω_ : (a : Ordinal.{u_1}) → Ordinal.{u_1})) x →
  Membership.mem (γ := Set Ordinal.{u_1}) {x : Ordinal.{u_1} | ω ≤ x ∧ x.IsInitial} x
Tactic: constructor
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Aleph (goal)
Goal:
x : Ordinal.{u_1}
h :
  Membership.mem (γ := Set Ordinal.{u_1}) (range (ι := Ordinal.{u_1}) (⇑ω_ : (a : Ordinal.{u_1}) → Ordinal.{u_1})) x →
    Membership.mem (γ := Set Ordinal.{u_1}) {x : Ordinal.{u_1} | ω ≤ x ∧ x.IsInitial} x
⊢ Membership.mem (γ := Set Ordinal.{u_1}) (range (ι := Ordinal.{u_1}) (⇑ω_ : (a : Ordinal.{u_1}) → Ordinal.{u_1})) x ↔
    Membership.mem (γ := Set Ordinal.{u_1}) {x : Ordinal.{u_1} | ω ≤ x ∧ x.IsInitial} x
have h₁ : Membership.mem (γ := Set Ordinal.{u_1}) {x : Ordinal.{u_1} | ω ≤ x ∧ x.IsInitial} x →
  Membership.mem (γ := Set Ordinal.{u_1}) (range (ι := Ordinal.{u_1}) (⇑ω_ : (a : Ordinal.{u_1}) → Ordinal.{u_1})) x
Tactic: constructor
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Aleph (goal)
Goal:
x : Ordinal.{u_1}
ha' : ω ≤ x
ha : x.IsInitial
⊢ Membership.mem (γ := Set Ordinal.{u_1}) (range (ι := Ordinal.{u_1}) (⇑ω_ : (a : Ordinal.{u_1}) → Ordinal.{u_1})) x
have h : ∀ (a : Ordinal.{u_1}) (ha' : ω ≤ (preOmega : (a : Ordinal.{u_1}) → Ordinal.{u_1}) a)
  (ha : IsInitial.{u_1} ((preOmega : (a : Ordinal.{u_1}) → Ordinal.{u_1}) a)),
  Membership.mem (α := Ordinal.{u_1}) (γ := Set Ordinal.{u_1})
    (range (ι := Ordinal.{u_1}) (⇑ω_ : (a : Ordinal.{u_1}) → Ordinal.{u_1}))
    ((preOmega : (a : Ordinal.{u_1}) → Ordinal.{u_1}) a : Ordinal.{u_1})
Tactic: obtain ⟨a, rfl⟩ := ha.mem_range_preOmega
Cleared hypotheses: x, ha', ha
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Aleph (goal)
Goal:
a : Ordinal.{u_1}
ha' : ω ≤ (preOmega : (a : Ordinal.{u_1}) → Ordinal.{u_1}) a
ha : IsInitial.{u_1} ((preOmega : (a : Ordinal.{u_1}) → Ordinal.{u_1}) a)
⊢ Membership.mem (α := Ordinal.{u_1}) (γ := Set Ordinal.{u_1})
    (range (ι := Ordinal.{u_1}) (⇑ω_ : (a : Ordinal.{u_1}) → Ordinal.{u_1}))
    ((preOmega : (a : Ordinal.{u_1}) → Ordinal.{u_1}) a : Ordinal.{u_1})
have h : Eq (α := Ordinal.{u_1}) ((ω_ : (a : Ordinal.{u_1}) → Ordinal.{u_1}) (a - ω) : Ordinal.{u_1})
  ((preOmega : (a : Ordinal.{u_1}) → Ordinal.{u_1}) a : Ordinal.{u_1})
Tactic: use a - ω
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Aleph (hypothesis)
Goal:
a : Ordinal.{u_1}
ha' : ω ≤ (preOmega : (a : Ordinal.{u_1}) → Ordinal.{u_1}) a
ha : IsInitial.{u_1} ((preOmega : (a : Ordinal.{u_1}) → Ordinal.{u_1}) a)
⊢ Eq (α := Ordinal.{u_1}) ((ω_ : (a : Ordinal.{u_1}) → Ordinal.{u_1}) (a - ω) : Ordinal.{u_1})
    ((preOmega : (a : Ordinal.{u_1}) → Ordinal.{u_1}) a : Ordinal.{u_1})
have ha'₁ : ω ≤ a
Tactic: rw [omega0_le_preOmega_iff] at ha'
Cleared hypotheses: ha', ha
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Aleph (goal)
Goal:
a : Ordinal.{u_1}
ha' : ω ≤ a
ha : IsInitial.{u_1} ((preOmega : (a : Ordinal.{u_1}) → Ordinal.{u_1}) a)
⊢ Eq (α := Ordinal.{u_1}) ((ω_ : (a : Ordinal.{u_1}) → Ordinal.{u_1}) (a - ω) : Ordinal.{u_1})
    ((preOmega : (a : Ordinal.{u_1}) → Ordinal.{u_1}) a : Ordinal.{u_1})
have h : Eq (α := Ordinal.{u_1}) ((preOmega : (a : Ordinal.{u_1}) → Ordinal.{u_1}) (ω + (a - ω)) : Ordinal.{u_1})
  ((preOmega : (a : Ordinal.{u_1}) → Ordinal.{u_1}) a : Ordinal.{u_1})
Tactic: rw [omega_eq_preOmega, Ordinal.add_sub_cancel_of_le ha']
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Aleph (goal)
Goal:
a : Ordinal.{u_1}
ha' : ω ≤ a
ha : IsInitial.{u_1} ((preOmega : (a : Ordinal.{u_1}) → Ordinal.{u_1}) a)
h :
  Eq (α := Ordinal.{u_1}) ((preOmega : (a : Ordinal.{u_1}) → Ordinal.{u_1}) (ω + (a - ω)) : Ordinal.{u_1})
    ((preOmega : (a : Ordinal.{u_1}) → Ordinal.{u_1}) a : Ordinal.{u_1})
⊢ Eq (α := Ordinal.{u_1}) ((ω_ : (a : Ordinal.{u_1}) → Ordinal.{u_1}) (a - ω) : Ordinal.{u_1})
    ((preOmega : (a : Ordinal.{u_1}) → Ordinal.{u_1}) a : Ordinal.{u_1})
have h₁ : Eq (α := Ordinal.{u_1}) ((preOmega : (a : Ordinal.{u_1}) → Ordinal.{u_1}) a : Ordinal.{u_1})
  ((preOmega : (a : Ordinal.{u_1}) → Ordinal.{u_1}) a : Ordinal.{u_1})
Tactic: rw [omega_eq_preOmega, Ordinal.add_sub_cancel_of_le ha']
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Aleph (goal)
Goal:
x : Ordinal.{u_1}
⊢ Membership.mem (γ := Set Ordinal.{u_1}) (range (ι := Ordinal.{u_1}) (⇑ω_ : (a : Ordinal.{u_1}) → Ordinal.{u_1})) x ↔
    ω ≤ x ∧ x.IsInitial
have rw : Membership.mem (γ := Set Ordinal.{u_1}) {x : Ordinal.{u_1} | ω ≤ x ∧ x.IsInitial} x ↔ ω ≤ x ∧ x.IsInitial
Tactic: rw [range_omega, mem_setOf]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Aleph (goal)
Goal:
x : Ordinal.{u_1}
rw : Membership.mem (γ := Set Ordinal.{u_1}) {x : Ordinal.{u_1} | ω ≤ x ∧ x.IsInitial} x ↔ ω ≤ x ∧ x.IsInitial
⊢ Membership.mem (γ := Set Ordinal.{u_1}) (range (ι := Ordinal.{u_1}) (⇑ω_ : (a : Ordinal.{u_1}) → Ordinal.{u_1})) x ↔
    ω ≤ x ∧ x.IsInitial
have rw₁ : ω ≤ x ∧ x.IsInitial ↔ ω ≤ x ∧ x.IsInitial
Tactic: rw [range_omega, mem_setOf]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Aleph (hypothesis)
Goal:
o : Ordinal.{u_1}
ho : HPow.hPow (β := ℕ) ω 2 ≤ o
⊢ Eq (α := Ordinal.{u_1}) ((preOmega : (a : Ordinal.{u_1}) → Ordinal.{u_1}) o : Ordinal.{u_1})
    ((ω_ : (a : Ordinal.{u_1}) → Ordinal.{u_1}) o : Ordinal.{u_1})
have ho₁ : HPow.hPow (β := Ordinal.{u_1}) ω (↑2 : Ordinal.{u_1}) ≤ o
Tactic: rw [← opow_natCast] at ho
Cleared hypotheses: ho
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Aleph (goal)
Goal:
o : Ordinal.{u_1}
ho : HPow.hPow (β := Ordinal.{u_1}) ω (↑2 : Ordinal.{u_1}) ≤ o
⊢ Eq (α := Ordinal.{u_1}) ((preOmega : (a : Ordinal.{u_1}) → Ordinal.{u_1}) o : Ordinal.{u_1})
    ((ω_ : (a : Ordinal.{u_1}) → Ordinal.{u_1}) o : Ordinal.{u_1})
have rw : ω < HPow.hPow (β := Ordinal.{u_1}) ω (↑2 : Ordinal.{u_1})
Tactic: rw [omega_eq_preOmega, add_of_omega0_opow_le _ ho]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Aleph (goal)
Goal:
o : Ordinal.{u_1}
ho : HPow.hPow (β := Ordinal.{u_1}) ω (↑2 : Ordinal.{u_1}) ≤ o
⊢ ω < HPow.hPow (β := Ordinal.{u_1}) ω (↑2 : Ordinal.{u_1})
have apply : LT.lt.{u_1 + 1} (α := Ordinal.{u_1}) 1 (↑2 : Ordinal.{u_1})
Tactic: apply left_lt_opow one_lt_omega0
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Aleph (goal)
Goal:
o : Ordinal.{u_1}
⊢ ord ((preAleph : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o) = (preOmega : (a : Ordinal.{u_1}) → Ordinal.{u_1}) o
have rw : (card ((preOmega : (a : Ordinal.{u_1}) → Ordinal.{u_1}) o)).ord = (preOmega : (a : Ordinal.{u_1}) → Ordinal.{u_1}) o
Tactic: rw [← o.card_preOmega, (isInitial_preOmega o).ord_card]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Aleph (goal)
Goal:
o : Ordinal.{u_1}
rw :
  (card ((preOmega : (a : Ordinal.{u_1}) → Ordinal.{u_1}) o)).ord = (preOmega : (a : Ordinal.{u_1}) → Ordinal.{u_1}) o
⊢ ord ((preAleph : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o) = (preOmega : (a : Ordinal.{u_1}) → Ordinal.{u_1}) o
have rw₁ : Eq (α := Ordinal.{u_1}) ((preOmega : (a : Ordinal.{u_1}) → Ordinal.{u_1}) o : Ordinal.{u_1})
  ((preOmega : (a : Ordinal.{u_1}) → Ordinal.{u_1}) o : Ordinal.{u_1})
Tactic: rw [← o.card_preOmega, (isInitial_preOmega o).ord_card]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Aleph (goal)
Goal:
n : ℕ
⊢ Eq (α := Cardinal.{u_1}) ((preAleph : (a : Ordinal.{u_1}) → Cardinal.{u_1}) (↑n : Ordinal.{u_1}))
    (↑n : Cardinal.{u_1})
have rw : card ((preOmega : (a : Ordinal.{u_1}) → Ordinal.{u_1}) (↑n : Ordinal.{u_1})) = (↑n : Cardinal.{u_1})
Tactic: rw [← card_preOmega, preOmega_natCast, card_nat]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Aleph (goal)
Goal:
n : ℕ
rw : card ((preOmega : (a : Ordinal.{u_1}) → Ordinal.{u_1}) (↑n : Ordinal.{u_1})) = (↑n : Cardinal.{u_1})
⊢ Eq (α := Cardinal.{u_1}) ((preAleph : (a : Ordinal.{u_1}) → Cardinal.{u_1}) (↑n : Ordinal.{u_1}))
    (↑n : Cardinal.{u_1})
have rw₁ : card (↑n : Ordinal.{u_1}) = (↑n : Cardinal.{u_1})
Tactic: rw [← card_preOmega, preOmega_natCast, card_nat]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Aleph (goal)
Goal:
n : ℕ
rw : card ((preOmega : (a : Ordinal.{u_1}) → Ordinal.{u_1}) (↑n : Ordinal.{u_1})) = (↑n : Cardinal.{u_1})
rw₁ : card (↑n : Ordinal.{u_1}) = (↑n : Cardinal.{u_1})
⊢ Eq (α := Cardinal.{u_1}) ((preAleph : (a : Ordinal.{u_1}) → Cardinal.{u_1}) (↑n : Ordinal.{u_1}))
    (↑n : Cardinal.{u_1})
have rw₂ : Eq.{u_1 + 2} (α := Cardinal.{u_1}) (↑n : Cardinal.{u_1}) (↑n : Cardinal.{u_1})
Tactic: rw [← card_preOmega, preOmega_natCast, card_nat]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Aleph (goal)
Goal:
⊢ (preAleph : (a : Ordinal.{u_1}) → Cardinal.{u_1}) ω = ℵ₀
have rw : card ((preOmega : (a : Ordinal.{u_1}) → Ordinal.{u_1}) ω) = ℵ₀
Tactic: rw [← card_preOmega, preOmega_omega0, card_omega0]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Aleph (goal)
Goal:
rw : card ((preOmega : (a : Ordinal.{u_1}) → Ordinal.{u_1}) ω) = ℵ₀
⊢ (preAleph : (a : Ordinal.{u_1}) → Cardinal.{u_1}) ω = ℵ₀
have rw₁ : ω.card = ℵ₀
Tactic: rw [← card_preOmega, preOmega_omega0, card_omega0]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Aleph (goal)
Goal:
rw : card ((preOmega : (a : Ordinal.{u_1}) → Ordinal.{u_1}) ω) = ℵ₀
rw₁ : ω.card = ℵ₀
⊢ (preAleph : (a : Ordinal.{u_1}) → Cardinal.{u_1}) ω = ℵ₀
have rw₂ : ℵ₀ = ℵ₀
Tactic: rw [← card_preOmega, preOmega_omega0, card_omega0]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Aleph (goal)
Goal:
o : Ordinal.{u_1}
⊢ LT.lt (α := Cardinal.{u_1}) (0 : Cardinal.{u_1})
      ((preAleph : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o : Cardinal.{u_1}) ↔
    0 < o
have rw : LT.lt (α := Cardinal.{u_1}) ((preAleph : (a : Ordinal.{u_1}) → Cardinal.{u_1}) 0 : Cardinal.{u_1})
    ((preAleph : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o : Cardinal.{u_1}) ↔
  0 < o
Tactic: rw [← preAleph_zero, preAleph_lt_preAleph]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Aleph (goal)
Goal:
o : Ordinal.{u_1}
rw :
  LT.lt (α := Cardinal.{u_1}) ((preAleph : (a : Ordinal.{u_1}) → Cardinal.{u_1}) 0 : Cardinal.{u_1})
      ((preAleph : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o : Cardinal.{u_1}) ↔
    0 < o
⊢ LT.lt (α := Cardinal.{u_1}) (0 : Cardinal.{u_1})
      ((preAleph : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o : Cardinal.{u_1}) ↔
    0 < o
have rw₁ : 0 < o ↔ 0 < o
Tactic: rw [← preAleph_zero, preAleph_lt_preAleph]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Aleph (goal)
Goal:
o : Ordinal.{u_1}
⊢ ℵ₀ ≤ (preAleph : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o ↔ ω ≤ o
have rw : LE.le (α := Cardinal.{u_1}) ((preAleph : (a : Ordinal.{u_1}) → Cardinal.{u_1}) ω : Cardinal.{u_1})
    ((preAleph : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o : Cardinal.{u_1}) ↔
  ω ≤ o
Tactic: rw [← preAleph_omega0, preAleph_le_preAleph]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Aleph (goal)
Goal:
o : Ordinal.{u_1}
rw :
  LE.le (α := Cardinal.{u_1}) ((preAleph : (a : Ordinal.{u_1}) → Cardinal.{u_1}) ω : Cardinal.{u_1})
      ((preAleph : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o : Cardinal.{u_1}) ↔
    ω ≤ o
⊢ ℵ₀ ≤ (preAleph : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o ↔ ω ≤ o
have rw₁ : ω ≤ o ↔ ω ≤ o
Tactic: rw [← preAleph_omega0, preAleph_le_preAleph]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Aleph (goal)
Goal:
o : Ordinal.{u}
⊢ Ordinal.lift.{v, u} ((preOmega : (a : Ordinal.{u}) → Ordinal.{u}) o) =
    (preOmega : (a : Ordinal.{max v u}) → Ordinal.{max v u}) (Ordinal.lift.{v, u} o)
have rw : Ordinal.lift.{v, u} (ord ((preAleph : (a : Ordinal.{u}) → Cardinal.{u}) o)) =
  (preOmega : (a : Ordinal.{max v u}) → Ordinal.{max v u}) (Ordinal.lift.{v, u} o)
Tactic: rw [← ord_preAleph, lift_ord, lift_preAleph, ord_preAleph]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Aleph (goal)
Goal:
o : Ordinal.{u}
rw :
  Ordinal.lift.{v, u} (ord ((preAleph : (a : Ordinal.{u}) → Cardinal.{u}) o)) =
    (preOmega : (a : Ordinal.{max v u}) → Ordinal.{max v u}) (Ordinal.lift.{v, u} o)
⊢ Ordinal.lift.{v, u} ((preOmega : (a : Ordinal.{u}) → Ordinal.{u}) o) =
    (preOmega : (a : Ordinal.{max v u}) → Ordinal.{max v u}) (Ordinal.lift.{v, u} o)
have rw₁ : (lift.{v, u} ((preAleph : (a : Ordinal.{u}) → Cardinal.{u}) o)).ord =
  (preOmega : (a : Ordinal.{max v u}) → Ordinal.{max v u}) (Ordinal.lift.{v, u} o)
Tactic: rw [← ord_preAleph, lift_ord, lift_preAleph, ord_preAleph]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Aleph (goal)
Goal:
o : Ordinal.{u}
rw :
  Ordinal.lift.{v, u} (ord ((preAleph : (a : Ordinal.{u}) → Cardinal.{u}) o)) =
    (preOmega : (a : Ordinal.{max v u}) → Ordinal.{max v u}) (Ordinal.lift.{v, u} o)
rw₁ :
  (lift.{v, u} ((preAleph : (a : Ordinal.{u}) → Cardinal.{u}) o)).ord =
    (preOmega : (a : Ordinal.{max v u}) → Ordinal.{max v u}) (Ordinal.lift.{v, u} o)
⊢ Ordinal.lift.{v, u} ((preOmega : (a : Ordinal.{u}) → Ordinal.{u}) o) =
    (preOmega : (a : Ordinal.{max v u}) → Ordinal.{max v u}) (Ordinal.lift.{v, u} o)
have rw₂ : ord ((preAleph : (a : Ordinal.{max v u}) → Cardinal.{max v u}) (Ordinal.lift.{v, u} o)) =
  (preOmega : (a : Ordinal.{max v u}) → Ordinal.{max v u}) (Ordinal.lift.{v, u} o)
Tactic: rw [← ord_preAleph, lift_ord, lift_preAleph, ord_preAleph]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Aleph (goal)
Goal:
o : Ordinal.{u}
rw :
  Ordinal.lift.{v, u} (ord ((preAleph : (a : Ordinal.{u}) → Cardinal.{u}) o)) =
    (preOmega : (a : Ordinal.{max v u}) → Ordinal.{max v u}) (Ordinal.lift.{v, u} o)
rw₁ :
  (lift.{v, u} ((preAleph : (a : Ordinal.{u}) → Cardinal.{u}) o)).ord =
    (preOmega : (a : Ordinal.{max v u}) → Ordinal.{max v u}) (Ordinal.lift.{v, u} o)
rw₂ :
  ord ((preAleph : (a : Ordinal.{max v u}) → Cardinal.{max v u}) (Ordinal.lift.{v, u} o)) =
    (preOmega : (a : Ordinal.{max v u}) → Ordinal.{max v u}) (Ordinal.lift.{v, u} o)
⊢ Ordinal.lift.{v, u} ((preOmega : (a : Ordinal.{u}) → Ordinal.{u}) o) =
    (preOmega : (a : Ordinal.{max v u}) → Ordinal.{max v u}) (Ordinal.lift.{v, u} o)
have rw₃ : Eq (α := Ordinal.{max u v})
  ((preOmega : (a : Ordinal.{max u v}) → Ordinal.{max u v}) (Ordinal.lift.{v, u} o) : Ordinal.{max u v})
  ((preOmega : (a : Ordinal.{max v u}) → Ordinal.{max v u}) (Ordinal.lift.{v, u} o) : Ordinal.{max v u})
Tactic: rw [← ord_preAleph, lift_ord, lift_preAleph, ord_preAleph]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Aleph (goal)
Goal:
o : Ordinal.{u_1}
l : IsSuccPrelimit o
c : Cardinal.{u_1}
⊢ (preAleph : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o ≤ c ↔
    ∀ o' < o, (preAleph : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o' ≤ c
have inl : ∀ (l : IsSuccPrelimit.{u_1 + 1} (α := Ordinal.{u_1}) 0),
  (preAleph : (a : Ordinal.{u_1}) → Cardinal.{u_1}) 0 ≤ c ↔
    ∀ o' < 0, (preAleph : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o' ≤ c
Tactic: obtain rfl | ho := eq_or_ne o 0
Cleared hypotheses: o, l
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Aleph (goal)
Goal:
o : Ordinal.{u_1}
l : IsSuccPrelimit o
c : Cardinal.{u_1}
inl :
  ∀ (l : IsSuccPrelimit.{u_1 + 1} (α := Ordinal.{u_1}) 0),
    (preAleph : (a : Ordinal.{u_1}) → Cardinal.{u_1}) 0 ≤ c ↔
      ∀ o' < 0, (preAleph : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o' ≤ c
⊢ (preAleph : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o ≤ c ↔
    ∀ o' < o, (preAleph : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o' ≤ c
have inr : ∀ (ho : o ≠ 0),
  (preAleph : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o ≤ c ↔
    ∀ o' < o, (preAleph : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o' ≤ c
Tactic: obtain rfl | ho := eq_or_ne o 0
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Aleph (goal)
Goal:
o : Ordinal.{u_1}
ho : IsSuccPrelimit o
⊢ Eq (α := Cardinal.{u_1}) ((preAleph : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o : Cardinal.{u_1})
    (⨆ (a : (↑(Iio o) : Type (u_1 + 1))), (preAleph : (a : Ordinal.{u_1}) → Cardinal.{u_1}) (↑a : Ordinal.{u_1}) :
      Cardinal.{u_1})
have inl : ∀ (ho : IsSuccPrelimit.{u_1 + 1} (α := Ordinal.{u_1}) 0),
  Eq (α := Cardinal.{u_1}) ((preAleph : (a : Ordinal.{u_1}) → Cardinal.{u_1}) 0)
    (⨆ (a : (↑(Iio 0) : Type (u_1 + 1))), (preAleph : (a : Ordinal.{u_1}) → Cardinal.{u_1}) (↑a : Ordinal.{u_1}))
Tactic: obtain rfl | h := eq_or_ne o 0
Cleared hypotheses: o, ho
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Aleph (goal)
Goal:
o : Ordinal.{u_1}
ho : IsSuccPrelimit o
inl :
  ∀ (ho : IsSuccPrelimit.{u_1 + 1} (α := Ordinal.{u_1}) 0),
    Eq (α := Cardinal.{u_1}) ((preAleph : (a : Ordinal.{u_1}) → Cardinal.{u_1}) 0)
      (⨆ (a : (↑(Iio 0) : Type (u_1 + 1))), (preAleph : (a : Ordinal.{u_1}) → Cardinal.{u_1}) (↑a : Ordinal.{u_1}))
⊢ Eq (α := Cardinal.{u_1}) ((preAleph : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o : Cardinal.{u_1})
    (⨆ (a : (↑(Iio o) : Type (u_1 + 1))), (preAleph : (a : Ordinal.{u_1}) → Cardinal.{u_1}) (↑a : Ordinal.{u_1}) :
      Cardinal.{u_1})
have inr : ∀ (h : o ≠ 0),
  Eq (α := Cardinal.{u_1}) ((preAleph : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o : Cardinal.{u_1})
    (⨆ (a : (↑(Iio o) : Type (u_1 + 1))), (preAleph : (a : Ordinal.{u_1}) → Cardinal.{u_1}) (↑a : Ordinal.{u_1}) :
      Cardinal.{u_1})
Tactic: obtain rfl | h := eq_or_ne o 0
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Aleph (goal)
Goal:
o : Ordinal.{u_1}
⊢ Eq (α := Cardinal.{u_1}) (succ ((ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o) : Cardinal.{u_1})
    ((ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) (o + 1) : Cardinal.{u_1})
have rw : Eq (α := Cardinal.{u_1}) (succ ((preAleph : (a : Ordinal.{u_1}) → Cardinal.{u_1}) (ω + o)) : Cardinal.{u_1})
  ((ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) (o + 1) : Cardinal.{u_1})
Tactic: rw [aleph_eq_preAleph, succ_preAleph, add_assoc, aleph_eq_preAleph]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Aleph (goal)
Goal:
o : Ordinal.{u_1}
rw :
  Eq (α := Cardinal.{u_1}) (succ ((preAleph : (a : Ordinal.{u_1}) → Cardinal.{u_1}) (ω + o)) : Cardinal.{u_1})
    ((ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) (o + 1) : Cardinal.{u_1})
⊢ Eq (α := Cardinal.{u_1}) (succ ((ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o) : Cardinal.{u_1})
    ((ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) (o + 1) : Cardinal.{u_1})
have rw₁ : Eq (α := Cardinal.{u_1}) ((preAleph : (a : Ordinal.{u_1}) → Cardinal.{u_1}) (ω + o + 1) : Cardinal.{u_1})
  ((ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) (o + 1) : Cardinal.{u_1})
Tactic: rw [aleph_eq_preAleph, succ_preAleph, add_assoc, aleph_eq_preAleph]