Def Mathlib.Tactic.BicategoryCoherence.mkLiftMap₂LiftExpr

Modification history

2023-06-07 03:09

Mathlib/Tactic/CategoryTheory/BicategoryCoherence.lean

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

Added Mathlib.Tactic.BicategoryCoherence.mkLiftMap₂LiftExpr View on Github →