evalWhiskerRight_cons_whisker — Mathlib

Lean4
theorem evalWhiskerRight_cons_whisker {f : a ⟶ b} {g : a ⟶ c} {h i : b ⟶ c} {j : a ⟶ c} {k : c ⟶ d} {α : 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_η₅]
Похожие утверждения