case none
n : ℕ
⊢ none ^ ↑n = none ^ n

case some
n : ℕ
val✝ : ℝ≥0
⊢ Option.some val✝ ^ ↑n = Option.some val✝ ^ n
x : ℝ≥0∞
n : ℕ
⊢ x ^ ↑n = x ^ n
cases x
no goals
case none
n : ℕ
⊢ none ^ ↑n = none ^ n
cases n <;> simp [top_rpow_of_pos (Nat.cast_add_one_pos _), top_pow (Nat.succ_pos _)]
no goals
case some
n : ℕ
val✝ : ℝ≥0
⊢ Option.some val✝ ^ ↑n = Option.some val✝ ^ n
simp [coe_rpow_of_nonneg _ (Nat.cast_nonneg n)]