α : Type u_1
β : Type ?u.6560
γ : Type ?u.6563
inst✝ : Finite α
p : α → Prop
x : α
hx : ¬p x
this : Fintype α
⊢ Nat.card { x // p x } < Nat.card α
α : Type u_1
β : Type ?u.6560
γ : Type ?u.6563
inst✝ : Finite α
p : α → Prop
x : α
hx : ¬p x
⊢ Nat.card { x // p x } < Nat.card α
haveI := Fintype.ofFinite α
no goals
α : Type u_1
β : Type ?u.6560
γ : Type ?u.6563
inst✝ : Finite α
p : α → Prop
x : α
hx : ¬p x
this : Fintype α
⊢ Nat.card { x // p x } < Nat.card α
simpa only [Nat.card_eq_fintype_card, gt_iff_lt] using Fintype.card_subtype_lt hx