theorem ProbabilityTheory.sum_meas_smul_cond_fiber' {Ω : Type u_1} {α : Type u_2} {m : MeasurableSpace Ω} [MeasurableSpace α] [MeasurableSingletonClass α] {X : Ω → α} (hX : Measurable X) [finX : FiniteRange X] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] : ∑ x ∈ FiniteRange.toFinset X, μ (X ⁻¹' {x}) • μ[|X ⁻¹' {x}] = μ

The law of total probability for a random variable taking finitely many values: a measure μ can be expressed as a linear combination of its conditional measures μ[|X ← x] on fibers of a random variable X valued in a fintype.