-- Mathlib/MeasureTheory/Function/UnifTight.lean
theorem tendsto_Lp_of_tendsto_ae (hp : 1 ≤ p) (hp' : p ≠ ∞)
    {f : ℕ → α → β} {g : α → β} (haef : ∀ n, AEStronglyMeasurable (f n) μ)
    (hg' : MemLp g p μ) (hui : UnifIntegrable f p μ) (hut : UnifTight f p μ)
    (hfg : ∀ᵐ x ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))) :
    Tendsto (fun n => eLpNorm (f n - g) p μ) atTop (𝓝 0)

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup β
μ : Measure α
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ⊤
f : ℕ → α → β
g : α → β
haef : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hg' : MemLp g p μ
hui : UnifIntegrable f p μ
hut : UnifTight f p μ
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))
hf : ∀ (n : ℕ), StronglyMeasurable (AEStronglyMeasurable.mk (f n) ⋯)
hff' : ∀ (n : ℕ), f n =ᶠ[ae μ] AEStronglyMeasurable.mk (f n) ⋯
f' : ℕ → α → β := fun n => AEStronglyMeasurable.mk (f n) ⋯
hui' : UnifIntegrable f' p μ
hut' : UnifTight f' p μ
g' : α → β := AEStronglyMeasurable.mk g ⋯
hg : StronglyMeasurable g'
hgg' : g =ᶠ[ae μ] g'
hg'' : MemLp g' p μ
haefg' : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => AEStronglyMeasurable.mk (f n) ⋯ x) atTop (𝓝 (g' x))
haefg : ∀ (n : ℕ), f n - g =ᶠ[ae μ] f' n - g'
⊢ Tendsto (fun n => eLpNorm (f n - g) p μ) atTop (𝓝 0)

Tactic:
have hsnfg (n : ℕ) := eLpNorm_congr_ae (p := p) (haefg n)

Result:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup β
μ : Measure α
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ⊤
f : ℕ → α → β
g : α → β
haef : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hg' : MemLp g p μ
hui : UnifIntegrable f p μ
hut : UnifTight f p μ
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))
hf : ∀ (n : ℕ), StronglyMeasurable (AEStronglyMeasurable.mk (f n) ⋯)
hff' : ∀ (n : ℕ), f n =ᶠ[ae μ] AEStronglyMeasurable.mk (f n) ⋯
f' : ℕ → α → β := fun n => AEStronglyMeasurable.mk (f n) ⋯
hui' : UnifIntegrable f' p μ
hut' : UnifTight f' p μ
g' : α → β := AEStronglyMeasurable.mk g ⋯
hg : StronglyMeasurable g'
hgg' : g =ᶠ[ae μ] g'
hg'' : MemLp g' p μ
haefg' : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => AEStronglyMeasurable.mk (f n) ⋯ x) atTop (𝓝 (g' x))
haefg : ∀ (n : ℕ), f n - g =ᶠ[ae μ] f' n - g'
hsnfg : ∀ (n : ℕ), eLpNorm (f n - g) p μ = eLpNorm (f' n - g') p μ
⊢ Tendsto (fun n => eLpNorm (f n - g) p μ) atTop (𝓝 0)

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup β
μ : Measure α
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ⊤
f : ℕ → α → β
g : α → β
haef : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hg' : MemLp g p μ
hui : UnifIntegrable f p μ
hut : UnifTight f p μ
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))
hf : ∀ (n : ℕ), StronglyMeasurable (AEStronglyMeasurable.mk (f n) ⋯)
hff' : ∀ (n : ℕ), f n =ᶠ[ae μ] AEStronglyMeasurable.mk (f n) ⋯
hui' : UnifIntegrable (fun n => AEStronglyMeasurable.mk (f n) ⋯) p μ
hut' : UnifTight (fun n => AEStronglyMeasurable.mk (f n) ⋯) p μ
hg : StronglyMeasurable (AEStronglyMeasurable.mk g ⋯)
hgg' : g =ᶠ[ae μ] AEStronglyMeasurable.mk g ⋯
hg'' : MemLp (AEStronglyMeasurable.mk g ⋯) p μ
⊢ Tendsto (fun n => eLpNorm (f n - g) p μ) atTop (𝓝 0)

Tactic:
have haefg' := ae_tendsto_ae_congr hff' hgg' hfg

Result:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup β
μ : Measure α
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ⊤
f : ℕ → α → β
g : α → β
haef : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hg' : MemLp g p μ
hui : UnifIntegrable f p μ
hut : UnifTight f p μ
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))
hf : ∀ (n : ℕ), StronglyMeasurable (AEStronglyMeasurable.mk (f n) ⋯)
hff' : ∀ (n : ℕ), f n =ᶠ[ae μ] AEStronglyMeasurable.mk (f n) ⋯
hui' : UnifIntegrable (fun n => AEStronglyMeasurable.mk (f n) ⋯) p μ
hut' : UnifTight (fun n => AEStronglyMeasurable.mk (f n) ⋯) p μ
hg : StronglyMeasurable (AEStronglyMeasurable.mk g ⋯)
hgg' : g =ᶠ[ae μ] AEStronglyMeasurable.mk g ⋯
hg'' : MemLp (AEStronglyMeasurable.mk g ⋯) p μ
haefg' : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => AEStronglyMeasurable.mk (f n) ⋯ x) atTop (𝓝 (AEStronglyMeasurable.mk g ⋯ x))
⊢ Tendsto (fun n => eLpNorm (f n - g) p μ) atTop (𝓝 0)

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup β
μ : Measure α
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ⊤
f : ℕ → α → β
g : α → β
haef : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hg' : MemLp g p μ
hui : UnifIntegrable f p μ
hut : UnifTight f p μ
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))
hf : ∀ (n : ℕ), StronglyMeasurable (AEStronglyMeasurable.mk (f n) ⋯)
hff' : ∀ (n : ℕ), f n =ᶠ[ae μ] AEStronglyMeasurable.mk (f n) ⋯
⊢ Tendsto (fun n => eLpNorm (f n - g) p μ) atTop (𝓝 0)

Tactic:
have hui' := hui.ae_eq hff'

Result:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup β
μ : Measure α
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ⊤
f : ℕ → α → β
g : α → β
haef : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hg' : MemLp g p μ
hui : UnifIntegrable f p μ
hut : UnifTight f p μ
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))
hf : ∀ (n : ℕ), StronglyMeasurable (AEStronglyMeasurable.mk (f n) ⋯)
hff' : ∀ (n : ℕ), f n =ᶠ[ae μ] AEStronglyMeasurable.mk (f n) ⋯
hui' : UnifIntegrable (fun n => AEStronglyMeasurable.mk (f n) ⋯) p μ
⊢ Tendsto (fun n => eLpNorm (f n - g) p μ) atTop (𝓝 0)

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup β
μ : Measure α
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ⊤
f : ℕ → α → β
g : α → β
haef : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hg' : MemLp g p μ
hui : UnifIntegrable f p μ
hut : UnifTight f p μ
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))
hf : ∀ (n : ℕ), StronglyMeasurable (AEStronglyMeasurable.mk (f n) ⋯)
hff' : ∀ (n : ℕ), f n =ᶠ[ae μ] AEStronglyMeasurable.mk (f n) ⋯
f' : ℕ → α → β := fun n => AEStronglyMeasurable.mk (f n) ⋯
hui' : UnifIntegrable f' p μ
hut' : UnifTight f' p μ
g' : α → β := AEStronglyMeasurable.mk g ⋯
hg : StronglyMeasurable g'
hgg' : g =ᶠ[ae μ] g'
hg'' : MemLp g' p μ
haefg' : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => AEStronglyMeasurable.mk (f n) ⋯ x) atTop (𝓝 (g' x))
⊢ Tendsto (fun n => eLpNorm (f n - g) p μ) atTop (𝓝 0)

Tactic:
have haefg (n : ℕ) : f n - g =ᵐ[μ] f' n - g' := (hff' n).sub hgg'

Result:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup β
μ : Measure α
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ⊤
f : ℕ → α → β
g : α → β
haef : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hg' : MemLp g p μ
hui : UnifIntegrable f p μ
hut : UnifTight f p μ
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))
hf : ∀ (n : ℕ), StronglyMeasurable (AEStronglyMeasurable.mk (f n) ⋯)
hff' : ∀ (n : ℕ), f n =ᶠ[ae μ] AEStronglyMeasurable.mk (f n) ⋯
f' : ℕ → α → β := fun n => AEStronglyMeasurable.mk (f n) ⋯
hui' : UnifIntegrable f' p μ
hut' : UnifTight f' p μ
g' : α → β := AEStronglyMeasurable.mk g ⋯
hg : StronglyMeasurable g'
hgg' : g =ᶠ[ae μ] g'
hg'' : MemLp g' p μ
haefg' : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => AEStronglyMeasurable.mk (f n) ⋯ x) atTop (𝓝 (g' x))
haefg : ∀ (n : ℕ), f n - g =ᶠ[ae μ] f' n - g'
⊢ Tendsto (fun n => eLpNorm (f n - g) p μ) atTop (𝓝 0)