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

State before:
⊢ ∞ ≠ 0
Tactic:
have e : (0 : 𝕊) = ((0 : ℂ) : 𝕊) := rfl
State after:
e : 0 = ↑0
⊢ ∞ ≠ 0

State before:
e : 0 = ↑0
⊢ ∞ ≠ 0
Tactic:
rw [e]
State after:
e : 0 = ↑0
⊢ ∞ ≠ ↑0

State before:
e : 0 = ↑0
⊢ ∞ ≠ ↑0
Tactic:
exact inf_ne_coe
State after:
no goals