case intro
α : Type u_1
β : Type ?u.59809
γ : Type ?u.59812
inst✝⁴ : Finite α
p q : α → Prop
inst✝³ : Fintype { x // p x }
inst✝² : Fintype { x // ¬p x }
inst✝¹ : Fintype { x // q x }
inst✝ : Fintype { x // ¬q x }
h : card { x // p x } = card { x // q x }
val✝ : Fintype α
⊢ card { x // ¬p x } = card { x // ¬q x }
α : Type u_1
β : Type ?u.59809
γ : Type ?u.59812
inst✝⁴ : Finite α
p q : α → Prop
inst✝³ : Fintype { x // p x }
inst✝² : Fintype { x // ¬p x }
inst✝¹ : Fintype { x // q x }
inst✝ : Fintype { x // ¬q x }
h : card { x // p x } = card { x // q x }
⊢ card { x // ¬p x } = card { x // ¬q x }
cases nonempty_fintype α
no goals
case intro
α : Type u_1
β : Type ?u.59809
γ : Type ?u.59812
inst✝⁴ : Finite α
p q : α → Prop
inst✝³ : Fintype { x // p x }
inst✝² : Fintype { x // ¬p x }
inst✝¹ : Fintype { x // q x }
inst✝ : Fintype { x // ¬q x }
h : card { x // p x } = card { x // q x }
val✝ : Fintype α
⊢ card { x // ¬p x } = card { x // ¬q x }
simp only [Fintype.card_subtype_compl, h]