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

State before:
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
s : Set ℂ
f : s ∈ atInf
⊢ (fun z => ↑z) '' s ∪ {∞} ∈ 𝓝 ∞
Tactic:
simp only [OnePoint.nhds_infty_eq, Filter.mem_sup, Filter.coclosedCompact_eq_cocompact, ←
  atInf_eq_cocompact, Filter.mem_map]
State after:
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
s : Set ℂ
f : s ∈ atInf
⊢ OnePoint.some ⁻¹' ((fun z => ↑z) '' s ∪ {∞}) ∈ atInf ∧ (fun z => ↑z) '' s ∪ {∞} ∈ pure ∞

State before:
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
s : Set ℂ
f : s ∈ atInf
⊢ OnePoint.some ⁻¹' ((fun z => ↑z) '' s ∪ {∞}) ∈ atInf ∧ (fun z => ↑z) '' s ∪ {∞} ∈ pure ∞
Tactic:
exact ⟨Filter.mem_of_superset f fun _ m ↦ Or.inl (mem_image_of_mem _ m), Or.inr rfl⟩
State after:
no goals