refactor: golf only Cyclotomic/Basic, ArithmeticFunction/Zeta

Mathlib/NumberTheory/ArithmeticFunction/Defs.lean

@@ -262,15 +262,11 @@ theorem mul_smul' (f g : ArithmeticFunction R) (h : ArithmeticFunction M) :
 
 theorem one_smul' (b : ArithmeticFunction M) : (1 : ArithmeticFunction R) • b = b := by
   ext x
-  rw [smul_apply]
-  by_cases x0 : x = 0
-  · simp [x0]
-  have h : {(1, x)} ⊆ divisorsAntidiagonal x := by simp [x0]
-  rw [← sum_subset h]
+  rw [smul_apply, ← Nat.map_div_right_divisors, sum_map, sum_eq_single 1]
   · simp
-  intro y ymem ynotMem
-  have y1ne : y.fst ≠ 1 := fun con => by simp_all [Prod.ext_iff]
-  simp [y1ne]
+  · intro d hd hd1
+    simp [one_apply_ne hd1]
+  · simpa using fun hx : x = 0 => by simp [hx]
 
 end Module
 
@@ -282,17 +278,11 @@ instance instMonoid : Monoid (ArithmeticFunction R) where
   one_mul := one_smul'
   mul_one f := by
     ext x
-    rw [mul_apply]
-    by_cases x0 : x = 0
-    · simp [x0]
-    have h : {(x, 1)} ⊆ divisorsAntidiagonal x := by simp [x0]
-    rw [← sum_subset h]
+    rw [mul_apply, ← Nat.map_div_left_divisors, sum_map, sum_eq_single 1]
     · simp
-    intro ⟨y₁, y₂⟩ ymem ynotMem
-    have y2ne : y₂ ≠ 1 := by
-      intro con
-      simp_all
-    simp [y2ne]
+    · intro d hd hd1
+      simp [one_apply_ne hd1]
+    · simpa using fun hx : x = 0 => by simp [hx]
   mul_assoc := mul_smul'
 
 instance instSemiring : Semiring (ArithmeticFunction R) where

Mathlib/NumberTheory/ArithmeticFunction/Zeta.lean

@@ -78,18 +78,14 @@ theorem coe_zeta_mul_apply [Semiring R] {f : ArithmeticFunction R} {x : ℕ} :
     (ζ * f) x = ∑ i ∈ divisors x, f i :=
   coe_zeta_smul_apply
 
-theorem coe_mul_zeta_apply [Semiring R] {f : ArithmeticFunction R} {x : ℕ} :
-    (f * ζ) x = ∑ i ∈ divisors x, f i := by
-  rw [mul_apply]
-  trans ∑ i ∈ divisorsAntidiagonal x, f i.1
-  · refine sum_congr rfl fun i hi => ?_
-    rcases mem_divisorsAntidiagonal.1 hi with ⟨rfl, h⟩
-    rw [natCoe_apply, zeta_apply_ne (right_ne_zero_of_mul h), cast_one, mul_one]
-  · rw [← map_div_right_divisors, sum_map, Function.Embedding.coeFn_mk]
-
 theorem coe_zeta_mul_comm [Semiring R] {f : ArithmeticFunction R} : ζ * f = f * ζ := by
   ext x
-  rw [coe_zeta_mul_apply, coe_mul_zeta_apply]
+  rw [mul_apply, ← map_swap_divisorsAntidiagonal, Finset.sum_map]
+  simp [mul_apply]
+
+theorem coe_mul_zeta_apply [Semiring R] {f : ArithmeticFunction R} {x : ℕ} :
+    (f * ζ) x = ∑ i ∈ divisors x, f i := by
+  rw [← coe_zeta_mul_comm, coe_zeta_mul_apply]
 
 theorem zeta_mul_apply {f : ArithmeticFunction ℕ} {x : ℕ} : (ζ * f) x = ∑ i ∈ divisors x, f i := by
   rw [← natCoe_nat ζ, coe_zeta_mul_apply]