MobiusLemma.sum_sq_div_moebius_eq_squarefree

lemma sum_sq_div_moebius_eq_squarefree (n : ℕ) (hn : n > 0) :    sum_sq_div_moebius n = if Squarefree n then 1 else 0 := by  induction n using Nat.strongRecOn with | _ n ih =>  by_cases h_prime_pow : ∃ p k, p.Prime ∧ n = p ^ k;  · obtain ⟨p, k, hp, rfl⟩ := h_prime_pow;    rw [sum_sq_div_moebius_prime_pow]    · rcases k with (_ | _ | k) <;> simp_all only [zero_add, pow_one, gt_iff_lt,        Nat.one_lt_ofNat, ↓reduceIte, left_eq_ite_iff, one_ne_zero, imp_false, Decidable.not_not]      · simp_all      · exact hp.squarefree      · rw [if_neg (by grind), if_neg (by rw [Nat.squarefree_pow_iff] <;> aesop)]    · assumption  · obtain ⟨m, n', hm, hn', h_coprime⟩ : ∃ m n' : ℕ, 1 < m ∧ 1 < n' ∧ m.Coprime n' ∧ n = m * n' := by      obtain ⟨p, hp⟩ : ∃ p, p.Prime ∧ p ∣ n :=        Nat.exists_prime_and_dvd fun rfl ↦ h_prime_pow ⟨2, 0, Nat.prime_two, rfl⟩      obtain ⟨k, m, hm⟩ : ∃ k m, n = p ^ k * m ∧ ¬p ∣ m :=        ⟨Nat.factorization n p, n / p ^ Nat.factorization n p, by          rw [Nat.mul_div_cancel' (Nat.ordProj_dvd n p)], Nat.not_dvd_ordCompl hp.1 hn.ne'⟩      simp only [gt_iff_lt, exists_and_left, not_exists, not_and] at *      exact ⟨p ^ k, one_lt_pow₀ hp.1.one_lt (by specialize h_prime_pow p hp.1 k; aesop), m,        Nat.one_lt_iff_ne_zero_and_ne_one.mpr ⟨by grind, by specialize h_prime_pow p hp.1 k; grind⟩,          Nat.Coprime.pow_left _ (hp.1.coprime_iff_not_dvd.mpr hm.2), hm.1⟩    have h_mul : sum_sq_div_moebius n = sum_sq_div_moebius m * sum_sq_div_moebius n' :=      h_coprime.2.symm ▸ sum_sq_div_moebius_is_multiplicative_explicit.2 _ _ h_coprime.1    simp_all [Nat.squarefree_mul_iff]    aesop