simp only [hi, ← compl_setOf, prob_compl_eq_one_sub₀, mem_setOf_eq, Finset.mem_coe,
  iff_false_iff, hX.nullMeasurableSet, hX.meas_apply]
α : 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 : α
hi : a ∉ s
⊢ μ {x | a ∈ {a | a ∈ X x} ↔ a ∈ ↑s} = 1 - ↑p
no goals