mathlib3

2084baf2 - feat(set_theory/ordinal/basic): mark `type_fintype` as `simp` (#15194)

feat(set_theory/ordinal/basic): mark `type_fintype` as `simp` (#15194) This PR does the following: - move `type_fintype` along with some other lemmas from `set_theory/ordinal/arithmetic.lean` to `set_theory/ordinal/basic.lean`. - tag `type_fintype` as `simp`. - untag various lemmas as `simp`, since they can now be proved by it. Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>