catAppSimp

Mathlib.Tactic.CategoryTheory.ToApp

URI: https://scilib.ai/kg/mathlib#CategoryTheory.catAppSimp

Lean4

/-- Simplify an expression in `Cat` using basic properties of `NatTrans.app`. -/
def catAppSimp (e : Expr) : MetaM Simp.Result :=
  simpOnlyNames
    [``Cat.comp_obj, ``Cat.whiskerLeft_app, ``Cat.whiskerRight_app, ``Cat.id_app, ``Cat.comp_app, ``Cat.eqToHom_app,
      ``Cat.leftUnitor_hom_app, ``Cat.leftUnitor_inv_app, ``Cat.rightUnitor_hom_app, ``Cat.rightUnitor_inv_app,
      ``Cat.associator_hom_app, ``Cat.associator_inv_app, ``eqToHom_refl, ``Category.comp_id, ``Category.id_comp]
    e (config := { decide := false })

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru