mathlib3

9db59165 - fix(data/fintype/basic): fix `fintype_of_option_equiv` (#13466)

fix(data/fintype/basic): fix `fintype_of_option_equiv` (#13466) A type is a `fintype` if its successor (using `option`) is a `fintype` This fixes an error introduced in #13086.