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 : ν.HaveLebesgueDecomposition μ
hμν : μ ≪ ν.singularPart μ + μ.withDensity (ν.rnDeriv μ)
s : Set α
h : MeasurableSet s
hνs : Eq (α := ℝ≥0∞) ((μ.withDensity (ν.rnDeriv μ) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
t : Set α
left : MeasurableSet t
ht1 : Eq (α := ℝ≥0∞) ((ν.singularPart μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
ht2 : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) tᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (s ∩ tᶜ) : ℝ≥0∞) ≤
    0
have simp : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) (0 : ℝ≥0∞) ∧
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ tᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: simp only [nonpos_iff_eq_zero, add_eq_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : ν.HaveLebesgueDecomposition μ
hμν : μ ≪ ν.singularPart μ + μ.withDensity (ν.rnDeriv μ)
s : Set α
h : MeasurableSet s
hνs : Eq (α := ℝ≥0∞) ((μ.withDensity (ν.rnDeriv μ) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
t : Set α
left : MeasurableSet t
ht1 : Eq (α := ℝ≥0∞) ((ν.singularPart μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
ht2 : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) tᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) (0 : ℝ≥0∞) ∧
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ tᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)
have left : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : ν.HaveLebesgueDecomposition μ
hμν : μ ≪ ν.singularPart μ + μ.withDensity (ν.rnDeriv μ)
s : Set α
h : MeasurableSet s
hνs : Eq (α := ℝ≥0∞) ((μ.withDensity (ν.rnDeriv μ) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
t : Set α
left_1 : MeasurableSet t
ht1 : Eq (α := ℝ≥0∞) ((ν.singularPart μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
ht2 : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) tᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
left : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) (0 : ℝ≥0∞) ∧
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ tᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)
have right : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ tᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : ν.HaveLebesgueDecomposition μ
hμν : μ ≪ ν.singularPart μ + μ.withDensity (ν.rnDeriv μ)
s : Set α
h : MeasurableSet s
hνs : Eq (α := ℝ≥0∞) ((μ.withDensity (ν.rnDeriv μ) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
t : Set α
left : MeasurableSet t
ht1 : Eq (α := ℝ≥0∞) ((ν.singularPart μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
ht2 : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) tᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) (0 : ℝ≥0∞)
have left : Eq (α := ℝ≥0∞) ((ν.singularPart μ + μ.withDensity (ν.rnDeriv μ) : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: refine hμν ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : ν.HaveLebesgueDecomposition μ
hμν : μ ≪ ν.singularPart μ + μ.withDensity (ν.rnDeriv μ)
s : Set α
h : MeasurableSet s
hνs : Eq (α := ℝ≥0∞) ((μ.withDensity (ν.rnDeriv μ) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
t : Set α
left : MeasurableSet t
ht1 : Eq (α := ℝ≥0∞) ((ν.singularPart μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
ht2 : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) tᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((ν.singularPart μ + μ.withDensity (ν.rnDeriv μ) : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) (0 : ℝ≥0∞)
have left : Eq (α := ℝ≥0∞) ((ν.singularPart μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) (0 : ℝ≥0∞) ∧
  Eq (α := ℝ≥0∞) ((μ.withDensity (ν.rnDeriv μ) : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: simp only [coe_add, Pi.add_apply, add_eq_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : ν.HaveLebesgueDecomposition μ
hμν : μ ≪ ν.singularPart μ + μ.withDensity (ν.rnDeriv μ)
s : Set α
h : MeasurableSet s
hνs : Eq (α := ℝ≥0∞) ((μ.withDensity (ν.rnDeriv μ) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
t : Set α
left : MeasurableSet t
ht1 : Eq (α := ℝ≥0∞) ((ν.singularPart μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
ht2 : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) tᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((ν.singularPart μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) (0 : ℝ≥0∞) ∧
    Eq (α := ℝ≥0∞) ((μ.withDensity (ν.rnDeriv μ) : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) (0 : ℝ≥0∞)
have left : Eq (α := ℝ≥0∞) ((ν.singularPart μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : ν.HaveLebesgueDecomposition μ
hμν : μ ≪ ν.singularPart μ + μ.withDensity (ν.rnDeriv μ)
s : Set α
h : MeasurableSet s
hνs : Eq (α := ℝ≥0∞) ((μ.withDensity (ν.rnDeriv μ) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
t : Set α
left_1 : MeasurableSet t
ht1 : Eq (α := ℝ≥0∞) ((ν.singularPart μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
ht2 : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) tᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
left : Eq (α := ℝ≥0∞) ((ν.singularPart μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((ν.singularPart μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) (0 : ℝ≥0∞) ∧
    Eq (α := ℝ≥0∞) ((μ.withDensity (ν.rnDeriv μ) : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) (0 : ℝ≥0∞)
have left₁ : Eq (α := ℝ≥0∞) ((μ.withDensity (ν.rnDeriv μ) : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν ξ : Measure α
inst : μ.HaveLebesgueDecomposition ν
hξμ : ξ ≪ μ
hξν : ξ ≪ ν
| μ
have rw : ν.withDensity (μ.rnDeriv ν) + μ.singularPart ν
Tactic: rw [μ.haveLebesgueDecomposition_add ν, add_comm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν ξ : Measure α
inst : μ.HaveLebesgueDecomposition ν
hξμ : ξ ≪ μ
hξν : ξ ≪ ν
⊢ ξ ≪ ν.withDensity (μ.rnDeriv ν)
have hξμ₁ : ξ ≪ ν.withDensity (μ.rnDeriv ν) + μ.singularPart ν
Tactic: conv_rhs at hξμ => rw [μ.haveLebesgueDecomposition_add ν, add_comm]
Cleared hypotheses: hξμ, hξν
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν ξ : Measure α
inst : μ.HaveLebesgueDecomposition ν
hξμ : ξ ≪ ν.withDensity (μ.rnDeriv ν) + μ.singularPart ν
hξν : ξ ≪ ν
⊢ ξ ≪ ν.withDensity (μ.rnDeriv ν)
have refine : ξ ⟂ₘ μ.singularPart ν
Tactic: refine absolutelyContinuous_of_add_of_mutuallySingular hξμ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
h : μ ≪ ν
⊢ μ.singularPart ν = 0
have rw : μ.singularPart ν ⟂ₘ μ.singularPart ν
Tactic: rw [← MutuallySingular.self_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
| μ
have rw : μ.singularPart 0 + withDensity 0 (μ.rnDeriv 0)
Tactic: rw [haveLebesgueDecomposition_add μ 0]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
⊢ μ.singularPart 0 = μ
have conv_rhs : μ.singularPart 0 = μ.singularPart 0 + withDensity 0 (μ.rnDeriv 0)
Tactic: conv_rhs => rw [haveLebesgueDecomposition_add μ 0]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
⊢ μ.singularPart ν = 0 ↔ μ ≪ ν
have h_dec : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
Tactic: have h_dec := haveLebesgueDecomposition_add μ ν
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
h_dec : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
⊢ μ.singularPart ν = 0 ↔ μ ≪ ν
have refine : ∀ (h : μ.singularPart ν = 0), μ ≪ ν
Tactic: refine ⟨fun h ↦ ?_, singularPart_eq_zero_of_ac⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
h_dec : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
h : μ.singularPart ν = 0
⊢ μ ≪ ν
have h_dec₁ : μ = ν.withDensity (μ.rnDeriv ν)
Tactic: rw [h, zero_add] at h_dec
Cleared hypotheses: h_dec, h
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
h_dec : μ = ν.withDensity (μ.rnDeriv ν)
h : μ.singularPart ν = 0
⊢ μ ≪ ν
have rw : ν.withDensity (μ.rnDeriv ν) ≪ ν
Tactic: rw [h_dec]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
⊢ ν.withDensity (μ.rnDeriv ν) = 0 ↔ μ ⟂ₘ ν
have h_dec : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
Tactic: have h_dec := haveLebesgueDecomposition_add μ ν
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
h_dec : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
⊢ ν.withDensity (μ.rnDeriv ν) = 0 ↔ μ ⟂ₘ ν
have refine_1 : ∀ (h : ν.withDensity (μ.rnDeriv ν) = 0), μ ⟂ₘ ν
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
h_dec : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
refine_1 : ∀ (h : ν.withDensity (μ.rnDeriv ν) = 0), μ ⟂ₘ ν
⊢ ν.withDensity (μ.rnDeriv ν) = 0 ↔ μ ⟂ₘ ν
have refine_2 : ∀ (h : μ ⟂ₘ ν), ν.withDensity (μ.rnDeriv ν) = 0
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
h_dec : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
h : ν.withDensity (μ.rnDeriv ν) = 0
⊢ μ ⟂ₘ ν
have h_dec₁ : μ = μ.singularPart ν
Tactic: rw [h, add_zero] at h_dec
Cleared hypotheses: h_dec, h
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
h_dec : μ = μ.singularPart ν
h : ν.withDensity (μ.rnDeriv ν) = 0
⊢ μ ⟂ₘ ν
have refine_1 : μ.singularPart ν ⟂ₘ ν
Tactic: rw [h_dec]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
h_dec : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
h : μ ⟂ₘ ν
⊢ ν.withDensity (μ.rnDeriv ν) = 0
have refine_2 : ν.withDensity (μ.rnDeriv ν) ⟂ₘ ν.withDensity (μ.rnDeriv ν)
Tactic: rw [← MutuallySingular.self_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
h_dec : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
h : μ ⟂ₘ ν
⊢ ν.withDensity (μ.rnDeriv ν) ⟂ₘ ν.withDensity (μ.rnDeriv ν)
have h₁ : μ.singularPart ν ⟂ₘ ν ∧ ν.withDensity (μ.rnDeriv ν) ⟂ₘ ν
Tactic: rw [h_dec, MutuallySingular.add_left_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
h_dec : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
h : μ.singularPart ν ⟂ₘ ν ∧ ν.withDensity (μ.rnDeriv ν) ⟂ₘ ν
⊢ ν.withDensity (μ.rnDeriv ν) ⟂ₘ ν.withDensity (μ.rnDeriv ν)
have refine_2 : ν.withDensity (μ.rnDeriv ν) ≪ ν
Tactic: refine MutuallySingular.mono_ac h.2 AbsolutelyContinuous.rfl ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
⊢ μ.rnDeriv ν =ᶠ[ae ν] 0 ↔ μ ⟂ₘ ν
have rw : μ.rnDeriv ν =ᶠ[ae ν] 0 ↔ ν.withDensity (μ.rnDeriv ν) = 0
Tactic: rw [← withDensity_rnDeriv_eq_zero, withDensity_eq_zero_iff (measurable_rnDeriv _ _).aemeasurable]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
rw : μ.rnDeriv ν =ᶠ[ae ν] 0 ↔ ν.withDensity (μ.rnDeriv ν) = 0
⊢ μ.rnDeriv ν =ᶠ[ae ν] 0 ↔ μ ⟂ₘ ν
have rw₁ : μ.rnDeriv ν =ᶠ[ae ν] 0 ↔ μ.rnDeriv ν =ᶠ[ae ν] 0
Tactic: rw [← withDensity_rnDeriv_eq_zero, withDensity_eq_zero_iff (measurable_rnDeriv _ _).aemeasurable]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
ν : Measure α
⊢ rnDeriv 0 ν =ᶠ[ae ν] 0
have rw : 0 ⟂ₘ ν
Tactic: rw [rnDeriv_eq_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
hμν : μ ⟂ₘ ν
⊢ μ.rnDeriv ν =ᶠ[ae ν] 0
have pos : ∀ (h : μ.HaveLebesgueDecomposition ν), μ.rnDeriv ν =ᶠ[ae ν] 0
Tactic: by_cases h : μ.HaveLebesgueDecomposition ν
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
hμν : μ ⟂ₘ ν
pos : ∀ (h : μ.HaveLebesgueDecomposition ν), μ.rnDeriv ν =ᶠ[ae ν] 0
⊢ μ.rnDeriv ν =ᶠ[ae ν] 0
have neg : ∀ (h : ¬μ.HaveLebesgueDecomposition ν), μ.rnDeriv ν =ᶠ[ae ν] 0
Tactic: by_cases h : μ.HaveLebesgueDecomposition ν
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
hμν : μ ⟂ₘ ν
h : ¬μ.HaveLebesgueDecomposition ν
⊢ μ.rnDeriv ν =ᶠ[ae ν] 0
have neg : (ae ν).EventuallyEq (β := ℝ≥0∞) 0 0
Tactic: rw [rnDeriv_of_not_haveLebesgueDecomposition h]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
⊢ (μ.singularPart ν).rnDeriv ν =ᶠ[ae ν] 0
have rw : μ.singularPart ν ⟂ₘ ν
Tactic: rw [rnDeriv_eq_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
⊢ μ.rnDeriv μ =ᶠ[ae μ] fun (x : α) ↦ 1
have h : μ.withDensity (μ.rnDeriv μ) + μ.singularPart μ = μ
Tactic: have h := rnDeriv_add_singularPart μ μ
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
h : μ.withDensity (μ.rnDeriv μ) + μ.singularPart μ = μ
⊢ μ.rnDeriv μ =ᶠ[ae μ] fun (x : α) ↦ 1
have h₁ : μ.withDensity (μ.rnDeriv μ) = μ
Tactic: rw [singularPart_self, add_zero] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
h : μ.withDensity (μ.rnDeriv μ) = μ
⊢ μ.rnDeriv μ =ᶠ[ae μ] fun (x : α) ↦ 1
have h_one : μ = μ.withDensity 1
Tactic: have h_one : μ = μ.withDensity 1 := by simp
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
h : μ.withDensity (μ.rnDeriv μ) = μ
h_one : μ = μ.withDensity 1
| μ
have rw : μ.withDensity 1
Tactic: rw [h_one]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
h : μ.withDensity (μ.rnDeriv μ) = μ
h_one : μ = μ.withDensity 1
⊢ μ.rnDeriv μ =ᶠ[ae μ] fun (x : α) ↦ 1
have h₁ : μ.withDensity (μ.rnDeriv μ) = μ.withDensity 1
Tactic: conv_rhs at h => rw [h_one]
Cleared hypotheses: h, h_one
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
h : μ.withDensity (μ.rnDeriv μ) = μ.withDensity 1
h_one : μ = μ.withDensity 1
⊢ μ.rnDeriv μ =ᶠ[ae μ] fun (x : α) ↦ 1
have rwa : AEMeasurable (β := ℝ≥0∞) 1 μ
Tactic: rwa [withDensity_eq_iff_of_sigmaFinite (measurable_rnDeriv _ _).aemeasurable] at h
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
⊢ μ.singularPart ν = μ ↔ μ ⟂ₘ ν
have refine_1 : ∀ (h : μ.singularPart ν = μ), μ ⟂ₘ ν
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
refine_1 : ∀ (h : μ.singularPart ν = μ), μ ⟂ₘ ν
⊢ μ.singularPart ν = μ ↔ μ ⟂ₘ ν
have refine_2 : ∀ (h : μ ⟂ₘ ν), μ.singularPart ν = μ
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
h : μ.singularPart ν = μ
⊢ μ ⟂ₘ ν
have refine_1 : μ.singularPart ν ⟂ₘ ν
Tactic: rw [← h]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
h : μ ⟂ₘ ν
⊢ μ.singularPart ν = μ
have this : μ.HaveLebesgueDecomposition ν
Tactic: have := h.haveLebesgueDecomposition
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
h : μ ⟂ₘ ν
this : μ.HaveLebesgueDecomposition ν
| μ
have rw : μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
Tactic: rw [← singularPart_add_rnDeriv μ ν]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
h : μ ⟂ₘ ν
this : μ.HaveLebesgueDecomposition ν
⊢ μ.singularPart ν = μ
have refine_2 : μ.singularPart ν = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
Tactic: conv_rhs => rw [← singularPart_add_rnDeriv μ ν]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
h : μ ⟂ₘ ν
this : μ.HaveLebesgueDecomposition ν
⊢ μ.singularPart ν = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
have refine_2 : μ.singularPart ν = μ.singularPart ν + 0
Tactic: rw [(withDensity_rnDeriv_eq_zero _ _).mpr h, add_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
h : μ ⟂ₘ ν
this : μ.HaveLebesgueDecomposition ν
refine_2 : μ.singularPart ν = μ.singularPart ν + 0
⊢ μ.singularPart ν = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
have refine_2₁ : μ.singularPart ν = μ.singularPart ν
Tactic: rw [(withDensity_rnDeriv_eq_zero _ _).mpr h, add_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
⊢ (μ.singularPart ν).singularPart ν = μ.singularPart ν
have rw : μ.singularPart ν ⟂ₘ ν
Tactic: rw [Measure.singularPart_eq_self]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ∫⁻ (x : α) in s, μ.rnDeriv ν x ∂ν < ∞
have pos : ∀ (hl : μ.HaveLebesgueDecomposition ν), ∫⁻ (x : α) in s, μ.rnDeriv ν x ∂ν < ∞
Tactic: by_cases hl : HaveLebesgueDecomposition μ ν
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
pos : ∀ (hl : μ.HaveLebesgueDecomposition ν), ∫⁻ (x : α) in s, μ.rnDeriv ν x ∂ν < ∞
⊢ ∫⁻ (x : α) in s, μ.rnDeriv ν x ∂ν < ∞
have neg : ∀ (hl : ¬μ.HaveLebesgueDecomposition ν), ∫⁻ (x : α) in s, μ.rnDeriv ν x ∂ν < ∞
Tactic: by_cases hl : HaveLebesgueDecomposition μ ν
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hl : μ.HaveLebesgueDecomposition ν
⊢ ∫⁻ (x : α) in s, μ.rnDeriv ν x ∂ν < ∞
have pos : ∫⁻ (x : α) in toMeasurable μ s, μ.rnDeriv ν x ∂ν < ∞
Tactic: suffices (∫⁻ x in toMeasurable μ s, μ.rnDeriv ν x ∂ν) < ∞ from
      lt_of_le_of_lt (lintegral_mono_set (subset_toMeasurable _ _)) this
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hl : μ.HaveLebesgueDecomposition ν
⊢ ∫⁻ (x : α) in toMeasurable μ s, μ.rnDeriv ν x ∂ν < ∞
have pos : LT.lt (α := ℝ≥0∞) ((ν.withDensity (μ.rnDeriv ν) : (a : Set α) → ℝ≥0∞) (toMeasurable μ s) : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: rw [← withDensity_apply _ (measurableSet_toMeasurable _ _)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hl : μ.HaveLebesgueDecomposition ν
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ.singularPart ν : (a : Set α) → ℝ≥0∞) (toMeasurable μ s) : ℝ≥0∞)
      ((ν.withDensity (μ.rnDeriv ν) : (a : Set α) → ℝ≥0∞) (toMeasurable μ s) : ℝ≥0∞) =
    (μ : (a : Set α) → ℝ≥0∞) s
have rw : Eq (α := ℝ≥0∞) ((μ.singularPart ν + ν.withDensity (μ.rnDeriv ν) : (a : Set α) → ℝ≥0∞) (toMeasurable μ s) : ℝ≥0∞)
  ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [← Measure.add_apply, ← haveLebesgueDecomposition_add, measure_toMeasurable]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hl : μ.HaveLebesgueDecomposition ν
rw :
  Eq (α := ℝ≥0∞) ((μ.singularPart ν + ν.withDensity (μ.rnDeriv ν) : (a : Set α) → ℝ≥0∞) (toMeasurable μ s) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ.singularPart ν : (a : Set α) → ℝ≥0∞) (toMeasurable μ s) : ℝ≥0∞)
      ((ν.withDensity (μ.rnDeriv ν) : (a : Set α) → ℝ≥0∞) (toMeasurable μ s) : ℝ≥0∞) =
    (μ : (a : Set α) → ℝ≥0∞) s
have rw₁ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [← Measure.add_apply, ← haveLebesgueDecomposition_add, measure_toMeasurable]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hl : μ.HaveLebesgueDecomposition ν
rw :
  Eq (α := ℝ≥0∞) ((μ.singularPart ν + ν.withDensity (μ.rnDeriv ν) : (a : Set α) → ℝ≥0∞) (toMeasurable μ s) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
rw₁ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ.singularPart ν : (a : Set α) → ℝ≥0∞) (toMeasurable μ s) : ℝ≥0∞)
      ((ν.withDensity (μ.rnDeriv ν) : (a : Set α) → ℝ≥0∞) (toMeasurable μ s) : ℝ≥0∞) =
    (μ : (a : Set α) → ℝ≥0∞) s
have rw₂ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [← Measure.add_apply, ← haveLebesgueDecomposition_add, measure_toMeasurable]