-- Mathlib/MeasureTheory/Decomposition/Lebesgue.lean
theorem singularPart_smul_right (μ ν : Measure α) (r : ℝ≥0) (hr : r ≠ 0) :
    μ.singularPart (r • ν) = μ.singularPart ν

Proof state:
case h.e'_3.h.e'_6.h.e'_4.h
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
r : ℝ≥0
hr : r ≠ 0
hl : μ.HaveLebesgueDecomposition ν
x : α
⊢ (↑r • r⁻¹ • μ.rnDeriv ν) x = μ.rnDeriv ν x

Tactic:
simp only [Pi.smul_apply]

Result:
case h.e'_3.h.e'_6.h.e'_4.h
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
r : ℝ≥0
hr : r ≠ 0
hl : μ.HaveLebesgueDecomposition ν
x : α
⊢ ↑r • r⁻¹ • μ.rnDeriv ν x = μ.rnDeriv ν x

Proof state:
case neg
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
r : ℝ≥0
hr : r ≠ 0
hl : ¬μ.HaveLebesgueDecomposition ν
⊢ μ.singularPart (r • ν) = μ.singularPart ν

Tactic:
rw [singularPart, singularPart, dif_neg hl, dif_neg]

Result:
case neg.hnc
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
r : ℝ≥0
hr : r ≠ 0
hl : ¬μ.HaveLebesgueDecomposition ν
⊢ ¬μ.HaveLebesgueDecomposition (r • ν)

Proof state:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
r : ℝ≥0
hr : r ≠ 0
⊢ μ.singularPart (r • ν) = μ.singularPart ν

Tactic:
by_cases hl : HaveLebesgueDecomposition μ ν

Result:
case pos
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
r : ℝ≥0
hr : r ≠ 0
hl : μ.HaveLebesgueDecomposition ν
⊢ μ.singularPart (r • ν) = μ.singularPart ν

case neg
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
r : ℝ≥0
hr : r ≠ 0
hl : ¬μ.HaveLebesgueDecomposition ν
⊢ μ.singularPart (r • ν) = μ.singularPart ν

Proof state:
case pos.refine_2
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
r : ℝ≥0
hr : r ≠ 0
hl : μ.HaveLebesgueDecomposition ν
⊢ μ = μ.singularPart ν + ν.withDensity (↑r • r⁻¹ • μ.rnDeriv ν)

Tactic:
convert haveLebesgueDecomposition_add μ ν

Result:
case h.e'_3.h.e'_6.h.e'_4
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
r : ℝ≥0
hr : r ≠ 0
hl : μ.HaveLebesgueDecomposition ν
⊢ ↑r • r⁻¹ • μ.rnDeriv ν = μ.rnDeriv ν

Proof state:
case neg.hnc
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
r : ℝ≥0
hr : r ≠ 0
hl : ¬μ.HaveLebesgueDecomposition ν
hl' : μ.HaveLebesgueDecomposition (r • ν)
⊢ μ.HaveLebesgueDecomposition ν

Tactic:
rw [← inv_smul_smul₀ hr ν]

Result:
case neg.hnc
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
r : ℝ≥0
hr : r ≠ 0
hl : ¬μ.HaveLebesgueDecomposition ν
hl' : μ.HaveLebesgueDecomposition (r • ν)
⊢ μ.HaveLebesgueDecomposition (r⁻¹ • r • ν)

Proof state:
case pos.refine_2.hf
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
r : ℝ≥0
hr : r ≠ 0
hl : μ.HaveLebesgueDecomposition ν
⊢ Measurable (r⁻¹ • μ.rnDeriv ν)

Tactic:
exact (measurable_rnDeriv _ _).const_smul _

Result:
no goals

Proof state:
case h.e'_3.h.e'_6.h.e'_4.h
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
r : ℝ≥0
hr : r ≠ 0
hl : μ.HaveLebesgueDecomposition ν
x : α
⊢ ↑r • r⁻¹ • μ.rnDeriv ν x = μ.rnDeriv ν x

Tactic:
rw [← ENNReal.smul_def, smul_inv_smul₀ hr]

Result:
no goals

Proof state:
case neg.hnc
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
r : ℝ≥0
hr : r ≠ 0
hl : ¬μ.HaveLebesgueDecomposition ν
hl' : μ.HaveLebesgueDecomposition (r • ν)
⊢ μ.HaveLebesgueDecomposition (r⁻¹ • r • ν)

Tactic:
infer_instance

Result:
no goals

Proof state:
case pos
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
r : ℝ≥0
hr : r ≠ 0
hl : μ.HaveLebesgueDecomposition ν
⊢ μ.singularPart (r • ν) = μ.singularPart ν

Tactic:
refine (eq_singularPart ((measurable_rnDeriv μ ν).const_smul r⁻¹) ?_ ?_).symm

Result:
case pos.refine_1
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
r : ℝ≥0
hr : r ≠ 0
hl : μ.HaveLebesgueDecomposition ν
⊢ μ.singularPart ν ⟂ₘ r • ν

case pos.refine_2
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
r : ℝ≥0
hr : r ≠ 0
hl : μ.HaveLebesgueDecomposition ν
⊢ μ = μ.singularPart ν + (r • ν).withDensity (r⁻¹ • μ.rnDeriv ν)

Proof state:
case h.e'_3.h.e'_6.h.e'_4
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
r : ℝ≥0
hr : r ≠ 0
hl : μ.HaveLebesgueDecomposition ν
⊢ ↑r • r⁻¹ • μ.rnDeriv ν = μ.rnDeriv ν

Tactic:
ext x

Result:
case h.e'_3.h.e'_6.h.e'_4.h
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
r : ℝ≥0
hr : r ≠ 0
hl : μ.HaveLebesgueDecomposition ν
x : α
⊢ (↑r • r⁻¹ • μ.rnDeriv ν) x = μ.rnDeriv ν x

Proof state:
case pos.refine_1
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
r : ℝ≥0
hr : r ≠ 0
hl : μ.HaveLebesgueDecomposition ν
⊢ μ.singularPart ν ⟂ₘ r • ν

Tactic:
exact (mutuallySingular_singularPart μ ν).mono_ac AbsolutelyContinuous.rfl
  smul_absolutelyContinuous

Result:
no goals

Proof state:
case neg.hnc
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
r : ℝ≥0
hr : r ≠ 0
hl : ¬μ.HaveLebesgueDecomposition ν
⊢ ¬μ.HaveLebesgueDecomposition (r • ν)

Tactic:
refine fun hl' ↦ hl ?_

Result:
case neg.hnc
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
r : ℝ≥0
hr : r ≠ 0
hl : ¬μ.HaveLebesgueDecomposition ν
hl' : μ.HaveLebesgueDecomposition (r • ν)
⊢ μ.HaveLebesgueDecomposition ν

Proof state:
case pos.refine_2
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
r : ℝ≥0
hr : r ≠ 0
hl : μ.HaveLebesgueDecomposition ν
⊢ μ = μ.singularPart ν + ν.withDensity (↑r • r⁻¹ • μ.rnDeriv ν)

case pos.refine_2.hf
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
r : ℝ≥0
hr : r ≠ 0
hl : μ.HaveLebesgueDecomposition ν
⊢ Measurable (r⁻¹ • μ.rnDeriv ν)

Tactic:
swap

Result:
case pos.refine_2.hf
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
r : ℝ≥0
hr : r ≠ 0
hl : μ.HaveLebesgueDecomposition ν
⊢ Measurable (r⁻¹ • μ.rnDeriv ν)

case pos.refine_2
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
r : ℝ≥0
hr : r ≠ 0
hl : μ.HaveLebesgueDecomposition ν
⊢ μ = μ.singularPart ν + ν.withDensity (↑r • r⁻¹ • μ.rnDeriv ν)

Proof state:
case pos.refine_2
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
r : ℝ≥0
hr : r ≠ 0
hl : μ.HaveLebesgueDecomposition ν
⊢ μ = μ.singularPart ν + (r • ν).withDensity (r⁻¹ • μ.rnDeriv ν)

Tactic:
rw [ENNReal.smul_def r, withDensity_smul_measure, ← withDensity_smul]

Result:
case pos.refine_2
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
r : ℝ≥0
hr : r ≠ 0
hl : μ.HaveLebesgueDecomposition ν
⊢ μ = μ.singularPart ν + ν.withDensity (↑r • r⁻¹ • μ.rnDeriv ν)

case pos.refine_2.hf
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
r : ℝ≥0
hr : r ≠ 0
hl : μ.HaveLebesgueDecomposition ν
⊢ Measurable (r⁻¹ • μ.rnDeriv ν)