internlm/Lean-Github huggingface dataset:
Theorem: RiemannSphere.holomorphicAt_fill_inf
Proof state before:
case neg
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f✝ : ℂ → ℂ
g : X → ℂ → ℂ
y✝ : 𝕊
x : X
z✝ : ℂ
f : ℂ → T
y : T
fa : ∀ᶠ (z : ℂ) in atInf, HolomorphicAt I I f z
fi : Tendsto f atInf (𝓝 y)
z : ℂ
z0 : ¬z = 0
⊢ ↑(chartAt ℂ y) (OnePoint.rec y f (↑z)⁻¹) = ↑(extChartAt I y) (if z = 0 then y else f z⁻¹)
Tactic:
simp only [inv_coe z0, rec_coe, extChartAt, PartialHomeomorph.extend,
  modelWithCornersSelf_partialEquiv, PartialEquiv.trans_refl, z0, ite_false,
  PartialHomeomorph.toFun_eq_coe]
Proof state after:
no goals
Theorem: RiemannSphere.holomorphicAt_fill_inf
Proof state before:
case right.hd
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f✝ : ℂ → ℂ
g : X → ℂ → ℂ
y✝ : 𝕊
x : X
z : ℂ
f : ℂ → T
y : T
fa : ∀ᶠ (z : ℂ) in atInf, HolomorphicAt I I f z
fi : Tendsto f atInf (𝓝 y)
⊢ ∀ᶠ (z : ℂ) in 𝓝[≠] 0, DifferentiableAt ℂ (fun z => ↑(extChartAt I y) (if z = 0 then y else f z⁻¹)) z
Tactic:
apply (inv_tendsto_atInf.eventually fa).mp
Proof state after:
case right.hd
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f✝ : ℂ → ℂ
g : X → ℂ → ℂ
y✝ : 𝕊
x : X
z : ℂ
f : ℂ → T
y : T
fa : ∀ᶠ (z : ℂ) in atInf, HolomorphicAt I I f z
fi : Tendsto f atInf (𝓝 y)
⊢ ∀ᶠ (x : ℂ) in 𝓝[≠] 0,
    HolomorphicAt I I f x⁻¹ → DifferentiableAt ℂ (fun z => ↑(extChartAt I y) (if z = 0 then y else f z⁻¹)) x
Theorem: RiemannSphere.holomorphicAt_fill_inf
Proof state before:
case right.hd
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f✝ : ℂ → ℂ
g : X → ℂ → ℂ
y✝ : 𝕊
x : X
z : ℂ
f : ℂ → T
y : T
fa : ∀ᶠ (z : ℂ) in atInf, HolomorphicAt I I f z
fi : Tendsto f atInf (𝓝 y)
⊢ ∀ᶠ (x : ℂ) in 𝓝[≠] 0,
    HolomorphicAt I I f x⁻¹ → DifferentiableAt ℂ (fun z => ↑(extChartAt I y) (if z = 0 then y else f z⁻¹)) x
Tactic:
apply (inv_tendsto_atInf.eventually (fi.eventually
  ((isOpen_extChartAt_source I y).eventually_mem (mem_extChartAt_source I y)))).mp
Proof state after:
case right.hd
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f✝ : ℂ → ℂ
g : X → ℂ → ℂ
y✝ : 𝕊
x : X
z : ℂ
f : ℂ → T
y : T
fa : ∀ᶠ (z : ℂ) in atInf, HolomorphicAt I I f z
fi : Tendsto f atInf (𝓝 y)
⊢ ∀ᶠ (x : ℂ) in 𝓝[≠] 0,
    f x⁻¹ ∈ (extChartAt I y).source →
      HolomorphicAt I I f x⁻¹ → DifferentiableAt ℂ (fun z => ↑(extChartAt I y) (if z = 0 then y else f z⁻¹)) x
Theorem: RiemannSphere.holomorphicAt_fill_inf
Proof state before:
case right.hd
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f✝ : ℂ → ℂ
g : X → ℂ → ℂ
y✝ : 𝕊
x : X
z : ℂ
f : ℂ → T
y : T
fa : ∀ᶠ (z : ℂ) in atInf, HolomorphicAt I I f z
fi : Tendsto f atInf (𝓝 y)
⊢ ∀ᶠ (x : ℂ) in 𝓝[≠] 0,
    f x⁻¹ ∈ (extChartAt I y).source →
      HolomorphicAt I I f x⁻¹ → DifferentiableAt ℂ (fun z => ↑(extChartAt I y) (if z = 0 then y else f z⁻¹)) x
Tactic:
apply eventually_nhdsWithin_of_forall
Proof state after:
case right.hd.h
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f✝ : ℂ → ℂ
g : X → ℂ → ℂ
y✝ : 𝕊
x : X
z : ℂ
f : ℂ → T
y : T
fa : ∀ᶠ (z : ℂ) in atInf, HolomorphicAt I I f z
fi : Tendsto f atInf (𝓝 y)
⊢ ∀ x ∈ {0}ᶜ,
    f x⁻¹ ∈ (extChartAt I y).source →
      HolomorphicAt I I f x⁻¹ → DifferentiableAt ℂ (fun z => ↑(extChartAt I y) (if z = 0 then y else f z⁻¹)) x
Theorem: RiemannSphere.holomorphicAt_fill_inf
Proof state before:
case right.hd.h
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f✝ : ℂ → ℂ
g : X → ℂ → ℂ
y✝ : 𝕊
x : X
z : ℂ
f : ℂ → T
y : T
fa : ∀ᶠ (z : ℂ) in atInf, HolomorphicAt I I f z
fi : Tendsto f atInf (𝓝 y)
⊢ ∀ x ∈ {0}ᶜ,
    f x⁻¹ ∈ (extChartAt I y).source →
      HolomorphicAt I I f x⁻¹ → DifferentiableAt ℂ (fun z => ↑(extChartAt I y) (if z = 0 then y else f z⁻¹)) x
Tactic:
intro z z0 m fa
Proof state after:
case right.hd.h
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f✝ : ℂ → ℂ
g : X → ℂ → ℂ
y✝ : 𝕊
x : X
z✝ : ℂ
f : ℂ → T
y : T
fa✝ : ∀ᶠ (z : ℂ) in atInf, HolomorphicAt I I f z
fi : Tendsto f atInf (𝓝 y)
z : ℂ
z0 : z ∈ {0}ᶜ
m : f z⁻¹ ∈ (extChartAt I y).source
fa : HolomorphicAt I I f z⁻¹
⊢ DifferentiableAt ℂ (fun z => ↑(extChartAt I y) (if z = 0 then y else f z⁻¹)) z
Theorem: RiemannSphere.holomorphicAt_fill_inf
Proof state before:
case right.hd.h
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f✝ : ℂ → ℂ
g : X → ℂ → ℂ
y✝ : 𝕊
x : X
z✝ : ℂ
f : ℂ → T
y : T
fa✝ : ∀ᶠ (z : ℂ) in atInf, HolomorphicAt I I f z
fi : Tendsto f atInf (𝓝 y)
z : ℂ
z0 : z ∈ {0}ᶜ
m : f z⁻¹ ∈ (extChartAt I y).source
fa : HolomorphicAt I I f z⁻¹
⊢ DifferentiableAt ℂ (fun z => ↑(extChartAt I y) (if z = 0 then y else f z⁻¹)) z
Tactic:
simp only [Set.mem_compl_iff, Set.mem_singleton_iff] at z0
Proof state after:
case right.hd.h
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f✝ : ℂ → ℂ
g : X → ℂ → ℂ
y✝ : 𝕊
x : X
z✝ : ℂ
f : ℂ → T
y : T
fa✝ : ∀ᶠ (z : ℂ) in atInf, HolomorphicAt I I f z
fi : Tendsto f atInf (𝓝 y)
z : ℂ
m : f z⁻¹ ∈ (extChartAt I y).source
fa : HolomorphicAt I I f z⁻¹
z0 : ¬z = 0
⊢ DifferentiableAt ℂ (fun z => ↑(extChartAt I y) (if z = 0 then y else f z⁻¹)) z
Theorem: RiemannSphere.holomorphicAt_fill_inf
Proof state before:
case right.hd.h
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f✝ : ℂ → ℂ
g : X → ℂ → ℂ
y✝ : 𝕊
x : X
z✝ : ℂ
f : ℂ → T
y : T
fa✝ : ∀ᶠ (z : ℂ) in atInf, HolomorphicAt I I f z
fi : Tendsto f atInf (𝓝 y)
z : ℂ
m : f z⁻¹ ∈ (extChartAt I y).source
fa : HolomorphicAt I I f z⁻¹
z0 : ¬z = 0
⊢ DifferentiableAt ℂ (fun z => ↑(extChartAt I y) (if z = 0 then y else f z⁻¹)) z
Tactic:
have e : (fun z ↦ extChartAt I y (if z = 0 then y else f z⁻¹)) =ᶠ[𝓝 z]
    fun z ↦ extChartAt I y (f z⁻¹) := 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 right.hd.h
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f✝ : ℂ → ℂ
g : X → ℂ → ℂ
y✝ : 𝕊
x : X
z✝ : ℂ
f : ℂ → T
y : T
fa✝ : ∀ᶠ (z : ℂ) in atInf, HolomorphicAt I I f z
fi : Tendsto f atInf (𝓝 y)
z : ℂ
m : f z⁻¹ ∈ (extChartAt I y).source
fa : HolomorphicAt I I f z⁻¹
z0 : ¬z = 0
e : (𝓝 z).EventuallyEq (fun z => ↑(extChartAt I y) (if z = 0 then y else f z⁻¹)) fun z => ↑(extChartAt I y) (f z⁻¹)
⊢ DifferentiableAt ℂ (fun z => ↑(extChartAt I y) (if z = 0 then y else f z⁻¹)) z
Theorem: RiemannSphere.holomorphicAt_fill_inf
Proof state before:
case right.hd.h
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f✝ : ℂ → ℂ
g : X → ℂ → ℂ
y✝ : 𝕊
x : X
z✝ : ℂ
f : ℂ → T
y : T
fa✝ : ∀ᶠ (z : ℂ) in atInf, HolomorphicAt I I f z
fi : Tendsto f atInf (𝓝 y)
z : ℂ
m : f z⁻¹ ∈ (extChartAt I y).source
fa : HolomorphicAt I I f z⁻¹
z0 : ¬z = 0
e : (𝓝 z).EventuallyEq (fun z => ↑(extChartAt I y) (if z = 0 then y else f z⁻¹)) fun z => ↑(extChartAt I y) (f z⁻¹)
⊢ DifferentiableAt ℂ (fun z => ↑(extChartAt I y) (if z = 0 then y else f z⁻¹)) z
Tactic:
refine DifferentiableAt.congr_of_eventuallyEq ?_ e
Proof state after:
case right.hd.h
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f✝ : ℂ → ℂ
g : X → ℂ → ℂ
y✝ : 𝕊
x : X
z✝ : ℂ
f : ℂ → T
y : T
fa✝ : ∀ᶠ (z : ℂ) in atInf, HolomorphicAt I I f z
fi : Tendsto f atInf (𝓝 y)
z : ℂ
m : f z⁻¹ ∈ (extChartAt I y).source
fa : HolomorphicAt I I f z⁻¹
z0 : ¬z = 0
e : (𝓝 z).EventuallyEq (fun z => ↑(extChartAt I y) (if z = 0 then y else f z⁻¹)) fun z => ↑(extChartAt I y) (f z⁻¹)
⊢ DifferentiableAt ℂ (fun z => ↑(extChartAt I y) (f z⁻¹)) z
Theorem: RiemannSphere.holomorphicAt_fill_inf
Proof state before:
case right.hd.h
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f✝ : ℂ → ℂ
g : X → ℂ → ℂ
y✝ : 𝕊
x : X
z✝ : ℂ
f : ℂ → T
y : T
fa✝ : ∀ᶠ (z : ℂ) in atInf, HolomorphicAt I I f z
fi : Tendsto f atInf (𝓝 y)
z : ℂ
m : f z⁻¹ ∈ (extChartAt I y).source
fa : HolomorphicAt I I f z⁻¹
z0 : ¬z = 0
e : (𝓝 z).EventuallyEq (fun z => ↑(extChartAt I y) (if z = 0 then y else f z⁻¹)) fun z => ↑(extChartAt I y) (f z⁻¹)
⊢ DifferentiableAt ℂ (fun z => ↑(extChartAt I y) (f z⁻¹)) z
Tactic:
apply AnalyticAt.differentiableAt
Proof state after:
case right.hd.h.a
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f✝ : ℂ → ℂ
g : X → ℂ → ℂ
y✝ : 𝕊
x : X
z✝ : ℂ
f : ℂ → T
y : T
fa✝ : ∀ᶠ (z : ℂ) in atInf, HolomorphicAt I I f z
fi : Tendsto f atInf (𝓝 y)
z : ℂ
m : f z⁻¹ ∈ (extChartAt I y).source
fa : HolomorphicAt I I f z⁻¹
z0 : ¬z = 0
e : (𝓝 z).EventuallyEq (fun z => ↑(extChartAt I y) (if z = 0 then y else f z⁻¹)) fun z => ↑(extChartAt I y) (f z⁻¹)
⊢ AnalyticAt ℂ (fun z => ↑(extChartAt I y) (f z⁻¹)) z
Theorem: RiemannSphere.holomorphicAt_fill_inf
Proof state before:
case right.hd.h.a
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f✝ : ℂ → ℂ
g : X → ℂ → ℂ
y✝ : 𝕊
x : X
z✝ : ℂ
f : ℂ → T
y : T
fa✝ : ∀ᶠ (z : ℂ) in atInf, HolomorphicAt I I f z
fi : Tendsto f atInf (𝓝 y)
z : ℂ
m : f z⁻¹ ∈ (extChartAt I y).source
fa : HolomorphicAt I I f z⁻¹
z0 : ¬z = 0
e : (𝓝 z).EventuallyEq (fun z => ↑(extChartAt I y) (if z = 0 then y else f z⁻¹)) fun z => ↑(extChartAt I y) (f z⁻¹)
⊢ AnalyticAt ℂ (fun z => ↑(extChartAt I y) (f z⁻¹)) z
Tactic:
apply HolomorphicAt.analyticAt I I
Proof state after:
case right.hd.h.a
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f✝ : ℂ → ℂ
g : X → ℂ → ℂ
y✝ : 𝕊
x : X
z✝ : ℂ
f : ℂ → T
y : T
fa✝ : ∀ᶠ (z : ℂ) in atInf, HolomorphicAt I I f z
fi : Tendsto f atInf (𝓝 y)
z : ℂ
m : f z⁻¹ ∈ (extChartAt I y).source
fa : HolomorphicAt I I f z⁻¹
z0 : ¬z = 0
e : (𝓝 z).EventuallyEq (fun z => ↑(extChartAt I y) (if z = 0 then y else f z⁻¹)) fun z => ↑(extChartAt I y) (f z⁻¹)
⊢ HolomorphicAt I I (fun z => ↑(extChartAt I y) (f z⁻¹)) z
Theorem: RiemannSphere.holomorphicAt_fill_inf
Proof state before:
case right.hd.h.a
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f✝ : ℂ → ℂ
g : X → ℂ → ℂ
y✝ : 𝕊
x : X
z✝ : ℂ
f : ℂ → T
y : T
fa✝ : ∀ᶠ (z : ℂ) in atInf, HolomorphicAt I I f z
fi : Tendsto f atInf (𝓝 y)
z : ℂ
m : f z⁻¹ ∈ (extChartAt I y).source
fa : HolomorphicAt I I f z⁻¹
z0 : ¬z = 0
e : (𝓝 z).EventuallyEq (fun z => ↑(extChartAt I y) (if z = 0 then y else f z⁻¹)) fun z => ↑(extChartAt I y) (f z⁻¹)
⊢ HolomorphicAt I I (fun z => ↑(extChartAt I y) (f z⁻¹)) z
Tactic:
refine (HolomorphicAt.extChartAt ?_).comp ?_
Proof state after:
case right.hd.h.a.refine_1
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f✝ : ℂ → ℂ
g : X → ℂ → ℂ
y✝ : 𝕊
x : X
z✝ : ℂ
f : ℂ → T
y : T
fa✝ : ∀ᶠ (z : ℂ) in atInf, HolomorphicAt I I f z
fi : Tendsto f atInf (𝓝 y)
z : ℂ
m : f z⁻¹ ∈ (extChartAt I y).source
fa : HolomorphicAt I I f z⁻¹
z0 : ¬z = 0
e : (𝓝 z).EventuallyEq (fun z => ↑(extChartAt I y) (if z = 0 then y else f z⁻¹)) fun z => ↑(extChartAt I y) (f z⁻¹)
⊢ f z⁻¹ ∈ (extChartAt I y).source

case right.hd.h.a.refine_2
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f✝ : ℂ → ℂ
g : X → ℂ → ℂ
y✝ : 𝕊
x : X
z✝ : ℂ
f : ℂ → T
y : T
fa✝ : ∀ᶠ (z : ℂ) in atInf, HolomorphicAt I I f z
fi : Tendsto f atInf (𝓝 y)
z : ℂ
m : f z⁻¹ ∈ (extChartAt I y).source
fa : HolomorphicAt I I f z⁻¹
z0 : ¬z = 0
e : (𝓝 z).EventuallyEq (fun z => ↑(extChartAt I y) (if z = 0 then y else f z⁻¹)) fun z => ↑(extChartAt I y) (f z⁻¹)
⊢ HolomorphicAt I I (fun z => f z⁻¹) z
Theorem: RiemannSphere.holomorphicAt_fill_inf
Proof state before:
case right.hd.h.a.refine_1
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f✝ : ℂ → ℂ
g : X → ℂ → ℂ
y✝ : 𝕊
x : X
z✝ : ℂ
f : ℂ → T
y : T
fa✝ : ∀ᶠ (z : ℂ) in atInf, HolomorphicAt I I f z
fi : Tendsto f atInf (𝓝 y)
z : ℂ
m : f z⁻¹ ∈ (extChartAt I y).source
fa : HolomorphicAt I I f z⁻¹
z0 : ¬z = 0
e : (𝓝 z).EventuallyEq (fun z => ↑(extChartAt I y) (if z = 0 then y else f z⁻¹)) fun z => ↑(extChartAt I y) (f z⁻¹)
⊢ f z⁻¹ ∈ (extChartAt I y).source

case right.hd.h.a.refine_2
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f✝ : ℂ → ℂ
g : X → ℂ → ℂ
y✝ : 𝕊
x : X
z✝ : ℂ
f : ℂ → T
y : T
fa✝ : ∀ᶠ (z : ℂ) in atInf, HolomorphicAt I I f z
fi : Tendsto f atInf (𝓝 y)
z : ℂ
m : f z⁻¹ ∈ (extChartAt I y).source
fa : HolomorphicAt I I f z⁻¹
z0 : ¬z = 0
e : (𝓝 z).EventuallyEq (fun z => ↑(extChartAt I y) (if z = 0 then y else f z⁻¹)) fun z => ↑(extChartAt I y) (f z⁻¹)
⊢ HolomorphicAt I I (fun z => f z⁻¹) z
Tactic:
exact m
Proof state after:
case right.hd.h.a.refine_2
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f✝ : ℂ → ℂ
g : X → ℂ → ℂ
y✝ : 𝕊
x : X
z✝ : ℂ
f : ℂ → T
y : T
fa✝ : ∀ᶠ (z : ℂ) in atInf, HolomorphicAt I I f z
fi : Tendsto f atInf (𝓝 y)
z : ℂ
m : f z⁻¹ ∈ (extChartAt I y).source
fa : HolomorphicAt I I f z⁻¹
z0 : ¬z = 0
e : (𝓝 z).EventuallyEq (fun z => ↑(extChartAt I y) (if z = 0 then y else f z⁻¹)) fun z => ↑(extChartAt I y) (f z⁻¹)
⊢ HolomorphicAt I I (fun z => f z⁻¹) z
Theorem: RiemannSphere.holomorphicAt_fill_inf
Proof state before:
case right.hd.h.a.refine_2
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f✝ : ℂ → ℂ
g : X → ℂ → ℂ
y✝ : 𝕊
x : X
z✝ : ℂ
f : ℂ → T
y : T
fa✝ : ∀ᶠ (z : ℂ) in atInf, HolomorphicAt I I f z
fi : Tendsto f atInf (𝓝 y)
z : ℂ
m : f z⁻¹ ∈ (extChartAt I y).source
fa : HolomorphicAt I I f z⁻¹
z0 : ¬z = 0
e : (𝓝 z).EventuallyEq (fun z => ↑(extChartAt I y) (if z = 0 then y else f z⁻¹)) fun z => ↑(extChartAt I y) (f z⁻¹)
⊢ HolomorphicAt I I (fun z => f z⁻¹) z
Tactic:
exact fa.comp (holomorphicAt_id.inv z0)
Proof state after:
no goals
Theorem: RiemannSphere.holomorphicAt_fill_inf
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
f✝ : ℂ → ℂ
g : X → ℂ → ℂ
y✝ : 𝕊
x : X
z✝ : ℂ
f : ℂ → T
y : T
fa✝ : ∀ᶠ (z : ℂ) in atInf, HolomorphicAt I I f z
fi : Tendsto f atInf (𝓝 y)
z : ℂ
m : f z⁻¹ ∈ (extChartAt I y).source
fa : HolomorphicAt I I f z⁻¹
z0 : ¬z = 0
⊢ (𝓝 z).EventuallyEq (fun z => ↑(extChartAt I y) (if z = 0 then y else f z⁻¹)) fun z => ↑(extChartAt I y) (f z⁻¹)
Tactic:
refine (continuousAt_id.eventually_ne z0).mp (eventually_of_forall fun w w0 ↦ ?_)
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
f✝ : ℂ → ℂ
g : X → ℂ → ℂ
y✝ : 𝕊
x : X
z✝ : ℂ
f : ℂ → T
y : T
fa✝ : ∀ᶠ (z : ℂ) in atInf, HolomorphicAt I I f z
fi : Tendsto f atInf (𝓝 y)
z : ℂ
m : f z⁻¹ ∈ (extChartAt I y).source
fa : HolomorphicAt I I f z⁻¹
z0 : ¬z = 0
w : ℂ
w0 : id w ≠ 0
⊢ (fun z => ↑(extChartAt I y) (if z = 0 then y else f z⁻¹)) w = (fun z => ↑(extChartAt I y) (f z⁻¹)) w
Theorem: RiemannSphere.holomorphicAt_fill_inf
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
f✝ : ℂ → ℂ
g : X → ℂ → ℂ
y✝ : 𝕊
x : X
z✝ : ℂ
f : ℂ → T
y : T
fa✝ : ∀ᶠ (z : ℂ) in atInf, HolomorphicAt I I f z
fi : Tendsto f atInf (𝓝 y)
z : ℂ
m : f z⁻¹ ∈ (extChartAt I y).source
fa : HolomorphicAt I I f z⁻¹
z0 : ¬z = 0
w : ℂ
w0 : id w ≠ 0
⊢ (fun z => ↑(extChartAt I y) (if z = 0 then y else f z⁻¹)) w = (fun z => ↑(extChartAt I y) (f z⁻¹)) w
Tactic:
simp only [Ne, id_eq] at w0
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
f✝ : ℂ → ℂ
g : X → ℂ → ℂ
y✝ : 𝕊
x : X
z✝ : ℂ
f : ℂ → T
y : T
fa✝ : ∀ᶠ (z : ℂ) in atInf, HolomorphicAt I I f z
fi : Tendsto f atInf (𝓝 y)
z : ℂ
m : f z⁻¹ ∈ (extChartAt I y).source
fa : HolomorphicAt I I f z⁻¹
z0 : ¬z = 0
w : ℂ
w0 : ¬w = 0
⊢ (fun z => ↑(extChartAt I y) (if z = 0 then y else f z⁻¹)) w = (fun z => ↑(extChartAt I y) (f z⁻¹)) w
Theorem: RiemannSphere.holomorphicAt_fill_inf
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
f✝ : ℂ → ℂ
g : X → ℂ → ℂ
y✝ : 𝕊
x : X
z✝ : ℂ
f : ℂ → T
y : T
fa✝ : ∀ᶠ (z : ℂ) in atInf, HolomorphicAt I I f z
fi : Tendsto f atInf (𝓝 y)
z : ℂ
m : f z⁻¹ ∈ (extChartAt I y).source
fa : HolomorphicAt I I f z⁻¹
z0 : ¬z = 0
w : ℂ
w0 : ¬w = 0
⊢ (fun z => ↑(extChartAt I y) (if z = 0 then y else f z⁻¹)) w = (fun z => ↑(extChartAt I y) (f z⁻¹)) w
Tactic:
simp only [w0, if_false]
Proof state after:
no goals
Theorem: RiemannSphere.holomorphicAt_fill_inf
Proof state before:
case right.hc
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f✝ : ℂ → ℂ
g : X → ℂ → ℂ
y✝ : 𝕊
x : X
z : ℂ
f : ℂ → T
y : T
fa : ∀ᶠ (z : ℂ) in atInf, HolomorphicAt I I f z
fi : Tendsto f atInf (𝓝 y)
⊢ ContinuousAt (fun z => ↑(extChartAt I y) (if z = 0 then y else f z⁻¹)) 0
Tactic:
refine (continuousAt_extChartAt' I ?_).comp ?_
Proof state after:
case right.hc.refine_1
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f✝ : ℂ → ℂ
g : X → ℂ → ℂ
y✝ : 𝕊
x : X
z : ℂ
f : ℂ → T
y : T
fa : ∀ᶠ (z : ℂ) in atInf, HolomorphicAt I I f z
fi : Tendsto f atInf (𝓝 y)
⊢ (if 0 = 0 then y else f 0⁻¹) ∈ (extChartAt I y).source

case right.hc.refine_2
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f✝ : ℂ → ℂ
g : X → ℂ → ℂ
y✝ : 𝕊
x : X
z : ℂ
f : ℂ → T
y : T
fa : ∀ᶠ (z : ℂ) in atInf, HolomorphicAt I I f z
fi : Tendsto f atInf (𝓝 y)
⊢ ContinuousAt (fun z => if z = 0 then y else f z⁻¹) 0
Theorem: RiemannSphere.holomorphicAt_fill_inf
Proof state before:
case right.hc.refine_1
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f✝ : ℂ → ℂ
g : X → ℂ → ℂ
y✝ : 𝕊
x : X
z : ℂ
f : ℂ → T
y : T
fa : ∀ᶠ (z : ℂ) in atInf, HolomorphicAt I I f z
fi : Tendsto f atInf (𝓝 y)
⊢ (if 0 = 0 then y else f 0⁻¹) ∈ (extChartAt I y).source
Tactic:
simp only [eq_self_iff_true, if_pos, mem_extChartAt_source]
Proof state after:
no goals
Theorem: RiemannSphere.holomorphicAt_fill_inf
Proof state before:
case right.hc.refine_2
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f✝ : ℂ → ℂ
g : X → ℂ → ℂ
y✝ : 𝕊
x : X
z : ℂ
f : ℂ → T
y : T
fa : ∀ᶠ (z : ℂ) in atInf, HolomorphicAt I I f z
fi : Tendsto f atInf (𝓝 y)
⊢ ContinuousAt (fun z => if z = 0 then y else f z⁻¹) 0
Tactic:
simp only [← continuousWithinAt_compl_self, ContinuousWithinAt]
Proof state after:
case right.hc.refine_2
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f✝ : ℂ → ℂ
g : X → ℂ → ℂ
y✝ : 𝕊
x : X
z : ℂ
f : ℂ → T
y : T
fa : ∀ᶠ (z : ℂ) in atInf, HolomorphicAt I I f z
fi : Tendsto f atInf (𝓝 y)
⊢ Tendsto (fun z => if z = 0 then y else f z⁻¹) (𝓝[≠] 0) (𝓝 (if True then y else f 0⁻¹))
Theorem: RiemannSphere.holomorphicAt_fill_inf
Proof state before:
case right.hc.refine_2
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f✝ : ℂ → ℂ
g : X → ℂ → ℂ
y✝ : 𝕊
x : X
z : ℂ
f : ℂ → T
y : T
fa : ∀ᶠ (z : ℂ) in atInf, HolomorphicAt I I f z
fi : Tendsto f atInf (𝓝 y)
⊢ Tendsto (fun z => if z = 0 then y else f z⁻¹) (𝓝[≠] 0) (𝓝 (if True then y else f 0⁻¹))
Tactic:
apply tendsto_nhdsWithin_congr (f := fun z ↦ f z⁻¹)
Proof state after:
case right.hc.refine_2.hfg
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f✝ : ℂ → ℂ
g : X → ℂ → ℂ
y✝ : 𝕊
x : X
z : ℂ
f : ℂ → T
y : T
fa : ∀ᶠ (z : ℂ) in atInf, HolomorphicAt I I f z
fi : Tendsto f atInf (𝓝 y)
⊢ ∀ x ∈ {0}ᶜ, f x⁻¹ = if x = 0 then y else f x⁻¹

case right.hc.refine_2.hf
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
f✝ : ℂ → ℂ
g : X → ℂ → ℂ
y✝ : 𝕊
x : X
z : ℂ
f : ℂ → T
y : T
fa : ∀ᶠ (z : ℂ) in atInf, HolomorphicAt I I f z
fi : Tendsto f atInf (𝓝 y)
⊢ Tendsto (fun z => f z⁻¹) (𝓝[≠] 0) (𝓝 (if True then y else f 0⁻¹))