English
When regrouping the three-component tensor, the composite with the new component equals the original iota map composed with the regrouped iota map, after adjusting indices via the associativity identity.
Русский
При перераспределении тройной тензорной конструкции композиция с новым компонентом равна исходной карте iota, далее композиция новой карты с учётом перестройки индексов через тождество ассоциативности.
LaTeX
$$$\iotaTensorObj_3 X_1 X_2 X_3 i_1 i_2 i_3 j h = (X_1 i_1 ◁ \iotaTensorObj X_2 X_3 i_2 i_3 i_{23} h') \circ \iotaTensorObj X_1 (tensorObj X_2 X_3) i_1 i_{23} j (by rw[...]).$$$
Lean4
@[reassoc]
theorem ιTensorObj₃_eq (i₁ i₂ i₃ j : I) (h : i₁ + i₂ + i₃ = j) (i₂₃ : I) (h' : i₂ + i₃ = i₂₃) :
ιTensorObj₃ X₁ X₂ X₃ i₁ i₂ i₃ j h =
(X₁ i₁ ◁ ιTensorObj X₂ X₃ i₂ i₃ i₂₃ h') ≫
ιTensorObj X₁ (tensorObj X₂ X₃) i₁ i₂₃ j (by rw [← h', ← add_assoc, h]) :=
by
subst h'
rfl
