-- Mathlib/SetTheory/Ordinal/Principal.lean
theorem mul_lt_omega0_opow (c0 : 0 < c) (ha : a < ω ^ c) (hb : b < ω) : a * b < ω ^ c

Proof state:
case inr.inr.intro.intro
a b c : Ordinal.{u}
c0 : 0 < c
ha : a < ω ^ c
hb : b < ω
l : c.IsLimit
x : Ordinal.{u}
hx : x < c
ax : a < ω ^ x
⊢ a * b < ω ^ c

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

Result:
case inr.inr.intro.intro
a b c : Ordinal.{u}
c0 : 0 < c
ha : a < ω ^ c
hb : b < ω
l : c.IsLimit
x : Ordinal.{u}
hx : x < c
ax : a < ω ^ x
⊢ ω ^ x * ω < ω ^ c

Proof state:
case inl
a b : Ordinal.{u}
hb : b < ω
c0 : 0 < 0
ha : a < ω ^ 0
⊢ a * b < ω ^ 0

Tactic:
exact (lt_irrefl _).elim c0

Result:
no goals

Proof state:
case inr.inr
a b c : Ordinal.{u}
c0 : 0 < c
ha : a < ω ^ c
hb : b < ω
l : c.IsLimit
⊢ a * b < ω ^ c

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

Result:
case inr.inr.intro.intro
a b c : Ordinal.{u}
c0 : 0 < c
ha : a < ω ^ c
hb : b < ω
l : c.IsLimit
x : Ordinal.{u}
hx : x < c
ax : a < ω ^ x
⊢ a * b < ω ^ c

Proof state:
case inr.inr.intro.intro
a b c : Ordinal.{u}
c0 : 0 < c
ha : a < ω ^ c
hb : b < ω
l : c.IsLimit
x : Ordinal.{u}
hx : x < c
ax : a < ω ^ x
⊢ succ x < c

Tactic:
exact l.succ_lt hx

Result:
no goals

Proof state:
case inr.inr.intro.intro
a b c : Ordinal.{u}
c0 : 0 < c
ha : a < ω ^ c
hb : b < ω
l : c.IsLimit
x : Ordinal.{u}
hx : x < c
ax : a < ω ^ x
⊢ ω ^ x * ω < ω ^ c

Tactic:
rw [← opow_succ, opow_lt_opow_iff_right one_lt_omega0]

Result:
case inr.inr.intro.intro
a b c : Ordinal.{u}
c0 : 0 < c
ha : a < ω ^ c
hb : b < ω
l : c.IsLimit
x : Ordinal.{u}
hx : x < c
ax : a < ω ^ x
⊢ succ x < c

Proof state:
case inr.inl.intro.intro.intro
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
⊢ ω ^ c * n * b < ω ^ succ c

Tactic:
rw [opow_succ, mul_assoc, mul_lt_mul_iff_left (opow_pos _ omega0_pos)]

Result:
case inr.inl.intro.intro.intro
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 < ω

Proof state:
case inr.inl.intro
a b : Ordinal.{u}
hb : b < ω
c : Ordinal.{u}
c0 : 0 < succ c
ha : a < ω ^ succ c
⊢ a * b < ω ^ succ c

Tactic:
rw [opow_succ] at ha

Result:
case inr.inl.intro
a b : Ordinal.{u}
hb : b < ω
c : Ordinal.{u}
c0 : 0 < succ c
ha : a < ω ^ c * ω
⊢ a * b < ω ^ succ c

Proof state:
case inr.inl.intro.intro.intro
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
⊢ a * b < ω ^ succ c

Tactic:
apply (mul_le_mul_right' (le_of_lt an) _).trans_lt

Result:
case inr.inl.intro.intro.intro
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
⊢ ω ^ c * n * b < ω ^ succ c

Proof state:
a b c : Ordinal.{u}
c0 : 0 < c
ha : a < ω ^ c
hb : b < ω
⊢ a * b < ω ^ c

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

Result:
case inl
a b : Ordinal.{u}
hb : b < ω
c0 : 0 < 0
ha : a < ω ^ 0
⊢ a * b < ω ^ 0

case inr.inl.intro
a b : Ordinal.{u}
hb : b < ω
c : Ordinal.{u}
c0 : 0 < succ c
ha : a < ω ^ succ c
⊢ a * b < ω ^ succ c

case inr.inr
a b c : Ordinal.{u}
c0 : 0 < c
ha : a < ω ^ c
hb : b < ω
l : c.IsLimit
⊢ a * b < ω ^ c

Proof state:
case inr.inl.intro
a b : Ordinal.{u}
hb : b < ω
c : Ordinal.{u}
c0 : 0 < succ c
ha : a < ω ^ c * ω
⊢ a * b < ω ^ succ c

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

Result:
case inr.inl.intro.intro.intro
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
⊢ a * b < ω ^ succ c

Proof state:
case inr.inl.intro.intro.intro
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:
exact principal_mul_omega0 hn hb

Result:
no goals