Theorem: hasMFDerivAt_iff_hasFDerivAt' (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
I : ModelWithCorners 𝕜 E A
inst✝⁷ : I.Boundaryless
inst✝⁶ : ChartedSpace A E
inst✝⁵ : AnalyticManifold I E
inst✝⁴ : ExtChartEqRefl I
J : ModelWithCorners 𝕜 F B
inst✝³ : J.Boundaryless
inst✝² : ChartedSpace B F
inst✝¹ : AnalyticManifold J F
inst✝ : ExtChartEqRefl J
f : E → F
x : E
f' : E →L[𝕜] F
⊢ HasMFDerivAt I J f x f' ↔ HasFDerivAt f f' x
Tactic:
simp only [HasMFDerivAt, ModelWithCorners.range_eq_univ, hasFDerivWithinAt_univ,
  writtenInExtChartAt, extChartAt_eq_refl, Function.comp, PartialEquiv.refl_coe,
  PartialEquiv.refl_symm, id]
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
I : ModelWithCorners 𝕜 E A
inst✝⁷ : I.Boundaryless
inst✝⁶ : ChartedSpace A E
inst✝⁵ : AnalyticManifold I E
inst✝⁴ : ExtChartEqRefl I
J : ModelWithCorners 𝕜 F B
inst✝³ : J.Boundaryless
inst✝² : ChartedSpace B F
inst✝¹ : AnalyticManifold J F
inst✝ : ExtChartEqRefl J
f : E → F
x : E
f' : E →L[𝕜] F
⊢ ContinuousAt f x ∧ HasFDerivAt (fun x => f x) f' x ↔ HasFDerivAt f 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
I : ModelWithCorners 𝕜 E A
inst✝⁷ : I.Boundaryless
inst✝⁶ : ChartedSpace A E
inst✝⁵ : AnalyticManifold I E
inst✝⁴ : ExtChartEqRefl I
J : ModelWithCorners 𝕜 F B
inst✝³ : J.Boundaryless
inst✝² : ChartedSpace B F
inst✝¹ : AnalyticManifold J F
inst✝ : ExtChartEqRefl J
f : E → F
x : E
f' : E →L[𝕜] F
⊢ ContinuousAt f x ∧ HasFDerivAt (fun x => f x) f' x ↔ HasFDerivAt f f' x
Tactic:
exact ⟨fun x ↦ x.2, fun d ↦ ⟨d.continuousAt, d⟩⟩
State after:
no goals