# The `reassoc`

attribute #

Adding `@[reassoc]`

to a lemma named `F`

of shape `∀ .., f = g`

,
where `f g : X ⟶ Y`

in some category
will create a new lemmas named `F_assoc`

of shape
`∀ .. {Z : C} (h : Y ⟶ Z), f ≫ h = g ≫ h`

but with the conclusions simplified used the axioms for a category
(`Category.comp_id`

, `Category.id_comp`

, and `Category.assoc`

).

This is useful for generating lemmas which the simplifier can use even on expressions that are already right associated.

There is also a term elaborator `reassoc_of% t`

for use within proofs.

A variant of `eq_whisker`

with a more convenient argument order for use in tactics.

Simplify an expression using only the axioms of a category.

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

Given an equation `f = g`

between morphisms `X ⟶ Y`

in a category (possibly after a `∀`

binder),
produce the equation `∀ {Z} (h : Y ⟶ Z), f ≫ h = g ≫ h`

,
but with compositions fully right associated and identities removed.

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

Syntax for the `reassoc`

attribute

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

`reassoc_of% t`

, where `t`

is
an equation `f = g`

between morphisms `X ⟶ Y`

in a category (possibly after a `∀`

binder),
produce the equation `∀ {Z} (h : Y ⟶ Z), f ≫ h = g ≫ h`

,
but with compositions fully right associated and identities removed.

## Equations

- One or more equations did not get rendered due to their size.