Lean4
/-- Given a commutative triangle `f ≫ g = h` or `e ≡ h = f ≫ g`, return a triangle diagram.
Otherwise `none`. -/
def commTriangleM? (e : Expr) : MetaM (Option Html) := do
let e ← instantiateMVars e
let some (_, lhs, rhs) := e.eq? |
return none
if let some (f, g) := homComp? lhs then
let some (A, C) := homType? (← inferType rhs) |
return none
let some (_, B) := homType? (← inferType f) |
return none
return some <| ← mkCommDiag subTriangle #[("A", A), ("B", B), ("C", C), ("f", f), ("g", g), ("h", rhs)]
let some (f, g) := homComp? rhs |
return none
let some (A, C) := homType? (← inferType lhs) |
return none
let some (_, B) := homType? (← inferType f) |
return none
return some <| ← mkCommDiag subTriangle #[("A", A), ("B", B), ("C", C), ("f", f), ("g", g), ("h", lhs)]
