simp only [count_eq_card]
case refine_2
α : Type u
β : Type v
inst✝³ : BishopFin α
inst✝² : BishopFin β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
⊢ (count fun a => ¬(q ∘ Subtype.val) a) = count fun a => p a ∧ ¬q a
case refine_2
α : Type u
β : Type v
inst✝³ : BishopFin α
inst✝² : BishopFin β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
⊢ card { a // ¬(q ∘ Subtype.val) a } = card { a // p a ∧ ¬q a }