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

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

Tactic:
refine (eq_singularPart ((measurable_rnDeriv μ ν).const_smul (r : ℝ≥0∞))
      (MutuallySingular.smul r (mutuallySingular_singularPart _ _)) ?_).symm

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

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

Tactic:
rw [hr, zero_smul, zero_smul, singularPart_zero]

Result:
no goals

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

Tactic:
refine fun hl' ↦ hl ?_

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

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

Tactic:
by_cases hl : HaveLebesgueDecomposition μ ν

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

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

Proof state:
case neg.hnc
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
r : ℝ≥0
hr : ¬r = 0
hl : ¬μ.HaveLebesgueDecomposition ν
hl' : (r • μ).HaveLebesgueDecomposition ν
⊢ μ.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' : (r • μ).HaveLebesgueDecomposition ν
⊢ (r⁻¹ • r • μ).HaveLebesgueDecomposition ν

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

Tactic:
by_cases hr : r = 0

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

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

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

Tactic:
infer_instance

Result:
no goals

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

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

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

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

Tactic:
rw [withDensity_smul _ (measurable_rnDeriv _ _), ← smul_add,
  ← haveLebesgueDecomposition_add μ ν, ENNReal.smul_def]

Result:
no goals