apply card_eq_card_of_bij fun x => ⟨x.1.1, x.1.2, x.2⟩
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 }
case refine_2.f_surj
α : Type u
β : Type v
inst✝³ : BishopFin α
inst✝² : BishopFin β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
⊢ ∀ (b : { a // p a ∧ ¬q a }), ∃ a, { val := a.val.val, property := (_ : p a.val.val ∧ ¬q a.val.val) } = b

case refine_2.f_inj
α : Type u
β : Type v
inst✝³ : BishopFin α
inst✝² : BishopFin β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
⊢ ∀ (a₁ a₂ : { a // ¬(q ∘ Subtype.val) a }),
    { val := a₁.val.val, property := (_ : p a₁.val.val ∧ ¬q a₁.val.val) } =
        { val := a₂.val.val, property := (_ : p a₂.val.val ∧ ¬q a₂.val.val) } →
      a₁ = a₂