rw[add_comm]
case h.h.h
K : Type u_1
inst✝³ : RCLike K
X : Type u_3
inst✝² : SemiInnerProductSpace K X
Y : Type u_3
inst✝¹ : SemiInnerProductSpace K Y
W : Type u_2
inst✝ : SemiInnerProductSpace K W
f : W → X
g : W → Y
hf : HasAdjDiff K f
hg : HasAdjDiff K g
x : W
dy : MProd X Y
dx : W
⊢ (revDeriv K (fun w => f w) x).2 dy.fst + (revDeriv K (fun w => g w) x).2 dy.snd =
    (revDeriv K g x).2 dy.snd + (revDeriv K f x).2 dy.fst
no goals