Range of an injection between finsets

Stream: mathlib4

[Jeremy Tan]

Let e : s ↪ t where s,t are finsets. Is there a cleaner computable way to write the range of e than (t.filter fun y ↦ ∃ x : s, (e x).1 = y)?

[Yaël Dillies]

s.attach.map e?

[Edward van de Meent]

is Finset.map not computable?

[Edward van de Meent]

ah nevermind, i see i didn't quite understand the question.