mathlib3

d997baa4 - refactor(logic/equiv/basic): remove `fin_equiv_subtype` (#14603)

refactor(logic/equiv/basic): remove `fin_equiv_subtype` (#14603) The types `fin n` and `{m // m < n}` are definitionally equal, so it doesn't make sense to have a dedicated equivalence between them (other than `equiv.refl`). We remove this equivalence and golf the places where it was used.