English
The horizontal composition of two commuting squares yields a new commuting square.
Русский
Горизонтальное сочетание двух коммутативных квадратов даёт новый коммутативный квадрат.
LaTeX
$$$CommSq f g h i \;\to\; CommSq f' h h' i' \rightarrow CommSq (f \ gg f') g h' (i \ ii')$$$
Lean4
/-- The horizontal composition of two commutative squares as below is a commutative square.
```
W ---f---> X ---f'--> X'
| | |
g h h'
| | |
v v v
Y ---i---> Z ---i'--> Z'
```
-/
theorem horiz_comp {W X X' Y Z Z' : C} {f : W ⟶ X} {f' : X ⟶ X'} {g : W ⟶ Y} {h : X ⟶ Z} {h' : X' ⟶ Z'} {i : Y ⟶ Z}
{i' : Z ⟶ Z'} (hsq₁ : CommSq f g h i) (hsq₂ : CommSq f' h h' i') : CommSq (f ≫ f') g h' (i ≫ i') :=
⟨by rw [← Category.assoc, Category.assoc, ← hsq₁.w, hsq₂.w, Category.assoc]⟩
