case pos
α : Type u_1
β : Type ?u.33482
m : MeasurableSpace α
μ✝ ν✝ μ ν : Measure α
h : HaveLebesgueDecomposition μ ν
⊢ singularPart μ ν ⟂ₘ ν

case neg
α : Type u_1
β : Type ?u.33482
m : MeasurableSpace α
μ✝ ν✝ μ ν : Measure α
h : ¬HaveLebesgueDecomposition μ ν
⊢ singularPart μ ν ⟂ₘ ν
α : Type u_1
β : Type ?u.33482
m : MeasurableSpace α
μ✝ ν✝ μ ν : Measure α
⊢ singularPart μ ν ⟂ₘ ν
by_cases h : HaveLebesgueDecomposition μ ν
no goals
case pos
α : Type u_1
β : Type ?u.33482
m : MeasurableSpace α
μ✝ ν✝ μ ν : Measure α
h : HaveLebesgueDecomposition μ ν
⊢ singularPart μ ν ⟂ₘ ν
exact (haveLebesgueDecomposition_spec μ ν).2.1
case neg
α : Type u_1
β : Type ?u.33482
m : MeasurableSpace α
μ✝ ν✝ μ ν : Measure α
h : ¬HaveLebesgueDecomposition μ ν
⊢ 0 ⟂ₘ ν
case neg
α : Type u_1
β : Type ?u.33482
m : MeasurableSpace α
μ✝ ν✝ μ ν : Measure α
h : ¬HaveLebesgueDecomposition μ ν
⊢ singularPart μ ν ⟂ₘ ν
rw [singularPart, dif_neg h]
no goals
case neg
α : Type u_1
β : Type ?u.33482
m : MeasurableSpace α
μ✝ ν✝ μ ν : Measure α
h : ¬HaveLebesgueDecomposition μ ν
⊢ 0 ⟂ₘ ν
exact MutuallySingular.zero_left