Ae eq of tendsto e Lp Norm sub

theorem ae_eq_of_tendsto_eLpNorm_sub    {p : ℝ≥0∞} (hp : 1 ≤ p)    {f : ℕ → α → E} {g₁ g₂ : α → E}    (hf_aesm : ∀ n, AEStronglyMeasurable (f n) μ)    (hg₁ : AEStronglyMeasurable g₁ μ) (hg₂ : AEStronglyMeasurable g₂ μ)    (h1 : Tendsto (fun n => eLpNorm (f n - g₁) p μ) atTop (nhds 0))    (h2 : Tendsto (fun n => eLpNorm (f n - g₂) p μ) atTop (nhds 0)) :    g₁ =ᵐ[μ] g₂ := by  -- eLpNorm(g₁ - g₂) is constant, bounded by eLpNorm(g₁ - f n) + eLpNorm(f n - g₂) → 0  have hzero : eLpNorm (g₁ - g₂) p μ = 0 := le_antisymm (by    have hbound : ∀ n, eLpNorm (g₁ - g₂) p μ ≤        eLpNorm (f n - g₁) p μ + eLpNorm (f n - g₂) p μ := by      intro n      calc eLpNorm (g₁ - g₂) p μ          = eLpNorm ((g₁ - f n) + (f n - g₂)) p μ := by            congr 1; ext x; simp [sub_add_sub_cancel]        _ ≤ eLpNorm (g₁ - f n) p μ + eLpNorm (f n - g₂) p μ :=            eLpNorm_add_le (hg₁.sub (hf_aesm n)) ((hf_aesm n).sub hg₂) hp        _ = eLpNorm (f n - g₁) p μ + eLpNorm (f n - g₂) p μ := by            congr 1            rw [show g₁ - f n = -(f n - g₁) from by                  ext x                  simp [sub_eq_add_neg],                eLpNorm_neg]    -- Constant ≤ sum → 0, so constant = 0    have hsum_tendsto : Tendsto (fun n => eLpNorm (f n - g₁) p μ + eLpNorm (f n - g₂) p μ)        atTop (nhds 0) := by simpa [add_zero] using h1.add h2    exact ge_of_tendsto hsum_tendsto (Filter.Eventually.of_forall hbound)) bot_le  have hae_zero := (eLpNorm_eq_zero_iff (hg₁.sub hg₂)    (ne_of_gt (lt_of_lt_of_le (by simp : (0 : ℝ≥0∞) < 1) hp))).mp hzero  -- g₁ - g₂ =ᵐ 0 → g₁ =ᵐ g₂  exact hae_zero.mono fun x hx => by simpa [sub_eq_zero] using hx