rw [sum_eq_single (∏ i, a i)]
case calc_2
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
a : Fin k → ℕ
a✝ : a ∈ Fintype.piFinset fun _i => P.divisors
⊢ (∑ x_1 ∈ P.divisors, if ∏ i : Fin k, a i = x_1 ∧ x_1 ∣ P then if ↑x_1 ≤ x then (↑x_1)⁻¹ else 0 else 0) =
    if ∏ i : Fin k, a i ∣ P then if ↑(∏ i : Fin k, a i) ≤ x then ∏ i : Fin k, (↑(a i))⁻¹ else 0 else 0
case calc_2
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
a : Fin k → ℕ
a✝ : a ∈ Fintype.piFinset fun _i => P.divisors
⊢ (if ∏ i : Fin k, a i = ∏ i : Fin k, a i ∧ ∏ i : Fin k, a i ∣ P then
      if ↑(∏ i : Fin k, a i) ≤ x then (↑(∏ i : Fin k, a i))⁻¹ else 0
    else 0) =
    if ∏ i : Fin k, a i ∣ P then if ↑(∏ i : Fin k, a i) ≤ x then ∏ i : Fin k, (↑(a i))⁻¹ else 0 else 0

case calc_2.h₀
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
a : Fin k → ℕ
a✝ : a ∈ Fintype.piFinset fun _i => P.divisors
⊢ ∀ b ∈ P.divisors,
    b ≠ ∏ i : Fin k, a i → (if ∏ i : Fin k, a i = b ∧ b ∣ P then if ↑b ≤ x then (↑b)⁻¹ else 0 else 0) = 0

case calc_2.h₁
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
a : Fin k → ℕ
a✝ : a ∈ Fintype.piFinset fun _i => P.divisors
⊢ ∏ i : Fin k, a i ∉ P.divisors →
    (if ∏ i : Fin k, a i = ∏ i : Fin k, a i ∧ ∏ i : Fin k, a i ∣ P then
        if ↑(∏ i : Fin k, a i) ≤ x then (↑(∏ i : Fin k, a i))⁻¹ else 0
      else 0) =
      0