refine' (Ne.dite_ne_right_iff fun hX' ↦ _).1 this
α : Type u_1
Ω : Type u_2
inst✝ : MeasurableSpace Ω
X Y : Ω → Set α
μ : Measure Ω
p q : ℝ≥0
hX : IsBernoulliSeq X p μ
hY : IsBernoulliSeq Y q μ
a : α
this :
  (if hf : AEMeasurable (fun ω => a ∈ X ω) μ then (Measure.mapₗ (AEMeasurable.mk (fun ω => a ∈ X ω) hf)) μ else 0) ≠ 0
⊢ AEMeasurable (fun ω => a ∈ X ω) μ
α : Type u_1
Ω : Type u_2
inst✝ : MeasurableSpace Ω
X Y : Ω → Set α
μ : Measure Ω
p q : ℝ≥0
hX : IsBernoulliSeq X p μ
hY : IsBernoulliSeq Y q μ
a : α
this :
  (if hf : AEMeasurable (fun ω => a ∈ X ω) μ then (Measure.mapₗ (AEMeasurable.mk (fun ω => a ∈ X ω) hf)) μ else 0) ≠ 0
hX' : AEMeasurable (fun ω => a ∈ X ω) μ
⊢ (Measure.mapₗ (AEMeasurable.mk (fun ω => a ∈ X ω) hX')) μ ≠ 0