case inl
a b c : Ordinal
h₁✝ : 0 < a
h₂ : b ≤ c
h₁ : 1 < a
⊢ a ^ b ≤ a ^ c

case inr
a b c : Ordinal
h₁✝ : 0 < a
h₂ : b ≤ c
h₁ : 1 = a
⊢ a ^ b ≤ a ^ c
a b c : Ordinal
h₁ : 0 < a
h₂ : b ≤ c
⊢ a ^ b ≤ a ^ c
cases' lt_or_eq_of_le (one_le_iff_pos.2 h₁) with h₁ h₁
no goals
case inl
a b c : Ordinal
h₁✝ : 0 < a
h₂ : b ≤ c
h₁ : 1 < a
⊢ a ^ b ≤ a ^ c
exact (opow_le_opow_iff_right h₁).2 h₂
case inr
b c : Ordinal
h₂ : b ≤ c
h₁ : 0 < 1
⊢ 1 ^ b ≤ 1 ^ c
case inr
a b c : Ordinal
h₁✝ : 0 < a
h₂ : b ≤ c
h₁ : 1 = a
⊢ a ^ b ≤ a ^ c
subst a
no goals
case inr
b c : Ordinal
h₂ : b ≤ c
h₁ : 0 < 1
⊢ 1 ^ b ≤ 1 ^ c
simp only [one_opow, le_refl]