exact fun _ => rfl
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
a : Fin k → ℕ
a✝ : a ∈ Fintype.piFinset fun _i => P.divisors
⊢ ∏ i : Fin k, a i ∣ P → ∏ i : Fin k, a i = ∏ i : Fin k, a i

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