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
⊢ (𝓝 z).EventuallyEq d 0
Tactic:
have d0 : ∃ᶠ y in 𝓝 z, d =ᶠ[𝓝 y] 0 := by
  rw [← hz]
  have xt' : ∃ᶠ y in 𝓝 x, (extChartAt J x).symm (extChartAt J x y) ∈ t := by
    apply xt.mp
    apply ((isOpen_extChartAt_source J x).eventually_mem (mem_extChartAt_source J x)).mp
    refine eventually_of_forall fun y m e ↦ ?_; rw [(extChartAt J x).left_inv m]; exact e
  apply (Filter.Tendsto.frequently (p := fun y ↦ (extChartAt J x).symm y ∈ t)
      (continuousAt_extChartAt J x) xt').mp
  apply ((isOpen_extChartAt_target J x).eventually_mem (mem_extChartAt_target J x)).mp
  refine eventually_of_forall fun y m e ↦ ?_; simp only [← ht] at e
  apply ((continuousAt_extChartAt_symm'' J m).eventually e).mp
  refine eventually_of_forall fun z e ↦ ?_; simp only at e
  simp only [← hd, Pi.zero_apply, sub_eq_zero, ex, 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
d0 : ∃ᶠ (y : E) in 𝓝 z, (𝓝 y).EventuallyEq d 0
⊢ (𝓝 z).EventuallyEq d 0