ArithmeticFunction.sum_moebius_sq_divisors_IsMultiplicative

@[blueprint  "sum_moebius_sq_divisors_IsMultiplicative"  (title := "sum-moebius-sq-divisors-is-multiplicative")  (statement := /-- The function $n \mapsto \sum_{d^2|n} \mu(d)$ is multiplicative. -/)  (proof := /--    We will show that for coprime $m$ and $n$, we have    $\sum_{d^2|mn} \mu(d) = \sum_{d^2|m} \mu(d) \cdot \sum_{d^2|n} \mu(d)$. This follows from    Lemma \ref{pow-divisors-mul}: the divisors $d$ of $mn$ with $d^2 \mid mn$ factor uniquely as    $d=ab$ with $a^2 \mid m$ and $b^2 \mid n$. Multiplicativity of $\mu$ then factors the sum.  -/)]lemma sum_moebius_sq_divisors_IsMultiplicative : sum_moebius_sq_divisors.IsMultiplicative := by  unfold sum_moebius_sq_divisors  refine ⟨by simp only [sum_filter, coe_mk, divisors_one, dvd_one, pow_eq_one_iff,    OfNat.ofNat_ne_zero, or_false, sum_ite_eq', mem_singleton, ↓reduceIte, isUnit_iff_eq_one,    IsUnit.squarefree, moebius_apply_of_squarefree, Int.reduceNeg, cardFactors_one, pow_zero], ?_⟩  intro m n mCn  simp only [coe_mk, pow_divisors_mul mCn, Finset.sum_product,    Finset.sum_image (fun x hx y hy => pow_divisors_mul_injective (k := 2) mCn      (Finset.coe_product _ _ ▸ Finset.mem_coe.mpr hx)      (Finset.coe_product _ _ ▸ Finset.mem_coe.mpr hy))]  trans (∑ i ∈ m.divisors.filter (fun x => x ^ 2 ∣ m), ∑ j ∈ n.divisors.filter (fun x => x ^ 2 ∣ n), μ i * μ j)  · apply Finset.sum_congr rfl    intro _ hi    apply Finset.sum_congr rfl    intro _ hj    exact isMultiplicative_moebius.map_mul_of_coprime      (mCn.coprime_dvd_left (Nat.dvd_of_mem_divisors (Finset.filter_subset _ _ hi))        |>.coprime_dvd_right (Nat.dvd_of_mem_divisors (Finset.filter_subset _ _ hj)))  · rw [← Finset.sum_mul_sum]