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
h : ∀ᶠ (a : M) in 𝓝 x, d (↑(extChartAt J x) a) = OfNat.ofNat 0 (↑(extChartAt J x) a)
⊢ ∀ᶠ (x_1 : M) in 𝓝 x,
    f x_1 ∈ (extChartAt K (f x)).source →
      x_1 ∈ (extChartAt J x).source → d (↑(extChartAt J x) x_1) = OfNat.ofNat 0 (↑(extChartAt J x) x_1) → f x_1 = g x_1
Tactic:
apply ((ga _ xs).continuousAt.eventually_mem ((isOpen_extChartAt_source _ _).mem_nhds
    (mem_extChartAt_source K (g x)))).mp
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
h : ∀ᶠ (a : M) in 𝓝 x, d (↑(extChartAt J x) a) = OfNat.ofNat 0 (↑(extChartAt J x) a)
⊢ ∀ᶠ (x_1 : M) in 𝓝 x,
    g x_1 ∈ (extChartAt K (g x)).source →
      f x_1 ∈ (extChartAt K (f x)).source →
        x_1 ∈ (extChartAt J x).source →
          d (↑(extChartAt J x) x_1) = OfNat.ofNat 0 (↑(extChartAt J x) x_1) → f x_1 = g x_1