conv =>
  lhs
  rewrite [count_eq_card, card_eq_count_add_count_not (q ∘ Subtype.val)]
α : Type u
β : Type v
inst✝³ : BishopFin α
inst✝² : BishopFin β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
⊢ count p = (count fun a => p a ∧ q a) + count fun a => p a ∧ ¬q a
α : Type u
β : Type v
inst✝³ : BishopFin α
inst✝² : BishopFin β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
⊢ (count (q ∘ Subtype.val) + count fun a => ¬(q ∘ Subtype.val) a) =
    (count fun a => p a ∧ q a) + count fun a => p a ∧ ¬q a