Theorem: SciLean.Inner.inner.arg_a0a1.cderiv_rule (SciLean/Core/FunctionTransformations/CDeriv.lean)

State before:
K✝ : Type ?u.107796
inst✝²⁰ : RCLike K✝
X✝¹ : Type ?u.107802
inst✝¹⁹ : Vec K✝ X✝¹
Y✝¹ : Type ?u.107815
inst✝¹⁸ : Vec K✝ Y✝¹
Z✝ : Type ?u.107826
inst✝¹⁷ : Vec K✝ Z✝
W✝ : Type ?u.107837
inst✝¹⁶ : Vec K✝ W✝
ι✝ : Type ?u.107848
inst✝¹⁵ : IndexType ι✝
inst✝¹⁴ : LawfulIndexType ι✝
inst✝¹³ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.107875
inst✝¹² : (i : ι✝) → Vec K✝ (E✝ i)
K : Type ?u.107891
inst✝¹¹ : RCLike K
X✝ : Type ?u.107897
inst✝¹⁰ : Vec K X✝
Y✝ : Type ?u.107910
inst✝⁹ : Vec K Y✝
Z : Type ?u.107921
inst✝⁸ : Vec K Z
W : Type ?u.107932
inst✝⁷ : Vec K W
ι : Type ?u.107943
inst✝⁶ : IndexType ι
inst✝⁵ : LawfulIndexType ι
inst✝⁴ : DecidableEq ι
E : ι → Type ?u.107970
inst✝³ : (i : ι) → Vec K (E i)
R : Type u_1
inst✝² : RealScalar R
X : Type u_2
inst✝¹ : Vec R X
Y : Type u_3
inst✝ : SemiHilbert R Y
f g : X → Y
hf : CDifferentiable R f
hg : CDifferentiable R g
⊢ (cderiv R fun x => ⟪f x, g x⟫_R) = fun x dx =>
    let y₁ := f x;
    let dy₁ := cderiv R f x dx;
    let y₂ := g x;
    let dy₂ := cderiv R g x dx;
    ⟪dy₁, y₂⟫_R + ⟪y₁, dy₂⟫_R
Tactic:
funext x
State after:
case h
K✝ : Type ?u.107796
inst✝²⁰ : RCLike K✝
X✝¹ : Type ?u.107802
inst✝¹⁹ : Vec K✝ X✝¹
Y✝¹ : Type ?u.107815
inst✝¹⁸ : Vec K✝ Y✝¹
Z✝ : Type ?u.107826
inst✝¹⁷ : Vec K✝ Z✝
W✝ : Type ?u.107837
inst✝¹⁶ : Vec K✝ W✝
ι✝ : Type ?u.107848
inst✝¹⁵ : IndexType ι✝
inst✝¹⁴ : LawfulIndexType ι✝
inst✝¹³ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.107875
inst✝¹² : (i : ι✝) → Vec K✝ (E✝ i)
K : Type ?u.107891
inst✝¹¹ : RCLike K
X✝ : Type ?u.107897
inst✝¹⁰ : Vec K X✝
Y✝ : Type ?u.107910
inst✝⁹ : Vec K Y✝
Z : Type ?u.107921
inst✝⁸ : Vec K Z
W : Type ?u.107932
inst✝⁷ : Vec K W
ι : Type ?u.107943
inst✝⁶ : IndexType ι
inst✝⁵ : LawfulIndexType ι
inst✝⁴ : DecidableEq ι
E : ι → Type ?u.107970
inst✝³ : (i : ι) → Vec K (E i)
R : Type u_1
inst✝² : RealScalar R
X : Type u_2
inst✝¹ : Vec R X
Y : Type u_3
inst✝ : SemiHilbert R Y
f g : X → Y
hf : CDifferentiable R f
hg : CDifferentiable R g
x : X
⊢ cderiv R (fun x => ⟪f x, g x⟫_R) x = fun dx =>
    let y₁ := f x;
    let dy₁ := cderiv R f x dx;
    let y₂ := g x;
    let dy₂ := cderiv R g x dx;
    ⟪dy₁, y₂⟫_R + ⟪y₁, dy₂⟫_R

State before:
case h
K✝ : Type ?u.107796
inst✝²⁰ : RCLike K✝
X✝¹ : Type ?u.107802
inst✝¹⁹ : Vec K✝ X✝¹
Y✝¹ : Type ?u.107815
inst✝¹⁸ : Vec K✝ Y✝¹
Z✝ : Type ?u.107826
inst✝¹⁷ : Vec K✝ Z✝
W✝ : Type ?u.107837
inst✝¹⁶ : Vec K✝ W✝
ι✝ : Type ?u.107848
inst✝¹⁵ : IndexType ι✝
inst✝¹⁴ : LawfulIndexType ι✝
inst✝¹³ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.107875
inst✝¹² : (i : ι✝) → Vec K✝ (E✝ i)
K : Type ?u.107891
inst✝¹¹ : RCLike K
X✝ : Type ?u.107897
inst✝¹⁰ : Vec K X✝
Y✝ : Type ?u.107910
inst✝⁹ : Vec K Y✝
Z : Type ?u.107921
inst✝⁸ : Vec K Z
W : Type ?u.107932
inst✝⁷ : Vec K W
ι : Type ?u.107943
inst✝⁶ : IndexType ι
inst✝⁵ : LawfulIndexType ι
inst✝⁴ : DecidableEq ι
E : ι → Type ?u.107970
inst✝³ : (i : ι) → Vec K (E i)
R : Type u_1
inst✝² : RealScalar R
X : Type u_2
inst✝¹ : Vec R X
Y : Type u_3
inst✝ : SemiHilbert R Y
f g : X → Y
hf : CDifferentiable R f
hg : CDifferentiable R g
x : X
⊢ cderiv R (fun x => ⟪f x, g x⟫_R) x = fun dx =>
    let y₁ := f x;
    let dy₁ := cderiv R f x dx;
    let y₂ := g x;
    let dy₂ := cderiv R g x dx;
    ⟪dy₁, y₂⟫_R + ⟪y₁, dy₂⟫_R
Tactic:
apply Inner.inner.arg_a0a1.cderiv_rule_at f g x (hf x) (hg x)
State after:
no goals