Theorem: hasFDerivAt_continuousMultilinearMap_apply_const (ForML/MultilinearDeriv.lean)

State before:
𝕜 : Type u_1
α : Type u_2
ι : Type u_3
inst✝¹² : DecidableEq ι
inst✝¹¹ : Fintype ι
D : ι → Type u_4
n : ℕ
E : Fin n → Type u_5
F : Type u_6
G : Type u_7
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NormedAddCommGroup α
inst✝⁸ : NormedSpace 𝕜 α
inst✝⁷ : (i : ι) → NormedAddCommGroup (D i)
inst✝⁶ : (i : ι) → NormedSpace 𝕜 (D i)
inst✝⁵ : (i : Fin n) → NormedAddCommGroup (E i)
inst✝⁴ : (i : Fin n) → NormedSpace 𝕜 (E i)
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
c : α → ContinuousMultilinearMap 𝕜 E G
v : (i : Fin n) → E i
x : α
c' : α →L[𝕜] ContinuousMultilinearMap 𝕜 E G
hc : HasFDerivAt c c' x
⊢ HasFDerivAt (fun y => (c y) v) ((ContinuousLinearMap.flipMultilinear c') v) x
Tactic:
change HasFDerivAt (ContinuousMultilinearMap.apply 𝕜 E G v ∘ c) _ _
State after:
𝕜 : Type u_1
α : Type u_2
ι : Type u_3
inst✝¹² : DecidableEq ι
inst✝¹¹ : Fintype ι
D : ι → Type u_4
n : ℕ
E : Fin n → Type u_5
F : Type u_6
G : Type u_7
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NormedAddCommGroup α
inst✝⁸ : NormedSpace 𝕜 α
inst✝⁷ : (i : ι) → NormedAddCommGroup (D i)
inst✝⁶ : (i : ι) → NormedSpace 𝕜 (D i)
inst✝⁵ : (i : Fin n) → NormedAddCommGroup (E i)
inst✝⁴ : (i : Fin n) → NormedSpace 𝕜 (E i)
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
c : α → ContinuousMultilinearMap 𝕜 E G
v : (i : Fin n) → E i
x : α
c' : α →L[𝕜] ContinuousMultilinearMap 𝕜 E G
hc : HasFDerivAt c c' x
⊢ HasFDerivAt (⇑(ContinuousMultilinearMap.apply 𝕜 E G v) ∘ c) ((ContinuousLinearMap.flipMultilinear c') v) x

State before:
𝕜 : Type u_1
α : Type u_2
ι : Type u_3
inst✝¹² : DecidableEq ι
inst✝¹¹ : Fintype ι
D : ι → Type u_4
n : ℕ
E : Fin n → Type u_5
F : Type u_6
G : Type u_7
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NormedAddCommGroup α
inst✝⁸ : NormedSpace 𝕜 α
inst✝⁷ : (i : ι) → NormedAddCommGroup (D i)
inst✝⁶ : (i : ι) → NormedSpace 𝕜 (D i)
inst✝⁵ : (i : Fin n) → NormedAddCommGroup (E i)
inst✝⁴ : (i : Fin n) → NormedSpace 𝕜 (E i)
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
c : α → ContinuousMultilinearMap 𝕜 E G
v : (i : Fin n) → E i
x : α
c' : α →L[𝕜] ContinuousMultilinearMap 𝕜 E G
hc : HasFDerivAt c c' x
⊢ HasFDerivAt (⇑(ContinuousMultilinearMap.apply 𝕜 E G v) ∘ c) ((ContinuousLinearMap.flipMultilinear c') v) x
Tactic:
exact (HasFDerivAt.comp x (ContinuousLinearMap.hasFDerivAt _) hc)
State after:
no goals