commSquareM?

Mathlib.Tactic.Widget.CommDiag

URI: https://scilib.ai/kg/mathlib#Mathlib.Tactic.Widget.commSquareM?

Lean4

/-- Given a commutative square `f ≫ g = i ≫ h`, return a square diagram. Otherwise `none`. -/
def commSquareM? (e : Expr) : MetaM (Option Html) := do
  let e ← instantiateMVars e
  let some (_, lhs, rhs) := e.eq? |
    return none
  let some (f, g) := homComp? lhs |
    return none
  let some (i, h) := homComp? rhs |
    return none
  let some (A, B) := homType? (← inferType f) |
    return none
  let some (D, C) := homType? (← inferType h) |
    return none
  some <$> mkCommDiag subSquare #[("A", A), ("B", B), ("C", C), ("D", D), ("f", f), ("g", g), ("h", h), ("i", i)]

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

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

Разделы

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

Аффилиация

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