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

State before:
X : Type
f : Filter X
g : X → ℂ
⊢ Tendsto (fun x => ↑(g x)) f (𝓝 ∞) ↔ Tendsto (fun x => g x) f atInf
Tactic:
constructor
State after:
case mp
X : Type
f : Filter X
g : X → ℂ
⊢ Tendsto (fun x => ↑(g x)) f (𝓝 ∞) → Tendsto (fun x => g x) f atInf

case mpr
X : Type
f : Filter X
g : X → ℂ
⊢ Tendsto (fun x => g x) f atInf → Tendsto (fun x => ↑(g x)) f (𝓝 ∞)

State before:
case mp
X : Type
f : Filter X
g : X → ℂ
⊢ Tendsto (fun x => ↑(g x)) f (𝓝 ∞) → Tendsto (fun x => g x) f atInf
Tactic:
intro t
State after:
case mp
X : Type
f : Filter X
g : X → ℂ
t : Tendsto (fun x => ↑(g x)) f (𝓝 ∞)
⊢ Tendsto (fun x => g x) f atInf

State before:
case mp
X : Type
f : Filter X
g : X → ℂ
t : Tendsto (fun x => ↑(g x)) f (𝓝 ∞)
⊢ Tendsto (fun x => g x) f atInf
Tactic:
simp only [Filter.tendsto_iff_comap] at t ⊢
State after:
case mp
X : Type
f : Filter X
g : X → ℂ
t : f ≤ Filter.comap (fun x => ↑(g x)) (𝓝 ∞)
⊢ f ≤ Filter.comap (fun x => g x) atInf

State before:
case mp
X : Type
f : Filter X
g : X → ℂ
t : f ≤ Filter.comap (fun x => ↑(g x)) (𝓝 ∞)
⊢ f ≤ Filter.comap (fun x => g x) atInf
Tactic:
rw [←Function.comp_def, ←Filter.comap_comap, OnePoint.comap_coe_nhds_infty,
  Filter.coclosedCompact_eq_cocompact, ←atInf_eq_cocompact] at t
State after:
case mp
X : Type
f : Filter X
g : X → ℂ
t : f ≤ Filter.comap (fun x => g x) atInf
⊢ f ≤ Filter.comap (fun x => g x) atInf

State before:
case mp
X : Type
f : Filter X
g : X → ℂ
t : f ≤ Filter.comap (fun x => g x) atInf
⊢ f ≤ Filter.comap (fun x => g x) atInf
Tactic:
exact t
State after:
no goals

State before:
case mpr
X : Type
f : Filter X
g : X → ℂ
⊢ Tendsto (fun x => g x) f atInf → Tendsto (fun x => ↑(g x)) f (𝓝 ∞)
Tactic:
exact fun h ↦ coe_tendsto_inf.comp h
State after:
no goals