Theorem: analyticAt_iff_holomorphicAt (Ray/AnalyticManifold/AnalyticManifold.lean)

State before:
𝕜 : 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
inst✝⁵ : ChartedSpace A E
inst✝⁴ : AnalyticManifold I E
inst✝³ : ChartedSpace B F
inst✝² : AnalyticManifold J F
inst✝¹ : ExtChartEqRefl I
inst✝ : ExtChartEqRefl J
f : E → F
x : E
⊢ AnalyticAt 𝕜 f x ↔ HolomorphicAt I J f x
Tactic:
simp only [holomorphicAt_iff, extChartAt_eq_refl, PartialEquiv.refl_coe, PartialEquiv.refl_symm,
  Function.id_comp, Function.comp_id, id_eq, iff_and_self]
State after:
𝕜 : 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
inst✝⁵ : ChartedSpace A E
inst✝⁴ : AnalyticManifold I E
inst✝³ : ChartedSpace B F
inst✝² : AnalyticManifold J F
inst✝¹ : ExtChartEqRefl I
inst✝ : ExtChartEqRefl J
f : E → F
x : E
⊢ AnalyticAt 𝕜 f x → ContinuousAt f x

State before:
𝕜 : 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
inst✝⁵ : ChartedSpace A E
inst✝⁴ : AnalyticManifold I E
inst✝³ : ChartedSpace B F
inst✝² : AnalyticManifold J F
inst✝¹ : ExtChartEqRefl I
inst✝ : ExtChartEqRefl J
f : E → F
x : E
⊢ AnalyticAt 𝕜 f x → ContinuousAt f x
Tactic:
exact AnalyticAt.continuousAt
State after:
no goals