mathlib3

36d300ce - refactor(data/fintype/basic): drop 2 noncomputable instances (#15943)

refactor(data/fintype/basic): drop 2 noncomputable instances (#15943) Drop `fintype.of_subsingleton'` and `function.embedding.fintype'`. First, we should use `finite` instances instead of noncomputable `fintype` instances. Second, these instances created diamonds with non-primed versions.