Theorem: HolomorphicAt.eventually
Proof state before:
case refine_1
𝕜 : Type
inst✝²⁶ : NontriviallyNormedField 𝕜
E A : Type
inst✝²⁵ : NormedAddCommGroup E
inst✝²⁴ : NormedSpace 𝕜 E
inst✝²³ : CompleteSpace E
inst✝²² : TopologicalSpace A
F B : Type
inst✝²¹ : NormedAddCommGroup F
inst✝²⁰ : NormedSpace 𝕜 F
inst✝¹⁹ : CompleteSpace F
inst✝¹⁸ : TopologicalSpace B
G C : Type
inst✝¹⁷ : NormedAddCommGroup G
inst✝¹⁶ : NormedSpace 𝕜 G
inst✝¹⁵ : TopologicalSpace C
H D : Type
inst✝¹⁴ : NormedAddCommGroup H
inst✝¹³ : NormedSpace 𝕜 H
inst✝¹² : TopologicalSpace D
M : Type
I : ModelWithCorners 𝕜 E A
inst✝¹¹ : TopologicalSpace M
N : Type
J : ModelWithCorners 𝕜 F B
inst✝¹⁰ : TopologicalSpace N
O : Type
K : ModelWithCorners 𝕜 G C
inst✝⁹ : TopologicalSpace O
P : Type
L : ModelWithCorners 𝕜 H D
inst✝⁸ : TopologicalSpace P
inst✝⁷ : I.Boundaryless
inst✝⁶ : ChartedSpace A M
cm : AnalyticManifold I M
inst✝⁵ : J.Boundaryless
inst✝⁴ : ChartedSpace B N
cn : AnalyticManifold J N
inst✝³ : K.Boundaryless
inst✝² : ChartedSpace C O
co : AnalyticManifold K O
inst✝¹ : L.Boundaryless
inst✝ : ChartedSpace D P
cp : AnalyticManifold L P
f : M → N
x : M
fa : HolomorphicAt I J f x
y : M
m : y ∈ (_root_.extChartAt I x).source
fm : ∀ᶠ (x_1 : M) in 𝓝 y, f x_1 ∈ (_root_.extChartAt J (f x)).source
h :
  HolomorphicAt 𝓘(𝕜, E) 𝓘(𝕜, F) (↑(_root_.extChartAt J (f x)) ∘ f ∘ ↑(_root_.extChartAt I x).symm)
    (↑(_root_.extChartAt I x) y)
⊢ (↑(_root_.extChartAt J (f x)) ∘ f ∘ ↑(_root_.extChartAt I x).symm) (↑(_root_.extChartAt I x) y) =
    ↑(_root_.extChartAt J (f x)) (f y)

case refine_2
𝕜 : Type
inst✝²⁶ : NontriviallyNormedField 𝕜
E A : Type
inst✝²⁵ : NormedAddCommGroup E
inst✝²⁴ : NormedSpace 𝕜 E
inst✝²³ : CompleteSpace E
inst✝²² : TopologicalSpace A
F B : Type
inst✝²¹ : NormedAddCommGroup F
inst✝²⁰ : NormedSpace 𝕜 F
inst✝¹⁹ : CompleteSpace F
inst✝¹⁸ : TopologicalSpace B
G C : Type
inst✝¹⁷ : NormedAddCommGroup G
inst✝¹⁶ : NormedSpace 𝕜 G
inst✝¹⁵ : TopologicalSpace C
H D : Type
inst✝¹⁴ : NormedAddCommGroup H
inst✝¹³ : NormedSpace 𝕜 H
inst✝¹² : TopologicalSpace D
M : Type
I : ModelWithCorners 𝕜 E A
inst✝¹¹ : TopologicalSpace M
N : Type
J : ModelWithCorners 𝕜 F B
inst✝¹⁰ : TopologicalSpace N
O : Type
K : ModelWithCorners 𝕜 G C
inst✝⁹ : TopologicalSpace O
P : Type
L : ModelWithCorners 𝕜 H D
inst✝⁸ : TopologicalSpace P
inst✝⁷ : I.Boundaryless
inst✝⁶ : ChartedSpace A M
cm : AnalyticManifold I M
inst✝⁵ : J.Boundaryless
inst✝⁴ : ChartedSpace B N
cn : AnalyticManifold J N
inst✝³ : K.Boundaryless
inst✝² : ChartedSpace C O
co : AnalyticManifold K O
inst✝¹ : L.Boundaryless
inst✝ : ChartedSpace D P
cp : AnalyticManifold L P
f : M → N
x : M
fa : HolomorphicAt I J f x
y : M
m : y ∈ (_root_.extChartAt I x).source
fm : ∀ᶠ (x_1 : M) in 𝓝 y, f x_1 ∈ (_root_.extChartAt J (f x)).source
h :
  HolomorphicAt 𝓘(𝕜, E) 𝓘(𝕜, F) (↑(_root_.extChartAt J (f x)) ∘ f ∘ ↑(_root_.extChartAt I x).symm)
    (↑(_root_.extChartAt I x) y)
h' :
  HolomorphicAt I J
    (fun x_1 =>
      ↑(_root_.extChartAt J (f x)).symm
        ((↑(_root_.extChartAt J (f x)) ∘ f ∘ ↑(_root_.extChartAt I x).symm) (↑(_root_.extChartAt I x) x_1)))
    y
⊢ HolomorphicAt I J f y
Tactic:
simp only [Function.comp, PartialEquiv.left_inv _ m]
Proof state after:
case refine_2
𝕜 : Type
inst✝²⁶ : NontriviallyNormedField 𝕜
E A : Type
inst✝²⁵ : NormedAddCommGroup E
inst✝²⁴ : NormedSpace 𝕜 E
inst✝²³ : CompleteSpace E
inst✝²² : TopologicalSpace A
F B : Type
inst✝²¹ : NormedAddCommGroup F
inst✝²⁰ : NormedSpace 𝕜 F
inst✝¹⁹ : CompleteSpace F
inst✝¹⁸ : TopologicalSpace B
G C : Type
inst✝¹⁷ : NormedAddCommGroup G
inst✝¹⁶ : NormedSpace 𝕜 G
inst✝¹⁵ : TopologicalSpace C
H D : Type
inst✝¹⁴ : NormedAddCommGroup H
inst✝¹³ : NormedSpace 𝕜 H
inst✝¹² : TopologicalSpace D
M : Type
I : ModelWithCorners 𝕜 E A
inst✝¹¹ : TopologicalSpace M
N : Type
J : ModelWithCorners 𝕜 F B
inst✝¹⁰ : TopologicalSpace N
O : Type
K : ModelWithCorners 𝕜 G C
inst✝⁹ : TopologicalSpace O
P : Type
L : ModelWithCorners 𝕜 H D
inst✝⁸ : TopologicalSpace P
inst✝⁷ : I.Boundaryless
inst✝⁶ : ChartedSpace A M
cm : AnalyticManifold I M
inst✝⁵ : J.Boundaryless
inst✝⁴ : ChartedSpace B N
cn : AnalyticManifold J N
inst✝³ : K.Boundaryless
inst✝² : ChartedSpace C O
co : AnalyticManifold K O
inst✝¹ : L.Boundaryless
inst✝ : ChartedSpace D P
cp : AnalyticManifold L P
f : M → N
x : M
fa : HolomorphicAt I J f x
y : M
m : y ∈ (_root_.extChartAt I x).source
fm : ∀ᶠ (x_1 : M) in 𝓝 y, f x_1 ∈ (_root_.extChartAt J (f x)).source
h :
  HolomorphicAt 𝓘(𝕜, E) 𝓘(𝕜, F) (↑(_root_.extChartAt J (f x)) ∘ f ∘ ↑(_root_.extChartAt I x).symm)
    (↑(_root_.extChartAt I x) y)
h' :
  HolomorphicAt I J
    (fun x_1 =>
      ↑(_root_.extChartAt J (f x)).symm
        ((↑(_root_.extChartAt J (f x)) ∘ f ∘ ↑(_root_.extChartAt I x).symm) (↑(_root_.extChartAt I x) x_1)))
    y
⊢ HolomorphicAt I J f y