Theorem: SciLean.ContCDiffMapFD_fwdDeriv_rule (SciLean/Core/FunctionSpaces/ContCDiffMapFD.lean)

State before:
K : Type u_4
inst✝⁸ : RCLike K
X : Type u_2
inst✝⁷ : Vec K X
Y : Type u_1
inst✝⁶ : Vec K Y
Z : Type u_3
inst✝⁵ : Vec K Z
W : Type u_5
inst✝⁴ : Vec K W
ι : Type ?u.62779
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.62806
inst✝ : (i : ι) → Vec K (E i)
n : ℕ∞
f : W → (X ⟿FD[K,⊤] Y) × Z
g : W → X
⊢ (fwdDeriv K fun w => (f w).1 (g w)) = fun w dw =>
    let fdfz := fwdDeriv K f w dw;
    let xdx := fwdDeriv K g w dw;
    let fw := fdfz.1.1;
    let df := fdfz.2.1;
    let zdz := fw.FD xdx.1 xdx.2;
    (zdz.1, df xdx.1 + zdz.2)
Tactic:
unfold fwdDeriv
State after:
K : Type u_4
inst✝⁸ : RCLike K
X : Type u_2
inst✝⁷ : Vec K X
Y : Type u_1
inst✝⁶ : Vec K Y
Z : Type u_3
inst✝⁵ : Vec K Z
W : Type u_5
inst✝⁴ : Vec K W
ι : Type ?u.62779
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.62806
inst✝ : (i : ι) → Vec K (E i)
n : ℕ∞
f : W → (X ⟿FD[K,⊤] Y) × Z
g : W → X
⊢ (fun x dx => ((fun w => (f w).1 (g w)) x, ∂ (w:=x;dx), (f w).1 (g w))) = fun w dw =>
    let fdfz := (f w, ∂ f w dw);
    let xdx := (g w, ∂ g w dw);
    let fw := fdfz.1.1;
    let df := fdfz.2.1;
    let zdz := fw.FD xdx.1 xdx.2;
    (zdz.1, df xdx.1 + zdz.2)

State before:
K : Type u_4
inst✝⁸ : RCLike K
X : Type u_2
inst✝⁷ : Vec K X
Y : Type u_1
inst✝⁶ : Vec K Y
Z : Type u_3
inst✝⁵ : Vec K Z
W : Type u_5
inst✝⁴ : Vec K W
ι : Type ?u.62779
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.62806
inst✝ : (i : ι) → Vec K (E i)
n : ℕ∞
f : W → (X ⟿FD[K,⊤] Y) × Z
g : W → X
⊢ (fun x dx => ((fun w => (f w).1 (g w)) x, ∂ (w:=x;dx), (f w).1 (g w))) = fun w dw =>
    let fdfz := (f w, ∂ f w dw);
    let xdx := (g w, ∂ g w dw);
    let fw := fdfz.1.1;
    let df := fdfz.2.1;
    let zdz := fw.FD xdx.1 xdx.2;
    (zdz.1, df xdx.1 + zdz.2)
Tactic:
fun_trans
State after:
no goals