simp only [MulZeroClass.zero_mul, eq_self_iff_true, h_mult.map_mul_of_coprime
  (coprime_of_squarefree_mul h_sq), h_zero]
case intro
f : ArithmeticFunction ℝ
h_mult : f.IsMultiplicative
m : ℕ
h_zero : f m = 0
k : ℕ
h_sq : Squarefree (m * k)
⊢ f (m * k) = 0
no goals