awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
x : Ordinal.{u_1}
rw : ω < x
| ω < (preOmega : (a : Ordinal.{u_1}) → Ordinal.{u_1}) x

Tactic:
rw [← preOmega_omega0, preOmega_lt_preOmega]

Premises used: Ordinal.preOmega_omega0, Ordinal.preOmega_lt_preOmega
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
x : Ordinal.{u_1}
conv_lhs : ω < (preOmega : (a : Ordinal.{u_1}) → Ordinal.{u_1}) x ↔ ω < x
conv_lhs₁ : ω < x ↔ ω < x
⊢ ω < (preOmega : (a : Ordinal.{u_1}) → Ordinal.{u_1}) x ↔ ω < x

Tactic:
conv_lhs => rw [← preOmega_omega0, preOmega_lt_preOmega]

Premises used: Ordinal.preOmega_omega0, Ordinal.preOmega_lt_preOmega
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
o : Ordinal.{u_1}
⊢ Eq (α := Ordinal.{u_1}) ((ω_ : (a : Ordinal.{u_1}) → Ordinal.{u_1}) o : Ordinal.{u_1})
    ((preOmega : (a : Ordinal.{u_1}) → Ordinal.{u_1}) (ω + o) : Ordinal.{u_1})

Tactic:
rfl

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

Tactic:
omega.strictMono

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

Tactic:
omega.lt_iff_lt

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

Tactic:
omega.le_iff_le

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

Tactic:
omega.monotone.map_max

Premises used: OrderEmbedding.monotone, Monotone.map_max, Ordinal.omega
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
o : Ordinal.{u_1}
⊢ LE.le (α := 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})

Tactic:
preOmega_le_preOmega.2 le_add_self

Premises used: Iff.mpr, Ordinal.preOmega_le_preOmega, le_add_self
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
o : Ordinal.{u_1}
⊢ IsInitial.{u_1} ((ω_ : (a : Ordinal.{u_1}) → Ordinal.{u_1}) o)

Tactic:
isInitial_preOmega _

Premises used: Ordinal.isInitial_preOmega
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
o : Ordinal.{u_1}
⊢ o ≤ (ω_ : (a : Ordinal.{u_1}) → Ordinal.{u_1}) o

Tactic:
omega_strictMono.le_apply

Premises used: StrictMono.le_apply, Ordinal.omega_strictMono
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
rw : (preOmega : (a : Ordinal.{u_1}) → Ordinal.{u_1}) (ω + 0) = ω
rw₁ : (preOmega : (a : Ordinal.{u_1}) → Ordinal.{u_1}) ω = ω
rw₂ rw₃ : ω = ω
⊢ (ω_ : (a : Ordinal.{u_1}) → Ordinal.{u_1}) 0 = ω

Tactic:
rw [omega_eq_preOmega, add_zero, preOmega_omega0]

Premises used: add_zero, Ordinal.preOmega_omega0, Ordinal.omega_eq_preOmega
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
o : Ordinal.{u_1}
rw : 0 ≤ o
⊢ ω ≤ (ω_ : (a : Ordinal.{u_1}) → Ordinal.{u_1}) o

Tactic:
rw [← omega_zero, omega_le_omega]

Premises used: Ordinal.omega_zero, Ordinal.omega_le_omega
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
o : Ordinal.{u_1}
⊢ 0 ≤ o

Tactic:
zero_le

Premises used: zero_le
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
o : Ordinal.{u_1}
⊢ 0 ≤ o

Tactic:
exact zero_le

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

Tactic:
omega0_pos.trans_le (omega0_le_omega o)

Premises used: Ordinal.omega0_pos, Ordinal.omega0_le_omega, LT.lt.trans_le
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
rw : LT.lt.{u_1 + 1} (α := Ordinal.{u_1}) 0 1
⊢ ω < (ω_ : (a : Ordinal.{u_1}) → Ordinal.{u_1}) 1

Tactic:
rw [← omega_zero, omega_lt_omega]

Premises used: Ordinal.omega_lt_omega, Ordinal.omega_zero
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
⊢ LT.lt.{u_1 + 1} (α := Ordinal.{u_1}) 0 1

Tactic:
zero_lt_one

Premises used: zero_lt_one
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
⊢ LT.lt.{u_1 + 1} (α := Ordinal.{u_1}) 0 1

Tactic:
exact zero_lt_one

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

Tactic:
isNormal_preOmega.comp (isNormal_add_right _)

Premises used: Ordinal.isNormal_preOmega, Order.IsNormal.comp, Ordinal.isNormal_add_right
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
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
⊢ Eq (α := Set Ordinal.{u_1}) (range (ι := Ordinal.{u_1}) (⇑ω_ : (a : Ordinal.{u_1}) → Ordinal.{u_1}))
    {x : Ordinal.{u_1} | ω ≤ x ∧ x.IsInitial}

Tactic:
ext x
-- Module: Mathlib.SetTheory.Cardinal.Aleph
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
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
⊢ 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
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
a : Ordinal.{u_1}
⊢ Membership.mem (α := Ordinal.{u_1}) (γ := Set Ordinal.{u_1}) {x : Ordinal.{u_1} | ω ≤ x ∧ x.IsInitial}
    ((ω_ : (a : Ordinal.{u_1}) → Ordinal.{u_1}) a : Ordinal.{u_1})

Tactic:
⟨omega0_le_omega a, isInitial_omega a⟩

Premises used: Set.Mem, setOf, Ordinal.omega0_le_omega, Ordinal.isInitial_omega, And.intro
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
a : Ordinal.{u_1}
⊢ Membership.mem (α := Ordinal.{u_1}) (γ := Set Ordinal.{u_1}) {x : Ordinal.{u_1} | ω ≤ x ∧ x.IsInitial}
    ((ω_ : (a : Ordinal.{u_1}) → Ordinal.{u_1}) a : Ordinal.{u_1})

Tactic:
exact ⟨omega0_le_omega a, isInitial_omega a⟩
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
x : Ordinal.{u_1}
ha' : ω ≤ x
ha : x.IsInitial
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})
⊢ Membership.mem (γ := Set Ordinal.{u_1}) (range (ι := Ordinal.{u_1}) (⇑ω_ : (a : Ordinal.{u_1}) → Ordinal.{u_1})) x

Tactic:
obtain ⟨a, rfl⟩ := ha.mem_range_preOmega

Premises used: Ordinal.IsInitial.mem_range_preOmega, rfl
-- Module: Mathlib.SetTheory.Cardinal.Aleph
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)
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})
⊢ 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:
use a - ω
-- Module: Mathlib.SetTheory.Cardinal.Aleph
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)
⊢ ω ≤ a

Tactic:
rw [omega0_le_preOmega_iff] at ha'

Premises used: Ordinal.omega0_le_preOmega_iff
-- Module: Mathlib.SetTheory.Cardinal.Aleph
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)
ha'₁ : ω ≤ a
⊢ IsInitial.{u_1} ((preOmega : (a : Ordinal.{u_1}) → Ordinal.{u_1}) a)

Tactic:
rw [omega0_le_preOmega_iff] at ha'

Premises used: Ordinal.omega0_le_preOmega_iff
-- Module: Mathlib.SetTheory.Cardinal.Aleph
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})
h₁ 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})

Tactic:
rw [omega_eq_preOmega, Ordinal.add_sub_cancel_of_le ha']

Premises used: Ordinal.add_sub_cancel_of_le, Ordinal.omega_eq_preOmega
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
x : Ordinal.{u_1}
rw : Membership.mem (γ := Set Ordinal.{u_1}) {x : Ordinal.{u_1} | ω ≤ x ∧ x.IsInitial} x ↔ ω ≤ x ∧ x.IsInitial
rw₁ rw₂ : ω ≤ x ∧ x.IsInitial ↔ ω ≤ x ∧ x.IsInitial
⊢ Membership.mem (γ := Set Ordinal.{u_1}) (range (ι := Ordinal.{u_1}) (⇑ω_ : (a : Ordinal.{u_1}) → Ordinal.{u_1})) x ↔
    ω ≤ x ∧ x.IsInitial

Tactic:
rw [range_omega, mem_setOf]

Premises used: Ordinal.range_omega, Set.mem_setOf
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
o : Ordinal.{u_1}
ho : HPow.hPow (β := ℕ) ω 2 ≤ o
⊢ HPow.hPow (β := Ordinal.{u_1}) ω (↑2 : Ordinal.{u_1}) ≤ o

Tactic:
rw [← opow_natCast] at ho

Premises used: Ordinal.opow_natCast
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
o : Ordinal.{u_1}
ho : HPow.hPow (β := Ordinal.{u_1}) ω (↑2 : Ordinal.{u_1}) ≤ o
rw : ω < HPow.hPow (β := Ordinal.{u_1}) ω (↑2 : Ordinal.{u_1})
⊢ 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})

Tactic:
rw [omega_eq_preOmega, add_of_omega0_opow_le _ ho]

Premises used: Ordinal.add_of_omega0_opow_le, Ordinal.omega_eq_preOmega
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
o : Ordinal.{u_1}
ho : HPow.hPow (β := Ordinal.{u_1}) ω (↑2 : Ordinal.{u_1}) ≤ o
apply : LT.lt.{u_1 + 1} (α := Ordinal.{u_1}) 1 (↑2 : Ordinal.{u_1})
⊢ ω < HPow.hPow (β := Ordinal.{u_1}) ω (↑2 : Ordinal.{u_1})

Tactic:
apply left_lt_opow one_lt_omega0

Premises used: Ordinal.left_lt_opow, Ordinal.one_lt_omega0
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
o : Ordinal.{u_1}
ho : HPow.hPow (β := Ordinal.{u_1}) ω (↑2 : Ordinal.{u_1}) ≤ o
⊢ LT.lt.{u_1 + 1} (α := Ordinal.{u_1}) 1 (↑2 : Ordinal.{u_1})

Tactic:
simp
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
o : Ordinal.{u_1}
⊢ card ((preOmega : (a : Ordinal.{u_1}) → Ordinal.{u_1}) o) = (preAleph : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o

Tactic:
rfl

Premises used: Quotient.map, Ordinal.card, Quot.map, rfl
-- Module: Mathlib.SetTheory.Cardinal.Aleph
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
rw₁ 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})
⊢ ord ((preAleph : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o) = (preOmega : (a : Ordinal.{u_1}) → Ordinal.{u_1}) o

Tactic:
rw [← o.card_preOmega, (isInitial_preOmega o).ord_card]

Premises used: Ordinal.isInitial_preOmega, Ordinal.IsInitial.ord_card, Ordinal.card_preOmega
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
⊢ (type fun (x1 x2 : Cardinal.{u}) ↦ x1 < x2) = Ordinal.univ.{u, u + 1}

Tactic:
simpa using preAleph.symm.toRelIsoLT.ordinal_type_eq

Premises used: OrderIso.toRelIsoLT, OrderIso.symm, Cardinal.preAleph, RelIso.ordinal_type_eq
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
⊢ #Cardinal.{u} = univ.{u, u + 1}

Tactic:
simpa only [card_type, card_univ] using congr_arg card type_lt_cardinal

Premises used: Ordinal.type_lt_cardinal, congr_arg, Ordinal.card, Ordinal.card_type, Ordinal.card_univ
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
⊢ cof Cardinal.{u} = univ.{u, u + 1}

Tactic:
simpa using preAleph.cof_congr.symm

Premises used: Cardinal.preAleph, Eq.symm, OrderIso.cof_congr
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
⊢ (type fun (x1 x2 : Cardinal.{u_1}) ↦ x1 < x2) ≤ (cof Cardinal.{u_1}).ord

Tactic:
simp [Order.cof_cardinal]

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

Tactic:
preAleph.lt_iff_lt

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

Tactic:
preAleph.le_iff_le

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

Tactic:
preAleph.monotone.map_max

Premises used: OrderIso.monotone, Monotone.map_max, Cardinal.preAleph
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
⊢ Eq (α := Cardinal.{u_1}) ((preAleph : (a : Ordinal.{u_1}) → Cardinal.{u_1}) 0) 0

Tactic:
preAleph.map_bot

Premises used: Cardinal.preAleph, OrderIso.map_bot
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
o : Ordinal.{u_1}
⊢ Eq (α := Cardinal.{u_1}) (succ ((preAleph : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o) : Cardinal.{u_1})
    ((preAleph : (a : Ordinal.{u_1}) → Cardinal.{u_1}) (o + 1) : Cardinal.{u_1})

Tactic:
(preAleph.map_succ o).symm

Premises used: Order.succ, OrderIso.map_succ, Cardinal.preAleph, Eq.symm
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
o : Ordinal.{u_1}
⊢ Eq (α := Cardinal.{u_1}) ((preAleph : (a : Ordinal.{u_1}) → Cardinal.{u_1}) (o + 1) : Cardinal.{u_1})
    (succ ((preAleph : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o) : Cardinal.{u_1})

Tactic:
preAleph.map_succ o

Premises used: Order.succ, OrderIso.map_succ, Cardinal.preAleph
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
o : Ordinal.{u_1}
⊢ Eq (α := Cardinal.{u_1}) ((preAleph : (a : Ordinal.{u_1}) → Cardinal.{u_1}) (succ o) : Cardinal.{u_1})
    (succ ((preAleph : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o) : Cardinal.{u_1})

Tactic:
preAleph.map_succ o

Premises used: OrderIso.map_succ, Cardinal.preAleph
-- Module: Mathlib.SetTheory.Cardinal.Aleph
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})
rw₂ rw₃ : Eq.{u_1 + 2} (α := Cardinal.{u_1}) (↑n : Cardinal.{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})

Tactic:
rw [← card_preOmega, preOmega_natCast, card_nat]

Premises used: Ordinal.card_preOmega, Ordinal.card_nat, Ordinal.preOmega_natCast
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
rw : card ((preOmega : (a : Ordinal.{u_1}) → Ordinal.{u_1}) ω) = ℵ₀
rw₁ : ω.card = ℵ₀
rw₂ rw₃ : ℵ₀ = ℵ₀
⊢ (preAleph : (a : Ordinal.{u_1}) → Cardinal.{u_1}) ω = ℵ₀

Tactic:
rw [← card_preOmega, preOmega_omega0, card_omega0]

Premises used: Ordinal.card_omega0, Ordinal.card_preOmega, Ordinal.preOmega_omega0
-- Module: Mathlib.SetTheory.Cardinal.Aleph
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
rw₁ rw₂ : 0 < o ↔ 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

Tactic:
rw [← preAleph_zero, preAleph_lt_preAleph]

Premises used: Cardinal.preAleph_zero, Cardinal.preAleph_lt_preAleph
-- Module: Mathlib.SetTheory.Cardinal.Aleph
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
rw₁ rw₂ : ω ≤ o ↔ ω ≤ o
⊢ ℵ₀ ≤ (preAleph : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o ↔ ω ≤ o

Tactic:
rw [← preAleph_omega0, preAleph_le_preAleph]

Premises used: Cardinal.preAleph_omega0, Cardinal.preAleph_le_preAleph
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
o : Ordinal.{u_1}
⊢ o.card ≤ (preAleph : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o

Tactic:
o.card_preOmega.trans_ge <| card_le_card <| o.le_preOmega_self

Premises used: Ordinal.card_le_card, Quotient.map, Eq.trans_ge, Ordinal.card, Ordinal.le_preOmega_self, Quot.map, Ordinal.card_preOmega
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
c : Cardinal.{u_1}
⊢ c ≤ (preAleph : (a : Ordinal.{u_1}) → Cardinal.{u_1}) c.ord

Tactic:
simpa using c.ord.card_le_preAleph

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

Tactic:
(preAleph.toInitialSeg.trans liftInitialSeg).eq
    (Ordinal.liftInitialSeg.trans preAleph.toInitialSeg) o

Premises used: OrderIso.toInitialSeg, setOf, Quotient.map, Cardinal.lift, Ordinal.lift, Ordinal.liftInitialSeg, Cardinal.preAleph, Cardinal.map, InitialSeg.trans, Cardinal.liftInitialSeg, Quot.map, InitialSeg.eq
-- Module: Mathlib.SetTheory.Cardinal.Aleph
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)
rw₃ 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})
⊢ 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)

Tactic:
rw [← ord_preAleph, lift_ord, lift_preAleph, ord_preAleph]

Premises used: Cardinal.lift_ord, Cardinal.ord_preAleph, Cardinal.lift_preAleph
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
⊢ IsNormal (α := Ordinal.{u_1}) (β := Cardinal.{u_1}) (⇑preAleph : (a : Ordinal.{u_1}) → Cardinal.{u_1})

Tactic:
OrderIso.isNormal _

Premises used: OrderIso.isNormal
-- Module: Mathlib.SetTheory.Cardinal.Aleph
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
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
⊢ (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

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
c : Cardinal.{u_1}
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:
simp
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
o : Ordinal.{u_1}
l : IsSuccPrelimit o
c : Cardinal.{u_1}
ho : o ≠ 0
⊢ ¬IsMin o

Tactic:
simpa
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
o : Ordinal.{u_1}
l : IsSuccPrelimit o
c : Cardinal.{u_1}
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:
exact isNormal_preAleph.le_iff_forall_le ⟨by simpa, l⟩

Premises used: Cardinal.isNormal_preAleph, Order.IsNormal.le_iff_forall_le, And.intro
-- Module: Mathlib.SetTheory.Cardinal.Aleph
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}))
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})
⊢ 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

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
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:
simp
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
o : Ordinal.{u_1}
ho : IsSuccPrelimit o
h : o ≠ 0
⊢ ¬IsMin o

Tactic:
simpa
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
o : Ordinal.{u_1}
ho : IsSuccPrelimit o
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:
exact isNormal_preAleph.apply_of_isSuccLimit ⟨by simpa, ho⟩

Premises used: Order.IsNormal.apply_of_isSuccLimit, Cardinal.isNormal_preAleph, And.intro
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
f : Ordinal.{u_1} → Cardinal.{u_1}
hf : StrictMono f
o : Ordinal.{u_1}
⊢ (preAleph : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o ≤ f o

Tactic:
simpa using (hf.comp preAleph.symm.strictMono).id_le (preAleph o)

Premises used: OrderIso.strictMono, OrderIso.symm, Cardinal.preAleph, StrictMono.id_le, StrictMono.comp, DFunLike.coe
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
o : Ordinal.{u_1}
⊢ Eq (α := Cardinal.{u_1}) ((ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o : Cardinal.{u_1})
    ((preAleph : (a : Ordinal.{u_1}) → Cardinal.{u_1}) (ω + o) : Cardinal.{u_1})

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.SetTheory.Cardinal.Aleph
Goal:
o : Ordinal.{u_1}
⊢ card ((ω_ : (a : Ordinal.{u_1}) → Ordinal.{u_1}) o) = (ℵ_ : (a : Ordinal.{u_1}) → Cardinal.{u_1}) o

Tactic:
rfl

Premises used: Quotient.map, Ordinal.card, Quot.map, rfl