Commit 2024-07-14 21:27 f7124c87

View on Github →

feat(Tactic/CategoryTheory): normalization in monoidal categories (#11133)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Tactic.lean

Created Mathlib/Tactic/CategoryTheory/Monoidal.lean

added def Mathlib.Tactic.Monoidal.Atom.src

added def Mathlib.Tactic.Monoidal.Atom.tgt

added structure Mathlib.Tactic.Monoidal.Atom

added structure Mathlib.Tactic.Monoidal.Atom₁

added structure Mathlib.Tactic.Monoidal.Context

added def Mathlib.Tactic.Monoidal.Mor₁.e

added def Mathlib.Tactic.Monoidal.Mor₁.toList

added inductive Mathlib.Tactic.Monoidal.Mor₁

added def Mathlib.Tactic.Monoidal.NormalExpr.associator

added def Mathlib.Tactic.Monoidal.NormalExpr.associatorInv

added def Mathlib.Tactic.Monoidal.NormalExpr.e

added def Mathlib.Tactic.Monoidal.NormalExpr.leftUnitor

added def Mathlib.Tactic.Monoidal.NormalExpr.leftUnitorInv

added def Mathlib.Tactic.Monoidal.NormalExpr.of

added def Mathlib.Tactic.Monoidal.NormalExpr.ofExpr

added def Mathlib.Tactic.Monoidal.NormalExpr.rightUnitor

added def Mathlib.Tactic.Monoidal.NormalExpr.rightUnitorInv

added def Mathlib.Tactic.Monoidal.NormalExpr.src

added def Mathlib.Tactic.Monoidal.NormalExpr.tgt

added def Mathlib.Tactic.Monoidal.NormalExpr.toList

added inductive Mathlib.Tactic.Monoidal.NormalExpr

added structure Mathlib.Tactic.Monoidal.Result

added def Mathlib.Tactic.Monoidal.Structural.src

added def Mathlib.Tactic.Monoidal.Structural.tgt

added inductive Mathlib.Tactic.Monoidal.Structural

added def Mathlib.Tactic.Monoidal.StructuralAtom.e

added def Mathlib.Tactic.Monoidal.StructuralAtom.src

added def Mathlib.Tactic.Monoidal.StructuralAtom.tgt

added inductive Mathlib.Tactic.Monoidal.StructuralAtom

added def Mathlib.Tactic.Monoidal.WhiskerLeftExpr.atom

added def Mathlib.Tactic.Monoidal.WhiskerLeftExpr.e

added def Mathlib.Tactic.Monoidal.WhiskerLeftExpr.src

added def Mathlib.Tactic.Monoidal.WhiskerLeftExpr.tgt

added inductive Mathlib.Tactic.Monoidal.WhiskerLeftExpr

added def Mathlib.Tactic.Monoidal.WhiskerRightExpr.atom

added def Mathlib.Tactic.Monoidal.WhiskerRightExpr.e

added def Mathlib.Tactic.Monoidal.WhiskerRightExpr.src

added def Mathlib.Tactic.Monoidal.WhiskerRightExpr.tgt

added inductive Mathlib.Tactic.Monoidal.WhiskerRightExpr

added theorem Mathlib.Tactic.Monoidal.evalComp_cons

added theorem Mathlib.Tactic.Monoidal.evalComp_nil_cons

added theorem Mathlib.Tactic.Monoidal.evalComp_nil_nil

added theorem Mathlib.Tactic.Monoidal.evalWhiskerLeft_comp

added theorem Mathlib.Tactic.Monoidal.evalWhiskerLeft_id

added theorem Mathlib.Tactic.Monoidal.evalWhiskerLeft_nil

added theorem Mathlib.Tactic.Monoidal.evalWhiskerLeft_of_cons

added theorem Mathlib.Tactic.Monoidal.evalWhiskerRight_comp

added theorem Mathlib.Tactic.Monoidal.evalWhiskerRight_cons_of_of

added theorem Mathlib.Tactic.Monoidal.evalWhiskerRight_cons_whisker

added theorem Mathlib.Tactic.Monoidal.evalWhiskerRight_id

added theorem Mathlib.Tactic.Monoidal.evalWhiskerRight_nil

added theorem Mathlib.Tactic.Monoidal.eval_comp

added theorem Mathlib.Tactic.Monoidal.eval_monoidalComp

added theorem Mathlib.Tactic.Monoidal.eval_of

added theorem Mathlib.Tactic.Monoidal.eval_whiskerLeft

added theorem Mathlib.Tactic.Monoidal.eval_whiskerRight

added def Mathlib.Tactic.Monoidal.isTensorObj?

added def Mathlib.Tactic.Monoidal.isTensorUnit?

added def Mathlib.Tactic.Monoidal.mkContext

added def Mathlib.Tactic.Monoidal.src

added def Mathlib.Tactic.Monoidal.structuralAtom?

added def Mathlib.Tactic.Monoidal.structuralOfMonoidalComp

added def Mathlib.Tactic.Monoidal.tgt

added def mkEq

added theorem mk_eq

Created test/CategoryTheory/Monoidal.lean