case pos
α : Type u_1
β : Type ?u.44567
m : MeasurableSpace α
μ✝ ν✝ μ ν : Measure α
r : ℝ≥0
hr : r = 0
⊢ singularPart (r • μ) ν = r • singularPart μ ν

case neg
α : Type u_1
β : Type ?u.44567
m : MeasurableSpace α
μ✝ ν✝ μ ν : Measure α
r : ℝ≥0
hr : ¬r = 0
⊢ singularPart (r • μ) ν = r • singularPart μ ν
α : Type u_1
β : Type ?u.44567
m : MeasurableSpace α
μ✝ ν✝ μ ν : Measure α
r : ℝ≥0
⊢ singularPart (r • μ) ν = r • singularPart μ ν
by_cases hr : r = 0
case pos
α : Type u_1
β : Type ?u.44567
m : MeasurableSpace α
μ✝ ν✝ μ ν : Measure α
r : ℝ≥0
hr : ¬r = 0
hl : HaveLebesgueDecomposition μ ν
⊢ singularPart (r • μ) ν = r • singularPart μ ν

case neg
α : Type u_1
β : Type ?u.44567
m : MeasurableSpace α
μ✝ ν✝ μ ν : Measure α
r : ℝ≥0
hr : ¬r = 0
hl : ¬HaveLebesgueDecomposition μ ν
⊢ singularPart (r • μ) ν = r • singularPart μ ν
case neg
α : Type u_1
β : Type ?u.44567
m : MeasurableSpace α
μ✝ ν✝ μ ν : Measure α
r : ℝ≥0
hr : ¬r = 0
⊢ singularPart (r • μ) ν = r • singularPart μ ν
by_cases hl : HaveLebesgueDecomposition μ ν
no goals
case pos
α : Type u_1
β : Type ?u.44567
m : MeasurableSpace α
μ✝ ν✝ μ ν : Measure α
r : ℝ≥0
hr : r = 0
⊢ singularPart (r • μ) ν = r • singularPart μ ν
rw [hr, zero_smul, zero_smul, singularPart_zero]
case pos
α : Type u_1
β : Type ?u.44567
m : MeasurableSpace α
μ✝ ν✝ μ ν : Measure α
r : ℝ≥0
hr : ¬r = 0
hl this : HaveLebesgueDecomposition μ ν
⊢ singularPart (r • μ) ν = r • singularPart μ ν
case pos
α : Type u_1
β : Type ?u.44567
m : MeasurableSpace α
μ✝ ν✝ μ ν : Measure α
r : ℝ≥0
hr : ¬r = 0
hl : HaveLebesgueDecomposition μ ν
⊢ singularPart (r • μ) ν = r • singularPart μ ν
haveI := hl
case pos
α : Type u_1
β : Type ?u.44567
m : MeasurableSpace α
μ✝ ν✝ μ ν : Measure α
r : ℝ≥0
hr : ¬r = 0
hl this : HaveLebesgueDecomposition μ ν
⊢ r • μ = ↑r • singularPart μ ν + withDensity ν (↑r • rnDeriv μ ν)
case pos
α : Type u_1
β : Type ?u.44567
m : MeasurableSpace α
μ✝ ν✝ μ ν : Measure α
r : ℝ≥0
hr : ¬r = 0
hl this : HaveLebesgueDecomposition μ ν
⊢ singularPart (r • μ) ν = r • singularPart μ ν
refine'
  (eq_singularPart ((measurable_rnDeriv μ ν).const_smul (r : ℝ≥0∞))
      (MutuallySingular.smul r (haveLebesgueDecomposition_spec _ _).2.1) _).symm
no goals
case pos
α : Type u_1
β : Type ?u.44567
m : MeasurableSpace α
μ✝ ν✝ μ ν : Measure α
r : ℝ≥0
hr : ¬r = 0
hl this : HaveLebesgueDecomposition μ ν
⊢ r • μ = ↑r • singularPart μ ν + withDensity ν (↑r • rnDeriv μ ν)
rw [withDensity_smul _ (measurable_rnDeriv _ _), ← smul_add,
  ← haveLebesgueDecomposition_add μ ν, ENNReal.smul_def]
case neg.hnc
α : Type u_1
β : Type ?u.44567
m : MeasurableSpace α
μ✝ ν✝ μ ν : Measure α
r : ℝ≥0
hr : ¬r = 0
hl : ¬HaveLebesgueDecomposition μ ν
⊢ ¬HaveLebesgueDecomposition (r • μ) ν
case neg
α : Type u_1
β : Type ?u.44567
m : MeasurableSpace α
μ✝ ν✝ μ ν : Measure α
r : ℝ≥0
hr : ¬r = 0
hl : ¬HaveLebesgueDecomposition μ ν
⊢ singularPart (r • μ) ν = r • singularPart μ ν
rw [singularPart, singularPart, dif_neg hl, dif_neg, smul_zero]
case neg.hnc
α : Type u_1
β : Type ?u.44567
m : MeasurableSpace α
μ✝ ν✝ μ ν : Measure α
r : ℝ≥0
hr : ¬r = 0
hl : ¬HaveLebesgueDecomposition μ ν
hl' : HaveLebesgueDecomposition (r • μ) ν
⊢ HaveLebesgueDecomposition μ ν
case neg.hnc
α : Type u_1
β : Type ?u.44567
m : MeasurableSpace α
μ✝ ν✝ μ ν : Measure α
r : ℝ≥0
hr : ¬r = 0
hl : ¬HaveLebesgueDecomposition μ ν
⊢ ¬HaveLebesgueDecomposition (r • μ) ν
refine' fun hl' => hl _
case neg.hnc
α : Type u_1
β : Type ?u.44567
m : MeasurableSpace α
μ✝ ν✝ μ ν : Measure α
r : ℝ≥0
hr : ¬r = 0
hl : ¬HaveLebesgueDecomposition μ ν
hl' : HaveLebesgueDecomposition (r • μ) ν
⊢ HaveLebesgueDecomposition (r⁻¹ • r • μ) ν
case neg.hnc
α : Type u_1
β : Type ?u.44567
m : MeasurableSpace α
μ✝ ν✝ μ ν : Measure α
r : ℝ≥0
hr : ¬r = 0
hl : ¬HaveLebesgueDecomposition μ ν
hl' : HaveLebesgueDecomposition (r • μ) ν
⊢ HaveLebesgueDecomposition μ ν
rw [← inv_smul_smul₀ hr μ]
no goals
case neg.hnc
α : Type u_1
β : Type ?u.44567
m : MeasurableSpace α
μ✝ ν✝ μ ν : Measure α
r : ℝ≥0
hr : ¬r = 0
hl : ¬HaveLebesgueDecomposition μ ν
hl' : HaveLebesgueDecomposition (r • μ) ν
⊢ HaveLebesgueDecomposition (r⁻¹ • r • μ) ν
exact @Measure.haveLebesgueDecomposition_smul _ _ _ _ hl' _