simp only [div_eq_mul_inv, one_mul, nsmul_eq_mul, cast_pow, mul_ite, mul_zero]
case calc_1
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
d : ℕ
hd : d ∣ P ∧ P ≠ 0
⊢ (if ↑d ≤ x then ↑k ^ ω d / ↑d else 0) = k ^ ω d • if ↑d ≤ x then (↑d)⁻¹ else 0
no goals