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} [CategoryTheory.Category.{u_2, u_1} C] {X : C} {Y : C} {f : X ⟶ Y} {g : X ⟶ Y} (w : f = g) {Z : C} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp f h = CategoryTheory.CategoryStruct.comp g h

A variant of eq_whisker with a more convenient argument order for use in tactics.

def CategoryTheory.categorySimp (e : Lean.Expr) : Lean.MetaM Lean.Meta.Simp.Result

Simplify an expression using only the axioms of a category.

Equations

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

def CategoryTheory.reassocExpr (e : Lean.Expr) : Lean.MetaM Lean.Expr

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.

def CategoryTheory.reassoc : Lean.ParserDescr

Syntax for the reassoc attribute

Equations

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

def CategoryTheory.«termReassoc_of%_» : Lean.ParserDescr

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.