Theorem: HolomorphicOn.eq_of_locally_eq
Proof state before:
case cl
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
⊢ x ∈ t
Tactic:
suffices h : d =ᶠ[𝓝 z] 0 by
  simp only [← hz, ← extChartAt_map_nhds' J x, Filter.eventually_map, Filter.EventuallyEq,
    ← ht] at h ⊢
  refine
    h.mp (((isOpen_extChartAt_source J x).eventually_mem (mem_extChartAt_source J x)).mp ?_)
  apply ((fa _ xs).continuousAt.eventually_mem ((isOpen_extChartAt_source _ _).mem_nhds
      (mem_extChartAt_source K (f x)))).mp
  apply ((ga _ xs).continuousAt.eventually_mem ((isOpen_extChartAt_source _ _).mem_nhds
      (mem_extChartAt_source K (g x)))).mp
  refine eventually_of_forall fun y gm fm m e ↦ ?_
  rw [← hd, Pi.zero_apply, sub_eq_zero, (extChartAt J x).left_inv m, ex] at e
  rw [ex] at fm; exact (extChartAt K (g x)).injOn fm gm e
Proof state after:
case cl
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
⊢ (𝓝 z).EventuallyEq d 0