intro d
case h
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
⊢ filter (fun d => ↑d ≤ x) P.divisors ⊆ Icc 1 ⌊x⌋₊

case hf
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
⊢ ∀ i ∈ Icc 1 ⌊x⌋₊, i ∉ filter (fun d => ↑d ≤ x) P.divisors → 0 ≤ (↑i)⁻¹
case h
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
d : ℕ
⊢ d ∈ filter (fun d => ↑d ≤ x) P.divisors → d ∈ Icc 1 ⌊x⌋₊

case hf
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
⊢ ∀ i ∈ Icc 1 ⌊x⌋₊, i ∉ filter (fun d => ↑d ≤ x) P.divisors → 0 ≤ (↑i)⁻¹