Theorem: HolomorphicOn.eq_of_locally_eq
Proof state before:
X : Type
inst✝²³ : TopologicalSpace X
S : Type
inst✝²² : TopologicalSpace S
inst✝²¹ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝²⁰ : TopologicalSpace T
inst✝¹⁹ : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹⁸ : TopologicalSpace U
inst✝¹⁷ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f✝ : ℂ → ℂ
s✝ : Set ℂ
E : Type
inst✝¹⁶ : NormedAddCommGroup E
inst✝¹⁵ : NormedSpace ℂ E
inst✝¹⁴ : CompleteSpace E
F : Type
inst✝¹³ : NormedAddCommGroup F
inst✝¹² : NormedSpace ℂ F
inst✝¹¹ : CompleteSpace F
A : Type
inst✝¹⁰ : TopologicalSpace A
J : ModelWithCorners ℂ E A
inst✝⁹ : J.Boundaryless
B : Type
inst✝⁸ : TopologicalSpace B
K : ModelWithCorners ℂ F B
inst✝⁷ : K.Boundaryless
M : Type
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace A M
inst✝⁴ : AnalyticManifold J M
N : Type
inst✝³ : TopologicalSpace N
inst✝² : ChartedSpace B N
inst✝¹ : AnalyticManifold K N
f g : M → N
inst✝ : T2Space N
s : Set M
fa : HolomorphicOn J K f s
ga : HolomorphicOn J K g s
sp : IsPreconnected s
e✝ : ∃ x ∈ s, (𝓝 x).EventuallyEq f g
t : Set M
ht : {x | (𝓝 x).EventuallyEq f g} = t
x : M
xs : x ∈ s
xt : ∃ᶠ (x : M) in 𝓝 x, x ∈ t
ex' : ∃ᶠ (y : M) in 𝓝 x, f y = g y
ex : f x = g x
d : E → F
hd :
  (fun y =>
      ↑(extChartAt K (f x)) (f (↑(extChartAt J x).symm y)) - ↑(extChartAt K (g x)) (g (↑(extChartAt J x).symm y))) =
    d
z : E
hz : ↑(extChartAt J x) x = z
xt' : ∃ᶠ (y : M) in 𝓝 x, ↑(extChartAt J x).symm (↑(extChartAt J x) y) ∈ t
y : E
m : y ∈ (extChartAt J x).target
e : ↑(extChartAt J x).symm y ∈ {x | (𝓝 x).EventuallyEq f g}
⊢ ∀ᶠ (x_1 : E) in 𝓝 y, f (↑(extChartAt J x).symm x_1) = g (↑(extChartAt J x).symm x_1) → d x_1 = 0 x_1
Tactic:
refine eventually_of_forall fun z e ↦ ?_
Proof state after:
X : Type
inst✝²³ : TopologicalSpace X
S : Type
inst✝²² : TopologicalSpace S
inst✝²¹ : ChartedSpace ℂ S
cms : AnalyticManifold 𝓘(ℂ, ℂ) S
T : Type
inst✝²⁰ : TopologicalSpace T
inst✝¹⁹ : ChartedSpace ℂ T
cmt : AnalyticManifold 𝓘(ℂ, ℂ) T
U : Type
inst✝¹⁸ : TopologicalSpace U
inst✝¹⁷ : ChartedSpace ℂ U
cmu : AnalyticManifold 𝓘(ℂ, ℂ) U
f✝ : ℂ → ℂ
s✝ : Set ℂ
E : Type
inst✝¹⁶ : NormedAddCommGroup E
inst✝¹⁵ : NormedSpace ℂ E
inst✝¹⁴ : CompleteSpace E
F : Type
inst✝¹³ : NormedAddCommGroup F
inst✝¹² : NormedSpace ℂ F
inst✝¹¹ : CompleteSpace F
A : Type
inst✝¹⁰ : TopologicalSpace A
J : ModelWithCorners ℂ E A
inst✝⁹ : J.Boundaryless
B : Type
inst✝⁸ : TopologicalSpace B
K : ModelWithCorners ℂ F B
inst✝⁷ : K.Boundaryless
M : Type
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace A M
inst✝⁴ : AnalyticManifold J M
N : Type
inst✝³ : TopologicalSpace N
inst✝² : ChartedSpace B N
inst✝¹ : AnalyticManifold K N
f g : M → N
inst✝ : T2Space N
s : Set M
fa : HolomorphicOn J K f s
ga : HolomorphicOn J K g s
sp : IsPreconnected s
e✝¹ : ∃ x ∈ s, (𝓝 x).EventuallyEq f g
t : Set M
ht : {x | (𝓝 x).EventuallyEq f g} = t
x : M
xs : x ∈ s
xt : ∃ᶠ (x : M) in 𝓝 x, x ∈ t
ex' : ∃ᶠ (y : M) in 𝓝 x, f y = g y
ex : f x = g x
d : E → F
hd :
  (fun y =>
      ↑(extChartAt K (f x)) (f (↑(extChartAt J x).symm y)) - ↑(extChartAt K (g x)) (g (↑(extChartAt J x).symm y))) =
    d
z✝ : E
hz : ↑(extChartAt J x) x = z✝
xt' : ∃ᶠ (y : M) in 𝓝 x, ↑(extChartAt J x).symm (↑(extChartAt J x) y) ∈ t
y : E
m : y ∈ (extChartAt J x).target
e✝ : ↑(extChartAt J x).symm y ∈ {x | (𝓝 x).EventuallyEq f g}
z : E
e : f (↑(extChartAt J x).symm z) = g (↑(extChartAt J x).symm z)
⊢ d z = 0 z