internlm/Lean-Github huggingface dataset:
Theorem: RiemannSphere.holomorphic_inv
Proof state before:
case right.h₁
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
⊢ AnalyticAt ℂ (↑(extChartAt I ∞⁻¹) ∘ (fun z => z⁻¹) ∘ ↑(extChartAt I ∞).symm) (↑(extChartAt I ∞) ∞)
Tactic:
simp only [inv_inf, extChartAt_inf, ← coe_zero, extChartAt_coe, Function.comp,
  PartialEquiv.trans_apply, Equiv.toPartialEquiv_apply, invEquiv_apply, coePartialEquiv_symm_apply,
  toComplex_coe, PartialEquiv.coe_trans_symm, PartialEquiv.symm_symm, coePartialEquiv_apply,
  Equiv.toPartialEquiv_symm_apply, invEquiv_symm, inv_inv]
Proof state after:
case right.h₁
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
⊢ AnalyticAt ℂ (fun x => x) 0
Theorem: RiemannSphere.holomorphic_inv
Proof state before:
case right.h₁
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
⊢ AnalyticAt ℂ (fun x => x) 0
Tactic:
apply analyticAt_id
Proof state after:
no goals
Theorem: RiemannSphere.holomorphic_inv
Proof state before:
case right.h₂
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
z : ℂ
⊢ AnalyticAt ℂ (↑(extChartAt I (↑z)⁻¹) ∘ (fun z => z⁻¹) ∘ ↑(extChartAt I ↑z).symm) (↑(extChartAt I ↑z) ↑z)
Tactic:
simp only [extChartAt_coe, PartialEquiv.symm_symm, Function.comp, coePartialEquiv_apply,
  coePartialEquiv_symm_apply, toComplex_coe]
Proof state after:
case right.h₂
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
z : ℂ
⊢ AnalyticAt ℂ (fun x => ↑(extChartAt I (↑z)⁻¹) (↑x)⁻¹) z
Theorem: RiemannSphere.holomorphic_inv
Proof state before:
case right.h₂
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
z : ℂ
⊢ AnalyticAt ℂ (fun x => ↑(extChartAt I (↑z)⁻¹) (↑x)⁻¹) z
Tactic:
by_cases z0 : z = 0
Proof state after:
case pos
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
z : ℂ
z0 : z = 0
⊢ AnalyticAt ℂ (fun x => ↑(extChartAt I (↑z)⁻¹) (↑x)⁻¹) z

case neg
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
z : ℂ
z0 : ¬z = 0
⊢ AnalyticAt ℂ (fun x => ↑(extChartAt I (↑z)⁻¹) (↑x)⁻¹) z
Theorem: RiemannSphere.holomorphic_inv
Proof state before:
case pos
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
z : ℂ
z0 : z = 0
⊢ AnalyticAt ℂ (fun x => ↑(extChartAt I (↑z)⁻¹) (↑x)⁻¹) z
Tactic:
simp only [z0, coe_zero, extChartAt_inf, PartialEquiv.trans_apply, coePartialEquiv_symm_apply,
  invEquiv_apply, Equiv.toPartialEquiv_apply, inv_zero', inv_inv, toComplex_coe]
Proof state after:
case pos
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
z : ℂ
z0 : z = 0
⊢ AnalyticAt ℂ (fun x => x) 0
Theorem: RiemannSphere.holomorphic_inv
Proof state before:
case pos
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
z : ℂ
z0 : z = 0
⊢ AnalyticAt ℂ (fun x => x) 0
Tactic:
apply analyticAt_id
Proof state after:
no goals
Theorem: RiemannSphere.holomorphic_inv
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
z : ℂ
z0 : ¬z = 0
⊢ AnalyticAt ℂ (fun x => ↑(extChartAt I (↑z)⁻¹) (↑x)⁻¹) z
Tactic:
simp only [inv_coe z0, extChartAt_coe, coePartialEquiv_symm_apply]
Proof state after:
case neg
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
z : ℂ
z0 : ¬z = 0
⊢ AnalyticAt ℂ (fun x => (↑x)⁻¹.toComplex) z
Theorem: RiemannSphere.holomorphic_inv
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
z : ℂ
z0 : ¬z = 0
⊢ AnalyticAt ℂ (fun x => (↑x)⁻¹.toComplex) z
Tactic:
refine ((analyticAt_id _ _).inv z0).congr ?_
Proof state after:
case neg
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
z : ℂ
z0 : ¬z = 0
⊢ (𝓝 z).EventuallyEq (fun x => (id x)⁻¹) fun x => (↑x)⁻¹.toComplex
Theorem: RiemannSphere.holomorphic_inv
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
z : ℂ
z0 : ¬z = 0
⊢ (𝓝 z).EventuallyEq (fun x => (id x)⁻¹) fun x => (↑x)⁻¹.toComplex
Tactic:
refine (continuousAt_id.eventually_ne z0).mp (eventually_of_forall fun w w0 ↦ ?_)
Proof state after:
case neg
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
z : ℂ
z0 : ¬z = 0
w : ℂ
w0 : id w ≠ 0
⊢ (fun x => (id x)⁻¹) w = (fun x => (↑x)⁻¹.toComplex) w
Theorem: RiemannSphere.holomorphic_inv
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
z : ℂ
z0 : ¬z = 0
w : ℂ
w0 : id w ≠ 0
⊢ (fun x => (id x)⁻¹) w = (fun x => (↑x)⁻¹.toComplex) w
Tactic:
rw [id] at w0
Proof state after:
case neg
X : Type
inst✝⁴ : TopologicalSpace X
Y : Type
inst✝³ : TopologicalSpace Y
T : Type
inst✝² : TopologicalSpace T
inst✝¹ : ChartedSpace ℂ T
inst✝ : AnalyticManifold I T
z : ℂ
z0 : ¬z = 0
w : ℂ
w0 : w ≠ 0
⊢ (fun x => (id x)⁻¹) w = (fun x => (↑x)⁻¹.toComplex) w
Theorem: RiemannSphere.holomorphic_inv
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
z : ℂ
z0 : ¬z = 0
w : ℂ
w0 : w ≠ 0
⊢ (fun x => (id x)⁻¹) w = (fun x => (↑x)⁻¹.toComplex) w
Tactic:
simp only [inv_coe w0, toComplex_coe, id]
Proof state after:
no goals
Theorem: RiemannSphere.continuousAt_fill_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
f✝ : ℂ → ℂ
g : X → ℂ → ℂ
y✝ : 𝕊
x : X
z : ℂ
f : ℂ → X
y : X
fc : ContinuousAt f z
⊢ ContinuousAt (fill f y) ↑z
Tactic:
simp only [OnePoint.continuousAt_coe, Function.comp, fill_coe, fc]
Proof state after:
no goals
Theorem: RiemannSphere.continuousAt_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 : ℂ → X
y : X
fi : Tendsto f atInf (𝓝 y)
⊢ ContinuousAt (fill f y) ∞
Tactic:
simp only [OnePoint.continuousAt_infty', lift_inf, Filter.coclosedCompact_eq_cocompact, ←
  atInf_eq_cocompact, Function.comp, fill_coe, fill_inf, fi]
Proof state after:
no goals
Theorem: RiemannSphere.continuous_fill
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 : ℂ → X
y : X
fc : Continuous f
fi : Tendsto f atInf (𝓝 y)
⊢ Continuous (fill f y)
Tactic:
rw [continuous_iff_continuousAt]
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 : ℂ → X
y : X
fc : Continuous f
fi : Tendsto f atInf (𝓝 y)
⊢ ∀ (x : 𝕊), ContinuousAt (fill f y) x
Theorem: RiemannSphere.continuous_fill
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 : ℂ → X
y : X
fc : Continuous f
fi : Tendsto f atInf (𝓝 y)
⊢ ∀ (x : 𝕊), ContinuousAt (fill f y) x
Tactic:
intro z
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 : ℂ → X
y : X
fc : Continuous f
fi : Tendsto f atInf (𝓝 y)
z : 𝕊
⊢ ContinuousAt (fill f y) z
Theorem: RiemannSphere.continuous_fill
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 : ℂ → X
y : X
fc : Continuous f
fi : Tendsto f atInf (𝓝 y)
z : 𝕊
⊢ ContinuousAt (fill f y) z
Tactic:
induction z using OnePoint.rec
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
f✝ : ℂ → ℂ
g : X → ℂ → ℂ
y✝ : 𝕊
x : X
z : ℂ
f : ℂ → X
y : X
fc : Continuous f
fi : Tendsto f atInf (𝓝 y)
⊢ ContinuousAt (fill f y) ∞

case 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 : ℂ → X
y : X
fc : Continuous f
fi : Tendsto f atInf (𝓝 y)
x✝ : ℂ
⊢ ContinuousAt (fill f y) ↑x✝
Theorem: RiemannSphere.continuous_fill
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
f✝ : ℂ → ℂ
g : X → ℂ → ℂ
y✝ : 𝕊
x : X
z : ℂ
f : ℂ → X
y : X
fc : Continuous f
fi : Tendsto f atInf (𝓝 y)
⊢ ContinuousAt (fill f y) ∞
Tactic:
exact continuousAt_fill_inf fi
Proof state after:
no goals
Theorem: RiemannSphere.continuous_fill
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
f✝ : ℂ → ℂ
g : X → ℂ → ℂ
y✝ : 𝕊
x : X
z : ℂ
f : ℂ → X
y : X
fc : Continuous f
fi : Tendsto f atInf (𝓝 y)
x✝ : ℂ
⊢ ContinuousAt (fill f y) ↑x✝
Tactic:
exact continuousAt_fill_coe fc.continuousAt
Proof state after:
no goals
Theorem: RiemannSphere.holomorphicAt_fill_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
f✝ : ℂ → ℂ
g : X → ℂ → ℂ
y✝ : 𝕊
x : X
z : ℂ
f : ℂ → T
y : T
fa : HolomorphicAt I I f z
⊢ HolomorphicAt I I (fill f y) ↑z
Tactic:
have e : (fun x : 𝕊 ↦ f x.toComplex) =ᶠ[𝓝 ↑z] fill f y := by
  simp only [OnePoint.nhds_coe_eq, Filter.EventuallyEq, Filter.eventually_map, toComplex_coe,
    fill_coe, eq_self_iff_true, Filter.eventually_true]
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 : HolomorphicAt I I f z
e : (𝓝 ↑z).EventuallyEq (fun x => f x.toComplex) (fill f y)
⊢ HolomorphicAt I I (fill f y) ↑z
Theorem: RiemannSphere.holomorphicAt_fill_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
f✝ : ℂ → ℂ
g : X → ℂ → ℂ
y✝ : 𝕊
x : X
z : ℂ
f : ℂ → T
y : T
fa : HolomorphicAt I I f z
e : (𝓝 ↑z).EventuallyEq (fun x => f x.toComplex) (fill f y)
⊢ HolomorphicAt I I (fill f y) ↑z
Tactic:
refine HolomorphicAt.congr ?_ 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
f✝ : ℂ → ℂ
g : X → ℂ → ℂ
y✝ : 𝕊
x : X
z : ℂ
f : ℂ → T
y : T
fa : HolomorphicAt I I f z
e : (𝓝 ↑z).EventuallyEq (fun x => f x.toComplex) (fill f y)
⊢ HolomorphicAt I I (fun x => f x.toComplex) ↑z
Theorem: RiemannSphere.holomorphicAt_fill_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
f✝ : ℂ → ℂ
g : X → ℂ → ℂ
y✝ : 𝕊
x : X
z : ℂ
f : ℂ → T
y : T
fa : HolomorphicAt I I f z
e : (𝓝 ↑z).EventuallyEq (fun x => f x.toComplex) (fill f y)
⊢ HolomorphicAt I I (fun x => f x.toComplex) ↑z
Tactic:
refine fa.comp_of_eq holomorphicAt_toComplex ?_
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 : HolomorphicAt I I f z
e : (𝓝 ↑z).EventuallyEq (fun x => f x.toComplex) (fill f y)
⊢ (↑z).toComplex = z
Theorem: RiemannSphere.holomorphicAt_fill_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
f✝ : ℂ → ℂ
g : X → ℂ → ℂ
y✝ : 𝕊
x : X
z : ℂ
f : ℂ → T
y : T
fa : HolomorphicAt I I f z
e : (𝓝 ↑z).EventuallyEq (fun x => f x.toComplex) (fill f y)
⊢ (↑z).toComplex = z
Tactic:
simp only [toComplex_coe]
Proof state after:
no goals
Theorem: RiemannSphere.holomorphicAt_fill_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
f✝ : ℂ → ℂ
g : X → ℂ → ℂ
y✝ : 𝕊
x : X
z : ℂ
f : ℂ → T
y : T
fa : HolomorphicAt I I f z
⊢ (𝓝 ↑z).EventuallyEq (fun x => f x.toComplex) (fill f y)
Tactic:
simp only [OnePoint.nhds_coe_eq, Filter.EventuallyEq, Filter.eventually_map, toComplex_coe,
  fill_coe, eq_self_iff_true, Filter.eventually_true]
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)
⊢ HolomorphicAt I I (fill f y) ∞
Tactic:
rw [holomorphicAt_iff]
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)
⊢ ContinuousAt (fill f y) ∞ ∧
    AnalyticAt ℂ (↑(extChartAt I (fill f y ∞)) ∘ fill f y ∘ ↑(extChartAt I ∞).symm) (↑(extChartAt I ∞) ∞)
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)
⊢ ContinuousAt (fill f y) ∞ ∧
    AnalyticAt ℂ (↑(extChartAt I (fill f y ∞)) ∘ fill f y ∘ ↑(extChartAt I ∞).symm) (↑(extChartAt I ∞) ∞)
Tactic:
use continuousAt_fill_inf fi
Proof state after:
case right
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)
⊢ AnalyticAt ℂ (↑(extChartAt I (fill f y ∞)) ∘ fill f y ∘ ↑(extChartAt I ∞).symm) (↑(extChartAt I ∞) ∞)
Theorem: RiemannSphere.holomorphicAt_fill_inf
Proof state before:
case right
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)
⊢ AnalyticAt ℂ (↑(extChartAt I (fill f y ∞)) ∘ fill f y ∘ ↑(extChartAt I ∞).symm) (↑(extChartAt I ∞) ∞)
Tactic:
simp only [Function.comp, extChartAt, PartialHomeomorph.extend, fill, rec_inf,
  modelWithCornersSelf_partialEquiv, PartialEquiv.trans_refl, chartAt_inf,
  PartialHomeomorph.symm_toPartialEquiv, PartialEquiv.symm_symm, PartialHomeomorph.toFun_eq_coe,
  invCoePartialHomeomorph_apply, PartialHomeomorph.coe_coe_symm, invCoePartialHomeomorph_symm_apply,
  inv_inf, toComplex_zero]
Proof state after:
case right
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)
⊢ AnalyticAt ℂ (fun x => ↑(chartAt ℂ y) (OnePoint.rec y f (↑x)⁻¹)) 0
Theorem: RiemannSphere.holomorphicAt_fill_inf
Proof state before:
case right
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)
e : (fun z => ↑(chartAt ℂ y) (OnePoint.rec y f (↑z)⁻¹)) = fun z => ↑(extChartAt I y) (if z = 0 then y else f z⁻¹)
⊢ AnalyticAt ℂ (fun x => ↑(chartAt ℂ y) (OnePoint.rec y f (↑x)⁻¹)) 0
Tactic:
rw [e]
Proof state after:
case right
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)
e : (fun z => ↑(chartAt ℂ y) (OnePoint.rec y f (↑z)⁻¹)) = fun z => ↑(extChartAt I y) (if z = 0 then y else f z⁻¹)
⊢ AnalyticAt ℂ (fun z => ↑(extChartAt I y) (if z = 0 then y else f z⁻¹)) 0
Theorem: RiemannSphere.holomorphicAt_fill_inf
Proof state before:
case right
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)
e : (fun z => ↑(chartAt ℂ y) (OnePoint.rec y f (↑z)⁻¹)) = fun z => ↑(extChartAt I y) (if z = 0 then y else f z⁻¹)
⊢ AnalyticAt ℂ (fun z => ↑(extChartAt I y) (if z = 0 then y else f z⁻¹)) 0
Tactic:
clear e
Proof state after:
case right
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)
⊢ AnalyticAt ℂ (fun z => ↑(extChartAt I y) (if z = 0 then y else f z⁻¹)) 0
Theorem: RiemannSphere.holomorphicAt_fill_inf
Proof state before:
case right
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)
⊢ AnalyticAt ℂ (fun z => ↑(extChartAt I y) (if z = 0 then y else f z⁻¹)) 0
Tactic:
apply Complex.analyticAt_of_differentiable_on_punctured_nhds_of_continuousAt
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)
⊢ ∀ᶠ (z : ℂ) in 𝓝[≠] 0, DifferentiableAt ℂ (fun z => ↑(extChartAt I y) (if z = 0 then y else f z⁻¹)) z

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
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)
⊢ (fun z => ↑(chartAt ℂ y) (OnePoint.rec y f (↑z)⁻¹)) = fun z => ↑(extChartAt I y) (if z = 0 then y else f z⁻¹)
Tactic:
funext 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
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 : ℂ
⊢ ↑(chartAt ℂ y) (OnePoint.rec y f (↑z)⁻¹) = ↑(extChartAt I y) (if z = 0 then y else f z⁻¹)
Theorem: RiemannSphere.holomorphicAt_fill_inf
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
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 : ℂ
⊢ ↑(chartAt ℂ y) (OnePoint.rec y f (↑z)⁻¹) = ↑(extChartAt I y) (if z = 0 then y else f z⁻¹)
Tactic:
by_cases z0 : z = 0
Proof state after:
case pos
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⁻¹)

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⁻¹)
Theorem: RiemannSphere.holomorphicAt_fill_inf
Proof state before:
case pos
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 [if_pos z0, z0, coe_zero, inv_zero', rec_inf, extChartAt, PartialHomeomorph.extend,
  modelWithCornersSelf_partialEquiv, PartialEquiv.trans_refl, PartialHomeomorph.toFun_eq_coe,
  if_true]
Proof state after:
no goals