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 Mathlib.Tactic.Reassoc.eq_whisker' {C : Type u_1} [CategoryTheory.Category.{v_1, 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 Mathlib.Tactic.Reassoc.categorySimp (e : Lean.Expr) : Lean.MetaM Lean.Meta.Simp.Result

Simplify an expression using only the axioms of a category.

def Mathlib.Tactic.Reassoc.reassocExprHom (e : Lean.Expr) : Lean.MetaM (Lean.Expr × Array Lean.MVarId)

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. Also returns the category C and any instance metavariables that need to be solved for.

def Mathlib.Tactic.Reassoc.toDualOpt : Lean.ParserDescr

An option to tag the lemma generated by @[reassoc] with to_dual none.

def Mathlib.Tactic.Reassoc.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 can be combined with to_dual in the form @[to_dual (attr := reassoc (attr := simp))], which tags all 4 lemmas with simp, or @[to_dual (attr := simp, reassoc)], which only tags F and its dual with simp.

If F is tagged with to_dual, then F_assoc will automatically get a @[to_dual none] tag. This also applies when using @[to_dual (attr := reassoc)]. In the rare case that only F_assoc should be tagged with to_dual, use @[reassoc +to_dual].

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 Mathlib.Tactic.Reassoc.registerReassocExpr (f : Lean.Expr → Lean.MetaM (Lean.Expr × Array Lean.MVarId)) : 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 Mathlib.Tactic.Reassoc.reassocExpr (pf : Lean.Expr) : Lean.MetaM (Lean.Expr × Array Lean.MVarId)

Reassociates the morphisms in the type of pf using the registered handlers, using reassocExprHom as the default.

Returns the proof of the lemma along with instance metavariables that need synthesis.

def Mathlib.Tactic.Reassoc.reassocExpr' (pf : Lean.Expr) : Lean.Elab.TermElabM Lean.Expr

Version of reassocExpr for the TermElabM monad. Handles instance metavariables automatically.

def Mathlib.Tactic.Reassoc.«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.