sorry_proof
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
⊢ semiAdjoint R (fun dx => ∂ (x:=w;dx), ((f x) φ + (g x) φ)) x✝ =
    semiAdjoint R (fun dx => ∂ (x:=w;dx), (f x) φ) x✝ + semiAdjoint R (fun dx => ∂ (x:=w;dx), (g x) φ) x✝
no goals