gcongr
case calc_5
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
⊢ (∑ a ∈ filter (fun d => ↑d ≤ x) P.divisors, (↑a)⁻¹) ^ k ≤ (1 + x.log) ^ k
case calc_5.hab
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
⊢ ∑ a ∈ filter (fun d => ↑d ≤ x) P.divisors, (↑a)⁻¹ ≤ 1 + x.log