mathlib3

8af7e08e - feat(data/fintype/basic): make subtype_of_fintype computable (#5919)

feat(data/fintype/basic): make subtype_of_fintype computable (#5919) This smokes out a few places downstream that are missing decidability hypotheses needed for the fintype instance to exist. Co-authored-by: Eric Wieser <wieser.eric@gmail.com>