inverse of injective functions

Stream: new members

[Alexander Bentkamp]

Given a function g : α → ɣ and an injective function f : β → ɣ, such that g.range ⊆ f.range, how can I access the function f⁻¹ ∘ g : α → β in Lean?

[Mario Carneiro]

there might be an equiv B ~= f.range in equiv.basic?

[Mario Carneiro]

alternatively, this seems like a good lemma on its own

[Mario Carneiro]

this is some kind of categorical thing about split monos

[Alexander Bentkamp]

Yes: equiv.set.range. That should do it. Thanks!