There is a complete proof formalised by Scott Morrison in the Lean proof assistant here:

monoidal/of_has_finite_products.lean

[UPDATE] Here is some commentary. In the above file, we see

```
variables (C : Type u) [category.{v} C] {X Y : C}
```

In ordinary mathematical language, this means roughly as follows:

Let $C$ be a set in the Grothendieck universe $u$. Suppose we have a category structure on $C$, i.e. a category with object set $C$; the hom sets are in the Grothendieck universe $v$. Let $X$ and $Y$ be objects of $C$.

This is slightly inaccurate because Lean is based on type theory rather than set theory, and $u$ and $v$ are not really Grothendieck universes but they play the same sort of role in avoiding Russell-type paradoxes.

Later we see

```
def monoidal_of_has_finite_products [has_terminal C] [has_binary_products C] : monoidal_category C :=
{ tensor_unit := ⊤_ C,
tensor_obj := λ X Y, X ⨯ Y,
tensor_hom := λ _ _ _ _ f g, limits.prod.map f g,
associator := prod.associator,
left_unitor := λ P, prod.left_unitor P,
right_unitor := λ P, prod.right_unitor P,
pentagon' := prod.pentagon,
triangle' := prod.triangle,
associator_naturality' := @prod.associator_naturality _ _ _, }
end
```

This can be translated as follows:

Suppose that $C$ also has a terminal object and binary products. Then we define a monoidal category structure on $C$, which we call `monoidal_of_has_finite_products C`

, as follows: the tensor unit is the terminal object, the tensor product of two objects `X`

and `Y`

is `X ⨯ Y`

, the tensor product of morphisms is given by the function `limits.prod.map`

that was defined elsewhere, ...

Most of the ingredients used here are actually defined in the file binary_products.lean. For example, in that file we see

```
lemma prod.pentagon [has_binary_products C] (W X Y Z : C) :
prod.map ((prod.associator W X Y).hom) (𝟙 Z) ≫
(prod.associator W (X ⨯ Y) Z).hom ≫ prod.map (𝟙 W) ((prod.associator X Y Z).hom) =
(prod.associator (W ⨯ X) Y Z).hom ≫ (prod.associator W X (Y ⨯ Z)).hom :=
by simp
```

The symbol `≫`

used here is just backwards composition, i.e. `f ≫ g = g o f`

.
Everything before the `:=`

is the statement of the pentagon lemma, and after the `:=`

we have the proof, which is just `by simp`

. Earlier in this file, and in other files, there are many lemmas marked with `@[simp]`

. The directive `by simp`

just tells Lean to try to apply any such lemmas that are applicable, and in this case, that is enough to complete the proof.

lotmore patience than I have for big commutative diagrams) $\endgroup$ – Denis Nardin Jan 27 at 16:52