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 lemma named F_assoc of shape ∀ .. {Z : C} (h : Y ⟶ Z), f ≫ h = g ≫ h but with the conclusions simplified using 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 Y : C} {f 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

Adding @[reassoc] to a lemma named F of shape ∀ .., f = g, where f g : X ⟶ Y are morphisms in some category, will create a new lemma named F_assoc of shape ∀ .. {Z : C} (h : Y ⟶ Z), f ≫ h = g ≫ h but with the conclusions simplified using the axioms for a category (Category.comp_id, Category.id_comp, and Category.assoc). So, for example, if the conclusion of F is a ≫ b = g then the conclusion of F_assoc will be a ≫ (b ≫ h) = g ≫ h (note that ≫ reassociates to the right so the brackets will not appear in the statement).

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

Note that if you want both the lemma and the reassociated lemma to be simp lemmas, you should tag the lemma @[reassoc (attr := simp)]. The variant @[simp, reassoc] on a lemma F will tag F with @[simp], but not F_assoc (this is sometimes useful).

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.