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

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]
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

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
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

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 ?_
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

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]
State after:
no goals

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]
State after:
no goals