Theorem: Prod.mk.arg_fstsnd.fderiv_rule_at (SciLean/Core/FunctionTransformations/FDeriv.lean)

State before:
K : Type u_3
inst✝⁹ : RCLike K
X : Type u_2
inst✝⁸ : NormedAddCommGroup X
inst✝⁷ : NormedSpace K X
Y : Type u_1
inst✝⁶ : NormedAddCommGroup Y
inst✝⁵ : NormedSpace K Y
Z : Type u_4
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace K Z
ι : Type ?u.97516
inst✝² : Fintype ι
E : ι → Type ?u.97524
inst✝¹ : (i : ι) → NormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace K (E i)
x : X
g : X → Y
hg : DifferentiableAt K g x
f : X → Z
hf : DifferentiableAt K f x
⊢ fderiv K (fun x => (g x, f x)) x = fun dx =>L[K] ((fderiv K g x) dx, (fderiv K f x) dx)
Tactic:
apply DifferentiableAt.fderiv_prod hg hf
State after:
no goals