internlm/Lean-Github huggingface dataset:
Theorem: RiemannSphere.continuous_inv
Proof 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]
Proof 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⁻¹))
Theorem: RiemannSphere.continuous_inv
Proof 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]
Proof 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⁻¹))
Theorem: RiemannSphere.continuous_inv
Proof 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
Proof 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⁻¹))
Theorem: RiemannSphere.continuous_inv
Proof 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
Proof 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⁻¹)
Theorem: RiemannSphere.continuous_inv
Proof 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⁻¹ : 𝕊))
Proof 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⁻¹)
Theorem: RiemannSphere.continuous_inv
Proof 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
Proof state after:
case pos.left.hfg
z✝ : ℂ
a✝ : ↑z✝ ∈ univ
z0 : z✝ = 0
z : ℂ
m : z ∈ {0}ᶜ
⊢ ↑z⁻¹ = if ↑z = 0 then ∞ else ↑z⁻¹
Theorem: RiemannSphere.continuous_inv
Proof 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
Proof state after:
case pos.left.hfg
z✝ : ℂ
a✝ : ↑z✝ ∈ univ
z0 : z✝ = 0
z : ℂ
m : z ≠ 0
⊢ ↑z⁻¹ = if ↑z = 0 then ∞ else ↑z⁻¹
Theorem: RiemannSphere.continuous_inv
Proof 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]
Proof state after:
no goals
Theorem: RiemannSphere.continuous_inv
Proof 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]
Proof state after:
case pos.left.hf
z : ℂ
a✝ : ↑z ∈ univ
z0 : z = 0
⊢ Tendsto (fun z => ↑z⁻¹) (𝓝[≠] 0) (𝓝[≠] ∞)
Theorem: RiemannSphere.continuous_inv
Proof state before:
case pos.left.hf
z : ℂ
a✝ : ↑z ∈ univ
z0 : z = 0
⊢ Tendsto (fun z => ↑z⁻¹) (𝓝[≠] 0) (𝓝[≠] ∞)
Tactic:
apply coe_tendsto_inf'.comp
Proof state after:
case pos.left.hf
z : ℂ
a✝ : ↑z ∈ univ
z0 : z = 0
⊢ Tendsto (fun z => z⁻¹) (𝓝[≠] 0) atInf
Theorem: RiemannSphere.continuous_inv
Proof 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]
Proof state after:
case pos.left.hf
z : ℂ
a✝ : ↑z ∈ univ
z0 : z = 0
⊢ Tendsto (fun z => z) atInf atInf
Theorem: RiemannSphere.continuous_inv
Proof state before:
case pos.left.hf
z : ℂ
a✝ : ↑z ∈ univ
z0 : z = 0
⊢ Tendsto (fun z => z) atInf atInf
Tactic:
exact Filter.tendsto_id
Proof state after:
no goals
Theorem: RiemannSphere.continuous_inv
Proof 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
Proof 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⁻¹))
Theorem: RiemannSphere.continuous_inv
Proof 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]
Proof state after:
no goals
Theorem: RiemannSphere.continuous_inv
Proof 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]
Proof 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
Theorem: RiemannSphere.continuous_inv
Proof 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]
Proof 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
Theorem: RiemannSphere.continuous_inv
Proof 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)
Proof state after:
no goals
Theorem: RiemannSphere.continuous_inv
Proof 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 ↦ ?_)
Proof state after:
z : ℂ
a✝ : ↑z ∈ univ
z0 : ¬z = 0
w : ℂ
w0 : id w ≠ 0
⊢ (if w = 0 then ∞ else ↑w⁻¹) = ↑w⁻¹
Theorem: RiemannSphere.continuous_inv
Proof 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
Proof state after:
z : ℂ
a✝ : ↑z ∈ univ
z0 : ¬z = 0
w : ℂ
w0 : ¬w = 0
⊢ (if w = 0 then ∞ else ↑w⁻¹) = ↑w⁻¹
Theorem: RiemannSphere.continuous_inv
Proof 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]
Proof state after:
no goals
Theorem: RiemannSphere.invEquiv_apply
Proof state before:
z : 𝕊
⊢ invEquiv z = z⁻¹
Tactic:
simp only [invEquiv, Equiv.coe_fn_mk]
Proof state after:
no goals
Theorem: RiemannSphere.invEquiv_symm
Proof state before:
⊢ invEquiv.symm = invEquiv
Tactic:
simp only [Equiv.ext_iff, invEquiv, Equiv.coe_fn_symm_mk, Equiv.coe_fn_mk, eq_self_iff_true,
  forall_const]
Proof state after:
no goals
Theorem: RiemannSphere.invHomeomorph_apply
Proof state before:
z : 𝕊
⊢ invHomeomorph z = z⁻¹
Tactic:
simp only [invHomeomorph, Homeomorph.homeomorph_mk_coe, invEquiv_apply]
Proof state after:
no goals
Theorem: RiemannSphere.invHomeomorph_symm
Proof state before:
⊢ ∀ (x : 𝕊), invHomeomorph.symm x = invHomeomorph x
Tactic:
simp only [invHomeomorph, Homeomorph.homeomorph_mk_coe_symm, invEquiv_symm,
  Homeomorph.homeomorph_mk_coe, eq_self_iff_true, forall_const]
Proof state after:
no goals
Theorem: RiemannSphere.coePartialHomeomorph_target
Proof state before:
⊢ coePartialHomeomorph.target = {∞}ᶜ
Tactic:
simp only [coePartialHomeomorph, coePartialEquiv_target]
Proof state after:
no goals
Theorem: RiemannSphere.invCoePartialHomeomorph_target
Proof state before:
⊢ invCoePartialHomeomorph.target = {0}ᶜ
Tactic:
ext z
Proof state after:
case h
z : 𝕊
⊢ z ∈ invCoePartialHomeomorph.target ↔ z ∈ {0}ᶜ
Theorem: RiemannSphere.invCoePartialHomeomorph_target
Proof state before:
case h
z : 𝕊
⊢ z ∈ invCoePartialHomeomorph.target ↔ z ∈ {0}ᶜ
Tactic:
simp only [invCoePartialHomeomorph, PartialHomeomorph.trans_toPartialEquiv,
PartialEquiv.trans_target, Homeomorph.toPartialHomeomorph_target, PartialHomeomorph.coe_coe_symm,
Homeomorph.toPartialHomeomorph_symm_apply, invHomeomorph_symm, coePartialHomeomorph_target,
preimage_compl, univ_inter, mem_compl_iff, mem_preimage, invHomeomorph_apply, mem_singleton_iff,
inv_eq_inf]
Proof state after:
no goals
Theorem: RiemannSphere.extChartAt_coe
Proof state before:
z : ℂ
⊢ extChartAt I ↑z = coePartialEquiv.symm
Tactic:
simp only [coePartialHomeomorph, extChartAt, PartialHomeomorph.extend, chartAt_coe,
  PartialHomeomorph.symm_toPartialEquiv, modelWithCornersSelf_partialEquiv,
  PartialEquiv.trans_refl]
Proof state after:
no goals
Theorem: RiemannSphere.extChartAt_zero
Proof state before:
⊢ extChartAt I 0 = coePartialEquiv.symm
Tactic:
simp only [← coe_zero, extChartAt_coe]
Proof state after:
no goals
Theorem: RiemannSphere.extChartAt_inf
Proof state before:
⊢ extChartAt I ∞ = invEquiv.toPartialEquiv.trans coePartialEquiv.symm
Tactic:
apply PartialEquiv.ext
Proof state after:
case h

⊢ ∀ (x : 𝕊), ↑(extChartAt I ∞) x = ↑(invEquiv.toPartialEquiv.trans coePartialEquiv.symm) x

case hsymm

⊢ ∀ (x : ℂ), ↑(extChartAt I ∞).symm x = ↑(invEquiv.toPartialEquiv.trans coePartialEquiv.symm).symm x

case hs

⊢ (extChartAt I ∞).source = (invEquiv.toPartialEquiv.trans coePartialEquiv.symm).source
Theorem: RiemannSphere.extChartAt_inf
Proof state before:
case h

⊢ ∀ (x : 𝕊), ↑(extChartAt I ∞) x = ↑(invEquiv.toPartialEquiv.trans coePartialEquiv.symm) x
Tactic:
intro z
Proof state after:
case h
z : 𝕊
⊢ ↑(extChartAt I ∞) z = ↑(invEquiv.toPartialEquiv.trans coePartialEquiv.symm) z
Theorem: RiemannSphere.extChartAt_inf
Proof state before:
case h
z : 𝕊
⊢ ↑(extChartAt I ∞) z = ↑(invEquiv.toPartialEquiv.trans coePartialEquiv.symm) z
Tactic:
simp only [extChartAt, invCoePartialHomeomorph, coePartialHomeomorph, invHomeomorph,
  PartialHomeomorph.extend, chartAt_inf, PartialHomeomorph.symm_toPartialEquiv,
  PartialHomeomorph.trans_toPartialEquiv, modelWithCornersSelf_partialEquiv,
  PartialEquiv.trans_refl, PartialEquiv.coe_trans_symm, PartialHomeomorph.coe_coe_symm,
  Homeomorph.toPartialHomeomorph_symm_apply, Homeomorph.homeomorph_mk_coe_symm, invEquiv_symm,
  PartialEquiv.coe_trans, Equiv.toPartialEquiv_apply]
Proof state after:
no goals
Theorem: RiemannSphere.extChartAt_inf
Proof state before:
case hsymm

⊢ ∀ (x : ℂ), ↑(extChartAt I ∞).symm x = ↑(invEquiv.toPartialEquiv.trans coePartialEquiv.symm).symm x
Tactic:
intro z
Proof state after:
case hsymm
z : ℂ
⊢ ↑(extChartAt I ∞).symm z = ↑(invEquiv.toPartialEquiv.trans coePartialEquiv.symm).symm z
Theorem: RiemannSphere.extChartAt_inf
Proof state before:
case hsymm
z : ℂ
⊢ ↑(extChartAt I ∞).symm z = ↑(invEquiv.toPartialEquiv.trans coePartialEquiv.symm).symm z
Tactic:
simp only [extChartAt, invCoePartialHomeomorph, coePartialHomeomorph, invHomeomorph,
  invEquiv, PartialHomeomorph.extend, chartAt_inf, PartialHomeomorph.symm_toPartialEquiv,
  PartialHomeomorph.trans_toPartialEquiv, modelWithCornersSelf_partialEquiv,
  PartialEquiv.trans_refl, PartialEquiv.symm_symm, PartialEquiv.coe_trans,
  PartialHomeomorph.coe_coe, Homeomorph.toPartialHomeomorph_apply, Homeomorph.homeomorph_mk_coe,
  Equiv.coe_fn_mk, PartialEquiv.coe_trans_symm, Equiv.toPartialEquiv_symm_apply,
  Equiv.coe_fn_symm_mk]
Proof state after:
no goals
Theorem: RiemannSphere.extChartAt_inf
Proof state before:
case hs

⊢ (extChartAt I ∞).source = (invEquiv.toPartialEquiv.trans coePartialEquiv.symm).source
Tactic:
simp only [extChartAt, invCoePartialHomeomorph, coePartialHomeomorph, invHomeomorph,
  PartialHomeomorph.extend, chartAt_inf, PartialHomeomorph.symm_toPartialEquiv,
  PartialHomeomorph.trans_toPartialEquiv, modelWithCornersSelf_partialEquiv,
  PartialEquiv.trans_refl,
  PartialEquiv.symm_source, PartialEquiv.trans_target, Homeomorph.toPartialHomeomorph_target,
  PartialHomeomorph.coe_coe_symm, Homeomorph.toPartialHomeomorph_symm_apply,
  Homeomorph.homeomorph_mk_coe_symm, invEquiv_symm, PartialEquiv.trans_source,
  Equiv.toPartialEquiv_source, Equiv.toPartialEquiv_apply]
Proof state after:
no goals
Theorem: RiemannSphere.extChartAt_inf_apply
Proof state before:
x : 𝕊
⊢ ↑(extChartAt I ∞) x = x⁻¹.toComplex
Tactic:
simp only [extChartAt_inf, PartialEquiv.trans_apply, coePartialEquiv_symm_apply,
  Equiv.toPartialEquiv_apply, invEquiv_apply]
Proof state after:
no goals
Theorem: RiemannSphere.tendsto_inf_iff_tendsto_atInf
Proof state before:
X : Type
f : Filter X
g : X → ℂ
⊢ Tendsto (fun x => ↑(g x)) f (𝓝 ∞) ↔ Tendsto (fun x => g x) f atInf
Tactic:
constructor
Proof 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 (𝓝 ∞)
Theorem: RiemannSphere.tendsto_inf_iff_tendsto_atInf
Proof 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
Proof 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
Theorem: RiemannSphere.tendsto_inf_iff_tendsto_atInf
Proof 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 ⊢
Proof 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
Theorem: RiemannSphere.tendsto_inf_iff_tendsto_atInf
Proof 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
Proof 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
Theorem: RiemannSphere.tendsto_inf_iff_tendsto_atInf
Proof 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
Proof state after:
no goals
Theorem: RiemannSphere.tendsto_inf_iff_tendsto_atInf
Proof 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
Proof state after:
no goals
Theorem: RiemannSphere.isOpenMap_coe
Proof state before:
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
⊢ IsOpenMap fun z => ↑z
Tactic:
intro s o
Proof 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 ℂ
o : IsOpen s
⊢ IsOpen ((fun z => ↑z) '' s)
Theorem: RiemannSphere.isOpenMap_coe
Proof 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 ℂ
o : IsOpen s
⊢ IsOpen ((fun z => ↑z) '' s)
Tactic:
have e : (fun z : ℂ ↦ (z : 𝕊)) '' s = {∞}ᶜ ∩ OnePoint.toComplex ⁻¹' s := by
  apply Set.ext; intro z
  simp only [mem_image, mem_inter_iff, mem_compl_singleton_iff, mem_preimage]
  constructor
  intro ⟨x, m, e⟩; simp only [← e, toComplex_coe, m, and_true_iff]; exact inf_ne_coe.symm
  intro ⟨n, m⟩; use z.toComplex, m, coe_toComplex n
Proof 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 ℂ
o : IsOpen s
e : (fun z => ↑z) '' s = {∞}ᶜ ∩ OnePoint.toComplex ⁻¹' s
⊢ IsOpen ((fun z => ↑z) '' s)
Theorem: RiemannSphere.isOpenMap_coe
Proof 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 ℂ
o : IsOpen s
e : (fun z => ↑z) '' s = {∞}ᶜ ∩ OnePoint.toComplex ⁻¹' s
⊢ IsOpen ((fun z => ↑z) '' s)
Tactic:
rw [e]
Proof 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 ℂ
o : IsOpen s
e : (fun z => ↑z) '' s = {∞}ᶜ ∩ OnePoint.toComplex ⁻¹' s
⊢ IsOpen ({∞}ᶜ ∩ OnePoint.toComplex ⁻¹' s)
Theorem: RiemannSphere.isOpenMap_coe
Proof 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 ℂ
o : IsOpen s
e : (fun z => ↑z) '' s = {∞}ᶜ ∩ OnePoint.toComplex ⁻¹' s
⊢ IsOpen ({∞}ᶜ ∩ OnePoint.toComplex ⁻¹' s)
Tactic:
exact continuousOn_toComplex.isOpen_inter_preimage isOpen_compl_singleton o
Proof state after:
no goals
Theorem: RiemannSphere.isOpenMap_coe
Proof 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 ℂ
o : IsOpen s
⊢ (fun z => ↑z) '' s = {∞}ᶜ ∩ OnePoint.toComplex ⁻¹' s
Tactic:
apply Set.ext
Proof state after:
case h
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
s : Set ℂ
o : IsOpen s
⊢ ∀ (x : 𝕊), x ∈ (fun z => ↑z) '' s ↔ x ∈ {∞}ᶜ ∩ OnePoint.toComplex ⁻¹' s
Theorem: RiemannSphere.isOpenMap_coe
Proof state before:
case h
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
s : Set ℂ
o : IsOpen s
⊢ ∀ (x : 𝕊), x ∈ (fun z => ↑z) '' s ↔ x ∈ {∞}ᶜ ∩ OnePoint.toComplex ⁻¹' s
Tactic:
intro z
Proof state after:
case h
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
s : Set ℂ
o : IsOpen s
z : 𝕊
⊢ z ∈ (fun z => ↑z) '' s ↔ z ∈ {∞}ᶜ ∩ OnePoint.toComplex ⁻¹' s
Theorem: RiemannSphere.isOpenMap_coe
Proof state before:
case h
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
s : Set ℂ
o : IsOpen s
z : 𝕊
⊢ z ∈ (fun z => ↑z) '' s ↔ z ∈ {∞}ᶜ ∩ OnePoint.toComplex ⁻¹' s
Tactic:
simp only [mem_image, mem_inter_iff, mem_compl_singleton_iff, mem_preimage]
Proof state after:
case h
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
s : Set ℂ
o : IsOpen s
z : 𝕊
⊢ (∃ x ∈ s, ↑x = z) ↔ z ≠ ∞ ∧ z.toComplex ∈ s
Theorem: RiemannSphere.isOpenMap_coe
Proof state before:
case h
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
s : Set ℂ
o : IsOpen s
z : 𝕊
⊢ (∃ x ∈ s, ↑x = z) ↔ z ≠ ∞ ∧ z.toComplex ∈ s
Tactic:
constructor
Proof state after:
case h.mp
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
s : Set ℂ
o : IsOpen s
z : 𝕊
⊢ (∃ x ∈ s, ↑x = z) → z ≠ ∞ ∧ z.toComplex ∈ s

case h.mpr
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
s : Set ℂ
o : IsOpen s
z : 𝕊
⊢ z ≠ ∞ ∧ z.toComplex ∈ s → ∃ x ∈ s, ↑x = z
Theorem: RiemannSphere.isOpenMap_coe
Proof state before:
case h.mp
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
s : Set ℂ
o : IsOpen s
z : 𝕊
⊢ (∃ x ∈ s, ↑x = z) → z ≠ ∞ ∧ z.toComplex ∈ s

case h.mpr
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
s : Set ℂ
o : IsOpen s
z : 𝕊
⊢ z ≠ ∞ ∧ z.toComplex ∈ s → ∃ x ∈ s, ↑x = z
Tactic:
intro ⟨x, m, e⟩
Proof state after:
case h.mp
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
s : Set ℂ
o : IsOpen s
z : 𝕊
x : ℂ
m : x ∈ s
e : ↑x = z
⊢ z ≠ ∞ ∧ z.toComplex ∈ s

case h.mpr
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
s : Set ℂ
o : IsOpen s
z : 𝕊
⊢ z ≠ ∞ ∧ z.toComplex ∈ s → ∃ x ∈ s, ↑x = z
Theorem: RiemannSphere.isOpenMap_coe
Proof state before:
case h.mp
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
s : Set ℂ
o : IsOpen s
z : 𝕊
x : ℂ
m : x ∈ s
e : ↑x = z
⊢ z ≠ ∞ ∧ z.toComplex ∈ s

case h.mpr
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
s : Set ℂ
o : IsOpen s
z : 𝕊
⊢ z ≠ ∞ ∧ z.toComplex ∈ s → ∃ x ∈ s, ↑x = z
Tactic:
simp only [← e, toComplex_coe, m, and_true_iff]
Proof state after:
case h.mp
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
s : Set ℂ
o : IsOpen s
z : 𝕊
x : ℂ
m : x ∈ s
e : ↑x = z
⊢ ↑x ≠ ∞

case h.mpr
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
s : Set ℂ
o : IsOpen s
z : 𝕊
⊢ z ≠ ∞ ∧ z.toComplex ∈ s → ∃ x ∈ s, ↑x = z
Theorem: RiemannSphere.isOpenMap_coe
Proof state before:
case h.mp
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
s : Set ℂ
o : IsOpen s
z : 𝕊
x : ℂ
m : x ∈ s
e : ↑x = z
⊢ ↑x ≠ ∞

case h.mpr
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
s : Set ℂ
o : IsOpen s
z : 𝕊
⊢ z ≠ ∞ ∧ z.toComplex ∈ s → ∃ x ∈ s, ↑x = z
Tactic:
exact inf_ne_coe.symm
Proof state after:
case h.mpr
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
s : Set ℂ
o : IsOpen s
z : 𝕊
⊢ z ≠ ∞ ∧ z.toComplex ∈ s → ∃ x ∈ s, ↑x = z