Commit 2025-08-28 09:43 41c70447

feat: mon_tauto, a simp set to prove tautologies about a monoid object (#26057) This simp set proves all tautologies involving (commutative) monoid objects in a (braided) monoidal category. The general algorithm it follows is to push the associators α_ and commutators β_ inwards until they cancel against the right sequence of multiplications. This approach is justified by the fact that a tautology in the language of (commutative) monoid objects "remembers" how it was proved: Every use of a (commutative) monoid object axiom inserts a unitor, associator or commutator, and proving a tautology simply amounts to undoing those moves as prescribed by the presence of unitors, associators and commutators in its expression. This simp set is opiniated about its normal form and therefore cannot be used concurrently to some of the simp lemmas in the standard simp set. As an example, we prove tensorμ M M M M ≫ (μ ⊗ₘ μ) ≫ μ = (μ ⊗ₘ μ) ≫ μ, the categorical equivalent of mul_mul_mul_comm. From Toric