refactor(NumberTheory): golf Mathlib/NumberTheory/ArithmeticFunction/Defs (leanprover-community#40072)

- golfs `ArithmeticFunction/Defs` by replacing explicit divisor-antidiagonal singleton arguments in the left-identity theorem and `mul_one` with direct `simp_all` calls using divisor map lemmas and `sum_eq_single`

Extracted from leanprover-community#38144

[![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)

Author: yuanyi-350

Mathlib/NumberTheory/ArithmeticFunction/Defs.lean

@@ -262,15 +262,7 @@ 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]
-  · simp
-  intro y ymem ynotMem
-  have y1ne : y.fst ≠ 1 := fun con => by simp_all [Prod.ext_iff]
-  simp [y1ne]
+  simp_all [← map_div_right_divisors, sum_eq_single 1]
 
 end Module
 
@@ -282,17 +274,7 @@ 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]
-    · simp
-    intro ⟨y₁, y₂⟩ ymem ynotMem
-    have y2ne : y₂ ≠ 1 := by
-      intro con
-      simp_all
-    simp [y2ne]
+    simp_all [← map_div_left_divisors, sum_eq_single 1]
   mul_assoc := mul_smul'
 
 instance instSemiring : Semiring (ArithmeticFunction R) where