Theorem: isOpen_aux (PrimeNumberTheoremAnd/ZetaBounds.lean)

State before:
⊢ IsOpen {z | z ≠ 1 ∧ 0 < z.re}
Tactic:
refine IsOpen.inter isOpen_ne ?_
State after:
⊢ IsOpen fun z => Real.lt 0 z.re

State before:
⊢ IsOpen fun z => Real.lt 0 z.re
Tactic:
exact isOpen_lt (g := fun (z : ℂ) ↦ z.re) (by continuity) (by continuity)
State after:
no goals

State before:
⊢ Continuous fun z => 0
Tactic:
continuity
State after:
no goals

State before:
⊢ Continuous fun z => z.re
Tactic:
continuity
State after:
no goals