-- Mathlib/Analysis/PSeries.lean
theorem summable_nat_rpow_inv {p : ℝ} :
    Summable (fun n => ((n : ℝ) ^ p)⁻¹ : ℕ → ℝ) ↔ 1 < p

Proof state:
p : ℝ
⊢ (Summable fun n => (↑n ^ p)⁻¹) ↔ 1 < p

Tactic:
rcases le_or_lt 0 p with hp | hp

Result:
case inl
p : ℝ
hp : 0 ≤ p
⊢ (Summable fun n => (↑n ^ p)⁻¹) ↔ 1 < p

case inr
p : ℝ
hp : p < 0
⊢ (Summable fun n => (↑n ^ p)⁻¹) ↔ 1 < p

Proof state:
case inl
p : ℝ
hp : 0 ≤ p
⊢ 2 = 0 ∧ 1 - p ≠ 0 ∨ 1 < 2 ∧ 1 - p < 0 ∨ 2 < 1 ∧ 0 < 1 - p ↔ 1 < p

Tactic:
norm_num

Result:
no goals

Proof state:
case inl.h_nonneg
p : ℝ
hp : 0 ≤ p
n : ℕ
⊢ 0 ≤ (↑n ^ p)⁻¹

Tactic:
positivity

Result:
no goals

Proof state:
case inr
p : ℝ
hp : p < 0
h : Summable fun n => (↑n ^ p)⁻¹
⊢ False

Tactic:
obtain ⟨k : ℕ, hk₁ : ((k : ℝ) ^ p)⁻¹ < 1, hk₀ : k ≠ 0⟩ :=
  ((h.tendsto_cofinite_zero.eventually (gt_mem_nhds zero_lt_one)).and
      (eventually_cofinite_ne 0)).exists

Result:
case inr.intro.intro
p : ℝ
hp : p < 0
h : Summable fun n => (↑n ^ p)⁻¹
k : ℕ
hk₁ : (↑k ^ p)⁻¹ < 1
hk₀ : k ≠ 0
⊢ False

Proof state:
case inr.intro.intro
p : ℝ
hp : p < 0
h : Summable fun n => (↑n ^ p)⁻¹
k : ℕ
hk₁ : (↑k ^ p)⁻¹ < 1
hk₀ : k ≠ 0
⊢ k = 0

Tactic:
rw [← pos_iff_ne_zero, ← @Nat.cast_pos ℝ] at hk₀

Result:
case inr.intro.intro
p : ℝ
hp : p < 0
h : Summable fun n => (↑n ^ p)⁻¹
k : ℕ
hk₁ : (↑k ^ p)⁻¹ < 1
hk₀ : 0 < ↑k
⊢ k = 0

Proof state:
case inl
p : ℝ
hp : 0 ≤ p
⊢ (Summable fun k => 2 ^ k * (↑(2 ^ k) ^ p)⁻¹) ↔ 1 < p

Tactic:
simp_rw [Nat.cast_pow, Nat.cast_two, ← rpow_natCast, ← rpow_mul zero_lt_two.le, mul_comm _ p,
  rpow_mul zero_lt_two.le, rpow_natCast, ← inv_pow, ← mul_pow,
  summable_geometric_iff_norm_lt_one]

Result:
case inl
p : ℝ
hp : 0 ≤ p
⊢ ‖2 * (2 ^ p)⁻¹‖ < 1 ↔ 1 < p

Proof state:
case inr.intro.intro
p : ℝ
hp : p < 0
h : Summable fun n => (↑n ^ p)⁻¹
k : ℕ
hk₁ : (↑k ^ p)⁻¹ < 1
hk₀ : k ≠ 0
⊢ False

Tactic:
apply hk₀

Result:
case inr.intro.intro
p : ℝ
hp : p < 0
h : Summable fun n => (↑n ^ p)⁻¹
k : ℕ
hk₁ : (↑k ^ p)⁻¹ < 1
hk₀ : k ≠ 0
⊢ k = 0

Proof state:
case inl.h_mono
p : ℝ
hp : 0 ≤ p
⊢ ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → (↑n ^ p)⁻¹ ≤ (↑m ^ p)⁻¹

Tactic:
intro m n hm hmn

Result:
case inl.h_mono
p : ℝ
hp : 0 ≤ p
m n : ℕ
hm : 0 < m
hmn : m ≤ n
⊢ (↑n ^ p)⁻¹ ≤ (↑m ^ p)⁻¹

Proof state:
case inl.h_nonneg
p : ℝ
hp : 0 ≤ p
⊢ ∀ (n : ℕ), 0 ≤ (↑n ^ p)⁻¹

Tactic:
intro n

Result:
case inl.h_nonneg
p : ℝ
hp : 0 ≤ p
n : ℕ
⊢ 0 ≤ (↑n ^ p)⁻¹

Proof state:
case inl
p : ℝ
hp : 0 ≤ p
⊢ (Summable fun n => (↑n ^ p)⁻¹) ↔ 1 < p

Tactic:
rw [← summable_condensed_iff_of_nonneg]

Result:
case inl
p : ℝ
hp : 0 ≤ p
⊢ (Summable fun k => 2 ^ k * (↑(2 ^ k) ^ p)⁻¹) ↔ 1 < p

case inl.h_nonneg
p : ℝ
hp : 0 ≤ p
⊢ ∀ (n : ℕ), 0 ≤ (↑n ^ p)⁻¹

case inl.h_mono
p : ℝ
hp : 0 ≤ p
⊢ ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → (↑n ^ p)⁻¹ ≤ (↑m ^ p)⁻¹

Proof state:
case inl
p : ℝ
hp : 0 ≤ p
⊢ ‖2 ^ 1 * (2 ^ p)⁻¹‖ < 1 ↔ 1 < p

Tactic:
rw [← division_def, ← rpow_sub zero_lt_two, norm_eq_abs,
  abs_of_pos (rpow_pos_of_pos zero_lt_two _), rpow_lt_one_iff zero_lt_two.le]

Result:
case inl
p : ℝ
hp : 0 ≤ p
⊢ 2 = 0 ∧ 1 - p ≠ 0 ∨ 1 < 2 ∧ 1 - p < 0 ∨ 2 < 1 ∧ 0 < 1 - p ↔ 1 < p

Proof state:
case inr
p : ℝ
hp : p < 0
⊢ ¬Summable fun n => (↑n ^ p)⁻¹

Tactic:
intro h

Result:
case inr
p : ℝ
hp : p < 0
h : Summable fun n => (↑n ^ p)⁻¹
⊢ False

Proof state:
case inl.h_mono
p : ℝ
hp : 0 ≤ p
m n : ℕ
hm : 0 < m
hmn : m ≤ n
⊢ (↑n ^ p)⁻¹ ≤ (↑m ^ p)⁻¹

Tactic:
gcongr

Result:
no goals

Proof state:
case inr.intro.intro
p : ℝ
hp : p < 0
h : Summable fun n => (↑n ^ p)⁻¹
k : ℕ
hk₁ : (↑k ^ p)⁻¹ < 1
hk₀ : 0 < ↑k
⊢ k = 0

Tactic:
simpa [inv_lt_one₀ (rpow_pos_of_pos hk₀ _), one_lt_rpow_iff_of_pos hk₀, hp,
  hp.not_lt, hk₀] using hk₁

Result:
no goals

Proof state:
p : ℝ
hp : p < 0
this : ¬Summable fun n => (↑n ^ p)⁻¹
⊢ (Summable fun n => (↑n ^ p)⁻¹) ↔ 1 < p

Tactic:
have : ¬1 < p := fun hp₁ => hp.not_le (zero_le_one.trans hp₁.le)

Result:
p : ℝ
hp : p < 0
this✝ : ¬Summable fun n => (↑n ^ p)⁻¹
this : ¬1 < p
⊢ (Summable fun n => (↑n ^ p)⁻¹) ↔ 1 < p

Proof state:
case inl
p : ℝ
hp : 0 ≤ p
⊢ ‖2 * (2 ^ p)⁻¹‖ < 1 ↔ 1 < p

Tactic:
nth_rw 1 [← rpow_one 2]

Result:
case inl
p : ℝ
hp : 0 ≤ p
⊢ ‖2 ^ 1 * (2 ^ p)⁻¹‖ < 1 ↔ 1 < p

Proof state:
case inr
p : ℝ
hp : p < 0
⊢ (Summable fun n => (↑n ^ p)⁻¹) ↔ 1 < p

Tactic:
suffices ¬Summable (fun n => ((n : ℝ) ^ p)⁻¹ : ℕ → ℝ) by
  have : ¬1 < p := fun hp₁ => hp.not_le (zero_le_one.trans hp₁.le)
  simpa only [this, iff_false]

Result:
case inr
p : ℝ
hp : p < 0
⊢ ¬Summable fun n => (↑n ^ p)⁻¹

Proof state:
p : ℝ
hp : p < 0
this✝ : ¬Summable fun n => (↑n ^ p)⁻¹
this : ¬1 < p
⊢ (Summable fun n => (↑n ^ p)⁻¹) ↔ 1 < p

Tactic:
simpa only [this, iff_false]

Result:
no goals