a b : Ordinal
b1 : 0 < b
⊢ a ^ 1 ≤ a ^ b
a b : Ordinal
b1 : 0 < b
⊢ a ≤ a ^ b
nth_rw 1 [← opow_one a]
case inl
a b : Ordinal
b1 : 0 < b
a1 : a ≤ 1
⊢ a ^ 1 ≤ a ^ b

case inr
a b : Ordinal
b1 : 0 < b
a1 : a > 1
⊢ a ^ 1 ≤ a ^ b
a b : Ordinal
b1 : 0 < b
⊢ a ^ 1 ≤ a ^ b
cases' le_or_gt a 1 with a1 a1
no goals
case inr
a b : Ordinal
b1 : 0 < b
a1 : a > 1
⊢ a ^ 1 ≤ a ^ b
rwa [opow_le_opow_iff_right a1, one_le_iff_pos]
case inl.inl
a b : Ordinal
b1 : 0 < b
a1 : a ≤ 1
a0 : a < 1
⊢ a ^ 1 ≤ a ^ b

case inl.inr
a b : Ordinal
b1 : 0 < b
a1✝ : a ≤ 1
a1 : a = 1
⊢ a ^ 1 ≤ a ^ b
case inl
a b : Ordinal
b1 : 0 < b
a1 : a ≤ 1
⊢ a ^ 1 ≤ a ^ b
cases' lt_or_eq_of_le a1 with a0 a1
no goals
case inl.inr
a b : Ordinal
b1 : 0 < b
a1✝ : a ≤ 1
a1 : a = 1
⊢ a ^ 1 ≤ a ^ b
rw [a1, one_opow, one_opow]
case inl.inl
a b : Ordinal
b1 : 0 < b
a1 : a ≤ 1
a0 : a = 0
⊢ a ^ 1 ≤ a ^ b
case inl.inl
a b : Ordinal
b1 : 0 < b
a1 : a ≤ 1
a0 : a < 1
⊢ a ^ 1 ≤ a ^ b
rw [lt_one_iff_zero] at a0
case inl.inl
a b : Ordinal
b1 : 0 < b
a1 : a ≤ 1
a0 : a = 0
⊢ 0 ≤ 0 ^ b
case inl.inl
a b : Ordinal
b1 : 0 < b
a1 : a ≤ 1
a0 : a = 0
⊢ a ^ 1 ≤ a ^ b
rw [a0, zero_opow Ordinal.one_ne_zero]
no goals
case inl.inl
a b : Ordinal
b1 : 0 < b
a1 : a ≤ 1
a0 : a = 0
⊢ 0 ≤ 0 ^ b
exact Ordinal.zero_le _