rcases hmn with ⟨k, rfl⟩
f : ArithmeticFunction ℝ
h_mult : f.IsMultiplicative
m n : ℕ
h_sq : Squarefree n
hmn : m ∣ n
h_zero : f m = 0
⊢ f n = 0
case intro
f : ArithmeticFunction ℝ
h_mult : f.IsMultiplicative
m : ℕ
h_zero : f m = 0
k : ℕ
h_sq : Squarefree (m * k)
⊢ f (m * k) = 0