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

case negSucc
α : Type ?u.434875
β : Type ?u.434878
a b c d : ℝ≥0∞
r p q : ℝ≥0
ha : a ≠ 0
h'a : a ≠ ⊤
a✝ : ℕ
⊢ a ^ Int.negSucc a✝ < ⊤
α : Type ?u.434875
β : Type ?u.434878
a b c d : ℝ≥0∞
r p q : ℝ≥0
ha : a ≠ 0
h'a : a ≠ ⊤
n : ℤ
⊢ a ^ n < ⊤
cases n
no goals
case ofNat
α : Type ?u.434875
β : Type ?u.434878
a b c d : ℝ≥0∞
r p q : ℝ≥0
ha : a ≠ 0
h'a : a ≠ ⊤
a✝ : ℕ
⊢ a ^ Int.ofNat a✝ < ⊤
exact ENNReal.pow_lt_top h'a.lt_top _
no goals
case negSucc
α : Type ?u.434875
β : Type ?u.434878
a b c d : ℝ≥0∞
r p q : ℝ≥0
ha : a ≠ 0
h'a : a ≠ ⊤
a✝ : ℕ
⊢ a ^ Int.negSucc a✝ < ⊤
simp only [ENNReal.pow_pos ha.bot_lt, zpow_negSucc, inv_lt_top]