α : Type u_1
β : Type ?u.19465
s t : Finset α
f : α → β
n : ℕ
p : α → Prop
inst✝ : DecidablePred p
h : card (filter p s) = card s
x : α
hx : x ∈ s ∧ p x
⊢ p x
α : Type u_1
β : Type ?u.19465
s t : Finset α
f : α → β
n : ℕ
p : α → Prop
inst✝ : DecidablePred p
h : card (filter p s) = card s
x : α
hx : x ∈ s
⊢ p x
rw [← eq_of_subset_of_card_le (s.filter_subset p) h.ge, mem_filter] at hx
no goals
α : Type u_1
β : Type ?u.19465
s t : Finset α
f : α → β
n : ℕ
p : α → Prop
inst✝ : DecidablePred p
h : card (filter p s) = card s
x : α
hx : x ∈ s ∧ p x
⊢ p x
exact hx.2