-- Mathlib/MeasureTheory/Integral/Lebesgue.lean
theorem lintegral_iInf_ae {f : ℕ → α → ℝ≥0∞} (h_meas : ∀ n, Measurable (f n))
    (h_mono : ∀ n : ℕ, f n.succ ≤ᵐ[μ] f n) (h_fin : ∫⁻ a, f 0 a ∂μ ≠ ∞) :
    ∫⁻ a, ⨅ n, f n a ∂μ = ⨅ n, ∫⁻ a, f n a ∂μ :=
  have fn_le_f0 : ∫⁻ a, ⨅ n, f n a ∂μ ≤ ∫⁻ a, f 0 a ∂μ :=
    lintegral_mono fun _ => iInf_le_of_le 0 le_rfl
  have fn_le_f0' : ⨅ n, ∫⁻ a, f n a ∂μ ≤ ∫⁻ a, f 0 a ∂μ := iInf_le_of_le 0 le_rfl
  (ENNReal.sub_right_inj h_fin fn_le_f0 fn_le_f0').1 <|
    show ∫⁻ a, f 0 a ∂μ - ∫⁻ a, ⨅ n, f n a ∂μ = ∫⁻ a, f 0 a ∂μ - ⨅ n, ∫⁻ a, f n a ∂μ from
      calc
        ∫⁻ a, f 0 a ∂μ - ∫⁻ a, ⨅ n, f n a ∂μ = ∫⁻ a, f 0 a - ⨅ n, f n a ∂μ :=
          (lintegral_sub (.iInf h_meas)
              (ne_top_of_le_ne_top h_fin <| lintegral_mono fun _ => iInf_le _ _)
              (ae_of_all _ fun _ => iInf_le _ _)).symm
        _ = ∫⁻ a, ⨆ n, f 0 a - f n a ∂μ := congr rfl (funext fun _ => ENNReal.sub_iInf)
        _ = ⨆ n, ∫⁻ a, f 0 a - f n a ∂μ :=
          (lintegral_iSup_ae (fun n => (h_meas 0).sub (h_meas n)) fun n =>
            (h_mono n).mono fun _ ha => tsub_le_tsub le_rfl ha)
        _ = ⨆ n, ∫⁻ a, f 0 a ∂μ - ∫⁻ a, f n a ∂μ :=
          (have h_mono : ∀ᵐ a ∂μ, ∀ n : ℕ, f n.succ a ≤ f n a := ae_all_iff.2 h_mono
          have h_mono : ∀ n, ∀ᵐ a ∂μ, f n a ≤ f 0 a := fun n =>
            h_mono.mono fun a h => by
              induction' n with n ih
              · exact le_rfl
              · exact le_trans (h n) ih
          congr_arg iSup <|
            funext fun n =>
              lintegral_sub (h_meas _) (ne_top_of_le_ne_top h_fin <| lintegral_mono_ae <| h_mono n)
                (h_mono n))
        _ = ∫⁻ a, f 0 a ∂μ - ⨅ n, ∫⁻ a, f n a ∂μ := ENNReal.sub_iInf.symm

Proof state:
case succ
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
h_meas : ∀ (n : ℕ), Measurable (f n)
h_mono✝ : ∀ (n : ℕ), f n.succ ≤ᶠ[ae μ] f n
h_fin : ∫⁻ (a : α), f 0 a ∂μ ≠ ⊤
fn_le_f0 : ∫⁻ (a : α), ⨅ n, f n a ∂μ ≤ ∫⁻ (a : α), f 0 a ∂μ
fn_le_f0' : ⨅ n, ∫⁻ (a : α), f n a ∂μ ≤ ∫⁻ (a : α), f 0 a ∂μ
h_mono : ∀ᵐ (a : α) ∂μ, ∀ (n : ℕ), f n.succ a ≤ f n a
a : α
h : ∀ (n : ℕ), f n.succ a ≤ f n a
n : ℕ
ih : f n a ≤ f 0 a
⊢ f (n + 1) a ≤ f 0 a

Tactic:
exact le_trans (h n) ih

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
h_meas : ∀ (n : ℕ), Measurable (f n)
h_mono✝ : ∀ (n : ℕ), f n.succ ≤ᶠ[ae μ] f n
h_fin : ∫⁻ (a : α), f 0 a ∂μ ≠ ⊤
fn_le_f0 : ∫⁻ (a : α), ⨅ n, f n a ∂μ ≤ ∫⁻ (a : α), f 0 a ∂μ
fn_le_f0' : ⨅ n, ∫⁻ (a : α), f n a ∂μ ≤ ∫⁻ (a : α), f 0 a ∂μ
h_mono : ∀ᵐ (a : α) ∂μ, ∀ (n : ℕ), f n.succ a ≤ f n a
n : ℕ
a : α
h : ∀ (n : ℕ), f n.succ a ≤ f n a
⊢ f n a ≤ f 0 a

Tactic:
induction' n with n ih

Result:
case zero
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
h_meas : ∀ (n : ℕ), Measurable (f n)
h_mono✝ : ∀ (n : ℕ), f n.succ ≤ᶠ[ae μ] f n
h_fin : ∫⁻ (a : α), f 0 a ∂μ ≠ ⊤
fn_le_f0 : ∫⁻ (a : α), ⨅ n, f n a ∂μ ≤ ∫⁻ (a : α), f 0 a ∂μ
fn_le_f0' : ⨅ n, ∫⁻ (a : α), f n a ∂μ ≤ ∫⁻ (a : α), f 0 a ∂μ
h_mono : ∀ᵐ (a : α) ∂μ, ∀ (n : ℕ), f n.succ a ≤ f n a
a : α
h : ∀ (n : ℕ), f n.succ a ≤ f n a
⊢ f 0 a ≤ f 0 a

case succ
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
h_meas : ∀ (n : ℕ), Measurable (f n)
h_mono✝ : ∀ (n : ℕ), f n.succ ≤ᶠ[ae μ] f n
h_fin : ∫⁻ (a : α), f 0 a ∂μ ≠ ⊤
fn_le_f0 : ∫⁻ (a : α), ⨅ n, f n a ∂μ ≤ ∫⁻ (a : α), f 0 a ∂μ
fn_le_f0' : ⨅ n, ∫⁻ (a : α), f n a ∂μ ≤ ∫⁻ (a : α), f 0 a ∂μ
h_mono : ∀ᵐ (a : α) ∂μ, ∀ (n : ℕ), f n.succ a ≤ f n a
a : α
h : ∀ (n : ℕ), f n.succ a ≤ f n a
n : ℕ
ih : f n a ≤ f 0 a
⊢ f (n + 1) a ≤ f 0 a

Proof state:
case zero
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
h_meas : ∀ (n : ℕ), Measurable (f n)
h_mono✝ : ∀ (n : ℕ), f n.succ ≤ᶠ[ae μ] f n
h_fin : ∫⁻ (a : α), f 0 a ∂μ ≠ ⊤
fn_le_f0 : ∫⁻ (a : α), ⨅ n, f n a ∂μ ≤ ∫⁻ (a : α), f 0 a ∂μ
fn_le_f0' : ⨅ n, ∫⁻ (a : α), f n a ∂μ ≤ ∫⁻ (a : α), f 0 a ∂μ
h_mono : ∀ᵐ (a : α) ∂μ, ∀ (n : ℕ), f n.succ a ≤ f n a
a : α
h : ∀ (n : ℕ), f n.succ a ≤ f n a
⊢ f 0 a ≤ f 0 a

Tactic:
exact le_rfl

Result:
no goals