-- Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean
theorem ae_bdd_liminf_atTop_of_eLpNorm_bdd {p : ℝ≥0∞} (hp : p ≠ 0) {f : ℕ → α → E}
    (hfmeas : ∀ n, Measurable (f n)) (hbdd : ∀ n, eLpNorm (f n) p μ ≤ R) :
    ∀ᵐ x ∂μ, liminf (fun n => (‖f n x‖ₑ)) atTop < ∞

Proof state:
case pos
α : Type u_1
E : Type u_3
m0 : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : MeasurableSpace E
inst✝ : OpensMeasurableSpace E
R : ℝ≥0
p : ℝ≥0∞
hp : p ≠ 0
f : ℕ → α → E
hfmeas : ∀ (n : ℕ), Measurable (f n)
hbdd : ∀ (n : ℕ), eLpNorm (f n) p μ ≤ ↑R
hp' : p = ⊤
⊢ ∀ᵐ (x : α) ∂μ, liminf (fun n => ‖f n x‖ₑ) atTop < ⊤

Tactic:
subst hp'

Result:
case pos
α : Type u_1
E : Type u_3
m0 : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : MeasurableSpace E
inst✝ : OpensMeasurableSpace E
R : ℝ≥0
f : ℕ → α → E
hfmeas : ∀ (n : ℕ), Measurable (f n)
hp : ⊤ ≠ 0
hbdd : ∀ (n : ℕ), eLpNorm (f n) ⊤ μ ≤ ↑R
⊢ ∀ᵐ (x : α) ∂μ, liminf (fun n => ‖f n x‖ₑ) atTop < ⊤

Proof state:
case pos
α : Type u_1
E : Type u_3
m0 : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : MeasurableSpace E
inst✝ : OpensMeasurableSpace E
R : ℝ≥0
f : ℕ → α → E
hfmeas : ∀ (n : ℕ), Measurable (f n)
hp : ⊤ ≠ 0
hbdd : ∀ (n : ℕ), eLpNormEssSup (f n) μ ≤ ↑R
this : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), ‖f i a‖ₑ < ↑R + 1
⊢ ∀ᵐ (x : α) ∂μ, liminf (fun n => ‖f n x‖ₑ) atTop < ⊤

Tactic:
filter_upwards [this] with x hx using lt_of_le_of_lt
    (liminf_le_of_frequently_le' <| Frequently.of_forall fun n => (hx n).le)
    (ENNReal.add_lt_top.2 ⟨ENNReal.coe_lt_top, ENNReal.one_lt_top⟩)

Result:
no goals

Proof state:
case neg
α : Type u_1
E : Type u_3
m0 : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : MeasurableSpace E
inst✝ : OpensMeasurableSpace E
R : ℝ≥0
p : ℝ≥0∞
hp : p ≠ 0
f : ℕ → α → E
hfmeas : ∀ (n : ℕ), Measurable (f n)
hbdd : ∀ (n : ℕ), eLpNorm (f n) p μ ≤ ↑R
hp' : ¬p = ⊤
⊢ ∀ᵐ (x : α) ∂μ, liminf (fun n => ‖f n x‖ₑ) atTop < ⊤

Tactic:
filter_upwards [ae_bdd_liminf_atTop_rpow_of_eLpNorm_bdd hfmeas hbdd] with x hx

Result:
case h
α : Type u_1
E : Type u_3
m0 : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : MeasurableSpace E
inst✝ : OpensMeasurableSpace E
R : ℝ≥0
p : ℝ≥0∞
hp : p ≠ 0
f : ℕ → α → E
hfmeas : ∀ (n : ℕ), Measurable (f n)
hbdd : ∀ (n : ℕ), eLpNorm (f n) p μ ≤ ↑R
hp' : ¬p = ⊤
x : α
hx : liminf (fun n => ‖f n x‖ₑ ^ p.toReal) atTop < ⊤
⊢ liminf (fun n => ‖f n x‖ₑ) atTop < ⊤

Proof state:
case pos
α : Type u_1
E : Type u_3
m0 : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : MeasurableSpace E
inst✝ : OpensMeasurableSpace E
R : ℝ≥0
f : ℕ → α → E
hfmeas : ∀ (n : ℕ), Measurable (f n)
hp : ⊤ ≠ 0
hbdd : ∀ (n : ℕ), eLpNormEssSup (f n) μ ≤ ↑R
⊢ ∀ᵐ (x : α) ∂μ, liminf (fun n => ‖f n x‖ₑ) atTop < ⊤

Tactic:
have : ∀ n, ∀ᵐ x ∂μ, (‖f n x‖ₑ) < R + 1 := fun n =>
  ae_lt_of_essSup_lt
    (lt_of_le_of_lt (hbdd n) <| ENNReal.lt_add_right ENNReal.coe_ne_top one_ne_zero)

Result:
case pos
α : Type u_1
E : Type u_3
m0 : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : MeasurableSpace E
inst✝ : OpensMeasurableSpace E
R : ℝ≥0
f : ℕ → α → E
hfmeas : ∀ (n : ℕ), Measurable (f n)
hp : ⊤ ≠ 0
hbdd : ∀ (n : ℕ), eLpNormEssSup (f n) μ ≤ ↑R
this : ∀ (n : ℕ), ∀ᵐ (x : α) ∂μ, ‖f n x‖ₑ < ↑R + 1
⊢ ∀ᵐ (x : α) ∂μ, liminf (fun n => ‖f n x‖ₑ) atTop < ⊤

Proof state:
α : Type u_1
E : Type u_3
m0 : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : MeasurableSpace E
inst✝ : OpensMeasurableSpace E
R : ℝ≥0
p : ℝ≥0∞
hp : p ≠ 0
f : ℕ → α → E
hfmeas : ∀ (n : ℕ), Measurable (f n)
hbdd : ∀ (n : ℕ), eLpNorm (f n) p μ ≤ ↑R
hp' : ¬p = ⊤
x : α
hx : liminf (fun n => ‖f n x‖ₑ ^ p.toReal) atTop < ⊤
hppos : 0 < p.toReal
⊢ liminf (fun n => (ENNReal.orderIsoRpow p.toReal hppos) ‖f n x‖ₑ) atTop =
    (ENNReal.orderIsoRpow p.toReal hppos) (liminf (fun n => ‖f n x‖ₑ) atTop)

Tactic:
refine (OrderIso.liminf_apply (ENNReal.orderIsoRpow p.toReal _) ?_ ?_ ?_ ?_).symm <;>
  isBoundedDefault

Result:
no goals