funext w
R : Type u_1
inst✝¹⁰ : RealScalar R
W : Type u_4
inst✝⁹ : SemiInnerProductSpace R W
X : Type u_2
inst✝⁸ : SemiInnerProductSpace R X
Y : Type u_3
inst✝⁷ : SemiInnerProductSpace R Y
inst✝⁶ : Module ℝ Y
Z : Type ?u.120911
inst✝⁵ : SemiInnerProductSpace R Z
inst✝⁴ : Module ℝ Z
U : Type ?u.121783
inst✝³ : SemiInnerProductSpace R U
V : Type ?u.121807
inst✝² : SemiInnerProductSpace R V
inst✝¹ : MeasureSpace X
inst✝ : MeasureSpace Y
f g : W → 𝒟'(X, Y)
hf : DistribDifferentiable f
hg : DistribDifferentiable g
⊢ (parDistribRevDeriv fun w => f w + g w) = fun w =>
    let ydf := parDistribRevDeriv f w;
    let ydg := parDistribRevDeriv g w;
    ydf + ydg
case h
R : Type u_1
inst✝¹⁰ : RealScalar R
W : Type u_4
inst✝⁹ : SemiInnerProductSpace R W
X : Type u_2
inst✝⁸ : SemiInnerProductSpace R X
Y : Type u_3
inst✝⁷ : SemiInnerProductSpace R Y
inst✝⁶ : Module ℝ Y
Z : Type ?u.120911
inst✝⁵ : SemiInnerProductSpace R Z
inst✝⁴ : Module ℝ Z
U : Type ?u.121783
inst✝³ : SemiInnerProductSpace R U
V : Type ?u.121807
inst✝² : SemiInnerProductSpace R V
inst✝¹ : MeasureSpace X
inst✝ : MeasureSpace Y
f g : W → 𝒟'(X, Y)
hf : DistribDifferentiable f
hg : DistribDifferentiable g
w : W
⊢ parDistribRevDeriv (fun w => f w + g w) w =
    let ydf := parDistribRevDeriv f w;
    let ydg := parDistribRevDeriv g w;
    ydf + ydg