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_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 :
  ∫⁻ (a : α), ξ a ∂ν < ∫⁻ (a : α), ξ a ∂ν + HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) E : ℝ≥0∞)
⊢ sSup (measurableLEEval ν μ) < ∫⁻ (a : α), ξ a + E.indicator (fun (x : α) ↦ (↑ε : ℝ≥0∞)) a ∂ν

Tactic:
rw [hξ₁, lintegral_add_left hξm, lintegral_indicator hE₁, setLIntegral_const]

Premises used: MeasureTheory.lintegral_add_left, MeasureTheory.lintegral_indicator, MeasureTheory.setLIntegral_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_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∞)

Tactic:
ENNReal.lt_add_right ?_ (ENNReal.mul_pos_iff.2 ⟨ENNReal.coe_pos.2 hε₁, hE₂⟩).ne'

Premises used: Iff.mpr, ENNReal.lt_add_right, LT.lt.ne', ENNReal.coe_pos, And.intro, ENNReal.mul_pos_iff
-- 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 : ∫⁻ (a : α), ξ a ∂ν ≠ ∞
⊢ ∫⁻ (a : α), ξ a ∂ν < ∫⁻ (a : α), ξ a ∂ν + HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) E : ℝ≥0∞)

Tactic:
refine ENNReal.lt_add_right ?_ (ENNReal.mul_pos_iff.2 ⟨ENNReal.coe_pos.2 hε₁, hE₂⟩).ne'

Premises used: Iff.mpr, ENNReal.lt_add_right, LT.lt.ne', ENNReal.coe_pos, And.intro, ENNReal.mul_pos_iff
-- 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 ν μ)
⊢ Ne (α := ℝ≥0∞) ((ν.withDensity ξ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
have := measure_ne_top (ν.withDensity ξ) univ
-- 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_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 ∂ν ≠ ∞
refine_1₁ refine_1₂ refine_1₃ refine_1₄ : ∀ (this : ∫⁻ (a : α), ξ a ∂ν ≠ ∞), ∫⁻ (a : α), ξ a ∂ν ≠ ∞
⊢ ∫⁻ (a : α), ξ a ∂ν ≠ ∞

Tactic:
rwa [withDensity_apply _ MeasurableSet.univ, Measure.restrict_univ] at this

Premises used: MeasurableSet.univ, MeasureTheory.withDensity_apply, MeasureTheory.Measure.restrict_univ
-- 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 ξ
hξle : ∀ (A : Set α) (hA : MeasurableSet A), ∫⁻ (a : α) in A, ξ a ∂ν ≤ (μ : (a : Set α) → ℝ≥0∞) A
hle : ν.withDensity ξ ≤ μ
this : IsFiniteMeasure (ν.withDensity ξ)
μ₁ : Measure α := μ - ν.withDensity ξ
hμ₁ : μ₁ = μ - ν.withDensity ξ
refine_2 : μ = (μ - ν.withDensity ξ, ξ).1 + ν.withDensity (μ - ν.withDensity ξ, ξ).2
⊢ μ = (μ₁, ξ).1 + ν.withDensity (μ₁, ξ).2

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 ξ
hξle : ∀ (A : Set α) (hA : MeasurableSet A), ∫⁻ (a : α) in A, ξ a ∂ν ≤ (μ : (a : Set α) → ℝ≥0∞) A
hle : ν.withDensity ξ ≤ μ
this : IsFiniteMeasure (ν.withDensity ξ)
μ₁ : Measure α := μ - ν.withDensity ξ
hμ₁ : μ₁ = μ - ν.withDensity ξ
refine_2 :
  ∀ (A : Set α) (hA : MeasurableSet A),
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)
      (((μ - ν.withDensity ξ, ξ).1 + ν.withDensity (μ - ν.withDensity ξ, ξ).2 : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)
⊢ μ = (μ - ν.withDensity ξ, ξ).1 + ν.withDensity (μ - ν.withDensity ξ, ξ).2

Tactic:
ext1 A hA
-- 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 ξ
hξle : ∀ (A : Set α) (hA : MeasurableSet A), ∫⁻ (a : α) in A, ξ a ∂ν ≤ (μ : (a : Set α) → ℝ≥0∞) A
hle : ν.withDensity ξ ≤ μ
this : IsFiniteMeasure (ν.withDensity ξ)
μ₁ : Measure α := μ - ν.withDensity ξ
hμ₁ : μ₁ = μ - ν.withDensity ξ
A : Set α
hA : MeasurableSet A
refine_2 :
  (μ : (a : Set α) → ℝ≥0∞) A =
    HAdd.hAdd (α := (a : Set α) → ℝ≥0∞) (β := (a : Set α) → ℝ≥0∞) (⇑(μ - ν.withDensity ξ, ξ).1 : (a : Set α) → ℝ≥0∞)
      (⇑(ν.withDensity (μ - ν.withDensity ξ, ξ).2) : (a : Set α) → ℝ≥0∞) A
refine_2₁ :
  (μ : (a : Set α) → ℝ≥0∞) A =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) (((μ - ν.withDensity ξ, ξ).1 : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)
      ((ν.withDensity (μ - ν.withDensity ξ, ξ).2 : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)
refine_2₂ :
  (μ : (a : Set α) → ℝ≥0∞) A =
    HAdd.hAdd (β := ℝ≥0∞)
      (HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)
        ((ν.withDensity ξ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞))
      ((ν.withDensity (μ - ν.withDensity ξ, ξ).2 : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)
refine_2₃ :
  (μ : (a : Set α) → ℝ≥0∞) A =
    HAdd.hAdd (α := ℝ≥0∞) ((ν.withDensity (μ - ν.withDensity ξ, ξ).2 : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)
      (HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)
        ((ν.withDensity ξ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞))
refine_2₄ refine_2₅ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)
    (((μ - ν.withDensity ξ, ξ).1 + ν.withDensity (μ - ν.withDensity ξ, ξ).2 : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)

Tactic:
rw [Measure.coe_add, Pi.add_apply, Measure.sub_apply hA hle, add_comm,
        add_tsub_cancel_of_le (hle A)]

Premises used: MeasureTheory.Measure.coe_add, add_comm, Pi.add_apply, MeasureTheory.Measure.sub_apply, add_tsub_cancel_of_le
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : SFinite μ
_h : ∀ (μ : Measure α) [IsFiniteMeasure μ], μ.HaveLebesgueDecomposition ν
⊢ μ.HaveLebesgueDecomposition ν

Tactic:
sum_sfiniteSeq μ ▸ sum_left _

Premises used: Eq.rec, MeasureTheory.sum_sfiniteSeq, MeasureTheory.Measure.HaveLebesgueDecomposition.sum_left
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : SFinite μ
inst_1 : SigmaFinite ν
inr :
  ∀ (this : ∀ (μ : Measure α) [SFinite μ] (hμ : IsFiniteMeasure μ), μ.HaveLebesgueDecomposition ν)
    (hμ : ¬IsFiniteMeasure μ), μ.HaveLebesgueDecomposition ν
wlog : ∀ (μ : Measure α) [SFinite μ] (hμ : IsFiniteMeasure μ), μ.HaveLebesgueDecomposition ν
⊢ μ.HaveLebesgueDecomposition ν

Tactic:
wlog hμ : IsFiniteMeasure μ generalizing μ

Premises used: MeasureTheory.IsFiniteMeasure
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : SFinite μ
inst_1 : SigmaFinite ν
this : ∀ (μ : Measure α) [SFinite μ] (hμ : IsFiniteMeasure μ), μ.HaveLebesgueDecomposition ν
hμ : ¬IsFiniteMeasure μ
⊢ μ.HaveLebesgueDecomposition ν

Tactic:
.sfinite_of_isFiniteMeasure fun μ _ ↦ this μ ‹_›

Premises used: MeasureTheory.Measure.HaveLebesgueDecomposition.sfinite_of_isFiniteMeasure
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : SFinite μ
inst_1 : SigmaFinite ν
this : ∀ (μ : Measure α) [SFinite μ] (hμ : IsFiniteMeasure μ), μ.HaveLebesgueDecomposition ν
hμ : ¬IsFiniteMeasure μ
⊢ μ.HaveLebesgueDecomposition ν

Tactic:
exact .sfinite_of_isFiniteMeasure fun μ _ ↦ this μ ‹_›
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
ν : Measure α
inst : SigmaFinite ν
μ : Measure α
inst_1 : SFinite μ
hμ : IsFiniteMeasure μ
s : ℕ → Set α := disjointed (spanningSets ν)
⊢ ∀ (n : ℕ), MeasurableSet (s n)

Tactic:
have hsm : ∀ n, MeasurableSet (s n) := .disjointed <| measurableSet_spanningSets _
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
ν : Measure α
inst : SigmaFinite ν
μ : Measure α
inst_1 : SFinite μ
hμ : IsFiniteMeasure μ
s : ℕ → Set α := disjointed (spanningSets ν)
hsm : ∀ (n : ℕ), MeasurableSet (s n)
⊢ ∀ (n : ℕ), Fact (LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (s n) : ℝ≥0∞) (∞ : ℝ≥0∞))

Tactic:
have hs : ∀ n, Fact (ν (s n) < ⊤) := fun n ↦
    ⟨lt_of_le_of_lt (measure_mono <| disjointed_le ..) (measure_spanningSets_lt_top ν n)⟩
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
ν : Measure α
inst : SigmaFinite ν
μ : Measure α
inst_1 : SFinite μ
hμ : IsFiniteMeasure μ
s : ℕ → Set α := disjointed (spanningSets ν)
hsm : ∀ (n : ℕ), MeasurableSet (s n)
hs : ∀ (n : ℕ), Fact (LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (s n) : ℝ≥0∞) (∞ : ℝ≥0∞))
ξ : ℕ → Measure α := fun (n : ℕ) ↦ (μ.restrict (s n)).singularPart (ν.restrict (s n))
f : ℕ → α → ℝ≥0∞ := fun (n : ℕ) ↦ (s n).indicator ((μ.restrict (s n)).rnDeriv (ν.restrict (s n)))
n : ℕ
⊢ Measurable (f n)

Tactic:
measurability
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
ν : Measure α
inst : SigmaFinite ν
μ : Measure α
inst_1 : SFinite μ
hμ : IsFiniteMeasure μ
s : ℕ → Set α := disjointed (spanningSets ν)
hsm : ∀ (n : ℕ), MeasurableSet (s n)
hs : ∀ (n : ℕ), Fact (LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (s n) : ℝ≥0∞) (∞ : ℝ≥0∞))
ξ : ℕ → Measure α := fun (n : ℕ) ↦ (μ.restrict (s n)).singularPart (ν.restrict (s n))
f : ℕ → α → ℝ≥0∞ := fun (n : ℕ) ↦ (s n).indicator ((μ.restrict (s n)).rnDeriv (ν.restrict (s n)))
⊢ ∀ (n : ℕ), Measurable (f n)

Tactic:
have hfm (n : ℕ) : Measurable (f n) := by measurability
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
ν : Measure α
inst : SigmaFinite ν
μ : Measure α
inst_1 : SFinite μ
hμ : IsFiniteMeasure μ
s : ℕ → Set α := disjointed (spanningSets ν)
hsm : ∀ (n : ℕ), MeasurableSet (s n)
hs : ∀ (n : ℕ), Fact (LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (s n) : ℝ≥0∞) (∞ : ℝ≥0∞))
ξ : ℕ → Measure α := fun (n : ℕ) ↦ (μ.restrict (s n)).singularPart (ν.restrict (s n))
f : ℕ → α → ℝ≥0∞ := fun (n : ℕ) ↦ (s n).indicator ((μ.restrict (s n)).rnDeriv (ν.restrict (s n)))
hfm : ∀ (n : ℕ), Measurable (f n)
⊢ sum ξ ⟂ₘ ν

Tactic:
MutuallySingular.sum_left.2 fun n ↦ ?_

Premises used: Iff.mpr, MeasureTheory.Measure.MutuallySingular.sum_left
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
ν : Measure α
inst : SigmaFinite ν
μ : Measure α
inst_1 : SFinite μ
hμ : IsFiniteMeasure μ
s : ℕ → Set α := disjointed (spanningSets ν)
hsm : ∀ (n : ℕ), MeasurableSet (s n)
hs : ∀ (n : ℕ), Fact (LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (s n) : ℝ≥0∞) (∞ : ℝ≥0∞))
ξ : ℕ → Measure α := fun (n : ℕ) ↦ (μ.restrict (s n)).singularPart (ν.restrict (s n))
f : ℕ → α → ℝ≥0∞ := fun (n : ℕ) ↦ (s n).indicator ((μ.restrict (s n)).rnDeriv (ν.restrict (s n)))
hfm : ∀ (n : ℕ), Measurable (f n)
refine : ∀ (n : ℕ), ξ n ⟂ₘ ν
⊢ sum ξ ⟂ₘ ν

Tactic:
refine MutuallySingular.sum_left.2 fun n ↦ ?_

Premises used: Iff.mpr, MeasureTheory.Measure.MutuallySingular.sum_left
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
ν : Measure α
inst : SigmaFinite ν
μ : Measure α
inst_1 : SFinite μ
hμ : IsFiniteMeasure μ
s : ℕ → Set α := disjointed (spanningSets ν)
hsm : ∀ (n : ℕ), MeasurableSet (s n)
hs : ∀ (n : ℕ), Fact (LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (s n) : ℝ≥0∞) (∞ : ℝ≥0∞))
ξ : ℕ → Measure α := fun (n : ℕ) ↦ (μ.restrict (s n)).singularPart (ν.restrict (s n))
f : ℕ → α → ℝ≥0∞ := fun (n : ℕ) ↦ (s n).indicator ((μ.restrict (s n)).rnDeriv (ν.restrict (s n)))
hfm : ∀ (n : ℕ), Measurable (f n)
n : ℕ
rw : ξ n ⟂ₘ ν.restrict (s n) + ν.restrict (s n)ᶜ
⊢ ξ n ⟂ₘ ν

Tactic:
rw [← ν.restrict_add_restrict_compl (hsm n)]

Premises used: MeasureTheory.Measure.restrict_add_restrict_compl
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
ν : Measure α
inst : SigmaFinite ν
μ : Measure α
inst_1 : SFinite μ
hμ : IsFiniteMeasure μ
s : ℕ → Set α := disjointed (spanningSets ν)
hsm : ∀ (n : ℕ), MeasurableSet (s n)
hs : ∀ (n : ℕ), Fact (LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (s n) : ℝ≥0∞) (∞ : ℝ≥0∞))
ξ : ℕ → Measure α := fun (n : ℕ) ↦ (μ.restrict (s n)).singularPart (ν.restrict (s n))
f : ℕ → α → ℝ≥0∞ := fun (n : ℕ) ↦ (s n).indicator ((μ.restrict (s n)).rnDeriv (ν.restrict (s n)))
hfm : ∀ (n : ℕ), Measurable (f n)
n : ℕ
⊢ ξ n ⟂ₘ ν.restrict (s n) + ν.restrict (s n)ᶜ

Tactic:
(mutuallySingular_singularPart ..).add_right (.singularPart ?_ _)

Premises used: MeasureTheory.Measure.MutuallySingular.singularPart, MeasureTheory.Measure.MutuallySingular.add_right, MeasureTheory.Measure.mutuallySingular_singularPart
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
ν : Measure α
inst : SigmaFinite ν
μ : Measure α
inst_1 : SFinite μ
hμ : IsFiniteMeasure μ
s : ℕ → Set α := disjointed (spanningSets ν)
hsm : ∀ (n : ℕ), MeasurableSet (s n)
hs : ∀ (n : ℕ), Fact (LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (s n) : ℝ≥0∞) (∞ : ℝ≥0∞))
ξ : ℕ → Measure α := fun (n : ℕ) ↦ (μ.restrict (s n)).singularPart (ν.restrict (s n))
f : ℕ → α → ℝ≥0∞ := fun (n : ℕ) ↦ (s n).indicator ((μ.restrict (s n)).rnDeriv (ν.restrict (s n)))
hfm : ∀ (n : ℕ), Measurable (f n)
n : ℕ
refine : μ.restrict (s n) ⟂ₘ ν.restrict (s n)ᶜ
⊢ ξ n ⟂ₘ ν.restrict (s n) + ν.restrict (s n)ᶜ

Tactic:
refine (mutuallySingular_singularPart ..).add_right (.singularPart ?_ _)

Premises used: MeasureTheory.Measure.MutuallySingular.singularPart, MeasureTheory.Measure.MutuallySingular.add_right, MeasureTheory.Measure.mutuallySingular_singularPart
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
ν : Measure α
inst : SigmaFinite ν
μ : Measure α
inst_1 : SFinite μ
hμ : IsFiniteMeasure μ
s : ℕ → Set α := disjointed (spanningSets ν)
hsm : ∀ (n : ℕ), MeasurableSet (s n)
hs : ∀ (n : ℕ), Fact (LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (s n) : ℝ≥0∞) (∞ : ℝ≥0∞))
ξ : ℕ → Measure α := fun (n : ℕ) ↦ (μ.restrict (s n)).singularPart (ν.restrict (s n))
f : ℕ → α → ℝ≥0∞ := fun (n : ℕ) ↦ (s n).indicator ((μ.restrict (s n)).rnDeriv (ν.restrict (s n)))
hfm : ∀ (n : ℕ), Measurable (f n)
n : ℕ
⊢ μ.restrict (s n) ⟂ₘ ν.restrict (s n)ᶜ

Tactic:
⟨(s n)ᶜ, (hsm n).compl, ?_⟩

Premises used: Compl.compl, MeasurableSet.compl, MeasureTheory.Measure.MutuallySingular, And.intro, Exists.intro
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
ν : Measure α
inst : SigmaFinite ν
μ : Measure α
inst_1 : SFinite μ
hμ : IsFiniteMeasure μ
s : ℕ → Set α := disjointed (spanningSets ν)
hsm : ∀ (n : ℕ), MeasurableSet (s n)
hs : ∀ (n : ℕ), Fact (LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (s n) : ℝ≥0∞) (∞ : ℝ≥0∞))
ξ : ℕ → Measure α := fun (n : ℕ) ↦ (μ.restrict (s n)).singularPart (ν.restrict (s n))
f : ℕ → α → ℝ≥0∞ := fun (n : ℕ) ↦ (s n).indicator ((μ.restrict (s n)).rnDeriv (ν.restrict (s n)))
hfm : ∀ (n : ℕ), Measurable (f n)
n : ℕ
refine :
  Eq (α := ℝ≥0∞) ((μ.restrict (s n) : (a : Set α) → ℝ≥0∞) (s n)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞) ∧
    Eq (α := ℝ≥0∞) ((ν.restrict (s n)ᶜ : (a : Set α) → ℝ≥0∞) (s n)ᶜᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ μ.restrict (s n) ⟂ₘ ν.restrict (s n)ᶜ

Tactic:
refine ⟨(s n)ᶜ, (hsm n).compl, ?_⟩
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
ν : Measure α
inst : SigmaFinite ν
μ : Measure α
inst_1 : SFinite μ
hμ : IsFiniteMeasure μ
s : ℕ → Set α := disjointed (spanningSets ν)
hsm : ∀ (n : ℕ), MeasurableSet (s n)
hs : ∀ (n : ℕ), Fact (LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (s n) : ℝ≥0∞) (∞ : ℝ≥0∞))
ξ : ℕ → Measure α := fun (n : ℕ) ↦ (μ.restrict (s n)).singularPart (ν.restrict (s n))
f : ℕ → α → ℝ≥0∞ := fun (n : ℕ) ↦ (s n).indicator ((μ.restrict (s n)).rnDeriv (ν.restrict (s n)))
hfm : ∀ (n : ℕ), Measurable (f n)
n : ℕ
⊢ Eq (α := ℝ≥0∞) ((μ.restrict (s n) : (a : Set α) → ℝ≥0∞) (s n)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞) ∧
    Eq (α := ℝ≥0∞) ((ν.restrict (s n)ᶜ : (a : Set α) → ℝ≥0∞) (s n)ᶜᶜ : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
simp [hsm]