Commit 2023-05-28 11:05 15ddd4be

View on Github →

feat: port coherence tactic (#4357) This is a by-hand port of category_theory.monoidal.coherence, which is blocking things like https://tqft.net/mathlib4/2023-05-26/representation_theory.group_cohomology.basic.pdf. It does not include a port of the coherence tactic for bicategories, but this is not actually used in mathlib yet.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Lean/Meta.lean

added def Lean.MVarId.applyConst

Modified Mathlib/Lean/Meta/Simp.lean

added def Lean.Meta.Simp.Simp.Context.ofNames

modified def Lean.Meta.Simp.simpTheoremsOfNames

Modified Mathlib/Tactic.lean

Created Mathlib/Tactic/CategoryTheory/Coherence.lean

added theorem Mathlib.Tactic.Coherence.assoc_LiftHom

added def Mathlib.Tactic.Coherence.coherence_loop

added def Mathlib.Tactic.Coherence.exception'

added def Mathlib.Tactic.Coherence.exception

added def Mathlib.Tactic.Coherence.insertTrailingIds

added theorem Mathlib.Tactic.Coherence.insert_id_lhs

added theorem Mathlib.Tactic.Coherence.insert_id_rhs

added def Mathlib.Tactic.Coherence.mkProjectMapExpr

added def Mathlib.Tactic.Coherence.monoidalComp

added theorem Mathlib.Tactic.Coherence.monoidalComp_refl

added def Mathlib.Tactic.Coherence.monoidalIso

added def Mathlib.Tactic.Coherence.monoidal_coherence

Created test/CategoryTheory/coherence.lean