classical
have : (PMF.bernoulli' p hX.le_one).toMeasure ≠ 0 := NeZero.ne _
rw [← hX.map a, Measure.map] at this
refine' (Ne.dite_ne_right_iff fun hX' ↦ _).1 this
rw [Measure.mapₗ_ne_zero_iff hX'.measurable_mk]
haveI : Nonempty α := ⟨a⟩
exact hX.ne_zero
α : Type u_1
Ω : Type u_2
inst✝ : MeasurableSpace Ω
X Y : Ω → Set α
μ : Measure Ω
p q : ℝ≥0
hX : IsBernoulliSeq X p μ
hY : IsBernoulliSeq Y q μ
a : α
⊢ AEMeasurable (fun ω => a ∈ X ω) μ
no goals