# Documentation

Mathlib.Tactic.CategoryTheory.Reassoc

# 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.

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

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.

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.

Instances For

Syntax for the reassoc attribute

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.

Instances For