Extension of reassoc to isomorphisms.

We extend reassoc and reassoc_of% for equality of isomorphisms. 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 basic propertions in isomorphisms in a category (Iso.trans_refl, Iso.refl_trans, Iso.trans_assoc, Iso.trans_symm, Iso.symm_self_id and Iso.self_symm_id).

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

theorem CategoryTheory.Iso.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) : f ≪≫ h = g ≪≫ h

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

Simplify an expression using only the axioms of a groupoid.

Equations

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

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

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

Equations

• CategoryTheory.reassocExprIso e = do let __do_lift ← Lean.Meta.mkAppM `CategoryTheory.Iso.eq_whisker #[e] Lean.Meta.simpType CategoryTheory.categoryIsoSimp __do_lift