Theorem: HMul.hMul.arg_a0a1.fderiv_rule_at (SciLean/Core/FunctionTransformations/FDeriv.lean)

State before:
K : Type u_2
inst✝¹¹ : RCLike K
X : Type u_3
inst✝¹⁰ : NormedAddCommGroup X
inst✝⁹ : NormedSpace K X
Y✝ : Type ?u.139024
inst✝⁸ : NormedAddCommGroup Y✝
inst✝⁷ : NormedSpace K Y✝
Z : Type ?u.139159
inst✝⁶ : NormedAddCommGroup Z
inst✝⁵ : NormedSpace K Z
ι : Type ?u.139294
inst✝⁴ : Fintype ι
E : ι → Type ?u.139302
inst✝³ : (i : ι) → NormedAddCommGroup (E i)
inst✝² : (i : ι) → NormedSpace K (E i)
Y : Type u_1
inst✝¹ : NormedCommRing Y
inst✝ : NormedAlgebra K Y
x : X
f g : X → Y
hf : DifferentiableAt K f x
hg : DifferentiableAt K g x
⊢ fderiv K (fun x => f x * g x) x =
    let fx := f x;
    let gx := g x;
    fun dx =>L[K] (fderiv K g x) dx * fx + (fderiv K f x) dx * gx
Tactic:
ext dx
State after:
case h
K : Type u_2
inst✝¹¹ : RCLike K
X : Type u_3
inst✝¹⁰ : NormedAddCommGroup X
inst✝⁹ : NormedSpace K X
Y✝ : Type ?u.139024
inst✝⁸ : NormedAddCommGroup Y✝
inst✝⁷ : NormedSpace K Y✝
Z : Type ?u.139159
inst✝⁶ : NormedAddCommGroup Z
inst✝⁵ : NormedSpace K Z
ι : Type ?u.139294
inst✝⁴ : Fintype ι
E : ι → Type ?u.139302
inst✝³ : (i : ι) → NormedAddCommGroup (E i)
inst✝² : (i : ι) → NormedSpace K (E i)
Y : Type u_1
inst✝¹ : NormedCommRing Y
inst✝ : NormedAlgebra K Y
x : X
f g : X → Y
hf : DifferentiableAt K f x
hg : DifferentiableAt K g x
dx : X
⊢ (fderiv K (fun x => f x * g x) x) dx =
    (let fx := f x;
      let gx := g x;
      fun dx =>L[K] (fderiv K g x) dx * fx + (fderiv K f x) dx * gx)
      dx

State before:
case h
K : Type u_2
inst✝¹¹ : RCLike K
X : Type u_3
inst✝¹⁰ : NormedAddCommGroup X
inst✝⁹ : NormedSpace K X
Y✝ : Type ?u.139024
inst✝⁸ : NormedAddCommGroup Y✝
inst✝⁷ : NormedSpace K Y✝
Z : Type ?u.139159
inst✝⁶ : NormedAddCommGroup Z
inst✝⁵ : NormedSpace K Z
ι : Type ?u.139294
inst✝⁴ : Fintype ι
E : ι → Type ?u.139302
inst✝³ : (i : ι) → NormedAddCommGroup (E i)
inst✝² : (i : ι) → NormedSpace K (E i)
Y : Type u_1
inst✝¹ : NormedCommRing Y
inst✝ : NormedAlgebra K Y
x : X
f g : X → Y
hf : DifferentiableAt K f x
hg : DifferentiableAt K g x
dx : X
⊢ (fderiv K (fun x => f x * g x) x) dx =
    (let fx := f x;
      let gx := g x;
      fun dx =>L[K] (fderiv K g x) dx * fx + (fderiv K f x) dx * gx)
      dx
Tactic:
simp[fderiv_mul hf hg, mul_comm]
State after:
no goals