evalHorizontalCompAux'_of_whisker

Lean4

theorem evalHorizontalCompAux'_of_whisker {f f' g g' h : C} {η : g ⟶ h} {θ : f' ⟶ g'} {η₁ : g ⊗ f ⟶ h ⊗ f}
    {ηθ : (g ⊗ f) ⊗ f' ⟶ (h ⊗ f) ⊗ g'} {ηθ₁ : (g ⊗ f) ⊗ f' ⟶ h ⊗ (f ⊗ g')} {ηθ₂ : g ⊗ (f ⊗ f') ⟶ h ⊗ (f ⊗ g')}
    (e_η₁ : η ▷ f = η₁) (e_ηθ : η₁ ⊗ₘ ((Iso.refl _).hom ≫ θ ≫ (Iso.refl _).hom) = ηθ)
    (e_ηθ₁ : ηθ ≫ (α_ _ _ _).hom = ηθ₁) (e_ηθ₂ : (α_ _ _ _).inv ≫ ηθ₁ = ηθ₂) : η ⊗ₘ (f ◁ θ) = ηθ₂ :=
  by
  simp only [← e_η₁, ← e_ηθ, ← e_ηθ₁, ← e_ηθ₂]
  simp [MonoidalCategory.tensorHom_def]

Похожие утверждения