Theorem: Collection.subset_iff_set_subset_set (Logic/Vorspiel/Collection.lean)

State before:
β : Type u_1
α : Type u_2
inst✝ : Collection β α
a b : α
⊢ a ⊆ b ↔ set a ⊆ set b
Tactic:
simp [subset_iff, set]
State after:
no goals