Commit 2024-12-05 09:31 498c8c34

refactor(Algebra/Category/ModuleCat): make ModuleCat.Hom a structure (#19511) This PR follows the approach of #19065 to solve painful definitional equalities problems by forbidding the identification of A ⟶ B and A →ₗ[R] B. These are not equal reducibly, so tactics get confused if one is replaced by the other. There seem to be a few regressions caused by defeq abuse that we were able to get away with previously, but some subtle elaboration differences made it evident. Otherwise the cost is inserting many .homs and asHoms. A few steps that might clean up the diff, but would be too much work to incorporate in this PR:

• Make the ext tactic pick up TensorProduct.ext again.
• Replace the defeq abuse between (restrictScalars f).obj M and M with explicit maps going back and forth. Overall quite a few proofs could be cleaned up at the cost of more bookkeeping.