Commit 2024-09-18 01:47 6a73625d

View on Github →

feat(CategoryTheory): proof producing coherence tactic (#16852) See Zulip.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/CategoryTheory/Bicategory/Adjunction.lean

deleted def CategoryTheory.Bicategory.leftZigzag

deleted def CategoryTheory.Bicategory.leftZigzagIso

deleted def CategoryTheory.Bicategory.rightZigzag

deleted def CategoryTheory.Bicategory.rightZigzagIso

Modified Mathlib/CategoryTheory/Bicategory/Kan/Adjunction.lean

Modified Mathlib/CategoryTheory/Monoidal/Bimod.lean

Modified Mathlib/CategoryTheory/Monoidal/Braided/Basic.lean

Modified Mathlib/CategoryTheory/Monoidal/Center.lean

Modified Mathlib/CategoryTheory/Monoidal/CoherenceLemmas.lean

Modified Mathlib/CategoryTheory/Monoidal/Comon_.lean

Modified Mathlib/CategoryTheory/Monoidal/Hopf_.lean

Modified Mathlib/CategoryTheory/Monoidal/Mon_.lean

Modified Mathlib/CategoryTheory/Monoidal/Opposite.lean

Modified Mathlib/CategoryTheory/Monoidal/Rigid/Basic.lean

Modified Mathlib/CategoryTheory/Monoidal/Rigid/Braided.lean

Modified Mathlib/Tactic.lean

Modified Mathlib/Tactic/CategoryTheory/BicategoricalComp.lean

deleted def CategoryTheory.bicategoricalIso

Created Mathlib/Tactic/CategoryTheory/Bicategory/Basic.lean

added def Mathlib.Tactic.Bicategory.bicategory

added def Mathlib.Tactic.Bicategory.bicategoryNf

Created Mathlib/Tactic/CategoryTheory/Bicategory/Datatypes.lean

added structure Mathlib.Tactic.Bicategory.Context

added theorem Mathlib.Tactic.Bicategory.StructuralOfExpr_bicategoricalComp

added def Mathlib.Tactic.Bicategory.comp?

added def Mathlib.Tactic.Bicategory.id₁?

added def Mathlib.Tactic.Bicategory.mkContext?

added def Mathlib.Tactic.Bicategory.srcExpr

added def Mathlib.Tactic.Bicategory.srcExprOfIso

added theorem Mathlib.Tactic.Bicategory.structuralIsoOfExpr_comp

added theorem Mathlib.Tactic.Bicategory.structuralIsoOfExpr_whiskerLeft

added theorem Mathlib.Tactic.Bicategory.structuralIsoOfExpr_whiskerRight

added theorem Mathlib.Tactic.Bicategory.structuralIso_inv

added def Mathlib.Tactic.Bicategory.tgtExpr

added def Mathlib.Tactic.Bicategory.tgtExprOfIso

Created Mathlib/Tactic/CategoryTheory/Bicategory/Normalize.lean

added theorem Mathlib.Tactic.Bicategory.evalComp_cons

added theorem Mathlib.Tactic.Bicategory.evalComp_nil_cons

added theorem Mathlib.Tactic.Bicategory.evalComp_nil_nil

added theorem Mathlib.Tactic.Bicategory.evalWhiskerLeft_comp

added theorem Mathlib.Tactic.Bicategory.evalWhiskerLeft_id

added theorem Mathlib.Tactic.Bicategory.evalWhiskerLeft_nil

added theorem Mathlib.Tactic.Bicategory.evalWhiskerLeft_of_cons

added theorem Mathlib.Tactic.Bicategory.evalWhiskerRightAux_of

added theorem Mathlib.Tactic.Bicategory.evalWhiskerRight_comp

added theorem Mathlib.Tactic.Bicategory.evalWhiskerRight_cons_of_of

added theorem Mathlib.Tactic.Bicategory.evalWhiskerRight_cons_whisker

added theorem Mathlib.Tactic.Bicategory.evalWhiskerRight_id

added theorem Mathlib.Tactic.Bicategory.evalWhiskerRight_nil

added theorem Mathlib.Tactic.Bicategory.eval_bicategoricalComp

added theorem Mathlib.Tactic.Bicategory.eval_comp

added theorem Mathlib.Tactic.Bicategory.eval_monoidalComp

added theorem Mathlib.Tactic.Bicategory.eval_of

added theorem Mathlib.Tactic.Bicategory.eval_whiskerLeft

added theorem Mathlib.Tactic.Bicategory.eval_whiskerRight

Created Mathlib/Tactic/CategoryTheory/Bicategory/PureCoherence.lean

added theorem Mathlib.Tactic.Bicategory.mk_eq_of_naturality

added theorem Mathlib.Tactic.Bicategory.naturality_associator

added theorem Mathlib.Tactic.Bicategory.naturality_comp

added theorem Mathlib.Tactic.Bicategory.naturality_id

added theorem Mathlib.Tactic.Bicategory.naturality_inv

added theorem Mathlib.Tactic.Bicategory.naturality_leftUnitor

added theorem Mathlib.Tactic.Bicategory.naturality_rightUnitor

added theorem Mathlib.Tactic.Bicategory.naturality_whiskerLeft

added theorem Mathlib.Tactic.Bicategory.naturality_whiskerRight

added theorem Mathlib.Tactic.Bicategory.of_normalize_eq

added def Mathlib.Tactic.Bicategory.pureCoherence

Modified Mathlib/Tactic/CategoryTheory/BicategoryCoherence.lean

Modified Mathlib/Tactic/CategoryTheory/Coherence.lean

Created Mathlib/Tactic/CategoryTheory/Coherence/Basic.lean

added def Mathlib.Tactic.BicategoryLike.List.splitEvenOdd

added def Mathlib.Tactic.BicategoryLike.main

added theorem Mathlib.Tactic.BicategoryLike.mk_eq

added theorem Mathlib.Tactic.BicategoryLike.mk_eq_of_cons

added def Mathlib.Tactic.BicategoryLike.normalForm

added def Mathlib.Tactic.BicategoryLike.ofNormalizedEq

Created Mathlib/Tactic/CategoryTheory/Coherence/Datatypes.lean

added structure Mathlib.Tactic.BicategoryLike.Atom

added structure Mathlib.Tactic.BicategoryLike.AtomIso

added structure Mathlib.Tactic.BicategoryLike.Atom₁

added structure Mathlib.Tactic.BicategoryLike.CoherenceHom

added def Mathlib.Tactic.BicategoryLike.CoherenceM.run

added structure Mathlib.Tactic.BicategoryLike.IsoLift

added def Mathlib.Tactic.BicategoryLike.MonadMor₂Iso.associatorM'

added def Mathlib.Tactic.BicategoryLike.MonadMor₂Iso.coherenceHomM'

added def Mathlib.Tactic.BicategoryLike.MonadMor₂Iso.id₂M'

added def Mathlib.Tactic.BicategoryLike.MonadMor₂Iso.leftUnitorM'

added def Mathlib.Tactic.BicategoryLike.MonadMor₂Iso.rightUnitorM'

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

added def Mathlib.Tactic.BicategoryLike.Mor₁.src

added def Mathlib.Tactic.BicategoryLike.Mor₁.tgt

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

added inductive Mathlib.Tactic.BicategoryLike.Mor₁

added def Mathlib.Tactic.BicategoryLike.Mor₂.e

added def Mathlib.Tactic.BicategoryLike.Mor₂.isoLift?

added def Mathlib.Tactic.BicategoryLike.Mor₂.srcM

added def Mathlib.Tactic.BicategoryLike.Mor₂.tgtM

added inductive Mathlib.Tactic.BicategoryLike.Mor₂

added def Mathlib.Tactic.BicategoryLike.Mor₂Iso.e

added def Mathlib.Tactic.BicategoryLike.Mor₂Iso.srcM

added def Mathlib.Tactic.BicategoryLike.Mor₂Iso.tgtM

added inductive Mathlib.Tactic.BicategoryLike.Mor₂Iso

added def Mathlib.Tactic.BicategoryLike.NormalizedHom.consM

added def Mathlib.Tactic.BicategoryLike.NormalizedHom.e

added def Mathlib.Tactic.BicategoryLike.NormalizedHom.src

added def Mathlib.Tactic.BicategoryLike.NormalizedHom.tgt

added inductive Mathlib.Tactic.BicategoryLike.NormalizedHom

added def Mathlib.Tactic.BicategoryLike.Obj.e

added structure Mathlib.Tactic.BicategoryLike.Obj

added structure Mathlib.Tactic.BicategoryLike.State

added def Mathlib.Tactic.BicategoryLike.StructuralAtom.e

added def Mathlib.Tactic.BicategoryLike.StructuralAtom.srcM

added def Mathlib.Tactic.BicategoryLike.StructuralAtom.tgtM

added inductive Mathlib.Tactic.BicategoryLike.StructuralAtom

added def Mathlib.Tactic.BicategoryLike.mkContext

added def Mathlib.Tactic.BicategoryLike.normalizedHom.nilM

Created Mathlib/Tactic/CategoryTheory/Coherence/Normalize.lean

added structure Mathlib.Tactic.BicategoryLike.Eval.Result

added def Mathlib.Tactic.BicategoryLike.HorizontalComp.e

added def Mathlib.Tactic.BicategoryLike.HorizontalComp.srcM

added def Mathlib.Tactic.BicategoryLike.HorizontalComp.tgtM

added inductive Mathlib.Tactic.BicategoryLike.HorizontalComp

added def Mathlib.Tactic.BicategoryLike.Mor₂Iso.isStructural

added def Mathlib.Tactic.BicategoryLike.NormalExpr.associatorInvM

added def Mathlib.Tactic.BicategoryLike.NormalExpr.associatorM

added def Mathlib.Tactic.BicategoryLike.NormalExpr.e

added def Mathlib.Tactic.BicategoryLike.NormalExpr.idM

added def Mathlib.Tactic.BicategoryLike.NormalExpr.leftUnitorInvM

added def Mathlib.Tactic.BicategoryLike.NormalExpr.leftUnitorM

added def Mathlib.Tactic.BicategoryLike.NormalExpr.ofAtomM

added def Mathlib.Tactic.BicategoryLike.NormalExpr.ofM

added def Mathlib.Tactic.BicategoryLike.NormalExpr.rightUnitorInvM

added def Mathlib.Tactic.BicategoryLike.NormalExpr.rightUnitorM

added def Mathlib.Tactic.BicategoryLike.NormalExpr.srcM

added def Mathlib.Tactic.BicategoryLike.NormalExpr.tgtM

added def Mathlib.Tactic.BicategoryLike.NormalExpr.toList

added inductive Mathlib.Tactic.BicategoryLike.NormalExpr

added def Mathlib.Tactic.BicategoryLike.WhiskerLeft.e

added def Mathlib.Tactic.BicategoryLike.WhiskerLeft.srcM

added def Mathlib.Tactic.BicategoryLike.WhiskerLeft.tgtM

added inductive Mathlib.Tactic.BicategoryLike.WhiskerLeft

added def Mathlib.Tactic.BicategoryLike.WhiskerRight.e

added def Mathlib.Tactic.BicategoryLike.WhiskerRight.srcM

added def Mathlib.Tactic.BicategoryLike.WhiskerRight.tgtM

added inductive Mathlib.Tactic.BicategoryLike.WhiskerRight

added def Mathlib.Tactic.BicategoryLike.eval

added def Mathlib.Tactic.BicategoryLike.evalComp

added def Mathlib.Tactic.BicategoryLike.evalCompNil

added def Mathlib.Tactic.BicategoryLike.evalWhiskerLeft

added def Mathlib.Tactic.BicategoryLike.traceProof

Created Mathlib/Tactic/CategoryTheory/Coherence/PureCoherence.lean

added structure Mathlib.Tactic.BicategoryLike.Normalize.Result

added def Mathlib.Tactic.BicategoryLike.normalize

added def Mathlib.Tactic.BicategoryLike.pureCoherence

Deleted Mathlib/Tactic/CategoryTheory/Monoidal.lean

deleted def Mathlib.Tactic.Monoidal.Atom.src

deleted def Mathlib.Tactic.Monoidal.Atom.tgt

deleted structure Mathlib.Tactic.Monoidal.Atom

deleted structure Mathlib.Tactic.Monoidal.Atom₁

deleted structure Mathlib.Tactic.Monoidal.Context

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

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

deleted inductive Mathlib.Tactic.Monoidal.Mor₁

deleted def Mathlib.Tactic.Monoidal.NormalExpr.associator

deleted def Mathlib.Tactic.Monoidal.NormalExpr.associatorInv

deleted def Mathlib.Tactic.Monoidal.NormalExpr.e

deleted def Mathlib.Tactic.Monoidal.NormalExpr.leftUnitor

deleted def Mathlib.Tactic.Monoidal.NormalExpr.leftUnitorInv

deleted def Mathlib.Tactic.Monoidal.NormalExpr.of

deleted def Mathlib.Tactic.Monoidal.NormalExpr.ofExpr

deleted def Mathlib.Tactic.Monoidal.NormalExpr.rightUnitor

deleted def Mathlib.Tactic.Monoidal.NormalExpr.rightUnitorInv

deleted def Mathlib.Tactic.Monoidal.NormalExpr.src

deleted def Mathlib.Tactic.Monoidal.NormalExpr.tgt

deleted def Mathlib.Tactic.Monoidal.NormalExpr.toList

deleted inductive Mathlib.Tactic.Monoidal.NormalExpr

deleted structure Mathlib.Tactic.Monoidal.Result

deleted def Mathlib.Tactic.Monoidal.Structural.src

deleted def Mathlib.Tactic.Monoidal.Structural.tgt

deleted inductive Mathlib.Tactic.Monoidal.Structural

deleted def Mathlib.Tactic.Monoidal.StructuralAtom.e

deleted def Mathlib.Tactic.Monoidal.StructuralAtom.src

deleted def Mathlib.Tactic.Monoidal.StructuralAtom.tgt

deleted inductive Mathlib.Tactic.Monoidal.StructuralAtom

deleted def Mathlib.Tactic.Monoidal.WhiskerLeftExpr.e

deleted def Mathlib.Tactic.Monoidal.WhiskerLeftExpr.src

deleted def Mathlib.Tactic.Monoidal.WhiskerLeftExpr.tgt

deleted inductive Mathlib.Tactic.Monoidal.WhiskerLeftExpr

deleted def Mathlib.Tactic.Monoidal.WhiskerRightExpr.e

deleted def Mathlib.Tactic.Monoidal.WhiskerRightExpr.src

deleted def Mathlib.Tactic.Monoidal.WhiskerRightExpr.tgt

deleted inductive Mathlib.Tactic.Monoidal.WhiskerRightExpr

deleted theorem Mathlib.Tactic.Monoidal.evalComp_cons

deleted theorem Mathlib.Tactic.Monoidal.evalComp_nil_cons

deleted theorem Mathlib.Tactic.Monoidal.evalComp_nil_nil

deleted theorem Mathlib.Tactic.Monoidal.evalWhiskerLeft_comp

deleted theorem Mathlib.Tactic.Monoidal.evalWhiskerLeft_id

deleted theorem Mathlib.Tactic.Monoidal.evalWhiskerLeft_nil

deleted theorem Mathlib.Tactic.Monoidal.evalWhiskerLeft_of_cons

deleted theorem Mathlib.Tactic.Monoidal.evalWhiskerRight_comp

deleted theorem Mathlib.Tactic.Monoidal.evalWhiskerRight_cons_of_of

deleted theorem Mathlib.Tactic.Monoidal.evalWhiskerRight_cons_whisker

deleted theorem Mathlib.Tactic.Monoidal.evalWhiskerRight_id

deleted theorem Mathlib.Tactic.Monoidal.evalWhiskerRight_nil

deleted theorem Mathlib.Tactic.Monoidal.eval_comp

deleted theorem Mathlib.Tactic.Monoidal.eval_monoidalComp

deleted theorem Mathlib.Tactic.Monoidal.eval_of

deleted theorem Mathlib.Tactic.Monoidal.eval_whiskerLeft

deleted theorem Mathlib.Tactic.Monoidal.eval_whiskerRight

deleted def Mathlib.Tactic.Monoidal.isTensorObj?

deleted def Mathlib.Tactic.Monoidal.isTensorUnit?

deleted def Mathlib.Tactic.Monoidal.mkContext?

deleted def Mathlib.Tactic.Monoidal.src

deleted def Mathlib.Tactic.Monoidal.structuralAtom?

deleted def Mathlib.Tactic.Monoidal.structuralOfMonoidalComp

deleted def Mathlib.Tactic.Monoidal.tgt

deleted def mkEq

deleted theorem mk_eq

Created Mathlib/Tactic/CategoryTheory/Monoidal/Basic.lean

added def Mathlib.Tactic.Monoidal.monoidal

added def Mathlib.Tactic.Monoidal.monoidalNf

Created Mathlib/Tactic/CategoryTheory/Monoidal/Datatypes.lean

added structure Mathlib.Tactic.Monoidal.Context

added theorem Mathlib.Tactic.Monoidal.StructuralOfExpr_monoidalComp

added def Mathlib.Tactic.Monoidal.comp?

added def Mathlib.Tactic.Monoidal.id₁?

added def Mathlib.Tactic.Monoidal.mkContext?

added def Mathlib.Tactic.Monoidal.srcExpr

added def Mathlib.Tactic.Monoidal.srcExprOfIso

added theorem Mathlib.Tactic.Monoidal.structuralIsoOfExpr_comp

added theorem Mathlib.Tactic.Monoidal.structuralIsoOfExpr_horizontalComp

added theorem Mathlib.Tactic.Monoidal.structuralIsoOfExpr_whiskerLeft

added theorem Mathlib.Tactic.Monoidal.structuralIsoOfExpr_whiskerRight

added def Mathlib.Tactic.Monoidal.synthMonoidalError

added def Mathlib.Tactic.Monoidal.tgtExpr

added def Mathlib.Tactic.Monoidal.tgtExprOfIso

Created Mathlib/Tactic/CategoryTheory/Monoidal/Normalize.lean

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.evalHorizontalCompAux'_of_whisker

added theorem Mathlib.Tactic.Monoidal.evalHorizontalCompAux'_whisker

added theorem Mathlib.Tactic.Monoidal.evalHorizontalCompAux_cons

added theorem Mathlib.Tactic.Monoidal.evalHorizontalCompAux_of

added theorem Mathlib.Tactic.Monoidal.evalHorizontalComp_cons_cons

added theorem Mathlib.Tactic.Monoidal.evalHorizontalComp_cons_nil

added theorem Mathlib.Tactic.Monoidal.evalHorizontalComp_nil_cons

added theorem Mathlib.Tactic.Monoidal.evalHorizontalComp_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.evalWhiskerRightAux_cons

added theorem Mathlib.Tactic.Monoidal.evalWhiskerRightAux_of

added theorem Mathlib.Tactic.Monoidal.evalWhiskerRight_comp

added theorem Mathlib.Tactic.Monoidal.evalWhiskerRight_cons_of

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_tensorHom

added theorem Mathlib.Tactic.Monoidal.eval_whiskerLeft

added theorem Mathlib.Tactic.Monoidal.eval_whiskerRight

Created Mathlib/Tactic/CategoryTheory/Monoidal/PureCoherence.lean

added theorem Mathlib.Tactic.Monoidal.mk_eq_of_naturality

added theorem Mathlib.Tactic.Monoidal.naturality_associator

added theorem Mathlib.Tactic.Monoidal.naturality_comp

added theorem Mathlib.Tactic.Monoidal.naturality_id

added theorem Mathlib.Tactic.Monoidal.naturality_inv

added theorem Mathlib.Tactic.Monoidal.naturality_leftUnitor

added theorem Mathlib.Tactic.Monoidal.naturality_rightUnitor

added theorem Mathlib.Tactic.Monoidal.naturality_tensorHom

added theorem Mathlib.Tactic.Monoidal.naturality_whiskerLeft

added theorem Mathlib.Tactic.Monoidal.naturality_whiskerRight

added theorem Mathlib.Tactic.Monoidal.of_normalize_eq

added def Mathlib.Tactic.Monoidal.pureCoherence

Modified Mathlib/Tactic/Widget/StringDiagram.lean

added def Mathlib.Tactic.BicategoryLike.HorizontalComp.nodes

added def Mathlib.Tactic.BicategoryLike.NormalExpr.nodes

added def Mathlib.Tactic.BicategoryLike.NormalExpr.nodesAux

added def Mathlib.Tactic.BicategoryLike.NormalExpr.strands

added def Mathlib.Tactic.BicategoryLike.WhiskerLeft.nodes

added def Mathlib.Tactic.BicategoryLike.WhiskerRight.nodes

added def Mathlib.Tactic.BicategoryLike.pairs

added def Mathlib.Tactic.BicategoryLike.topNodes

deleted def Mathlib.Tactic.Monoidal.NormalExpr.nodes

deleted def Mathlib.Tactic.Monoidal.NormalExpr.nodesAux

deleted def Mathlib.Tactic.Monoidal.NormalExpr.strands

deleted def Mathlib.Tactic.Monoidal.WhiskerLeftExpr.nodes

deleted def Mathlib.Tactic.Monoidal.WhiskerRightExpr.nodes

deleted def Mathlib.Tactic.Monoidal.pairs

added def Mathlib.Tactic.Widget.StringDiagram.Kind.name

added inductive Mathlib.Tactic.Widget.StringDiagram.Kind

modified def Mathlib.Tactic.Widget.StringDiagram.Node.srcList

modified def Mathlib.Tactic.Widget.StringDiagram.Node.tarList

deleted def Mathlib.Tactic.Widget.StringDiagram.fromExpr

added def Mathlib.Tactic.Widget.StringDiagram.mkKind

modified def Mathlib.Tactic.Widget.StringDiagram.mkStringDiagram

deleted def Mathlib.Tactic.Widget.StringDiagram.topNodes

Modified scripts/noshake.json

Created test/CategoryTheory/Bicategory/Basic.lean

Created test/CategoryTheory/Bicategory/Normalize.lean

Deleted test/CategoryTheory/Monoidal.lean

Created test/CategoryTheory/Monoidal/Basic.lean

Created test/CategoryTheory/Monoidal/Normalize.lean

Modified test/StringDiagram.lean