-- Mathlib/Analysis/SumOverResidueClass.lean
/-- If a decreasing sequence of real numbers is summable on one residue class
modulo `m`, then it is also summable on every other residue class mod `m`. -/
lemma summable_indicator_mod_iff_summable_indicator_mod {m : ℕ} [NeZero m] {f : ℕ → ℝ}
    (hf : Antitone f) {k : ZMod m} (l : ZMod m)
    (hs : Summable ({n : ℕ | (n : ZMod m) = k}.indicator f)) :
    Summable ({n : ℕ | (n : ZMod m) = l}.indicator f)

Proof state:
case neg
m : ℕ
inst✝ : NeZero m
f : ℕ → ℝ
hf : Antitone f
k l : ZMod m
hs : Summable ({n | ↑n = k}.indicator f)
hf₀ : ¬∀ (n : ℕ), 0 ≤ f n
⊢ Summable ({n | ↑n = l}.indicator f)

Tactic:
push_neg at hf₀

Result:
case neg
m : ℕ
inst✝ : NeZero m
f : ℕ → ℝ
hf : Antitone f
k l : ZMod m
hs : Summable ({n | ↑n = k}.indicator f)
hf₀ : ∃ n, f n < 0
⊢ Summable ({n | ↑n = l}.indicator f)

Proof state:
case pos
m : ℕ
inst✝ : NeZero m
f : ℕ → ℝ
hf : Antitone f
k l : ZMod m
hs : Summable fun n => f (m * n + k.val)
hf₀ : ∀ (n : ℕ), 0 ≤ f n
hl : ↑l.val + ↑m = l
⊢ Summable fun n => f (m * n + (l.val + m))

Tactic:
exact hs.of_nonneg_of_le (fun _ ↦ hf₀ _)
  fun _ ↦ hf <| Nat.add_le_add Nat.le.refl (k.val_lt.trans_le <| m.le_add_left l.val).le

Result:
no goals

Proof state:
case pos
m : ℕ
inst✝ : NeZero m
f : ℕ → ℝ
hf : Antitone f
k l : ZMod m
hs : Summable fun n => f (m * n + k.val)
hf₀ : ∀ (n : ℕ), 0 ≤ f n
⊢ Summable ({n | ↑n = l}.indicator f)

Tactic:
have hl : (l.val + m : ZMod m) = l := by
  simp only [ZMod.natCast_val, ZMod.cast_id', id_eq, CharP.cast_eq_zero, add_zero]

Result:
case pos
m : ℕ
inst✝ : NeZero m
f : ℕ → ℝ
hf : Antitone f
k l : ZMod m
hs : Summable fun n => f (m * n + k.val)
hf₀ : ∀ (n : ℕ), 0 ≤ f n
hl : ↑l.val + ↑m = l
⊢ Summable ({n | ↑n = l}.indicator f)

Proof state:
m : ℕ
inst✝ : NeZero m
f : ℕ → ℝ
hf : Antitone f
k l : ZMod m
hs : Summable ({n | ↑n = k}.indicator f)
⊢ Summable ({n | ↑n = l}.indicator f)

Tactic:
by_cases hf₀ : ∀ n, 0 ≤ f n

Result:
case pos
m : ℕ
inst✝ : NeZero m
f : ℕ → ℝ
hf : Antitone f
k l : ZMod m
hs : Summable ({n | ↑n = k}.indicator f)
hf₀ : ∀ (n : ℕ), 0 ≤ f n
⊢ Summable ({n | ↑n = l}.indicator f)

case neg
m : ℕ
inst✝ : NeZero m
f : ℕ → ℝ
hf : Antitone f
k l : ZMod m
hs : Summable ({n | ↑n = k}.indicator f)
hf₀ : ¬∀ (n : ℕ), 0 ≤ f n
⊢ Summable ({n | ↑n = l}.indicator f)

Proof state:
case neg
m : ℕ
inst✝ : NeZero m
f : ℕ → ℝ
hf : Antitone f
k l : ZMod m
hs : Summable ({n | ↑n = k}.indicator f)
hf₀ : ∃ n, f n < 0
⊢ Summable ({n | ↑n = l}.indicator f)

Tactic:
obtain ⟨n, hn⟩ := hf₀

Result:
case neg.intro
m : ℕ
inst✝ : NeZero m
f : ℕ → ℝ
hf : Antitone f
k l : ZMod m
hs : Summable ({n | ↑n = k}.indicator f)
n : ℕ
hn : f n < 0
⊢ Summable ({n | ↑n = l}.indicator f)

Proof state:
m : ℕ
inst✝ : NeZero m
f : ℕ → ℝ
hf : Antitone f
k l : ZMod m
hs : Summable fun n => f (m * n + k.val)
hf₀ : ∀ (n : ℕ), 0 ≤ f n
⊢ ↑l.val + ↑m = l

Tactic:
simp only [ZMod.natCast_val, ZMod.cast_id', id_eq, CharP.cast_eq_zero, add_zero]

Result:
no goals

Proof state:
case pos
m : ℕ
inst✝ : NeZero m
f : ℕ → ℝ
hf : Antitone f
k l : ZMod m
hs : Summable ({n | ↑n = k}.indicator f)
hf₀ : ∀ (n : ℕ), 0 ≤ f n
⊢ Summable ({n | ↑n = l}.indicator f)

Tactic:
rw [← ZMod.natCast_zmod_val k, summable_indicator_mod_iff_summable] at hs

Result:
case pos
m : ℕ
inst✝ : NeZero m
f : ℕ → ℝ
hf : Antitone f
k l : ZMod m
hs : Summable fun n => f (m * n + k.val)
hf₀ : ∀ (n : ℕ), 0 ≤ f n
⊢ Summable ({n | ↑n = l}.indicator f)

Proof state:
case neg.intro
m : ℕ
inst✝ : NeZero m
f : ℕ → ℝ
hf : Antitone f
k l : ZMod m
hs : Summable ({n | ↑n = k}.indicator f)
n : ℕ
hn : f n < 0
⊢ Summable ({n | ↑n = l}.indicator f)

Tactic:
exact (not_summable_indicator_mod_of_antitone_of_neg hf hn k hs).elim

Result:
no goals

Proof state:
case pos
m : ℕ
inst✝ : NeZero m
f : ℕ → ℝ
hf : Antitone f
k l : ZMod m
hs : Summable fun n => f (m * n + k.val)
hf₀ : ∀ (n : ℕ), 0 ≤ f n
hl : ↑l.val + ↑m = l
⊢ Summable ({n | ↑n = l}.indicator f)

Tactic:
rw [← hl, ← Nat.cast_add, summable_indicator_mod_iff_summable]

Result:
case pos
m : ℕ
inst✝ : NeZero m
f : ℕ → ℝ
hf : Antitone f
k l : ZMod m
hs : Summable fun n => f (m * n + k.val)
hf₀ : ∀ (n : ℕ), 0 ≤ f n
hl : ↑l.val + ↑m = l
⊢ Summable fun n => f (m * n + (l.val + m))