English
With the same data as above, the inv.app X for the left-hand side equals the inv.app X for the right-hand side after applying associativity of shifts.
Русский
С теми же данными, inv.app X левой стороны равен inv.app X правой стороны после применения ассоциативности смещений.
LaTeX
$$$ ((\\mathrm{shiftFunctorAdd} \\, C a_1 a_2_3).inv.app X) \\\\gg ((\\mathrm{shiftFunctorAdd} \\, C a_2 a_3).inv.app (X a_1)) = ((\\mathrm{shiftFunctorAdd'} \\, C a_1 a_2 a_3).inv.app X) \\\\gg ((\\mathrm{shiftFunctorAdd'} \\, C a_2 a_3 a_3).inv.app X) $$$
Lean4
@[reassoc]
theorem shiftFunctorAdd_assoc_inv_app (a₁ a₂ a₃ : A) (X : C) :
((shiftFunctorAdd C a₁ a₂).inv.app X)⟦a₃⟧' ≫ (shiftFunctorAdd C (a₁ + a₂) a₃).inv.app X =
(shiftFunctorAdd C a₂ a₃).inv.app (X⟦a₁⟧) ≫
(shiftFunctorAdd' C a₁ (a₂ + a₃) (a₁ + a₂ + a₃) (add_assoc _ _ _).symm).inv.app X :=
by simpa using NatTrans.congr_app (congr_arg Iso.inv (shiftFunctorAdd_assoc C a₁ a₂ a₃)) X
