Commit 2021-03-14 03:22 3e011d66

chore(equiv/*): add missing lemmas to traverse coercion diamonds (#6648) These don't have a preferred direction, but there are cases when they are definitely needed. The conversion paths commute as squares:

`→+` <-- `→+*` <-- `→ₐ[R]`
 ^         ^          ^
 |         |          |
`≃+` <-- `≃+*` <-- `≃ₐ[R]`

so we only need lemmas to swap within each square.