case ofNat
α : Type ?u.409403
β : Type ?u.409406
a b c d : ℝ≥0∞
r p q : ℝ≥0
ha : a ≠ 0
h'a : a ≠ ⊤
a✝ : ℕ
⊢ 0 < a ^ Int.ofNat a✝

case negSucc
α : Type ?u.409403
β : Type ?u.409406
a b c d : ℝ≥0∞
r p q : ℝ≥0
ha : a ≠ 0
h'a : a ≠ ⊤
a✝ : ℕ
⊢ 0 < a ^ Int.negSucc a✝
α : Type ?u.409403
β : Type ?u.409406
a b c d : ℝ≥0∞
r p q : ℝ≥0
ha : a ≠ 0
h'a : a ≠ ⊤
n : ℤ
⊢ 0 < a ^ n
cases n
no goals
case ofNat
α : Type ?u.409403
β : Type ?u.409406
a b c d : ℝ≥0∞
r p q : ℝ≥0
ha : a ≠ 0
h'a : a ≠ ⊤
a✝ : ℕ
⊢ 0 < a ^ Int.ofNat a✝
exact ENNReal.pow_pos ha.bot_lt _
no goals
case negSucc
α : Type ?u.409403
β : Type ?u.409406
a b c d : ℝ≥0∞
r p q : ℝ≥0
ha : a ≠ 0
h'a : a ≠ ⊤
a✝ : ℕ
⊢ 0 < a ^ Int.negSucc a✝
simp only [h'a, pow_eq_top_iff, zpow_negSucc, Ne.def, not_false, ENNReal.inv_pos, false_and]