(
simp only [count_eq_card]
apply card_eq_card_of_bij fun x => ⟨x.1.1, x.1.2, x.2⟩
. intro y; exact ⟨⟨⟨y.1,y.2.1⟩,y.2.2⟩,rfl⟩
. intro x₁ x₂
simp only [Subtype.mk.injEq]
exact Subtype.eq ∘ Subtype.eq
)
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
no goals