rw [s.nu_mult.mult_lcm_eq_of_ne_zero]
s : Sieve
w : ℕ → ℝ
d1 : ℕ
hd1 : d1 ∈ P.divisors
d2 : ℕ
hd2 : d2 ∈ P.divisors
h : d1.lcm d2 ∣ P
⊢ w d1 * w d2 * ν (d1.lcm d2) = ν d1 * w d1 * ν d2 * w d2 * (ν (d1.gcd d2))⁻¹
s : Sieve
w : ℕ → ℝ
d1 : ℕ
hd1 : d1 ∈ P.divisors
d2 : ℕ
hd2 : d2 ∈ P.divisors
h : d1.lcm d2 ∣ P
⊢ w d1 * w d2 * (ν d1 * ν d2 / ν (d1.gcd d2)) = ν d1 * w d1 * ν d2 * w d2 * (ν (d1.gcd d2))⁻¹

case hf
s : Sieve
w : ℕ → ℝ
d1 : ℕ
hd1 : d1 ∈ P.divisors
d2 : ℕ
hd2 : d2 ∈ P.divisors
h : d1.lcm d2 ∣ P
⊢ ν (d1.gcd d2) ≠ 0