categoryIsoSimp

Mathlib.Tactic.CategoryTheory.IsoReassoc

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

Lean4

/-- Simplify an expression using only the axioms of a groupoid. -/
def categoryIsoSimp (e : Expr) : MetaM Simp.Result :=
  simpOnlyNames
    [``Iso.trans_symm, ``Iso.trans_refl, ``Iso.refl_trans, ``Iso.trans_assoc, ``Iso.symm_self_id, ``Iso.self_symm_id,
      ``Iso.symm_self_id_assoc, ``Iso.self_symm_id_assoc, ``Functor.mapIso_trans, ``Functor.mapIso_symm,
      ``Functor.mapIso_refl, ``Functor.id_obj]
    e (config := { decide := false })

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

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

Разделы

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

Аффилиация

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