awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
h : μ.HaveLebesgueDecomposition ν
⊢ Measurable (μ.rnDeriv ν)

Tactic:
(haveLebesgueDecomposition_spec μ ν).1

Premises used: And.left, MeasureTheory.Measure.haveLebesgueDecomposition_spec
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
h : μ.HaveLebesgueDecomposition ν
⊢ Measurable (μ.rnDeriv ν)

Tactic:
exact (haveLebesgueDecomposition_spec μ ν).1

Premises used: And.left, MeasureTheory.Measure.haveLebesgueDecomposition_spec
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
h : ¬μ.HaveLebesgueDecomposition ν
neg : Measurable.{u_1, 0} (α := α) (β := ℝ≥0∞) 0
⊢ Measurable (μ.rnDeriv ν)

Tactic:
rw [rnDeriv_of_not_haveLebesgueDecomposition h]

Premises used: MeasureTheory.Measure.rnDeriv_of_not_haveLebesgueDecomposition
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
h : ¬μ.HaveLebesgueDecomposition ν
⊢ Measurable.{u_1, 0} (α := α) (β := ℝ≥0∞) 0

Tactic:
measurable_zero

Premises used: measurable_zero
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
h : ¬μ.HaveLebesgueDecomposition ν
⊢ Measurable.{u_1, 0} (α := α) (β := ℝ≥0∞) 0

Tactic:
exact measurable_zero

Premises used: measurable_zero
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
pos : ∀ (h : μ.HaveLebesgueDecomposition ν), μ.singularPart ν ⟂ₘ ν
neg : ∀ (h : ¬μ.HaveLebesgueDecomposition ν), μ.singularPart ν ⟂ₘ ν
⊢ μ.singularPart ν ⟂ₘ ν

Tactic:
by_cases h : HaveLebesgueDecomposition μ ν

Premises used: MeasureTheory.Measure.HaveLebesgueDecomposition
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
h : μ.HaveLebesgueDecomposition ν
⊢ μ.singularPart ν ⟂ₘ ν

Tactic:
(haveLebesgueDecomposition_spec μ ν).2.1

Premises used: And.right, And.left, MeasureTheory.Measure.haveLebesgueDecomposition_spec
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
h : μ.HaveLebesgueDecomposition ν
⊢ μ.singularPart ν ⟂ₘ ν

Tactic:
exact (haveLebesgueDecomposition_spec μ ν).2.1

Premises used: And.right, And.left, MeasureTheory.Measure.haveLebesgueDecomposition_spec
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
h : ¬μ.HaveLebesgueDecomposition ν
neg : 0 ⟂ₘ ν
⊢ μ.singularPart ν ⟂ₘ ν

Tactic:
rw [singularPart_of_not_haveLebesgueDecomposition h]

Premises used: MeasureTheory.Measure.singularPart_of_not_haveLebesgueDecomposition
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
h : ¬μ.HaveLebesgueDecomposition ν
⊢ 0 ⟂ₘ ν

Tactic:
MutuallySingular.zero_left

Premises used: MeasureTheory.Measure.MutuallySingular.zero_left
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
h : ¬μ.HaveLebesgueDecomposition ν
⊢ 0 ⟂ₘ ν

Tactic:
exact MutuallySingular.zero_left

Premises used: MeasureTheory.Measure.MutuallySingular.zero_left
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
h : μ ⟂ₘ ν
⊢ μ = (μ, 0).1 + ν.withDensity (μ, 0).2

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
⊢ μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)

Tactic:
(haveLebesgueDecomposition_spec μ ν).2.2

Premises used: And.right, MeasureTheory.Measure.haveLebesgueDecomposition_spec
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
⊢ μ.singularPart ν + ν.withDensity (μ.rnDeriv ν) = μ

Tactic:
(haveLebesgueDecomposition_add μ ν).symm

Premises used: MeasureTheory.Measure.haveLebesgueDecomposition_add, Eq.symm
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
rw : μ.singularPart ν + ν.withDensity (μ.rnDeriv ν) = μ
rw₁ rw₂ : μ = μ
⊢ ν.withDensity (μ.rnDeriv ν) + μ.singularPart ν = μ

Tactic:
rw [add_comm, singularPart_add_rnDeriv]

Premises used: add_comm, MeasureTheory.Measure.singularPart_add_rnDeriv
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
⊢ HaveLebesgueDecomposition 0 ν

Tactic:
MutuallySingular.zero_left.haveLebesgueDecomposition

Premises used: MeasureTheory.Measure.MutuallySingular.zero_left, MeasureTheory.Measure.MutuallySingular.haveLebesgueDecomposition
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
⊢ μ.HaveLebesgueDecomposition 0

Tactic:
MutuallySingular.zero_right.haveLebesgueDecomposition

Premises used: MeasureTheory.Measure.MutuallySingular.zero_right, MeasureTheory.Measure.MutuallySingular.haveLebesgueDecomposition
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
⊢ μ = (0, 1).1 + μ.withDensity (0, 1).2

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ_1 ν : Measure α
ι : Type u_2
inst : Countable ι
μ : ι → Measure α
inst_1 : ∀ (i : ι), (μ i).HaveLebesgueDecomposition ν
⊢ Measurable.{u_1, 0} (α := α) (β := ℝ≥0∞) (∑' (i : ι), (μ i).rnDeriv ν)

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ_1 ν : Measure α
ι : Type u_2
inst : Countable ι
μ : ι → Measure α
inst_1 : ∀ (i : ι), (μ i).HaveLebesgueDecomposition ν
⊢ (sum fun (i : ι) ↦ (μ i).singularPart ν, ∑' (i : ι), (μ i).rnDeriv ν).1 ⟂ₘ ν

Tactic:
simp [mutuallySingular_singularPart]

Premises used: MeasureTheory.Measure.mutuallySingular_singularPart
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ_1 ν : Measure α
ι : Type u_2
inst : Countable ι
μ : ι → Measure α
inst_1 : ∀ (i : ι), (μ i).HaveLebesgueDecomposition ν
⊢ sum μ =
    (sum fun (i : ι) ↦ (μ i).singularPart ν, ∑' (i : ι), (μ i).rnDeriv ν).1 +
      ν.withDensity (sum fun (i : ι) ↦ (μ i).singularPart ν, ∑' (i : ι), (μ i).rnDeriv ν).2

Tactic:
simp [withDensity_tsum, measurable_rnDeriv, Measure.sum_add_sum, singularPart_add_rnDeriv]

Premises used: MeasureTheory.withDensity_tsum, MeasureTheory.Measure.sum_add_sum, MeasureTheory.Measure.singularPart_add_rnDeriv, MeasureTheory.Measure.measurable_rnDeriv
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν μ' : Measure α
inst : μ.HaveLebesgueDecomposition ν
inst_1 : μ'.HaveLebesgueDecomposition ν
⊢ ∀ (b : Bool), (bif b then μ else μ').HaveLebesgueDecomposition ν

Tactic:
simp [*]
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν μ' : Measure α
inst : μ.HaveLebesgueDecomposition ν
inst_1 : μ'.HaveLebesgueDecomposition ν
⊢ ∀ (b : Bool), (bif b then μ else μ').HaveLebesgueDecomposition ν

Tactic:
have : ∀ b, HaveLebesgueDecomposition (cond b μ μ') ν := by simp [*]
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν μ' : Measure α
inst : μ.HaveLebesgueDecomposition ν
inst_1 : μ'.HaveLebesgueDecomposition ν
this : ∀ (b : Bool), (bif b then μ else μ').HaveLebesgueDecomposition ν
⊢ (μ + μ').HaveLebesgueDecomposition ν

Tactic:
simpa using sum_left (cond · μ μ')

Premises used: cond, MeasureTheory.Measure.HaveLebesgueDecomposition.sum_left
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ_1 ν_1 μ ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
r : ℝ≥0∞
⊢ Measurable (μ.rnDeriv ν)

Tactic:
obtain ⟨hmeas, hsing, hadd⟩ := haveLebesgueDecomposition_spec μ ν

Premises used: MeasureTheory.Measure.haveLebesgueDecomposition_spec
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ_1 ν_1 μ ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
r : ℝ≥0∞
hmeas : Measurable (μ.rnDeriv ν)
⊢ μ.singularPart ν ⟂ₘ ν

Tactic:
obtain ⟨hmeas, hsing, hadd⟩ := haveLebesgueDecomposition_spec μ ν

Premises used: MeasureTheory.Measure.haveLebesgueDecomposition_spec
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ_1 ν_1 μ ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
r : ℝ≥0∞
hmeas : Measurable (μ.rnDeriv ν)
hsing : μ.singularPart ν ⟂ₘ ν
⊢ μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)

Tactic:
obtain ⟨hmeas, hsing, hadd⟩ := haveLebesgueDecomposition_spec μ ν

Premises used: MeasureTheory.Measure.haveLebesgueDecomposition_spec
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ_1 ν_1 μ ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
r : ℝ≥0∞
hmeas : Measurable (μ.rnDeriv ν)
hsing : μ.singularPart ν ⟂ₘ ν
hadd : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
⊢ ∃ (p : Measure α × (α → ℝ≥0∞)), Measurable p.2 ∧ p.1 ⟂ₘ ν ∧ r • μ = p.1 + ν.withDensity p.2

Tactic:
⟨⟨r • μ.singularPart ν, r • μ.rnDeriv ν⟩, hmeas.const_smul _, hsing.smul _, ?_⟩

Premises used: MeasureTheory.Measure.rnDeriv, MeasureTheory.Measure.MutuallySingular.smul, Prod.mk, Measurable.const_smul, MeasureTheory.Measure.singularPart, And.intro, Exists.intro, HSMul.hSMul
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ_1 ν_1 μ ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
r : ℝ≥0∞
hmeas : Measurable (μ.rnDeriv ν)
hsing : μ.singularPart ν ⟂ₘ ν
hadd : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
refine : r • μ = (r • μ.singularPart ν, r • μ.rnDeriv ν).1 + ν.withDensity (r • μ.singularPart ν, r • μ.rnDeriv ν).2
⊢ ∃ (p : Measure α × (α → ℝ≥0∞)), Measurable p.2 ∧ p.1 ⟂ₘ ν ∧ r • μ = p.1 + ν.withDensity p.2

Tactic:
refine ⟨⟨r • μ.singularPart ν, r • μ.rnDeriv ν⟩, hmeas.const_smul _, hsing.smul _, ?_⟩
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ_1 ν_1 μ ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
r : ℝ≥0∞
hmeas : Measurable (μ.rnDeriv ν)
hsing : μ.singularPart ν ⟂ₘ ν
hadd : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
rw : r • μ = r • μ.singularPart ν + r • ν.withDensity (μ.rnDeriv ν)
rw₁ : r • μ = r • (μ.singularPart ν + ν.withDensity (μ.rnDeriv ν))
rw₂ rw₃ : r • μ = r • μ
⊢ r • μ = r • μ.singularPart ν + ν.withDensity (r • μ.rnDeriv ν)

Tactic:
rw [withDensity_smul _ hmeas, ← smul_add, ← hadd]

Premises used: MeasureTheory.withDensity_smul, smul_add
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ_1 ν_1 μ ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
r : ℝ≥0
⊢ ((↑r : ℝ≥0∞) • μ).HaveLebesgueDecomposition ν

Tactic:
infer_instance
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ_1 ν_1 μ ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
r : ℝ≥0
⊢ Measurable (μ.rnDeriv ν)

Tactic:
obtain ⟨hmeas, hsing, hadd⟩ := haveLebesgueDecomposition_spec μ ν

Premises used: MeasureTheory.Measure.haveLebesgueDecomposition_spec
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ_1 ν_1 μ ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
r : ℝ≥0
hmeas : Measurable (μ.rnDeriv ν)
⊢ μ.singularPart ν ⟂ₘ ν

Tactic:
obtain ⟨hmeas, hsing, hadd⟩ := haveLebesgueDecomposition_spec μ ν

Premises used: MeasureTheory.Measure.haveLebesgueDecomposition_spec
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ_1 ν_1 μ ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
r : ℝ≥0
hmeas : Measurable (μ.rnDeriv ν)
hsing : μ.singularPart ν ⟂ₘ ν
⊢ μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)

Tactic:
obtain ⟨hmeas, hsing, hadd⟩ := haveLebesgueDecomposition_spec μ ν

Premises used: MeasureTheory.Measure.haveLebesgueDecomposition_spec
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ_1 ν_1 μ ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
r : ℝ≥0
hmeas : Measurable (μ.rnDeriv ν)
hsing : μ.singularPart ν ⟂ₘ ν
hadd : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
pos : ∀ (hr : r = 0), ∃ (p : Measure α × (α → ℝ≥0∞)), Measurable p.2 ∧ p.1 ⟂ₘ r • ν ∧ μ = p.1 + (r • ν).withDensity p.2
neg : ∀ (hr : ¬r = 0), ∃ (p : Measure α × (α → ℝ≥0∞)), Measurable p.2 ∧ p.1 ⟂ₘ r • ν ∧ μ = p.1 + (r • ν).withDensity p.2
⊢ ∃ (p : Measure α × (α → ℝ≥0∞)), Measurable p.2 ∧ p.1 ⟂ₘ r • ν ∧ μ = p.1 + (r • ν).withDensity p.2

Tactic:
by_cases hr : r = 0
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ_1 ν_1 μ ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
r : ℝ≥0
hmeas : Measurable (μ.rnDeriv ν)
hsing : μ.singularPart ν ⟂ₘ ν
hadd : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
hr : r = 0
⊢ (μ, 0).1 ⟂ₘ r • ν

Tactic:
simp [hr]
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ_1 ν_1 μ ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
r : ℝ≥0
hmeas : Measurable (μ.rnDeriv ν)
hsing : μ.singularPart ν ⟂ₘ ν
hadd : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
hr : r = 0
⊢ μ = (μ, 0).1 + (r • ν).withDensity (μ, 0).2

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ_1 ν_1 μ ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
r : ℝ≥0
hmeas : Measurable (μ.rnDeriv ν)
hsing : μ.singularPart ν ⟂ₘ ν
hadd : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
hr : r = 0
⊢ ∃ (p : Measure α × (α → ℝ≥0∞)), Measurable p.2 ∧ p.1 ⟂ₘ r • ν ∧ μ = p.1 + (r • ν).withDensity p.2

Tactic:
exact ⟨⟨μ, 0⟩, measurable_const, by simp [hr], by simp⟩
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ_1 ν_1 μ ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
r : ℝ≥0
hmeas : Measurable (μ.rnDeriv ν)
hsing : μ.singularPart ν ⟂ₘ ν
hadd : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
hr : ¬r = 0
⊢ ∃ (p : Measure α × (α → ℝ≥0∞)), Measurable p.2 ∧ p.1 ⟂ₘ r • ν ∧ μ = p.1 + (r • ν).withDensity p.2

Tactic:
⟨⟨μ.singularPart ν, r⁻¹ • μ.rnDeriv ν⟩, hmeas.const_smul _,
      hsing.mono_ac AbsolutelyContinuous.rfl smul_absolutelyContinuous, ?_⟩

Premises used: MeasureTheory.Measure.rnDeriv, Prod.mk, Measurable.const_smul, MeasureTheory.Measure.smul_absolutelyContinuous, MeasureTheory.Measure.singularPart, Inv.inv, And.intro, Exists.intro, MeasureTheory.Measure.AbsolutelyContinuous.rfl, HSMul.hSMul, MeasureTheory.Measure.MutuallySingular.mono_ac
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ_1 ν_1 μ ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
r : ℝ≥0
hmeas : Measurable (μ.rnDeriv ν)
hsing : μ.singularPart ν ⟂ₘ ν
hadd : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
hr : ¬r = 0
neg : μ = (μ.singularPart ν, r⁻¹ • μ.rnDeriv ν).1 + (r • ν).withDensity (μ.singularPart ν, r⁻¹ • μ.rnDeriv ν).2
⊢ ∃ (p : Measure α × (α → ℝ≥0∞)), Measurable p.2 ∧ p.1 ⟂ₘ r • ν ∧ μ = p.1 + (r • ν).withDensity p.2

Tactic:
refine ⟨⟨μ.singularPart ν, r⁻¹ • μ.rnDeriv ν⟩, hmeas.const_smul _,
      hsing.mono_ac AbsolutelyContinuous.rfl smul_absolutelyContinuous, ?_⟩
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ_1 ν_1 μ ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
r : ℝ≥0
hmeas : Measurable (μ.rnDeriv ν)
hsing : μ.singularPart ν ⟂ₘ ν
hadd : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
hr : ¬r = 0
⊢ r⁻¹ • μ.rnDeriv ν = (↑r⁻¹ : ℝ≥0∞) • μ.rnDeriv ν

Tactic:
simp [ENNReal.smul_def]

Premises used: ENNReal.smul_def
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ_1 ν_1 μ ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
r : ℝ≥0
hmeas : Measurable (μ.rnDeriv ν)
hsing : μ.singularPart ν ⟂ₘ ν
hadd : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
hr : ¬r = 0
⊢ r⁻¹ • μ.rnDeriv ν = (↑r⁻¹ : ℝ≥0∞) • μ.rnDeriv ν

Tactic:
have : r⁻¹ • rnDeriv μ ν = ((r⁻¹ : ℝ≥0) : ℝ≥0∞) • rnDeriv μ ν := by simp [ENNReal.smul_def]
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ_1 ν_1 μ ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
r : ℝ≥0
hmeas : Measurable (μ.rnDeriv ν)
hsing : μ.singularPart ν ⟂ₘ ν
hadd : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
hr : ¬r = 0
this : r⁻¹ • μ.rnDeriv ν = (↑r⁻¹ : ℝ≥0∞) • μ.rnDeriv ν
neg : μ = (μ.singularPart ν, (↑r : ℝ≥0∞)⁻¹ • μ.rnDeriv ν).1 + ν.withDensity (μ.rnDeriv ν)
neg₁ : (↑r : ℝ≥0∞) ≠ 0
neg₂ : (↑r : ℝ≥0∞) ≠ ∞
⊢ μ = (μ.singularPart ν, r⁻¹ • μ.rnDeriv ν).1 + (r • ν).withDensity (μ.singularPart ν, r⁻¹ • μ.rnDeriv ν).2

Tactic:
rw [this, withDensity_smul _ hmeas, ENNReal.smul_def r, withDensity_smul_measure,
      ← smul_assoc, smul_eq_mul, ENNReal.coe_inv hr, ENNReal.inv_mul_cancel, one_smul]

Premises used: ENNReal.coe_inv, ENNReal.smul_def, smul_assoc, one_smul, MeasureTheory.withDensity_smul_measure, ENNReal.inv_mul_cancel, MeasureTheory.withDensity_smul, smul_eq_mul
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ_1 ν_1 μ ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
r : ℝ≥0
hmeas : Measurable (μ.rnDeriv ν)
hsing : μ.singularPart ν ⟂ₘ ν
hadd : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
hr : ¬r = 0
this : r⁻¹ • μ.rnDeriv ν = (↑r⁻¹ : ℝ≥0∞) • μ.rnDeriv ν
⊢ μ = (μ.singularPart ν, (↑r : ℝ≥0∞)⁻¹ • μ.rnDeriv ν).1 + ν.withDensity (μ.rnDeriv ν)

Tactic:
hadd
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ_1 ν_1 μ ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
r : ℝ≥0
hmeas : Measurable (μ.rnDeriv ν)
hsing : μ.singularPart ν ⟂ₘ ν
hadd : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
hr : ¬r = 0
this : r⁻¹ • μ.rnDeriv ν = (↑r⁻¹ : ℝ≥0∞) • μ.rnDeriv ν
⊢ μ = (μ.singularPart ν, (↑r : ℝ≥0∞)⁻¹ • μ.rnDeriv ν).1 + ν.withDensity (μ.rnDeriv ν)

Tactic:
exact hadd
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ_1 ν_1 μ ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
r : ℝ≥0
hmeas : Measurable (μ.rnDeriv ν)
hsing : μ.singularPart ν ⟂ₘ ν
hadd : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
hr : ¬r = 0
this : r⁻¹ • μ.rnDeriv ν = (↑r⁻¹ : ℝ≥0∞) • μ.rnDeriv ν
⊢ (↑r : ℝ≥0∞) ≠ 0

Tactic:
simp [hr]
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ_1 ν_1 μ ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
r : ℝ≥0
hmeas : Measurable (μ.rnDeriv ν)
hsing : μ.singularPart ν ⟂ₘ ν
hadd : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
hr : ¬r = 0
this : r⁻¹ • μ.rnDeriv ν = (↑r⁻¹ : ℝ≥0∞) • μ.rnDeriv ν
⊢ (↑r : ℝ≥0∞) ≠ ∞

Tactic:
ENNReal.coe_ne_top

Premises used: ENNReal.coe_ne_top
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ_1 ν_1 μ ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
r : ℝ≥0
hmeas : Measurable (μ.rnDeriv ν)
hsing : μ.singularPart ν ⟂ₘ ν
hadd : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
hr : ¬r = 0
this : r⁻¹ • μ.rnDeriv ν = (↑r⁻¹ : ℝ≥0∞) • μ.rnDeriv ν
⊢ (↑r : ℝ≥0∞) ≠ ∞

Tactic:
exact ENNReal.coe_ne_top

Premises used: ENNReal.coe_ne_top
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
⊢ (μ.withDensity f).HaveLebesgueDecomposition μ

Tactic:
⟨⟨⟨0, f⟩, hf, .zero_left, (zero_add _).symm⟩⟩

Premises used: Prod.mk, zero_add, MeasureTheory.Measure.MutuallySingular.zero_left, And.intro, Exists.intro, OfNat.ofNat, Eq.symm, MeasureTheory.Measure.HaveLebesgueDecomposition.mk
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ_1 ν_1 μ ν : Measure α
⊢ (ν.withDensity (μ.rnDeriv ν)).HaveLebesgueDecomposition ν

Tactic:
haveLebesgueDecomposition_withDensity ν (measurable_rnDeriv _ _)

Premises used: MeasureTheory.Measure.haveLebesgueDecomposition_withDensity, MeasureTheory.Measure.measurable_rnDeriv
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
⊢ μ.singularPart ν = (μ.singularPart ν, 0).1 + ν.withDensity (μ.singularPart ν, 0).2

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
pos : ∀ (hl : μ.HaveLebesgueDecomposition ν), μ.singularPart ν ≤ μ
neg : ∀ (hl : ¬μ.HaveLebesgueDecomposition ν), μ.singularPart ν ≤ μ
⊢ μ.singularPart ν ≤ μ

Tactic:
by_cases hl : HaveLebesgueDecomposition μ ν

Premises used: MeasureTheory.Measure.HaveLebesgueDecomposition
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
hl : μ.HaveLebesgueDecomposition ν
rw : μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
| μ

Tactic:
rw [haveLebesgueDecomposition_add μ ν]

Premises used: MeasureTheory.Measure.haveLebesgueDecomposition_add
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
hl : μ.HaveLebesgueDecomposition ν
pos : μ.singularPart ν ≤ μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
⊢ μ.singularPart ν ≤ μ

Tactic:
conv_rhs => rw [haveLebesgueDecomposition_add μ ν]

Premises used: MeasureTheory.Measure.haveLebesgueDecomposition_add
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
hl : μ.HaveLebesgueDecomposition ν
⊢ μ.singularPart ν ≤ μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)

Tactic:
Measure.le_add_right le_rfl

Premises used: le_rfl, MeasureTheory.Measure.le_add_right
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
hl : μ.HaveLebesgueDecomposition ν
⊢ μ.singularPart ν ≤ μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)

Tactic:
exact Measure.le_add_right le_rfl

Premises used: le_rfl, MeasureTheory.Measure.le_add_right
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
hl : ¬μ.HaveLebesgueDecomposition ν
neg : 0 ≤ μ
⊢ μ.singularPart ν ≤ μ

Tactic:
rw [singularPart, dif_neg hl]

Premises used: dif_neg, MeasureTheory.Measure.singularPart
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
hl : ¬μ.HaveLebesgueDecomposition ν
⊢ 0 ≤ μ

Tactic:
Measure.zero_le μ

Premises used: MeasureTheory.Measure.zero_le
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
hl : ¬μ.HaveLebesgueDecomposition ν
⊢ 0 ≤ μ

Tactic:
exact Measure.zero_le μ

Premises used: MeasureTheory.Measure.zero_le
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
pos : ∀ (hl : μ.HaveLebesgueDecomposition ν), ν.withDensity (μ.rnDeriv ν) ≤ μ
neg : ∀ (hl : ¬μ.HaveLebesgueDecomposition ν), ν.withDensity (μ.rnDeriv ν) ≤ μ
⊢ ν.withDensity (μ.rnDeriv ν) ≤ μ

Tactic:
by_cases hl : HaveLebesgueDecomposition μ ν

Premises used: MeasureTheory.Measure.HaveLebesgueDecomposition
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
hl : μ.HaveLebesgueDecomposition ν
pos : ν.withDensity (μ.rnDeriv ν) ≤ μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
⊢ ν.withDensity (μ.rnDeriv ν) ≤ μ

Tactic:
conv_rhs => rw [haveLebesgueDecomposition_add μ ν]

Premises used: MeasureTheory.Measure.haveLebesgueDecomposition_add