Lean4
/-- `mon_tauto` is a simp set to prove tautologies about morphisms from some (tensor) power of `M`
to `M`, where `M` is a (commutative) monoid object in a (braided) monoidal category.
**This `simp` set is incompatible with the standard simp set.**
If you want to use it, make sure to add the following to your simp call to disable the problematic
default simp lemmas:
```
-MonoidalCategory.whiskerLeft_id, -MonoidalCategory.id_whiskerRight,
-MonoidalCategory.tensor_comp, -MonoidalCategory.tensor_comp_assoc,
-MonObj.mul_assoc, -MonObj.mul_assoc_assoc
```
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, which is why it cannot be used concurrently with
some of the simp lemmas in the standard simp set:
* It eliminates all mentions of whiskers by rewriting them to tensored homs,
which goes against `whiskerLeft_id` and `id_whiskerRight`:
`X ◁ f = 𝟙 X ⊗ₘ f`, `f ▷ X = 𝟙 X ⊗ₘ f`.
This goes against `whiskerLeft_id` and `id_whiskerRight` in the standard simp set.
* It collapses compositions of tensored homs to the tensored hom of the compositions,
which goes against `tensor_comp`:
`(f₁ ⊗ₘ g₁) ≫ (f₂ ⊗ₘ g₂) = (f₁ ≫ f₂) ⊗ₘ (g₁ ≫ g₂)`. TODO: Isn't this direction Just Better?
* It cancels the associators against multiplications,
which goes against `mul_assoc`:
`(α_ M M M).hom ≫ (𝟙 M ⊗ₘ μ) ≫ μ = (μ ⊗ₘ 𝟙 M) ≫ μ`,
`(α_ M M M).inv ≫ (μ ⊗ₘ 𝟙 M) ≫ μ = (𝟙 M ⊗ₘ μ) ≫ μ`
* It unfolds non-primitive coherence isomorphisms, like the tensor strengths `tensorμ`, `tensorδ`.
-/
@[attr_parser 1000]
public meta def mon_tauto : Lean.ParserDescr✝ :=
ParserDescr.node✝ `Parser.Attr.mon_tauto 1022
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen (ParserDescr.nonReservedSymbol✝ "mon_tauto" false✝)
(ParserDescr.unary✝ `optional
(ParserDescr.binary✝ `orelse Lean.Parser.Tactic.simpPre Lean.Parser.Tactic.simpPost)))
(ParserDescr.unary✝ `optional
(ParserDescr.unary✝ `patternIgnore
(ParserDescr.binary✝ `orelse (ParserDescr.nodeWithAntiquot✝ "← " `token.«← » (ParserDescr.symbol✝ "← "))
(ParserDescr.nodeWithAntiquot✝ "<- " `token.«<- » (ParserDescr.symbol✝ "<- "))))))
(ParserDescr.unary✝ `optional (ParserDescr.cat✝ `prio 0)))
