-- Mathlib/MeasureTheory/Integral/Lebesgue.lean
theorem limsup_lintegral_le {f : ℕ → α → ℝ≥0∞} (g : α → ℝ≥0∞) (hf_meas : ∀ n, Measurable (f n))
    (h_bound : ∀ n, f n ≤ᵐ[μ] g) (h_fin : ∫⁻ a, g a ∂μ ≠ ∞) :
    limsup (fun n => ∫⁻ a, f n a ∂μ) atTop ≤ ∫⁻ a, limsup (fun n => f n a) atTop ∂μ :=
  calc
    limsup (fun n => ∫⁻ a, f n a ∂μ) atTop = ⨅ n : ℕ, ⨆ i ≥ n, ∫⁻ a, f i a ∂μ :=
      limsup_eq_iInf_iSup_of_nat
    _ ≤ ⨅ n : ℕ, ∫⁻ a, ⨆ i ≥ n, f i a ∂μ := iInf_mono fun _ => iSup₂_lintegral_le _
    _ = ∫⁻ a, ⨅ n : ℕ, ⨆ i ≥ n, f i a ∂μ

Proof state:
case refine_1
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
g : α → ℝ≥0∞
hf_meas : ∀ (n : ℕ), Measurable (f n)
h_bound : ∀ (n : ℕ), f n ≤ᶠ[ae μ] g
h_fin : ∫⁻ (a : α), g a ∂μ ≠ ⊤
n : ℕ
⊢ Measurable fun a => ⨆ i, ⨆ (_ : i ≥ n), f i a

Tactic:
exact .biSup _ (to_countable _) (fun i _ ↦ hf_meas i)

Result:
no goals

Proof state:
case refine_3
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
g : α → ℝ≥0∞
hf_meas : ∀ (n : ℕ), Measurable (f n)
h_bound : ∀ (n : ℕ), f n ≤ᶠ[ae μ] g
h_fin : ∫⁻ (a : α), g a ∂μ ≠ ⊤
⊢ ∀ᵐ (a : α) ∂μ, ⨆ i, ⨆ (_ : i ≥ 0), f i a ≤ g a

Tactic:
refine (ae_all_iff.2 h_bound).mono fun n hn => ?_

Result:
case refine_3
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
g : α → ℝ≥0∞
hf_meas : ∀ (n : ℕ), Measurable (f n)
h_bound : ∀ (n : ℕ), f n ≤ᶠ[ae μ] g
h_fin : ∫⁻ (a : α), g a ∂μ ≠ ⊤
n : α
hn : ∀ (i : ℕ), f i n ≤ g n
⊢ ⨆ i, ⨆ (_ : i ≥ 0), f i n ≤ g n

Proof state:
case refine_2
α : Type u_1
m✝ : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
g : α → ℝ≥0∞
hf_meas : ∀ (n : ℕ), Measurable (f n)
h_bound : ∀ (n : ℕ), f n ≤ᶠ[ae μ] g
h_fin : ∫⁻ (a : α), g a ∂μ ≠ ⊤
n m : ℕ
hnm : n ≤ m
a : α
⊢ (fun n a => ⨆ i, ⨆ (_ : i ≥ n), f i a) m a ≤ (fun n a => ⨆ i, ⨆ (_ : i ≥ n), f i a) n a

Tactic:
exact iSup_le_iSup_of_subset fun i hi => le_trans hnm hi

Result:
no goals

Proof state:
case refine_3
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
g : α → ℝ≥0∞
hf_meas : ∀ (n : ℕ), Measurable (f n)
h_bound : ∀ (n : ℕ), f n ≤ᶠ[ae μ] g
h_fin : ∫⁻ (a : α), g a ∂μ ≠ ⊤
n : α
hn : ∀ (i : ℕ), f i n ≤ g n
⊢ ⨆ i, ⨆ (_ : i ≥ 0), f i n ≤ g n

Tactic:
exact iSup_le fun i => iSup_le fun _ => hn i

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
g : α → ℝ≥0∞
hf_meas : ∀ (n : ℕ), Measurable (f n)
h_bound : ∀ (n : ℕ), f n ≤ᶠ[ae μ] g
h_fin : ∫⁻ (a : α), g a ∂μ ≠ ⊤
⊢ ∫⁻ (a : α), ⨅ n, ⨆ i, ⨆ (_ : i ≥ n), f i a ∂μ = ∫⁻ (a : α), limsup (fun n => f n a) atTop ∂μ

Tactic:
simp only [limsup_eq_iInf_iSup_of_nat]

Result:
no goals

Proof state:
case refine_1
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
g : α → ℝ≥0∞
hf_meas : ∀ (n : ℕ), Measurable (f n)
h_bound : ∀ (n : ℕ), f n ≤ᶠ[ae μ] g
h_fin : ∫⁻ (a : α), g a ∂μ ≠ ⊤
⊢ ∀ (n : ℕ), Measurable fun a => ⨆ i, ⨆ (_ : i ≥ n), f i a

Tactic:
intro n

Result:
case refine_1
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
g : α → ℝ≥0∞
hf_meas : ∀ (n : ℕ), Measurable (f n)
h_bound : ∀ (n : ℕ), f n ≤ᶠ[ae μ] g
h_fin : ∫⁻ (a : α), g a ∂μ ≠ ⊤
n : ℕ
⊢ Measurable fun a => ⨆ i, ⨆ (_ : i ≥ n), f i a

Proof state:
case refine_3
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
g : α → ℝ≥0∞
hf_meas : ∀ (n : ℕ), Measurable (f n)
h_bound : ∀ (n : ℕ), f n ≤ᶠ[ae μ] g
h_fin : ∫⁻ (a : α), g a ∂μ ≠ ⊤
⊢ ∫⁻ (a : α), ⨆ i, ⨆ (_ : i ≥ 0), f i a ∂μ ≠ ⊤

Tactic:
refine ne_top_of_le_ne_top h_fin (lintegral_mono_ae ?_)

Result:
case refine_3
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
g : α → ℝ≥0∞
hf_meas : ∀ (n : ℕ), Measurable (f n)
h_bound : ∀ (n : ℕ), f n ≤ᶠ[ae μ] g
h_fin : ∫⁻ (a : α), g a ∂μ ≠ ⊤
⊢ ∀ᵐ (a : α) ∂μ, ⨆ i, ⨆ (_ : i ≥ 0), f i a ≤ g a

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
g : α → ℝ≥0∞
hf_meas : ∀ (n : ℕ), Measurable (f n)
h_bound : ∀ (n : ℕ), f n ≤ᶠ[ae μ] g
h_fin : ∫⁻ (a : α), g a ∂μ ≠ ⊤
⊢ ⨅ n, ∫⁻ (a : α), ⨆ i, ⨆ (_ : i ≥ n), f i a ∂μ = ∫⁻ (a : α), ⨅ n, ⨆ i, ⨆ (_ : i ≥ n), f i a ∂μ

Tactic:
refine (lintegral_iInf ?_ ?_ ?_).symm

Result:
case refine_1
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
g : α → ℝ≥0∞
hf_meas : ∀ (n : ℕ), Measurable (f n)
h_bound : ∀ (n : ℕ), f n ≤ᶠ[ae μ] g
h_fin : ∫⁻ (a : α), g a ∂μ ≠ ⊤
⊢ ∀ (n : ℕ), Measurable fun a => ⨆ i, ⨆ (_ : i ≥ n), f i a

case refine_2
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
g : α → ℝ≥0∞
hf_meas : ∀ (n : ℕ), Measurable (f n)
h_bound : ∀ (n : ℕ), f n ≤ᶠ[ae μ] g
h_fin : ∫⁻ (a : α), g a ∂μ ≠ ⊤
⊢ Antitone fun n a => ⨆ i, ⨆ (_ : i ≥ n), f i a

case refine_3
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
g : α → ℝ≥0∞
hf_meas : ∀ (n : ℕ), Measurable (f n)
h_bound : ∀ (n : ℕ), f n ≤ᶠ[ae μ] g
h_fin : ∫⁻ (a : α), g a ∂μ ≠ ⊤
⊢ ∫⁻ (a : α), ⨆ i, ⨆ (_ : i ≥ 0), f i a ∂μ ≠ ⊤

Proof state:
case refine_2
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
g : α → ℝ≥0∞
hf_meas : ∀ (n : ℕ), Measurable (f n)
h_bound : ∀ (n : ℕ), f n ≤ᶠ[ae μ] g
h_fin : ∫⁻ (a : α), g a ∂μ ≠ ⊤
⊢ Antitone fun n a => ⨆ i, ⨆ (_ : i ≥ n), f i a

Tactic:
intro n m hnm a

Result:
case refine_2
α : Type u_1
m✝ : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
g : α → ℝ≥0∞
hf_meas : ∀ (n : ℕ), Measurable (f n)
h_bound : ∀ (n : ℕ), f n ≤ᶠ[ae μ] g
h_fin : ∫⁻ (a : α), g a ∂μ ≠ ⊤
n m : ℕ
hnm : n ≤ m
a : α
⊢ (fun n a => ⨆ i, ⨆ (_ : i ≥ n), f i a) m a ≤ (fun n a => ⨆ i, ⨆ (_ : i ≥ n), f i a) n a