evalWhiskerRight_cons_whisker — Mathlib

Lean4
theorem evalWhiskerRight_cons_whisker {f g h i j k : C} {α : g ≅ f ⊗ h} {η : h ⟶ i} {ηs : f ⊗ i ⟶ j}
    {η₁ : h ⊗ k ⟶ i ⊗ k} {η₂ : f ⊗ (h ⊗ k) ⟶ f ⊗ (i ⊗ k)} {ηs₁ : (f ⊗ i) ⊗ k ⟶ j ⊗ k} {ηs₂ : f ⊗ (i ⊗ k) ⟶ j ⊗ k}
    {η₃ : f ⊗ (h ⊗ k) ⟶ j ⊗ k} {η₄ : (f ⊗ h) ⊗ k ⟶ j ⊗ k} {η₅ : g ⊗ k ⟶ j ⊗ k}
    (e_η₁ : ((Iso.refl _).hom ≫ η ≫ (Iso.refl _).hom) ▷ k = η₁) (e_η₂ : f ◁ η₁ = η₂) (e_ηs₁ : ηs ▷ k = ηs₁)
    (e_ηs₂ : (α_ _ _ _).inv ≫ ηs₁ = ηs₂) (e_η₃ : η₂ ≫ ηs₂ = η₃) (e_η₄ : (α_ _ _ _).hom ≫ η₃ = η₄)
    (e_η₅ : (whiskerRightIso α k).hom ≫ η₄ = η₅) : (α.hom ≫ (f ◁ η) ≫ ηs) ▷ k = η₅ :=
  by
  simp at e_η₁ e_η₅
  simp [e_η₁, e_η₂, e_ηs₁, e_ηs₂, e_η₃, e_η₄, e_η₅]
Похожие утверждения