Theorem: Set.collection_finite_iff (Logic/Vorspiel/Collection.lean)

State before:
α : Type u_1
s : Set α
⊢ Collection.Finite s ↔ s.Finite
Tactic:
simp [Collection.Finite]
State after:
no goals