Theorem: mfderiv_comp' (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
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
H : Type
inst✝⁹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type
inst✝⁸ : TopologicalSpace M
cs : ChartedSpace H M
E' : Type
inst✝⁷ : NormedAddCommGroup E'
inst✝⁶ : NormedSpace 𝕜 E'
H' : Type
inst✝⁵ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type
inst✝⁴ : TopologicalSpace M'
cs' : ChartedSpace H' M'
E'' : Type
inst✝³ : NormedAddCommGroup E''
inst✝² : NormedSpace 𝕜 E''
H'' : Type
inst✝¹ : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type
inst✝ : TopologicalSpace M''
cs'' : ChartedSpace H'' M''
f : M → M'
x : M
g : M' → M''
sm : SmoothManifoldWithCorners I M
sm' : SmoothManifoldWithCorners I' M'
sm'' : SmoothManifoldWithCorners I'' M''
hg : MDifferentiableAt I' I'' g (f x)
hf : MDifferentiableAt I I' f x
⊢ mfderiv I I'' (fun x => g (f x)) x = (mfderiv I' I'' g (f x)).comp (mfderiv I I' f x)
Tactic:
apply mfderiv_comp
State after:
case hg
𝕜✝ : 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
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
H : Type
inst✝⁹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type
inst✝⁸ : TopologicalSpace M
cs : ChartedSpace H M
E' : Type
inst✝⁷ : NormedAddCommGroup E'
inst✝⁶ : NormedSpace 𝕜 E'
H' : Type
inst✝⁵ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type
inst✝⁴ : TopologicalSpace M'
cs' : ChartedSpace H' M'
E'' : Type
inst✝³ : NormedAddCommGroup E''
inst✝² : NormedSpace 𝕜 E''
H'' : Type
inst✝¹ : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type
inst✝ : TopologicalSpace M''
cs'' : ChartedSpace H'' M''
f : M → M'
x : M
g : M' → M''
sm : SmoothManifoldWithCorners I M
sm' : SmoothManifoldWithCorners I' M'
sm'' : SmoothManifoldWithCorners I'' M''
hg : MDifferentiableAt I' I'' g (f x)
hf : MDifferentiableAt I I' f x
⊢ MDifferentiableAt I' I'' g (f x)

case hf
𝕜✝ : 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
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
H : Type
inst✝⁹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type
inst✝⁸ : TopologicalSpace M
cs : ChartedSpace H M
E' : Type
inst✝⁷ : NormedAddCommGroup E'
inst✝⁶ : NormedSpace 𝕜 E'
H' : Type
inst✝⁵ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type
inst✝⁴ : TopologicalSpace M'
cs' : ChartedSpace H' M'
E'' : Type
inst✝³ : NormedAddCommGroup E''
inst✝² : NormedSpace 𝕜 E''
H'' : Type
inst✝¹ : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type
inst✝ : TopologicalSpace M''
cs'' : ChartedSpace H'' M''
f : M → M'
x : M
g : M' → M''
sm : SmoothManifoldWithCorners I M
sm' : SmoothManifoldWithCorners I' M'
sm'' : SmoothManifoldWithCorners I'' M''
hg : MDifferentiableAt I' I'' g (f x)
hf : MDifferentiableAt I I' f x
⊢ MDifferentiableAt I I' (fun x => f x) x

State before:
case hg
𝕜✝ : 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
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
H : Type
inst✝⁹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type
inst✝⁸ : TopologicalSpace M
cs : ChartedSpace H M
E' : Type
inst✝⁷ : NormedAddCommGroup E'
inst✝⁶ : NormedSpace 𝕜 E'
H' : Type
inst✝⁵ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type
inst✝⁴ : TopologicalSpace M'
cs' : ChartedSpace H' M'
E'' : Type
inst✝³ : NormedAddCommGroup E''
inst✝² : NormedSpace 𝕜 E''
H'' : Type
inst✝¹ : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type
inst✝ : TopologicalSpace M''
cs'' : ChartedSpace H'' M''
f : M → M'
x : M
g : M' → M''
sm : SmoothManifoldWithCorners I M
sm' : SmoothManifoldWithCorners I' M'
sm'' : SmoothManifoldWithCorners I'' M''
hg : MDifferentiableAt I' I'' g (f x)
hf : MDifferentiableAt I I' f x
⊢ MDifferentiableAt I' I'' g (f x)

case hf
𝕜✝ : 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
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
H : Type
inst✝⁹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type
inst✝⁸ : TopologicalSpace M
cs : ChartedSpace H M
E' : Type
inst✝⁷ : NormedAddCommGroup E'
inst✝⁶ : NormedSpace 𝕜 E'
H' : Type
inst✝⁵ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type
inst✝⁴ : TopologicalSpace M'
cs' : ChartedSpace H' M'
E'' : Type
inst✝³ : NormedAddCommGroup E''
inst✝² : NormedSpace 𝕜 E''
H'' : Type
inst✝¹ : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type
inst✝ : TopologicalSpace M''
cs'' : ChartedSpace H'' M''
f : M → M'
x : M
g : M' → M''
sm : SmoothManifoldWithCorners I M
sm' : SmoothManifoldWithCorners I' M'
sm'' : SmoothManifoldWithCorners I'' M''
hg : MDifferentiableAt I' I'' g (f x)
hf : MDifferentiableAt I I' f x
⊢ MDifferentiableAt I I' (fun x => f x) x
Tactic:
repeat assumption
State after:
no goals

State before:
case hf
𝕜✝ : 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
𝕜 : Type
inst✝¹² : NontriviallyNormedField 𝕜
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
H : Type
inst✝⁹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type
inst✝⁸ : TopologicalSpace M
cs : ChartedSpace H M
E' : Type
inst✝⁷ : NormedAddCommGroup E'
inst✝⁶ : NormedSpace 𝕜 E'
H' : Type
inst✝⁵ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type
inst✝⁴ : TopologicalSpace M'
cs' : ChartedSpace H' M'
E'' : Type
inst✝³ : NormedAddCommGroup E''
inst✝² : NormedSpace 𝕜 E''
H'' : Type
inst✝¹ : TopologicalSpace H''
I'' : ModelWithCorners 𝕜 E'' H''
M'' : Type
inst✝ : TopologicalSpace M''
cs'' : ChartedSpace H'' M''
f : M → M'
x : M
g : M' → M''
sm : SmoothManifoldWithCorners I M
sm' : SmoothManifoldWithCorners I' M'
sm'' : SmoothManifoldWithCorners I'' M''
hg : MDifferentiableAt I' I'' g (f x)
hf : MDifferentiableAt I I' f x
⊢ MDifferentiableAt I I' (fun x => f x) x
Tactic:
assumption
State after:
no goals