awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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})
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})
⊢ 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]
-- 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})
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})
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})
⊢ 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})
  ((preAleph : (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:
⊢ (ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) 0 = ℵ₀
have rw : (preAleph : (a : Ordinal.{u_1}) → Cardinal.{u_1}) (ω + 0) = ℵ₀
Tactic: rw [aleph_eq_preAleph, add_zero, preAleph_omega0]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Aleph (goal)
Goal:
rw : (preAleph : (a : Ordinal.{u_1}) → Cardinal.{u_1}) (ω + 0) = ℵ₀
⊢ (ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) 0 = ℵ₀
have rw₁ : (preAleph : (a : Ordinal.{u_1}) → Cardinal.{u_1}) ω = ℵ₀
Tactic: rw [aleph_eq_preAleph, add_zero, preAleph_omega0]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Aleph (goal)
Goal:
rw : (preAleph : (a : Ordinal.{u_1}) → Cardinal.{u_1}) (ω + 0) = ℵ₀
rw₁ : (preAleph : (a : Ordinal.{u_1}) → Cardinal.{u_1}) ω = ℵ₀
⊢ (ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) 0 = ℵ₀
have rw₂ : ℵ₀ = ℵ₀
Tactic: rw [aleph_eq_preAleph, add_zero, preAleph_omega0]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Aleph (goal)
Goal:
o : Ordinal.{u_1}
⊢ ℵ₀ ≤ (ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o
have rw : ω ≤ ω + o
Tactic: rw [aleph_eq_preAleph, aleph0_le_preAleph]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Aleph (goal)
Goal:
o : Ordinal.{u_1}
⊢ ℵ₀ < (ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o ↔ 0 < o
have rw : LT.lt (α := Cardinal.{u_1}) ((ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) 0 : Cardinal.{u_1})
    ((ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o : Cardinal.{u_1}) ↔
  0 < o
Tactic: rw [← aleph_zero, aleph_lt_aleph]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Aleph (goal)
Goal:
o : Ordinal.{u_1}
rw :
  LT.lt (α := Cardinal.{u_1}) ((ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) 0 : Cardinal.{u_1})
      ((ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o : Cardinal.{u_1}) ↔
    0 < o
⊢ ℵ₀ < (ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o ↔ 0 < o
have rw₁ : 0 < o ↔ 0 < o
Tactic: rw [← aleph_zero, aleph_lt_aleph]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Aleph (goal)
Goal:
o : Ordinal.{u_1}
⊢ IsSuccLimit (α := Ordinal.{u_1}) ((ω_ : (a : Ordinal.{u_1}) → Ordinal.{u_1}) o : Ordinal.{u_1})
have rw : IsSuccLimit (ord ((ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o))
Tactic: rw [← ord_aleph]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Aleph (goal)
Goal:
⊢ range (ι := Ordinal.{u_1}) (⇑ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) = Ici ℵ₀
have h : ∀ (c : Cardinal.{u_1}),
  Membership.mem (γ := Set Cardinal.{u_1}) (range (ι := Ordinal.{u_1}) (⇑ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1})) c ↔
    c ∈ Ici ℵ₀
Tactic: ext c
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Aleph (goal)
Goal:
c : Cardinal.{u_1}
⊢ Membership.mem (γ := Set Cardinal.{u_1}) (range (ι := Ordinal.{u_1}) (⇑ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1})) c ↔
    c ∈ Ici ℵ₀
have h : ∀ (hc : c ∈ Ici ℵ₀),
  (ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1})
      (HSub.hSub (α := Ordinal.{u_1}) ((preAleph.symm : (a : Cardinal.{u_1}) → Ordinal.{u_1}) c : Ordinal.{u_1}) ω) =
    c
Tactic: refine ⟨fun ⟨o, e⟩ => e ▸ aleph0_le_aleph _, fun hc ↦ ⟨preAleph.symm c - ω, ?_⟩⟩
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Aleph (goal)
Goal:
c : Cardinal.{u_1}
hc : c ∈ Ici ℵ₀
⊢ (ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1})
      (HSub.hSub (α := Ordinal.{u_1}) ((preAleph.symm : (a : Cardinal.{u_1}) → Ordinal.{u_1}) c : Ordinal.{u_1}) ω) =
    c
have h : ω ≤ (preAleph.symm : (a : Cardinal.{u_1}) → Ordinal.{u_1}) c
Tactic: rw [aleph_eq_preAleph, Ordinal.add_sub_cancel_of_le, preAleph.apply_symm_apply]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Aleph (goal)
Goal:
c : Cardinal.{u_1}
hc : c ∈ Ici ℵ₀
⊢ ω ≤ (preAleph.symm : (a : Cardinal.{u_1}) → Ordinal.{u_1}) c
have h : ℵ₀ ≤ (preAleph : (a : Ordinal.{u_1}) → Cardinal.{u_1}) ((preAleph.symm : (a : Cardinal.{u_1}) → Ordinal.{u_1}) c)
Tactic: rwa [← aleph0_le_preAleph, preAleph.apply_symm_apply]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Aleph (goal)
Goal:
c : Cardinal.{u_1}
hc : c ∈ Ici ℵ₀
h : ℵ₀ ≤ (preAleph : (a : Ordinal.{u_1}) → Cardinal.{u_1}) ((preAleph.symm : (a : Cardinal.{u_1}) → Ordinal.{u_1}) c)
⊢ ω ≤ (preAleph.symm : (a : Cardinal.{u_1}) → Ordinal.{u_1}) c
have h₁ : ℵ₀ ≤ c
Tactic: rwa [← aleph0_le_preAleph, preAleph.apply_symm_apply]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Aleph (goal)
Goal:
c : Cardinal.{u_1}
⊢ Membership.mem (γ := Set Cardinal.{u_1}) (range (ι := Ordinal.{u_1}) (⇑ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1})) c ↔
    ℵ₀ ≤ c
have rw : c ∈ Ici ℵ₀ ↔ ℵ₀ ≤ c
Tactic: rw [range_aleph, mem_Ici]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Aleph (goal)
Goal:
c : Cardinal.{u_1}
rw : c ∈ Ici ℵ₀ ↔ ℵ₀ ≤ c
⊢ Membership.mem (γ := Set Cardinal.{u_1}) (range (ι := Ordinal.{u_1}) (⇑ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1})) c ↔
    ℵ₀ ≤ c
have rw₁ : ℵ₀ ≤ c ↔ ℵ₀ ≤ c
Tactic: rw [range_aleph, mem_Ici]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Aleph (goal)
Goal:
x o : Ordinal.{u_1}
⊢ x < (ω_ : (a : Ordinal.{u_1}) → Ordinal.{u_1}) o ↔ x.card < (ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o
have rw : x.card < card ((ω_ : (a : Ordinal.{u_1}) → Ordinal.{u_1}) o) ↔ x.card < (ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o
Tactic: rw [← (isInitial_omega o).card_lt_card, card_omega]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Aleph (goal)
Goal:
x o : Ordinal.{u_1}
rw :
  x.card < card ((ω_ : (a : Ordinal.{u_1}) → Ordinal.{u_1}) o) ↔ x.card < (ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o
⊢ x < (ω_ : (a : Ordinal.{u_1}) → Ordinal.{u_1}) o ↔ x.card < (ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o
have rw₁ : x.card < (ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o ↔ x.card < (ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o
Tactic: rw [← (isInitial_omega o).card_lt_card, card_omega]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Aleph (goal)
Goal:
⊢ succ ℵ₀ = (ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) 1
have rw : Eq (α := Cardinal.{u_1}) (succ ((ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) 0))
  ((ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) 1)
Tactic: rw [← aleph_zero, succ_aleph, zero_add]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Aleph (goal)
Goal:
rw :
  Eq (α := Cardinal.{u_1}) (succ ((ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) 0))
    ((ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) 1)
⊢ succ ℵ₀ = (ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) 1
have rw₁ : Eq (α := Cardinal.{u_1})
  ((ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) (HAdd.hAdd (α := Ordinal.{u_1}) 0 1) : Cardinal.{u_1})
  ((ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) 1 : Cardinal.{u_1})
Tactic: rw [← aleph_zero, succ_aleph, zero_add]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Aleph (goal)
Goal:
rw :
  Eq (α := Cardinal.{u_1}) (succ ((ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) 0))
    ((ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) 1)
rw₁ :
  Eq (α := Cardinal.{u_1})
    ((ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) (HAdd.hAdd (α := Ordinal.{u_1}) 0 1) : Cardinal.{u_1})
    ((ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) 1 : Cardinal.{u_1})
⊢ succ ℵ₀ = (ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) 1
have rw₂ : Eq (α := Cardinal.{u_1}) ((ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) 1) ((ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) 1)
Tactic: rw [← aleph_zero, succ_aleph, zero_add]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Aleph (goal)
Goal:
c : Cardinal.{u_1}
⊢ (ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) 1 ≤ c ↔ ℵ₀ < c
have rw : succ ℵ₀ ≤ c ↔ ℵ₀ < c
Tactic: rw [← succ_aleph0, succ_le_iff]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Aleph (goal)
Goal:
c : Cardinal.{u_1}
rw : succ ℵ₀ ≤ c ↔ ℵ₀ < c
⊢ (ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) 1 ≤ c ↔ ℵ₀ < c
have rw₁ : ℵ₀ < c ↔ ℵ₀ < c
Tactic: rw [← succ_aleph0, succ_le_iff]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Aleph (goal)
Goal:
c : Cardinal.{u_1}
⊢ c < (ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) 1 ↔ c ≤ ℵ₀
have rw : c < succ ℵ₀ ↔ c ≤ ℵ₀
Tactic: rw [← succ_aleph0, lt_succ_iff]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Aleph (goal)
Goal:
c : Cardinal.{u_1}
rw : c < succ ℵ₀ ↔ c ≤ ℵ₀
⊢ c < (ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) 1 ↔ c ≤ ℵ₀
have rw₁ : c ≤ ℵ₀ ↔ c ≤ ℵ₀
Tactic: rw [← succ_aleph0, lt_succ_iff]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Aleph (goal)
Goal:
α : Type u_1
⊢ (ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) 1 ≤ #α ↔ Uncountable α
have rw : ℵ₀ < #α ↔ Uncountable α
Tactic: rw [aleph_one_le_iff, aleph0_lt_mk_iff]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Aleph (goal)
Goal:
α : Type u_1
rw : ℵ₀ < #α ↔ Uncountable α
⊢ (ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) 1 ≤ #α ↔ Uncountable α
have rw₁ : Uncountable α ↔ Uncountable α
Tactic: rw [aleph_one_le_iff, aleph0_lt_mk_iff]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Aleph (goal)
Goal:
α : Type u_1
s : Set α
⊢ s.Countable ↔ #(↑s : Type u_1) < (ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) 1
have rw : s.Countable ↔ #(↑s : Type u_1) ≤ ℵ₀
Tactic: rw [lt_aleph_one_iff, le_aleph0_iff_set_countable]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Aleph (goal)
Goal:
α : Type u_1
s : Set α
rw : s.Countable ↔ #(↑s : Type u_1) ≤ ℵ₀
⊢ s.Countable ↔ #(↑s : Type u_1) < (ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) 1
have rw₁ : s.Countable ↔ s.Countable
Tactic: rw [lt_aleph_one_iff, le_aleph0_iff_set_countable]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Aleph (goal)
Goal:
a b : Ordinal.{u_1}
h : a < b
| preBeth b
have rw : ⨆ (a : (↑(Iio b) : Type (u_1 + 1))), HPow.hPow (α := Cardinal.{u_1}) 2 (preBeth (↑a : Ordinal.{u_1}))
Tactic: rw [preBeth]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Aleph (goal)
Goal:
a b : Ordinal.{u_1}
h : a < b
⊢ preBeth a < preBeth b
have conv_rhs : preBeth a < ⨆ (a : (↑(Iio b) : Type (u_1 + 1))), HPow.hPow (α := Cardinal.{u_1}) 2 (preBeth (↑a : Ordinal.{u_1}))
Tactic: conv_rhs => rw [preBeth]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Aleph (goal)
Goal:
a b : Ordinal.{u_1}
h : a < b
⊢ preBeth a < ⨆ (a : (↑(Iio b) : Type (u_1 + 1))), HPow.hPow (α := Cardinal.{u_1}) 2 (preBeth (↑a : Ordinal.{u_1}))
have rw : ∃ (i : (↑(Iio b) : Type (u_1 + 1))), preBeth a < HPow.hPow (α := Cardinal.{u_1}) 2 (preBeth (↑i : Ordinal.{u_1}))
Tactic: rw [lt_ciSup_iff' bddAbove_of_small]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Aleph (goal)
Goal:
⊢ preBeth 0 = 0
have rw : Eq.{u_1 + 2} (α := Cardinal.{u_1})
  (⨆ (a : (↑(Iio 0) : Type (u_1 + 1))), HPow.hPow (α := Cardinal.{u_1}) 2 (preBeth (↑a : Ordinal.{u_1}))) 0
Tactic: rw [preBeth]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Aleph (goal)
Goal:
o : Ordinal.{u_1}
⊢ preBeth (o + 1) = HPow.hPow (α := Cardinal.{u_1}) 2 (preBeth o)
have rw : ⨆ (a : (↑(Iic o) : Type (u_1 + 1))), HPow.hPow (α := Cardinal.{u_1}) 2 (preBeth (↑a : Ordinal.{u_1})) =
  HPow.hPow (α := Cardinal.{u_1}) 2 (preBeth o)
Tactic: rw [preBeth, ← succ_eq_add_one, Iio_succ]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Aleph (goal)
Goal:
o : Ordinal.{u_1}
ho : IsSuccPrelimit o
⊢ preBeth o = ⨆ (a : (↑(Iio o) : Type (u_1 + 1))), preBeth (↑a : Ordinal.{u_1})
have rw : Eq.{u_1 + 2} (α := Cardinal.{u_1})
  (⨆ (a : (↑(Iio o) : Type (u_1 + 1))), HPow.hPow (α := Cardinal.{u_1}) 2 (preBeth (↑a : Ordinal.{u_1})))
  (⨆ (a : (↑(Iio o) : Type (u_1 + 1))), preBeth (↑a : Ordinal.{u_1}))
Tactic: rw [preBeth]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Aleph (goal)
Goal:
o : Ordinal.{u_1}
ho : IsSuccPrelimit o
⊢ Eq.{u_1 + 2} (α := Cardinal.{u_1})
    (⨆ (a : (↑(Iio o) : Type (u_1 + 1))), HPow.hPow (α := Cardinal.{u_1}) 2 (preBeth (↑a : Ordinal.{u_1})))
    (⨆ (a : (↑(Iio o) : Type (u_1 + 1))), preBeth (↑a : Ordinal.{u_1}))
have apply : LE.le.{u_1 + 1} (α := Cardinal.{u_1})
  (⨆ (x : (↑(Iio o) : Type (u_1 + 1))), HPow.hPow (α := Cardinal.{u_1}) 2 (preBeth (↑x : Ordinal.{u_1})))
  (⨆ (x : (↑(Iio o) : Type (u_1 + 1))), preBeth (↑x : Ordinal.{u_1}))
Tactic: apply (ciSup_mono bddAbove_of_small fun _ ↦ (cantor _).le).antisymm'
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Aleph (goal)
Goal:
o : Ordinal.{u_1}
ho : IsSuccPrelimit o
⊢ LE.le.{u_1 + 1} (α := Cardinal.{u_1})
    (⨆ (x : (↑(Iio o) : Type (u_1 + 1))), HPow.hPow (α := Cardinal.{u_1}) 2 (preBeth (↑x : Ordinal.{u_1})))
    (⨆ (x : (↑(Iio o) : Type (u_1 + 1))), preBeth (↑x : Ordinal.{u_1}))
have rw : ∀ (i : (↑(Iio o) : Type (u_1 + 1))),
  HPow.hPow (α := Cardinal.{u_1}) 2 (preBeth (↑i : Ordinal.{u_1})) ≤
    ⨆ (x : (↑(Iio o) : Type (u_1 + 1))), preBeth (↑x : Ordinal.{u_1})
Tactic: rw [ciSup_le_iff' bddAbove_of_small]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Aleph (goal)
Goal:
o : Ordinal.{u_1}
ho : IsSuccPrelimit o
a : (↑(Iio o) : Type (u_1 + 1))
⊢ HPow.hPow (α := Cardinal.{u_1}) 2 (preBeth (↑a : Ordinal.{u_1})) ≤
    ⨆ (x : (↑(Iio o) : Type (u_1 + 1))), preBeth (↑x : Ordinal.{u_1})
have rw : preBeth (succ (↑a : Ordinal.{u_1})) ≤ ⨆ (x : (↑(Iio o) : Type (u_1 + 1))), preBeth (↑x : Ordinal.{u_1})
Tactic: rw [← preBeth_succ]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Aleph (goal)
Goal:
⊢ IsNormal preBeth
have rw : StrictMono preBeth ∧
  ∀ (o : Ordinal.{u_1}), IsSuccLimit o → ∀ (a : Cardinal.{u_1}), (∀ b < o, preBeth b ≤ a) → preBeth o ≤ a
Tactic: rw [isNormal_iff]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Aleph (goal)
Goal:
⊢ StrictMono preBeth ∧
    ∀ (o : Ordinal.{u_1}), IsSuccLimit o → ∀ (a : Cardinal.{u_1}), (∀ b < o, preBeth b ≤ a) → preBeth o ≤ a
have refine : ∀ (o : Ordinal.{u_1}) (ho : IsSuccLimit o) (a : Cardinal.{u_1}), (∀ b < o, preBeth b ≤ a) → preBeth o ≤ a
Tactic: refine ⟨preBeth_strictMono, fun o ho ↦ ?_⟩
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Aleph (goal)
Goal:
⊢ preBeth ω = ℵ₀
have a : preBeth ω ≤ ℵ₀
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Aleph (goal)
Goal:
a : preBeth ω ≤ ℵ₀
⊢ preBeth ω = ℵ₀
have a₁ : ℵ₀ ≤ preBeth ω
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Aleph (goal)
Goal:
⊢ preBeth ω ≤ ℵ₀
have a : ∀ (i : (↑(Iio ω) : Type (u_1 + 1))), preBeth (↑i : Ordinal.{u_1}) ≤ ℵ₀
Tactic: rw [preBeth_limit isSuccLimit_omega0.isSuccPrelimit, ciSup_le_iff' bddAbove_of_small]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Aleph (goal)
Goal:
a : Ordinal.{u_1}
ha : a ∈ Iio ω
⊢ preBeth (↑(Subtype.mk (p := fun (x : Ordinal.{u_1}) ↦ x ∈ Iio ω) a ha) : Ordinal.{u_1}) ≤ ℵ₀
have a₁ : ∀ (n : ℕ) (ha : (↑n : Ordinal.{u_1}) ∈ Iio ω),
  preBeth (↑(Subtype.mk (p := fun (x : Ordinal.{u_1}) ↦ x ∈ Iio ω) (↑n : Ordinal.{u_1}) ha) : Ordinal.{u_1}) ≤ ℵ₀
Tactic: obtain ⟨n, rfl⟩ := lt_omega0.1 ha
Cleared hypotheses: a, ha
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Aleph (goal)
Goal:
n : ℕ
ha : (↑n : Ordinal.{u_1}) ∈ Iio ω
⊢ preBeth (↑(Subtype.mk (p := fun (x : Ordinal.{u_1}) ↦ x ∈ Iio ω) (↑n : Ordinal.{u_1}) ha) : Ordinal.{u_1}) ≤ ℵ₀
have a : (↑((fun (x : ℕ) ↦ HPow.hPow (α := ℕ) 2 x)^[n] 0) : Cardinal.{u_1}) ≤ ℵ₀
Tactic: rw [preBeth_nat]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Aleph (goal)
Goal:
o : Ordinal.{u_1}
⊢ IsStrongPrelimit.{u_1} (preBeth o) ↔ IsSuccPrelimit o
have refine_1 : IsStrongPrelimit.{u_1} (preBeth o) → IsSuccPrelimit o
Tactic: refine ⟨?_, fun ho x hx ↦ ?_⟩
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Aleph (goal)
Goal:
o : Ordinal.{u_1}
refine_1 : IsStrongPrelimit.{u_1} (preBeth o) → IsSuccPrelimit o
⊢ IsStrongPrelimit.{u_1} (preBeth o) ↔ IsSuccPrelimit o
have refine_2 : ∀ (ho : IsSuccPrelimit o) (x : Cardinal.{u_1}) (hx : x < preBeth o), HPow.hPow (α := Cardinal.{u_1}) 2 x < preBeth o
Tactic: refine ⟨?_, fun ho x hx ↦ ?_⟩
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Aleph (goal)
Goal:
o : Ordinal.{u_1}
⊢ IsStrongPrelimit.{u_1} (preBeth o) → IsSuccPrelimit o
have refine_1 : ¬IsSuccPrelimit o → ¬IsStrongPrelimit.{u_1} (preBeth o)
Tactic: contrapose!
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Aleph (goal)
Goal:
o : Ordinal.{u_1}
⊢ ¬IsSuccPrelimit o → ¬IsStrongPrelimit.{u_1} (preBeth o)
have refine_1 : Membership.mem (γ := Set Ordinal.{u_1}) (range succ) o →
  ∃ x < preBeth o, preBeth o ≤ HPow.hPow (α := Cardinal.{u_1}) 2 x
Tactic: rw [not_isSuccPrelimit_iff_mem_range_succ, not_isStrongPrelimit_iff]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Aleph (goal)
Goal:
a : Ordinal.{u_1}
⊢ ∃ x < preBeth (succ a), preBeth (succ a) ≤ HPow.hPow (α := Cardinal.{u_1}) 2 x
have refine_1 : preBeth a < preBeth (succ a)
Tactic: refine ⟨preBeth a, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Aleph (goal)
Goal:
a : Ordinal.{u_1}
refine_1 : preBeth a < preBeth (succ a)
⊢ ∃ x < preBeth (succ a), preBeth (succ a) ≤ HPow.hPow (α := Cardinal.{u_1}) 2 x
have refine_1₁ : preBeth (succ a) ≤ HPow.hPow (α := Cardinal.{u_1}) 2 (preBeth a)
Tactic: refine ⟨preBeth a, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Aleph (goal)
Goal:
a : Ordinal.{u_1}
⊢ preBeth a < preBeth (succ a)
have refine_1 : a < succ a
Tactic: rw [preBeth_lt_preBeth, lt_succ_iff]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Aleph (goal)
Goal:
a : Ordinal.{u_1}
refine_1 : a < succ a
⊢ preBeth a < preBeth (succ a)
have refine_1₁ : a ≤ a
Tactic: rw [preBeth_lt_preBeth, lt_succ_iff]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Aleph (hypothesis)
Goal:
o : Ordinal.{u_1}
ho : IsSuccPrelimit o
x : Cardinal.{u_1}
hx : x < preBeth o
⊢ HPow.hPow (α := Cardinal.{u_1}) 2 x < preBeth o
have hx₁ : x < ⨆ (a : (↑(Iio o) : Type (u_1 + 1))), preBeth (↑a : Ordinal.{u_1})
Tactic: rw [preBeth_limit ho] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Aleph (goal)
Goal:
o : Ordinal.{u_1}
ho : IsSuccPrelimit o
x : Cardinal.{u_1}
hx : x < ⨆ (a : (↑(Iio o) : Type (u_1 + 1))), preBeth (↑a : Ordinal.{u_1})
⊢ HPow.hPow (α := Cardinal.{u_1}) 2 x < preBeth o
have refine_2 : ∀ (a : (↑(Iio o) : Type (u_1 + 1))) (ha : x < preBeth (↑a : Ordinal.{u_1})),
  HPow.hPow (α := Cardinal.{u_1}) 2 x < preBeth o
Tactic: obtain ⟨a, ha⟩ := exists_lt_of_lt_ciSup' hx
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Aleph (goal)
Goal:
o : Ordinal.{u_1}
ho : IsSuccPrelimit o
x : Cardinal.{u_1}
hx : x < ⨆ (a : (↑(Iio o) : Type (u_1 + 1))), preBeth (↑a : Ordinal.{u_1})
a : (↑(Iio o) : Type (u_1 + 1))
ha : x < preBeth (↑a : Ordinal.{u_1})
⊢ HPow.hPow (α := Cardinal.{u_1}) 2 x < preBeth o
have refine_2 : HPow.hPow (α := Cardinal.{u_1}) 2 x ≤ preBeth ((↑a : Ordinal.{u_1}) + 1)
Tactic: apply (preBeth_strictMono (ho.add_one_lt a.2)).trans_le'
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Aleph (goal)
Goal:
o : Ordinal.{u_1}
⊢ IsStrongLimit.{u_1} (preBeth o) ↔ IsSuccLimit o
have rw : preBeth o ≠ 0 ∧ IsStrongPrelimit.{u_1} (preBeth o) ↔ IsSuccLimit o
Tactic: rw [isStrongLimit_iff, isSuccLimit_iff, preBeth_eq_zero.ne, isStrongPrelimit_preBeth]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Aleph (goal)
Goal:
o : Ordinal.{u_1}
rw : preBeth o ≠ 0 ∧ IsStrongPrelimit.{u_1} (preBeth o) ↔ IsSuccLimit o
⊢ IsStrongLimit.{u_1} (preBeth o) ↔ IsSuccLimit o
have rw₁ : preBeth o ≠ 0 ∧ IsStrongPrelimit.{u_1} (preBeth o) ↔ o ≠ 0 ∧ IsSuccPrelimit o
Tactic: rw [isStrongLimit_iff, isSuccLimit_iff, preBeth_eq_zero.ne, isStrongPrelimit_preBeth]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Aleph (goal)
Goal:
o : Ordinal.{u_1}
rw : preBeth o ≠ 0 ∧ IsStrongPrelimit.{u_1} (preBeth o) ↔ IsSuccLimit o
rw₁ : preBeth o ≠ 0 ∧ IsStrongPrelimit.{u_1} (preBeth o) ↔ o ≠ 0 ∧ IsSuccPrelimit o
⊢ IsStrongLimit.{u_1} (preBeth o) ↔ IsSuccLimit o
have rw₂ : o ≠ 0 ∧ IsStrongPrelimit.{u_1} (preBeth o) ↔ o ≠ 0 ∧ IsSuccPrelimit o
Tactic: rw [isStrongLimit_iff, isSuccLimit_iff, preBeth_eq_zero.ne, isStrongPrelimit_preBeth]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Aleph (goal)
Goal:
o : Ordinal.{u_1}
rw : preBeth o ≠ 0 ∧ IsStrongPrelimit.{u_1} (preBeth o) ↔ IsSuccLimit o
rw₁ : preBeth o ≠ 0 ∧ IsStrongPrelimit.{u_1} (preBeth o) ↔ o ≠ 0 ∧ IsSuccPrelimit o
rw₂ : o ≠ 0 ∧ IsStrongPrelimit.{u_1} (preBeth o) ↔ o ≠ 0 ∧ IsSuccPrelimit o
⊢ IsStrongLimit.{u_1} (preBeth o) ↔ IsSuccLimit o
have rw₃ : o ≠ 0 ∧ IsSuccPrelimit o ↔ o ≠ 0 ∧ IsSuccPrelimit o
Tactic: rw [isStrongLimit_iff, isSuccLimit_iff, preBeth_eq_zero.ne, isStrongPrelimit_preBeth]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Aleph (goal)
Goal:
o : Ordinal.{u_1}
ho : IsSuccPrelimit o
IH : ∀ b < o, lift.{v, u_1} (preBeth b) = preBeth (Ordinal.lift.{v, u_1} b)
⊢ lift.{v, u_1} (preBeth o) = preBeth (Ordinal.lift.{v, u_1} o)
have isSuccPrelimit : Eq (α := Cardinal.{max u_1 v}) (⨆ (i : (↑(Iio o) : Type (u_1 + 1))), lift.{v, u_1} (preBeth (↑i : Ordinal.{u_1})))
  (⨆ (a : (↑(Iio (Ordinal.lift.{v, u_1} o)) : Type ((max u_1 v) + 1))), preBeth (↑a : Ordinal.{max u_1 v}))
Tactic: rw [preBeth_limit ho, preBeth_limit (isSuccPrelimit_lift.2 ho), lift_iSup bddAbove_of_small]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Aleph (goal)
Goal:
o : Ordinal.{u_1}
ho : IsSuccPrelimit o
IH : ∀ b < o, lift.{v, u_1} (preBeth b) = preBeth (Ordinal.lift.{v, u_1} b)
⊢ Eq (α := Cardinal.{max u_1 v}) (⨆ (i : (↑(Iio o) : Type (u_1 + 1))), lift.{v, u_1} (preBeth (↑i : Ordinal.{u_1})))
    (⨆ (a : (↑(Iio (Ordinal.lift.{v, u_1} o)) : Type ((max u_1 v) + 1))), preBeth (↑a : Ordinal.{max u_1 v}))
have isSuccPrelimit : Eq (α := Set Cardinal.{max u_1 v})
  (range fun (i : (↑(Iio o) : Type (u_1 + 1))) ↦ lift.{v, u_1} (preBeth (↑i : Ordinal.{u_1})))
  (range fun (a : (↑(Iio (Ordinal.lift.{v, u_1} o)) : Type ((max u_1 v) + 1))) ↦ preBeth (↑a : Ordinal.{max u_1 v}))
Tactic: apply congrArg sSup
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Aleph (goal)
Goal:
o : Ordinal.{u_1}
ho : IsSuccPrelimit o
IH : ∀ b < o, lift.{v, u_1} (preBeth b) = preBeth (Ordinal.lift.{v, u_1} b)
⊢ Eq (α := Set Cardinal.{max u_1 v})
    (range fun (i : (↑(Iio o) : Type (u_1 + 1))) ↦ lift.{v, u_1} (preBeth (↑i : Ordinal.{u_1})))
    (range fun (a : (↑(Iio (Ordinal.lift.{v, u_1} o)) : Type ((max u_1 v) + 1))) ↦ preBeth (↑a : Ordinal.{max u_1 v}))
have isSuccPrelimit : ∀ (x : Cardinal.{max u_1 v}),
  Membership.mem (γ := Set Cardinal.{max u_1 v})
      (range fun (i : (↑(Iio o) : Type (u_1 + 1))) ↦ lift.{v, u_1} (preBeth (↑i : Ordinal.{u_1}))) x ↔
    Membership.mem (γ := Set Cardinal.{max u_1 v})
      (range fun (a : (↑(Iio (Ordinal.lift.{v, u_1} o)) : Type ((max u_1 v) + 1))) ↦ preBeth (↑a : Ordinal.{max u_1 v}))
      x
Tactic: ext x