split_ifs <;> simp [ENNReal.sub_sub_cancel WithTop.one_ne_top (ENNReal.coe_le_coe.2 hp)]
case e_f.h
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
p : ℝ≥0
hp : p ≤ 1
b : Prop
this : ∀ (p : Prop), Finset.filter (fun q => ¬q ↔ p) Finset.univ = {¬p}
q : Prop
⊢ (if ¬q then ↑p else 1 - ↑p) = if q then ↑(1 - p) else 1 - ↑(1 - p)
no goals