a b : Ordinal
a0 : 0 < a
h0 : 0 < a ^ 0
⊢ 0 < a ^ b
a b : Ordinal
a0 : 0 < a
⊢ 0 < a ^ b
have h0 : 0 < (a^0) := by simp only [opow_zero, zero_lt_one]
case H₁
a b : Ordinal
a0 : 0 < a
h0 : 0 < a ^ 0
⊢ 0 < a ^ 0

case H₂
a b : Ordinal
a0 : 0 < a
h0 : 0 < a ^ 0
⊢ ∀ (o : Ordinal), 0 < a ^ o → 0 < a ^ succ o

case H₃
a b : Ordinal
a0 : 0 < a
h0 : 0 < a ^ 0
⊢ ∀ (o : Ordinal), IsLimit o → (∀ (o' : Ordinal), o' < o → 0 < a ^ o') → 0 < a ^ o
a b : Ordinal
a0 : 0 < a
h0 : 0 < a ^ 0
⊢ 0 < a ^ b
apply limitRecOn b
no goals
a b : Ordinal
a0 : 0 < a
⊢ 0 < a ^ 0
simp only [opow_zero, zero_lt_one]
no goals
case H₁
a b : Ordinal
a0 : 0 < a
h0 : 0 < a ^ 0
⊢ 0 < a ^ 0
exact h0
case H₂
a b✝ : Ordinal
a0 : 0 < a
h0 : 0 < a ^ 0
b : Ordinal
IH : 0 < a ^ b
⊢ 0 < a ^ succ b
case H₂
a b : Ordinal
a0 : 0 < a
h0 : 0 < a ^ 0
⊢ ∀ (o : Ordinal), 0 < a ^ o → 0 < a ^ succ o
intro b IH
case H₂
a b✝ : Ordinal
a0 : 0 < a
h0 : 0 < a ^ 0
b : Ordinal
IH : 0 < a ^ b
⊢ 0 < a ^ b * a
case H₂
a b✝ : Ordinal
a0 : 0 < a
h0 : 0 < a ^ 0
b : Ordinal
IH : 0 < a ^ b
⊢ 0 < a ^ succ b
rw [opow_succ]
no goals
case H₂
a b✝ : Ordinal
a0 : 0 < a
h0 : 0 < a ^ 0
b : Ordinal
IH : 0 < a ^ b
⊢ 0 < a ^ b * a
exact mul_pos IH a0
no goals
case H₃
a b : Ordinal
a0 : 0 < a
h0 : 0 < a ^ 0
⊢ ∀ (o : Ordinal), IsLimit o → (∀ (o' : Ordinal), o' < o → 0 < a ^ o') → 0 < a ^ o
exact fun b l _ => (lt_opow_of_limit (Ordinal.pos_iff_ne_zero.1 a0) l).2 ⟨0, l.pos, h0⟩