simp[parDistribRevDeriv]
case h.a.a
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
φ : 𝒟 X
⊢ ((parDistribRevDeriv (fun w => f w + g w) w) φ).1 =
    ((let ydf := parDistribRevDeriv f w;
        let ydg := parDistribRevDeriv g w;
        ydf + ydg)
        φ).1

case h.a.a.a
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
φ : 𝒟 X
x✝ : Y
⊢ ((parDistribRevDeriv (fun w => f w + g w) w) φ).2 x✝ =
    ((let ydf := parDistribRevDeriv f w;
          let ydg := parDistribRevDeriv g w;
          ydf + ydg)
          φ).2
      x✝
case h.a.a.a
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
φ : 𝒟 X
x✝ : Y
⊢ ((parDistribRevDeriv (fun w => f w + g w) w) φ).2 x✝ =
    ((let ydf := parDistribRevDeriv f w;
          let ydg := parDistribRevDeriv g w;
          ydf + ydg)
          φ).2
      x✝