rw [←h_mult.lcm_apply_mul_gcd_apply]
R : Type u_1
inst✝ : CommGroupWithZero R
f : ArithmeticFunction R
h_mult : f.IsMultiplicative
x y : ℕ
hf : f (x.gcd y) ≠ 0
⊢ f (x.lcm y) = f x * f y / f (x.gcd y)
R : Type u_1
inst✝ : CommGroupWithZero R
f : ArithmeticFunction R
h_mult : f.IsMultiplicative
x y : ℕ
hf : f (x.gcd y) ≠ 0
⊢ f (x.lcm y) = f (x.lcm y) * f (x.gcd y) / f (x.gcd y)