Theorem: RiemannSphere.coe_tendsto_inf' (Ray/AnalyticManifold/RiemannSphere.lean)

State before:
e : {∞}ᶜ = range fun z => ↑z
⊢ Tendsto (fun z => ↑z) atInf (𝓝[≠] ∞)
Tactic:
simp only [e, tendsto_nhdsWithin_range, coe_tendsto_inf]
State after:
no goals

State before:
⊢ {∞}ᶜ = range fun z => ↑z
Tactic:
ext z
State after:
case h
z : 𝕊
⊢ z ∈ {∞}ᶜ ↔ z ∈ range fun z => ↑z

State before:
case h
z : 𝕊
⊢ z ∈ {∞}ᶜ ↔ z ∈ range fun z => ↑z
Tactic:
induction' z using OnePoint.rec with z
State after:
case h.h₁

⊢ ∞ ∈ {∞}ᶜ ↔ ∞ ∈ range fun z => ↑z

case h.h₂
z : ℂ
⊢ ↑z ∈ {∞}ᶜ ↔ ↑z ∈ range fun z => ↑z

State before:
case h.h₁

⊢ ∞ ∈ {∞}ᶜ ↔ ∞ ∈ range fun z => ↑z
Tactic:
simp only [mem_compl_iff, mem_singleton_iff, not_true, mem_range, OnePoint.coe_ne_infty,
  exists_false]
State after:
no goals

State before:
case h.h₂
z : ℂ
⊢ ↑z ∈ {∞}ᶜ ↔ ↑z ∈ range fun z => ↑z
Tactic:
simp only [mem_compl_iff, mem_singleton_iff, OnePoint.coe_ne_infty, not_false_eq_true,
  mem_range, coe_eq_coe, exists_eq]
State after:
no goals