Commit 2023-06-07 03:09 b59f0ddb

View on Github →

feat: port CategoryTheory.Bicategory.CoherenceTactic (#4610)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Category/ModuleCat/Adjunctions.lean

Modified Mathlib/Algebra/Category/ModuleCat/Monoidal/Closed.lean

Modified Mathlib/Algebra/Category/ModuleCat/Monoidal/Symmetric.lean

Modified Mathlib/CategoryTheory/Limits/Yoneda.lean

Modified Mathlib/CategoryTheory/Monoidal/Braided.lean

Modified Mathlib/CategoryTheory/Monoidal/Category.lean

Modified Mathlib/CategoryTheory/Monoidal/Discrete.lean

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

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

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

Modified Mathlib/CategoryTheory/Monoidal/Types/Symmetric.lean

Modified Mathlib/RepresentationTheory/Action.lean

Modified Mathlib/Tactic.lean

Created Mathlib/Tactic/CategoryTheory/BicategoryCoherence.lean

added def Mathlib.Tactic.BicategoryCoherence.BicategoricalCoherence.hom

added theorem Mathlib.Tactic.BicategoryCoherence.assoc_liftHom₂

added def Mathlib.Tactic.BicategoryCoherence.bicategoricalComp

added theorem Mathlib.Tactic.BicategoryCoherence.bicategoricalComp_refl

added def Mathlib.Tactic.BicategoryCoherence.bicategoricalIso

added def Mathlib.Tactic.BicategoryCoherence.bicategoricalIsoComp

added def Mathlib.Tactic.BicategoryCoherence.bicategory_coherence

added def Mathlib.Tactic.BicategoryCoherence.exception'

added def Mathlib.Tactic.BicategoryCoherence.exception

added def Mathlib.Tactic.BicategoryCoherence.mkLiftMap₂LiftExpr

Modified Mathlib/Tactic/CategoryTheory/Coherence.lean

deleted theorem Mathlib.Tactic.Coherence.assoc_LiftHom

added theorem Mathlib.Tactic.Coherence.assoc_liftHom

Modified test/CategoryTheory/Coherence.lean