awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
m n : ℕ
rw :
  (↑n : Ordinal.{u_4}) * HDiv.hDiv (α := Ordinal.{u_4}) (↑m : Ordinal.{u_4}) (↑n : Ordinal.{u_4}) +
      (↑(m % n) : Ordinal.{u_4}) =
    (↑n : Ordinal.{u_4}) * HDiv.hDiv (α := Ordinal.{u_4}) (↑m : Ordinal.{u_4}) (↑n : Ordinal.{u_4}) +
      HMod.hMod (α := Ordinal.{u_4}) (↑m : Ordinal.{u_4}) (↑n : Ordinal.{u_4})
rw₁ : Ordinal.{u_4}
rw₂ :
  (↑n : Ordinal.{u_4}) * HDiv.hDiv (α := Ordinal.{u_4}) (↑m : Ordinal.{u_4}) (↑n : Ordinal.{u_4}) +
      (↑(m % n) : Ordinal.{u_4}) =
    (↑m : Ordinal.{u_4})
rw₃ :
  HMul.hMul (α := Ordinal.{u_4}) (↑n : Ordinal.{u_4}) (↑(m / n) : Ordinal.{u_4}) + (↑(m % n) : Ordinal.{u_4}) =
    (↑m : Ordinal.{u_4})
rw₄ : HAdd.hAdd (α := Ordinal.{u_4}) (↑(n * (m / n)) : Ordinal.{u_4}) (↑(m % n) : Ordinal.{u_4}) = (↑m : Ordinal.{u_4})
rw₅ : Eq.{u_4 + 2} (α := Ordinal.{u_4}) (↑(n * (m / n) + m % n) : Ordinal.{u_4}) (↑m : Ordinal.{u_4})
rw₆ rw₇ : Eq.{u_4 + 2} (α := Ordinal.{u_4}) (↑m : Ordinal.{u_4}) (↑m : Ordinal.{u_4})
⊢ (↑(m % n) : Ordinal.{u_4}) = HMod.hMod (α := Ordinal.{u_4}) (↑m : Ordinal.{u_4}) (↑n : Ordinal.{u_4})

Tactic:
rw [← add_left_cancel_iff, div_add_mod, ← natCast_div, ← natCast_mul, ← Nat.cast_add,
    Nat.div_add_mod]

Premises used: Ordinal.div_add_mod, Nat.div_add_mod, add_left_cancel_iff, Ordinal.natCast_mul, Nat.cast_add, Ordinal.natCast_div
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
⊢ lift.{u, v} (↑0 : Ordinal.{v}) = (↑0 : Ordinal.{max v u})

Tactic:
simp
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
n : ℕ
⊢ lift.{u, v} (↑(n + 1) : Ordinal.{v}) = (↑(n + 1) : Ordinal.{max v u})

Tactic:
simp [lift_natCast n]
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
n : ℕ
inst : n.AtLeastTwo
⊢ lift.{u, v} (OfNat.ofNat n) = OfNat.ofNat n

Tactic:
lift_natCast n

Premises used: Ordinal.lift_natCast
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
x : ℕ
have :
  ∀ (this : Fintype (↑(Iio x) : Type)),
    Eq (α := Ordinal.{0})
      ((PrincipalSeg.toRelEmbedding (r := LT.lt) (s := fun (x1 x2 : Ordinal.{0}) ↦ x1 < x2) (typein LT.lt) :
            (a : ℕ) → Ordinal.{0})
          x :
        Ordinal.{0})
      ((↑x : Ordinal.{0}) : Ordinal.{0})
⊢ Eq (α := Ordinal.{0})
    ((PrincipalSeg.toRelEmbedding (r := LT.lt) (s := fun (x1 x2 : Ordinal.{0}) ↦ x1 < x2) (typein LT.lt) :
          (a : ℕ) → Ordinal.{0})
        x :
      Ordinal.{0})
    ((↑x : Ordinal.{0}) : Ordinal.{0})

Tactic:
have : Fintype <| Iio x := Nat.fintypeIio x
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
x : ℕ
this : Fintype (↑(Iio x) : Type)
rw : Fintype.card (↑(Iio x) : Type) = x
⊢ Eq (α := Ordinal.{0})
    ((PrincipalSeg.toRelEmbedding (r := LT.lt) (s := fun (x1 x2 : Ordinal.{0}) ↦ x1 < x2) (typein LT.lt) :
          (a : ℕ) → Ordinal.{0})
        x :
      Ordinal.{0})
    ((↑x : Ordinal.{0}) : Ordinal.{0})

Tactic:
rw [← type_Iio_lt, type_fintype, Nat.cast_inj]

Premises used: Nat.cast_inj, Ordinal.type_fintype, Ordinal.type_Iio_lt
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
x : ℕ
this : Fintype (↑(Iio x) : Type)
nth_rw : Fintype.card (↑(Iio x) : Type) = Fintype.card (Fin x)
⊢ Fintype.card (↑(Iio x) : Type) = x

Tactic:
nth_rw 2 [← Fintype.card_fin x]

Premises used: Fintype.card_fin
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
x : ℕ
this : Fintype (↑(Iio x) : Type)
⊢ Fintype.card (↑(Iio x) : Type) = Fintype.card (Fin x)

Tactic:
Fintype.card_congr Fin.equivSubtype.symm

Premises used: Fintype.card_congr, Fin.equivSubtype, Equiv.symm
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
x : ℕ
this : Fintype (↑(Iio x) : Type)
⊢ Fintype.card (↑(Iio x) : Type) = Fintype.card (Fin x)

Tactic:
exact Fintype.card_congr Fin.equivSubtype.symm

Premises used: Fintype.card_congr, Fin.equivSubtype, Equiv.symm
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
n : ℕ
x : Fin n
rw : Fintype.card (↑(Iio x) : Type) = (↑x : ℕ)
⊢ Eq (α := Ordinal.{0})
    ((PrincipalSeg.toRelEmbedding (r := LT.lt) (s := fun (x1 x2 : Ordinal.{0}) ↦ x1 < x2) (typein LT.lt) :
          (a : Fin n) → Ordinal.{0})
        x :
      Ordinal.{0})
    ((↑(↑x : ℕ) : Ordinal.{0}) : Ordinal.{0})

Tactic:
rw [← type_Iio_lt, type_fintype, Nat.cast_inj]

Premises used: Nat.cast_inj, Ordinal.type_fintype, Ordinal.type_Iio_lt
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
n : ℕ
x : Fin n
⊢ Fintype.card (↑(Iio x) : Type) = (↑x : ℕ)

Tactic:
Fintype.card_fin_lt_of_le x.is_le'

Premises used: Set.Mem, setOf, Fintype.card_fin_lt_of_le, dite, Fin.is_le', Set.Iio, Nat.lt
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
n : ℕ
x : Fin n
⊢ Fintype.card (↑(Iio x) : Type) = (↑x : ℕ)

Tactic:
exact Fintype.card_fin_lt_of_le x.is_le'

Premises used: Fintype.card_fin_lt_of_le, Fin.is_le'
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
n : ℕ
x : Fin n
⊢ (↑(↑x : ℕ) : Ordinal.{0}) ∈ Iio (type (α := Fin n) LT.lt)

Tactic:
simp
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
n : ℕ
x : Fin n
⊢ (enum LT.lt : (a : (↑(Iio (type LT.lt)) : Type 1)) → Fin n)
      (Subtype.mk (p := fun (x : Ordinal.{0}) ↦ x ∈ Iio (type (α := Fin n) LT.lt)) (↑(↑x : ℕ) : Ordinal.{0}) ⋯) =
    x

Tactic:
simp [← typein_inj LT.lt]

Premises used: LT.lt, Ordinal.typein_inj
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
o : Ordinal.{u_4}
simp_rw : o < ℵ₀.ord ↔ ∃ (n : ℕ), o = (↑n : Ordinal.{u_4})
simp_rw₁ : o.card < ℵ₀ ↔ ∃ (n : ℕ), o = (↑n : Ordinal.{u_4})
simp_rw₂ : (∃ (n : ℕ), o.card = (↑n : Cardinal.{u_4})) ↔ ∃ (n : ℕ), o = (↑n : Ordinal.{u_4})
⊢ o < ω ↔ ∃ (n : ℕ), o = (↑n : Ordinal.{u_4})

Tactic:
simp_rw [← Cardinal.ord_aleph0, Cardinal.lt_ord, lt_aleph0, card_eq_nat]

Premises used: Cardinal.ord_aleph0, Ordinal.card_eq_nat, Cardinal.lt_aleph0, Cardinal.lt_ord
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
n : ℕ
⊢ (↑n : Ordinal.{u_4}) < ω

Tactic:
lt_omega0.2 ⟨_, rfl⟩

Premises used: Iff.mpr, Exists.intro, Ordinal.lt_omega0, rfl
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
x : ℕ
⊢ (↑x : Ordinal.{0}) ∈ Iio (type (α := ℕ) LT.lt)

Tactic:
simp
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
x : ℕ
⊢ (enum LT.lt : (a : (↑(Iio (type LT.lt)) : Type 1)) → ℕ)
      (Subtype.mk (p := fun (x : Ordinal.{0}) ↦ x ∈ Iio (type (α := ℕ) LT.lt)) (↑x : Ordinal.{0}) ⋯) =
    x

Tactic:
simp [← typein_inj LT.lt]

Premises used: LT.lt, Ordinal.typein_inj
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a : Ordinal.{u_4}
b : ℕ
h : a ≤ (↑b : Ordinal.{u_4})
⊢ ∃ (c : ℕ), a = (↑c : Ordinal.{u_4})

Tactic:
lt_omega0.1 (h.trans_lt (natCast_lt_omega0 b))

Premises used: Ordinal.natCast_lt_omega0, Iff.mp, Ordinal.lt_omega0, LE.le.trans_lt
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
o : Ordinal.{u_4}
inl : ∀ (ho : o < ω), (∃ (n : ℕ), o = (↑n : Ordinal.{u_4})) ∨ ω ≤ o
inr : ∀ (ho : ω ≤ o), (∃ (n : ℕ), o = (↑n : Ordinal.{u_4})) ∨ ω ≤ o
⊢ (∃ (n : ℕ), o = (↑n : Ordinal.{u_4})) ∨ ω ≤ o

Tactic:
obtain ho | ho := lt_or_ge o ω

Premises used: Ordinal.omega0, lt_or_ge
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
o : Ordinal.{u_4}
ho : o < ω
⊢ (∃ (n : ℕ), o = (↑n : Ordinal.{u_4})) ∨ ω ≤ o

Tactic:
Or.inl <| lt_omega0.1 ho

Premises used: Iff.mp, Or.inl, Ordinal.lt_omega0
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
o : Ordinal.{u_4}
ho : o < ω
⊢ (∃ (n : ℕ), o = (↑n : Ordinal.{u_4})) ∨ ω ≤ o

Tactic:
exact Or.inl <| lt_omega0.1 ho

Premises used: Iff.mp, Or.inl, Ordinal.lt_omega0
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
o : Ordinal.{u_4}
ho : ω ≤ o
⊢ (∃ (n : ℕ), o = (↑n : Ordinal.{u_4})) ∨ ω ≤ o

Tactic:
Or.inr ho

Premises used: Or.inr
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
o : Ordinal.{u_4}
ho : ω ≤ o
⊢ (∃ (n : ℕ), o = (↑n : Ordinal.{u_4})) ∨ ω ≤ o

Tactic:
exact Or.inr ho

Premises used: Or.inr
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
n : ℕ
h :
  ∀ (o : Ordinal.{u_4}),
    Membership.mem (γ := Set Ordinal.{u_4}) (Nat.cast '' Iio n) o ↔
      Membership.mem (γ := Set Ordinal.{u_4}) (Iio (↑n : Ordinal.{u_4})) o
⊢ Eq.{u_4 + 2} (α := Set Ordinal.{u_4}) (Nat.cast '' Iio n) (Iio (↑n : Ordinal.{u_4}))

Tactic:
ext o
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
n : ℕ
o : Ordinal.{u_4}
⊢ ∀ {b : ℕ} (h : o ≤ (↑b : Ordinal.{u_4})), ∃ (c : ℕ), o = (↑c : Ordinal.{u_4})

Tactic:
have := @eq_natCast_of_le_natCast o
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
n : ℕ
o : Ordinal.{u_4}
this : ∀ {b : ℕ} (h : o ≤ (↑b : Ordinal.{u_4})), ∃ (c : ℕ), o = (↑c : Ordinal.{u_4})
⊢ Membership.mem (γ := Set Ordinal.{u_4}) (Nat.cast '' Iio n) o ↔
    Membership.mem (γ := Set Ordinal.{u_4}) (Iio (↑n : Ordinal.{u_4})) o

Tactic:
grind [Nat.cast_lt]

Premises used: Nat.cast_lt
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
⊢ 0 < ω

Tactic:
natCast_lt_omega0 0

Premises used: Ordinal.natCast_lt_omega0, OfNat.ofNat
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
⊢ ω ≠ 0

Tactic:
omega0_pos.ne'

Premises used: Ordinal.omega0_pos, LT.lt.ne'
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
⊢ 1 < ω

Tactic:
simpa only [Nat.cast_one] using natCast_lt_omega0 1

Premises used: Ordinal.natCast_lt_omega0, OfNat.ofNat, Nat.cast_one
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
rw : ω ≠ 0 ∧ ∀ a < ω, succ a < ω
⊢ IsSuccLimit ω

Tactic:
rw [isSuccLimit_iff, isSuccPrelimit_iff_succ_lt]

Premises used: Order.isSuccPrelimit_iff_succ_lt, Ordinal.isSuccLimit_iff
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
⊢ ω ≠ 0 ∧ ∀ a < ω, succ a < ω

Tactic:
⟨omega0_ne_zero, fun o h => ?_⟩

Premises used: Ordinal.omega0_ne_zero, And.intro
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
refine : ∀ (o : Ordinal.{u_4}) (h : o < ω), succ o < ω
⊢ ω ≠ 0 ∧ ∀ a < ω, succ a < ω

Tactic:
refine ⟨omega0_ne_zero, fun o h => ?_⟩
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
o : Ordinal.{u_4}
h : o < ω
obtain : ∀ (n : ℕ) (h : (↑n : Ordinal.{u_4}) < ω), succ (↑n : Ordinal.{u_4}) < ω
⊢ succ o < ω

Tactic:
obtain ⟨n, rfl⟩ := lt_omega0.1 h

Premises used: Iff.mp, Ordinal.lt_omega0, rfl
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
n : ℕ
h : (↑n : Ordinal.{u_4}) < ω
⊢ succ (↑n : Ordinal.{u_4}) < ω

Tactic:
natCast_lt_omega0 (n + 1)

Premises used: Order.succ, Ordinal.natCast_lt_omega0, HAdd.hAdd, Nat.unaryCast, OfNat.ofNat
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
n : ℕ
h : (↑n : Ordinal.{u_4}) < ω
⊢ succ (↑n : Ordinal.{u_4}) < ω

Tactic:
exact natCast_lt_omega0 (n + 1)

Premises used: Ordinal.natCast_lt_omega0, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
o : Ordinal.{u_4}
H : ∀ (n : ℕ), (↑n : Ordinal.{u_4}) ≤ o
a : Ordinal.{u_4}
h : a < ω
let : ∀ (n : ℕ) (e : a = (↑n : Ordinal.{u_4})), a < o
⊢ a < o

Tactic:
let ⟨n, e⟩ := lt_omega0.1 h
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
o : Ordinal.{u_4}
H : ∀ (n : ℕ), (↑n : Ordinal.{u_4}) ≤ o
a : Ordinal.{u_4}
h : a < ω
n : ℕ
e : a = (↑n : Ordinal.{u_4})
rw : succ (↑n : Ordinal.{u_4}) ≤ o
⊢ a < o

Tactic:
rw [e, ← succ_le_iff]

Premises used: Order.succ_le_iff
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
o : Ordinal.{u_4}
H : ∀ (n : ℕ), (↑n : Ordinal.{u_4}) ≤ o
a : Ordinal.{u_4}
h : a < ω
n : ℕ
e : a = (↑n : Ordinal.{u_4})
⊢ succ (↑n : Ordinal.{u_4}) ≤ o

Tactic:
H (n + 1)

Premises used: Order.succ, HAdd.hAdd, Nat.unaryCast, OfNat.ofNat
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
o : Ordinal.{u_4}
H : ∀ (n : ℕ), (↑n : Ordinal.{u_4}) ≤ o
a : Ordinal.{u_4}
h : a < ω
n : ℕ
e : a = (↑n : Ordinal.{u_4})
⊢ succ (↑n : Ordinal.{u_4}) ≤ o

Tactic:
exact H (n + 1)

Premises used: HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
o : Ordinal.{u_4}
h : IsSuccLimit o
⊢ ω ≤ o

Tactic:
omega0_le.2 fun n => le_of_lt <| natCast_lt_of_isSuccLimit h n

Premises used: Iff.mpr, le_of_lt, Ordinal.omega0_le, Ordinal.natCast_lt_of_isSuccLimit
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
n : ℕ
⊢ (↑n : Ordinal.{u_4}) + ω = ω

Tactic:
le_antisymm (le_of_forall_lt fun a ha ↦ ?_) le_add_self

Premises used: le_of_forall_lt, le_antisymm, le_add_self
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
n : ℕ
refine : ∀ (a : Ordinal.{u_4}) (ha : a < (↑n : Ordinal.{u_4}) + ω), a < ω
⊢ (↑n : Ordinal.{u_4}) + ω = ω

Tactic:
refine le_antisymm (le_of_forall_lt fun a ha ↦ ?_) le_add_self

Premises used: le_of_forall_lt, le_antisymm, le_add_self
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
n : ℕ
a : Ordinal.{u_4}
ha : a < (↑n : Ordinal.{u_4}) + ω
obtain : ∀ (b : Ordinal.{u_4}) (hb' : b < ω) (hb : a ≤ (↑n : Ordinal.{u_4}) + b), a < ω
⊢ a < ω

Tactic:
obtain ⟨b, hb', hb⟩ := (lt_add_iff omega0_ne_zero).1 ha

Premises used: Ordinal.lt_add_iff, Ordinal.omega0_ne_zero, Iff.mp
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
n : ℕ
a : Ordinal.{u_4}
ha : a < (↑n : Ordinal.{u_4}) + ω
b : Ordinal.{u_4}
hb' : b < ω
hb : a ≤ (↑n : Ordinal.{u_4}) + b
obtain :
  ∀ (m : ℕ) (hb' : (↑m : Ordinal.{u_4}) < ω)
    (hb : a ≤ HAdd.hAdd (α := Ordinal.{u_4}) (↑n : Ordinal.{u_4}) (↑m : Ordinal.{u_4})), a < ω
⊢ a < ω

Tactic:
obtain ⟨m, rfl⟩ := lt_omega0.1 hb'

Premises used: Iff.mp, Ordinal.lt_omega0, rfl
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
n : ℕ
a : Ordinal.{u_4}
ha : a < (↑n : Ordinal.{u_4}) + ω
m : ℕ
hb' : (↑m : Ordinal.{u_4}) < ω
hb : a ≤ HAdd.hAdd (α := Ordinal.{u_4}) (↑n : Ordinal.{u_4}) (↑m : Ordinal.{u_4})
apply : HAdd.hAdd (α := Ordinal.{u_4}) (↑n : Ordinal.{u_4}) (↑m : Ordinal.{u_4}) < ω
⊢ a < ω

Tactic:
apply hb.trans_lt

Premises used: LE.le.trans_lt
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
n : ℕ
a : Ordinal.{u_4}
ha : a < (↑n : Ordinal.{u_4}) + ω
m : ℕ
hb' : (↑m : Ordinal.{u_4}) < ω
hb : a ≤ HAdd.hAdd (α := Ordinal.{u_4}) (↑n : Ordinal.{u_4}) (↑m : Ordinal.{u_4})
⊢ HAdd.hAdd (α := Ordinal.{u_4}) (↑n : Ordinal.{u_4}) (↑m : Ordinal.{u_4}) < ω

Tactic:
exact_mod_cast natCast_lt_omega0 (n + m)

Premises used: Ordinal.natCast_lt_omega0, HAdd.hAdd
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
⊢ 1 + ω = ω

Tactic:
mod_cast natCast_add_omega0 1

Premises used: Ordinal.omega0, congrArg, cast, HAdd.hAdd, congrFun', OfNat.ofNat, Eq.symm, Eq, Nat.cast_one, Ordinal.natCast_add_omega0, Eq.trans
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a : Ordinal.{u_4}
h : a < ω
obtain : ∀ (n : ℕ) (h : (↑n : Ordinal.{u_4}) < ω), (↑n : Ordinal.{u_4}) + ω = ω
⊢ a + ω = ω

Tactic:
obtain ⟨n, rfl⟩ := lt_omega0.1 h

Premises used: Iff.mp, Ordinal.lt_omega0, rfl
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
n : ℕ
h : (↑n : Ordinal.{u_4}) < ω
⊢ (↑n : Ordinal.{u_4}) + ω = ω

Tactic:
natCast_add_omega0 n

Premises used: Ordinal.natCast_add_omega0
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
n : ℕ
h : (↑n : Ordinal.{u_4}) < ω
⊢ (↑n : Ordinal.{u_4}) + ω = ω

Tactic:
exact natCast_add_omega0 n

Premises used: Ordinal.natCast_add_omega0
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
o : Ordinal.{u_4}
h : ω ≤ o
n : ℕ
rw : (↑n : Ordinal.{u_4}) + (ω + (o - ω)) = ω + (o - ω)
rw₁ : (↑n : Ordinal.{u_4}) + ω + (o - ω) = ω + (o - ω)
rw₂ rw₃ : ω + (o - ω) = ω + (o - ω)
⊢ (↑n : Ordinal.{u_4}) + o = o

Tactic:
rw [← Ordinal.add_sub_cancel_of_le h, ← add_assoc, natCast_add_omega0]

Premises used: add_assoc, Ordinal.add_sub_cancel_of_le, Ordinal.natCast_add_omega0
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
o : Ordinal.{u_4}
h : ω ≤ o
⊢ 1 + o = o

Tactic:
mod_cast natCast_add_of_omega0_le h 1

Premises used: congrArg, cast, Ordinal.natCast_add_of_omega0_le, HAdd.hAdd, congrFun', OfNat.ofNat, Eq.symm, Eq, Nat.cast_one, Eq.trans
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a : Ordinal.{u_4}
⊢ IsSuccPrelimit a ↔ ω ∣ a

Tactic:
⟨fun l => ⟨a / ω, le_antisymm ?_ (mul_div_le _ _)⟩, fun h => ?_⟩

Premises used: Ordinal.omega0, HDiv.hDiv, le_antisymm, Iff.intro, Exists.intro, Ordinal.mul_div_le
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a : Ordinal.{u_4}
refine_1 : ∀ (l : IsSuccPrelimit a), a ≤ ω * (a / ω)
refine_2 : ∀ (h : ω ∣ a), IsSuccPrelimit a
⊢ IsSuccPrelimit a ↔ ω ∣ a

Tactic:
refine ⟨fun l => ⟨a / ω, le_antisymm ?_ (mul_div_le _ _)⟩, fun h => ?_⟩
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a : Ordinal.{u_4}
l : IsSuccPrelimit a
⊢ a ≤ ω * (a / ω)

Tactic:
l.le_iff_forall_le.2 fun x hx => le_of_lt ?_

Premises used: Iff.mpr, Order.IsSuccPrelimit.le_iff_forall_le, le_of_lt
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a : Ordinal.{u_4}
l : IsSuccPrelimit a
refine_1 : ∀ (x : Ordinal.{u_4}) (hx : x < a), x < ω * (a / ω)
⊢ a ≤ ω * (a / ω)

Tactic:
refine l.le_iff_forall_le.2 fun x hx => le_of_lt ?_

Premises used: Iff.mpr, Order.IsSuccPrelimit.le_iff_forall_le, le_of_lt
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a : Ordinal.{u_4}
l : IsSuccPrelimit a
x : Ordinal.{u_4}
hx : x < a
refine_1 : ∀ d < ω, ω * (x / ω) + d ≤ a
⊢ x < ω * (a / ω)

Tactic:
rw [lt_mul_iff_div_lt omega0_ne_zero, ← succ_le_iff, ← mul_le_iff_le_div omega0_ne_zero,
      mul_succ, add_le_iff_of_isSuccLimit isSuccLimit_omega0]

Premises used: Ordinal.add_le_iff_of_isSuccLimit, Ordinal.isSuccLimit_omega0, Ordinal.lt_mul_iff_div_lt, Ordinal.omega0_ne_zero, Ordinal.mul_succ, Order.succ_le_iff, Ordinal.mul_le_iff_le_div
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a : Ordinal.{u_4}
l : IsSuccPrelimit a
x : Ordinal.{u_4}
hx : x < a
b : Ordinal.{u_4}
hb : b < ω
refine_1 : ∀ (n : ℕ) (hb : (↑n : Ordinal.{u_4}) < ω), ω * (x / ω) + (↑n : Ordinal.{u_4}) ≤ a
⊢ ω * (x / ω) + b ≤ a

Tactic:
rcases lt_omega0.1 hb with ⟨n, rfl⟩

Premises used: Iff.mp, Ordinal.lt_omega0, rfl
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a : Ordinal.{u_4}
l : IsSuccPrelimit a
x : Ordinal.{u_4}
hx : x < a
n : ℕ
hb : (↑n : Ordinal.{u_4}) < ω
refine_1 : x + (↑n : Ordinal.{u_4}) ≤ a
⊢ ω * (x / ω) + (↑n : Ordinal.{u_4}) ≤ a

Tactic:
grw [mul_div_le]

Premises used: Ordinal.mul_div_le
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a : Ordinal.{u_4}
l : IsSuccPrelimit a
x : Ordinal.{u_4}
hx : x < a
n : ℕ
hb : (↑n : Ordinal.{u_4}) < ω
⊢ x + (↑n : Ordinal.{u_4}) ≤ a

Tactic:
(lt_sub.1 <| natCast_lt_of_isSuccLimit (isSuccLimit_sub l hx) _).le

Premises used: Ordinal.lt_sub, LT.lt.le, Iff.mp, Ordinal.natCast_lt_of_isSuccLimit, Ordinal.isSuccLimit_sub
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a : Ordinal.{u_4}
l : IsSuccPrelimit a
x : Ordinal.{u_4}
hx : x < a
n : ℕ
hb : (↑n : Ordinal.{u_4}) < ω
⊢ x + (↑n : Ordinal.{u_4}) ≤ a

Tactic:
exact (lt_sub.1 <| natCast_lt_of_isSuccLimit (isSuccLimit_sub l hx) _).le

Premises used: Ordinal.lt_sub, LT.lt.le, Iff.mp, Ordinal.natCast_lt_of_isSuccLimit, Ordinal.isSuccLimit_sub
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a : Ordinal.{u_4}
h : ω ∣ a
refine_2 : ∀ (a0 : Ordinal.{u_4}), IsSuccPrelimit (ω * a0)
⊢ IsSuccPrelimit a

Tactic:
rcases h with ⟨a0, b, rfl⟩

Premises used: rfl
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a0 : Ordinal.{u_4}
⊢ IsSuccPrelimit (ω * a0)

Tactic:
isSuccPrelimit_mul_left isSuccLimit_omega0

Premises used: Ordinal.isSuccLimit_omega0, Ordinal.isSuccPrelimit_mul_left
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a0 : Ordinal.{u_4}
⊢ IsSuccPrelimit (ω * a0)

Tactic:
exact isSuccPrelimit_mul_left isSuccLimit_omega0

Premises used: Ordinal.isSuccLimit_omega0, Ordinal.isSuccPrelimit_mul_left
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a : Ordinal.{u_4}
rw : a ≠ 0 ∧ IsSuccPrelimit a ↔ a ≠ 0 ∧ ω ∣ a
rw₁ rw₂ : a ≠ 0 ∧ ω ∣ a ↔ a ≠ 0 ∧ ω ∣ a
⊢ IsSuccLimit a ↔ a ≠ 0 ∧ ω ∣ a

Tactic:
rw [isSuccLimit_iff, isSuccPrelimit_iff_omega0_dvd]

Premises used: Ordinal.isSuccLimit_iff, Ordinal.isSuccPrelimit_iff_omega0_dvd
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
n : ℕ
⊢ (↑n : Ordinal.{u_4}) % ω = (↑n : Ordinal.{u_4})

Tactic:
mod_eq_of_lt (natCast_lt_omega0 n)

Premises used: Ordinal.natCast_lt_omega0, Ordinal.mod_eq_of_lt
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
c : Cardinal.{u_1}
h : ℵ₀ ≤ c
rw : ω ≤ c.ord
⊢ c + 1 = c

Tactic:
rw [add_comm, ← card_ord c, ← card_one, ← card_add, one_add_of_omega0_le]

Premises used: Ordinal.card_one, Ordinal.one_add_of_omega0_le, Ordinal.card_add, add_comm, Cardinal.card_ord
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
c : Cardinal.{u_1}
h : ℵ₀ ≤ c
rwa : ℵ₀.ord ≤ c.ord
rwa₁ rwa₂ rwa₃ rwa₄ : ℵ₀ ≤ c
⊢ ω ≤ c.ord

Tactic:
rwa [← ord_aleph0, ord_le_ord]

Premises used: Cardinal.ord_aleph0, Cardinal.ord_le_ord
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
left : ¬IsMin c.ord
right : IsSuccPrelimit c.ord
⊢ IsSuccLimit c.ord

Tactic:
constructor
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
⊢ ¬IsMin c.ord

Tactic:
simpa using (aleph0_pos.trans_le hc).ne'

Premises used: LT.lt.ne', LT.lt.trans_le, Cardinal.aleph0_pos
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
right : ∀ (a : Ordinal.{u_1}), a.card < c → a.card + 1 < c
⊢ IsSuccPrelimit c.ord

Tactic:
simp_rw [isSuccPrelimit_iff_succ_lt, succ_eq_add_one, lt_ord, card_add_one]

Premises used: Ordinal.card_add_one, Order.succ_eq_add_one, Order.isSuccPrelimit_iff_succ_lt, Cardinal.lt_ord
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
⊢ ∀ (a : Ordinal.{u_1}), a.card < c → a.card + 1 < c

Tactic:
fun a ha ↦ ?_
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
right : ∀ (a : Ordinal.{u_1}) (ha : a.card < c), a.card + 1 < c
⊢ ∀ (a : Ordinal.{u_1}), a.card < c → a.card + 1 < c

Tactic:
refine fun a ha ↦ ?_
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
a : Ordinal.{u_1}
ha : a.card < c
right : ∀ (ha : c ≤ a.card + 1), c ≤ a.card
⊢ a.card + 1 < c

Tactic:
contrapose! ha
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
a : Ordinal.{u_1}
ha : c ≤ a.card + 1
right : ℵ₀ ≤ a.card
⊢ c ≤ a.card

Tactic:
rwa [add_one_of_aleph0_le] at ha

Premises used: Cardinal.add_one_of_aleph0_le
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
a : Ordinal.{u_1}
ha : c ≤ a.card + 1
right : ℵ₀ ≤ a.card + 1
right₁ : IsSuccLimit ℵ₀.ord
⊢ ℵ₀ ≤ a.card

Tactic:
rw [← ord_le, ← IsSuccLimit.le_succ_iff, succ_eq_add_one, ord_le, card_add_one]

Premises used: Ordinal.card_add_one, Order.succ_eq_add_one, Cardinal.ord_le, Order.IsSuccLimit.le_succ_iff
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
a : Ordinal.{u_1}
ha : c ≤ a.card + 1
⊢ ℵ₀ ≤ a.card + 1

Tactic:
hc.trans ha

Premises used: LE.le.trans
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
a : Ordinal.{u_1}
ha : c ≤ a.card + 1
⊢ ℵ₀ ≤ a.card + 1

Tactic:
exact hc.trans ha

Premises used: LE.le.trans
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
a : Ordinal.{u_1}
ha : c ≤ a.card + 1
⊢ IsSuccLimit ℵ₀.ord

Tactic:
simp
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
c : Cardinal.{u_1}
h : ℵ₀ ≤ c
rw : IsSuccPrelimit c.ord
⊢ NoMaxOrder.{u_1} c.ord.ToType

Tactic:
rw [← isSuccPrelimit_type_lt_iff, type_toType]

Premises used: Ordinal.isSuccPrelimit_type_lt_iff, Ordinal.type_toType
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
c : Cardinal.{u_1}
h : ℵ₀ ≤ c
⊢ IsSuccPrelimit c.ord

Tactic:
(isSuccLimit_ord h).isSuccPrelimit

Premises used: Cardinal.isSuccLimit_ord, Order.IsSuccLimit.isSuccPrelimit
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
c : Cardinal.{u_1}
h : ℵ₀ ≤ c
⊢ IsSuccPrelimit c.ord

Tactic:
exact (isSuccLimit_ord h).isSuccPrelimit

Premises used: Cardinal.isSuccLimit_ord, Order.IsSuccLimit.isSuccPrelimit
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
⊢ Nonempty.{u + 1} ℵ₀.ord.ToType

Tactic:
simp
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
α : Type u
β : Type v
γ : Type w
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o : Ordinal.{u_1}
⊢ WellFoundedLT.{u_1} o.ToType

Tactic:
o.out.wo.toIsWellFounded

Premises used: IsWellOrder.toIsWellFounded, Ordinal.ToType
-- Module: Mathlib.SetTheory.Ordinal.Basic
Goal:
o : Ordinal.{u_1}
⊢ (type fun (x1 x2 : o.ToType) ↦ x1 < x2) = o

Tactic:
o.out_eq

Premises used: Quot.out, Ordinal.type, Quotient.out, Classical.choose, Quotient.out_eq, Ordinal.ToType, Ordinal