simp_rw [ite_and]
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) =
    ∑ a ∈ Fintype.piFinset fun _i => P.divisors,
      if ∏ i : Fin k, a i = d ∧ d ∣ P then if ↑d ≤ x then (↑d)⁻¹ else 0 else 0
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) =
    ∑ x_1 ∈ Fintype.piFinset fun _i => P.divisors,
      if ∏ i : Fin k, x_1 i = d then if d ∣ P then if ↑d ≤ x then (↑d)⁻¹ else 0 else 0 else 0