apply sum_le_sum
case calc_4
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
⊢ (∑ a ∈ Fintype.piFinset fun _i => P.divisors, if ↑(∏ i : Fin k, a i) ≤ x then ∏ i : Fin k, (↑(a i))⁻¹ else 0) ≤
    ∑ a ∈ Fintype.piFinset fun _i => P.divisors, ∏ i : Fin k, if ↑(a i) ≤ x then (↑(a i))⁻¹ else 0
case calc_4.h
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
⊢ ∀ i ∈ Fintype.piFinset fun _i => P.divisors,
    (if ↑(∏ i_1 : Fin k, i i_1) ≤ x then ∏ i_1 : Fin k, (↑(i i_1))⁻¹ else 0) ≤
      ∏ i_1 : Fin k, if ↑(i i_1) ≤ x then (↑(i i_1))⁻¹ else 0