English
If two pushout squares are vertically composed, the outer composition is again a pushout square.
Русский
Если два пушаута образуют вертикальное соединение, получившийся внешний квадрат снова является пушаутом.
LaTeX
$$$\text{Let } s: \operatorname{IsPushout}(h_{11}, v_{11}, v_{12}, h_{21}) \\ \\ t: \operatorname{IsPushout}(h_{21}, v_{21}, v_{22}, h_{31}) \\text{ then } \operatorname{IsPushout}(h_{11}, v_{11}\circ v_{21}, v_{12}\circ v_{22}, h_{31}).$$$
Lean4
/-- Paste two pushout squares "vertically" to obtain another pushout square.
The objects in the statement fit into the following diagram:
```
X₁₁ - h₁₁ -> X₁₂
| |
v₁₁ v₁₂
↓ ↓
X₂₁ - h₂₁ -> X₂₂
| |
v₂₁ v₂₂
↓ ↓
X₃₁ - h₃₁ -> X₃₂
```
-/
theorem paste_vert {X₁₁ X₁₂ X₂₁ X₂₂ X₃₁ X₃₂ : C} {h₁₁ : X₁₁ ⟶ X₁₂} {h₂₁ : X₂₁ ⟶ X₂₂} {h₃₁ : X₃₁ ⟶ X₃₂} {v₁₁ : X₁₁ ⟶ X₂₁}
{v₁₂ : X₁₂ ⟶ X₂₂} {v₂₁ : X₂₁ ⟶ X₃₁} {v₂₂ : X₂₂ ⟶ X₃₂} (s : IsPushout h₁₁ v₁₁ v₁₂ h₂₁)
(t : IsPushout h₂₁ v₂₁ v₂₂ h₃₁) : IsPushout h₁₁ (v₁₁ ≫ v₂₁) (v₁₂ ≫ v₂₂) h₃₁ :=
of_isColimit (pasteHorizIsPushout rfl s.isColimit t.isColimit)
