α : Type u_1
β : Type ?u.2715
m : MeasurableSpace α
μ✝ ν✝ μ ν : Measure α
h : HaveLebesgueDecomposition μ ν
⊢ Measurable (Classical.choose (_ : ∃ p, Measurable p.snd ∧ p.fst ⟂ₘ ν ∧ μ = p.fst + withDensity ν p.snd)).snd ∧
    (Classical.choose (_ : ∃ p, Measurable p.snd ∧ p.fst ⟂ₘ ν ∧ μ = p.fst + withDensity ν p.snd)).fst ⟂ₘ ν ∧
      μ =
        (Classical.choose (_ : ∃ p, Measurable p.snd ∧ p.fst ⟂ₘ ν ∧ μ = p.fst + withDensity ν p.snd)).fst +
          withDensity ν
            (Classical.choose (_ : ∃ p, Measurable p.snd ∧ p.fst ⟂ₘ ν ∧ μ = p.fst + withDensity ν p.snd)).snd
α : Type u_1
β : Type ?u.2715
m : MeasurableSpace α
μ✝ ν✝ μ ν : Measure α
h : HaveLebesgueDecomposition μ ν
⊢ Measurable (rnDeriv μ ν) ∧ singularPart μ ν ⟂ₘ ν ∧ μ = singularPart μ ν + withDensity ν (rnDeriv μ ν)
rw [singularPart, rnDeriv, dif_pos h, dif_pos h]
no goals
α : Type u_1
β : Type ?u.2715
m : MeasurableSpace α
μ✝ ν✝ μ ν : Measure α
h : HaveLebesgueDecomposition μ ν
⊢ Measurable (Classical.choose (_ : ∃ p, Measurable p.snd ∧ p.fst ⟂ₘ ν ∧ μ = p.fst + withDensity ν p.snd)).snd ∧
    (Classical.choose (_ : ∃ p, Measurable p.snd ∧ p.fst ⟂ₘ ν ∧ μ = p.fst + withDensity ν p.snd)).fst ⟂ₘ ν ∧
      μ =
        (Classical.choose (_ : ∃ p, Measurable p.snd ∧ p.fst ⟂ₘ ν ∧ μ = p.fst + withDensity ν p.snd)).fst +
          withDensity ν
            (Classical.choose (_ : ∃ p, Measurable p.snd ∧ p.fst ⟂ₘ ν ∧ μ = p.fst + withDensity ν p.snd)).snd
exact Classical.choose_spec h.lebesgue_decomposition