left_inverse imples ` α ≃ set.range f`

Stream: Is there code for X?

[Eric Wieser]

Do we have a computable version of docs#equiv.set.range?

def function.left_inverse.equiv_range {α β : Sort*} {f' : β → α} {f : α → β} (hf : function.left_inverse f' f):
  α ≃ set.range f :=
{ to_fun := λ a, ⟨f a, a, rfl⟩,
  inv_fun := λ b, f' b,
  left_inv := hf,
  right_inv := λ ⟨b, a, ha⟩, subtype.eq $ show f (f' b) = b,
    from (ha ▸ hf a : f' b = a).symm ▸ ha }

[Eric Wieser]

I'll take silence as "no", pr'd as #6821. We have similar definitions as docs#linear_equiv.of_left_inverse and docs#ring_equiv.of_left_inverse, so I went for the name equiv.set.range_of_injective