awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Sort u_2
f : ℕ → α → ℝ≥0∞
m : ℕ
a : α
c : ℝ≥0∞ := ⨆ (k : ℕ), ⨆ (_ : k ≤ m + 1), f k a
hc : c = ⨆ (k : ℕ), ⨆ (_ : k ≤ m + 1), f k a
d : ℝ≥0∞ := max (f m.succ a) (⨆ (k : ℕ), ⨆ (_ : k ≤ m), f k a)
hd : d = max (f m.succ a) (⨆ (k : ℕ), ⨆ (_ : k ≤ m), f k a)
⊢ ⨆ (k : ℕ), ⨆ (_ : k ≤ m + 1), f k a ≤ max (f m.succ a) (⨆ (k : ℕ), ⨆ (_ : k ≤ m), f k a)
have left : ∀ (n : ℕ) (hn : n ≤ m + 1), f n a ≤ max (f m.succ a) (⨆ (k : ℕ), ⨆ (_ : k ≤ m), f k a)
Tactic: refine iSup₂_le fun n hn ↦ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Sort u_2
f : ℕ → α → ℝ≥0∞
m : ℕ
a : α
c : ℝ≥0∞ := ⨆ (k : ℕ), ⨆ (_ : k ≤ m + 1), f k a
hc : c = ⨆ (k : ℕ), ⨆ (_ : k ≤ m + 1), f k a
d : ℝ≥0∞ := max (f m.succ a) (⨆ (k : ℕ), ⨆ (_ : k ≤ m), f k a)
hd : d = max (f m.succ a) (⨆ (k : ℕ), ⨆ (_ : k ≤ m), f k a)
n : ℕ
hn : n ≤ m + 1
⊢ f n a ≤ max (f m.succ a) (⨆ (k : ℕ), ⨆ (_ : k ≤ m), f k a)
have left : ∀ (h : n ≤ m), f n a ≤ max (f m.succ a) (⨆ (k : ℕ), ⨆ (_ : k ≤ m), f k a)
Tactic: rcases Nat.of_le_succ hn with (h | h)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Sort u_2
f : ℕ → α → ℝ≥0∞
m : ℕ
a : α
c : ℝ≥0∞ := ⨆ (k : ℕ), ⨆ (_ : k ≤ m + 1), f k a
hc : c = ⨆ (k : ℕ), ⨆ (_ : k ≤ m + 1), f k a
d : ℝ≥0∞ := max (f m.succ a) (⨆ (k : ℕ), ⨆ (_ : k ≤ m), f k a)
hd : d = max (f m.succ a) (⨆ (k : ℕ), ⨆ (_ : k ≤ m), f k a)
n : ℕ
hn : n ≤ m + 1
left : ∀ (h : n ≤ m), f n a ≤ max (f m.succ a) (⨆ (k : ℕ), ⨆ (_ : k ≤ m), f k a)
⊢ f n a ≤ max (f m.succ a) (⨆ (k : ℕ), ⨆ (_ : k ≤ m), f k a)
have left₁ : ∀ (h : n = m.succ), f n a ≤ max (f m.succ a) (⨆ (k : ℕ), ⨆ (_ : k ≤ m), f k a)
Tactic: rcases Nat.of_le_succ hn with (h | h)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Sort u_2
f : ℕ → α → ℝ≥0∞
m : ℕ
a : α
c : ℝ≥0∞ := ⨆ (k : ℕ), ⨆ (_ : k ≤ m + 1), f k a
hc : c = ⨆ (k : ℕ), ⨆ (_ : k ≤ m + 1), f k a
d : ℝ≥0∞ := max (f m.succ a) (⨆ (k : ℕ), ⨆ (_ : k ≤ m), f k a)
hd : d = max (f m.succ a) (⨆ (k : ℕ), ⨆ (_ : k ≤ m), f k a)
⊢ max (f m.succ a) (⨆ (k : ℕ), ⨆ (_ : k ≤ m), f k a) ≤ ⨆ (k : ℕ), ⨆ (_ : k ≤ m + 1), f k a
have right : f m.succ a ≤ ⨆ (k : ℕ), ⨆ (_ : k ≤ m + 1), f k a
Tactic: refine sup_le ?_ (biSup_mono fun n hn ↦ hn.trans m.le_succ)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), f n ∈ measurableLE μ ν
⊢ (fun (x : α) ↦ ⨆ (k : ℕ), ⨆ (_ : k ≤ 0), f k x) ∈ measurableLE μ ν
have zero : Measurable (β := ℝ≥0∞) fun (x : α) ↦ ⨆ (k : ℕ), ⨆ (_ : k ≤ 0), f k x
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), f n ∈ measurableLE μ ν
zero : Measurable (β := ℝ≥0∞) fun (x : α) ↦ ⨆ (k : ℕ), ⨆ (_ : k ≤ 0), f k x
⊢ (fun (x : α) ↦ ⨆ (k : ℕ), ⨆ (_ : k ≤ 0), f k x) ∈ measurableLE μ ν
have zero₁ : ∀ (A : Set α),
  MeasurableSet A →
    ∫⁻ (x : α) in A, (fun (x : α) ↦ (⨆ (k : ℕ), ⨆ (_ : k ≤ 0), f k x : ℝ≥0∞)) x ∂μ ≤ (ν : (a : Set α) → ℝ≥0∞) A
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (hypothesis)
Goal:
α : Type u_1
m_1 : MeasurableSpace α
μ ν : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), f n ∈ measurableLE μ ν
m : ℕ
hm : (fun (x : α) ↦ ⨆ (k : ℕ), ⨆ (_ : k ≤ m), f k x) ∈ measurableLE μ ν
⊢ (fun (x : α) ↦ ⨆ (k : ℕ), ⨆ (_ : k ≤ m + 1), f k x) ∈ measurableLE μ ν
have this : Eq.{u_1 + 1} (α := (a : α) → ℝ≥0∞) (fun (a : α) ↦ ⨆ (k : ℕ), ⨆ (_ : k ≤ m + 1), f k a) fun (a : α) ↦
  max (f m.succ a) (⨆ (k : ℕ), ⨆ (_ : k ≤ m), f k a)
Tactic: have :
      (fun a : α ↦ ⨆ (k : ℕ) (_ : k ≤ m + 1), f k a) = fun a ↦
        f m.succ a ⊔ ⨆ (k : ℕ) (_ : k ≤ m), f k a :=
      funext fun _ ↦ iSup_succ_eq_sup _ _ _
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m_1 : MeasurableSpace α
μ ν : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), f n ∈ measurableLE μ ν
m : ℕ
hm : (fun (x : α) ↦ ⨆ (k : ℕ), ⨆ (_ : k ≤ m), f k x) ∈ measurableLE μ ν
this :
  Eq.{u_1 + 1} (α := (a : α) → ℝ≥0∞) (fun (a : α) ↦ ⨆ (k : ℕ), ⨆ (_ : k ≤ m + 1), f k a) fun (a : α) ↦
    max (f m.succ a) (⨆ (k : ℕ), ⨆ (_ : k ≤ m), f k a)
⊢ (fun (x : α) ↦ ⨆ (k : ℕ), ⨆ (_ : k ≤ m + 1), f k x) ∈ measurableLE μ ν
have succ : ∀ (A : Set α) (hA : MeasurableSet A),
  ∫⁻ (x : α) in A, (fun (x : α) ↦ (⨆ (k : ℕ), ⨆ (_ : k ≤ m + 1), f k x : ℝ≥0∞)) x ∂μ ≤ (ν : (a : Set α) → ℝ≥0∞) A
Tactic: refine ⟨.iSup fun n ↦ Measurable.iSup_Prop _ (hf n).1, fun A hA ↦ ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m_1 : MeasurableSpace α
μ ν : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), f n ∈ measurableLE μ ν
m : ℕ
hm : (fun (x : α) ↦ ⨆ (k : ℕ), ⨆ (_ : k ≤ m), f k x) ∈ measurableLE μ ν
this :
  Eq.{u_1 + 1} (α := (a : α) → ℝ≥0∞) (fun (a : α) ↦ ⨆ (k : ℕ), ⨆ (_ : k ≤ m + 1), f k a) fun (a : α) ↦
    max (f m.succ a) (⨆ (k : ℕ), ⨆ (_ : k ≤ m), f k a)
A : Set α
hA : MeasurableSet A
⊢ ∫⁻ (x : α) in A, (fun (x : α) ↦ (⨆ (k : ℕ), ⨆ (_ : k ≤ m + 1), f k x : ℝ≥0∞)) x ∂μ ≤ (ν : (a : Set α) → ℝ≥0∞) A
have succ : ∫⁻ (a : α) in A, max (f m.succ a) (⨆ (k : ℕ), ⨆ (_ : k ≤ m), f k a) ∂μ ≤ (ν : (a : Set α) → ℝ≥0∞) A
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), f n ∈ measurableLE μ ν
n : ℕ
⊢ (fun (x : α) ↦ ⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k x) ∈ measurableLE μ ν
have zero : (fun (x : α) ↦ ⨆ (k : ℕ), ⨆ (_ : k ≤ 0), f k x) ∈ measurableLE μ ν
Tactic: induction n with
  | zero =>
    constructor
    · simp [(hf 0).1]
    · intro A hA; simp [(hf 0).2 A hA]
  | succ m hm =>
    have :
      (fun a : α ↦ ⨆ (k : ℕ) (_ : k ≤ m + 1), f k a) = fun a ↦
        f m.succ a ⊔ ⨆ (k : ℕ) (_ : k ≤ m), f k a :=
      funext fun _ ↦ iSup_succ_eq_sup _ _ _
    refine ⟨.iSup fun n ↦ Measurable.iSup_Prop _ (hf n).1, fun A hA ↦ ?_⟩
    rw [this]; exact (sup_mem_measurableLE (hf m.succ) hm).2 A hA
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), f n ∈ measurableLE μ ν
n : ℕ
zero : (fun (x : α) ↦ ⨆ (k : ℕ), ⨆ (_ : k ≤ 0), f k x) ∈ measurableLE μ ν
⊢ (fun (x : α) ↦ ⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k x) ∈ measurableLE μ ν
have succ : ∀ (m_1 : ℕ) (hm : (fun (x : α) ↦ ⨆ (k : ℕ), ⨆ (_ : k ≤ m_1), f k x) ∈ measurableLE μ ν),
  (fun (x : α) ↦ ⨆ (k : ℕ), ⨆ (_ : k ≤ m_1 + 1), f k x) ∈ measurableLE μ ν
Tactic: induction n with
  | zero =>
    constructor
    · simp [(hf 0).1]
    · intro A hA; simp [(hf 0).2 A hA]
  | succ m hm =>
    have :
      (fun a : α ↦ ⨆ (k : ℕ) (_ : k ≤ m + 1), f k a) = fun a ↦
        f m.succ a ⊔ ⨆ (k : ℕ) (_ : k ≤ m), f k a :=
      funext fun _ ↦ iSup_succ_eq_sup _ _ _
    refine ⟨.iSup fun n ↦ Measurable.iSup_Prop _ (hf n).1, fun A hA ↦ ?_⟩
    rw [this]; exact (sup_mem_measurableLE (hf m.succ) hm).2 A hA
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), f n ∈ measurableLE μ ν
n : ℕ
⊢ ⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k ∈ measurableLE μ ν
have h : ∀ (x : α), Eq (α := ℝ≥0∞) ((⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k) x) (⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k x)
Tactic: convert! iSup_mem_measurableLE f hf n
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
⊢ ∃ (p : Measure α × (α → ℝ≥0∞)), Measurable p.2 ∧ p.1 ⟂ₘ ν ∧ μ = p.1 + ν.withDensity p.2
have h : ∃ (u : ℕ → ℝ≥0∞),
  Monotone u ∧
    Filter.Tendsto u Filter.atTop (nhds (sSup (measurableLEEval ν μ))) ∧ ∀ (n : ℕ), u n ∈ measurableLEEval ν μ
Tactic: have h := @exists_seq_tendsto_sSup _ _ _ _ _ (measurableLEEval ν μ)
      ⟨0, 0, zero_mem_measurableLE, by simp⟩ (OrderTop.bddAbove _)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
h :
  ∃ (u : ℕ → ℝ≥0∞),
    Monotone u ∧
      Filter.Tendsto u Filter.atTop (nhds (sSup (measurableLEEval ν μ))) ∧ ∀ (n : ℕ), u n ∈ measurableLEEval ν μ
⊢ ∃ (p : Measure α × (α → ℝ≥0∞)), Measurable p.2 ∧ p.1 ⟂ₘ ν ∧ μ = p.1 + ν.withDensity p.2
have choose : ∀ (g : ℕ → ℝ≥0∞),
  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),
      ∃ (p : Measure α × (α → ℝ≥0∞)), Measurable p.2 ∧ p.1 ⟂ₘ ν ∧ μ = p.1 + ν.withDensity p.2
Tactic: choose g _ hg₂ f hf₁ hf₂ using h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (hypothesis)
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
⊢ ∃ (p : Measure α × (α → ℝ≥0∞)), Measurable p.2 ∧ p.1 ⟂ₘ ν ∧ μ = p.1 + ν.withDensity p.2
have hξ : let ξ : α → ℝ≥0∞ := ⨆ (n : ℕ), ⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k;
ξ = ⨆ (n : ℕ), ⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k
Tactic: set ξ := ⨆ (n) (k) (_ : k ≤ n), f k with hξ
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
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 ∂ν
have refine_4 : ∀
  (this :
    Filter.Tendsto (fun (n : ℕ) ↦ ∫⁻ (x : α), (⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k) x ∂ν) Filter.atTop
      (nhds (∫⁻ (x : α), (⨆ (n : ℕ), ⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k) x ∂ν))),
  sSup (measurableLEEval ν μ) = ∫⁻ (a : α), ξ a ∂ν
Tactic: have := @lintegral_tendsto_of_tendsto_of_monotone _ _ ν (fun n ↦ ⨆ (k) (_ : k ≤ n), f k)
          (⨆ (n) (k) (_ : k ≤ n), f k) ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
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_4 :
  ∀
    (this :
      Filter.Tendsto (fun (n : ℕ) ↦ ∫⁻ (x : α), (⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k) x ∂ν) Filter.atTop
        (nhds (∫⁻ (x : α), (⨆ (n : ℕ), ⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k) x ∂ν))),
    sSup (measurableLEEval ν μ) = ∫⁻ (a : α), ξ a ∂ν
⊢ sSup (measurableLEEval ν μ) = ∫⁻ (a : α), ξ a ∂ν
have refine_1 : ∀ (n : ℕ), AEMeasurable (β := ℝ≥0∞) ((fun (n : ℕ) ↦ (⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k : α → ℝ≥0∞)) n) ν
Tactic: have := @lintegral_tendsto_of_tendsto_of_monotone _ _ ν (fun n ↦ ⨆ (k) (_ : k ≤ n), f k)
          (⨆ (n) (k) (_ : k ≤ n), f k) ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
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_4 :
  ∀
    (this :
      Filter.Tendsto (fun (n : ℕ) ↦ ∫⁻ (x : α), (⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k) x ∂ν) Filter.atTop
        (nhds (∫⁻ (x : α), (⨆ (n : ℕ), ⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k) x ∂ν))),
    sSup (measurableLEEval ν μ) = ∫⁻ (a : α), ξ a ∂ν
refine_1 : ∀ (n : ℕ), AEMeasurable (β := ℝ≥0∞) ((fun (n : ℕ) ↦ (⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k : α → ℝ≥0∞)) n) ν
⊢ sSup (measurableLEEval ν μ) = ∫⁻ (a : α), ξ a ∂ν
have refine_2 : ∀ᵐ (x : α) ∂ν, Monotone (β := ℝ≥0∞) fun (n : ℕ) ↦ (fun (n : ℕ) ↦ (⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k : α → ℝ≥0∞)) n x
Tactic: have := @lintegral_tendsto_of_tendsto_of_monotone _ _ ν (fun n ↦ ⨆ (k) (_ : k ≤ n), f k)
          (⨆ (n) (k) (_ : k ≤ n), f k) ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
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_4 :
  ∀
    (this :
      Filter.Tendsto (fun (n : ℕ) ↦ ∫⁻ (x : α), (⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k) x ∂ν) Filter.atTop
        (nhds (∫⁻ (x : α), (⨆ (n : ℕ), ⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k) x ∂ν))),
    sSup (measurableLEEval ν μ) = ∫⁻ (a : α), ξ a ∂ν
refine_1 : ∀ (n : ℕ), AEMeasurable (β := ℝ≥0∞) ((fun (n : ℕ) ↦ (⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k : α → ℝ≥0∞)) n) ν
refine_2 :
  ∀ᵐ (x : α) ∂ν, Monotone (β := ℝ≥0∞) fun (n : ℕ) ↦ (fun (n : ℕ) ↦ (⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k : α → ℝ≥0∞)) n x
⊢ sSup (measurableLEEval ν μ) = ∫⁻ (a : α), ξ a ∂ν
have refine_3 : ∀ᵐ (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: have := @lintegral_tendsto_of_tendsto_of_monotone _ _ ν (fun n ↦ ⨆ (k) (_ : k ≤ n), f k)
          (⨆ (n) (k) (_ : k ≤ n), f k) ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
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 ∂ν))
⊢ sSup (measurableLEEval ν μ) = ∫⁻ (a : α), ξ a ∂ν
have refine_4 : Filter.Tendsto (fun (n : ℕ) ↦ ∫⁻ (x : α), (⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k) x ∂ν) Filter.atTop
  (nhds (sSup (measurableLEEval ν μ)))
Tactic: refine tendsto_nhds_unique ?_ this
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
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 ν μ)))
have refine_4 : ∀ (n : ℕ), g n ≤ ∫⁻ (x : α), (⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k) x ∂ν
Tactic: refine tendsto_of_tendsto_of_tendsto_of_le_of_le hg₂ tendsto_const_nhds (fun n ↦ ?_)
          fun n ↦ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
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 ∂ν
⊢ Filter.Tendsto (fun (n : ℕ) ↦ ∫⁻ (x : α), (⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k) x ∂ν) Filter.atTop
    (nhds (sSup (measurableLEEval ν μ)))
have refine_4₁ : ∀ (n : ℕ), ∫⁻ (x : α), (⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k) x ∂ν ≤ sSup (measurableLEEval ν μ)
Tactic: refine tendsto_of_tendsto_of_tendsto_of_le_of_le hg₂ tendsto_const_nhds (fun n ↦ ?_)
          fun n ↦ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
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 : ℕ
⊢ g n ≤ ∫⁻ (x : α), (⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k) x ∂ν
have refine_4 : (fun (f : α → ℝ≥0∞) ↦ ∫⁻ (x : α), f x ∂ν) (f n) ≤ ∫⁻ (x : α), (⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k) x ∂ν
Tactic: rw [← hf₂ n]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
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 : ℕ
⊢ (fun (f : α → ℝ≥0∞) ↦ ∫⁻ (x : α), f x ∂ν) (f n) ≤ ∫⁻ (x : α), (⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k) x ∂ν
have refine_4 : f n ≤ ⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k
Tactic: apply lintegral_mono
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
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 ≤ ⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k
have h : ∀ (x : α), Eq (α := ℝ≥0∞) ((⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k) x) (⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k x)
Tactic: convert! iSup_le_le f n n le_rfl
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
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) ν
have refine_1 : Measurable.{u_1, 0} (α := α) (β := ℝ≥0∞) ((fun (n : ℕ) ↦ (⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k : α → ℝ≥0∞)) n)
Tactic: refine Measurable.aemeasurable ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
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.{u_1, 0} (α := α) (β := ℝ≥0∞) ((fun (n : ℕ) ↦ (⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k : α → ℝ≥0∞)) n)
have h : ∀ (x : α),
  Eq (α := ℝ≥0∞) ((fun (n : ℕ) ↦ (⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k : α → ℝ≥0∞)) n x) (⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k x)
Tactic: convert! (iSup_mem_measurableLE _ hf₁ n).1
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
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
have refine_2 : ∀ (a : α), Monotone (β := ℝ≥0∞) fun (n : ℕ) ↦ (fun (n : ℕ) ↦ (⨆ (k : ℕ), ⨆ (_ : k ≤ n), f k : α → ℝ≥0∞)) n a
Tactic: refine Filter.Eventually.of_forall fun a ↦ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
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))
have 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))
Tactic: refine Filter.Eventually.of_forall fun a ↦ ?_