awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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_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ξm : Measurable ξ
hξle : ∀ (A : Set α) (hA : MeasurableSet A), ∫⁻ (a : α) in A, ξ a ∂ν ≤ (μ : (a : Set α) → ℝ≥0∞) A
hle : ν.withDensity ξ ≤ μ
this : IsFiniteMeasure (ν.withDensity ξ)
μ₁ : Measure α := μ - ν.withDensity ξ
hμ₁ : μ₁ = μ - ν.withDensity ξ
h : ¬(μ₁, ξ).1 ⟂ₘ ν
ε : ℝ≥0
hε₁ : 0 < ε
E : Set α
hE₁ : MeasurableSet E
hE₂ : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) E : ℝ≥0∞)
hE₃ :
  ∀ (A : Set α),
    MeasurableSet A →
      HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (A ∩ E) : ℝ≥0∞) ≤
        (μ - ν.withDensity ξ : (a : Set α) → ℝ≥0∞) (A ∩ E)
hε₂ : ∀ (A : Set α) (hA : MeasurableSet A), ∫⁻ (a : α) in A ∩ E, (↑ε : ℝ≥0∞) + ξ a ∂ν ≤ (μ : (a : Set α) → ℝ≥0∞) (A ∩ E)
A : Set α
hA : MeasurableSet A
⊢ ∫⁻ (a : α) in A, HAdd.hAdd (β := (x : α) → ℝ≥0∞) ξ (E.indicator fun (x : α) ↦ (↑ε : ℝ≥0∞)) a ∂ν =
    ∫⁻ (a : α) in A ∩ E, (↑ε : ℝ≥0∞) + ξ a ∂ν + ∫⁻ (a : α) in A \ E, ξ a ∂ν
have simp : ∫⁻ (a : α) in A, ξ a ∂ν + HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (E ∩ A) : ℝ≥0∞) =
  HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (A ∩ E) : ℝ≥0∞) + ∫⁻ (a : α) in A, ξ a ∂ν
Tactic: simp only [lintegral_add_left measurable_const, lintegral_add_left hξm,
            setLIntegral_const, add_assoc, lintegral_inter_add_diff _ _ hE₁, Pi.add_apply,
            lintegral_indicator hE₁, restrict_apply hE₁]
-- 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_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ξm : Measurable ξ
hξle : ∀ (A : Set α) (hA : MeasurableSet A), ∫⁻ (a : α) in A, ξ a ∂ν ≤ (μ : (a : Set α) → ℝ≥0∞) A
hle : ν.withDensity ξ ≤ μ
this : IsFiniteMeasure (ν.withDensity ξ)
μ₁ : Measure α := μ - ν.withDensity ξ
hμ₁ : μ₁ = μ - ν.withDensity ξ
h : ¬(μ₁, ξ).1 ⟂ₘ ν
ε : ℝ≥0
hε₁ : 0 < ε
E : Set α
hE₁ : MeasurableSet E
hE₂ : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) E : ℝ≥0∞)
hE₃ :
  ∀ (A : Set α),
    MeasurableSet A →
      HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (A ∩ E) : ℝ≥0∞) ≤
        (μ - ν.withDensity ξ : (a : Set α) → ℝ≥0∞) (A ∩ E)
hε₂ : ∀ (A : Set α) (hA : MeasurableSet A), ∫⁻ (a : α) in A ∩ E, (↑ε : ℝ≥0∞) + ξ a ∂ν ≤ (μ : (a : Set α) → ℝ≥0∞) (A ∩ E)
A : Set α
hA : MeasurableSet A
⊢ ∫⁻ (a : α) in A, ξ a ∂ν + HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (E ∩ A) : ℝ≥0∞) =
    HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (A ∩ E) : ℝ≥0∞) + ∫⁻ (a : α) in A, ξ a ∂ν
have rw : ∫⁻ (a : α) in A, ξ a ∂ν + HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (A ∩ E) : ℝ≥0∞) =
  HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (A ∩ E) : ℝ≥0∞) + ∫⁻ (a : α) in A, ξ a ∂ν
Tactic: rw [inter_comm, add_comm]
-- 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_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ξm : Measurable ξ
hξle : ∀ (A : Set α) (hA : MeasurableSet A), ∫⁻ (a : α) in A, ξ a ∂ν ≤ (μ : (a : Set α) → ℝ≥0∞) A
hle : ν.withDensity ξ ≤ μ
this : IsFiniteMeasure (ν.withDensity ξ)
μ₁ : Measure α := μ - ν.withDensity ξ
hμ₁ : μ₁ = μ - ν.withDensity ξ
h : ¬(μ₁, ξ).1 ⟂ₘ ν
ε : ℝ≥0
hε₁ : 0 < ε
E : Set α
hE₁ : MeasurableSet E
hE₂ : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) E : ℝ≥0∞)
hE₃ :
  ∀ (A : Set α),
    MeasurableSet A →
      HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (A ∩ E) : ℝ≥0∞) ≤
        (μ - ν.withDensity ξ : (a : Set α) → ℝ≥0∞) (A ∩ E)
hε₂ : ∀ (A : Set α) (hA : MeasurableSet A), ∫⁻ (a : α) in A ∩ E, (↑ε : ℝ≥0∞) + ξ a ∂ν ≤ (μ : (a : Set α) → ℝ≥0∞) (A ∩ E)
A : Set α
hA : MeasurableSet A
rw :
  ∫⁻ (a : α) in A, ξ a ∂ν + HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (A ∩ E) : ℝ≥0∞) =
    HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (A ∩ E) : ℝ≥0∞) + ∫⁻ (a : α) in A, ξ a ∂ν
⊢ ∫⁻ (a : α) in A, ξ a ∂ν + HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (E ∩ A) : ℝ≥0∞) =
    HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (A ∩ E) : ℝ≥0∞) + ∫⁻ (a : α) in A, ξ a ∂ν
have rw₁ : HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (A ∩ E) : ℝ≥0∞) + ∫⁻ (a : α) in A, ξ a ∂ν =
  HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (A ∩ E) : ℝ≥0∞) + ∫⁻ (a : α) in A, ξ a ∂ν
Tactic: rw [inter_comm, add_comm]
-- 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_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ξm : Measurable ξ
hξle : ∀ (A : Set α) (hA : MeasurableSet A), ∫⁻ (a : α) in A, ξ a ∂ν ≤ (μ : (a : Set α) → ℝ≥0∞) A
hle : ν.withDensity ξ ≤ μ
this : IsFiniteMeasure (ν.withDensity ξ)
μ₁ : Measure α := μ - ν.withDensity ξ
hμ₁ : μ₁ = μ - ν.withDensity ξ
h : ¬(μ₁, ξ).1 ⟂ₘ ν
ε : ℝ≥0
hε₁ : 0 < ε
E : Set α
hE₁ : MeasurableSet E
hE₂ : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) E : ℝ≥0∞)
hE₃ :
  ∀ (A : Set α),
    MeasurableSet A →
      HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (A ∩ E) : ℝ≥0∞) ≤
        (μ - ν.withDensity ξ : (a : Set α) → ℝ≥0∞) (A ∩ E)
hε₂ : ∀ (A : Set α) (hA : MeasurableSet A), ∫⁻ (a : α) in A ∩ E, (↑ε : ℝ≥0∞) + ξ a ∂ν ≤ (μ : (a : Set α) → ℝ≥0∞) (A ∩ E)
A : Set α
hA : MeasurableSet A
⊢ ∫⁻ (x : α) in A, HAdd.hAdd (β := (x : α) → ℝ≥0∞) ξ (E.indicator fun (x : α) ↦ (↑ε : ℝ≥0∞)) x ∂ν ≤
    (μ : (a : Set α) → ℝ≥0∞) A
have this₁ : ∫⁻ (a : α) in A, HAdd.hAdd (β := (x : α) → ℝ≥0∞) ξ (E.indicator fun (x : α) ↦ (↑ε : ℝ≥0∞)) a ∂ν =
  ∫⁻ (a : α) in A ∩ E, (↑ε : ℝ≥0∞) + ξ a ∂ν + ∫⁻ (a : α) in A \ E, ξ a ∂ν
Tactic: have : ∫⁻ a in A, (ξ + E.indicator fun _ ↦ (ε : ℝ≥0∞)) a ∂ν =
            ∫⁻ a in A ∩ E, ε + ξ a ∂ν + ∫⁻ a in A \ E, ξ a ∂ν := by
          simp only [lintegral_add_left measurable_const, lintegral_add_left hξm,
            setLIntegral_const, add_assoc, lintegral_inter_add_diff _ _ hE₁, Pi.add_apply,
            lintegral_indicator hE₁, restrict_apply hE₁]
          rw [inter_comm, add_comm]
-- 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_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ξm : Measurable ξ
hξle : ∀ (A : Set α) (hA : MeasurableSet A), ∫⁻ (a : α) in A, ξ a ∂ν ≤ (μ : (a : Set α) → ℝ≥0∞) A
hle : ν.withDensity ξ ≤ μ
this_1 : IsFiniteMeasure (ν.withDensity ξ)
μ₁ : Measure α := μ - ν.withDensity ξ
hμ₁ : μ₁ = μ - ν.withDensity ξ
h : ¬(μ₁, ξ).1 ⟂ₘ ν
ε : ℝ≥0
hε₁ : 0 < ε
E : Set α
hE₁ : MeasurableSet E
hE₂ : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) E : ℝ≥0∞)
hE₃ :
  ∀ (A : Set α),
    MeasurableSet A →
      HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (A ∩ E) : ℝ≥0∞) ≤
        (μ - ν.withDensity ξ : (a : Set α) → ℝ≥0∞) (A ∩ E)
hε₂ : ∀ (A : Set α) (hA : MeasurableSet A), ∫⁻ (a : α) in A ∩ E, (↑ε : ℝ≥0∞) + ξ a ∂ν ≤ (μ : (a : Set α) → ℝ≥0∞) (A ∩ E)
A : Set α
hA : MeasurableSet A
this :
  ∫⁻ (a : α) in A, HAdd.hAdd (β := (x : α) → ℝ≥0∞) ξ (E.indicator fun (x : α) ↦ (↑ε : ℝ≥0∞)) a ∂ν =
    ∫⁻ (a : α) in A ∩ E, (↑ε : ℝ≥0∞) + ξ a ∂ν + ∫⁻ (a : α) in A \ E, ξ a ∂ν
⊢ ∫⁻ (x : α) in A, HAdd.hAdd (β := (x : α) → ℝ≥0∞) ξ (E.indicator fun (x : α) ↦ (↑ε : ℝ≥0∞)) x ∂ν ≤
    (μ : (a : Set α) → ℝ≥0∞) A
have rw : ∫⁻ (a : α) in A ∩ E, (↑ε : ℝ≥0∞) + ξ a ∂ν + ∫⁻ (a : α) in A \ E, ξ a ∂ν ≤
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (A ∩ E) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (A \ E) : ℝ≥0∞)
Tactic: rw [this, ← measure_inter_add_diff A hE₁]
-- 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_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ξm : Measurable ξ
hξle : ∀ (A : Set α) (hA : MeasurableSet A), ∫⁻ (a : α) in A, ξ a ∂ν ≤ (μ : (a : Set α) → ℝ≥0∞) A
hle : ν.withDensity ξ ≤ μ
this : IsFiniteMeasure (ν.withDensity ξ)
μ₁ : Measure α := μ - ν.withDensity ξ
hμ₁ : μ₁ = μ - ν.withDensity ξ
h : ¬(μ₁, ξ).1 ⟂ₘ ν
ε : ℝ≥0
hε₁ : 0 < ε
E : Set α
hE₁ : MeasurableSet E
hE₂ : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) E : ℝ≥0∞)
hE₃ :
  ∀ (A : Set α),
    MeasurableSet A →
      HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (A ∩ E) : ℝ≥0∞) ≤
        (μ - ν.withDensity ξ : (a : Set α) → ℝ≥0∞) (A ∩ E)
hε₂ : ∀ (A : Set α) (hA : MeasurableSet A), ∫⁻ (a : α) in A ∩ E, (↑ε : ℝ≥0∞) + ξ a ∂ν ≤ (μ : (a : Set α) → ℝ≥0∞) (A ∩ E)
⊢ False
have hξε : (ξ + E.indicator fun (x : α) ↦ (↑ε : ℝ≥0∞)) ∈ measurableLE ν μ
Tactic: have hξε : (ξ + E.indicator fun _ ↦ (ε : ℝ≥0∞)) ∈ measurableLE ν μ := by
        refine ⟨hξm.add (measurable_const.indicator hE₁), fun A hA ↦ ?_⟩
        have : ∫⁻ a in A, (ξ + E.indicator fun _ ↦ (ε : ℝ≥0∞)) a ∂ν =
            ∫⁻ a in A ∩ E, ε + ξ a ∂ν + ∫⁻ a in A \ E, ξ a ∂ν := by
          simp only [lintegral_add_left measurable_const, lintegral_add_left hξm,
            setLIntegral_const, add_assoc, lintegral_inter_add_diff _ _ hE₁, Pi.add_apply,
            lintegral_indicator hE₁, restrict_apply hE₁]
          rw [inter_comm, add_comm]
        rw [this, ← measure_inter_add_diff A hE₁]
        exact add_le_add (hε₂ A hA) (hξle (A \ E) (hA.diff hE₁))
-- 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_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ξm : Measurable ξ
hξle : ∀ (A : Set α) (hA : MeasurableSet A), ∫⁻ (a : α) in A, ξ a ∂ν ≤ (μ : (a : Set α) → ℝ≥0∞) A
hle : ν.withDensity ξ ≤ μ
this : IsFiniteMeasure (ν.withDensity ξ)
μ₁ : Measure α := μ - ν.withDensity ξ
hμ₁ : μ₁ = μ - ν.withDensity ξ
h : ¬(μ₁, ξ).1 ⟂ₘ ν
ε : ℝ≥0
hε₁ : 0 < ε
E : Set α
hE₁ : MeasurableSet E
hE₂ : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) E : ℝ≥0∞)
hE₃ :
  ∀ (A : Set α),
    MeasurableSet A →
      HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (A ∩ E) : ℝ≥0∞) ≤
        (μ - ν.withDensity ξ : (a : Set α) → ℝ≥0∞) (A ∩ E)
hε₂ : ∀ (A : Set α) (hA : MeasurableSet A), ∫⁻ (a : α) in A ∩ E, (↑ε : ℝ≥0∞) + ξ a ∂ν ≤ (μ : (a : Set α) → ℝ≥0∞) (A ∩ E)
hξε : (ξ + E.indicator fun (x : α) ↦ (↑ε : ℝ≥0∞)) ∈ measurableLE ν μ
⊢ False
have this₁ : ∫⁻ (a : α), ξ a + E.indicator (fun (x : α) ↦ (↑ε : ℝ≥0∞)) a ∂ν ≤ sSup (measurableLEEval ν μ)
Tactic: have : (∫⁻ a, ξ a + E.indicator (fun _ ↦ (ε : ℝ≥0∞)) a ∂ν) ≤ sSup (measurableLEEval ν μ) :=
        le_sSup ⟨ξ + E.indicator fun _ ↦ (ε : ℝ≥0∞), hξε, 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_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ξm : Measurable ξ
hξle : ∀ (A : Set α) (hA : MeasurableSet A), ∫⁻ (a : α) in A, ξ a ∂ν ≤ (μ : (a : Set α) → ℝ≥0∞) A
hle : ν.withDensity ξ ≤ μ
this_1 : IsFiniteMeasure (ν.withDensity ξ)
μ₁ : Measure α := μ - ν.withDensity ξ
hμ₁ : μ₁ = μ - ν.withDensity ξ
h : ¬(μ₁, ξ).1 ⟂ₘ ν
ε : ℝ≥0
hε₁ : 0 < ε
E : Set α
hE₁ : MeasurableSet E
hE₂ : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) E : ℝ≥0∞)
hE₃ :
  ∀ (A : Set α),
    MeasurableSet A →
      HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (A ∩ E) : ℝ≥0∞) ≤
        (μ - ν.withDensity ξ : (a : Set α) → ℝ≥0∞) (A ∩ E)
hε₂ : ∀ (A : Set α) (hA : MeasurableSet A), ∫⁻ (a : α) in A ∩ E, (↑ε : ℝ≥0∞) + ξ a ∂ν ≤ (μ : (a : Set α) → ℝ≥0∞) (A ∩ E)
hξε : (ξ + E.indicator fun (x : α) ↦ (↑ε : ℝ≥0∞)) ∈ measurableLE ν μ
this : ∫⁻ (a : α), ξ a + E.indicator (fun (x : α) ↦ (↑ε : ℝ≥0∞)) a ∂ν ≤ sSup (measurableLEEval ν μ)
⊢ False
have refine_1 : sSup (measurableLEEval ν μ) < ∫⁻ (a : α), ξ a + E.indicator (fun (x : α) ↦ (↑ε : ℝ≥0∞)) a ∂ν
Tactic: refine not_lt.2 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_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ξm : Measurable ξ
hξle : ∀ (A : Set α) (hA : MeasurableSet A), ∫⁻ (a : α) in A, ξ a ∂ν ≤ (μ : (a : Set α) → ℝ≥0∞) A
hle : ν.withDensity ξ ≤ μ
this_1 : IsFiniteMeasure (ν.withDensity ξ)
μ₁ : Measure α := μ - ν.withDensity ξ
hμ₁ : μ₁ = μ - ν.withDensity ξ
h : ¬(μ₁, ξ).1 ⟂ₘ ν
ε : ℝ≥0
hε₁ : 0 < ε
E : Set α
hE₁ : MeasurableSet E
hE₂ : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) E : ℝ≥0∞)
hE₃ :
  ∀ (A : Set α),
    MeasurableSet A →
      HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (A ∩ E) : ℝ≥0∞) ≤
        (μ - ν.withDensity ξ : (a : Set α) → ℝ≥0∞) (A ∩ E)
hε₂ : ∀ (A : Set α) (hA : MeasurableSet A), ∫⁻ (a : α) in A ∩ E, (↑ε : ℝ≥0∞) + ξ a ∂ν ≤ (μ : (a : Set α) → ℝ≥0∞) (A ∩ E)
hξε : (ξ + E.indicator fun (x : α) ↦ (↑ε : ℝ≥0∞)) ∈ measurableLE ν μ
this : ∫⁻ (a : α), ξ a + E.indicator (fun (x : α) ↦ (↑ε : ℝ≥0∞)) a ∂ν ≤ sSup (measurableLEEval ν μ)
⊢ sSup (measurableLEEval ν μ) < ∫⁻ (a : α), ξ a + E.indicator (fun (x : α) ↦ (↑ε : ℝ≥0∞)) a ∂ν
have refine_1 : ∫⁻ (a : α), ξ a ∂ν < ∫⁻ (a : α), ξ a ∂ν + HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) E : ℝ≥0∞)
Tactic: rw [hξ₁, lintegral_add_left hξm, lintegral_indicator hE₁, setLIntegral_const]
-- 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_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ξm : Measurable ξ
hξle : ∀ (A : Set α) (hA : MeasurableSet A), ∫⁻ (a : α) in A, ξ a ∂ν ≤ (μ : (a : Set α) → ℝ≥0∞) A
hle : ν.withDensity ξ ≤ μ
this_1 : IsFiniteMeasure (ν.withDensity ξ)
μ₁ : Measure α := μ - ν.withDensity ξ
hμ₁ : μ₁ = μ - ν.withDensity ξ
h : ¬(μ₁, ξ).1 ⟂ₘ ν
ε : ℝ≥0
hε₁ : 0 < ε
E : Set α
hE₁ : MeasurableSet E
hE₂ : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) E : ℝ≥0∞)
hE₃ :
  ∀ (A : Set α),
    MeasurableSet A →
      HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (A ∩ E) : ℝ≥0∞) ≤
        (μ - ν.withDensity ξ : (a : Set α) → ℝ≥0∞) (A ∩ E)
hε₂ : ∀ (A : Set α) (hA : MeasurableSet A), ∫⁻ (a : α) in A ∩ E, (↑ε : ℝ≥0∞) + ξ a ∂ν ≤ (μ : (a : Set α) → ℝ≥0∞) (A ∩ E)
hξε : (ξ + E.indicator fun (x : α) ↦ (↑ε : ℝ≥0∞)) ∈ measurableLE ν μ
this : ∫⁻ (a : α), ξ a + E.indicator (fun (x : α) ↦ (↑ε : ℝ≥0∞)) a ∂ν ≤ sSup (measurableLEEval ν μ)
⊢ ∫⁻ (a : α), ξ a ∂ν < ∫⁻ (a : α), ξ a ∂ν + HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) E : ℝ≥0∞)
have refine_1 : ∫⁻ (a : α), ξ a ∂ν ≠ ∞
Tactic: refine ENNReal.lt_add_right ?_ (ENNReal.mul_pos_iff.2 ⟨ENNReal.coe_pos.2 hε₁, hE₂⟩).ne'
-- 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_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ξm : Measurable ξ
hξle : ∀ (A : Set α) (hA : MeasurableSet A), ∫⁻ (a : α) in A, ξ a ∂ν ≤ (μ : (a : Set α) → ℝ≥0∞) A
hle : ν.withDensity ξ ≤ μ
this_1 : IsFiniteMeasure (ν.withDensity ξ)
μ₁ : Measure α := μ - ν.withDensity ξ
hμ₁ : μ₁ = μ - ν.withDensity ξ
h : ¬(μ₁, ξ).1 ⟂ₘ ν
ε : ℝ≥0
hε₁ : 0 < ε
E : Set α
hE₁ : MeasurableSet E
hE₂ : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) E : ℝ≥0∞)
hE₃ :
  ∀ (A : Set α),
    MeasurableSet A →
      HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (A ∩ E) : ℝ≥0∞) ≤
        (μ - ν.withDensity ξ : (a : Set α) → ℝ≥0∞) (A ∩ E)
hε₂ : ∀ (A : Set α) (hA : MeasurableSet A), ∫⁻ (a : α) in A ∩ E, (↑ε : ℝ≥0∞) + ξ a ∂ν ≤ (μ : (a : Set α) → ℝ≥0∞) (A ∩ E)
hξε : (ξ + E.indicator fun (x : α) ↦ (↑ε : ℝ≥0∞)) ∈ measurableLE ν μ
this : ∫⁻ (a : α), ξ a + E.indicator (fun (x : α) ↦ (↑ε : ℝ≥0∞)) a ∂ν ≤ sSup (measurableLEEval ν μ)
⊢ ∫⁻ (a : α), ξ a ∂ν ≠ ∞
have this₁ : Ne (α := ℝ≥0∞) ((ν.withDensity ξ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: have := measure_ne_top (ν.withDensity ξ) univ
-- 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_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ξm : Measurable ξ
hξle : ∀ (A : Set α) (hA : MeasurableSet A), ∫⁻ (a : α) in A, ξ a ∂ν ≤ (μ : (a : Set α) → ℝ≥0∞) A
hle : ν.withDensity ξ ≤ μ
this_1 : IsFiniteMeasure (ν.withDensity ξ)
μ₁ : Measure α := μ - ν.withDensity ξ
hμ₁ : μ₁ = μ - ν.withDensity ξ
h : ¬(μ₁, ξ).1 ⟂ₘ ν
ε : ℝ≥0
hε₁ : 0 < ε
E : Set α
hE₁ : MeasurableSet E
hE₂ : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) E : ℝ≥0∞)
hE₃ :
  ∀ (A : Set α),
    MeasurableSet A →
      HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (A ∩ E) : ℝ≥0∞) ≤
        (μ - ν.withDensity ξ : (a : Set α) → ℝ≥0∞) (A ∩ E)
hε₂ : ∀ (A : Set α) (hA : MeasurableSet A), ∫⁻ (a : α) in A ∩ E, (↑ε : ℝ≥0∞) + ξ a ∂ν ≤ (μ : (a : Set α) → ℝ≥0∞) (A ∩ E)
hξε : (ξ + E.indicator fun (x : α) ↦ (↑ε : ℝ≥0∞)) ∈ measurableLE ν μ
this_2 : ∫⁻ (a : α), ξ a + E.indicator (fun (x : α) ↦ (↑ε : ℝ≥0∞)) a ∂ν ≤ sSup (measurableLEEval ν μ)
this : Ne (α := ℝ≥0∞) ((ν.withDensity ξ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ∫⁻ (a : α), ξ a ∂ν ≠ ∞
have refine_1 : ∀ (this : ∫⁻ (a : α) in univ, ξ a ∂ν ≠ ∞), ∫⁻ (a : α), ξ a ∂ν ≠ ∞
Tactic: rwa [withDensity_apply _ MeasurableSet.univ, Measure.restrict_univ] at this
Cleared hypotheses: 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_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ξm : Measurable ξ
hξle : ∀ (A : Set α) (hA : MeasurableSet A), ∫⁻ (a : α) in A, ξ a ∂ν ≤ (μ : (a : Set α) → ℝ≥0∞) A
hle : ν.withDensity ξ ≤ μ
this_1 : IsFiniteMeasure (ν.withDensity ξ)
μ₁ : Measure α := μ - ν.withDensity ξ
hμ₁ : μ₁ = μ - ν.withDensity ξ
h : ¬(μ₁, ξ).1 ⟂ₘ ν
ε : ℝ≥0
hε₁ : 0 < ε
E : Set α
hE₁ : MeasurableSet E
hE₂ : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) E : ℝ≥0∞)
hE₃ :
  ∀ (A : Set α),
    MeasurableSet A →
      HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (A ∩ E) : ℝ≥0∞) ≤
        (μ - ν.withDensity ξ : (a : Set α) → ℝ≥0∞) (A ∩ E)
hε₂ : ∀ (A : Set α) (hA : MeasurableSet A), ∫⁻ (a : α) in A ∩ E, (↑ε : ℝ≥0∞) + ξ a ∂ν ≤ (μ : (a : Set α) → ℝ≥0∞) (A ∩ E)
hξε : (ξ + E.indicator fun (x : α) ↦ (↑ε : ℝ≥0∞)) ∈ measurableLE ν μ
this_2 : ∫⁻ (a : α), ξ a + E.indicator (fun (x : α) ↦ (↑ε : ℝ≥0∞)) a ∂ν ≤ sSup (measurableLEEval ν μ)
this : Ne (α := ℝ≥0∞) ((ν.withDensity ξ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)
refine_1 : ∀ (this : ∫⁻ (a : α) in univ, ξ a ∂ν ≠ ∞), ∫⁻ (a : α), ξ a ∂ν ≠ ∞
⊢ ∫⁻ (a : α), ξ a ∂ν ≠ ∞
have refine_1₁ : ∀ (this : ∫⁻ (a : α), ξ a ∂ν ≠ ∞), ∫⁻ (a : α), ξ a ∂ν ≠ ∞
Tactic: rwa [withDensity_apply _ MeasurableSet.univ, Measure.restrict_univ] at this
Cleared hypotheses: this