-- Mathlib/Analysis/SumOverResidueClass.lean
/-- A sequence `f` with values in an additive topological group `R` is summable on the
residue class of `k` mod `m` if and only if `f (m*n + k)` is summable. -/
lemma summable_indicator_mod_iff_summable {R : Type*} [AddCommGroup R] [TopologicalSpace R]
    [IsTopologicalAddGroup R] (m : ℕ) [hm : NeZero m] (k : ℕ) (f : ℕ → R) :
    Summable ({n : ℕ | (n : ZMod m) = k}.indicator f) ↔ Summable fun n ↦ f (m * n + k)

Proof state:
R : Type u_1
inst✝² : AddCommGroup R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalAddGroup R
m✝ : ℕ
hm : NeZero m✝
k : ℕ
f : ℕ → R
g : ℕ → ℕ := fun n => m✝ * n + k
m n : ℕ
hmn : g m = g n
⊢ m = n

Tactic:
simpa [g, hm.ne] using hmn

Result:
no goals

Proof state:
R : Type u_1
inst✝² : AddCommGroup R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalAddGroup R
m : ℕ
hm : NeZero m
k : ℕ
f : ℕ → R
g : ℕ → ℕ := fun n => m * n + k
hg : Function.Injective g
n : ℕ
hn : n ∉ range g
⊢ {n | ↑n = ↑k ∧ k ≤ n}.indicator f n = 0

Tactic:
contrapose! hn

Result:
R : Type u_1
inst✝² : AddCommGroup R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalAddGroup R
m : ℕ
hm : NeZero m
k : ℕ
f : ℕ → R
g : ℕ → ℕ := fun n => m * n + k
hg : Function.Injective g
n : ℕ
hn : {n | ↑n = ↑k ∧ k ≤ n}.indicator f n ≠ 0
⊢ n ∈ range g

Proof state:
R : Type u_1
inst✝² : AddCommGroup R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalAddGroup R
m : ℕ
hm : NeZero m
k : ℕ
f : ℕ → R
g : ℕ → ℕ := fun n => m * n + k
hg : Function.Injective g
⊢ ∀ n ∉ range g, {n | ↑n = ↑k ∧ k ≤ n}.indicator f n = 0

Tactic:
intro n hn

Result:
R : Type u_1
inst✝² : AddCommGroup R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalAddGroup R
m : ℕ
hm : NeZero m
k : ℕ
f : ℕ → R
g : ℕ → ℕ := fun n => m * n + k
hg : Function.Injective g
n : ℕ
hn : n ∉ range g
⊢ {n | ↑n = ↑k ∧ k ≤ n}.indicator f n = 0

Proof state:
case h.e'_2.h.e'_5.h
R : Type u_1
inst✝² : AddCommGroup R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalAddGroup R
m : ℕ
hm : NeZero m
k : ℕ
f : ℕ → R
g : ℕ → ℕ := fun n => m * n + k
hg : Function.Injective g
hg' : ∀ n ∉ range g, {n | ↑n = ↑k ∧ k ≤ n}.indicator f n = 0
x✝ : ℕ
⊢ f (m * x✝ + k) = ({n | ↑n = ↑k ∧ k ≤ n}.indicator f ∘ g) x✝

Tactic:
simp only [Function.comp_apply, mem_setOf_eq, Nat.cast_add, Nat.cast_mul, CharP.cast_eq_zero,
  zero_mul, zero_add, le_add_iff_nonneg_left, zero_le, and_self, indicator_of_mem, g]

Result:
no goals

Proof state:
R : Type u_1
inst✝² : AddCommGroup R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalAddGroup R
m : ℕ
hm : NeZero m
k : ℕ
f : ℕ → R
⊢ Summable ({n | ↑n = ↑k}.indicator f) ↔ Summable fun n => f (m * n + k)

Tactic:
trans Summable ({n : ℕ | (n : ZMod m) = k ∧ k ≤ n}.indicator f)

Result:
R : Type u_1
inst✝² : AddCommGroup R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalAddGroup R
m : ℕ
hm : NeZero m
k : ℕ
f : ℕ → R
⊢ Summable ({n | ↑n = ↑k}.indicator f) ↔ Summable ({n | ↑n = ↑k ∧ k ≤ n}.indicator f)

R : Type u_1
inst✝² : AddCommGroup R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalAddGroup R
m : ℕ
hm : NeZero m
k : ℕ
f : ℕ → R
⊢ Summable ({n | ↑n = ↑k ∧ k ≤ n}.indicator f) ↔ Summable fun n => f (m * n + k)

Proof state:
R : Type u_1
inst✝² : AddCommGroup R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalAddGroup R
m : ℕ
hm : NeZero m
k : ℕ
f : ℕ → R
⊢ Summable ({n | ↑n = ↑k ∧ k ≤ n}.indicator f) ↔ Summable fun n => f (m * n + k)

Tactic:
let g : ℕ → ℕ := fun n ↦ m * n + k

Result:
R : Type u_1
inst✝² : AddCommGroup R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalAddGroup R
m : ℕ
hm : NeZero m
k : ℕ
f : ℕ → R
g : ℕ → ℕ := fun n => m * n + k
⊢ Summable ({n | ↑n = ↑k ∧ k ≤ n}.indicator f) ↔ Summable fun n => f (m * n + k)

Proof state:
R : Type u_1
inst✝² : AddCommGroup R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalAddGroup R
m : ℕ
hm : NeZero m
k : ℕ
f : ℕ → R
g : ℕ → ℕ := fun n => m * n + k
hg : Function.Injective g
⊢ Summable ({n | ↑n = ↑k ∧ k ≤ n}.indicator f) ↔ Summable fun n => f (m * n + k)

Tactic:
have hg' : ∀ n ∉ range g, {n : ℕ | (n : ZMod m) = k ∧ k ≤ n}.indicator f n = 0 := by
  intro n hn
  contrapose! hn
  exact (Nat.range_mul_add m k).symm ▸ mem_of_indicator_ne_zero hn

Result:
R : Type u_1
inst✝² : AddCommGroup R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalAddGroup R
m : ℕ
hm : NeZero m
k : ℕ
f : ℕ → R
g : ℕ → ℕ := fun n => m * n + k
hg : Function.Injective g
hg' : ∀ n ∉ range g, {n | ↑n = ↑k ∧ k ≤ n}.indicator f n = 0
⊢ Summable ({n | ↑n = ↑k ∧ k ≤ n}.indicator f) ↔ Summable fun n => f (m * n + k)

Proof state:
R : Type u_1
inst✝² : AddCommGroup R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalAddGroup R
m : ℕ
hm : NeZero m
k : ℕ
f : ℕ → R
g : ℕ → ℕ := fun n => m * n + k
hg : Function.Injective g
hg' : ∀ n ∉ range g, {n | ↑n = ↑k ∧ k ≤ n}.indicator f n = 0
⊢ Summable ({n | ↑n = ↑k ∧ k ≤ n}.indicator f) ↔ Summable fun n => f (m * n + k)

Tactic:
convert (Function.Injective.summable_iff hg hg').symm using 3

Result:
case h.e'_2.h.e'_5.h
R : Type u_1
inst✝² : AddCommGroup R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalAddGroup R
m : ℕ
hm : NeZero m
k : ℕ
f : ℕ → R
g : ℕ → ℕ := fun n => m * n + k
hg : Function.Injective g
hg' : ∀ n ∉ range g, {n | ↑n = ↑k ∧ k ≤ n}.indicator f n = 0
x✝ : ℕ
⊢ f (m * x✝ + k) = ({n | ↑n = ↑k ∧ k ≤ n}.indicator f ∘ g) x✝

Proof state:
R : Type u_1
inst✝² : AddCommGroup R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalAddGroup R
m : ℕ
hm : NeZero m
k : ℕ
f : ℕ → R
⊢ Summable ({n | ↑n = ↑k}.indicator f ∘ Subtype.val) ↔ Summable ({n | ↑n = ↑k ∧ k ≤ n}.indicator f)

Tactic:
simp only [summable_subtype_iff_indicator, indicator_indicator, inter_comm, setOf_and,
  compl_setOf, not_lt]

Result:
no goals

Proof state:
R : Type u_1
inst✝² : AddCommGroup R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalAddGroup R
m : ℕ
hm : NeZero m
k : ℕ
f : ℕ → R
⊢ Summable ({n | ↑n = ↑k}.indicator f) ↔ Summable ({n | ↑n = ↑k ∧ k ≤ n}.indicator f)

Tactic:
rw [← (finite_lt_nat k).summable_compl_iff (f := {n : ℕ | (n : ZMod m) = k}.indicator f)]

Result:
R : Type u_1
inst✝² : AddCommGroup R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalAddGroup R
m : ℕ
hm : NeZero m
k : ℕ
f : ℕ → R
⊢ Summable ({n | ↑n = ↑k}.indicator f ∘ Subtype.val) ↔ Summable ({n | ↑n = ↑k ∧ k ≤ n}.indicator f)

Proof state:
R : Type u_1
inst✝² : AddCommGroup R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalAddGroup R
m : ℕ
hm : NeZero m
k : ℕ
f : ℕ → R
g : ℕ → ℕ := fun n => m * n + k
hg : Function.Injective g
n : ℕ
hn : {n | ↑n = ↑k ∧ k ≤ n}.indicator f n ≠ 0
⊢ n ∈ range g

Tactic:
exact (Nat.range_mul_add m k).symm ▸ mem_of_indicator_ne_zero hn

Result:
no goals

Proof state:
R : Type u_1
inst✝² : AddCommGroup R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalAddGroup R
m : ℕ
hm : NeZero m
k : ℕ
f : ℕ → R
g : ℕ → ℕ := fun n => m * n + k
⊢ Summable ({n | ↑n = ↑k ∧ k ≤ n}.indicator f) ↔ Summable fun n => f (m * n + k)

Tactic:
have hg : Function.Injective g := fun m n hmn ↦ by simpa [g, hm.ne] using hmn

Result:
R : Type u_1
inst✝² : AddCommGroup R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalAddGroup R
m : ℕ
hm : NeZero m
k : ℕ
f : ℕ → R
g : ℕ → ℕ := fun n => m * n + k
hg : Function.Injective g
⊢ Summable ({n | ↑n = ↑k ∧ k ≤ n}.indicator f) ↔ Summable fun n => f (m * n + k)