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_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)
⊢ ∀ (A : Set α) (hA : MeasurableSet A), ∫⁻ (a : α) in A ∩ E, (↑ε : ℝ≥0∞) + ξ a ∂ν ≤ (μ : (a : Set α) → ℝ≥0∞) (A ∩ E)

Tactic:
have hε₂ (A : Set α) (hA : MeasurableSet A) : ∫⁻ a in A ∩ E, ε + ξ a ∂ν ≤ μ (A ∩ E) := by
        specialize hE₃ A hA
        rw [lintegral_add_left measurable_const, lintegral_const, restrict_apply_univ]
        rw [Measure.sub_apply (hA.inter hE₁) hle, withDensity_apply _ (hA.inter hE₁)] at hE₃
        refine add_le_of_le_tsub_right_of_le (hξle _ (hA.inter hE₁)) hE₃
-- 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ξ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)
⊢ (ξ + E.indicator fun (x : α) ↦ (↑ε : ℝ≥0∞)) ∈ measurableLE ν μ

Tactic:
⟨hξm.add (measurable_const.indicator hE₁), fun A hA ↦ ?_⟩

Premises used: Set.Mem, setOf, Measurable.add, Measurable.indicator, And.intro, measurable_const, MeasureTheory.Measure.LebesgueDecomposition.measurableLE
-- 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ξ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)
refine :
  ∀ (A : Set α) (hA : MeasurableSet A),
    ∫⁻ (x : α) in A, HAdd.hAdd (β := (x : α) → ℝ≥0∞) ξ (E.indicator fun (x : α) ↦ (↑ε : ℝ≥0∞)) x ∂ν ≤
      (μ : (a : Set α) → ℝ≥0∞) A
⊢ (ξ + E.indicator fun (x : α) ↦ (↑ε : ℝ≥0∞)) ∈ measurableLE ν μ

Tactic:
refine ⟨hξm.add (measurable_const.indicator hE₁), fun A hA ↦ ?_⟩
-- 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ξ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
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 ∂ν
⊢ ∫⁻ (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:
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₁]

Premises used: add_assoc, MeasureTheory.Measure.restrict_apply, MeasureTheory.lintegral_inter_add_diff, MeasureTheory.lintegral_add_left, Pi.add_apply, MeasureTheory.lintegral_indicator, MeasureTheory.setLIntegral_const, measurable_const
-- 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ξ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 ∂ν
rw₁ 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 ∂ν
⊢ ∫⁻ (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:
rw [inter_comm, add_comm]

Premises used: add_comm, Set.inter_comm
-- 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ξ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 ∂ν

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]
-- 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ξ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 ∂ν
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∞)
⊢ ∫⁻ (x : α) in A, HAdd.hAdd (β := (x : α) → ℝ≥0∞) ξ (E.indicator fun (x : α) ↦ (↑ε : ℝ≥0∞)) x ∂ν ≤
    (μ : (a : Set α) → ℝ≥0∞) A

Tactic:
rw [this, ← measure_inter_add_diff A hE₁]

Premises used: MeasureTheory.measure_inter_add_diff
-- 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ξ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 ∂ν
⊢ ∫⁻ (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:
add_le_add (hε₂ A hA) (hξle (A \ E) (hA.diff hE₁))

Premises used: MeasurableSet.diff, add_le_add, SDiff.sdiff
-- 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ξ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 ∂ν
⊢ ∫⁻ (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:
exact add_le_add (hε₂ A hA) (hξle (A \ E) (hA.diff hE₁))

Premises used: MeasurableSet.diff, add_le_add, SDiff.sdiff
-- 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ξ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)
⊢ (ξ + 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₁))
-- 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ξ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 ν μ
⊢ ∫⁻ (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⟩
-- 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ξ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

Tactic:
not_lt.2 this ?_

Premises used: Iff.mpr, not_lt
-- 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ξ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 ν μ)
refine_1 : sSup (measurableLEEval ν μ) < ∫⁻ (a : α), ξ a + E.indicator (fun (x : α) ↦ (↑ε : ℝ≥0∞)) a ∂ν
⊢ False

Tactic:
refine not_lt.2 this ?_

Premises used: Iff.mpr, not_lt