rw [sum_comm]
case calc_2
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
⊢ (∑ d ∈ P.divisors,
      ∑ 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) =
    ∑ a ∈ Fintype.piFinset fun _i => P.divisors,
      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
⊢ (∑ y ∈ Fintype.piFinset fun _i => P.divisors,
      ∑ x_1 ∈ P.divisors, if ∏ i : Fin k, y i = x_1 ∧ x_1 ∣ P then if ↑x_1 ≤ x then (↑x_1)⁻¹ else 0 else 0) =
    ∑ a ∈ Fintype.piFinset fun _i => P.divisors,
      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