by_cases b <;> simp [*, hp.lt_iff_ne, tsub_eq_zero_iff_le]
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
p : ℝ≥0
hp : p ≤ 1
b✝ b : Prop
⊢ b ∈ (bernoulli' p hp).support ↔ b ∈ {b | if b then p ≠ 0 else p ≠ 1}
no goals