sorry
W : Type u_1
inst✝¹¹ : NormedAddCommGroup W
inst✝¹⁰ : NormedSpace ℝ W
inst✝⁹ : CompleteSpace W
X : Type u_2
inst✝⁸ : NormedAddCommGroup X
inst✝⁷ : NormedSpace ℝ X
inst✝⁶ : CompleteSpace X
Y : Type u_1
inst✝⁵ : NormedAddCommGroup Y
inst✝⁴ : NormedSpace ℝ Y
inst✝³ : CompleteSpace Y
Z : Type u_1
inst✝² : NormedAddCommGroup Z
inst✝¹ : NormedSpace ℝ Z
inst✝ : CompleteSpace Z
g : X → Distribution Y
f : X → Y → Distribution Z
φ : Z → W × W
x dx : X
hg : DistribDifferentiable g
hf :
  DistribDifferentiable fun x =>
    match x with
    | (x, y) => f x y
⊢ ⟪g x, fun x' => ⟪distribDeriv (fun x => f x x') x dx, fun x => (φ x).1⟫⟫ +
      ⟪g x, fun x' => ⟪f x x', fun x => (φ x).2⟫⟫ =
    ⟪g x, fun x_1 => ⟪distribDeriv (fun x => f x x_1) x dx, fun x => (φ x).1⟫ + ⟪f x x_1, fun x => (φ x).2⟫⟫
no goals