mathlib

3e011d66 - chore(equiv/*): add missing lemmas to traverse coercion diamonds (#6648)

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.