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

State before:
β : Type u_1
α : Type u_2
inst✝ : Collection β α
z : β
a : α
h : Finite (cons z a)
⊢ a ⊆ cons z a
Tactic:
simp
State after:
no goals

State before:
β : Type u_1
α : Type u_2
inst✝ : Collection β α
z : β
a : α
⊢ Finite a → Finite (cons z a)
Tactic:
simpa [Finite] using Set.Finite.insert z
State after:
no goals