internlm/Lean-Github huggingface dataset:
Theorem: holomorphicAt_snd
Proof state before:
case right
𝕜 : 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✝¹ : I.Boundaryless
inst✝ : J.Boundaryless
x : M × N
⊢ (𝓝 (↑(extChartAt (I.prod J) x) x)).EventuallyEq (fun p => p.2)
    (↑(extChartAt J x.2) ∘ (fun p => p.2) ∘ ↑(extChartAt (I.prod J) x).symm)
Tactic:
filter_upwards [((isOpen_extChartAt_target _ x).eventually_mem (mem_extChartAt_target _ _))]
Proof state after:
case h
𝕜 : 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✝¹ : I.Boundaryless
inst✝ : J.Boundaryless
x : M × N
⊢ ∀ a ∈ (extChartAt (I.prod J) x).target,
    a.2 = (↑(extChartAt J x.2) ∘ (fun p => p.2) ∘ ↑(extChartAt (I.prod J) x).symm) a
Theorem: holomorphicAt_snd
Proof state before:
case h
𝕜 : 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✝¹ : I.Boundaryless
inst✝ : J.Boundaryless
x : M × N
⊢ ∀ a ∈ (extChartAt (I.prod J) x).target,
    a.2 = (↑(extChartAt J x.2) ∘ (fun p => p.2) ∘ ↑(extChartAt (I.prod J) x).symm) a
Tactic:
intro y m
Proof state after:
case h
𝕜 : 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✝¹ : I.Boundaryless
inst✝ : J.Boundaryless
x : M × N
y : E × F
m : y ∈ (extChartAt (I.prod J) x).target
⊢ y.2 = (↑(extChartAt J x.2) ∘ (fun p => p.2) ∘ ↑(extChartAt (I.prod J) x).symm) y
Theorem: holomorphicAt_snd
Proof state before:
case h
𝕜 : 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✝¹ : I.Boundaryless
inst✝ : J.Boundaryless
x : M × N
y : E × F
m : y ∈ (extChartAt (I.prod J) x).target
⊢ y.2 = (↑(extChartAt J x.2) ∘ (fun p => p.2) ∘ ↑(extChartAt (I.prod J) x).symm) y
Tactic:
rw [extChartAt_prod] at m
Proof state after:
case h
𝕜 : 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✝¹ : I.Boundaryless
inst✝ : J.Boundaryless
x : M × N
y : E × F
m : y ∈ ((extChartAt I x.1).prod (extChartAt J x.2)).target
⊢ y.2 = (↑(extChartAt J x.2) ∘ (fun p => p.2) ∘ ↑(extChartAt (I.prod J) x).symm) y
Theorem: holomorphicAt_snd
Proof state before:
case h
𝕜 : 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✝¹ : I.Boundaryless
inst✝ : J.Boundaryless
x : M × N
y : E × F
m : y ∈ ((extChartAt I x.1).prod (extChartAt J x.2)).target
⊢ y.2 = (↑(extChartAt J x.2) ∘ (fun p => p.2) ∘ ↑(extChartAt (I.prod J) x).symm) y
Tactic:
simp only [PartialHomeomorph.prod_toPartialEquiv, PartialEquiv.prod_target, mem_prod] at m
Proof state after:
case h
𝕜 : 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✝¹ : I.Boundaryless
inst✝ : J.Boundaryless
x : M × N
y : E × F
m : y.1 ∈ (extChartAt I x.1).target ∧ y.2 ∈ (extChartAt J x.2).target
⊢ y.2 = (↑(extChartAt J x.2) ∘ (fun p => p.2) ∘ ↑(extChartAt (I.prod J) x).symm) y
Theorem: holomorphicAt_snd
Proof state before:
case h
𝕜 : 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✝¹ : I.Boundaryless
inst✝ : J.Boundaryless
x : M × N
y : E × F
m : y.1 ∈ (extChartAt I x.1).target ∧ y.2 ∈ (extChartAt J x.2).target
⊢ y.2 = (↑(extChartAt J x.2) ∘ (fun p => p.2) ∘ ↑(extChartAt (I.prod J) x).symm) y
Tactic:
simp only [extChartAt_prod, Function.comp, PartialEquiv.prod_coe_symm]
Proof state after:
case h
𝕜 : 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✝¹ : I.Boundaryless
inst✝ : J.Boundaryless
x : M × N
y : E × F
m : y.1 ∈ (extChartAt I x.1).target ∧ y.2 ∈ (extChartAt J x.2).target
⊢ y.2 = ↑(extChartAt J x.2) (↑(extChartAt J x.2).symm y.2)
Theorem: holomorphicAt_snd
Proof state before:
case h
𝕜 : 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✝¹ : I.Boundaryless
inst✝ : J.Boundaryless
x : M × N
y : E × F
m : y.1 ∈ (extChartAt I x.1).target ∧ y.2 ∈ (extChartAt J x.2).target
⊢ y.2 = ↑(extChartAt J x.2) (↑(extChartAt J x.2).symm y.2)
Tactic:
exact ((extChartAt J x.2).right_inv m.2).symm
Proof state after:
no goals
Theorem: HolomorphicAt.extChartAt
Proof 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
x y : M
ys : y ∈ (_root_.extChartAt I x).source
⊢ HolomorphicAt I 𝓘(𝕜, E) (↑(_root_.extChartAt I x)) y
Tactic:
rw [holomorphicAt_iff]
Proof 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
x y : M
ys : y ∈ (_root_.extChartAt I x).source
⊢ ContinuousAt (↑(_root_.extChartAt I x)) y ∧
    AnalyticAt 𝕜
      (↑(_root_.extChartAt 𝓘(𝕜, E) (↑(_root_.extChartAt I x) y)) ∘
        ↑(_root_.extChartAt I x) ∘ ↑(_root_.extChartAt I y).symm)
      (↑(_root_.extChartAt I y) y)
Theorem: HolomorphicAt.extChartAt
Proof 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
x y : M
ys : y ∈ (_root_.extChartAt I x).source
⊢ ContinuousAt (↑(_root_.extChartAt I x)) y ∧
    AnalyticAt 𝕜
      (↑(_root_.extChartAt 𝓘(𝕜, E) (↑(_root_.extChartAt I x) y)) ∘
        ↑(_root_.extChartAt I x) ∘ ↑(_root_.extChartAt I y).symm)
      (↑(_root_.extChartAt I y) y)
Tactic:
use continuousAt_extChartAt' I ys
Proof state after:
case right
𝕜 : 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
x y : M
ys : y ∈ (_root_.extChartAt I x).source
⊢ AnalyticAt 𝕜
    (↑(_root_.extChartAt 𝓘(𝕜, E) (↑(_root_.extChartAt I x) y)) ∘
      ↑(_root_.extChartAt I x) ∘ ↑(_root_.extChartAt I y).symm)
    (↑(_root_.extChartAt I y) y)
Theorem: HolomorphicAt.extChartAt
Proof state before:
case right
𝕜 : 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
x y : M
ys : y ∈ (_root_.extChartAt I x).source
⊢ AnalyticAt 𝕜
    (↑(_root_.extChartAt 𝓘(𝕜, E) (↑(_root_.extChartAt I x) y)) ∘
      ↑(_root_.extChartAt I x) ∘ ↑(_root_.extChartAt I y).symm)
    (↑(_root_.extChartAt I y) y)
Tactic:
simp only [Function.comp, extChartAt, PartialHomeomorph.extend, PartialEquiv.coe_trans,
  PartialHomeomorph.toFun_eq_coe, ModelWithCorners.toPartialEquiv_coe,
  PartialHomeomorph.refl_partialEquiv, PartialEquiv.refl_source,
  PartialHomeomorph.singletonChartedSpace_chartAt_eq, modelWithCornersSelf_partialEquiv,
  PartialEquiv.trans_refl, PartialEquiv.trans_symm_eq_symm_trans_symm,
  ModelWithCorners.toPartialEquiv_coe_symm, PartialHomeomorph.coe_coe_symm,
  PartialEquiv.refl_coe, id, _root_.extChartAt]
Proof state after:
case right
𝕜 : 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
x y : M
ys : y ∈ (_root_.extChartAt I x).source
⊢ AnalyticAt 𝕜 (fun x_1 => ↑I (↑(_root_.chartAt A x) (↑(_root_.chartAt A y).symm (↑I.symm x_1))))
    (↑I (↑(_root_.chartAt A y) y))