-- Mathlib/Analysis/PSeries.lean
/-- The harmonic series restricted to a residue class is not summable. -/
lemma Real.not_summable_indicator_one_div_natCast {m : ℕ} (hm : m ≠ 0) (k : ZMod m) :
    ¬ Summable ({n : ℕ | (n : ZMod m) = k}.indicator fun n : ℕ ↦ (1 / n : ℝ))

Proof state:
m : ℕ
hm : m ≠ 0
k : ZMod m
this : NeZero m
⊢ ¬Summable ({n | ↑n = k}.indicator fun n => 1 / ↑n)

Tactic:
rw [← summable_nat_add_iff 1]

Result:
m : ℕ
hm : m ≠ 0
k : ZMod m
this : NeZero m
⊢ ¬Summable fun n => {n | ↑n = k}.indicator (fun n => 1 / ↑n) (n + 1)

Proof state:
m : ℕ
hm : m ≠ 0
k : ZMod m
this : NeZero m
h✝ : ∀ (n : ℕ), {n | ↑n = k - 1}.indicator (fun n => 1 / ↑(n + 1)) n = if ↑n = k - 1 then 1 / (↑n + 1) else 0
n₁ n₂ : ℕ
h : n₁ ≤ n₂
⊢ 1 / ↑(n₂ + 1) ≤ 1 / ↑(n₁ + 1)

Tactic:
gcongr

Result:
no goals

Proof state:
m : ℕ
hm : m ≠ 0
k : ZMod m
⊢ ¬Summable ({n | ↑n = k}.indicator fun n => 1 / ↑n)

Tactic:
have : NeZero m := ⟨hm⟩

Result:
m : ℕ
hm : m ≠ 0
k : ZMod m
this : NeZero m
⊢ ¬Summable ({n | ↑n = k}.indicator fun n => 1 / ↑n)

Proof state:
m : ℕ
hm : m ≠ 0
k : ZMod m
this : NeZero m
h : ∀ (n : ℕ), {n | ↑n = k - 1}.indicator (fun n => 1 / ↑(n + 1)) n = if ↑n = k - 1 then 1 / (↑n + 1) else 0
⊢ ¬Summable fun n => {n | ↑n = k}.indicator (fun n => 1 / ↑n) (n + 1)

Tactic:
simp_rw [indicator_apply, mem_setOf, cast_add, cast_one, ← eq_sub_iff_add_eq, ← h]

Result:
m : ℕ
hm : m ≠ 0
k : ZMod m
this : NeZero m
h : ∀ (n : ℕ), {n | ↑n = k - 1}.indicator (fun n => 1 / ↑(n + 1)) n = if ↑n = k - 1 then 1 / (↑n + 1) else 0
⊢ ¬Summable fun n => {n | ↑n = k - 1}.indicator (fun n => 1 / ↑(n + 1)) n

Proof state:
m : ℕ
hm : m ≠ 0
k : ZMod m
this : NeZero m
n : ℕ
⊢ {n | ↑n = k - 1}.indicator (fun n => 1 / ↑(n + 1)) n = if ↑n = k - 1 then 1 / (↑n + 1) else 0

Tactic:
simp only [indicator_apply, mem_setOf_eq, cast_add, cast_one]

Result:
no goals

Proof state:
m : ℕ
hm : m ≠ 0
k : ZMod m
this : NeZero m
⊢ ¬Summable fun n => {n | ↑n = k}.indicator (fun n => 1 / ↑n) (n + 1)

Tactic:
have h (n : ℕ) : {n : ℕ | (n : ZMod m) = k - 1}.indicator (fun n : ℕ ↦ (1 / (n + 1 :) : ℝ)) n =
    if (n : ZMod m) = k - 1 then (1 / (n + 1) : ℝ) else (0 : ℝ) := by
  simp only [indicator_apply, mem_setOf_eq, cast_add, cast_one]

Result:
m : ℕ
hm : m ≠ 0
k : ZMod m
this : NeZero m
h : ∀ (n : ℕ), {n | ↑n = k - 1}.indicator (fun n => 1 / ↑(n + 1)) n = if ↑n = k - 1 then 1 / (↑n + 1) else 0
⊢ ¬Summable fun n => {n | ↑n = k}.indicator (fun n => 1 / ↑n) (n + 1)

Proof state:
m : ℕ
hm : m ≠ 0
k : ZMod m
this : NeZero m
h : ∀ (n : ℕ), {n | ↑n = k - 1}.indicator (fun n => 1 / ↑(n + 1)) n = if ↑n = k - 1 then 1 / (↑n + 1) else 0
⊢ ¬Summable fun n => 1 / ↑(n + 1)

Tactic:
exact mt (summable_nat_add_iff (f := fun n : ℕ ↦ 1 / (n : ℝ)) 1).mp not_summable_one_div_natCast

Result:
no goals

Proof state:
m : ℕ
hm : m ≠ 0
k : ZMod m
this : NeZero m
h : ∀ (n : ℕ), {n | ↑n = k - 1}.indicator (fun n => 1 / ↑(n + 1)) n = if ↑n = k - 1 then 1 / (↑n + 1) else 0
⊢ ¬Summable fun n => {n | ↑n = k - 1}.indicator (fun n => 1 / ↑(n + 1)) n

Tactic:
rw [summable_indicator_mod_iff (fun n₁ n₂ h ↦ by gcongr) (k - 1)]

Result:
m : ℕ
hm : m ≠ 0
k : ZMod m
this : NeZero m
h : ∀ (n : ℕ), {n | ↑n = k - 1}.indicator (fun n => 1 / ↑(n + 1)) n = if ↑n = k - 1 then 1 / (↑n + 1) else 0
⊢ ¬Summable fun n => 1 / ↑(n + 1)