Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
This forward-ports: * leanprover-community/mathlib#18277. No action is needed as the proof was already fixed during porting. * leanprover-community/mathlib#18337. This was forward-ported in #1970 but the SHA was not updated. See the diff here: * [`data.fintype.basic`@`9003f28797c0664a49e4179487267c494477d853`..`d78597269638367c3863d40d45108f52207e03cf`](https://leanprover-community.github.io/mathlib-port-status/file/data/fintype/basic?range=9003f28797c0664a49e4179487267c494477d853..d78597269638367c3863d40d45108f52207e03cf)
- Loading branch information