no goals
α : Type u
β : Type v
ι : Sort w
γ : Type x
s✝ t : Set α
a : α
hs : Set.Finite s✝
ht : Set.Finite t
s : Finset α
⊢ s ⊂ Finite.toFinset ht ↔ ↑s ⊂ t
rw [← Finset.coe_ssubset, Finite.coe_toFinset]