Theorem: SciLean.fwdDeriv.Inner.inner.arg_a0a1.fwdDeriv_rule (SciLean/Core/FunctionTransformations/FwdDeriv.lean)

State before:
K : Type ?u.132059
inst✝¹¹ : RCLike K
X✝ : Type ?u.132065
inst✝¹⁰ : Vec K X✝
Y✝ : Type ?u.132078
inst✝⁹ : Vec K Y✝
Z : Type ?u.132089
inst✝⁸ : Vec K Z
W : Type ?u.132100
inst✝⁷ : Vec K W
ι : Type ?u.132111
inst✝⁶ : IndexType ι
inst✝⁵ : LawfulIndexType ι
inst✝⁴ : DecidableEq ι
E : ι → Type ?u.132138
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
⊢ (fwdDeriv R fun x => ⟪f x, g x⟫_R) = fun x dx =>
    let y₁dy₁ := fwdDeriv R f x dx;
    let y₂dy₂ := fwdDeriv R g x dx;
    (⟪y₁dy₁.1, y₂dy₂.1⟫_R, ⟪y₁dy₁.2, y₂dy₂.1⟫_R + ⟪y₁dy₁.1, y₂dy₂.2⟫_R)
Tactic:
unfold fwdDeriv
State after:
K : Type ?u.132059
inst✝¹¹ : RCLike K
X✝ : Type ?u.132065
inst✝¹⁰ : Vec K X✝
Y✝ : Type ?u.132078
inst✝⁹ : Vec K Y✝
Z : Type ?u.132089
inst✝⁸ : Vec K Z
W : Type ?u.132100
inst✝⁷ : Vec K W
ι : Type ?u.132111
inst✝⁶ : IndexType ι
inst✝⁵ : LawfulIndexType ι
inst✝⁴ : DecidableEq ι
E : ι → Type ?u.132138
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
⊢ (fun x dx => ((fun x => ⟪f x, g x⟫_R) x, cderiv R (fun x => ⟪f x, g x⟫_R) x dx)) = fun x dx =>
    let y₁dy₁ := (f x, cderiv R f x dx);
    let y₂dy₂ := (g x, cderiv R g x dx);
    (⟪y₁dy₁.1, y₂dy₂.1⟫_R, ⟪y₁dy₁.2, y₂dy₂.1⟫_R + ⟪y₁dy₁.1, y₂dy₂.2⟫_R)

State before:
K : Type ?u.132059
inst✝¹¹ : RCLike K
X✝ : Type ?u.132065
inst✝¹⁰ : Vec K X✝
Y✝ : Type ?u.132078
inst✝⁹ : Vec K Y✝
Z : Type ?u.132089
inst✝⁸ : Vec K Z
W : Type ?u.132100
inst✝⁷ : Vec K W
ι : Type ?u.132111
inst✝⁶ : IndexType ι
inst✝⁵ : LawfulIndexType ι
inst✝⁴ : DecidableEq ι
E : ι → Type ?u.132138
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
⊢ (fun x dx => ((fun x => ⟪f x, g x⟫_R) x, cderiv R (fun x => ⟪f x, g x⟫_R) x dx)) = fun x dx =>
    let y₁dy₁ := (f x, cderiv R f x dx);
    let y₂dy₂ := (g x, cderiv R g x dx);
    (⟪y₁dy₁.1, y₂dy₂.1⟫_R, ⟪y₁dy₁.2, y₂dy₂.1⟫_R + ⟪y₁dy₁.1, y₂dy₂.2⟫_R)
Tactic:
fun_trans
State after:
no goals