insertTrailingIds

Mathlib.Tactic.CategoryTheory.Coherence

URI: https://scilib.ai/kg/mathlib#Mathlib.Tactic.Coherence.insertTrailingIds

Lean4

/-- If either the lhs or rhs is not a composition, compose it on the right with an identity. -/
def insertTrailingIds (g : MVarId) : MetaM MVarId := do
  let some (_, lhs, rhs) := (← withReducible g.getType').eq? |
    exception g "Not an equality."
  let mut g := g
  if !(lhs.isAppOf ``CategoryStruct.comp) then
    let [g'] ← g.applyConst ``insert_id_lhs |
      exception g "failed to apply insert_id_lhs"
    g := g'
  if !(rhs.isAppOf ``CategoryStruct.comp) then
    let [g'] ← g.applyConst ``insert_id_rhs |
      exception g "failed to apply insert_id_rhs"
    g := g'
  return g

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

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

Разделы

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

Аффилиация

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