English
Let a1, a2, a3 ∈ A. Then the hom component of shiftFunctorAdd C (a1+a2) a3 equals the appropriate composition of hom components from shiftFunctorAdd and shiftFunctor.
Русский
Пусть a1, a2, a3 ∈ A. Тогда гом-компонента shiftFunctorAdd C (a1+a2) a3 равна соответствующей композиции гом-компонентов shiftFunctorAdd и shiftFunctor.
LaTeX
$$$ (\\mathrm{shiftFunctorAdd} \\, C \\, (a_1 + a_2) \\, a_3).hom.app X = (\\mathrm{shiftFunctorAdd'} \\, C a_1 (a_2 + a_3) (a_1 + a_2 + a_3) (\\mathrm{add\\ assoc}).symm).hom.app X \\\\gg (\\mathrm{shiftFunctorAdd} \\ C a_2 a_3).hom.app (X⟦a_1⟧) $$$
Lean4
@[reassoc]
theorem shiftFunctorAdd_assoc_hom_app (a₁ a₂ a₃ : A) (X : C) :
(shiftFunctorAdd C (a₁ + a₂) a₃).hom.app X ≫ ((shiftFunctorAdd C a₁ a₂).hom.app X)⟦a₃⟧' =
(shiftFunctorAdd' C a₁ (a₂ + a₃) (a₁ + a₂ + a₃) (add_assoc _ _ _).symm).hom.app X ≫
(shiftFunctorAdd C a₂ a₃).hom.app (X⟦a₁⟧) :=
by simpa using NatTrans.congr_app (congr_arg Iso.hom (shiftFunctorAdd_assoc C a₁ a₂ a₃)) X
