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 : SigmaFinite ν₁
inst_1 : SigmaFinite ν₂
inst_2 : SigmaFinite μ
rw : ν₁ + ν₂ = (ν₁ + ν₂).singularPart μ + μ.withDensity (ν₁.rnDeriv μ + ν₂.rnDeriv μ)
rw₁ : ν₁ + ν₂ = ν₁.singularPart μ + ν₂.singularPart μ + μ.withDensity (ν₁.rnDeriv μ + ν₂.rnDeriv μ)
rw₂ : ν₁ + ν₂ = ν₁.singularPart μ + ν₂.singularPart μ + (μ.withDensity (ν₁.rnDeriv μ) + μ.withDensity (ν₂.rnDeriv μ))
rw₃ : ν₁ + ν₂ = ν₁.singularPart μ + (ν₂.singularPart μ + (μ.withDensity (ν₁.rnDeriv μ) + μ.withDensity (ν₂.rnDeriv μ)))
rw₄ : ν₁ + ν₂ = ν₁.singularPart μ + (μ.withDensity (ν₁.rnDeriv μ) + μ.withDensity (ν₂.rnDeriv μ) + ν₂.singularPart μ)
rw₅ : ν₁ + ν₂ = ν₁.singularPart μ + (μ.withDensity (ν₁.rnDeriv μ) + (μ.withDensity (ν₂.rnDeriv μ) + ν₂.singularPart μ))
rw₆ : ν₁ + ν₂ = ν₁.singularPart μ + (μ.withDensity (ν₁.rnDeriv μ) + (ν₂.singularPart μ + μ.withDensity (ν₂.rnDeriv μ)))
⊢ (ν₁ + ν₂).singularPart μ + μ.withDensity ((ν₁ + ν₂).rnDeriv μ) =
    (ν₁ + ν₂).singularPart μ + μ.withDensity (ν₁.rnDeriv μ + ν₂.rnDeriv μ)
have rw₇ : ν₁ + ν₂ = ν₁.singularPart μ + (μ.withDensity (ν₁.rnDeriv μ) + ν₂)
Tactic: rw [← (ν₁ + ν₂).haveLebesgueDecomposition_add μ, singularPart_add,
      withDensity_add_left (measurable_rnDeriv _ _), add_assoc,
      add_comm (ν₂.singularPart μ), add_assoc, add_comm _ (ν₂.singularPart μ),
      ← ν₂.haveLebesgueDecomposition_add μ, ← add_assoc, ← ν₁.haveLebesgueDecomposition_add μ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
ν₁ ν₂ μ : Measure α
inst : SigmaFinite ν₁
inst_1 : SigmaFinite ν₂
inst_2 : SigmaFinite μ
rw : ν₁ + ν₂ = (ν₁ + ν₂).singularPart μ + μ.withDensity (ν₁.rnDeriv μ + ν₂.rnDeriv μ)
rw₁ : ν₁ + ν₂ = ν₁.singularPart μ + ν₂.singularPart μ + μ.withDensity (ν₁.rnDeriv μ + ν₂.rnDeriv μ)
rw₂ : ν₁ + ν₂ = ν₁.singularPart μ + ν₂.singularPart μ + (μ.withDensity (ν₁.rnDeriv μ) + μ.withDensity (ν₂.rnDeriv μ))
rw₃ : ν₁ + ν₂ = ν₁.singularPart μ + (ν₂.singularPart μ + (μ.withDensity (ν₁.rnDeriv μ) + μ.withDensity (ν₂.rnDeriv μ)))
rw₄ : ν₁ + ν₂ = ν₁.singularPart μ + (μ.withDensity (ν₁.rnDeriv μ) + μ.withDensity (ν₂.rnDeriv μ) + ν₂.singularPart μ)
rw₅ : ν₁ + ν₂ = ν₁.singularPart μ + (μ.withDensity (ν₁.rnDeriv μ) + (μ.withDensity (ν₂.rnDeriv μ) + ν₂.singularPart μ))
rw₆ : ν₁ + ν₂ = ν₁.singularPart μ + (μ.withDensity (ν₁.rnDeriv μ) + (ν₂.singularPart μ + μ.withDensity (ν₂.rnDeriv μ)))
rw₇ : ν₁ + ν₂ = ν₁.singularPart μ + (μ.withDensity (ν₁.rnDeriv μ) + ν₂)
⊢ (ν₁ + ν₂).singularPart μ + μ.withDensity ((ν₁ + ν₂).rnDeriv μ) =
    (ν₁ + ν₂).singularPart μ + μ.withDensity (ν₁.rnDeriv μ + ν₂.rnDeriv μ)
have rw₈ : ν₁ + ν₂ = ν₁.singularPart μ + μ.withDensity (ν₁.rnDeriv μ) + ν₂
Tactic: rw [← (ν₁ + ν₂).haveLebesgueDecomposition_add μ, singularPart_add,
      withDensity_add_left (measurable_rnDeriv _ _), add_assoc,
      add_comm (ν₂.singularPart μ), add_assoc, add_comm _ (ν₂.singularPart μ),
      ← ν₂.haveLebesgueDecomposition_add μ, ← add_assoc, ← ν₁.haveLebesgueDecomposition_add μ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
ν₁ ν₂ μ : Measure α
inst : SigmaFinite ν₁
inst_1 : SigmaFinite ν₂
inst_2 : SigmaFinite μ
rw : ν₁ + ν₂ = (ν₁ + ν₂).singularPart μ + μ.withDensity (ν₁.rnDeriv μ + ν₂.rnDeriv μ)
rw₁ : ν₁ + ν₂ = ν₁.singularPart μ + ν₂.singularPart μ + μ.withDensity (ν₁.rnDeriv μ + ν₂.rnDeriv μ)
rw₂ : ν₁ + ν₂ = ν₁.singularPart μ + ν₂.singularPart μ + (μ.withDensity (ν₁.rnDeriv μ) + μ.withDensity (ν₂.rnDeriv μ))
rw₃ : ν₁ + ν₂ = ν₁.singularPart μ + (ν₂.singularPart μ + (μ.withDensity (ν₁.rnDeriv μ) + μ.withDensity (ν₂.rnDeriv μ)))
rw₄ : ν₁ + ν₂ = ν₁.singularPart μ + (μ.withDensity (ν₁.rnDeriv μ) + μ.withDensity (ν₂.rnDeriv μ) + ν₂.singularPart μ)
rw₅ : ν₁ + ν₂ = ν₁.singularPart μ + (μ.withDensity (ν₁.rnDeriv μ) + (μ.withDensity (ν₂.rnDeriv μ) + ν₂.singularPart μ))
rw₆ : ν₁ + ν₂ = ν₁.singularPart μ + (μ.withDensity (ν₁.rnDeriv μ) + (ν₂.singularPart μ + μ.withDensity (ν₂.rnDeriv μ)))
rw₇ : ν₁ + ν₂ = ν₁.singularPart μ + (μ.withDensity (ν₁.rnDeriv μ) + ν₂)
rw₈ : ν₁ + ν₂ = ν₁.singularPart μ + μ.withDensity (ν₁.rnDeriv μ) + ν₂
⊢ (ν₁ + ν₂).singularPart μ + μ.withDensity ((ν₁ + ν₂).rnDeriv μ) =
    (ν₁ + ν₂).singularPart μ + μ.withDensity (ν₁.rnDeriv μ + ν₂.rnDeriv μ)
have rw₉ : ν₁ + ν₂ = ν₁ + ν₂
Tactic: rw [← (ν₁ + ν₂).haveLebesgueDecomposition_add μ, singularPart_add,
      withDensity_add_left (measurable_rnDeriv _ _), add_assoc,
      add_comm (ν₂.singularPart μ), add_assoc, add_comm _ (ν₂.singularPart μ),
      ← ν₂.haveLebesgueDecomposition_add μ, ← add_assoc, ← ν₁.haveLebesgueDecomposition_add μ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
ν₁ ν₂ μ : Measure α
inst : SigmaFinite ν₁
inst_1 : SigmaFinite ν₂
inst_2 : SigmaFinite μ
h : ν₂ ⟂ₘ μ
⊢ (ν₁ + ν₂).rnDeriv μ =ᶠ[ae μ] ν₁.rnDeriv μ
have h₁ : ∀ (x : α) (hx_add : (ν₁ + ν₂).rnDeriv μ x = (ν₁.rnDeriv μ + ν₂.rnDeriv μ) x) (hx_zero : ν₂.rnDeriv μ x = 0 x),
  (ν₁ + ν₂).rnDeriv μ x = ν₁.rnDeriv μ x
Tactic: filter_upwards [rnDeriv_add' ν₁ ν₂ μ, (rnDeriv_eq_zero ν₂ μ).mpr h] with x hx_add hx_zero
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν ξ : Measure α
h : μ ⟂ₘ ξ
s : Set α := h.nullSet
⊢ μ + (ν - ξ) = μ + ν - ξ
have hs : MeasurableSet s
Tactic: have hs : MeasurableSet s := h.measurableSet_nullSet
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν ξ : Measure α
h : μ ⟂ₘ ξ
s : Set α := h.nullSet
hs : MeasurableSet s
⊢ μ.restrict s + (ν - ξ).restrict s = μ.restrict s + ν.restrict s - ξ.restrict s
have rw : 0 + (ν.restrict s - ξ.restrict s) = 0 + ν.restrict s - ξ.restrict s
Tactic: rw [h.restrict_nullSet, restrict_sub_eq_restrict_sub_restrict hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν ξ : Measure α
h : μ ⟂ₘ ξ
s : Set α := h.nullSet
hs : MeasurableSet s
⊢ μ + (ν - ξ) = μ + ν - ξ
have h_le_s : μ.restrict s + (ν - ξ).restrict s = μ.restrict s + ν.restrict s - ξ.restrict s
Tactic: have h_le_s : μ.restrict s + (ν - ξ).restrict s = μ.restrict s + ν.restrict s - ξ.restrict s := by
    rw [h.restrict_nullSet, restrict_sub_eq_restrict_sub_restrict hs]
    simp
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν ξ : Measure α
h : μ ⟂ₘ ξ
s : Set α := h.nullSet
hs : MeasurableSet s
h_le_s : μ.restrict s + (ν - ξ).restrict s = μ.restrict s + ν.restrict s - ξ.restrict s
⊢ μ.restrict sᶜ + (ν - ξ).restrict sᶜ = μ.restrict sᶜ + ν.restrict sᶜ - ξ.restrict sᶜ
have rw : μ.restrict sᶜ + (ν.restrict sᶜ - 0) = μ.restrict sᶜ + ν.restrict sᶜ - 0
Tactic: rw [restrict_sub_eq_restrict_sub_restrict hs.compl, h.restrict_compl_nullSet]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν ξ : Measure α
h : μ ⟂ₘ ξ
s : Set α := h.nullSet
hs : MeasurableSet s
h_le_s : μ.restrict s + (ν - ξ).restrict s = μ.restrict s + ν.restrict s - ξ.restrict s
⊢ μ + (ν - ξ) = μ + ν - ξ
have h_le_s_compl : μ.restrict sᶜ + (ν - ξ).restrict sᶜ = μ.restrict sᶜ + ν.restrict sᶜ - ξ.restrict sᶜ
Tactic: have h_le_s_compl : μ.restrict sᶜ + (ν - ξ).restrict sᶜ =
      μ.restrict sᶜ + ν.restrict sᶜ - ξ.restrict sᶜ := by
    rw [restrict_sub_eq_restrict_sub_restrict hs.compl, h.restrict_compl_nullSet]
    simp
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν ξ : Measure α
h : μ ⟂ₘ ξ
s : Set α := h.nullSet
hs : MeasurableSet s
h_le_s : μ.restrict s + (ν - ξ).restrict s = μ.restrict s + ν.restrict s - ξ.restrict s
h_le_s_compl : μ.restrict sᶜ + (ν - ξ).restrict sᶜ = μ.restrict sᶜ + ν.restrict sᶜ - ξ.restrict sᶜ
⊢ μ + (ν - ξ) = μ.restrict s + μ.restrict sᶜ + (ν - ξ).restrict s + (ν - ξ).restrict sᶜ
have rw : μ + (ν - ξ) = μ + (ν - ξ).restrict s + (ν - ξ).restrict sᶜ
Tactic: rw [restrict_add_restrict_compl hs, add_assoc, restrict_add_restrict_compl hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν ξ : Measure α
h : μ ⟂ₘ ξ
s : Set α := h.nullSet
hs : MeasurableSet s
h_le_s : μ.restrict s + (ν - ξ).restrict s = μ.restrict s + ν.restrict s - ξ.restrict s
h_le_s_compl : μ.restrict sᶜ + (ν - ξ).restrict sᶜ = μ.restrict sᶜ + ν.restrict sᶜ - ξ.restrict sᶜ
rw : μ + (ν - ξ) = μ + (ν - ξ).restrict s + (ν - ξ).restrict sᶜ
⊢ μ + (ν - ξ) = μ.restrict s + μ.restrict sᶜ + (ν - ξ).restrict s + (ν - ξ).restrict sᶜ
have rw₁ : μ + (ν - ξ) = μ + ((ν - ξ).restrict s + (ν - ξ).restrict sᶜ)
Tactic: rw [restrict_add_restrict_compl hs, add_assoc, restrict_add_restrict_compl hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν ξ : Measure α
h : μ ⟂ₘ ξ
s : Set α := h.nullSet
hs : MeasurableSet s
h_le_s : μ.restrict s + (ν - ξ).restrict s = μ.restrict s + ν.restrict s - ξ.restrict s
h_le_s_compl : μ.restrict sᶜ + (ν - ξ).restrict sᶜ = μ.restrict sᶜ + ν.restrict sᶜ - ξ.restrict sᶜ
rw : μ + (ν - ξ) = μ + (ν - ξ).restrict s + (ν - ξ).restrict sᶜ
rw₁ : μ + (ν - ξ) = μ + ((ν - ξ).restrict s + (ν - ξ).restrict sᶜ)
⊢ μ + (ν - ξ) = μ.restrict s + μ.restrict sᶜ + (ν - ξ).restrict s + (ν - ξ).restrict sᶜ
have rw₂ : μ + (ν - ξ) = μ + (ν - ξ)
Tactic: rw [restrict_add_restrict_compl hs, add_assoc, restrict_add_restrict_compl hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν ξ : Measure α
h : μ ⟂ₘ ξ
s : Set α := h.nullSet
hs : MeasurableSet s
h_le_s : μ.restrict s + (ν - ξ).restrict s = μ.restrict s + ν.restrict s - ξ.restrict s
h_le_s_compl : μ.restrict sᶜ + (ν - ξ).restrict sᶜ = μ.restrict sᶜ + ν.restrict sᶜ - ξ.restrict sᶜ
⊢ μ.restrict s + (ν - ξ).restrict s + (μ.restrict sᶜ + (ν - ξ).restrict sᶜ) =
    μ.restrict s + ν.restrict s - ξ.restrict s + (μ.restrict sᶜ + ν.restrict sᶜ - ξ.restrict sᶜ)
have rw : μ.restrict s + ν.restrict s - ξ.restrict s + (μ.restrict sᶜ + (ν - ξ).restrict sᶜ) =
  μ.restrict s + ν.restrict s - ξ.restrict s + (μ.restrict sᶜ + ν.restrict sᶜ - ξ.restrict sᶜ)
Tactic: rw [h_le_s, h_le_s_compl]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν ξ : Measure α
h : μ ⟂ₘ ξ
s : Set α := h.nullSet
hs : MeasurableSet s
h_le_s : μ.restrict s + (ν - ξ).restrict s = μ.restrict s + ν.restrict s - ξ.restrict s
h_le_s_compl : μ.restrict sᶜ + (ν - ξ).restrict sᶜ = μ.restrict sᶜ + ν.restrict sᶜ - ξ.restrict sᶜ
rw :
  μ.restrict s + ν.restrict s - ξ.restrict s + (μ.restrict sᶜ + (ν - ξ).restrict sᶜ) =
    μ.restrict s + ν.restrict s - ξ.restrict s + (μ.restrict sᶜ + ν.restrict sᶜ - ξ.restrict sᶜ)
⊢ μ.restrict s + (ν - ξ).restrict s + (μ.restrict sᶜ + (ν - ξ).restrict sᶜ) =
    μ.restrict s + ν.restrict s - ξ.restrict s + (μ.restrict sᶜ + ν.restrict sᶜ - ξ.restrict sᶜ)
have rw₁ : μ.restrict s + ν.restrict s - ξ.restrict s + (μ.restrict sᶜ + ν.restrict sᶜ - ξ.restrict sᶜ) =
  μ.restrict s + ν.restrict s - ξ.restrict s + (μ.restrict sᶜ + ν.restrict sᶜ - ξ.restrict sᶜ)
Tactic: rw [h_le_s, h_le_s_compl]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν ξ : Measure α
h : μ ⟂ₘ ξ
s : Set α := h.nullSet
hs : MeasurableSet s
h_le_s : μ.restrict s + (ν - ξ).restrict s = μ.restrict s + ν.restrict s - ξ.restrict s
h_le_s_compl : μ.restrict sᶜ + (ν - ξ).restrict sᶜ = μ.restrict sᶜ + ν.restrict sᶜ - ξ.restrict sᶜ
⊢ (μ + ν - ξ).restrict s + (μ + ν - ξ).restrict sᶜ = μ + ν - ξ
have rw : μ + ν - ξ = μ + ν - ξ
Tactic: rw [restrict_add_restrict_compl hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν ξ : Measure α
h : μ ⟂ₘ ξ
s : Set α := h.nullSet
hs : MeasurableSet s
h_le_s : μ.restrict s + (ν - ξ).restrict s = μ.restrict s + ν.restrict s - ξ.restrict s
h_le_s_compl : μ.restrict sᶜ + (ν - ξ).restrict sᶜ = μ.restrict sᶜ + ν.restrict sᶜ - ξ.restrict sᶜ
⊢ μ + (ν - ξ) = μ + ν - ξ
have calc : μ + (ν - ξ) = μ.restrict s + μ.restrict sᶜ + (ν - ξ).restrict s + (ν - ξ).restrict sᶜ
Tactic: calc μ + (ν - ξ)
  _ = μ.restrict s + μ.restrict sᶜ + (ν - ξ).restrict s + (ν - ξ).restrict sᶜ := by
    rw [restrict_add_restrict_compl hs, add_assoc, restrict_add_restrict_compl hs]
  _ = μ.restrict s + (ν - ξ).restrict s + (μ.restrict sᶜ + (ν - ξ).restrict sᶜ) := by abel
  _ = (μ.restrict s + ν.restrict s - ξ.restrict s) +
      (μ.restrict sᶜ + ν.restrict sᶜ - ξ.restrict sᶜ) := by rw [h_le_s, h_le_s_compl]
  _ = (μ + ν - ξ).restrict s + (μ + ν - ξ).restrict sᶜ := by
      simp [restrict_sub_eq_restrict_sub_restrict hs,
        restrict_sub_eq_restrict_sub_restrict hs.compl]
  _ = μ + ν - ξ := by rw [restrict_add_restrict_compl hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν ξ : Measure α
h : μ ⟂ₘ ξ
s : Set α := h.nullSet
hs : MeasurableSet s
h_le_s : μ.restrict s + (ν - ξ).restrict s = μ.restrict s + ν.restrict s - ξ.restrict s
h_le_s_compl : μ.restrict sᶜ + (ν - ξ).restrict sᶜ = μ.restrict sᶜ + ν.restrict sᶜ - ξ.restrict sᶜ
calc : μ + (ν - ξ) = μ.restrict s + μ.restrict sᶜ + (ν - ξ).restrict s + (ν - ξ).restrict sᶜ
⊢ μ + (ν - ξ) = μ + ν - ξ
have calc₁ : μ.restrict s + μ.restrict sᶜ + (ν - ξ).restrict s + (ν - ξ).restrict sᶜ =
  μ.restrict s + (ν - ξ).restrict s + (μ.restrict sᶜ + (ν - ξ).restrict sᶜ)
Tactic: calc μ + (ν - ξ)
  _ = μ.restrict s + μ.restrict sᶜ + (ν - ξ).restrict s + (ν - ξ).restrict sᶜ := by
    rw [restrict_add_restrict_compl hs, add_assoc, restrict_add_restrict_compl hs]
  _ = μ.restrict s + (ν - ξ).restrict s + (μ.restrict sᶜ + (ν - ξ).restrict sᶜ) := by abel
  _ = (μ.restrict s + ν.restrict s - ξ.restrict s) +
      (μ.restrict sᶜ + ν.restrict sᶜ - ξ.restrict sᶜ) := by rw [h_le_s, h_le_s_compl]
  _ = (μ + ν - ξ).restrict s + (μ + ν - ξ).restrict sᶜ := by
      simp [restrict_sub_eq_restrict_sub_restrict hs,
        restrict_sub_eq_restrict_sub_restrict hs.compl]
  _ = μ + ν - ξ := by rw [restrict_add_restrict_compl hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν ξ : Measure α
h : μ ⟂ₘ ξ
s : Set α := h.nullSet
hs : MeasurableSet s
h_le_s : μ.restrict s + (ν - ξ).restrict s = μ.restrict s + ν.restrict s - ξ.restrict s
h_le_s_compl : μ.restrict sᶜ + (ν - ξ).restrict sᶜ = μ.restrict sᶜ + ν.restrict sᶜ - ξ.restrict sᶜ
calc : μ + (ν - ξ) = μ.restrict s + μ.restrict sᶜ + (ν - ξ).restrict s + (ν - ξ).restrict sᶜ
calc₁ :
  μ.restrict s + μ.restrict sᶜ + (ν - ξ).restrict s + (ν - ξ).restrict sᶜ =
    μ.restrict s + (ν - ξ).restrict s + (μ.restrict sᶜ + (ν - ξ).restrict sᶜ)
⊢ μ + (ν - ξ) = μ + ν - ξ
have calc₂ : μ.restrict s + (ν - ξ).restrict s + (μ.restrict sᶜ + (ν - ξ).restrict sᶜ) =
  μ.restrict s + ν.restrict s - ξ.restrict s + (μ.restrict sᶜ + ν.restrict sᶜ - ξ.restrict sᶜ)
Tactic: calc μ + (ν - ξ)
  _ = μ.restrict s + μ.restrict sᶜ + (ν - ξ).restrict s + (ν - ξ).restrict sᶜ := by
    rw [restrict_add_restrict_compl hs, add_assoc, restrict_add_restrict_compl hs]
  _ = μ.restrict s + (ν - ξ).restrict s + (μ.restrict sᶜ + (ν - ξ).restrict sᶜ) := by abel
  _ = (μ.restrict s + ν.restrict s - ξ.restrict s) +
      (μ.restrict sᶜ + ν.restrict sᶜ - ξ.restrict sᶜ) := by rw [h_le_s, h_le_s_compl]
  _ = (μ + ν - ξ).restrict s + (μ + ν - ξ).restrict sᶜ := by
      simp [restrict_sub_eq_restrict_sub_restrict hs,
        restrict_sub_eq_restrict_sub_restrict hs.compl]
  _ = μ + ν - ξ := by rw [restrict_add_restrict_compl hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν ξ : Measure α
h : μ ⟂ₘ ξ
s : Set α := h.nullSet
hs : MeasurableSet s
h_le_s : μ.restrict s + (ν - ξ).restrict s = μ.restrict s + ν.restrict s - ξ.restrict s
h_le_s_compl : μ.restrict sᶜ + (ν - ξ).restrict sᶜ = μ.restrict sᶜ + ν.restrict sᶜ - ξ.restrict sᶜ
calc : μ + (ν - ξ) = μ.restrict s + μ.restrict sᶜ + (ν - ξ).restrict s + (ν - ξ).restrict sᶜ
calc₁ :
  μ.restrict s + μ.restrict sᶜ + (ν - ξ).restrict s + (ν - ξ).restrict sᶜ =
    μ.restrict s + (ν - ξ).restrict s + (μ.restrict sᶜ + (ν - ξ).restrict sᶜ)
calc₂ :
  μ.restrict s + (ν - ξ).restrict s + (μ.restrict sᶜ + (ν - ξ).restrict sᶜ) =
    μ.restrict s + ν.restrict s - ξ.restrict s + (μ.restrict sᶜ + ν.restrict sᶜ - ξ.restrict sᶜ)
⊢ μ + (ν - ξ) = μ + ν - ξ
have calc₃ : μ.restrict s + ν.restrict s - ξ.restrict s + (μ.restrict sᶜ + ν.restrict sᶜ - ξ.restrict sᶜ) =
  (μ + ν - ξ).restrict s + (μ + ν - ξ).restrict sᶜ
Tactic: calc μ + (ν - ξ)
  _ = μ.restrict s + μ.restrict sᶜ + (ν - ξ).restrict s + (ν - ξ).restrict sᶜ := by
    rw [restrict_add_restrict_compl hs, add_assoc, restrict_add_restrict_compl hs]
  _ = μ.restrict s + (ν - ξ).restrict s + (μ.restrict sᶜ + (ν - ξ).restrict sᶜ) := by abel
  _ = (μ.restrict s + ν.restrict s - ξ.restrict s) +
      (μ.restrict sᶜ + ν.restrict sᶜ - ξ.restrict sᶜ) := by rw [h_le_s, h_le_s_compl]
  _ = (μ + ν - ξ).restrict s + (μ + ν - ξ).restrict sᶜ := by
      simp [restrict_sub_eq_restrict_sub_restrict hs,
        restrict_sub_eq_restrict_sub_restrict hs.compl]
  _ = μ + ν - ξ := by rw [restrict_add_restrict_compl hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν ξ : Measure α
h : μ ⟂ₘ ξ
s : Set α := h.nullSet
hs : MeasurableSet s
h_le_s : μ.restrict s + (ν - ξ).restrict s = μ.restrict s + ν.restrict s - ξ.restrict s
h_le_s_compl : μ.restrict sᶜ + (ν - ξ).restrict sᶜ = μ.restrict sᶜ + ν.restrict sᶜ - ξ.restrict sᶜ
calc : μ + (ν - ξ) = μ.restrict s + μ.restrict sᶜ + (ν - ξ).restrict s + (ν - ξ).restrict sᶜ
calc₁ :
  μ.restrict s + μ.restrict sᶜ + (ν - ξ).restrict s + (ν - ξ).restrict sᶜ =
    μ.restrict s + (ν - ξ).restrict s + (μ.restrict sᶜ + (ν - ξ).restrict sᶜ)
calc₂ :
  μ.restrict s + (ν - ξ).restrict s + (μ.restrict sᶜ + (ν - ξ).restrict sᶜ) =
    μ.restrict s + ν.restrict s - ξ.restrict s + (μ.restrict sᶜ + ν.restrict sᶜ - ξ.restrict sᶜ)
calc₃ :
  μ.restrict s + ν.restrict s - ξ.restrict s + (μ.restrict sᶜ + ν.restrict sᶜ - ξ.restrict sᶜ) =
    (μ + ν - ξ).restrict s + (μ + ν - ξ).restrict sᶜ
⊢ μ + (ν - ξ) = μ + ν - ξ
have calc₄ : (μ + ν - ξ).restrict s + (μ + ν - ξ).restrict sᶜ = μ + ν - ξ
Tactic: calc μ + (ν - ξ)
  _ = μ.restrict s + μ.restrict sᶜ + (ν - ξ).restrict s + (ν - ξ).restrict sᶜ := by
    rw [restrict_add_restrict_compl hs, add_assoc, restrict_add_restrict_compl hs]
  _ = μ.restrict s + (ν - ξ).restrict s + (μ.restrict sᶜ + (ν - ξ).restrict sᶜ) := by abel
  _ = (μ.restrict s + ν.restrict s - ξ.restrict s) +
      (μ.restrict sᶜ + ν.restrict sᶜ - ξ.restrict sᶜ) := by rw [h_le_s, h_le_s_compl]
  _ = (μ + ν - ξ).restrict s + (μ + ν - ξ).restrict sᶜ := by
      simp [restrict_sub_eq_restrict_sub_restrict hs,
        restrict_sub_eq_restrict_sub_restrict hs.compl]
  _ = μ + ν - ξ := by rw [restrict_add_restrict_compl hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Dirac (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
s : Set α
a : α
⊢ Eq (α := ℝ≥0∞) (((dirac a : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ∨
    Eq (α := ℝ≥0∞) (((dirac a : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) (if a ∈ toMeasurable (dirac a) s then 1 a else 0) 0 ∨
  Eq (α := ℝ≥0∞) (if a ∈ toMeasurable (dirac a) s then 1 a else 0) 1
Tactic: rw [← measure_toMeasurable s, dirac_apply' a (measurableSet_toMeasurable ..), indicator]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Dirac (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
s : Set α
a : α
⊢ Eq (α := ℝ≥0∞) (if a ∈ toMeasurable (dirac a) s then 1 a else 0) 0 ∨
    Eq (α := ℝ≥0∞) (if a ∈ toMeasurable (dirac a) s then 1 a else 0) 1
have simp : a ∉ toMeasurable (dirac a) s ∨ a ∈ toMeasurable (dirac a) s
Tactic: simp only [Pi.one_apply, ite_eq_right_iff, one_ne_zero, imp_false, ite_eq_left_iff, zero_ne_one,
    not_not]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Dirac (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
s : Set α
a : α
⊢ a ∉ toMeasurable (dirac a) s ∨ a ∈ toMeasurable (dirac a) s
have tauto : ¬a ∉ toMeasurable (dirac a) s → a ∈ toMeasurable (dirac a) s
Tactic: tauto
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Dirac (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
s : Set α
a : α
tauto : ¬a ∉ toMeasurable (dirac a) s → a ∈ toMeasurable (dirac a) s
⊢ a ∉ toMeasurable (dirac a) s ∨ a ∈ toMeasurable (dirac a) s
have tauto₁ : a ∈ toMeasurable (dirac a) s → a ∈ toMeasurable (dirac a) s
Tactic: tauto
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Dirac (hypothesis)
Goal:
α : Type u_1
inst : MeasurableSpace α
s : Set α
a : α
h : a ∈ s
⊢ Eq (α := ℝ≥0∞) (((dirac a : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 : ℝ≥0∞)
have this : ∀ (t : Set α), a ∈ t → Eq (α := ℝ≥0∞) (t.indicator 1 a) 1
Tactic: have : ∀ t : Set α, a ∈ t → t.indicator (1 : α → ℝ≥0∞) a = 1 := fun t ht => indicator_of_mem ht 1
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Dirac (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
s : Set α
a : α
h : a ∈ s
this : ∀ (t : Set α), a ∈ t → Eq (α := ℝ≥0∞) (t.indicator 1 a) 1
⊢ Eq (α := ℝ≥0∞) (((dirac a : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 : ℝ≥0∞)
have refine : LE.le (α := ℝ≥0∞) (((dirac a : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (indicator univ 1 a : ℝ≥0∞)
Tactic: refine le_antisymm (this univ trivial ▸ ?_) (this s h ▸ le_dirac_apply)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Dirac (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
s : Set α
a : α
h : a ∈ s
this : ∀ (t : Set α), a ∈ t → Eq (α := ℝ≥0∞) (t.indicator 1 a) 1
⊢ LE.le (α := ℝ≥0∞) (((dirac a : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (indicator univ 1 a : ℝ≥0∞)
have rw : LE.le (α := ℝ≥0∞) (((dirac a : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
  (((dirac a : Measure α) : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
Tactic: rw [← dirac_apply' a MeasurableSet.univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Dirac (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : MeasurableSingletonClass α
a : α
s : Set α
⊢ Eq (α := ℝ≥0∞) (((dirac a : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (s.indicator 1 a : ℝ≥0∞)
have pos : ∀ (h : a ∈ s), Eq (α := ℝ≥0∞) (((dirac a : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (s.indicator 1 a : ℝ≥0∞)
Tactic: by_cases h : a ∈ s
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Dirac (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : MeasurableSingletonClass α
a : α
s : Set α
pos : ∀ (h : a ∈ s), Eq (α := ℝ≥0∞) (((dirac a : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (s.indicator 1 a : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((dirac a : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (s.indicator 1 a : ℝ≥0∞)
have neg : ∀ (h : a ∉ s), Eq (α := ℝ≥0∞) (((dirac a : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (s.indicator 1 a : ℝ≥0∞)
Tactic: by_cases h : a ∈ s
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Dirac (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : MeasurableSingletonClass α
a : α
s : Set α
h : a ∈ s
⊢ Eq (α := ℝ≥0∞) (((dirac a : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (s.indicator 1 a : ℝ≥0∞)
have pos : Eq (α := ℝ≥0∞) 1 (s.indicator 1 a)
Tactic: rw [dirac_apply_of_mem h, indicator_of_mem h, Pi.one_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Dirac (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : MeasurableSingletonClass α
a : α
s : Set α
h : a ∈ s
pos : Eq (α := ℝ≥0∞) 1 (s.indicator 1 a)
⊢ Eq (α := ℝ≥0∞) (((dirac a : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (s.indicator 1 a : ℝ≥0∞)
have pos₁ : Eq (α := ℝ≥0∞) 1 (1 a)
Tactic: rw [dirac_apply_of_mem h, indicator_of_mem h, Pi.one_apply]