simp only [List.mem_map, mem_elems, true_and]
α : Type u
β : Type v
inst✝¹ : BishopFin α
inst✝ : BishopFin β
f : α → β
f_surj : ∀ (b : β), ∃ a, f a = b
b : β
a✝ : b ∈ elems β
⊢ b ∈ List.map f (elems α)
α : Type u
β : Type v
inst✝¹ : BishopFin α
inst✝ : BishopFin β
f : α → β
f_surj : ∀ (b : β), ∃ a, f a = b
b : β
a✝ : b ∈ elems β
⊢ ∃ a, f a = b