MobiusLemma.sum_sq_div_moebius_is_multiplicative_explicit

lemma sum_sq_div_moebius_is_multiplicative_explicit : (sum_sq_div_moebius 1 = 1) ∧    (∀ m n : ℕ, Nat.Coprime m n →      sum_sq_div_moebius (m * n) = sum_sq_div_moebius m * sum_sq_div_moebius n) := by  have h_map : ∀ m n, m.Coprime n →      (Nat.divisors (m * n)).filter (fun d ↦ d ^ 2 ∣ m * n) =        image (fun p : ℕ × ℕ ↦ p.1 * p.2)          ((Nat.divisors m).filter (fun d ↦ d ^ 2 ∣ m) ×ˢ            (Nat.divisors n).filter (fun d ↦ d ^ 2 ∣ n)) := by    intro m n hmn    ext d    simp only [mem_filter, Nat.mem_divisors, ne_eq, mul_eq_zero, not_or, mem_image,      mem_product, Prod.exists]    refine ⟨fun hd ↦ ?_, ?_⟩    swap    · rintro ⟨a, b, ⟨⟨⟨ha₁, ha₂⟩, ha₃⟩, ⟨⟨hb₁, hb₂⟩, hb₃⟩⟩, rfl⟩      exact ⟨⟨mul_dvd_mul ha₁ hb₁, ha₂, hb₂⟩, by convert! mul_dvd_mul ha₃ hb₃ using 1; ring⟩    obtain ⟨hd_div, hd_sq_div⟩ := hd    obtain ⟨a, b, ha, hb, rfl⟩ : ∃ a b : ℕ, a ∣ m ∧ b ∣ n ∧ d = a * b :=      Exists.imp (by grind) (Nat.dvd_mul.mp hd_div.1)    simp_all only [mul_pow, not_false_eq_true, and_true]    exact ⟨a, b, ⟨⟨ha, (hmn.coprime_dvd_left ha).pow_left 2 |>.dvd_of_dvd_mul_right <|      dvd_of_mul_right_dvd hd_sq_div⟩, hb,      (hmn.symm.coprime_dvd_left hb).pow_left 2 |>.dvd_of_dvd_mul_left <|        dvd_of_mul_left_dvd hd_sq_div⟩, rfl⟩  have h_sum : ∀ m n : ℕ, Nat.Coprime m n →      ∑ d ∈ (Nat.divisors (m * n)).filter (fun d ↦ d ^ 2 ∣ m * n), (moebius d : ℤ) =        ∑ a ∈ (Nat.divisors m).filter (fun d ↦ d ^ 2 ∣ m),          ∑ b ∈ (Nat.divisors n).filter (fun d ↦ d ^ 2 ∣ n), (moebius (a * b) : ℤ) := by    intro m n hmn    rw [h_map m n hmn, sum_image, sum_product]    intro p hp q hq h_eq    have hp1_eq_q1 : p.1 = q.1 := by      norm_num at *      have hdvd : p.1 ∣ q.1 ∧ q.1 ∣ p.1 :=        ⟨(hmn.coprime_dvd_left (by grind)).coprime_dvd_right (by grind) |>.dvd_of_dvd_mul_right <|          h_eq ▸ dvd_mul_right _ _,         (hmn.coprime_dvd_left (by grind)).coprime_dvd_right (by grind) |>.dvd_of_dvd_mul_right <|          h_eq.symm ▸ dvd_mul_right _ _⟩      exact Nat.dvd_antisymm hdvd.1 hdvd.2    aesop  have h_inner : ∀ m n, m.Coprime n → ∀ a ∈ (Nat.divisors m).filter (fun d ↦ d ^ 2 ∣ m),      ∀ b ∈ (Nat.divisors n).filter (fun d ↦ d ^ 2 ∣ n),        (moebius (a * b) : ℤ) = (moebius a : ℤ) * (moebius b : ℤ) := by    intro m n hmn a ha b hb    simp only [moebius, mem_filter, Nat.mem_divisors, ne_eq, Int.reduceNeg, coe_mk,      mul_ite, ite_mul, zero_mul, mul_zero] at *    split_ifs with h <;> simp_all only [Nat.squarefree_mul_iff, and_self, and_true, ne_eq,      Int.reduceNeg, zero_eq_mul, pow_eq_zero_iff', neg_eq_zero, one_ne_zero,      cardFactors_eq_zero_iff_eq_zero_or_one, not_or, false_and, or_self, and_false]    · rw [← pow_add, cardFactors_mul]      · intro a; simp_all [Int.reduceNeg]      · intro a; simp_all [Int.reduceNeg]    · exact h (hmn.coprime_dvd_left ha.1.1 |>.coprime_dvd_right hb.1.1)  dsimp only [sum_sq_div_moebius]  exact ⟨by simp [sum_filter], fun m n hmn ↦ by    rw [h_sum m n hmn, sum_mul]    exact sum_congr rfl fun i hi ↦ by      rw [mul_sum]; exact sum_congr rfl fun j hj ↦ h_inner m n hmn i hi j hj⟩