rw [← h_mult.right, Nat.div_mul_cancel hdl]
f : ArithmeticFunction ℝ
h_mult : f.IsMultiplicative
l d : ℕ
hdl : d ∣ l
hl : Squarefree l
hd : f d ≠ 0
⊢ f l = f (l / d) * f d
f : ArithmeticFunction ℝ
h_mult : f.IsMultiplicative
l d : ℕ
hdl : d ∣ l
hl : Squarefree l
hd : f d ≠ 0
⊢ (l / d).Coprime d