no goals
α : Type u_1
β : Type ?u.123371
γ : Type ?u.123374
p : α → Prop
inst✝ : DecidablePred p
s : Finset α
a : α
ha : p a
⊢ { val := a, property := ha } ∈ Finset.subtype p s ↔ ↑{ val := a, property := ha } ∈ s
simp [Finset.subtype, ha]