case inl
a b : Ordinal
l : IsLimit a
hb : b ≠ 0
e : b = 0
⊢ IsLimit (a ^ b)

case inr.inl.intro
a : Ordinal
l : IsLimit a
b : Ordinal
hb : succ b ≠ 0
⊢ IsLimit (a ^ succ b)

case inr.inr
a b : Ordinal
l : IsLimit a
hb : b ≠ 0
l' : IsLimit b
⊢ IsLimit (a ^ b)
a b : Ordinal
l : IsLimit a
hb : b ≠ 0
⊢ IsLimit (a ^ b)
rcases zero_or_succ_or_limit b with (e | ⟨b, rfl⟩ | l')
no goals
case inl
a b : Ordinal
l : IsLimit a
hb : b ≠ 0
e : b = 0
⊢ IsLimit (a ^ b)
exact absurd e hb
case inr.inl.intro
a : Ordinal
l : IsLimit a
b : Ordinal
hb : succ b ≠ 0
⊢ IsLimit (a ^ b * a)
case inr.inl.intro
a : Ordinal
l : IsLimit a
b : Ordinal
hb : succ b ≠ 0
⊢ IsLimit (a ^ succ b)
rw [opow_succ]
no goals
case inr.inl.intro
a : Ordinal
l : IsLimit a
b : Ordinal
hb : succ b ≠ 0
⊢ IsLimit (a ^ b * a)
exact mul_isLimit (opow_pos _ l.pos) l
no goals
case inr.inr
a b : Ordinal
l : IsLimit a
hb : b ≠ 0
l' : IsLimit b
⊢ IsLimit (a ^ b)
exact opow_isLimit l.one_lt l'