case inl
α : Type ?u.95091
β : Type ?u.95094
a b c d : ℝ≥0∞
r p q : ℝ≥0
⊢ a ^ 0 = ⊤ ↔ a = ⊤ ∧ 0 ≠ 0

case inr
α : Type ?u.95091
β : Type ?u.95094
a b c d : ℝ≥0∞
r p q : ℝ≥0
n : ℕ
hn : 0 < n
⊢ a ^ n = ⊤ ↔ a = ⊤ ∧ n ≠ 0
α : Type ?u.95091
β : Type ?u.95094
a b c d : ℝ≥0∞
r p q : ℝ≥0
n : ℕ
⊢ a ^ n = ⊤ ↔ a = ⊤ ∧ n ≠ 0
rcases n.eq_zero_or_pos with rfl | (hn : 0 < n)
no goals
case inl
α : Type ?u.95091
β : Type ?u.95094
a b c d : ℝ≥0∞
r p q : ℝ≥0
⊢ a ^ 0 = ⊤ ↔ a = ⊤ ∧ 0 ≠ 0
simp
case inr.top
α : Type ?u.95091
β : Type ?u.95094
a b c d : ℝ≥0∞
r p q : ℝ≥0
n : ℕ
hn : 0 < n
⊢ ⊤ ^ n = ⊤ ↔ ⊤ = ⊤ ∧ n ≠ 0

case inr.coe
α : Type ?u.95091
β : Type ?u.95094
a b c d : ℝ≥0∞
r p q : ℝ≥0
n : ℕ
hn : 0 < n
x✝ : ℝ≥0
⊢ ↑x✝ ^ n = ⊤ ↔ ↑x✝ = ⊤ ∧ n ≠ 0
case inr
α : Type ?u.95091
β : Type ?u.95094
a b c d : ℝ≥0∞
r p q : ℝ≥0
n : ℕ
hn : 0 < n
⊢ a ^ n = ⊤ ↔ a = ⊤ ∧ n ≠ 0
induction a using recTopCoe
no goals
case inr.top
α : Type ?u.95091
β : Type ?u.95094
a b c d : ℝ≥0∞
r p q : ℝ≥0
n : ℕ
hn : 0 < n
⊢ ⊤ ^ n = ⊤ ↔ ⊤ = ⊤ ∧ n ≠ 0
simp only [Ne.def, hn.ne', top_pow hn]
no goals
case inr.coe
α : Type ?u.95091
β : Type ?u.95094
a b c d : ℝ≥0∞
r p q : ℝ≥0
n : ℕ
hn : 0 < n
x✝ : ℝ≥0
⊢ ↑x✝ ^ n = ⊤ ↔ ↑x✝ = ⊤ ∧ n ≠ 0
simp only [← coe_pow, coe_ne_top, false_and]