∀ {X : Type u_1} {mX : MeasurableSpace X} {μ : MeasureTheory.Measure X} {q : ENNReal} [inst : Fact (1 ≤ q)]
  {E : Type u_2} {F : Type u_3} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedAddCommGroup F]
  {f : X → WithLp q (E × F)} [inst_3 : NormedSpace ℝ E] [inst_4 : NormedSpace ℝ F] [CompleteSpace F],
  MeasureTheory.Integrable f μ → (∫ (x : X), f x ∂μ).fst = ∫ (x : X), (f x).fst ∂μ