-- Mathlib/MeasureTheory/Function/LpSpace/Basic.lean
theorem eLpNorm_exponent_top_lim_eq_essSup_liminf {ι} [Nonempty ι] [LinearOrder ι] {f : ι → α → G}
    {f_lim : α → G} (h_lim : ∀ᵐ x : α ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (f_lim x))) :
    eLpNorm f_lim ∞ μ = essSup (fun x => atTop.liminf fun m => ‖f m x‖ₑ) μ

Proof state:
α : Type u_1
G : Type u_6
m0 : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup G
ι : Type u_7
inst✝¹ : Nonempty ι
inst✝ : LinearOrder ι
f : ι → α → G
f_lim : α → G
h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (f_lim x))
⊢ eLpNorm f_lim ⊤ μ = essSup (fun x => liminf (fun m => ‖f m x‖ₑ) atTop) μ

Tactic:
rw [eLpNorm_exponent_top, eLpNormEssSup_eq_essSup_enorm]

Result:
α : Type u_1
G : Type u_6
m0 : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup G
ι : Type u_7
inst✝¹ : Nonempty ι
inst✝ : LinearOrder ι
f : ι → α → G
f_lim : α → G
h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (f_lim x))
⊢ essSup (fun x => ‖f_lim x‖ₑ) μ = essSup (fun x => liminf (fun m => ‖f m x‖ₑ) atTop) μ

Proof state:
α : Type u_1
G : Type u_6
m0 : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup G
ι : Type u_7
inst✝¹ : Nonempty ι
inst✝ : LinearOrder ι
f : ι → α → G
f_lim : α → G
h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (f_lim x))
⊢ essSup (fun x => ‖f_lim x‖ₑ) μ = essSup (fun x => liminf (fun m => ‖f m x‖ₑ) atTop) μ

Tactic:
refine essSup_congr_ae (h_lim.mono fun x hx => ?_)

Result:
α : Type u_1
G : Type u_6
m0 : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup G
ι : Type u_7
inst✝¹ : Nonempty ι
inst✝ : LinearOrder ι
f : ι → α → G
f_lim : α → G
h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (f_lim x))
x : α
hx : Tendsto (fun n => f n x) atTop (𝓝 (f_lim x))
⊢ (fun x => ‖f_lim x‖ₑ) x = (fun x => liminf (fun m => ‖f m x‖ₑ) atTop) x

Proof state:
α : Type u_1
G : Type u_6
m0 : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup G
ι : Type u_7
inst✝¹ : Nonempty ι
inst✝ : LinearOrder ι
f : ι → α → G
f_lim : α → G
h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (f_lim x))
x : α
hx : Tendsto (fun n => f n x) atTop (𝓝 (f_lim x))
⊢ Tendsto (fun m => ‖f m x‖ₑ) atTop (𝓝 ‖f_lim x‖ₑ)

Tactic:
exact (continuous_enorm.tendsto (f_lim x)).comp hx

Result:
no goals

Proof state:
α : Type u_1
G : Type u_6
m0 : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup G
ι : Type u_7
inst✝¹ : Nonempty ι
inst✝ : LinearOrder ι
f : ι → α → G
f_lim : α → G
h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (f_lim x))
x : α
hx : Tendsto (fun n => f n x) atTop (𝓝 (f_lim x))
⊢ (fun x => ‖f_lim x‖ₑ) x = (fun x => liminf (fun m => ‖f m x‖ₑ) atTop) x

Tactic:
dsimp only

Result:
α : Type u_1
G : Type u_6
m0 : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup G
ι : Type u_7
inst✝¹ : Nonempty ι
inst✝ : LinearOrder ι
f : ι → α → G
f_lim : α → G
h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (f_lim x))
x : α
hx : Tendsto (fun n => f n x) atTop (𝓝 (f_lim x))
⊢ ‖f_lim x‖ₑ = liminf (fun m => ‖f m x‖ₑ) atTop

Proof state:
α : Type u_1
G : Type u_6
m0 : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup G
ι : Type u_7
inst✝¹ : Nonempty ι
inst✝ : LinearOrder ι
f : ι → α → G
f_lim : α → G
h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (f_lim x))
x : α
hx : Tendsto (fun n => f n x) atTop (𝓝 (f_lim x))
⊢ ‖f_lim x‖ₑ = liminf (fun m => ‖f m x‖ₑ) atTop

Tactic:
apply (Tendsto.liminf_eq ..).symm

Result:
α : Type u_1
G : Type u_6
m0 : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup G
ι : Type u_7
inst✝¹ : Nonempty ι
inst✝ : LinearOrder ι
f : ι → α → G
f_lim : α → G
h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (f_lim x))
x : α
hx : Tendsto (fun n => f n x) atTop (𝓝 (f_lim x))
⊢ Tendsto (fun m => ‖f m x‖ₑ) atTop (𝓝 ‖f_lim x‖ₑ)