exact (add_le_add_left (mul_le_of_le_one_right' $ hY.le_one) _).trans_eq
  (add_tsub_cancel_of_le hX.le_one)
case h.e'_5
α : 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 μ
h : IndepFun X Y μ
⊢ p + (1 - p) * q ≤ 1
no goals