∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} [inst : NormedAddCommGroup β] {μ : MeasureTheory.Measure α}
  {p : ENNReal} {f : ℕ → α → β} {g : α → β},
  p ≠ ⊤ →
    (∀ (n : ℕ), MeasureTheory.MemLp (f n) p μ) →
      MeasureTheory.MemLp g p μ →
        Filter.Tendsto (fun n => MeasureTheory.eLpNorm (f n - g) p μ) Filter.atTop (nhds 0) →
          MeasureTheory.UnifTight f p μ