Normalization of 2-morphisms in bicategories

This file provides the implementation of the normalization given in Mathlib/Tactic/CategoryTheory/Coherence/Normalize.lean. See this file for more details.

theorem Mathlib.Tactic.Bicategory.evalComp_nil_nil {B : Type u} [CategoryTheory.Bicategory B] {a b : B} {f g h : a ⟶ b} (α : f ≅ g) (β : g ≅ h) : (α ≪≫ β).hom = (α ≪≫ β).hom

theorem Mathlib.Tactic.Bicategory.evalComp_nil_cons {B : Type u} [CategoryTheory.Bicategory B] {a b : B} {f g h i j : a ⟶ b} (α : f ≅ g) (β : g ≅ h) (η : h ⟶ i) (ηs : i ⟶ j) : CategoryTheory.CategoryStruct.comp α.hom (CategoryTheory.CategoryStruct.comp β.hom (CategoryTheory.CategoryStruct.comp η ηs)) = CategoryTheory.CategoryStruct.comp (α ≪≫ β).hom (CategoryTheory.CategoryStruct.comp η ηs)

theorem Mathlib.Tactic.Bicategory.evalComp_cons {B : Type u} [CategoryTheory.Bicategory B] {a b : B} {f g h i j : a ⟶ b} (α : f ≅ g) (η : g ⟶ h) {ηs : h ⟶ i} {θ : i ⟶ j} {ι : h ⟶ j} (e_ι : CategoryTheory.CategoryStruct.comp ηs θ = ι) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp α.hom (CategoryTheory.CategoryStruct.comp η ηs)) θ = CategoryTheory.CategoryStruct.comp α.hom (CategoryTheory.CategoryStruct.comp η ι)

theorem Mathlib.Tactic.Bicategory.eval_comp {B : Type u} [CategoryTheory.Bicategory B] {a b : B} {f g h : a ⟶ b} {η η' : f ⟶ g} {θ θ' : g ⟶ h} {ι : f ⟶ h} (e_η : η = η') (e_θ : θ = θ') (e_ηθ : CategoryTheory.CategoryStruct.comp η' θ' = ι) : CategoryTheory.CategoryStruct.comp η θ = ι

theorem Mathlib.Tactic.Bicategory.eval_of {B : Type u} [CategoryTheory.Bicategory B] {a b : B} {f g : a ⟶ b} (η : f ⟶ g) : η = CategoryTheory.CategoryStruct.comp (CategoryTheory.Iso.refl f).hom (CategoryTheory.CategoryStruct.comp η (CategoryTheory.Iso.refl g).hom)

theorem Mathlib.Tactic.Bicategory.eval_monoidalComp {B : Type u} [CategoryTheory.Bicategory B] {a b : B} {f g h i : a ⟶ b} {η η' : f ⟶ g} {α : g ≅ h} {θ θ' : h ⟶ i} {αθ : g ⟶ i} {ηαθ : f ⟶ i} (e_η : η = η') (e_θ : θ = θ') (e_αθ : CategoryTheory.CategoryStruct.comp α.hom θ' = αθ) (e_ηαθ : CategoryTheory.CategoryStruct.comp η' αθ = ηαθ) : CategoryTheory.CategoryStruct.comp η (CategoryTheory.CategoryStruct.comp α.hom θ) = ηαθ

theorem Mathlib.Tactic.Bicategory.evalWhiskerLeft_nil {B : Type u} [CategoryTheory.Bicategory B] {a b c : B} (f : a ⟶ b) {g h : b ⟶ c} (α : g ≅ h) : (CategoryTheory.Bicategory.whiskerLeftIso f α).hom = (CategoryTheory.Bicategory.whiskerLeftIso f α).hom

theorem Mathlib.Tactic.Bicategory.evalWhiskerLeft_of_cons {B : Type u} [CategoryTheory.Bicategory B] {a b c : B} {f : a ⟶ b} {g h i j : b ⟶ c} (α : g ≅ h) (η : h ⟶ i) {ηs : i ⟶ j} {θ : CategoryTheory.CategoryStruct.comp f i ⟶ CategoryTheory.CategoryStruct.comp f j} (e_θ : CategoryTheory.Bicategory.whiskerLeft f ηs = θ) : CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.CategoryStruct.comp α.hom (CategoryTheory.CategoryStruct.comp η ηs)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeftIso f α).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f η) θ)

theorem Mathlib.Tactic.Bicategory.evalWhiskerLeft_comp {B : Type u} [CategoryTheory.Bicategory B] {a b c d : B} {f : a ⟶ b} {g : b ⟶ c} {h i : c ⟶ d} {η : h ⟶ i} {η₁ : CategoryTheory.CategoryStruct.comp g h ⟶ CategoryTheory.CategoryStruct.comp g i} {η₂ : CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp g h) ⟶ CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp g i)} {η₃ : CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp g h) ⟶ CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g) i} {η₄ : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g) h ⟶ CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g) i} (e_η₁ : CategoryTheory.Bicategory.whiskerLeft g η = η₁) (e_η₂ : CategoryTheory.Bicategory.whiskerLeft f η₁ = η₂) (e_η₃ : CategoryTheory.CategoryStruct.comp η₂ (CategoryTheory.Bicategory.associator f g i).inv = η₃) (e_η₄ : CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f g h).hom η₃ = η₄) : CategoryTheory.Bicategory.whiskerLeft (CategoryTheory.CategoryStruct.comp f g) η = η₄

theorem Mathlib.Tactic.Bicategory.evalWhiskerLeft_id {B : Type u} [CategoryTheory.Bicategory B] {a b : B} {f g : a ⟶ b} {η : f ⟶ g} {η₁ : f ⟶ CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id a) g} {η₂ : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id a) f ⟶ CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id a) g} (e_η₁ : CategoryTheory.CategoryStruct.comp η (CategoryTheory.Bicategory.leftUnitor g).inv = η₁) (e_η₂ : CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.leftUnitor f).hom η₁ = η₂) : CategoryTheory.Bicategory.whiskerLeft (CategoryTheory.CategoryStruct.id a) η = η₂

theorem Mathlib.Tactic.Bicategory.eval_whiskerLeft {B : Type u} [CategoryTheory.Bicategory B] {a b c : B} {f : a ⟶ b} {g h : b ⟶ c} {η η' : g ⟶ h} {θ : CategoryTheory.CategoryStruct.comp f g ⟶ CategoryTheory.CategoryStruct.comp f h} (e_η : η = η') (e_θ : CategoryTheory.Bicategory.whiskerLeft f η' = θ) : CategoryTheory.Bicategory.whiskerLeft f η = θ

theorem Mathlib.Tactic.Bicategory.eval_whiskerRight {B : Type u} [CategoryTheory.Bicategory B] {a b c : B} {f g : a ⟶ b} {h : b ⟶ c} {η η' : f ⟶ g} {θ : CategoryTheory.CategoryStruct.comp f h ⟶ CategoryTheory.CategoryStruct.comp g h} (e_η : η = η') (e_θ : CategoryTheory.Bicategory.whiskerRight η' h = θ) : CategoryTheory.Bicategory.whiskerRight η h = θ

theorem Mathlib.Tactic.Bicategory.evalWhiskerRight_nil {B : Type u} [CategoryTheory.Bicategory B] {a b c : B} {f g : a ⟶ b} (α : f ≅ g) (h : b ⟶ c) : CategoryTheory.Bicategory.whiskerRight α.hom h = CategoryTheory.Bicategory.whiskerRight α.hom h

theorem Mathlib.Tactic.Bicategory.evalWhiskerRightAux_of {B : Type u} [CategoryTheory.Bicategory B] {a b c : B} {f g : a ⟶ b} (η : f ⟶ g) (h : b ⟶ c) : CategoryTheory.Bicategory.whiskerRight η h = CategoryTheory.CategoryStruct.comp (CategoryTheory.Iso.refl (CategoryTheory.CategoryStruct.comp f h)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight η h) (CategoryTheory.Iso.refl (CategoryTheory.CategoryStruct.comp g h)).hom)

theorem Mathlib.Tactic.Bicategory.evalWhiskerRight_cons_of_of {B : Type u} [CategoryTheory.Bicategory B] {a b c : B} {f g h i : a ⟶ b} {j : b ⟶ c} {α : f ≅ g} {η : g ⟶ h} {ηs : h ⟶ i} {ηs₁ : CategoryTheory.CategoryStruct.comp h j ⟶ CategoryTheory.CategoryStruct.comp i j} {η₁ : CategoryTheory.CategoryStruct.comp g j ⟶ CategoryTheory.CategoryStruct.comp h j} {η₂ : CategoryTheory.CategoryStruct.comp g j ⟶ CategoryTheory.CategoryStruct.comp i j} {η₃ : CategoryTheory.CategoryStruct.comp f j ⟶ CategoryTheory.CategoryStruct.comp i j} (e_ηs₁ : CategoryTheory.Bicategory.whiskerRight ηs j = ηs₁) (e_η₁ : CategoryTheory.Bicategory.whiskerRight η j = η₁) (e_η₂ : CategoryTheory.CategoryStruct.comp η₁ ηs₁ = η₂) (e_η₃ : CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRightIso α j).hom η₂ = η₃) : CategoryTheory.Bicategory.whiskerRight (CategoryTheory.CategoryStruct.comp α.hom (CategoryTheory.CategoryStruct.comp η ηs)) j = η₃

theorem Mathlib.Tactic.Bicategory.evalWhiskerRight_cons_whisker {B : Type u} [CategoryTheory.Bicategory B] {a b c d : B} {f : a ⟶ b} {g : a ⟶ c} {h i : b ⟶ c} {j : a ⟶ c} {k : c ⟶ d} {α : g ≅ CategoryTheory.CategoryStruct.comp f h} {η : h ⟶ i} {ηs : CategoryTheory.CategoryStruct.comp f i ⟶ j} {η₁ : CategoryTheory.CategoryStruct.comp h k ⟶ CategoryTheory.CategoryStruct.comp i k} {η₂ : CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp h k) ⟶ CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp i k)} {ηs₁ : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f i) k ⟶ CategoryTheory.CategoryStruct.comp j k} {ηs₂ : CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp i k) ⟶ CategoryTheory.CategoryStruct.comp j k} {η₃ : CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp h k) ⟶ CategoryTheory.CategoryStruct.comp j k} {η₄ : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f h) k ⟶ CategoryTheory.CategoryStruct.comp j k} {η₅ : CategoryTheory.CategoryStruct.comp g k ⟶ CategoryTheory.CategoryStruct.comp j k} (e_η₁ : CategoryTheory.Bicategory.whiskerRight (CategoryTheory.CategoryStruct.comp (CategoryTheory.Iso.refl h).hom (CategoryTheory.CategoryStruct.comp η (CategoryTheory.Iso.refl i).hom)) k = η₁) (e_η₂ : CategoryTheory.Bicategory.whiskerLeft f η₁ = η₂) (e_ηs₁ : CategoryTheory.Bicategory.whiskerRight ηs k = ηs₁) (e_ηs₂ : CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f i k).inv ηs₁ = ηs₂) (e_η₃ : CategoryTheory.CategoryStruct.comp η₂ ηs₂ = η₃) (e_η₄ : CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f h k).hom η₃ = η₄) (e_η₅ : CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRightIso α k).hom η₄ = η₅) : CategoryTheory.Bicategory.whiskerRight (CategoryTheory.CategoryStruct.comp α.hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f η) ηs)) k = η₅

theorem Mathlib.Tactic.Bicategory.evalWhiskerRight_comp {B : Type u} [CategoryTheory.Bicategory B] {a b c d : B} {f f' : a ⟶ b} {g : b ⟶ c} {h : c ⟶ d} {η : f ⟶ f'} {η₁ : CategoryTheory.CategoryStruct.comp f g ⟶ CategoryTheory.CategoryStruct.comp f' g} {η₂ : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g) h ⟶ CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f' g) h} {η₃ : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g) h ⟶ CategoryTheory.CategoryStruct.comp f' (CategoryTheory.CategoryStruct.comp g h)} {η₄ : CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp g h) ⟶ CategoryTheory.CategoryStruct.comp f' (CategoryTheory.CategoryStruct.comp g h)} (e_η₁ : CategoryTheory.Bicategory.whiskerRight η g = η₁) (e_η₂ : CategoryTheory.Bicategory.whiskerRight η₁ h = η₂) (e_η₃ : CategoryTheory.CategoryStruct.comp η₂ (CategoryTheory.Bicategory.associator f' g h).hom = η₃) (e_η₄ : CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f g h).inv η₃ = η₄) : CategoryTheory.Bicategory.whiskerRight η (CategoryTheory.CategoryStruct.comp g h) = η₄

theorem Mathlib.Tactic.Bicategory.evalWhiskerRight_id {B : Type u} [CategoryTheory.Bicategory B] {a b : B} {f g : a ⟶ b} {η : f ⟶ g} {η₁ : f ⟶ CategoryTheory.CategoryStruct.comp g (CategoryTheory.CategoryStruct.id b)} {η₂ : CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.id b) ⟶ CategoryTheory.CategoryStruct.comp g (CategoryTheory.CategoryStruct.id b)} (e_η₁ : CategoryTheory.CategoryStruct.comp η (CategoryTheory.Bicategory.rightUnitor g).inv = η₁) (e_η₂ : CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.rightUnitor f).hom η₁ = η₂) : CategoryTheory.Bicategory.whiskerRight η (CategoryTheory.CategoryStruct.id b) = η₂

theorem Mathlib.Tactic.Bicategory.eval_bicategoricalComp {B : Type u} [CategoryTheory.Bicategory B] {a b : B} {f g h i : a ⟶ b} {η η' : f ⟶ g} {α : g ≅ h} {θ θ' : h ⟶ i} {αθ : g ⟶ i} {ηαθ : f ⟶ i} (e_η : η = η') (e_θ : θ = θ') (e_αθ : CategoryTheory.CategoryStruct.comp α.hom θ' = αθ) (e_ηαθ : CategoryTheory.CategoryStruct.comp η' αθ = ηαθ) : CategoryTheory.CategoryStruct.comp η (CategoryTheory.CategoryStruct.comp α.hom θ) = ηαθ

@[instance_reducible]

instance Mathlib.Tactic.Bicategory.instMkEvalCompBicategoryM : BicategoryLike.MkEvalComp BicategoryM

Equations

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

@[instance_reducible]

instance Mathlib.Tactic.Bicategory.instMkEvalWhiskerLeftBicategoryM : BicategoryLike.MkEvalWhiskerLeft BicategoryM

Equations

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

@[instance_reducible]

instance Mathlib.Tactic.Bicategory.instMkEvalWhiskerRightBicategoryM : BicategoryLike.MkEvalWhiskerRight BicategoryM

Equations

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

@[instance_reducible]

instance Mathlib.Tactic.Bicategory.instMkEvalHorizontalCompBicategoryM : BicategoryLike.MkEvalHorizontalComp BicategoryM

Equations

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

@[instance_reducible]

instance Mathlib.Tactic.Bicategory.instMkEvalBicategoryM : BicategoryLike.MkEval BicategoryM

Equations

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

@[instance_reducible]

instance Mathlib.Tactic.Bicategory.instMonadNormalExprBicategoryM : BicategoryLike.MonadNormalExpr BicategoryM

Equations

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

@[instance_reducible]

instance Mathlib.Tactic.Bicategory.instMkMor₂BicategoryM_1 : BicategoryLike.MkMor₂ BicategoryM

Equations

• Mathlib.Tactic.Bicategory.instMkMor₂BicategoryM_1 = { ofExpr := Mathlib.Tactic.Bicategory.Mor₂OfExpr }