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

State before:
⊢ Continuous fun z => z⁻¹
Tactic:
rw [continuous_iff_continuousOn_univ]
State after:
⊢ ContinuousOn (fun z => z⁻¹) univ

State before:
⊢ ContinuousOn (fun z => z⁻¹) univ
Tactic:
intro z _
State after:
z : 𝕊
a✝ : z ∈ univ
⊢ ContinuousWithinAt (fun z => z⁻¹) univ z

State before:
z : 𝕊
a✝ : z ∈ univ
⊢ ContinuousWithinAt (fun z => z⁻¹) univ z
Tactic:
apply ContinuousAt.continuousWithinAt
State after:
case h
z : 𝕊
a✝ : z ∈ univ
⊢ ContinuousAt (fun z => z⁻¹) z

State before:
case h
z : 𝕊
a✝ : z ∈ univ
⊢ ContinuousAt (fun z => z⁻¹) z
Tactic:
induction' z using OnePoint.rec with z
State after:
case h.h₁
a✝ : ∞ ∈ univ
⊢ ContinuousAt (fun z => z⁻¹) ∞

case h.h₂
z : ℂ
a✝ : ↑z ∈ univ
⊢ ContinuousAt (fun z => z⁻¹) ↑z

State before:
case h.h₁
a✝ : ∞ ∈ univ
⊢ ContinuousAt (fun z => z⁻¹) ∞
Tactic:
simp only [OnePoint.continuousAt_infty', Function.comp, Filter.coclosedCompact_eq_cocompact,
  inv_inf, ← atInf_eq_cocompact]
State after:
case h.h₁
a✝ : ∞ ∈ univ
⊢ Tendsto (fun x => (↑x)⁻¹) atInf (𝓝 0)

State before:
case h.h₁
a✝ : ∞ ∈ univ
⊢ Tendsto (fun x => (↑x)⁻¹) atInf (𝓝 0)
Tactic:
have e : ∀ᶠ z : ℂ in atInf, ↑z⁻¹ = (↑z : 𝕊)⁻¹ := by
  refine (eventually_atInf 0).mp (eventually_of_forall fun z z0 ↦ ?_)
  simp only [gt_iff_lt, Complex.norm_eq_abs, AbsoluteValue.pos_iff] at z0; rw [inv_coe z0]
State after:
case h.h₁
a✝ : ∞ ∈ univ
e : ∀ᶠ (z : ℂ) in atInf, ↑z⁻¹ = (↑z)⁻¹
⊢ Tendsto (fun x => (↑x)⁻¹) atInf (𝓝 0)

State before:
case h.h₁
a✝ : ∞ ∈ univ
e : ∀ᶠ (z : ℂ) in atInf, ↑z⁻¹ = (↑z)⁻¹
⊢ Tendsto (fun x => (↑x)⁻¹) atInf (𝓝 0)
Tactic:
apply Filter.Tendsto.congr' e
State after:
case h.h₁
a✝ : ∞ ∈ univ
e : ∀ᶠ (z : ℂ) in atInf, ↑z⁻¹ = (↑z)⁻¹
⊢ Tendsto (fun x => ↑x⁻¹) atInf (𝓝 0)

State before:
case h.h₁
a✝ : ∞ ∈ univ
e : ∀ᶠ (z : ℂ) in atInf, ↑z⁻¹ = (↑z)⁻¹
⊢ Tendsto (fun x => ↑x⁻¹) atInf (𝓝 0)
Tactic:
exact Filter.Tendsto.comp continuous_coe.continuousAt inv_tendsto_atInf'
State after:
no goals

State before:
a✝ : ∞ ∈ univ
⊢ ∀ᶠ (z : ℂ) in atInf, ↑z⁻¹ = (↑z)⁻¹
Tactic:
refine (eventually_atInf 0).mp (eventually_of_forall fun z z0 ↦ ?_)
State after:
a✝ : ∞ ∈ univ
z : ℂ
z0 : ‖z‖ > 0
⊢ ↑z⁻¹ = (↑z)⁻¹

State before:
a✝ : ∞ ∈ univ
z : ℂ
z0 : ‖z‖ > 0
⊢ ↑z⁻¹ = (↑z)⁻¹
Tactic:
simp only [gt_iff_lt, Complex.norm_eq_abs, AbsoluteValue.pos_iff] at z0
State after:
a✝ : ∞ ∈ univ
z : ℂ
z0 : z ≠ 0
⊢ ↑z⁻¹ = (↑z)⁻¹

State before:
a✝ : ∞ ∈ univ
z : ℂ
z0 : z ≠ 0
⊢ ↑z⁻¹ = (↑z)⁻¹
Tactic:
rw [inv_coe z0]
State after:
no goals

State before:
case h.h₂
z : ℂ
a✝ : ↑z ∈ univ
⊢ ContinuousAt (fun z => z⁻¹) ↑z
Tactic:
simp only [OnePoint.continuousAt_coe, Function.comp, inv_def, inv, WithTop.coe_eq_zero,
  toComplex_coe]
State after:
case h.h₂
z : ℂ
a✝ : ↑z ∈ univ
⊢ ContinuousAt (fun x => if ↑x = 0 then ∞ else ↑x⁻¹) z

State before:
case h.h₂
z : ℂ
a✝ : ↑z ∈ univ
⊢ ContinuousAt (fun x => if ↑x = 0 then ∞ else ↑x⁻¹) z
Tactic:
by_cases z0 : z = 0
State after:
case pos
z : ℂ
a✝ : ↑z ∈ univ
z0 : z = 0
⊢ ContinuousAt (fun x => if ↑x = 0 then ∞ else ↑x⁻¹) z

case neg
z : ℂ
a✝ : ↑z ∈ univ
z0 : ¬z = 0
⊢ ContinuousAt (fun x => if ↑x = 0 then ∞ else ↑x⁻¹) z

State before:
case pos
z : ℂ
a✝ : ↑z ∈ univ
z0 : z = 0
⊢ ContinuousAt (fun x => if ↑x = 0 then ∞ else ↑x⁻¹) z
Tactic:
simp only [z0, ContinuousAt, OnePoint.nhds_infty_eq, eq_self_iff_true, if_true,
  Filter.coclosedCompact_eq_cocompact]
State after:
case pos
z : ℂ
a✝ : ↑z ∈ univ
z0 : z = 0
⊢ Tendsto (fun x => if ↑x = 0 then ∞ else ↑x⁻¹) (𝓝 0) (𝓝 (if ↑0 = 0 then ∞ else ↑0⁻¹))

State before:
case pos
z : ℂ
a✝ : ↑z ∈ univ
z0 : z = 0
⊢ Tendsto (fun x => if ↑x = 0 then ∞ else ↑x⁻¹) (𝓝 0) (𝓝 (if ↑0 = 0 then ∞ else ↑0⁻¹))
Tactic:
simp only [← nhdsWithin_compl_singleton_sup_pure, Filter.tendsto_sup]
State after:
case pos
z : ℂ
a✝ : ↑z ∈ univ
z0 : z = 0
⊢ Tendsto (fun x => if ↑x = 0 then ∞ else ↑x⁻¹) (𝓝[≠] 0)
      ((𝓝[≠] if ↑0 = 0 then ∞ else ↑0⁻¹) ⊔ pure (if ↑0 = 0 then ∞ else ↑0⁻¹)) ∧
    Tendsto (fun x => if ↑x = 0 then ∞ else ↑x⁻¹) (pure 0)
      ((𝓝[≠] if ↑0 = 0 then ∞ else ↑0⁻¹) ⊔ pure (if ↑0 = 0 then ∞ else ↑0⁻¹))

State before:
case pos
z : ℂ
a✝ : ↑z ∈ univ
z0 : z = 0
⊢ Tendsto (fun x => if ↑x = 0 then ∞ else ↑x⁻¹) (𝓝[≠] 0)
      ((𝓝[≠] if ↑0 = 0 then ∞ else ↑0⁻¹) ⊔ pure (if ↑0 = 0 then ∞ else ↑0⁻¹)) ∧
    Tendsto (fun x => if ↑x = 0 then ∞ else ↑x⁻¹) (pure 0)
      ((𝓝[≠] if ↑0 = 0 then ∞ else ↑0⁻¹) ⊔ pure (if ↑0 = 0 then ∞ else ↑0⁻¹))
Tactic:
constructor
State after:
case pos.left
z : ℂ
a✝ : ↑z ∈ univ
z0 : z = 0
⊢ Tendsto (fun x => if ↑x = 0 then ∞ else ↑x⁻¹) (𝓝[≠] 0)
    ((𝓝[≠] if ↑0 = 0 then ∞ else ↑0⁻¹) ⊔ pure (if ↑0 = 0 then ∞ else ↑0⁻¹))

case pos.right
z : ℂ
a✝ : ↑z ∈ univ
z0 : z = 0
⊢ Tendsto (fun x => if ↑x = 0 then ∞ else ↑x⁻¹) (pure 0)
    ((𝓝[≠] if ↑0 = 0 then ∞ else ↑0⁻¹) ⊔ pure (if ↑0 = 0 then ∞ else ↑0⁻¹))

State before:
case pos.left
z : ℂ
a✝ : ↑z ∈ univ
z0 : z = 0
⊢ Tendsto (fun x => if ↑x = 0 then ∞ else ↑x⁻¹) (𝓝[≠] 0)
    ((𝓝[≠] if ↑0 = 0 then ∞ else ↑0⁻¹) ⊔ pure (if ↑0 = 0 then ∞ else ↑0⁻¹))
Tactic:
refine Filter.Tendsto.mono_right ?_ le_sup_left
State after:
case pos.left
z : ℂ
a✝ : ↑z ∈ univ
z0 : z = 0
⊢ Tendsto (fun x => if ↑x = 0 then ∞ else ↑x⁻¹) (𝓝[≠] 0) (𝓝[≠] if ↑0 = 0 then ∞ else ↑0⁻¹)

State before:
case pos.left
z : ℂ
a✝ : ↑z ∈ univ
z0 : z = 0
⊢ Tendsto (fun x => if ↑x = 0 then ∞ else ↑x⁻¹) (𝓝[≠] 0) (𝓝[≠] if ↑0 = 0 then ∞ else ↑0⁻¹)
Tactic:
apply tendsto_nhdsWithin_congr (f := fun z : ℂ ↦ (↑z⁻¹ : 𝕊))
State after:
case pos.left.hfg
z : ℂ
a✝ : ↑z ∈ univ
z0 : z = 0
⊢ ∀ x ∈ {0}ᶜ, ↑x⁻¹ = if ↑x = 0 then ∞ else ↑x⁻¹

case pos.left.hf
z : ℂ
a✝ : ↑z ∈ univ
z0 : z = 0
⊢ Tendsto (fun z => ↑z⁻¹) (𝓝[≠] 0) (𝓝[≠] if ↑0 = 0 then ∞ else ↑0⁻¹)

State before:
case pos.left.hfg
z : ℂ
a✝ : ↑z ∈ univ
z0 : z = 0
⊢ ∀ x ∈ {0}ᶜ, ↑x⁻¹ = if ↑x = 0 then ∞ else ↑x⁻¹
Tactic:
intro z m
State after:
case pos.left.hfg
z✝ : ℂ
a✝ : ↑z✝ ∈ univ
z0 : z✝ = 0
z : ℂ
m : z ∈ {0}ᶜ
⊢ ↑z⁻¹ = if ↑z = 0 then ∞ else ↑z⁻¹

State before:
case pos.left.hfg
z✝ : ℂ
a✝ : ↑z✝ ∈ univ
z0 : z✝ = 0
z : ℂ
m : z ∈ {0}ᶜ
⊢ ↑z⁻¹ = if ↑z = 0 then ∞ else ↑z⁻¹
Tactic:
rw [mem_compl_singleton_iff] at m
State after:
case pos.left.hfg
z✝ : ℂ
a✝ : ↑z✝ ∈ univ
z0 : z✝ = 0
z : ℂ
m : z ≠ 0
⊢ ↑z⁻¹ = if ↑z = 0 then ∞ else ↑z⁻¹

State before:
case pos.left.hfg
z✝ : ℂ
a✝ : ↑z✝ ∈ univ
z0 : z✝ = 0
z : ℂ
m : z ≠ 0
⊢ ↑z⁻¹ = if ↑z = 0 then ∞ else ↑z⁻¹
Tactic:
simp only [coe_eq_zero, m, ite_false]
State after:
no goals

State before:
case pos.left.hf
z : ℂ
a✝ : ↑z ∈ univ
z0 : z = 0
⊢ Tendsto (fun z => ↑z⁻¹) (𝓝[≠] 0) (𝓝[≠] if ↑0 = 0 then ∞ else ↑0⁻¹)
Tactic:
simp only [coe_zero, ite_true]
State after:
case pos.left.hf
z : ℂ
a✝ : ↑z ∈ univ
z0 : z = 0
⊢ Tendsto (fun z => ↑z⁻¹) (𝓝[≠] 0) (𝓝[≠] ∞)

State before:
case pos.left.hf
z : ℂ
a✝ : ↑z ∈ univ
z0 : z = 0
⊢ Tendsto (fun z => ↑z⁻¹) (𝓝[≠] 0) (𝓝[≠] ∞)
Tactic:
apply coe_tendsto_inf'.comp
State after:
case pos.left.hf
z : ℂ
a✝ : ↑z ∈ univ
z0 : z = 0
⊢ Tendsto (fun z => z⁻¹) (𝓝[≠] 0) atInf

State before:
case pos.left.hf
z : ℂ
a✝ : ↑z ∈ univ
z0 : z = 0
⊢ Tendsto (fun z => z⁻¹) (𝓝[≠] 0) atInf
Tactic:
rw [← @tendsto_atInf_iff_tendsto_nhds_zero ℂ ℂ _ _ fun z : ℂ ↦ z]
State after:
case pos.left.hf
z : ℂ
a✝ : ↑z ∈ univ
z0 : z = 0
⊢ Tendsto (fun z => z) atInf atInf

State before:
case pos.left.hf
z : ℂ
a✝ : ↑z ∈ univ
z0 : z = 0
⊢ Tendsto (fun z => z) atInf atInf
Tactic:
exact Filter.tendsto_id
State after:
no goals

State before:
case pos.right
z : ℂ
a✝ : ↑z ∈ univ
z0 : z = 0
⊢ Tendsto (fun x => if ↑x = 0 then ∞ else ↑x⁻¹) (pure 0)
    ((𝓝[≠] if ↑0 = 0 then ∞ else ↑0⁻¹) ⊔ pure (if ↑0 = 0 then ∞ else ↑0⁻¹))
Tactic:
refine Filter.Tendsto.mono_right ?_ le_sup_right
State after:
case pos.right
z : ℂ
a✝ : ↑z ∈ univ
z0 : z = 0
⊢ Tendsto (fun x => if ↑x = 0 then ∞ else ↑x⁻¹) (pure 0) (pure (if ↑0 = 0 then ∞ else ↑0⁻¹))

State before:
case pos.right
z : ℂ
a✝ : ↑z ∈ univ
z0 : z = 0
⊢ Tendsto (fun x => if ↑x = 0 then ∞ else ↑x⁻¹) (pure 0) (pure (if ↑0 = 0 then ∞ else ↑0⁻¹))
Tactic:
simp only [Filter.pure_zero, Filter.tendsto_pure, ite_eq_left_iff, Filter.eventually_zero,
  eq_self_iff_true, not_true, IsEmpty.forall_iff]
State after:
no goals

State before:
case neg
z : ℂ
a✝ : ↑z ∈ univ
z0 : ¬z = 0
⊢ ContinuousAt (fun x => if ↑x = 0 then ∞ else ↑x⁻¹) z
Tactic:
have e : ∀ᶠ w : ℂ in 𝓝 z, (if w = 0 then ∞ else ↑w⁻¹ : 𝕊) = ↑w⁻¹ := by
  refine (continuousAt_id.eventually_ne z0).mp (eventually_of_forall fun w w0 ↦ ?_)
  simp only [Ne, id_eq] at w0; simp only [w0, if_false]
State after:
case neg
z : ℂ
a✝ : ↑z ∈ univ
z0 : ¬z = 0
e : ∀ᶠ (w : ℂ) in 𝓝 z, (if w = 0 then ∞ else ↑w⁻¹) = ↑w⁻¹
⊢ ContinuousAt (fun x => if ↑x = 0 then ∞ else ↑x⁻¹) z

State before:
case neg
z : ℂ
a✝ : ↑z ∈ univ
z0 : ¬z = 0
e : ∀ᶠ (w : ℂ) in 𝓝 z, (if w = 0 then ∞ else ↑w⁻¹) = ↑w⁻¹
⊢ ContinuousAt (fun x => if ↑x = 0 then ∞ else ↑x⁻¹) z
Tactic:
simp only [coe_eq_zero, continuousAt_congr e]
State after:
case neg
z : ℂ
a✝ : ↑z ∈ univ
z0 : ¬z = 0
e : ∀ᶠ (w : ℂ) in 𝓝 z, (if w = 0 then ∞ else ↑w⁻¹) = ↑w⁻¹
⊢ ContinuousAt (fun x => ↑x⁻¹) z

State before:
case neg
z : ℂ
a✝ : ↑z ∈ univ
z0 : ¬z = 0
e : ∀ᶠ (w : ℂ) in 𝓝 z, (if w = 0 then ∞ else ↑w⁻¹) = ↑w⁻¹
⊢ ContinuousAt (fun x => ↑x⁻¹) z
Tactic:
exact continuous_coe.continuousAt.comp (tendsto_inv₀ z0)
State after:
no goals

State before:
z : ℂ
a✝ : ↑z ∈ univ
z0 : ¬z = 0
⊢ ∀ᶠ (w : ℂ) in 𝓝 z, (if w = 0 then ∞ else ↑w⁻¹) = ↑w⁻¹
Tactic:
refine (continuousAt_id.eventually_ne z0).mp (eventually_of_forall fun w w0 ↦ ?_)
State after:
z : ℂ
a✝ : ↑z ∈ univ
z0 : ¬z = 0
w : ℂ
w0 : id w ≠ 0
⊢ (if w = 0 then ∞ else ↑w⁻¹) = ↑w⁻¹

State before:
z : ℂ
a✝ : ↑z ∈ univ
z0 : ¬z = 0
w : ℂ
w0 : id w ≠ 0
⊢ (if w = 0 then ∞ else ↑w⁻¹) = ↑w⁻¹
Tactic:
simp only [Ne, id_eq] at w0
State after:
z : ℂ
a✝ : ↑z ∈ univ
z0 : ¬z = 0
w : ℂ
w0 : ¬w = 0
⊢ (if w = 0 then ∞ else ↑w⁻¹) = ↑w⁻¹

State before:
z : ℂ
a✝ : ↑z ∈ univ
z0 : ¬z = 0
w : ℂ
w0 : ¬w = 0
⊢ (if w = 0 then ∞ else ↑w⁻¹) = ↑w⁻¹
Tactic:
simp only [w0, if_false]
State after:
no goals