no goals
α : Type u_1
β : Type ?u.85081
γ : Type ?u.85084
s t : Set α
inst✝¹ : Fintype ↑s
inst✝ : Fintype ↑t
⊢ toFinset s ⊂ toFinset t ↔ s ⊂ t
simp only [Finset.ssubset_def, toFinset_subset_toFinset, ssubset_def]