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

Equations
  • One or more equations did not get rendered due to their size.
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.

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

      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_apply (this is sometimes useful).

      Equations
      • One or more equations did not get rendered due to their size.
      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.

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