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