awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
o : Ordinal.{u}
ho : IsPrincipal (fun (x1 x2 : Ordinal.{u}) ↦ x1 * x2) o
ho₂ : o ≠ 2
ho₁ : o < 2
⊢ IsPrincipal (fun (x1 x2 : Ordinal.{u}) ↦ x1 + x2) o

Tactic:
isPrincipal_add_of_le_one <| lt_two_iff.mp ho₁

Premises used: Order.lt_two_iff, Iff.mp, Ordinal.isPrincipal_add_of_le_one
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
o : Ordinal.{u}
ho : IsPrincipal (fun (x1 x2 : Ordinal.{u}) ↦ x1 * x2) o
ho₂ : o ≠ 2
ho₁ : o < 2
⊢ IsPrincipal (fun (x1 x2 : Ordinal.{u}) ↦ x1 + x2) o

Tactic:
exact isPrincipal_add_of_le_one <| lt_two_iff.mp ho₁

Premises used: Order.lt_two_iff, Iff.mp, Ordinal.isPrincipal_add_of_le_one
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
o : Ordinal.{u}
ho : IsPrincipal (fun (x1 x2 : Ordinal.{u}) ↦ x1 * x2) o
ho₂_1 : o ≠ 2
ho₂ : 2 < o
inr : ∀ b < o, b * 2 < o
⊢ IsPrincipal (fun (x1 x2 : Ordinal.{u}) ↦ x1 + x2) o

Tactic:
simp_rw [isPrincipal_add_iff_add_self_lt, ← Ordinal.mul_two]

Premises used: Ordinal.isPrincipal_add_iff_add_self_lt, Ordinal.mul_two
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
o : Ordinal.{u}
ho : IsPrincipal (fun (x1 x2 : Ordinal.{u}) ↦ x1 * x2) o
ho₂_1 : o ≠ 2
ho₂ : 2 < o
⊢ ∀ b < o, b * 2 < o

Tactic:
fun a ha ↦ ho ha ho₂
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
o : Ordinal.{u}
ho : IsPrincipal (fun (x1 x2 : Ordinal.{u}) ↦ x1 * x2) o
ho₂_1 : o ≠ 2
ho₂ : 2 < o
⊢ ∀ b < o, b * 2 < o

Tactic:
exact fun a ha ↦ ho ha ho₂
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
o : Ordinal.{u}
ho₂ : 2 < o
ho : IsPrincipal (fun (x1 x2 : Ordinal.{u}) ↦ x1 * x2) o
⊢ IsSuccLimit o

Tactic:
isSuccLimit_of_isPrincipal_add (one_lt_two.trans ho₂)
    (isPrincipal_add_of_isPrincipal_mul ho (ne_of_gt ho₂))

Premises used: Ordinal.isPrincipal_add_of_isPrincipal_mul, ne_of_gt, Ordinal.isSuccLimit_of_isPrincipal_add, LT.lt.trans, one_lt_two
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
o : Ordinal.{u}
⊢ IsPrincipal (fun (x1 x2 : Ordinal.{u}) ↦ x1 * x2) o ↔ ∀ (a : Ordinal.{u}), 0 < a → a < o → a * o = o

Tactic:
⟨fun h a ha₀ hao => ?_, fun h a b hao hbo => ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
o : Ordinal.{u}
refine_1 :
  ∀ (h : IsPrincipal (fun (x1 x2 : Ordinal.{u}) ↦ x1 * x2) o) (a : Ordinal.{u}) (ha₀ : 0 < a) (hao : a < o), a * o = o
refine_2 :
  ∀ (h : ∀ (a : Ordinal.{u}), 0 < a → a < o → a * o = o) (a b : Ordinal.{u}) (hao : a < o) (hbo : b < o),
    (fun (x1 x2 : Ordinal.{u}) ↦ x1 * x2) a b < o
⊢ IsPrincipal (fun (x1 x2 : Ordinal.{u}) ↦ x1 * x2) o ↔ ∀ (a : Ordinal.{u}), 0 < a → a < o → a * o = o

Tactic:
refine ⟨fun h a ha₀ hao => ?_, fun h a b hao hbo => ?_⟩
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
o : Ordinal.{u}
h : IsPrincipal (fun (x1 x2 : Ordinal.{u}) ↦ x1 * x2) o
a : Ordinal.{u}
ha₀ : 0 < a
hao : a < o
refine_1 : ∀ (ho : o ≤ 2), a * o = o
refine_1₁ : ∀ (ho : 2 < o), a * o = o
⊢ a * o = o

Tactic:
rcases le_or_gt o 2 with ho | ho

Premises used: le_or_gt, OfNat.ofNat
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
o : Ordinal.{u}
h : IsPrincipal (fun (x1 x2 : Ordinal.{u}) ↦ x1 * x2) o
a : Ordinal.{u}
ha₀ : 0 < a
hao : a < o
ho : o ≤ 2
⊢ 1 * o = o

Tactic:
one_mul o

Premises used: one_mul
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
o : Ordinal.{u}
h : IsPrincipal (fun (x1 x2 : Ordinal.{u}) ↦ x1 * x2) o
a : Ordinal.{u}
ha₀ : 0 < a
hao : a < o
ho : o ≤ 2
h₁ : a = 1
⊢ a * o = o

Tactic:
convert! one_mul o

Premises used: one_mul
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
o : Ordinal.{u}
h : IsPrincipal (fun (x1 x2 : Ordinal.{u}) ↦ x1 * x2) o
a : Ordinal.{u}
ha₀ : 0 < a
hao : a < o
ho : o ≤ 2
h₁ : a ≤ 1
h₂ : 1 ≤ a
⊢ a = 1

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
o : Ordinal.{u}
h : IsPrincipal (fun (x1 x2 : Ordinal.{u}) ↦ x1 * x2) o
a : Ordinal.{u}
ha₀ : 0 < a
hao : a < o
ho : o ≤ 2
h₁ : a < 2
⊢ a ≤ 1

Tactic:
rw [← lt_add_one_iff, one_add_one_eq_two]

Premises used: one_add_one_eq_two, Order.lt_add_one_iff
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
o : Ordinal.{u}
h : IsPrincipal (fun (x1 x2 : Ordinal.{u}) ↦ x1 * x2) o
a : Ordinal.{u}
ha₀ : 0 < a
hao : a < o
ho : o ≤ 2
⊢ a < 2

Tactic:
hao.trans_le ho

Premises used: LT.lt.trans_le
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
o : Ordinal.{u}
h : IsPrincipal (fun (x1 x2 : Ordinal.{u}) ↦ x1 * x2) o
a : Ordinal.{u}
ha₀ : 0 < a
hao : a < o
ho : o ≤ 2
⊢ a < 2

Tactic:
exact hao.trans_le ho

Premises used: LT.lt.trans_le
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
o : Ordinal.{u}
h : IsPrincipal (fun (x1 x2 : Ordinal.{u}) ↦ x1 * x2) o
a : Ordinal.{u}
ha₀ : 0 < a
hao : a < o
ho : o ≤ 2
h₁ h₂ h₃ h₄ : 0 < a
⊢ 1 ≤ a

Tactic:
rwa [one_le_iff_pos]

Premises used: Order.one_le_iff_pos
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
o : Ordinal.{u}
h : IsPrincipal (fun (x1 x2 : Ordinal.{u}) ↦ x1 * x2) o
a : Ordinal.{u}
ha₀ : 0 < a
hao : a < o
ho : 2 < o
⊢ a * o = o

Tactic:
op_eq_self_of_isPrincipal hao (isNormal_mul_right ha₀) h
        (isSuccLimit_of_isPrincipal_mul ho h)

Premises used: Ordinal.isNormal_mul_right, Ordinal.isSuccLimit_of_isPrincipal_mul, Ordinal.op_eq_self_of_isPrincipal
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
o : Ordinal.{u}
h : IsPrincipal (fun (x1 x2 : Ordinal.{u}) ↦ x1 * x2) o
a : Ordinal.{u}
ha₀ : 0 < a
hao : a < o
ho : 2 < o
⊢ a * o = o

Tactic:
exact op_eq_self_of_isPrincipal hao (isNormal_mul_right ha₀) h
        (isSuccLimit_of_isPrincipal_mul ho h)

Premises used: Ordinal.isSuccLimit_of_isPrincipal_mul, Ordinal.op_eq_self_of_isPrincipal
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
o : Ordinal.{u}
h : ∀ (a : Ordinal.{u}), 0 < a → a < o → a * o = o
a b : Ordinal.{u}
hao : a < o
hbo : b < o
refine_2 : ∀ (hao : 0 < o), (fun (x1 x2 : Ordinal.{u}) ↦ x1 * x2) 0 b < o
refine_2₁ : ∀ (ha : a ≠ 0), (fun (x1 x2 : Ordinal.{u}) ↦ x1 * x2) a b < o
⊢ (fun (x1 x2 : Ordinal.{u}) ↦ x1 * x2) a b < o

Tactic:
rcases eq_or_ne a 0 with (rfl | ha)

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
o : Ordinal.{u}
h : ∀ (a : Ordinal.{u}), 0 < a → a < o → a * o = o
b : Ordinal.{u}
hbo : b < o
hao : 0 < o
refine_2 : 0 * b < o
⊢ (fun (x1 x2 : Ordinal.{u}) ↦ x1 * x2) 0 b < o

Tactic:
dsimp only
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
o : Ordinal.{u}
h : ∀ (a : Ordinal.{u}), 0 < a → a < o → a * o = o
b : Ordinal.{u}
hbo : b < o
hao : 0 < o
refine_2 refine_2₁ refine_2₂ refine_2₃ : 0 < o
⊢ 0 * b < o

Tactic:
rwa [zero_mul]

Premises used: MulZeroClass.zero_mul
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
o : Ordinal.{u}
h : ∀ (a : Ordinal.{u}), 0 < a → a < o → a * o = o
a b : Ordinal.{u}
hao : a < o
hbo : b < o
ha : a ≠ 0
⊢ 0 < a

Tactic:
rw [← pos_iff_ne_zero] at ha

Premises used: pos_iff_ne_zero
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
o : Ordinal.{u}
h : ∀ (a : Ordinal.{u}), 0 < a → a < o → a * o = o
a b : Ordinal.{u}
hao : a < o
hbo : b < o
ha : 0 < a
refine_2 : (fun (x1 x2 : Ordinal.{u}) ↦ x1 * x2) a b < a * o
⊢ (fun (x1 x2 : Ordinal.{u}) ↦ x1 * x2) a b < o

Tactic:
rw [← h a ha hao]
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
o : Ordinal.{u}
h : ∀ (a : Ordinal.{u}), 0 < a → a < o → a * o = o
a b : Ordinal.{u}
hao : a < o
hbo : b < o
ha : 0 < a
⊢ (fun (x1 x2 : Ordinal.{u}) ↦ x1 * x2) a b < a * o

Tactic:
(isNormal_mul_right ha).strictMono hbo

Premises used: Ordinal.isNormal_mul_right, Order.IsNormal.strictMono
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
o : Ordinal.{u}
h : ∀ (a : Ordinal.{u}), 0 < a → a < o → a * o = o
a b : Ordinal.{u}
hao : a < o
hbo : b < o
ha : 0 < a
⊢ (fun (x1 x2 : Ordinal.{u}) ↦ x1 * x2) a b < a * o

Tactic:
exact (isNormal_mul_right ha).strictMono hbo

Premises used: Ordinal.isNormal_mul_right, Order.IsNormal.strictMono
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
a b : Ordinal.{u_1}
m n : ℕ
ha : (↑m : Ordinal.{u_1}) < ω
hb : (↑n : Ordinal.{u_1}) < ω
dsimp : HMul.hMul (α := Ordinal.{u_1}) (↑m : Ordinal.{u_1}) (↑n : Ordinal.{u_1}) < ω
⊢ (fun (x1 x2 : Ordinal.{u_1}) ↦ x1 * x2) (↑m : Ordinal.{u_1}) (↑n : Ordinal.{u_1}) < ω

Tactic:
dsimp only
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
a b : Ordinal.{u_1}
m n : ℕ
ha : (↑m : Ordinal.{u_1}) < ω
hb : (↑n : Ordinal.{u_1}) < ω
rw : (↑(m * n) : Ordinal.{u_1}) < ω
⊢ HMul.hMul (α := Ordinal.{u_1}) (↑m : Ordinal.{u_1}) (↑n : Ordinal.{u_1}) < ω

Tactic:
rw [← natCast_mul]

Premises used: Ordinal.natCast_mul
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
a b : Ordinal.{u_1}
m n : ℕ
ha : (↑m : Ordinal.{u_1}) < ω
hb : (↑n : Ordinal.{u_1}) < ω
⊢ (↑(m * n) : Ordinal.{u_1}) < ω

Tactic:
apply natCast_lt_omega0

Premises used: Ordinal.natCast_lt_omega0
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
a : Ordinal.{u}
a0 : 0 < a
ha : a < ω
⊢ a * ω = ω

Tactic:
isPrincipal_mul_iff_mul_left_eq.1 isPrincipal_mul_omega0 a a0 ha

Premises used: Ordinal.isPrincipal_mul_omega0, Iff.mp, Ordinal.isPrincipal_mul_iff_mul_left_eq
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
n : ℕ
hn : 0 < n
⊢ (↑n : Ordinal.{u_1}) * ω = ω

Tactic:
mul_omega0 (mod_cast hn) (natCast_lt_omega0 n)

Premises used: congrArg, Nat.cast_lt._simp_1, cast, Nat.cast, Ordinal.natCast_lt_omega0, LT.lt, congrFun', Nat.cast_zero, Eq.symm, Ordinal.mul_omega0, Eq.trans
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
a b c : Ordinal.{u}
c0 : 0 < c
ha : a < ω ^ c
hb : b < ω
inl :
  ∀ (c0 : LT.lt.{u + 1} (α := Ordinal.{u}) 0 0) (ha : a < HPow.hPow (β := Ordinal.{u}) ω 0),
    a * b < HPow.hPow (β := Ordinal.{u}) ω 0
inr : ∀ (c : Ordinal.{u}) (c0 : 0 < succ c) (ha : a < ω ^ succ c), a * b < ω ^ succ c
inr₁ : ∀ (l : IsSuccLimit c), a * b < ω ^ c
⊢ a * b < ω ^ c

Tactic:
rcases zero_or_succ_or_isSuccLimit c with (rfl | ⟨c, rfl⟩ | l)

Premises used: Ordinal.zero_or_succ_or_isSuccLimit, rfl
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
a b : Ordinal.{u}
hb : b < ω
c0 : LT.lt.{u + 1} (α := Ordinal.{u}) 0 0
ha : a < HPow.hPow (β := Ordinal.{u}) ω 0
⊢ a * b < HPow.hPow (β := Ordinal.{u}) ω 0

Tactic:
(lt_irrefl _).elim c0

Premises used: lt_irrefl, Not.elim
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
a b : Ordinal.{u}
hb : b < ω
c0 : LT.lt.{u + 1} (α := Ordinal.{u}) 0 0
ha : a < HPow.hPow (β := Ordinal.{u}) ω 0
⊢ a * b < HPow.hPow (β := Ordinal.{u}) ω 0

Tactic:
exact (lt_irrefl _).elim c0

Premises used: lt_irrefl, Not.elim
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
a b : Ordinal.{u}
hb : b < ω
c : Ordinal.{u}
c0 : 0 < succ c
ha : a < ω ^ succ c
⊢ a < ω ^ c * ω

Tactic:
rw [opow_succ] at ha

Premises used: Ordinal.opow_succ
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
a b : Ordinal.{u}
hb : b < ω
c : Ordinal.{u}
c0 : 0 < succ c
ha : a < ω ^ c * ω
inr : ∀ (n : Ordinal.{u}) (hn : n < ω) (an : a < ω ^ c * n), a * b < ω ^ succ c
⊢ a * b < ω ^ succ c

Tactic:
obtain ⟨n, hn, an⟩ :=
      ((isNormal_mul_right <| opow_pos _ omega0_pos).lt_iff_exists_lt isSuccLimit_omega0).1 ha

Premises used: Ordinal.isNormal_mul_right, Ordinal.isSuccLimit_omega0, Ordinal.omega0_pos, Order.IsNormal.lt_iff_exists_lt, Iff.mp, Ordinal.opow_pos
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
a b : Ordinal.{u}
hb : b < ω
c : Ordinal.{u}
c0 : 0 < succ c
ha : a < ω ^ c * ω
n : Ordinal.{u}
hn : n < ω
an : a < ω ^ c * n
inr : ω ^ c * (n * b) < ω ^ c * ω
⊢ a * b < ω ^ succ c

Tactic:
grw [an, opow_succ, mul_assoc]

Premises used: mul_assoc, Ordinal.opow_succ
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
a b : Ordinal.{u}
hb : b < ω
c : Ordinal.{u}
c0 : 0 < succ c
ha : a < ω ^ c * ω
n : Ordinal.{u}
hn : n < ω
an : a < ω ^ c * n
inr : 0 < ω ^ c
inr₁ : n * b < ω
⊢ ω ^ c * (n * b) < ω ^ c * ω

Tactic:
gcongr
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
a b : Ordinal.{u}
hb : b < ω
c : Ordinal.{u}
c0 : 0 < succ c
ha : a < ω ^ c * ω
n : Ordinal.{u}
hn : n < ω
an : a < ω ^ c * n
⊢ 0 < ω ^ c

Tactic:
opow_pos _ omega0_pos

Premises used: Ordinal.omega0_pos, Ordinal.opow_pos
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
a b : Ordinal.{u}
hb : b < ω
c : Ordinal.{u}
c0 : 0 < succ c
ha : a < ω ^ c * ω
n : Ordinal.{u}
hn : n < ω
an : a < ω ^ c * n
⊢ n * b < ω

Tactic:
isPrincipal_mul_omega0 hn hb

Premises used: Ordinal.isPrincipal_mul_omega0
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
a b : Ordinal.{u}
hb : b < ω
c : Ordinal.{u}
c0 : 0 < succ c
ha : a < ω ^ c * ω
n : Ordinal.{u}
hn : n < ω
an : a < ω ^ c * n
⊢ 0 < ω ^ c

Tactic:
exacts [opow_pos _ omega0_pos, isPrincipal_mul_omega0 hn hb]

Premises used: Ordinal.omega0_pos, Ordinal.isPrincipal_mul_omega0, Ordinal.opow_pos
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
a b c : Ordinal.{u}
c0 : 0 < c
ha : a < ω ^ c
hb : b < ω
l : IsSuccLimit c
inr : ∀ (x : Ordinal.{u}) (hx : x < c) (ax : a < ω ^ x), a * b < ω ^ c
⊢ a * b < ω ^ c

Tactic:
rcases ((isNormal_opow one_lt_omega0).lt_iff_exists_lt l).1 ha with ⟨x, hx, ax⟩

Premises used: Ordinal.isNormal_opow, Order.IsNormal.lt_iff_exists_lt, Iff.mp, Ordinal.one_lt_omega0
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
a b c : Ordinal.{u}
c0 : 0 < c
ha : a < ω ^ c
hb : b < ω
l : IsSuccLimit c
x : Ordinal.{u}
hx : x < c
ax : a < ω ^ x
⊢ a * b < ω ^ c

Tactic:
(mul_le_mul' (le_of_lt ax) (le_of_lt hb)).trans_lt ?_

Premises used: le_of_lt, LE.le.trans_lt, mul_le_mul'
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
a b c : Ordinal.{u}
c0 : 0 < c
ha : a < ω ^ c
hb : b < ω
l : IsSuccLimit c
x : Ordinal.{u}
hx : x < c
ax : a < ω ^ x
inr : ω ^ x * ω < ω ^ c
⊢ a * b < ω ^ c

Tactic:
refine (mul_le_mul' (le_of_lt ax) (le_of_lt hb)).trans_lt ?_

Premises used: le_of_lt, LE.le.trans_lt, mul_le_mul'
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
a b c : Ordinal.{u}
c0 : 0 < c
ha : a < ω ^ c
hb : b < ω
l : IsSuccLimit c
x : Ordinal.{u}
hx : x < c
ax : a < ω ^ x
inr : succ x < c
⊢ ω ^ x * ω < ω ^ c

Tactic:
rw [← opow_succ, opow_lt_opow_iff_right one_lt_omega0]

Premises used: Ordinal.opow_lt_opow_iff_right, Ordinal.opow_succ, Ordinal.one_lt_omega0
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
a b c : Ordinal.{u}
c0 : 0 < c
ha : a < ω ^ c
hb : b < ω
l : IsSuccLimit c
x : Ordinal.{u}
hx : x < c
ax : a < ω ^ x
⊢ succ x < c

Tactic:
l.succ_lt hx

Premises used: Order.IsSuccLimit.succ_lt
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
a b c : Ordinal.{u}
c0 : 0 < c
ha : a < ω ^ c
hb : b < ω
l : IsSuccLimit c
x : Ordinal.{u}
hx : x < c
ax : a < ω ^ x
⊢ succ x < c

Tactic:
exact l.succ_lt hx

Premises used: Order.IsSuccLimit.succ_lt
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
a b : Ordinal.{u}
a0 : 0 < a
h : a < ω ^ ω ^ b
inl :
  ∀ (h : a < ω ^ HPow.hPow (β := Ordinal.{u}) ω 0),
    a * ω ^ HPow.hPow (β := Ordinal.{u}) ω 0 = ω ^ HPow.hPow (β := Ordinal.{u}) ω 0
inr : ∀ (b0 : b ≠ 0), a * ω ^ ω ^ b = ω ^ ω ^ b
⊢ a * ω ^ ω ^ b = ω ^ ω ^ b

Tactic:
obtain rfl | b0 := eq_or_ne b 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
a : Ordinal.{u}
a0 : 0 < a
h : a < ω ^ HPow.hPow (β := Ordinal.{u}) ω 0
inl : ∀ (h : a < ω), a * ω = ω
⊢ a * ω ^ HPow.hPow (β := Ordinal.{u}) ω 0 = ω ^ HPow.hPow (β := Ordinal.{u}) ω 0

Tactic:
rw [opow_zero, opow_one] at h ⊢

Premises used: Ordinal.opow_one, Ordinal.opow_zero
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
a : Ordinal.{u}
a0 : 0 < a
h : a < ω
⊢ a * ω = ω

Tactic:
mul_omega0 a0 h

Premises used: Ordinal.mul_omega0
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
a : Ordinal.{u}
a0 : 0 < a
h : a < ω
⊢ a * ω = ω

Tactic:
exact mul_omega0 a0 h

Premises used: Ordinal.mul_omega0
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
a b : Ordinal.{u}
a0 : 0 < a
h : a < ω ^ ω ^ b
b0 : b ≠ 0
inr : a * ω ^ ω ^ b ≤ ω ^ ω ^ b
inr₁ : ω ^ ω ^ b ≤ a * ω ^ ω ^ b
⊢ a * ω ^ ω ^ b = ω ^ ω ^ b

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
a b : Ordinal.{u}
a0 : 0 < a
h : a < ω ^ ω ^ b
b0 : b ≠ 0
inr : ∀ (x : Ordinal.{u}) (xb : x < ω ^ b) (ax : a < ω ^ x), a * ω ^ ω ^ b ≤ ω ^ ω ^ b
⊢ a * ω ^ ω ^ b ≤ ω ^ ω ^ b

Tactic:
obtain ⟨x, xb, ax⟩ :=
        (lt_opow_of_isSuccLimit omega0_ne_zero (isSuccLimit_opow_left isSuccLimit_omega0 b0)).1 h

Premises used: Ordinal.isSuccLimit_omega0, Ordinal.isSuccLimit_opow_left, Ordinal.omega0_ne_zero, Iff.mp, Ordinal.lt_opow_of_isSuccLimit
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
a b : Ordinal.{u}
a0 : 0 < a
h : a < ω ^ ω ^ b
b0 : b ≠ 0
x : Ordinal.{u}
xb : x < ω ^ b
ax : a < ω ^ x
inr : ω ^ x * ω ^ ω ^ b ≤ ω ^ ω ^ b
inr₁ : ω ^ (x + ω ^ b) ≤ ω ^ ω ^ b
inr₂ inr₃ : ω ^ ω ^ b ≤ ω ^ ω ^ b
⊢ a * ω ^ ω ^ b ≤ ω ^ ω ^ b

Tactic:
grw [ax, ← opow_add, add_omega0_opow xb]

Premises used: Ordinal.opow_add, Ordinal.add_omega0_opow
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
a b : Ordinal.{u}
a0 : 0 < a
h : a < ω ^ ω ^ b
b0 : b ≠ 0
rw : 1 * ω ^ ω ^ b
| ω ^ ω ^ b

Tactic:
rw [← one_mul (ω ^ _)]

Premises used: Ordinal.omega0, HPow.hPow, one_mul
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
a b : Ordinal.{u}
a0 : 0 < a
h : a < ω ^ ω ^ b
b0 : b ≠ 0
inr : 1 * ω ^ ω ^ b ≤ a * ω ^ ω ^ b
⊢ ω ^ ω ^ b ≤ a * ω ^ ω ^ b

Tactic:
conv_lhs => rw [← one_mul (ω ^ _)]

Premises used: Ordinal.omega0, HPow.hPow, one_mul
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
a b : Ordinal.{u}
a0 : 0 < a
h : a < ω ^ ω ^ b
b0 : b ≠ 0
inr inr₁ : a * ω ^ ω ^ b ≤ a * ω ^ ω ^ b
⊢ 1 * ω ^ ω ^ b ≤ a * ω ^ ω ^ b

Tactic:
grw [one_le_iff_pos.2 a0]

Premises used: Iff.mpr, Order.one_le_iff_pos
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
o : Ordinal.{u_1}
⊢ IsPrincipal.{u_1} (fun (x1 x2 : Ordinal.{u_1}) ↦ x1 * x2) (ω ^ ω ^ o)

Tactic:
isPrincipal_mul_iff_mul_left_eq.2 fun _ => mul_omega0_opow_opow

Premises used: Iff.mpr, Ordinal.mul_omega0_opow_opow, Ordinal.isPrincipal_mul_iff_mul_left_eq
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
b o : Ordinal.{u}
hb : 1 < b
ho : IsPrincipal.{u} (fun (x1 x2 : Ordinal.{u}) ↦ x1 * x2) (b ^ o)
x y : Ordinal.{u}
hx : x < o
hy : y < o
⊢ (fun (x1 x2 : Ordinal.{u}) ↦ x1 * x2) (b ^ x) (b ^ y) < b ^ o

Tactic:
have := ho ((opow_lt_opow_iff_right hb).2 hx) ((opow_lt_opow_iff_right hb).2 hy)
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
b o : Ordinal.{u}
hb : 1 < b
ho : IsPrincipal.{u} (fun (x1 x2 : Ordinal.{u}) ↦ x1 * x2) (b ^ o)
x y : Ordinal.{u}
hx : x < o
hy : y < o
this : (fun (x1 x2 : Ordinal.{u}) ↦ x1 * x2) (b ^ x) (b ^ y) < b ^ o
dsimp : x + y < o
⊢ (fun (x1 x2 : Ordinal.{u}) ↦ x1 + x2) x y < o

Tactic:
dsimp only at *
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
b o : Ordinal.{u}
hb : 1 < b
ho : IsPrincipal.{u} (fun (x1 x2 : Ordinal.{u}) ↦ x1 * x2) (b ^ o)
x y : Ordinal.{u}
hx : x < o
hy : y < o
this : b ^ x * b ^ y < b ^ o
rwa : ∀ (this : b ^ (x + y) < b ^ o), x + y < o
rwa₁ rwa₂ rwa₃ rwa₄ : ∀ (this : x + y < o), x + y < o
⊢ x + y < o

Tactic:
rwa [← opow_add, opow_lt_opow_iff_right hb] at this

Premises used: Ordinal.opow_add, Ordinal.opow_lt_opow_iff_right
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
o : Ordinal.{u}
⊢ IsPrincipal (fun (x1 x2 : Ordinal.{u}) ↦ x1 * x2) o ↔
    o ≤ 2 ∨ Membership.mem (γ := Set Ordinal.{u}) (Set.range fun (x : Ordinal.{u}) ↦ ω ^ ω ^ x) o

Tactic:
⟨fun ho => ?_, ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
o : Ordinal.{u}
refine_1 :
  ∀ (ho : IsPrincipal (fun (x1 x2 : Ordinal.{u}) ↦ x1 * x2) o),
    o ≤ 2 ∨ Membership.mem (γ := Set Ordinal.{u}) (Set.range fun (x : Ordinal.{u}) ↦ ω ^ ω ^ x) o
refine_2 :
  o ≤ 2 ∨ Membership.mem (γ := Set Ordinal.{u}) (Set.range fun (x : Ordinal.{u}) ↦ ω ^ ω ^ x) o →
    IsPrincipal (fun (x1 x2 : Ordinal.{u}) ↦ x1 * x2) o
⊢ IsPrincipal (fun (x1 x2 : Ordinal.{u}) ↦ x1 * x2) o ↔
    o ≤ 2 ∨ Membership.mem (γ := Set Ordinal.{u}) (Set.range fun (x : Ordinal.{u}) ↦ ω ^ ω ^ x) o

Tactic:
refine ⟨fun ho => ?_, ?_⟩
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
o : Ordinal.{u}
ho : IsPrincipal (fun (x1 x2 : Ordinal.{u}) ↦ x1 * x2) o
refine_1 :
  ∀ (ho₂ : o ≤ 2), o ≤ 2 ∨ Membership.mem (γ := Set Ordinal.{u}) (Set.range fun (x : Ordinal.{u}) ↦ ω ^ ω ^ x) o
refine_1₁ :
  ∀ (ho₂ : 2 < o), o ≤ 2 ∨ Membership.mem (γ := Set Ordinal.{u}) (Set.range fun (x : Ordinal.{u}) ↦ ω ^ ω ^ x) o
⊢ o ≤ 2 ∨ Membership.mem (γ := Set Ordinal.{u}) (Set.range fun (x : Ordinal.{u}) ↦ ω ^ ω ^ x) o

Tactic:
rcases le_or_gt o 2 with ho₂ | ho₂

Premises used: le_or_gt, OfNat.ofNat
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
o : Ordinal.{u}
ho : IsPrincipal (fun (x1 x2 : Ordinal.{u}) ↦ x1 * x2) o
ho₂ : o ≤ 2
⊢ o ≤ 2 ∨ Membership.mem (γ := Set Ordinal.{u}) (Set.range fun (x : Ordinal.{u}) ↦ ω ^ ω ^ x) o

Tactic:
Or.inl ho₂

Premises used: Or.inl
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
o : Ordinal.{u}
ho : IsPrincipal (fun (x1 x2 : Ordinal.{u}) ↦ x1 * x2) o
ho₂ : o ≤ 2
⊢ o ≤ 2 ∨ Membership.mem (γ := Set Ordinal.{u}) (Set.range fun (x : Ordinal.{u}) ↦ ω ^ ω ^ x) o

Tactic:
exact Or.inl ho₂

Premises used: Or.inl
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
o : Ordinal.{u}
ho : IsPrincipal (fun (x1 x2 : Ordinal.{u}) ↦ x1 * x2) o
ho₂ : 2 < o
refine_1 :
  ∀ (ho : IsPrincipal.{u} (fun (x1 x2 : Ordinal.{u}) ↦ x1 * x2) 0) (ho₂ : LT.lt.{u + 1} (α := Ordinal.{u}) 2 0),
    LE.le.{u + 1} (α := Ordinal.{u}) 0 2 ∨
      Membership.mem (γ := Set Ordinal.{u}) (Set.range fun (x : Ordinal.{u}) ↦ ω ^ ω ^ x) 0
refine_1₁ :
  ∀ (a : Ordinal.{u}) (ho : IsPrincipal.{u} (fun (x1 x2 : Ordinal.{u}) ↦ x1 * x2) ((fun (x : Ordinal.{u}) ↦ ω ^ x) a))
    (ho₂ : LT.lt.{u + 1} (α := Ordinal.{u}) 2 ((fun (x : Ordinal.{u}) ↦ ω ^ x) a)),
    LE.le.{u + 1} (α := Ordinal.{u}) ((fun (x : Ordinal.{u}) ↦ ω ^ x) a) 2 ∨
      Membership.mem (γ := Set Ordinal.{u}) (Set.range fun (x : Ordinal.{u}) ↦ ω ^ ω ^ x)
        ((fun (x : Ordinal.{u}) ↦ ω ^ x) a)
⊢ o ≤ 2 ∨ Membership.mem (γ := Set Ordinal.{u}) (Set.range fun (x : Ordinal.{u}) ↦ ω ^ ω ^ x) o

Tactic:
rcases isPrincipal_add_iff_zero_or_omega0_opow.1
        (isPrincipal_add_of_isPrincipal_mul ho ho₂.ne') with (rfl | ⟨a, rfl⟩)

Premises used: Ordinal.isPrincipal_add_iff_zero_or_omega0_opow, Ordinal.isPrincipal_add_of_isPrincipal_mul, LT.lt.ne', Iff.mp, rfl
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
ho : IsPrincipal.{u} (fun (x1 x2 : Ordinal.{u}) ↦ x1 * x2) 0
ho₂ : LT.lt.{u + 1} (α := Ordinal.{u}) 2 0
⊢ LE.le.{u + 1} (α := Ordinal.{u}) 0 2 ∨
    Membership.mem (γ := Set Ordinal.{u}) (Set.range fun (x : Ordinal.{u}) ↦ ω ^ ω ^ x) 0

Tactic:
(not_lt_zero ho₂).elim

Premises used: False.elim, not_lt_zero
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
ho : IsPrincipal.{u} (fun (x1 x2 : Ordinal.{u}) ↦ x1 * x2) 0
ho₂ : LT.lt.{u + 1} (α := Ordinal.{u}) 2 0
⊢ LE.le.{u + 1} (α := Ordinal.{u}) 0 2 ∨
    Membership.mem (γ := Set Ordinal.{u}) (Set.range fun (x : Ordinal.{u}) ↦ ω ^ ω ^ x) 0

Tactic:
exact (not_lt_zero ho₂).elim

Premises used: False.elim, not_lt_zero