update with to_additive

Author: CBirkbeck

Mathlib/Analysis/SpecialFunctions/Trigonometric/Cotangent.lean

@@ -216,10 +216,9 @@ theorem cot_series_rep' (hz : x ∈ ℂ_ℤ) : π * cot (π * x) - 1 / x =
 /-- The cotangent infinite sum representation. -/
 theorem cot_series_rep (hz : x ∈ ℂ_ℤ) :
     π * cot (π * x) = 1 / x + ∑' n : ℕ+, (1 / (x - n) + 1 / (x + n)) := by
-  have h0 := tsum_pnat_eq_tsum_succ fun n ↦ 1 / (x - n) + 1 / (x + n)
-  have h1 := cot_series_rep' hz
-  simp only [one_div, Nat.cast_add, Nat.cast_one] at *
-  rw [h0, ← h1]
+  have h0 := tsum_pnat_eq_tsum_succ (f := fun n ↦ 1 / (x - n) + 1 / (x + n))
+  rw [one_div] at *
+  rw [h0, ← cot_series_rep' hz]
   ring
 
 end MittagLeffler

Mathlib/Topology/Algebra/InfiniteSum/NatInt.lean

@@ -540,53 +540,32 @@ section pnat
 
 variable {α R : Type*} [TopologicalSpace α] [CommMonoid α] [AddMonoidWithOne R]
 
---remove these once the to_additive bug is fixed below.
-@[to_additive]
-theorem pnat_multipliable_iff_multipliable_succ
-    {f : ℕ → α} : Multipliable (fun x : ℕ+ => f x) ↔ Multipliable fun x : ℕ => f (x + 1) :=
-  Equiv.pnatEquivNat.symm.multipliable_iff.symm
-
-@[to_additive]
-theorem tprod_pnat_eq_tprod_succ (f : ℕ → α) :
-    ∏' n : ℕ+, f n = ∏' n, f (n + 1) := (Equiv.pnatEquivNat.symm.tprod_eq _).symm
-
-@[to_additive]
-lemma tprod_zero_pnat_eq_tprod_nat {α : Type*} [TopologicalSpace α] [CommGroup α]
-    [IsTopologicalGroup α] [T2Space α] (f : ℕ → α) (hf : Multipliable f) :
-    f 0 * ∏' (n : ℕ+), f ↑n = ∏' (n : ℕ), f n := by
-  simp [Multipliable.tprod_eq_zero_mul hf, tprod_pnat_eq_tprod_succ f]
 
-theorem pnat_multipliable_iff_multipliable_succ' {f : R → α} :
+@[to_additive (dont_translate := R)]
+theorem pnat_multipliable_iff_multipliable_succ {f : R → α} :
     Multipliable (fun x : ℕ+ => f x) ↔ Multipliable fun x : ℕ => f (x + 1) := by
   convert Equiv.pnatEquivNat.symm.multipliable_iff.symm
   simp
 
-theorem pnat_summable_iff_summable_succ' {α : Type*} [TopologicalSpace α]
-  [AddCommMonoid α] {f : R → α} :
-  Summable (fun x : ℕ+ => f x) ↔ Summable fun x : ℕ => f (x + 1) := by
-  convert Equiv.pnatEquivNat.symm.summable_iff.symm
-  simp
-
-theorem tprod_pnat_eq_tprod_succ'
-    (f : R → α) : ∏' n : ℕ+, f n = ∏' (n : ℕ), f (n + 1) := by
+@[to_additive (dont_translate := R)]
+theorem tprod_pnat_eq_tprod_succ {f : R → α} : ∏' n : ℕ+, f n = ∏' (n : ℕ), f (n + 1) := by
   convert (Equiv.pnatEquivNat.symm.tprod_eq _).symm
   simp
 
-theorem tsum_pnat_eq_tsum_succ' {α : Type*}
-    [TopologicalSpace α] [AddCommMonoid α]
-    (f : R → α) : ∑' n : ℕ+, f n = ∑' (n : ℕ), f (n + 1) := by
-  convert (Equiv.pnatEquivNat.symm.tsum_eq _).symm
-  simp
+@[to_additive]
+lemma tprod_zero_pnat_eq_tprod_nat {α : Type*} [TopologicalSpace α] [CommGroup α]
+    [IsTopologicalGroup α] [T2Space α] (f : ℕ → α) (hf : Multipliable f) :
+    f 0 * ∏' (n : ℕ+), f ↑n = ∏' (n : ℕ), f n := by
+  simpa [Multipliable.tprod_eq_zero_mul hf] using tprod_pnat_eq_tprod_succ (f := f)
 
 theorem tsum_nat_eq_zero_two_pnat {α : Type*} [UniformSpace α] [Ring α] [IsUniformAddGroup α]
     [CompleteSpace α] [T2Space α] {f : ℤ → α} (hf : ∀ n : ℤ, f n = f (-n)) (hf2 : Summable f) :
     ∑' n, f n = f 0 + 2 * ∑' n : ℕ+, f n := by
   rw [tsum_of_add_one_of_neg_add_one]
   · conv =>
-      enter [1,2,1]
-      ext n
+      enter [1,2,1,n]
       rw [hf]
-    simp only [neg_add_rev, Int.reduceNeg, neg_neg, tsum_pnat_eq_tsum_succ', two_mul]
+    simp only [neg_add_rev, Int.reduceNeg, neg_neg, tsum_pnat_eq_tsum_succ, two_mul]
     abel
   · simpa using ((summable_nat_add_iff (k := 1)).mpr
       (summable_int_iff_summable_nat_and_neg.mp hf2).1)