this : ¬Summable fun n => (↑n ^ ↑1)⁻¹
⊢ ¬Summable fun n => (↑n)⁻¹
⊢ ¬Summable fun n => (↑n)⁻¹
have : ¬Summable (fun n => ((n : ℝ) ^ ((1 : ℕ) : ℝ))⁻¹ : ℕ → ℝ) :=
  mt (Real.summable_nat_pow_inv (p := 1)).1 (lt_irrefl 1)
case h.e'_1.h.e'_5.h.h.e'_3
this : ¬Summable fun n => (↑n ^ ↑1)⁻¹
x✝ : ℕ
⊢ ↑x✝ = ↑x✝ ^ ↑1
this : ¬Summable fun n => (↑n ^ ↑1)⁻¹
⊢ ¬Summable fun n => (↑n)⁻¹
convert this
no goals
case h.e'_1.h.e'_5.h.h.e'_3
this : ¬Summable fun n => (↑n ^ ↑1)⁻¹
x✝ : ℕ
⊢ ↑x✝ = ↑x✝ ^ ↑1
simp