mathlib

7ee73e4a - feat(data/fintype/basic): Constructing an equivalence from a left inverse (#14816)

feat(data/fintype/basic): Constructing an equivalence from a left inverse (#14816) When `f : α → β`, `g : β → α` are inverses one way and `card α ≤ card β`, then they form an equivalence.