∀ {α : Type u_1} {E' : Type u_2} {𝕜 : Type u_4} {p : ENNReal} {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E'] [inst_2 : InnerProductSpace 𝕜 E'] [CompleteSpace E']
  [inst_4 : NormedSpace ℝ E'],
  m ≤ m0 →
    ∀ (f : ↥(MeasureTheory.lpMeas E' 𝕜 m p μ)),
      p ≠ 0 →
        p ≠ ⊤ →
          (∀ (s : Set α), MeasurableSet s → μ s < ⊤ → MeasureTheory.IntegrableOn (↑↑↑f) s μ) →
            (∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, ↑↑↑f x ∂μ = 0) → ↑↑↑f =ᵐ[μ] 0