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.

The Mathlib.Tactic.CategoryTheory.IsoReassoc extends @[reassoc] and reassoc_of% to support creating isomorphism reassociation lemmas.

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

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

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

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

This attribute also works for lemmas of shape ∀ .., f = g where f g : X ≅ Y are isomorphisms, provided that Tactic.CategoryTheory.IsoReassoc has been imported.

def CategoryTheory.registerReassocExpr (f : Lean.Expr → Lean.MetaM Lean.Expr) : IO Unit

Registers a handler for reassocExpr. The handler takes a proof of an equation and returns a proof of the reassociation lemma. Handlers are considered in order of registration. They are applied directly to the equation in the body of the forall.

def CategoryTheory.reassocExpr (pf : Lean.Expr) (type? : Option Lean.Expr) : Lean.MetaM Lean.Expr

Reassociates the morphisms in type? using the registered handlers, using reassocExprHom as the default. If type? is not given, it is assumed to be the type of pf.

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. This also works for equations between isomorphisms, provided that Tactic.CategoryTheory.IsoReassoc has been imported.