awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
o : Ordinal.{u_1}
⊢ ord ((ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o) = (ω_ : (a : Ordinal.{u_1}) → Ordinal.{u_1}) o

Tactic:
ord_preAleph _

Premises used: Cardinal.ord_preAleph
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
o₁ o₂ : Ordinal.{u_1}
⊢ LT.lt (α := Cardinal.{u_1}) ((ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o₁ : Cardinal.{u_1})
      ((ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o₂ : Cardinal.{u_1}) ↔
    o₁ < o₂

Tactic:
aleph.lt_iff_lt

Premises used: Cardinal.aleph, OrderEmbedding.lt_iff_lt
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
o₁ o₂ : Ordinal.{u_1}
⊢ LE.le (α := Cardinal.{u_1}) ((ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o₁ : Cardinal.{u_1})
      ((ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o₂ : Cardinal.{u_1}) ↔
    o₁ ≤ o₂

Tactic:
aleph.le_iff_le

Premises used: Cardinal.aleph, OrderEmbedding.le_iff_le
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
o₁ o₂ : Ordinal.{u_1}
⊢ Eq (α := Cardinal.{u_1}) ((ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) (max o₁ o₂) : Cardinal.{u_1})
    (max ((ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o₁) ((ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o₂) :
      Cardinal.{u_1})

Tactic:
aleph.monotone.map_max

Premises used: OrderEmbedding.monotone, Cardinal.aleph, Monotone.map_max
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
o : Ordinal.{u_1}
⊢ LE.le (α := Cardinal.{u_1}) ((preAleph : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o : Cardinal.{u_1})
    ((ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o : Cardinal.{u_1})

Tactic:
preAleph_le_preAleph.2 le_add_self

Premises used: Iff.mpr, Cardinal.preAleph_le_preAleph, le_add_self
-- Module: Mathlib.SetTheory.Cardinal.Aleph
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})
rw₃ 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})
⊢ 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})

Tactic:
rw [aleph_eq_preAleph, succ_preAleph, add_assoc, aleph_eq_preAleph]

Premises used: add_assoc, Cardinal.succ_preAleph, Cardinal.aleph_eq_preAleph
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
o : Ordinal.{u_1}
⊢ Eq (α := Cardinal.{u_1}) ((ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) (o + 1) : Cardinal.{u_1})
    (succ ((ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o) : Cardinal.{u_1})

Tactic:
simp
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
o : Ordinal.{u_1}
⊢ Eq (α := Cardinal.{u_1}) ((ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) (succ o) : Cardinal.{u_1})
    (succ ((ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o) : Cardinal.{u_1})

Tactic:
(succ_aleph o).symm

Premises used: Order.succ, Eq.symm, Cardinal.succ_aleph
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
rw : (preAleph : (a : Ordinal.{u_1}) → Cardinal.{u_1}) (ω + 0) = ℵ₀
rw₁ : (preAleph : (a : Ordinal.{u_1}) → Cardinal.{u_1}) ω = ℵ₀
rw₂ rw₃ : ℵ₀ = ℵ₀
⊢ (ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) 0 = ℵ₀

Tactic:
rw [aleph_eq_preAleph, add_zero, preAleph_omega0]

Premises used: Cardinal.preAleph_omega0, Cardinal.aleph_eq_preAleph, add_zero
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
o : Ordinal.{u}
⊢ lift.{v, u} ((ℵ_ : (a : Ordinal.{u}) → Cardinal.{u}) o) =
    (ℵ_ : (a : Ordinal.{max v u}) → Cardinal.{max v u}) (Ordinal.lift.{v, u} o)

Tactic:
simp [aleph_eq_preAleph]

Premises used: Cardinal.aleph_eq_preAleph
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
o : Ordinal.{u}
⊢ Ordinal.lift.{v, u} ((ω_ : (a : Ordinal.{u}) → Ordinal.{u}) o) =
    (ω_ : (a : Ordinal.{max v u}) → Ordinal.{max v u}) (Ordinal.lift.{v, u} o)

Tactic:
simp [omega_eq_preOmega]

Premises used: Ordinal.omega_eq_preOmega
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
⊢ IsNormal (α := Ordinal.{u_1}) (β := Cardinal.{u_1}) (⇑ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1})

Tactic:
isNormal_preAleph.comp (isNormal_add_right _)

Premises used: Cardinal.isNormal_preAleph, Order.IsNormal.comp, Ordinal.isNormal_add_right
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
o : Ordinal.{u_1}
ho : IsSuccLimit o
⊢ Eq (α := Cardinal.{u_1}) ((ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o : Cardinal.{u_1})
    (⨆ (a : (↑(Iio o) : Type (u_1 + 1))), (ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) (↑a : Ordinal.{u_1}) :
      Cardinal.{u_1})

Tactic:
isNormal_aleph.apply_of_isSuccLimit ho

Premises used: Order.IsNormal.apply_of_isSuccLimit, Cardinal.isNormal_aleph
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
o : Ordinal.{u_1}
rw : ω ≤ ω + o
⊢ ℵ₀ ≤ (ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o

Tactic:
rw [aleph_eq_preAleph, aleph0_le_preAleph]

Premises used: Cardinal.aleph0_le_preAleph, Cardinal.aleph_eq_preAleph
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
o : Ordinal.{u_1}
⊢ ω ≤ ω + o

Tactic:
le_self_add

Premises used: le_self_add
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
o : Ordinal.{u_1}
⊢ ω ≤ ω + o

Tactic:
exact le_self_add

Premises used: le_self_add
-- Module: Mathlib.SetTheory.Cardinal.Aleph
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
rw₁ rw₂ : 0 < o ↔ 0 < o
⊢ ℵ₀ < (ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o ↔ 0 < o

Tactic:
rw [← aleph_zero, aleph_lt_aleph]

Premises used: Cardinal.aleph_lt_aleph, Cardinal.aleph_zero
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
o : Ordinal.{u_1}
⊢ LT.lt (α := Cardinal.{u_1}) (0 : Cardinal.{u_1}) ((ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o : Cardinal.{u_1})

Tactic:
aleph0_pos.trans_le (aleph0_le_aleph o)

Premises used: LT.lt.trans_le, Cardinal.aleph0_le_aleph, Cardinal.aleph0_pos
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
o : Ordinal.{u_1}
⊢ o.card ≤ (ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o

Tactic:
o.card_le_preAleph.trans (preAleph_le_aleph o)

Premises used: Cardinal.preAleph_le_aleph, Ordinal.card_le_preAleph, LE.le.trans
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
c : Cardinal.{u_1}
⊢ c ≤ (ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) c.ord

Tactic:
simpa using c.ord.card_le_aleph

Premises used: Ordinal.card_le_aleph, Cardinal.ord
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
o : Ordinal.{u_1}
⊢ Eq (α := ℕ) ((toNat : (a : Cardinal.{u_1}) → ℕ) ((ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o : Cardinal.{u_1}) : ℕ)
    (0 : ℕ)

Tactic:
toNat_apply_of_aleph0_le <| aleph0_le_aleph o

Premises used: Cardinal.toNat_apply_of_aleph0_le, Cardinal.aleph0_le_aleph
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
o : Ordinal.{u_1}
⊢ Eq (α := ℕ∞) ((toENat : (a : Cardinal.{u_1}) → ℕ∞) ((ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o) : ℕ∞) (⊤ : ℕ∞)

Tactic:
(toENat_eq_top.2 (aleph0_le_aleph o))

Premises used: Iff.mpr, Cardinal.aleph0_le_aleph, Cardinal.toENat_eq_top
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
o : Ordinal.{u_1}
rw : IsSuccLimit (ord ((ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o))
⊢ IsSuccLimit (α := Ordinal.{u_1}) ((ω_ : (a : Ordinal.{u_1}) → Ordinal.{u_1}) o : Ordinal.{u_1})

Tactic:
rw [← ord_aleph]

Premises used: Cardinal.ord_aleph
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
o : Ordinal.{u_1}
⊢ IsSuccLimit (ord ((ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o))

Tactic:
isSuccLimit_ord (aleph0_le_aleph _)

Premises used: Cardinal.isSuccLimit_ord, Cardinal.aleph0_le_aleph
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
o : Ordinal.{u_1}
⊢ IsSuccLimit (ord ((ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o))

Tactic:
exact isSuccLimit_ord (aleph0_le_aleph _)

Premises used: Cardinal.isSuccLimit_ord, Cardinal.aleph0_le_aleph
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
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 ℵ₀
⊢ range (ι := Ordinal.{u_1}) (⇑ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) = Ici ℵ₀

Tactic:
ext c
-- Module: Mathlib.SetTheory.Cardinal.Aleph
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 ℵ₀

Tactic:
⟨fun ⟨o, e⟩ => e ▸ aleph0_le_aleph _, fun hc ↦ ⟨preAleph.symm c - ω, ?_⟩⟩

Premises used: Set.Ici, Ordinal.omega0, HSub.hSub, Membership.mem, Eq.rec, Cardinal.aleph0, OrderIso.symm, Cardinal.preAleph, Cardinal.aleph0_le_aleph, _private.0.Cardinal.range_aleph.match_1, Iff.intro, Exists.intro, DFunLike.coe
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
c : Cardinal.{u_1}
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
⊢ Membership.mem (γ := Set Cardinal.{u_1}) (range (ι := Ordinal.{u_1}) (⇑ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1})) c ↔
    c ∈ Ici ℵ₀

Tactic:
refine ⟨fun ⟨o, e⟩ => e ▸ aleph0_le_aleph _, fun hc ↦ ⟨preAleph.symm c - ω, ?_⟩⟩
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
c : Cardinal.{u_1}
hc : c ∈ Ici ℵ₀
h : ω ≤ (preAleph.symm : (a : Cardinal.{u_1}) → Ordinal.{u_1}) c
⊢ (ℵ_ : (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:
rw [aleph_eq_preAleph, Ordinal.add_sub_cancel_of_le, preAleph.apply_symm_apply]

Premises used: OrderIso.apply_symm_apply, Cardinal.preAleph, Ordinal.add_sub_cancel_of_le, Cardinal.aleph_eq_preAleph
-- Module: Mathlib.SetTheory.Cardinal.Aleph
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)
h₁ h₂ h₃ h₄ : ℵ₀ ≤ c
⊢ ω ≤ (preAleph.symm : (a : Cardinal.{u_1}) → Ordinal.{u_1}) c

Tactic:
rwa [← aleph0_le_preAleph, preAleph.apply_symm_apply]

Premises used: OrderIso.apply_symm_apply, Cardinal.preAleph, Cardinal.aleph0_le_preAleph
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
c : Cardinal.{u_1}
rw : c ∈ Ici ℵ₀ ↔ ℵ₀ ≤ c
rw₁ rw₂ : ℵ₀ ≤ c ↔ ℵ₀ ≤ c
⊢ Membership.mem (γ := Set Cardinal.{u_1}) (range (ι := Ordinal.{u_1}) (⇑ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1})) c ↔
    ℵ₀ ≤ c

Tactic:
rw [range_aleph, mem_Ici]

Premises used: Cardinal.range_aleph, Set.mem_Ici
-- Module: Mathlib.SetTheory.Cardinal.Aleph
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
rw₁ rw₂ :
  x.card < (ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{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

Tactic:
rw [← (isInitial_omega o).card_lt_card, card_omega]

Premises used: Ordinal.IsInitial.card_lt_card, Ordinal.isInitial_omega, Ordinal.card_omega
-- Module: Mathlib.SetTheory.Cardinal.Aleph
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})
rw₂ rw₃ :
  Eq (α := Cardinal.{u_1}) ((ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) 1)
    ((ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) 1)
⊢ succ ℵ₀ = (ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) 1

Tactic:
rw [← aleph_zero, succ_aleph, zero_add]

Premises used: zero_add, Cardinal.aleph_zero, Cardinal.succ_aleph
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
c : Cardinal.{u_1}
rw : succ ℵ₀ ≤ c ↔ ℵ₀ < c
rw₁ rw₂ : ℵ₀ < c ↔ ℵ₀ < c
⊢ (ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) 1 ≤ c ↔ ℵ₀ < c

Tactic:
rw [← succ_aleph0, succ_le_iff]

Premises used: Order.succ_le_iff, Cardinal.succ_aleph0
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
c : Cardinal.{u_1}
rw : c < succ ℵ₀ ↔ c ≤ ℵ₀
rw₁ rw₂ : c ≤ ℵ₀ ↔ c ≤ ℵ₀
⊢ c < (ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) 1 ↔ c ≤ ℵ₀

Tactic:
rw [← succ_aleph0, lt_succ_iff]

Premises used: Order.lt_succ_iff, Cardinal.succ_aleph0
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
⊢ ℵ₀ < (ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) 1

Tactic:
simp
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
c : Cardinal.{u_1}
⊢ ℵ₀ < c ↔ (ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) 1 ≤ c

Tactic:
aleph_one_le_iff.symm

Premises used: Cardinal.aleph_one_le_iff, Iff.symm
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
α : Type u_1
rw : ℵ₀ < #α ↔ Uncountable α
rw₁ rw₂ : Uncountable α ↔ Uncountable α
⊢ (ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) 1 ≤ #α ↔ Uncountable α

Tactic:
rw [aleph_one_le_iff, aleph0_lt_mk_iff]

Premises used: Cardinal.aleph0_lt_mk_iff, Cardinal.aleph_one_le_iff
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
α : Type u_1
inst : Uncountable α
⊢ (ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) 1 ≤ #α

Tactic:
simp
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
α : Type u_1
s : Set α
rw : s.Countable ↔ #(↑s : Type u_1) ≤ ℵ₀
rw₁ rw₂ : s.Countable ↔ s.Countable
⊢ s.Countable ↔ #(↑s : Type u_1) < (ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) 1

Tactic:
rw [lt_aleph_one_iff, le_aleph0_iff_set_countable]

Premises used: Cardinal.le_aleph0_iff_set_countable, Cardinal.lt_aleph_one_iff
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
o : Ordinal.{u_1}
ho : HPow.hPow (β := ℕ) ω 2 ≤ o
⊢ Eq (α := Cardinal.{u_1}) ((preAleph : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o : Cardinal.{u_1})
    ((ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o : Cardinal.{u_1})

Tactic:
simpa [← ord_inj] using preOmega_of_omega0_sq_le ho

Premises used: Cardinal.ord_inj, Ordinal.preOmega_of_omega0_sq_le
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
o : Ordinal.{u}
a : (↑(Iio o) : Type (u + 1))
⊢ (↑a : Ordinal.{u}) < o

Tactic:
a.2

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

Tactic:
exact a.2

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

Tactic:
decreasing_by exact a.2

Premises used: Subtype.property
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
a b : Ordinal.{u_1}
h : a < b
rw : ⨆ (a : (↑(Iio b) : Type (u_1 + 1))), HPow.hPow (α := Cardinal.{u_1}) 2 (preBeth (↑a : Ordinal.{u_1}))
| preBeth b

Tactic:
rw [preBeth]

Premises used: Cardinal.preBeth
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
a b : Ordinal.{u_1}
h : a < b
conv_rhs :
  preBeth a < ⨆ (a : (↑(Iio b) : Type (u_1 + 1))), HPow.hPow (α := Cardinal.{u_1}) 2 (preBeth (↑a : Ordinal.{u_1}))
⊢ preBeth a < preBeth b

Tactic:
conv_rhs => rw [preBeth]

Premises used: Cardinal.preBeth
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
a b : Ordinal.{u_1}
h : a < b
rw : ∃ (i : (↑(Iio b) : Type (u_1 + 1))), preBeth a < HPow.hPow (α := Cardinal.{u_1}) 2 (preBeth (↑i : Ordinal.{u_1}))
⊢ preBeth a < ⨆ (a : (↑(Iio b) : Type (u_1 + 1))), HPow.hPow (α := Cardinal.{u_1}) 2 (preBeth (↑a : Ordinal.{u_1}))

Tactic:
rw [lt_ciSup_iff' bddAbove_of_small]

Premises used: Cardinal.bddAbove_of_small, lt_ciSup_iff'
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
a b : Ordinal.{u_1}
h : a < b
⊢ ∃ (i : (↑(Iio b) : Type (u_1 + 1))), preBeth a < HPow.hPow (α := Cardinal.{u_1}) 2 (preBeth (↑i : Ordinal.{u_1}))

Tactic:
⟨⟨a, h⟩, cantor _⟩

Premises used: Subtype.mk, Cardinal.cantor, Exists.intro
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
a b : Ordinal.{u_1}
h : a < b
⊢ ∃ (i : (↑(Iio b) : Type (u_1 + 1))), preBeth a < HPow.hPow (α := Cardinal.{u_1}) 2 (preBeth (↑i : Ordinal.{u_1}))

Tactic:
exact ⟨⟨a, h⟩, cantor _⟩
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
⊢ Monotone preBeth

Tactic:
preBeth_strictMono.monotone

Premises used: StrictMono.monotone, Cardinal.preBeth_strictMono
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
o : Ordinal.{u_1}
⊢ (preAleph : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o ≤ preBeth o

Tactic:
preAleph_le_of_strictMono preBeth_strictMono o

Premises used: Cardinal.preAleph_le_of_strictMono, Cardinal.preBeth_strictMono
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
o₁ o₂ : Ordinal.{u_1}
⊢ preBeth o₁ < preBeth o₂ ↔ o₁ < o₂

Tactic:
preBeth_strictMono.lt_iff_lt

Premises used: StrictMono.lt_iff_lt, Cardinal.preBeth_strictMono
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
o₁ o₂ : Ordinal.{u_1}
⊢ preBeth o₁ ≤ preBeth o₂ ↔ o₁ ≤ o₂

Tactic:
preBeth_strictMono.le_iff_le

Premises used: Cardinal.preBeth_strictMono, StrictMono.le_iff_le
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
o₁ o₂ : Ordinal.{u_1}
⊢ preBeth o₁ = preBeth o₂ ↔ o₁ = o₂

Tactic:
preBeth_strictMono.injective.eq_iff

Premises used: Function.Injective.eq_iff, StrictMono.injective, Cardinal.preBeth_strictMono
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
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
⊢ preBeth 0 = 0

Tactic:
rw [preBeth]

Premises used: Cardinal.preBeth
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
⊢ 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:
simp
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
o : Ordinal.{u_1}
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)
⊢ preBeth (o + 1) = HPow.hPow (α := Cardinal.{u_1}) 2 (preBeth o)

Tactic:
rw [preBeth, ← succ_eq_add_one, Iio_succ]

Premises used: Order.succ_eq_add_one, Cardinal.preBeth, Order.Iio_succ
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
o : Ordinal.{u_1}
⊢ ⨆ (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:
ciSup_Iic o fun x y h ↦ power_le_power_left two_ne_zero (preBeth_mono h)

Premises used: ciSup_Iic, two_ne_zero, Cardinal.preBeth_mono, Cardinal.power_le_power_left
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
o : Ordinal.{u_1}
⊢ ⨆ (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:
exact ciSup_Iic o fun x y h ↦ power_le_power_left two_ne_zero (preBeth_mono h)

Premises used: ciSup_Iic, two_ne_zero, Cardinal.preBeth_mono, Cardinal.power_le_power_left
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
o : Ordinal.{u_1}
⊢ preBeth (succ o) = HPow.hPow (α := Cardinal.{u_1}) 2 (preBeth o)

Tactic:
preBeth_add_one o

Premises used: Order.succ, Cardinal.preBeth_add_one
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
o : Ordinal.{u_1}
ho : IsSuccPrelimit o
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}))
⊢ preBeth o = ⨆ (a : (↑(Iio o) : Type (u_1 + 1))), preBeth (↑a : Ordinal.{u_1})

Tactic:
rw [preBeth]

Premises used: Cardinal.preBeth
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
o : Ordinal.{u_1}
ho : IsSuccPrelimit o
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}))
⊢ 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:
apply (ciSup_mono bddAbove_of_small fun _ ↦ (cantor _).le).antisymm'

Premises used: LE.le.antisymm', LT.lt.le, Cardinal.cantor, Cardinal.bddAbove_of_small, ciSup_mono
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
o : Ordinal.{u_1}
ho : IsSuccPrelimit o
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})
⊢ 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:
rw [ciSup_le_iff' bddAbove_of_small]

Premises used: ciSup_le_iff', Cardinal.bddAbove_of_small
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
o : Ordinal.{u_1}
ho : IsSuccPrelimit o
a : (↑(Iio o) : Type (u_1 + 1))
rw : preBeth (succ (↑a : Ordinal.{u_1})) ≤ ⨆ (x : (↑(Iio o) : Type (u_1 + 1))), preBeth (↑x : Ordinal.{u_1})
⊢ HPow.hPow (α := Cardinal.{u_1}) 2 (preBeth (↑a : Ordinal.{u_1})) ≤
    ⨆ (x : (↑(Iio o) : Type (u_1 + 1))), preBeth (↑x : Ordinal.{u_1})

Tactic:
rw [← preBeth_succ]

Premises used: Cardinal.preBeth_succ
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
o : Ordinal.{u_1}
ho : IsSuccPrelimit o
a : (↑(Iio o) : Type (u_1 + 1))
⊢ preBeth (succ (↑a : Ordinal.{u_1})) ≤ ⨆ (x : (↑(Iio o) : Type (u_1 + 1))), preBeth (↑x : Ordinal.{u_1})

Tactic:
le_ciSup bddAbove_of_small (⟨_, ho.succ_lt a.2⟩ : Iio o)

Premises used: Order.succ, Subtype.mk, le_ciSup, Order.IsSuccPrelimit.succ_lt, Cardinal.bddAbove_of_small, Subtype.property
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
o : Ordinal.{u_1}
ho : IsSuccPrelimit o
a : (↑(Iio o) : Type (u_1 + 1))
⊢ preBeth (succ (↑a : Ordinal.{u_1})) ≤ ⨆ (x : (↑(Iio o) : Type (u_1 + 1))), preBeth (↑x : Ordinal.{u_1})

Tactic:
exact le_ciSup bddAbove_of_small (⟨_, ho.succ_lt a.2⟩ : Iio o)

Premises used: Subtype.mk, le_ciSup, Order.IsSuccPrelimit.succ_lt, Cardinal.bddAbove_of_small, Subtype.property
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
rw :
  StrictMono preBeth ∧
    ∀ (o : Ordinal.{u_1}), IsSuccLimit o → ∀ (a : Cardinal.{u_1}), (∀ b < o, preBeth b ≤ a) → preBeth o ≤ a
⊢ IsNormal preBeth

Tactic:
rw [isNormal_iff]

Premises used: Order.isNormal_iff
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
⊢ StrictMono preBeth ∧
    ∀ (o : Ordinal.{u_1}), IsSuccLimit o → ∀ (a : Cardinal.{u_1}), (∀ b < o, preBeth b ≤ a) → preBeth o ≤ a

Tactic:
⟨preBeth_strictMono, fun o ho ↦ ?_⟩

Premises used: And.intro, Cardinal.preBeth_strictMono
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
refine : ∀ (o : Ordinal.{u_1}) (ho : IsSuccLimit o) (a : Cardinal.{u_1}), (∀ b < o, preBeth b ≤ a) → preBeth o ≤ a
⊢ StrictMono preBeth ∧
    ∀ (o : Ordinal.{u_1}), IsSuccLimit o → ∀ (a : Cardinal.{u_1}), (∀ b < o, preBeth b ≤ a) → preBeth o ≤ a

Tactic:
refine ⟨preBeth_strictMono, fun o ho ↦ ?_⟩
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
o : Ordinal.{u_1}
ho : IsSuccLimit o
⊢ ∀ (a : Cardinal.{u_1}), (∀ b < o, preBeth b ≤ a) → preBeth o ≤ a

Tactic:
simp [preBeth_limit ho.isSuccPrelimit, ciSup_le_iff' bddAbove_of_small]

Premises used: ciSup_le_iff', Cardinal.preBeth_limit, Order.IsSuccLimit.isSuccPrelimit, Cardinal.bddAbove_of_small
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
⊢ preBeth (↑0 : Ordinal.{u_1}) = (↑((fun (x : ℕ) ↦ HPow.hPow (α := ℕ) 2 x)^[0] 0) : Cardinal.{u_1})

Tactic:
simp
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
n : ℕ
⊢ preBeth (↑(n + 1) : Ordinal.{u_1}) = (↑((fun (x : ℕ) ↦ HPow.hPow (α := ℕ) 2 x)^[n + 1] 0) : Cardinal.{u_1})

Tactic:
simp [Function.iterate_succ_apply', preBeth_nat]

Premises used: Function.iterate_succ_apply'
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
⊢ preBeth 1 = 1

Tactic:
simpa using preBeth_nat 1

Premises used: OfNat.ofNat, Cardinal.preBeth_nat
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
a : preBeth ω ≤ ℵ₀
a₁ : ℵ₀ ≤ preBeth ω
⊢ preBeth ω = ℵ₀

Tactic:
apply le_antisymm

Premises used: le_antisymm