Theorem: Finset.mem_rangeOfFinite_iff (Logic/Vorspiel/Vorspiel.lean)

State before:
α : Type u
β : Type v
γ : Type w
ι : Sort v
inst✝ : Finite ι
f : ι → α
a : α
⊢ a ∈ rangeOfFinite f ↔ ∃ i, f i = a
Tactic:
simp[rangeOfFinite]
State after:
no goals