-- Mathlib/Probability/ConditionalProbability.lean
/-- 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. -/
lemma sum_meas_smul_cond_fiber {X : Ω → α} (hX : Measurable X) (μ : Measure Ω) [IsFiniteMeasure μ] :
    ∑ x, μ (X ⁻¹' {x}) • μ[|X ← x] = μ

Proof state:
case h
Ω : Type u_1
α : Type u_3
m : MeasurableSpace Ω
inst✝³ : Fintype α
inst✝² : MeasurableSpace α
inst✝¹ : DiscreteMeasurableSpace α
X : Ω → α
hX : Measurable X
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
E : Set Ω
hE : MeasurableSet E
⊢ (∑ x : α, μ (X ⁻¹' {x}) • μ[|X ⁻¹' {x}]) E = μ E

Tactic:
calc
  _ = ∑ x, μ (X ⁻¹' {x} ∩ E) := by
    simp only [Measure.coe_finset_sum, Measure.coe_smul, Finset.sum_apply,
      Pi.smul_apply, smul_eq_mul]
    simp_rw [mul_comm (μ _), cond_mul_eq_inter (hX (.singleton _))]
  _ = _ := by
    have : ⋃ x ∈ Finset.univ, X ⁻¹' {x} ∩ E = E := by ext; simp
    rw [← measure_biUnion_finset _ fun _ _ ↦ (hX (.singleton _)).inter hE, this]
    aesop (add simp [PairwiseDisjoint, Set.Pairwise, Function.onFun, disjoint_left])

Result:
no goals

Proof state:
Ω : Type u_1
α : Type u_3
m : MeasurableSpace Ω
inst✝³ : Fintype α
inst✝² : MeasurableSpace α
inst✝¹ : DiscreteMeasurableSpace α
X : Ω → α
hX : Measurable X
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
⊢ ∑ x : α, μ (X ⁻¹' {x}) • μ[|X ⁻¹' {x}] = μ

Tactic:
ext E hE

Result:
case h
Ω : Type u_1
α : Type u_3
m : MeasurableSpace Ω
inst✝³ : Fintype α
inst✝² : MeasurableSpace α
inst✝¹ : DiscreteMeasurableSpace α
X : Ω → α
hX : Measurable X
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
E : Set Ω
hE : MeasurableSet E
⊢ (∑ x : α, μ (X ⁻¹' {x}) • μ[|X ⁻¹' {x}]) E = μ E

Proof state:
Ω : Type u_1
α : Type u_3
m : MeasurableSpace Ω
inst✝³ : Fintype α
inst✝² : MeasurableSpace α
inst✝¹ : DiscreteMeasurableSpace α
X : Ω → α
hX : Measurable X
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
E : Set Ω
hE : MeasurableSet E
⊢ ∑ x : α, μ (X ⁻¹' {x}) * μ[E | X ⁻¹' {x}] = ∑ x : α, μ (X ⁻¹' {x} ∩ E)

Tactic:
simp_rw [mul_comm (μ _), cond_mul_eq_inter (hX (.singleton _))]

Result:
no goals

Proof state:
Ω : Type u_1
α : Type u_3
m : MeasurableSpace Ω
inst✝³ : Fintype α
inst✝² : MeasurableSpace α
inst✝¹ : DiscreteMeasurableSpace α
X : Ω → α
hX : Measurable X
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
E : Set Ω
hE : MeasurableSet E
this : ⋃ x ∈ Finset.univ, X ⁻¹' {x} ∩ E = E
⊢ ∑ x : α, μ (X ⁻¹' {x} ∩ E) = μ E

Tactic:
rw [← measure_biUnion_finset _ fun _ _ ↦ (hX (.singleton _)).inter hE, this]

Result:
Ω : Type u_1
α : Type u_3
m : MeasurableSpace Ω
inst✝³ : Fintype α
inst✝² : MeasurableSpace α
inst✝¹ : DiscreteMeasurableSpace α
X : Ω → α
hX : Measurable X
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
E : Set Ω
hE : MeasurableSet E
this : ⋃ x ∈ Finset.univ, X ⁻¹' {x} ∩ E = E
⊢ (↑Finset.univ).PairwiseDisjoint fun x => X ⁻¹' {x} ∩ E

Proof state:
Ω : Type u_1
α : Type u_3
m : MeasurableSpace Ω
inst✝³ : Fintype α
inst✝² : MeasurableSpace α
inst✝¹ : DiscreteMeasurableSpace α
X : Ω → α
hX : Measurable X
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
E : Set Ω
hE : MeasurableSet E
⊢ ∑ x : α, μ (X ⁻¹' {x} ∩ E) = μ E

Tactic:
have : ⋃ x ∈ Finset.univ, X ⁻¹' {x} ∩ E = E := by ext; simp

Result:
Ω : Type u_1
α : Type u_3
m : MeasurableSpace Ω
inst✝³ : Fintype α
inst✝² : MeasurableSpace α
inst✝¹ : DiscreteMeasurableSpace α
X : Ω → α
hX : Measurable X
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
E : Set Ω
hE : MeasurableSet E
this : ⋃ x ∈ Finset.univ, X ⁻¹' {x} ∩ E = E
⊢ ∑ x : α, μ (X ⁻¹' {x} ∩ E) = μ E

Proof state:
case h
Ω : Type u_1
α : Type u_3
m : MeasurableSpace Ω
inst✝³ : Fintype α
inst✝² : MeasurableSpace α
inst✝¹ : DiscreteMeasurableSpace α
X : Ω → α
hX : Measurable X
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
E : Set Ω
hE : MeasurableSet E
x✝ : Ω
⊢ x✝ ∈ ⋃ x ∈ Finset.univ, X ⁻¹' {x} ∩ E ↔ x✝ ∈ E

Tactic:
simp

Result:
no goals

Proof state:
Ω : Type u_1
α : Type u_3
m : MeasurableSpace Ω
inst✝³ : Fintype α
inst✝² : MeasurableSpace α
inst✝¹ : DiscreteMeasurableSpace α
X : Ω → α
hX : Measurable X
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
E : Set Ω
hE : MeasurableSet E
⊢ (∑ x : α, μ (X ⁻¹' {x}) • μ[|X ⁻¹' {x}]) E = ∑ x : α, μ (X ⁻¹' {x} ∩ E)

Tactic:
simp only [Measure.coe_finset_sum, Measure.coe_smul, Finset.sum_apply,
  Pi.smul_apply, smul_eq_mul]

Result:
Ω : Type u_1
α : Type u_3
m : MeasurableSpace Ω
inst✝³ : Fintype α
inst✝² : MeasurableSpace α
inst✝¹ : DiscreteMeasurableSpace α
X : Ω → α
hX : Measurable X
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
E : Set Ω
hE : MeasurableSet E
⊢ ∑ x : α, μ (X ⁻¹' {x}) * μ[E | X ⁻¹' {x}] = ∑ x : α, μ (X ⁻¹' {x} ∩ E)

Proof state:
Ω : Type u_1
α : Type u_3
m : MeasurableSpace Ω
inst✝³ : Fintype α
inst✝² : MeasurableSpace α
inst✝¹ : DiscreteMeasurableSpace α
X : Ω → α
hX : Measurable X
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
E : Set Ω
hE : MeasurableSet E
this : ⋃ x ∈ Finset.univ, X ⁻¹' {x} ∩ E = E
⊢ (↑Finset.univ).PairwiseDisjoint fun x => X ⁻¹' {x} ∩ E

Tactic:
aesop (add simp [PairwiseDisjoint, Set.Pairwise, Function.onFun, disjoint_left])

Result:
no goals

Proof state:
Ω : Type u_1
α : Type u_3
m : MeasurableSpace Ω
inst✝³ : Fintype α
inst✝² : MeasurableSpace α
inst✝¹ : DiscreteMeasurableSpace α
X : Ω → α
hX : Measurable X
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
E : Set Ω
hE : MeasurableSet E
⊢ ⋃ x ∈ Finset.univ, X ⁻¹' {x} ∩ E = E

Tactic:
ext

Result:
case h
Ω : Type u_1
α : Type u_3
m : MeasurableSpace Ω
inst✝³ : Fintype α
inst✝² : MeasurableSpace α
inst✝¹ : DiscreteMeasurableSpace α
X : Ω → α
hX : Measurable X
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
E : Set Ω
hE : MeasurableSet E
x✝ : Ω
⊢ x✝ ∈ ⋃ x ∈ Finset.univ, X ⁻¹' {x} ∩ E ↔ x✝ ∈ E