Commit 2025-09-20 19:08 d5b94b66

refactor: simplify (f₁ ⊗ₘ f₂) ≫ (g₁ ⊗ₘ g₂) to (f₁ ≫ g₁) ⊗ₘ (f₂ ≫ g₂) (#26448) ... instead of the other way around. This is motivated by the fact that homs happening "in parallel" is a non-concept (time along a branch can always be reparametrised), while homs happening "in series" is a well-defined concept. One should not simp the well-defined concept into the non-concept but instead the other way around. This is also motivated by the advent of the mon_tauto simp set in #26057. From Toric