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

case neg
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
a : Fin k → ℕ
ha : a ∈ Fintype.piFinset fun _i => P.divisors
h : ¬↑(∏ i : Fin k, a i) ≤ x
⊢ 0 ≤ ∏ i : Fin k, if ↑(a i) ≤ x then (↑(a i))⁻¹ else 0