awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : (n : ℕ) → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun (f : α → ℝ≥0∞) ↦ ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ (n : ℕ), ⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k
hξ : ξ = ⨆ (n : ℕ), ⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k
this :
  Filter.Tendsto (fun (n : ℕ) ↦ ∫⁻ (x : α), (⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k) x ∂ν) Filter.atTop
    (nhds (∫⁻ (x : α), (⨆ (n : ℕ), ⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k) x ∂ν))
refine_4 :
  Filter.Tendsto (fun (n : ℕ) ↦ ∫⁻ (x : α), (⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k) x ∂ν) Filter.atTop
    (nhds (sSup (measurableLEEval ν μ)))
⊢ sSup (measurableLEEval ν μ) = ∫⁻ (a : α), ξ a ∂ν

Tactic:
refine tendsto_nhds_unique ?_ this

Premises used: tendsto_nhds_unique
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : (n : ℕ) → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun (f : α → ℝ≥0∞) ↦ ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ (n : ℕ), ⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k
hξ : ξ = ⨆ (n : ℕ), ⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k
this :
  Filter.Tendsto (fun (n : ℕ) ↦ ∫⁻ (x : α), (⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k) x ∂ν) Filter.atTop
    (nhds (∫⁻ (x : α), (⨆ (n : ℕ), ⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k) x ∂ν))
⊢ Filter.Tendsto (fun (n : ℕ) ↦ ∫⁻ (x : α), (⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k) x ∂ν) Filter.atTop
    (nhds (sSup (measurableLEEval ν μ)))

Tactic:
tendsto_of_tendsto_of_tendsto_of_le_of_le hg₂ tendsto_const_nhds (fun n ↦ ?_)
          fun n ↦ ?_

Premises used: tendsto_of_tendsto_of_tendsto_of_le_of_le, tendsto_const_nhds
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : (n : ℕ) → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun (f : α → ℝ≥0∞) ↦ ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ (n : ℕ), ⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k
hξ : ξ = ⨆ (n : ℕ), ⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k
this :
  Filter.Tendsto (fun (n : ℕ) ↦ ∫⁻ (x : α), (⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k) x ∂ν) Filter.atTop
    (nhds (∫⁻ (x : α), (⨆ (n : ℕ), ⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k) x ∂ν))
refine_4 : ∀ (n : ℕ), g n ≤ ∫⁻ (x : α), (⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k) x ∂ν
refine_4₁ : ∀ (n : ℕ), ∫⁻ (x : α), (⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k) x ∂ν ≤ sSup (measurableLEEval ν μ)
⊢ Filter.Tendsto (fun (n : ℕ) ↦ ∫⁻ (x : α), (⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k) x ∂ν) Filter.atTop
    (nhds (sSup (measurableLEEval ν μ)))

Tactic:
refine tendsto_of_tendsto_of_tendsto_of_le_of_le hg₂ tendsto_const_nhds (fun n ↦ ?_)
          fun n ↦ ?_

Premises used: tendsto_of_tendsto_of_tendsto_of_le_of_le, tendsto_const_nhds
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : (n : ℕ) → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun (f : α → ℝ≥0∞) ↦ ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ (n : ℕ), ⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k
hξ : ξ = ⨆ (n : ℕ), ⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k
this :
  Filter.Tendsto (fun (n : ℕ) ↦ ∫⁻ (x : α), (⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k) x ∂ν) Filter.atTop
    (nhds (∫⁻ (x : α), (⨆ (n : ℕ), ⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k) x ∂ν))
n : ℕ
refine_4 : (fun (f : α → ℝ≥0∞) ↦ ∫⁻ (x : α), f x ∂ν) (f n) ≤ ∫⁻ (x : α), (⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k) x ∂ν
⊢ g n ≤ ∫⁻ (x : α), (⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k) x ∂ν

Tactic:
rw [← hf₂ n]
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : (n : ℕ) → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun (f : α → ℝ≥0∞) ↦ ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ (n : ℕ), ⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k
hξ : ξ = ⨆ (n : ℕ), ⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k
this :
  Filter.Tendsto (fun (n : ℕ) ↦ ∫⁻ (x : α), (⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k) x ∂ν) Filter.atTop
    (nhds (∫⁻ (x : α), (⨆ (n : ℕ), ⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k) x ∂ν))
n : ℕ
refine_4 : f n ≤ ⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k
⊢ (fun (f : α → ℝ≥0∞) ↦ ∫⁻ (x : α), f x ∂ν) (f n) ≤ ∫⁻ (x : α), (⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k) x ∂ν

Tactic:
apply lintegral_mono

Premises used: MeasureTheory.lintegral_mono
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : (n : ℕ) → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun (f : α → ℝ≥0∞) ↦ ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ (n : ℕ), ⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k
hξ : ξ = ⨆ (n : ℕ), ⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k
this :
  Filter.Tendsto (fun (n : ℕ) ↦ ∫⁻ (x : α), (⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k) x ∂ν) Filter.atTop
    (nhds (∫⁻ (x : α), (⨆ (n : ℕ), ⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k) x ∂ν))
n : ℕ
⊢ f n ≤ fun (x : α) ↦ ⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k x

Tactic:
iSup_le_le f n n le_rfl

Premises used: le_rfl, MeasureTheory.Measure.LebesgueDecomposition.iSup_le_le
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h_1 : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : (n : ℕ) → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun (f : α → ℝ≥0∞) ↦ ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ (n : ℕ), ⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k
hξ : ξ = ⨆ (n : ℕ), ⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k
this :
  Filter.Tendsto (fun (n : ℕ) ↦ ∫⁻ (x : α), (⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k) x ∂ν) Filter.atTop
    (nhds (∫⁻ (x : α), (⨆ (n : ℕ), ⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k) x ∂ν))
n : ℕ
h : ∀ (x : α), Eq (α := ℝ≥0∞) ((⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k) x) (⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k x)
⊢ f n ≤ ⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k

Tactic:
convert! iSup_le_le f n n le_rfl

Premises used: le_rfl, MeasureTheory.Measure.LebesgueDecomposition.iSup_le_le
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : (n : ℕ) → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun (f : α → ℝ≥0∞) ↦ ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ (n : ℕ), ⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k
hξ : ξ = ⨆ (n : ℕ), ⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k
this :
  Filter.Tendsto (fun (n : ℕ) ↦ ∫⁻ (x : α), (⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k) x ∂ν) Filter.atTop
    (nhds (∫⁻ (x : α), (⨆ (n : ℕ), ⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k) x ∂ν))
n : ℕ
x : α
⊢ Eq (α := ℝ≥0∞) ((⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k) x) (⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k x)

Tactic:
simp only [iSup_apply]

Premises used: iSup_apply
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : (n : ℕ) → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun (f : α → ℝ≥0∞) ↦ ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ (n : ℕ), ⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k
hξ : ξ = ⨆ (n : ℕ), ⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k
this :
  Filter.Tendsto (fun (n : ℕ) ↦ ∫⁻ (x : α), (⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k) x ∂ν) Filter.atTop
    (nhds (∫⁻ (x : α), (⨆ (n : ℕ), ⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k) x ∂ν))
n : ℕ
⊢ ∫⁻ (x : α), (⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k) x ∂ν ≤ sSup (measurableLEEval ν μ)

Tactic:
le_sSup ⟨⨆ (k : ℕ) (_ : k ≤ n), f k, iSup_mem_measurableLE' _ hf₁ _, rfl⟩

Premises used: iSup, MeasureTheory.Measure.LebesgueDecomposition.iSup_mem_measurableLE', And.intro, Exists.intro, le_sSup, rfl
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : (n : ℕ) → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun (f : α → ℝ≥0∞) ↦ ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ (n : ℕ), ⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k
hξ : ξ = ⨆ (n : ℕ), ⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k
this :
  Filter.Tendsto (fun (n : ℕ) ↦ ∫⁻ (x : α), (⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k) x ∂ν) Filter.atTop
    (nhds (∫⁻ (x : α), (⨆ (n : ℕ), ⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k) x ∂ν))
n : ℕ
⊢ ∫⁻ (x : α), (⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k) x ∂ν ≤ sSup (measurableLEEval ν μ)

Tactic:
exact le_sSup ⟨⨆ (k : ℕ) (_ : k ≤ n), f k, iSup_mem_measurableLE' _ hf₁ _, rfl⟩
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : (n : ℕ) → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun (f : α → ℝ≥0∞) ↦ ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ (n : ℕ), ⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k
hξ : ξ = ⨆ (n : ℕ), ⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k
n : ℕ
⊢ AEMeasurable (β := ℝ≥0∞) ((fun (n : ℕ) ↦ (⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k : α → ℝ≥0∞)) n) ν

Tactic:
Measurable.aemeasurable ?_

Premises used: Measurable.aemeasurable
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : (n : ℕ) → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun (f : α → ℝ≥0∞) ↦ ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ (n : ℕ), ⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k
hξ : ξ = ⨆ (n : ℕ), ⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k
n : ℕ
refine_1 : Measurable.{u_1, 0} (α := α) (β := ℝ≥0∞) ((fun (n : ℕ) ↦ (⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k : α → ℝ≥0∞)) n)
⊢ AEMeasurable (β := ℝ≥0∞) ((fun (n : ℕ) ↦ (⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k : α → ℝ≥0∞)) n) ν

Tactic:
refine Measurable.aemeasurable ?_

Premises used: Measurable.aemeasurable
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : (n : ℕ) → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun (f : α → ℝ≥0∞) ↦ ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ (n : ℕ), ⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k
hξ : ξ = ⨆ (n : ℕ), ⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k
n : ℕ
⊢ Measurable (β := ℝ≥0∞) fun (x : α) ↦ ⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k x

Tactic:
(iSup_mem_measurableLE _ hf₁ n).1

Premises used: MeasureTheory.Measure.LebesgueDecomposition.iSup_mem_measurableLE, And.left
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h_1 : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : (n : ℕ) → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun (f : α → ℝ≥0∞) ↦ ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ (n : ℕ), ⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k
hξ : ξ = ⨆ (n : ℕ), ⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k
n : ℕ
h :
  ∀ (x : α),
    Eq (α := ℝ≥0∞) ((fun (n : ℕ) ↦ (⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k : α → ℝ≥0∞)) n x) (⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k x)
⊢ Measurable.{u_1, 0} (α := α) (β := ℝ≥0∞) ((fun (n : ℕ) ↦ (⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k : α → ℝ≥0∞)) n)

Tactic:
convert! (iSup_mem_measurableLE _ hf₁ n).1

Premises used: MeasureTheory.Measure.LebesgueDecomposition.iSup_mem_measurableLE, And.left
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : (n : ℕ) → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun (f : α → ℝ≥0∞) ↦ ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ (n : ℕ), ⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k
hξ : ξ = ⨆ (n : ℕ), ⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k
n : ℕ
x : α
⊢ Eq (α := ℝ≥0∞) ((fun (n : ℕ) ↦ (⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k : α → ℝ≥0∞)) n x) (⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k x)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : (n : ℕ) → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun (f : α → ℝ≥0∞) ↦ ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ (n : ℕ), ⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k
hξ : ξ = ⨆ (n : ℕ), ⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k
⊢ ∀ᵐ (x : α) ∂ν, Monotone (β := ℝ≥0∞) fun (n : ℕ) ↦ (fun (n : ℕ) ↦ (⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k : α → ℝ≥0∞)) n x

Tactic:
Filter.Eventually.of_forall fun a ↦ ?_

Premises used: Filter.Eventually.of_forall
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : (n : ℕ) → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun (f : α → ℝ≥0∞) ↦ ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ (n : ℕ), ⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k
hξ : ξ = ⨆ (n : ℕ), ⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k
refine_2 : ∀ (a : α), Monotone (β := ℝ≥0∞) fun (n : ℕ) ↦ (fun (n : ℕ) ↦ (⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k : α → ℝ≥0∞)) n a
⊢ ∀ᵐ (x : α) ∂ν, Monotone (β := ℝ≥0∞) fun (n : ℕ) ↦ (fun (n : ℕ) ↦ (⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k : α → ℝ≥0∞)) n x

Tactic:
refine Filter.Eventually.of_forall fun a ↦ ?_

Premises used: Filter.Eventually.of_forall
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : (n : ℕ) → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun (f : α → ℝ≥0∞) ↦ ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ (n : ℕ), ⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k
hξ : ξ = ⨆ (n : ℕ), ⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k
a : α
⊢ Monotone (β := ℝ≥0∞) fun (n : ℕ) ↦ (fun (n : ℕ) ↦ (⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k : α → ℝ≥0∞)) n a

Tactic:
simp [iSup_monotone' f _]

Premises used: MeasureTheory.Measure.LebesgueDecomposition.iSup_monotone'
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : (n : ℕ) → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun (f : α → ℝ≥0∞) ↦ ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ (n : ℕ), ⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k
hξ : ξ = ⨆ (n : ℕ), ⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k
⊢ ∀ᵐ (x : α) ∂ν,
    Filter.Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ (fun (n : ℕ) ↦ (⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k : α → ℝ≥0∞)) n x)
      Filter.atTop (nhds ((⨆ (n : ℕ), ⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k) x))

Tactic:
Filter.Eventually.of_forall fun a ↦ ?_

Premises used: Filter.Eventually.of_forall
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : (n : ℕ) → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun (f : α → ℝ≥0∞) ↦ ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ (n : ℕ), ⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k
hξ : ξ = ⨆ (n : ℕ), ⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k
refine_3 :
  ∀ (a : α),
    Filter.Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ (fun (n : ℕ) ↦ (⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k : α → ℝ≥0∞)) n a)
      Filter.atTop (nhds ((⨆ (n : ℕ), ⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k) a))
⊢ ∀ᵐ (x : α) ∂ν,
    Filter.Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ (fun (n : ℕ) ↦ (⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k : α → ℝ≥0∞)) n x)
      Filter.atTop (nhds ((⨆ (n : ℕ), ⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k) x))

Tactic:
refine Filter.Eventually.of_forall fun a ↦ ?_

Premises used: Filter.Eventually.of_forall
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : (n : ℕ) → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun (f : α → ℝ≥0∞) ↦ ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ (n : ℕ), ⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k
hξ : ξ = ⨆ (n : ℕ), ⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k
a : α
⊢ Filter.Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ (fun (n : ℕ) ↦ (⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k : α → ℝ≥0∞)) n a) Filter.atTop
    (nhds ((⨆ (n : ℕ), ⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k) a))

Tactic:
simp [tendsto_atTop_iSup (iSup_monotone' f a)]

Premises used: MeasureTheory.Measure.LebesgueDecomposition.iSup_monotone', tendsto_atTop_iSup
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : (n : ℕ) → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun (f : α → ℝ≥0∞) ↦ ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ (n : ℕ), ⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k
hξ : ξ = ⨆ (n : ℕ), ⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k
⊢ sSup (measurableLEEval ν μ) = ∫⁻ (a : α), ξ a ∂ν

Tactic:
have hξ₁ : sSup (measurableLEEval ν μ) = ∫⁻ a, ξ a ∂ν := by
      have := @lintegral_tendsto_of_tendsto_of_monotone _ _ ν (fun n ↦ ⨆ (k) (_ : k ≤ n), f k)
          (⨆ (n) (k) (_ : k ≤ n), f k) ?_ ?_ ?_
      · refine tendsto_nhds_unique ?_ this
        refine tendsto_of_tendsto_of_tendsto_of_le_of_le hg₂ tendsto_const_nhds (fun n ↦ ?_)
          fun n ↦ ?_
        · rw [← hf₂ n]
          apply lintegral_mono
          convert! iSup_le_le f n n le_rfl
          simp only [iSup_apply]
        · exact le_sSup ⟨⨆ (k : ℕ) (_ : k ≤ n), f k, iSup_mem_measurableLE' _ hf₁ _, rfl⟩
      · intro n
        refine Measurable.aemeasurable ?_
        convert! (iSup_mem_measurableLE _ hf₁ n).1
        simp
      · refine Filter.Eventually.of_forall fun a ↦ ?_
        simp [iSup_monotone' f _]
      · refine Filter.Eventually.of_forall fun a ↦ ?_
        simp [tendsto_atTop_iSup (iSup_monotone' f a)]
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : (n : ℕ) → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun (f : α → ℝ≥0∞) ↦ ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ (n : ℕ), ⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k
hξ : ξ = ⨆ (n : ℕ), ⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k
hξ₁ : sSup (measurableLEEval ν μ) = ∫⁻ (a : α), ξ a ∂ν
⊢ Measurable (β := ℝ≥0∞) fun (b : α) ↦ ⨆ (i : ℕ), ⨆ (k : ℕ), ⨆ (_ : k ≤ i), f k b

Tactic:
Measurable.iSup fun n ↦ (iSup_mem_measurableLE _ hf₁ n).1

Premises used: MeasureTheory.Measure.LebesgueDecomposition.iSup_mem_measurableLE, Measurable.iSup, And.left
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h_1 : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : (n : ℕ) → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun (f : α → ℝ≥0∞) ↦ ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ (n : ℕ), ⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k
hξ : ξ = ⨆ (n : ℕ), ⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k
hξ₁ : sSup (measurableLEEval ν μ) = ∫⁻ (a : α), ξ a ∂ν
h : ∀ (x : α), ξ x = ⨆ (i : ℕ), ⨆ (k : ℕ), ⨆ (_ : k ≤ i), f k x
⊢ Measurable ξ

Tactic:
convert! Measurable.iSup fun n ↦ (iSup_mem_measurableLE _ hf₁ n).1

Premises used: MeasureTheory.Measure.LebesgueDecomposition.iSup_mem_measurableLE, Measurable.iSup, And.left
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : (n : ℕ) → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun (f : α → ℝ≥0∞) ↦ ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ (n : ℕ), ⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k
hξ : ξ = ⨆ (n : ℕ), ⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k
hξ₁ : sSup (measurableLEEval ν μ) = ∫⁻ (a : α), ξ a ∂ν
x : α
⊢ ξ x = ⨆ (i : ℕ), ⨆ (k : ℕ), ⨆ (_ : k ≤ i), f k x

Tactic:
simp [hξ]
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : (n : ℕ) → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun (f : α → ℝ≥0∞) ↦ ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ (n : ℕ), ⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k
hξ : ξ = ⨆ (n : ℕ), ⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k
hξ₁ : sSup (measurableLEEval ν μ) = ∫⁻ (a : α), ξ a ∂ν
⊢ Measurable ξ

Tactic:
have hξm : Measurable ξ := by
      convert! Measurable.iSup fun n ↦ (iSup_mem_measurableLE _ hf₁ n).1
      simp [hξ]
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : (n : ℕ) → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun (f : α → ℝ≥0∞) ↦ ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ (n : ℕ), ⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k
hξ : ξ = ⨆ (n : ℕ), ⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k
hξ₁ : sSup (measurableLEEval ν μ) = ∫⁻ (a : α), ξ a ∂ν
hξm : Measurable ξ
A : Set α
hA : MeasurableSet A
rw : ∫⁻ (a : α) in A, (⨆ (n : ℕ), ⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k) a ∂ν ≤ (μ : (a : Set α) → ℝ≥0∞) A
⊢ ∫⁻ (a : α) in A, ξ a ∂ν ≤ (μ : (a : Set α) → ℝ≥0∞) A

Tactic:
rw [hξ]
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
g : ℕ → ℝ≥0∞
h : Monotone g
hg₂ : Filter.Tendsto g Filter.atTop (nhds (sSup (measurableLEEval ν μ)))
f : (n : ℕ) → α → ℝ≥0∞
hf₁ : ∀ (n : ℕ), f n ∈ measurableLE ν μ
hf₂ : ∀ (n : ℕ), (fun (f : α → ℝ≥0∞) ↦ ∫⁻ (x : α), f x ∂ν) (f n) = g n
ξ : α → ℝ≥0∞ := ⨆ (n : ℕ), ⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k
hξ : ξ = ⨆ (n : ℕ), ⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k
hξ₁ : sSup (measurableLEEval ν μ) = ∫⁻ (a : α), ξ a ∂ν
hξm : Measurable ξ
A : Set α
hA : MeasurableSet A
simp_rw : ∫⁻ (a : α) in A, ⨆ (i : ℕ), ⨆ (i_1 : ℕ), ⨆ (_ : i_1 ≤ i), f i_1 a ∂ν ≤ (μ : (a : Set α) → ℝ≥0∞) A
⊢ ∫⁻ (a : α) in A, (⨆ (n : ℕ), ⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k) a ∂ν ≤ (μ : (a : Set α) → ℝ≥0∞) A

Tactic:
simp_rw [iSup_apply]

Premises used: iSup_apply