# Documentation

## Mathlib.Tactic.Widget.CommDiag

This module defines tactic/meta infrastructure for displaying commutative diagrams in the infoview.

@[inline]
def Lean.Expr.app7? (e : Lean.Expr) (fName : Lean.Name) :

If the expression is a function application of fName with 7 arguments, return those arguments. Otherwise return none.

Equations
• One or more equations did not get rendered due to their size.
Instances For

## Metaprogramming utilities for breaking down category theory expressions #

Given a Hom type α ⟶ β, return (α, β). Otherwise none.

Equations
• = match e.app4? Quiver.Hom with | some (fst, fst_1, A, B) => pure (A, B) | x => none
Instances For

Given composed homs g ≫ h, return (g, h). Otherwise none.

Equations
• = match f.app7? CategoryTheory.CategoryStruct.comp with | some (fst, fst_1, fst_2, fst_3, fst_4, f, g) => pure (f, g) | x => none
Instances For
@[reducible, inline]

Expressions to display as labels in a diagram.

Equations
Instances For

## Widget for general commutative diagrams #

Construct a commutative diagram from a Penrose substance program and expressions embeds to display as labels in the diagram.

Equations
• One or more equations did not get rendered due to their size.
Instances For

## Commutative triangles #

Triangle with homs = [f,g,h] and objs = [A,B,C]

A f B
h g
C

Equations
• One or more equations did not get rendered due to their size.
Instances For

Given a commutative triangle f ≫ g = h or e ≡ h = f ≫ g, return a triangle diagram. Otherwise none.

Equations
• One or more equations did not get rendered due to their size.
Instances For
Equations
• One or more equations did not get rendered due to their size.
Instances For

## Commutative squares #

Square with homs = [f,g,h,i] and objs = [A,B,C,D]

A f B
i   g
D h C

Equations
• One or more equations did not get rendered due to their size.
Instances For

Given a commutative square f ≫ g = i ≫ h, return a square diagram. Otherwise none.

Equations
• One or more equations did not get rendered due to their size.
Instances For
Equations
• One or more equations did not get rendered due to their size.
Instances For