no goals
Ω : Type u_1
ι : Type ?u.1351878
inst✝ : MeasurableSpace Ω
s t : Set Ω
μ : MeasureTheory.Measure Ω
h : ↑↑μ (s ∩ t) = ↑↑μ s * ↑↑μ t
s1 t1 : Set Ω
hs1 : s1 ∈ {s}
ht1 : t1 ∈ {t}
⊢ ↑↑μ (s1 ∩ t1) = ↑↑μ s1 * ↑↑μ t1
rwa [Set.mem_singleton_iff.mp hs1, Set.mem_singleton_iff.mp ht1]