English
Associativity of multiplication for holors: the two ways of multiplying three holors are equal after transporting along the left associator; precisely, (x ⊗ y) ⊗ z equals (x ⊗ (y ⊗ z)).assocLeft.
Русский
Сопряжённость умножения Holor: два способа умножения трёх холоров совпадают после переноса вдоль левостороннего ассоциатора; то есть (x ⊗ y) ⊗ z = (x ⊗ (y ⊗ z)).assocLeft.
LaTeX
$$$((x \otimes y) \otimes z) = (x \otimes (y \otimes z)).assocLeft$$$
Lean4
theorem mul_assoc0 [Semigroup α] (x : Holor α ds₁) (y : Holor α ds₂) (z : Holor α ds₃) :
x ⊗ y ⊗ z = (x ⊗ (y ⊗ z)).assocLeft :=
funext fun t : HolorIndex (ds₁ ++ ds₂ ++ ds₃) => by
rw [assocLeft]
unfold mul
rw [mul_assoc, ← HolorIndex.take_take, ← HolorIndex.drop_take, ← HolorIndex.drop_drop, cast_type]
· rfl
rw [append_assoc]
