Theorem: primorial_bounds (PrimeNumberTheoremAnd/Consequences.lean)

State before:
⊢ ∃ E, (E =o[atTop] fun x => x) ∧ ∀ (x : ℝ), ↑(∏ p ∈ filter Nat.Prime (range ⌊x⌋₊), p) = rexp (x + E x)
Tactic:
sorry
State after:
no goals