simp_rw [ext_iff, setOf_forall]
α : Type u_1
Ω : Type u_2
inst✝² : MeasurableSpace Ω
X Y : Ω → Set α
μ : Measure Ω
p q : ℝ≥0
hX : IsBernoulliSeq X p μ
hY : IsBernoulliSeq Y q μ
inst✝¹ : IsProbabilityMeasure μ
inst✝ : Fintype α
s : Finset α
⊢ μ {ω | {a | a ∈ X ω} = ↑s} = ↑p ^ s.card * (1 - ↑p) ^ (card α - s.card)
α : Type u_1
Ω : Type u_2
inst✝² : MeasurableSpace Ω
X Y : Ω → Set α
μ : Measure Ω
p q : ℝ≥0
hX : IsBernoulliSeq X p μ
hY : IsBernoulliSeq Y q μ
inst✝¹ : IsProbabilityMeasure μ
inst✝ : Fintype α
s : Finset α
⊢ μ (⋂ i, {x | i ∈ {a | a ∈ X x} ↔ i ∈ ↑s}) = ↑p ^ s.card * (1 - ↑p) ^ (card α - s.card)