-- Mathlib/SetTheory/Ordinal/Notation.lean
theorem NFBelow.repr_lt {o b} (h : NFBelow o b) : repr o < ω ^ b

Proof state:
case zero
o : ONote
b b✝ : Ordinal.{0}
⊢ repr 0 < ω ^ b✝

Tactic:
exact opow_pos _ omega0_pos

Result:
no goals

Proof state:
o : ONote
b : Ordinal.{0}
h : o.NFBelow b
⊢ o.repr < ω ^ b

Tactic:
induction h with
| zero => exact opow_pos _ omega0_pos
| oadd' _ _ h₃ _ IH =>
  rw [repr]
  apply ((add_lt_add_iff_left _).2 IH).trans_le
  rw [← mul_succ]
  apply (mul_le_mul_left' (succ_le_of_lt (nat_lt_omega0 _)) _).trans
  rw [← opow_succ]
  exact opow_le_opow_right omega0_pos (succ_le_of_lt h₃)

Result:
no goals

Proof state:
case oadd'
o : ONote
b : Ordinal.{0}
e✝ : ONote
n✝ : ℕ+
a✝² : ONote
eb✝ b✝ : Ordinal.{0}
a✝¹ : e✝.NFBelow eb✝
a✝ : a✝².NFBelow e✝.repr
h₃ : e✝.repr < b✝
a_ih✝ : e✝.repr < ω ^ eb✝
IH : a✝².repr < ω ^ e✝.repr
⊢ ω ^ e✝.repr * ↑↑n✝ + a✝².repr < ω ^ b✝

Tactic:
apply ((add_lt_add_iff_left _).2 IH).trans_le

Result:
case oadd'
o : ONote
b : Ordinal.{0}
e✝ : ONote
n✝ : ℕ+
a✝² : ONote
eb✝ b✝ : Ordinal.{0}
a✝¹ : e✝.NFBelow eb✝
a✝ : a✝².NFBelow e✝.repr
h₃ : e✝.repr < b✝
a_ih✝ : e✝.repr < ω ^ eb✝
IH : a✝².repr < ω ^ e✝.repr
⊢ ω ^ e✝.repr * ↑↑n✝ + ω ^ e✝.repr ≤ ω ^ b✝

Proof state:
case oadd'
o : ONote
b : Ordinal.{0}
e✝ : ONote
n✝ : ℕ+
a✝² : ONote
eb✝ b✝ : Ordinal.{0}
a✝¹ : e✝.NFBelow eb✝
a✝ : a✝².NFBelow e✝.repr
h₃ : e✝.repr < b✝
a_ih✝ : e✝.repr < ω ^ eb✝
IH : a✝².repr < ω ^ e✝.repr
⊢ ω ^ e✝.repr * succ ↑↑n✝ ≤ ω ^ b✝

Tactic:
apply (mul_le_mul_left' (succ_le_of_lt (nat_lt_omega0 _)) _).trans

Result:
case oadd'
o : ONote
b : Ordinal.{0}
e✝ : ONote
n✝ : ℕ+
a✝² : ONote
eb✝ b✝ : Ordinal.{0}
a✝¹ : e✝.NFBelow eb✝
a✝ : a✝².NFBelow e✝.repr
h₃ : e✝.repr < b✝
a_ih✝ : e✝.repr < ω ^ eb✝
IH : a✝².repr < ω ^ e✝.repr
⊢ ω ^ e✝.repr * ω ≤ ω ^ b✝

Proof state:
case oadd'
o : ONote
b : Ordinal.{0}
e✝ : ONote
n✝ : ℕ+
a✝² : ONote
eb✝ b✝ : Ordinal.{0}
a✝¹ : e✝.NFBelow eb✝
a✝ : a✝².NFBelow e✝.repr
h₃ : e✝.repr < b✝
a_ih✝ : e✝.repr < ω ^ eb✝
IH : a✝².repr < ω ^ e✝.repr
⊢ (e✝.oadd n✝ a✝²).repr < ω ^ b✝

Tactic:
rw [repr]

Result:
case oadd'
o : ONote
b : Ordinal.{0}
e✝ : ONote
n✝ : ℕ+
a✝² : ONote
eb✝ b✝ : Ordinal.{0}
a✝¹ : e✝.NFBelow eb✝
a✝ : a✝².NFBelow e✝.repr
h₃ : e✝.repr < b✝
a_ih✝ : e✝.repr < ω ^ eb✝
IH : a✝².repr < ω ^ e✝.repr
⊢ ω ^ e✝.repr * ↑↑n✝ + a✝².repr < ω ^ b✝

Proof state:
case oadd'
o : ONote
b : Ordinal.{0}
e✝ : ONote
n✝ : ℕ+
a✝² : ONote
eb✝ b✝ : Ordinal.{0}
a✝¹ : e✝.NFBelow eb✝
a✝ : a✝².NFBelow e✝.repr
h₃ : e✝.repr < b✝
a_ih✝ : e✝.repr < ω ^ eb✝
IH : a✝².repr < ω ^ e✝.repr
⊢ ω ^ e✝.repr * ↑↑n✝ + ω ^ e✝.repr ≤ ω ^ b✝

Tactic:
rw [← mul_succ]

Result:
case oadd'
o : ONote
b : Ordinal.{0}
e✝ : ONote
n✝ : ℕ+
a✝² : ONote
eb✝ b✝ : Ordinal.{0}
a✝¹ : e✝.NFBelow eb✝
a✝ : a✝².NFBelow e✝.repr
h₃ : e✝.repr < b✝
a_ih✝ : e✝.repr < ω ^ eb✝
IH : a✝².repr < ω ^ e✝.repr
⊢ ω ^ e✝.repr * succ ↑↑n✝ ≤ ω ^ b✝

Proof state:
case oadd'
o : ONote
b : Ordinal.{0}
e✝ : ONote
n✝ : ℕ+
a✝² : ONote
eb✝ b✝ : Ordinal.{0}
a✝¹ : e✝.NFBelow eb✝
a✝ : a✝².NFBelow e✝.repr
h₃ : e✝.repr < b✝
a_ih✝ : e✝.repr < ω ^ eb✝
IH : a✝².repr < ω ^ e✝.repr
⊢ ω ^ succ e✝.repr ≤ ω ^ b✝

Tactic:
exact opow_le_opow_right omega0_pos (succ_le_of_lt h₃)

Result:
no goals

Proof state:
case oadd'
o : ONote
b : Ordinal.{0}
e✝ : ONote
n✝ : ℕ+
a✝² : ONote
eb✝ b✝ : Ordinal.{0}
a✝¹ : e✝.NFBelow eb✝
a✝ : a✝².NFBelow e✝.repr
h₃ : e✝.repr < b✝
a_ih✝ : e✝.repr < ω ^ eb✝
IH : a✝².repr < ω ^ e✝.repr
⊢ ω ^ e✝.repr * ω ≤ ω ^ b✝

Tactic:
rw [← opow_succ]

Result:
case oadd'
o : ONote
b : Ordinal.{0}
e✝ : ONote
n✝ : ℕ+
a✝² : ONote
eb✝ b✝ : Ordinal.{0}
a✝¹ : e✝.NFBelow eb✝
a✝ : a✝².NFBelow e✝.repr
h₃ : e✝.repr < b✝
a_ih✝ : e✝.repr < ω ^ eb✝
IH : a✝².repr < ω ^ e✝.repr
⊢ ω ^ succ e✝.repr ≤ ω ^ b✝