simp [ContinuousLinearMap.precompL]
𝕜 : Type u_1
S : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝¹⁸ : NontriviallyNormedField 𝕜
inst✝¹⁷ : NormedAddCommGroup E
inst✝¹⁶ : NormedSpace ℝ E
inst✝¹⁵ : NormedSpace 𝕜 E
inst✝¹⁴ : NormedAddCommGroup F
inst✝¹³ : NormedSpace ℝ F
inst✝¹² : NormedSpace 𝕜 F
inst✝¹¹ : NormedAddCommGroup G
inst✝¹⁰ : NormedSpace ℝ G
inst✝⁹ : NormedSpace 𝕜 G
inst✝⁸ : CompleteSpace G
inst✝⁷ : NontriviallyNormedField S
inst✝⁶ : NormedSpace S G
inst✝⁵ : NormedSpace ℝ S
inst✝⁴ : SMulCommClass ℝ S G
inst✝³ : IsScalarTower ℝ S G
inst✝² : NormedSpace 𝕜 S
inst✝¹ : SMulCommClass 𝕜 S G
inst✝ : IsScalarTower 𝕜 S G
u : 𝕜 → E
u' : E
v : 𝕜 → F
v' : F
B : E →L[𝕜] F →L[𝕜] G
x : 𝕜
hu : HasFDerivAt u (ContinuousLinearMap.smulRight 1 u') x
hv : HasFDerivAt v (ContinuousLinearMap.smulRight 1 v') x
dx : 𝕜
⊢ (((ContinuousLinearMap.precompR 𝕜 B) (u x)) (ContinuousLinearMap.smulRight 1 v') +
        ((ContinuousLinearMap.precompL 𝕜 B) (ContinuousLinearMap.smulRight 1 u')) (v x))
      dx =
    (ContinuousLinearMap.smulRight 1 ((B u') (v x) + (B (u x)) v')) dx
𝕜 : Type u_1
S : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝¹⁸ : NontriviallyNormedField 𝕜
inst✝¹⁷ : NormedAddCommGroup E
inst✝¹⁶ : NormedSpace ℝ E
inst✝¹⁵ : NormedSpace 𝕜 E
inst✝¹⁴ : NormedAddCommGroup F
inst✝¹³ : NormedSpace ℝ F
inst✝¹² : NormedSpace 𝕜 F
inst✝¹¹ : NormedAddCommGroup G
inst✝¹⁰ : NormedSpace ℝ G
inst✝⁹ : NormedSpace 𝕜 G
inst✝⁸ : CompleteSpace G
inst✝⁷ : NontriviallyNormedField S
inst✝⁶ : NormedSpace S G
inst✝⁵ : NormedSpace ℝ S
inst✝⁴ : SMulCommClass ℝ S G
inst✝³ : IsScalarTower ℝ S G
inst✝² : NormedSpace 𝕜 S
inst✝¹ : SMulCommClass 𝕜 S G
inst✝ : IsScalarTower 𝕜 S G
u : 𝕜 → E
u' : E
v : 𝕜 → F
v' : F
B : E →L[𝕜] F →L[𝕜] G
x : 𝕜
hu : HasFDerivAt u (ContinuousLinearMap.smulRight 1 u') x
hv : HasFDerivAt v (ContinuousLinearMap.smulRight 1 v') x
dx : 𝕜
⊢ dx • (B (u x)) v' + dx • (B u') (v x) = dx • (B u') (v x) + dx • (B (u x)) v'