awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SumIntegralExpDecay
Goal:
k M : ℕ
c : ℝ
hc : 0 < c
⊢ ∀ (i : ℕ), HPow.hPow (α := ℝ) 2 (-(c * (↑i : ℝ))) = rexp (-(log 2 * c) * (↑i : ℝ))

Tactic:
have A (i : ℕ) : (2 : ℝ) ^ (- (c * i)) = rexp (- (Real.log 2 * c) * i) := by
    conv_lhs => rw [← exp_log zero_lt_two, ← exp_mul]
    congr 1
    ring
-- Module: Mathlib.Analysis.SumIntegralExpDecay
Goal:
k M : ℕ
c : ℝ
hc : 0 < c
A : ∀ (i : ℕ), HPow.hPow (α := ℝ) 2 (-(c * (↑i : ℝ))) = rexp (-(log 2 * c) * (↑i : ℝ))
simp :
  ∑ x ∈ Finset.Iic M, HPow.hPow (α := ℝ) (↑x : ℝ) k * rexp (-(log 2 * c * (↑x : ℝ))) ≤
    HPow.hPow (α := ℝ) 2 c * (↑k ! : ℝ) / (log 2 * c) ^ (k + 1)
⊢ ∑ i ∈ Finset.Iic M, HPow.hPow (α := ℝ) (↑i : ℝ) k * HPow.hPow (α := ℝ) 2 (-(c * (↑i : ℝ))) ≤
    HPow.hPow (α := ℝ) 2 c * (↑k ! : ℝ) / (log 2 * c) ^ (k + 1)

Tactic:
simp only [A, neg_mul]

Premises used: neg_mul
-- Module: Mathlib.Analysis.SumIntegralExpDecay
Goal:
k M : ℕ
c : ℝ
hc : 0 < c
A : ∀ (i : ℕ), HPow.hPow (α := ℝ) 2 (-(c * (↑i : ℝ))) = rexp (-(log 2 * c) * (↑i : ℝ))
⊢ 0 < log 2 * c

Tactic:
positivity
-- Module: Mathlib.Analysis.SumIntegralExpDecay
Goal:
k M : ℕ
c : ℝ
hc : 0 < c
A : ∀ (i : ℕ), HPow.hPow (α := ℝ) 2 (-(c * (↑i : ℝ))) = rexp (-(log 2 * c) * (↑i : ℝ))
apply :
  rexp (log 2 * c) * (↑k ! : ℝ) / (log 2 * c) ^ (k + 1) = HPow.hPow (α := ℝ) 2 c * (↑k ! : ℝ) / (log 2 * c) ^ (k + 1)
⊢ ∑ x ∈ Finset.Iic M, HPow.hPow (α := ℝ) (↑x : ℝ) k * rexp (-(log 2 * c * (↑x : ℝ))) ≤
    HPow.hPow (α := ℝ) 2 c * (↑k ! : ℝ) / (log 2 * c) ^ (k + 1)

Tactic:
apply (sum_Iic_pow_mul_exp_neg_le (by positivity)).trans_eq

Premises used: LE.le.trans_eq, sum_Iic_pow_mul_exp_neg_le
-- Module: Mathlib.Analysis.SumIntegralExpDecay
Goal:
k M : ℕ
c : ℝ
hc : 0 < c
A : ∀ (i : ℕ), HPow.hPow (α := ℝ) 2 (-(c * (↑i : ℝ))) = rexp (-(log 2 * c) * (↑i : ℝ))
rw : rexp (log 2) ^ c * (↑k ! : ℝ) / (log 2 * c) ^ (k + 1) = HPow.hPow (α := ℝ) 2 c * (↑k ! : ℝ) / (log 2 * c) ^ (k + 1)
rw₁ rw₂ :
  HPow.hPow (α := ℝ) 2 c * (↑k ! : ℝ) / (log 2 * c) ^ (k + 1) =
    HPow.hPow (α := ℝ) 2 c * (↑k ! : ℝ) / (log 2 * c) ^ (k + 1)
⊢ rexp (log 2 * c) * (↑k ! : ℝ) / (log 2 * c) ^ (k + 1) = HPow.hPow (α := ℝ) 2 c * (↑k ! : ℝ) / (log 2 * c) ^ (k + 1)

Tactic:
rw [exp_mul, exp_log zero_lt_two]

Premises used: Real.exp_mul, Real.exp_log, zero_lt_two
-- Module: Mathlib.Analysis.SumOverResidueClass
Goal:
R : Type u_1
inst : AddCommMonoid R
m : ℕ
inst_1 : NeZero m
f : ℕ → R
h : ∀ (n : ℕ), f n = (∑ a : ZMod m, Set.indicator {n : ℕ | (↑n : ZMod m) = a} f) n
⊢ f = ∑ a : ZMod m, Set.indicator {n : ℕ | (↑n : ZMod m) = a} f

Tactic:
ext n
-- Module: Mathlib.Analysis.SumOverResidueClass
Goal:
R : Type u_1
inst : AddCommMonoid R
m : ℕ
inst_1 : NeZero m
f : ℕ → R
n : ℕ
⊢ f n = (∑ a : ZMod m, Set.indicator {n : ℕ | (↑n : ZMod m) = a} f) n

Tactic:
simp only [Finset.sum_apply, Set.indicator_apply, Set.mem_setOf_eq, Finset.sum_ite_eq,
    Finset.mem_univ, ↓reduceIte]

Premises used: Finset.mem_univ, Set.indicator_apply, Finset.sum_apply, Set.mem_setOf_eq, reduceIte, Finset.sum_ite_eq
-- Module: Mathlib.Analysis.SumOverResidueClass
Goal:
R : Type u_1
inst : AddCommGroup R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalAddGroup R
m : ℕ
hm : NeZero m
k : ℕ
f : ℕ → R
trans :
  Summable (indicator {n : ℕ | Eq (α := ZMod m) (↑n : ZMod m) (↑k : ZMod m)} f) ↔
    Summable (indicator {n : ℕ | Eq (α := ZMod m) (↑n : ZMod m) (↑k : ZMod m) ∧ k ≤ n} f)
trans₁ :
  Summable (indicator {n : ℕ | Eq (α := ZMod m) (↑n : ZMod m) (↑k : ZMod m) ∧ k ≤ n} f) ↔
    Summable.{u_1, 0} (α := R) fun (n : ℕ) ↦ f (m * n + k)
⊢ Summable (indicator {n : ℕ | Eq (α := ZMod m) (↑n : ZMod m) (↑k : ZMod m)} f) ↔
    Summable.{u_1, 0} (α := R) fun (n : ℕ) ↦ f (m * n + k)

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

Premises used: Set.indicator, setOf, LE.le, Nat.cast, And, Summable, Eq, SummationFilter.unconditional
-- Module: Mathlib.Analysis.SumOverResidueClass
Goal:
R : Type u_1
inst : AddCommGroup R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalAddGroup R
m : ℕ
hm : NeZero m
k : ℕ
f : ℕ → R
rw :
  Summable (β := (↑{i : ℕ | i < k}ᶜ : Type))
      (indicator {n : ℕ | Eq (α := ZMod m) (↑n : ZMod m) (↑k : ZMod m)} f ∘
        Subtype.val (p := fun (x : ℕ) ↦ Membership.mem (γ := Set ℕ) {i : ℕ | i < k}ᶜ x)) ↔
    Summable (indicator {n : ℕ | Eq (α := ZMod m) (↑n : ZMod m) (↑k : ZMod m) ∧ k ≤ n} f)
⊢ Summable (indicator {n : ℕ | Eq (α := ZMod m) (↑n : ZMod m) (↑k : ZMod m)} f) ↔
    Summable (indicator {n : ℕ | Eq (α := ZMod m) (↑n : ZMod m) (↑k : ZMod m) ∧ k ≤ n} f)

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

Premises used: Set.Finite.summable_compl_iff, Set.finite_lt_nat
-- Module: Mathlib.Analysis.SumOverResidueClass
Goal:
R : Type u_1
inst : AddCommGroup R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalAddGroup R
m : ℕ
hm : NeZero m
k : ℕ
f : ℕ → R
⊢ Summable (β := (↑{i : ℕ | i < k}ᶜ : Type))
      (indicator {n : ℕ | Eq (α := ZMod m) (↑n : ZMod m) (↑k : ZMod m)} f ∘
        Subtype.val (p := fun (x : ℕ) ↦ Membership.mem (γ := Set ℕ) {i : ℕ | i < k}ᶜ x)) ↔
    Summable (indicator {n : ℕ | Eq (α := ZMod m) (↑n : ZMod m) (↑k : ZMod m) ∧ k ≤ n} f)

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

Premises used: Set.setOf_and, Set.inter_comm, not_lt, Set.indicator_indicator, summable_subtype_iff_indicator, Set.compl_setOf
-- Module: Mathlib.Analysis.SumOverResidueClass
Goal:
R : Type u_1
inst : AddCommGroup R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalAddGroup R
m_1 : ℕ
hm : NeZero m_1
k : ℕ
f : ℕ → R
g : ℕ → ℕ := fun (n : ℕ) ↦ m_1 * n + k
m n : ℕ
hmn : g m = g n
⊢ m = n

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

Premises used: NeZero.ne
-- Module: Mathlib.Analysis.SumOverResidueClass
Goal:
R : Type u_1
inst : AddCommGroup R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalAddGroup R
m : ℕ
hm : NeZero m
k : ℕ
f : ℕ → R
g : ℕ → ℕ := fun (n : ℕ) ↦ m * n + k
⊢ Function.Injective g

Tactic:
have hg : Function.Injective g := fun m n hmn ↦ by simpa [g, hm.ne] using hmn
-- Module: Mathlib.Analysis.SumOverResidueClass
Goal:
R : Type u_1
inst : AddCommGroup R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalAddGroup R
m : ℕ
hm : NeZero m
k : ℕ
f : ℕ → R
g : ℕ → ℕ := fun (n : ℕ) ↦ m * n + k
hg : Function.Injective g
n : ℕ
hn : n ∉ range g
contrapose! : ∀ (hn : indicator {n : ℕ | Eq (α := ZMod m) (↑n : ZMod m) (↑k : ZMod m) ∧ k ≤ n} f n ≠ 0), n ∈ range g
⊢ indicator {n : ℕ | Eq (α := ZMod m) (↑n : ZMod m) (↑k : ZMod m) ∧ k ≤ n} f n = 0

Tactic:
contrapose! hn
-- Module: Mathlib.Analysis.SumOverResidueClass
Goal:
R : Type u_1
inst : AddCommGroup R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalAddGroup R
m : ℕ
hm : NeZero m
k : ℕ
f : ℕ → R
g : ℕ → ℕ := fun (n : ℕ) ↦ m * n + k
hg : Function.Injective g
n : ℕ
hn : indicator {n : ℕ | Eq (α := ZMod m) (↑n : ZMod m) (↑k : ZMod m) ∧ k ≤ n} f n ≠ 0
⊢ n ∈ range g

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

Premises used: Set.mem_of_indicator_ne_zero, Set.Mem, Eq.rec, Nat.range_mul_add, Eq.symm
-- Module: Mathlib.Analysis.SumOverResidueClass
Goal:
R : Type u_1
inst : AddCommGroup R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalAddGroup R
m : ℕ
hm : NeZero m
k : ℕ
f : ℕ → R
g : ℕ → ℕ := fun (n : ℕ) ↦ m * n + k
hg : Function.Injective g
n : ℕ
hn : indicator {n : ℕ | Eq (α := ZMod m) (↑n : ZMod m) (↑k : ZMod m) ∧ k ≤ n} f n ≠ 0
⊢ n ∈ range g

Tactic:
exact (Nat.range_mul_add m k).symm ▸ mem_of_indicator_ne_zero hn
-- Module: Mathlib.Analysis.SumOverResidueClass
Goal:
R : Type u_1
inst : AddCommGroup R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalAddGroup R
m : ℕ
hm : NeZero m
k : ℕ
f : ℕ → R
g : ℕ → ℕ := fun (n : ℕ) ↦ m * n + k
hg : Function.Injective g
⊢ ∀ n ∉ range g, indicator {n : ℕ | Eq (α := ZMod m) (↑n : ZMod m) (↑k : ZMod m) ∧ k ≤ n} f n = 0

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
-- Module: Mathlib.Analysis.SumOverResidueClass
Goal:
R : Type u_1
inst : AddCommGroup R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalAddGroup R
m : ℕ
hm : NeZero m
k : ℕ
f : ℕ → R
g : ℕ → ℕ := fun (n : ℕ) ↦ m * n + k
hg : Function.Injective g
hg' : ∀ n ∉ range g, indicator {n : ℕ | Eq (α := ZMod m) (↑n : ZMod m) (↑k : ZMod m) ∧ k ≤ n} f n = 0
⊢ Summable (indicator {n : ℕ | Eq (α := ZMod m) (↑n : ZMod m) (↑k : ZMod m) ∧ k ≤ n} f) ↔
    Summable (indicator {n : ℕ | Eq (α := ZMod m) (↑n : ZMod m) (↑k : ZMod m) ∧ k ≤ n} f ∘ g)

Tactic:
(Function.Injective.summable_iff hg hg').symm

Premises used: Function.Injective.summable_iff, Iff.symm
-- Module: Mathlib.Analysis.SumOverResidueClass
Goal:
R : Type u_1
inst : AddCommGroup R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalAddGroup R
m : ℕ
hm : NeZero m
k : ℕ
f : ℕ → R
g : ℕ → ℕ := fun (n : ℕ) ↦ m * n + k
hg : Function.Injective g
hg' : ∀ n ∉ range g, indicator {n : ℕ | Eq (α := ZMod m) (↑n : ZMod m) (↑k : ZMod m) ∧ k ≤ n} f n = 0
h : ∀ (x : ℕ), f (m * x + k) = (indicator {n : ℕ | Eq (α := ZMod m) (↑n : ZMod m) (↑k : ZMod m) ∧ k ≤ n} f ∘ g) x
⊢ Summable (indicator {n : ℕ | Eq (α := ZMod m) (↑n : ZMod m) (↑k : ZMod m) ∧ k ≤ n} f) ↔
    Summable.{u_1, 0} (α := R) fun (n : ℕ) ↦ f (m * n + k)

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

Premises used: Function.Injective.summable_iff, Iff.symm
-- Module: Mathlib.Analysis.SumOverResidueClass
Goal:
R : Type u_1
inst : AddCommGroup R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalAddGroup R
m : ℕ
hm : NeZero m
k : ℕ
f : ℕ → R
g : ℕ → ℕ := fun (n : ℕ) ↦ m * n + k
hg : Function.Injective g
hg' : ∀ n ∉ range g, indicator {n : ℕ | Eq (α := ZMod m) (↑n : ZMod m) (↑k : ZMod m) ∧ k ≤ n} f n = 0
x : ℕ
⊢ f (m * x + k) = (indicator {n : ℕ | Eq (α := ZMod m) (↑n : ZMod m) (↑k : ZMod m) ∧ k ≤ n} 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]

Premises used: CharP.cast_eq_zero, zero_le, and_self, MulZeroClass.zero_mul, Set.mem_setOf_eq, zero_add, Nat.cast_add, Set.indicator_of_mem, Nat.cast_mul, Function.comp_apply, le_add_iff_nonneg_left
-- Module: Mathlib.Analysis.SumOverResidueClass
Goal:
f : ℕ → ℝ
hf : Antitone f
n : ℕ
hn : f n < 0
hs : Summable f
⊢ Filter.Tendsto f Filter.atTop (nhds 0)

Tactic:
have := hs.tendsto_atTop_zero
-- Module: Mathlib.Analysis.SumOverResidueClass
Goal:
f : ℕ → ℝ
hf : Antitone f
n : ℕ
hn : f n < 0
hs : Summable f
this : Filter.Tendsto f Filter.atTop (nhds 0)
⊢ ∀ ε > 0, ∃ (N : ℕ), ∀ n ≥ N, |f n| < ε

Tactic:
simp only [Metric.tendsto_atTop, dist_zero_right, Real.norm_eq_abs] at this

Premises used: Metric.tendsto_atTop, dist_zero_right, Real.norm_eq_abs
-- Module: Mathlib.Analysis.SumOverResidueClass
Goal:
f : ℕ → ℝ
hf : Antitone f
n : ℕ
hn : f n < 0
hs : Summable f
this : ∀ ε > 0, ∃ (N : ℕ), ∀ n ≥ N, |f n| < ε
obtain : ∀ (N : ℕ) (hN : ∀ n_1 ≥ N, |f n_1| < |f n|), False
⊢ False

Tactic:
obtain ⟨N, hN⟩ := this (|f n|) (abs_pos_of_neg hn)

Premises used: abs, abs_pos_of_neg
-- Module: Mathlib.Analysis.SumOverResidueClass
Goal:
f : ℕ → ℝ
hf : Antitone f
n : ℕ
hn : f n < 0
hs : Summable f
this : ∀ ε > 0, ∃ (N : ℕ), ∀ n ≥ N, |f n| < ε
N : ℕ
hN : ∀ n_1 ≥ N, |f n_1| < |f n|
⊢ |f (max n N)| < |f n|

Tactic:
specialize hN (max n N) (n.le_max_right N)

Premises used: Nat.le_max_right, Max.max
-- Module: Mathlib.Analysis.SumOverResidueClass
Goal:
f : ℕ → ℝ
hf : Antitone f
n : ℕ
hn : f n < 0
hs : Summable f
this : ∀ ε > 0, ∃ (N : ℕ), ∀ n ≥ N, |f n| < ε
N : ℕ
hN : |f (max n N)| < |f n|
contrapose! : ∀ (hN : True), |f n| ≤ |f (max n N)|
⊢ False

Tactic:
contrapose! hN
-- Module: Mathlib.Analysis.SumOverResidueClass
Goal:
f : ℕ → ℝ
hf : Antitone f
n : ℕ
hn : f n < 0
hs : Summable f
this : ∀ ε > 0, ∃ (N : ℕ), ∀ n ≥ N, |f n| < ε
N : ℕ
⊢ f (max n N) ≤ f n

Tactic:
have H : f (max n N) ≤ f n := hf (n.le_max_left N)
-- Module: Mathlib.Analysis.SumOverResidueClass
Goal:
f : ℕ → ℝ
hf : Antitone f
n : ℕ
hn : f n < 0
hs : Summable f
this : ∀ ε > 0, ∃ (N : ℕ), ∀ n ≥ N, |f n| < ε
N : ℕ
H : f (max n N) ≤ f n
rwa : -f n ≤ |f (max n N)|
rwa₁ : -f n ≤ -f (max n N)
rwa₂ rwa₃ rwa₄ rwa₅ : f (max n N) ≤ f n
⊢ |f n| ≤ |f (max n N)|

Tactic:
rwa [abs_of_neg hn, abs_of_neg (H.trans_lt hn), neg_le_neg_iff]

Premises used: abs_of_neg, LE.le.trans_lt, neg_le_neg_iff
-- Module: Mathlib.Analysis.SumOverResidueClass
Goal:
m : ℕ
hm : NeZero m
f : ℕ → ℝ
hf : Antitone f
n : ℕ
hn : f n < 0
k : ZMod m
rw : ¬Summable (α := ℝ) fun (n : ℕ) ↦ f (m * n + k.val)
⊢ ¬Summable (Set.indicator {n : ℕ | (↑n : ZMod m) = k} f)

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

Premises used: ZMod.natCast_zmod_val, summable_indicator_mod_iff_summable
-- Module: Mathlib.Analysis.SumOverResidueClass
Goal:
m : ℕ
hm : NeZero m
f : ℕ → ℝ
hf : Antitone f
n : ℕ
hn : f n < 0
k : ZMod m
⊢ ¬Summable (α := ℝ) fun (n : ℕ) ↦ f (m * n + k.val)

Tactic:
not_summable_of_antitone_of_neg
    (hf.comp_monotone <| (Covariant.monotone_of_const m).add_const k.val) <|
    (hf <| (Nat.le_mul_of_pos_left n Fin.pos').trans <| Nat.le_add_right ..).trans_lt hn

Premises used: not_summable_of_antitone_of_neg, Nat.le_add_right, Antitone.comp_monotone, Monotone.add_const, Covariant.monotone_of_const, Nat.le_mul_of_pos_left, LE.le.trans, Fin.pos', LE.le.trans_lt, ZMod.val
-- Module: Mathlib.Analysis.SumOverResidueClass
Goal:
m : ℕ
hm : NeZero m
f : ℕ → ℝ
hf : Antitone f
n : ℕ
hn : f n < 0
k : ZMod m
⊢ ¬Summable (α := ℝ) fun (n : ℕ) ↦ f (m * n + k.val)

Tactic:
exact not_summable_of_antitone_of_neg
    (hf.comp_monotone <| (Covariant.monotone_of_const m).add_const k.val) <|
    (hf <| (Nat.le_mul_of_pos_left n Fin.pos').trans <| Nat.le_add_right ..).trans_lt hn

Premises used: not_summable_of_antitone_of_neg, Nat.le_add_right, Antitone.comp_monotone, Monotone.add_const, Covariant.monotone_of_const, Nat.le_mul_of_pos_left, LE.le.trans, Fin.pos', LE.le.trans_lt, ZMod.val
-- Module: Mathlib.Analysis.SumOverResidueClass
Goal:
m : ℕ
inst : NeZero m
f : ℕ → ℝ
hf : Antitone f
k l : ZMod m
hs : Summable (Set.indicator {n : ℕ | (↑n : ZMod m) = k} f)
pos : ∀ (hf₀ : ∀ (n : ℕ), 0 ≤ f n), Summable (Set.indicator {n : ℕ | (↑n : ZMod m) = l} f)
neg : ∀ (hf₀ : ∃ (n : ℕ), f n < 0), Summable (Set.indicator {n : ℕ | (↑n : ZMod m) = l} f)
⊢ Summable (Set.indicator {n : ℕ | (↑n : ZMod m) = l} f)

Tactic:
by_cases! hf₀ : ∀ n, 0 ≤ f n
-- Module: Mathlib.Analysis.SumOverResidueClass
Goal:
m : ℕ
inst : NeZero m
f : ℕ → ℝ
hf : Antitone f
k l : ZMod m
hs : Summable (Set.indicator {n : ℕ | (↑n : ZMod m) = k} f)
hf₀ : ∀ (n : ℕ), 0 ≤ f n
⊢ Summable (α := ℝ) fun (n : ℕ) ↦ f (m * n + k.val)

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

Premises used: ZMod.natCast_zmod_val, summable_indicator_mod_iff_summable
-- Module: Mathlib.Analysis.SumOverResidueClass
Goal:
m : ℕ
inst : NeZero m
f : ℕ → ℝ
hf : Antitone f
k l : ZMod m
hs : Summable (Set.indicator {n : ℕ | (↑n : ZMod m) = k} f)
hf₀ : ∀ (n : ℕ), 0 ≤ f n
hs₁ : Summable (α := ℝ) fun (n : ℕ) ↦ f (m * n + k.val)
⊢ ∀ (n : ℕ), 0 ≤ f n

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

Premises used: ZMod.natCast_zmod_val, summable_indicator_mod_iff_summable
-- Module: Mathlib.Analysis.SumOverResidueClass
Goal:
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
⊢ HAdd.hAdd (α := ZMod m) (↑l.val : ZMod m) (↑m : ZMod m) = l

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

Premises used: CharP.cast_eq_zero, ZMod.natCast_val, ZMod.cast_id', add_zero, id_eq
-- Module: Mathlib.Analysis.SumOverResidueClass
Goal:
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
⊢ HAdd.hAdd (α := ZMod m) (↑l.val : ZMod m) (↑m : ZMod m) = l

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]
-- Module: Mathlib.Analysis.SumOverResidueClass
Goal:
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 : HAdd.hAdd (α := ZMod m) (↑l.val : ZMod m) (↑m : ZMod m) = l
pos : Summable (α := ℝ) fun (n : ℕ) ↦ f (m * n + (l.val + m))
⊢ Summable (Set.indicator {n : ℕ | (↑n : ZMod m) = l} f)

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

Premises used: Nat.cast_add, summable_indicator_mod_iff_summable
-- Module: Mathlib.Analysis.SumOverResidueClass
Goal:
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 : HAdd.hAdd (α := ZMod m) (↑l.val : ZMod m) (↑m : ZMod m) = l
⊢ Summable (α := ℝ) fun (n : ℕ) ↦ f (m * n + (l.val + m))

Tactic:
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

Premises used: HMul.hMul, Nat.le_add_left, LT.lt.le, Summable.of_nonneg_of_le, HAdd.hAdd, LT.lt.trans_le, Nat.add_le_add, Nat.le.refl, ZMod.val_lt, ZMod.val
-- Module: Mathlib.Analysis.SumOverResidueClass
Goal:
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 : HAdd.hAdd (α := ZMod m) (↑l.val : ZMod m) (↑m : ZMod 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

Premises used: Nat.le_add_left, LT.lt.le, Summable.of_nonneg_of_le, LT.lt.trans_le, Nat.add_le_add, Nat.le.refl, ZMod.val_lt, ZMod.val
-- Module: Mathlib.Analysis.SumOverResidueClass
Goal:
m : ℕ
inst : NeZero m
f : ℕ → ℝ
hf : Antitone f
k l : ZMod m
hs : Summable (Set.indicator {n : ℕ | (↑n : ZMod m) = k} f)
hf₀ : ∃ (n : ℕ), f n < 0
neg : ∀ (n : ℕ) (hn : f n < 0), Summable (Set.indicator {n : ℕ | (↑n : ZMod m) = l} f)
⊢ Summable (Set.indicator {n : ℕ | (↑n : ZMod m) = l} f)

Tactic:
obtain ⟨n, hn⟩ := hf₀
-- Module: Mathlib.Analysis.SumOverResidueClass
Goal:
m : ℕ
inst : NeZero m
f : ℕ → ℝ
hf : Antitone f
k l : ZMod m
hs : Summable (Set.indicator {n : ℕ | (↑n : ZMod m) = k} f)
n : ℕ
hn : f n < 0
⊢ Summable (Set.indicator {n : ℕ | (↑n : ZMod m) = l} f)

Tactic:
(not_summable_indicator_mod_of_antitone_of_neg hf hn k hs).elim

Premises used: False.elim, not_summable_indicator_mod_of_antitone_of_neg
-- Module: Mathlib.Analysis.SumOverResidueClass
Goal:
m : ℕ
inst : NeZero m
f : ℕ → ℝ
hf : Antitone f
k l : ZMod m
hs : Summable (Set.indicator {n : ℕ | (↑n : ZMod m) = k} f)
n : ℕ
hn : f n < 0
⊢ Summable (Set.indicator {n : ℕ | (↑n : ZMod m) = l} f)

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

Premises used: False.elim, not_summable_indicator_mod_of_antitone_of_neg
-- Module: Mathlib.Analysis.SumOverResidueClass
Goal:
m : ℕ
inst : NeZero m
f : ℕ → ℝ
hf : Antitone f
k : ZMod m
⊢ Summable (Set.indicator {n : ℕ | (↑n : ZMod m) = k} f) ↔ Summable f

Tactic:
⟨fun H ↦ ?_, fun H ↦ Summable.indicator H _⟩

Premises used: setOf, Nat.cast, Iff.intro, Summable.indicator, Eq
-- Module: Mathlib.Analysis.SumOverResidueClass
Goal:
m : ℕ
inst : NeZero m
f : ℕ → ℝ
hf : Antitone f
k : ZMod m
refine : ∀ (H : Summable (Set.indicator {n : ℕ | (↑n : ZMod m) = k} f)), Summable f
⊢ Summable (Set.indicator {n : ℕ | (↑n : ZMod m) = k} f) ↔ Summable f

Tactic:
refine ⟨fun H ↦ ?_, fun H ↦ Summable.indicator H _⟩
-- Module: Mathlib.Analysis.SumOverResidueClass
Goal:
m : ℕ
inst : NeZero m
f : ℕ → ℝ
hf : Antitone f
k : ZMod m
H : Summable (Set.indicator {n : ℕ | (↑n : ZMod m) = k} f)
rw : Summable (α := ℝ) (∑ a : ZMod m, Set.indicator {n : ℕ | (↑n : ZMod m) = a} f)
⊢ Summable f

Tactic:
rw [Finset.sum_indicator_mod m f]

Premises used: Finset.sum_indicator_mod
-- Module: Mathlib.Analysis.SumOverResidueClass
Goal:
m : ℕ
inst : NeZero m
f : ℕ → ℝ
hf : Antitone f
k : ZMod m
H : Summable (Set.indicator {n : ℕ | (↑n : ZMod m) = k} f)
⊢ Summable (α := ℝ) fun (b : ℕ) ↦ ∑ i : ZMod m, Set.indicator {n : ℕ | (↑n : ZMod m) = i} f b

Tactic:
summable_sum (s := Finset.univ) fun a _ ↦
      summable_indicator_mod_iff_summable_indicator_mod hf a H

Premises used: summable_sum, summable_indicator_mod_iff_summable_indicator_mod
-- Module: Mathlib.Analysis.SumOverResidueClass
Goal:
m : ℕ
inst : NeZero m
f : ℕ → ℝ
hf : Antitone f
k : ZMod m
H : Summable (Set.indicator {n : ℕ | (↑n : ZMod m) = k} f)
h :
  ∀ (x : ℕ),
    Eq (α := ℝ) ((∑ a : ZMod m, Set.indicator {n : ℕ | (↑n : ZMod m) = a} f) x)
      (∑ i : ZMod m, Set.indicator {n : ℕ | (↑n : ZMod m) = i} f x)
⊢ Summable (α := ℝ) (∑ a : ZMod m, Set.indicator {n : ℕ | (↑n : ZMod m) = a} f)

Tactic:
convert!
    summable_sum (s := Finset.univ) fun a _ ↦
      summable_indicator_mod_iff_summable_indicator_mod hf a H

Premises used: summable_sum, summable_indicator_mod_iff_summable_indicator_mod
-- Module: Mathlib.Analysis.SumOverResidueClass
Goal:
m : ℕ
inst : NeZero m
f : ℕ → ℝ
hf : Antitone f
k : ZMod m
H : Summable (Set.indicator {n : ℕ | (↑n : ZMod m) = k} f)
x : ℕ
⊢ Eq (α := ℝ) ((∑ a : ZMod m, Set.indicator {n : ℕ | (↑n : ZMod m) = a} f) x)
    (∑ i : ZMod m, Set.indicator {n : ℕ | (↑n : ZMod m) = i} f x)

Tactic:
simp only [Finset.sum_apply]

Premises used: Finset.sum_apply
-- Module: Mathlib.Analysis.SumOverResidueClass
Goal:
R : Type u_1
inst : AddCommGroup R
inst_1 : UniformSpace R
inst_2 : IsUniformAddGroup R
inst_3 : CompleteSpace R
inst_4 : T0Space R
f : ℕ → R
hf : Summable f
N : ℕ
inst_5 : NeZero N
rw : Summable.{u_1, 0} (α := R) fun (c : ZMod N × ℕ) ↦ f ((N.residueClassesEquiv.symm : (a : ZMod N × ℕ) → ℕ) c)
⊢ Eq.{u_1 + 1} (α := R) (∑' (n : ℕ), f n) (∑ j : ZMod N, ∑' (m : ℕ), f (j.val + N * m))

Tactic:
rw [← (residueClassesEquiv N).symm.tsum_eq f, Summable.tsum_prod, tsum_fintype,
    residueClassesEquiv, Equiv.coe_fn_symm_mk]

Premises used: Equiv.coe_fn_symm_mk, Nat.residueClassesEquiv, Equiv.tsum_eq, Summable.tsum_prod, tsum_fintype, Equiv.symm
-- Module: Mathlib.Analysis.SumOverResidueClass
Goal:
R : Type u_1
inst : AddCommGroup R
inst_1 : UniformSpace R
inst_2 : IsUniformAddGroup R
inst_3 : CompleteSpace R
inst_4 : T0Space R
f : ℕ → R
hf : Summable f
N : ℕ
inst_5 : NeZero N
⊢ Summable.{u_1, 0} (α := R) fun (c : ZMod N × ℕ) ↦ f ((N.residueClassesEquiv.symm : (a : ZMod N × ℕ) → ℕ) c)

Tactic:
hf.comp_injective (residueClassesEquiv N).symm.injective

Premises used: Nat.residueClassesEquiv, Summable.comp_injective, Equiv.injective, Equiv.symm
-- Module: Mathlib.Analysis.SumOverResidueClass
Goal:
R : Type u_1
inst : AddCommGroup R
inst_1 : UniformSpace R
inst_2 : IsUniformAddGroup R
inst_3 : CompleteSpace R
inst_4 : T0Space R
f : ℕ → R
hf : Summable f
N : ℕ
inst_5 : NeZero N
⊢ Summable.{u_1, 0} (α := R) fun (c : ZMod N × ℕ) ↦ f ((N.residueClassesEquiv.symm : (a : ZMod N × ℕ) → ℕ) c)

Tactic:
exact hf.comp_injective (residueClassesEquiv N).symm.injective

Premises used: Nat.residueClassesEquiv, Summable.comp_injective, Equiv.injective, Equiv.symm
-- Module: Mathlib.Analysis.VonNeumannAlgebra.Basic
Goal:
H : Type u
inst : NormedAddCommGroup H
inst_1 : InnerProductSpace ℂ H
inst_2 : CompleteSpace H
S : VonNeumannAlgebra H
x : H →L[ℂ] H
⊢ x ∈ S.toStarSubalgebra ↔ x ∈ (↑S : Set (H →L[ℂ] H))

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl
-- Module: Mathlib.Analysis.VonNeumannAlgebra.Basic
Goal:
H : Type u
inst : NormedAddCommGroup H
inst_1 : InnerProductSpace ℂ H
inst_2 : CompleteSpace H
S : VonNeumannAlgebra H
⊢ (↑S.toStarSubalgebra : Set (H →L[ℂ] H)) = (↑S : Set (H →L[ℂ] H))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.VonNeumannAlgebra.Basic
Goal:
H : Type u
inst : NormedAddCommGroup H
inst_1 : InnerProductSpace ℂ H
inst_2 : CompleteSpace H
S : StarSubalgebra ℂ (H →L[ℂ] H)
h : S.carrier.centralizer.centralizer = S.carrier
⊢ (↑{ toStarSubalgebra := S, centralizer_centralizer' := h : VonNeumannAlgebra H } : Set (H →L[ℂ] H)) =
    (↑S : Set (H →L[ℂ] H))

Tactic:
rfl

Premises used: rfl