Commit 2022-12-04 13:01 8aaf2807
View on Github →feat: port CategoryTheory.NatIso (#820)
- feat: port CategoryTheory.NatIso
- Initial fixes
- Additional porting notes
- Update to mathlib4 names
- Fix lints
- Swap tidy with aesop
- Use the correct lowerCamelCase
- Fix Category.assoc proofs. Explicitly prove ofComponents
- fix reassoc
- chore: fix aesop_cat wrapper for aesop
- .
- fix reassoc
- aesop rules
- cleanup