# Documentation

Mathlib.Tactic.Reassoc

# The reasoc attribute #

Adding @[reassoc] to a lemma named F of shape ∀ .., f = g∀ .., f = g, where f g : X ⟶ Y⟶ Y in some category will create a new lemmas named F_assoc of shape ∀ .. {Z : C} (h : Y ⟶ Z), f ≫ h = g ≫ h∀ .. {Z : C} (h : Y ⟶ Z), f ≫ h = g ≫ h⟶ Z), f ≫ h = g ≫ h≫ h = g ≫ h≫ 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.

theorem CategoryTheory.eq_whisker' {C : Type u_2} [inst : ] {X : C} {Y : C} {f : X Y} {g : X Y} (w : f = g) {Z : C} (h : Y Z) :
f h = g h

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
• = Lean.Meta.simpOnlyNames [CategoryTheory.Category.comp_id, CategoryTheory.Category.id_comp, CategoryTheory.Category.assoc] e

Given an equation f = g between morphisms X ⟶ Y⟶ Y in a category (possibly after a ∀∀ binder), produce the equation ∀ {Z} (h : Y ⟶ Z), f ≫ h = g ≫ h∀ {Z} (h : Y ⟶ Z), f ≫ h = g ≫ h⟶ Z), f ≫ h = g ≫ h≫ h = g ≫ h≫ h, but with compositions fully right associated and identities removed.

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

Syntax for the reassoc attribute

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

reassoc_of% t, where t is an equation f = g between morphisms X ⟶ Y⟶ Y in a category (possibly after a ∀∀ binder), produce the equation ∀ {Z} (h : Y ⟶ Z), f ≫ h = g ≫ h∀ {Z} (h : Y ⟶ Z), f ≫ h = g ≫ h⟶ Z), f ≫ h = g ≫ h≫ h = g ≫ h≫ h`, but with compositions fully right associated and identities removed.

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