Theorem: RiemannSphere.inf_ne_coe (Ray/AnalyticManifold/RiemannSphere.lean)

State before:
z : ℂ
⊢ ∞ ≠ ↑z
Tactic:
simp only [Ne, OnePoint.infty_ne_coe, not_false_iff]
State after:
no goals