-- Mathlib/Analysis/Calculus/FDeriv/Mul.lean
theorem HasStrictFDerivAt.clm_comp (hc : HasStrictFDerivAt c c' x) (hd : HasStrictFDerivAt d d' x) :
    HasStrictFDerivAt (fun y => (c y).comp (d y))
      ((compL 𝕜 F G H (c x)).comp d' + ((compL 𝕜 F G H).flip (d x)).comp c') x

Proof state:
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
x : E
H : Type u_5
inst✝¹ : NormedAddCommGroup H
inst✝ : NormedSpace 𝕜 H
c : E → G →L[𝕜] H
c' : E →L[𝕜] G →L[𝕜] H
d : E → F →L[𝕜] G
d' : E →L[𝕜] F →L[𝕜] G
hc : HasStrictFDerivAt c c' x
hd : HasStrictFDerivAt d d' x
this✝ : HasStrictFDerivAt (fun p => p.1.comp p.2) (⋯.deriv (c x, d x)) (c x, d x)
this : HasStrictFDerivAt (fun x => (c x, d x).1.comp (c x, d x).2) ((⋯.deriv (c x, d x)).comp (c'.prod d')) x
⊢ HasStrictFDerivAt (fun y => (c y).comp (d y)) (((compL 𝕜 F G H) (c x)).comp d' + ((compL 𝕜 F G H).flip (d x)).comp c')
    x

Tactic:
exact this

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
x : E
H : Type u_5
inst✝¹ : NormedAddCommGroup H
inst✝ : NormedSpace 𝕜 H
c : E → G →L[𝕜] H
c' : E →L[𝕜] G →L[𝕜] H
d : E → F →L[𝕜] G
d' : E →L[𝕜] F →L[𝕜] G
hc : HasStrictFDerivAt c c' x
hd : HasStrictFDerivAt d d' x
this : HasStrictFDerivAt (fun p => p.1.comp p.2) (⋯.deriv (c x, d x)) (c x, d x)
⊢ HasStrictFDerivAt (fun y => (c y).comp (d y)) (((compL 𝕜 F G H) (c x)).comp d' + ((compL 𝕜 F G H).flip (d x)).comp c')
    x

Tactic:
have := this.comp x (hc.prod hd)

Result:
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
x : E
H : Type u_5
inst✝¹ : NormedAddCommGroup H
inst✝ : NormedSpace 𝕜 H
c : E → G →L[𝕜] H
c' : E →L[𝕜] G →L[𝕜] H
d : E → F →L[𝕜] G
d' : E →L[𝕜] F →L[𝕜] G
hc : HasStrictFDerivAt c c' x
hd : HasStrictFDerivAt d d' x
this✝ : HasStrictFDerivAt (fun p => p.1.comp p.2) (⋯.deriv (c x, d x)) (c x, d x)
this : HasStrictFDerivAt (fun x => (c x, d x).1.comp (c x, d x).2) ((⋯.deriv (c x, d x)).comp (c'.prod d')) x
⊢ HasStrictFDerivAt (fun y => (c y).comp (d y)) (((compL 𝕜 F G H) (c x)).comp d' + ((compL 𝕜 F G H).flip (d x)).comp c')
    x

Proof state:
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
x : E
H : Type u_5
inst✝¹ : NormedAddCommGroup H
inst✝ : NormedSpace 𝕜 H
c : E → G →L[𝕜] H
c' : E →L[𝕜] G →L[𝕜] H
d : E → F →L[𝕜] G
d' : E →L[𝕜] F →L[𝕜] G
hc : HasStrictFDerivAt c c' x
hd : HasStrictFDerivAt d d' x
⊢ HasStrictFDerivAt (fun y => (c y).comp (d y)) (((compL 𝕜 F G H) (c x)).comp d' + ((compL 𝕜 F G H).flip (d x)).comp c')
    x

Tactic:
have := isBoundedBilinearMap_comp.hasStrictFDerivAt (c x, d x)

Result:
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
x : E
H : Type u_5
inst✝¹ : NormedAddCommGroup H
inst✝ : NormedSpace 𝕜 H
c : E → G →L[𝕜] H
c' : E →L[𝕜] G →L[𝕜] H
d : E → F →L[𝕜] G
d' : E →L[𝕜] F →L[𝕜] G
hc : HasStrictFDerivAt c c' x
hd : HasStrictFDerivAt d d' x
this : HasStrictFDerivAt (fun p => p.1.comp p.2) (⋯.deriv (c x, d x)) (c x, d x)
⊢ HasStrictFDerivAt (fun y => (c y).comp (d y)) (((compL 𝕜 F G H) (c x)).comp d' + ((compL 𝕜 F G H).flip (d x)).comp c')
    x