3.2. Associativity of the composition🔗

The composition of morphisms in a category is associative. When a term is a composition of more than two morphisms, the syntax is set up so that f ≫ g ≫ h means f ≫ (g ≫ h), and this is also the simp normal form (i.e. (f ≫ g) ≫ h simplifies to f ≫ g ≫ h):

In non-formalized mathematics, the associativity of the composition is often used implicitly. In formalized mathematics, we need to take care about this associativity in one way or another when proving equalities of morphisms:

This proof uses the associativity in order to make the term f₀ ≫ (f₁ ≫ f₂) ≫ f₃ appear, which allows to rewrite h. Proceeding like this would be very unpractical in more intricate cases, and it is also inconvenient because this would often require using Category.assoc explicitly in both forward and backwards directions. As it is a simp lemma, it is recommended to use it explicitly only in the forward direction.

An alternative proof can be obtained using specialized tactics:

slice_lhs (and slice_rhs) are specialized conv-like tactics which allow to zoom on certain chunks in the middle of compositions of multiple morphisms. When there is no better way, this method can be used when dealing with very long compositions.

In this case, the preferred proof would be:

This proof uses the term elaborator reassoc_of%: from an an equality like h : f₁ ≫ f₂ = φ, it produces a term f₁ ≫ f₂ ≫ α = f₂ ≫ α for a generic morphism α, and it can be used in rewrites. Note that we do not need the "dual" construction of a term β ≫ f₁ ≫ f₂ = β ≫ f₂ because h can be directly rewritten in it. Indeed, this reassoc_of% h term could be rewritten in an arbitrary composition like β₀ ≫ ... ≫ βₙ ≫ f₁ ≫ f₂ ≫ γ₀ ≫ ... ≫ γₘ as soon as the list [γ₀, ..., γₘ] is nonempty.

Similarly, we have a @[reassoc] attribute (often used in combination with simp as @[reassoc (attr := simp)]); when it is applied to a lemma foo, it generates another lemma foo_assoc similarly as reassoc_of% h is generated from h above.