∀ {E : Type u_1} {F : Type u_2} {G : Type u_3} {W : Type u_4} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] [inst_4 : NormedAddCommGroup G] [inst_5 : NormedSpace ℝ G]
  [inst_6 : NormedAddCommGroup W] [inst_7 : NormedSpace ℝ W] [inst_8 : MeasurableSpace E] {μ : MeasureTheory.Measure E}
  [BorelSpace E] [FiniteDimensional ℝ E] [μ.IsAddHaarMeasure] {f f' : E → F} {g g' : E → G} {v : E}
  {B : F →L[ℝ] G →L[ℝ] W},
  MeasureTheory.Integrable (fun x => (B (f' x)) (g x)) μ →
    MeasureTheory.Integrable (fun x => (B (f x)) (g' x)) μ →
      MeasureTheory.Integrable (fun x => (B (f x)) (g x)) μ →
        (∀ (x : E), HasLineDerivAt ℝ f (f' x) x v) →
          (∀ (x : E), HasLineDerivAt ℝ g (g' x) x v) → ∫ (x : E), (B (f x)) (g' x) ∂μ = -∫ (x : E), (B (f' x)) (g x) ∂μ