English
Given the same data as in the previous item, the inv.app X for the left-hand side equals the inv.app X for the right-hand side after applying the associativity isomorphism.
Русский
С учетом тех же данных, inv.app X левой стороны равен inv.app X правой стороны после применения изоморфизма ассоциативности.
LaTeX
$$$ ((\\mathrm{shiftFunctorAdd'} \\, C a_1 a_2 a_1_2 h_{12}).inv.\\mathrm{app} \\, X) \\langle a_3 \\rangle' \\gg (\\mathrm{shiftFunctorAdd'} \\, C a_1 a_2_3 a_1_2_3 (..)).inv.app X = (\\mathrm{shiftFunctorAdd'} \\, C a_2 a_3 a_2_3 h_{23}).inv.app (X\\langle a_1 \\rangle) \\gg (\\mathrm{shiftFunctorAdd'} \\, C a_1 a_2_3 a_1_2_3 (..)).inv.app X $$$$
Lean4
@[reassoc]
theorem shiftFunctorAdd'_assoc_inv_app (a₁ a₂ a₃ a₁₂ a₂₃ a₁₂₃ : A) (h₁₂ : a₁ + a₂ = a₁₂) (h₂₃ : a₂ + a₃ = a₂₃)
(h₁₂₃ : a₁ + a₂ + a₃ = a₁₂₃) (X : C) :
((shiftFunctorAdd' C a₁ a₂ a₁₂ h₁₂).inv.app X)⟦a₃⟧' ≫
(shiftFunctorAdd' C a₁₂ a₃ a₁₂₃ (by rw [← h₁₂, h₁₂₃])).inv.app X =
(shiftFunctorAdd' C a₂ a₃ a₂₃ h₂₃).inv.app (X⟦a₁⟧) ≫
(shiftFunctorAdd' C a₁ a₂₃ a₁₂₃ (by rw [← h₂₃, ← add_assoc, h₁₂₃])).inv.app X :=
by simpa using NatTrans.congr_app (congr_arg Iso.inv (shiftFunctorAdd'_assoc C _ _ _ _ _ _ h₁₂ h₂₃ h₁₂₃)) X
