English
Two pushout squares pasted horizontally yield a new pushout square.
Русский
Два пушаута, соединённые горизонтально, дают новый пушаут.
LaTeX
$$$\operatorname{IsPushout}((h_{11}\!\circ\! h_{12}), v_{11}, v_{13}, (h_{21}\!\circ\! h_{22}))$$$
Lean4
/-- Given a pushout square assembled from a pushout square on the left and
a commuting square on the right, the right square is a pushout square.
The objects in the statement fit into the following diagram:
```
X₁₁ - h₁₁ -> X₁₂ - h₁₂ -> X₁₃
| | |
v₁₁ v₁₂ v₁₃
↓ ↓ ↓
X₂₁ - h₂₁ -> X₂₂ - h₂₂ -> X₂₃
```
-/
theorem of_left {X₁₁ X₁₂ X₁₃ X₂₁ X₂₂ X₂₃ : C} {h₁₁ : X₁₁ ⟶ X₁₂} {h₁₂ : X₁₂ ⟶ X₁₃} {h₂₁ : X₂₁ ⟶ X₂₂} {h₂₂ : X₂₂ ⟶ X₂₃}
{v₁₁ : X₁₁ ⟶ X₂₁} {v₁₂ : X₁₂ ⟶ X₂₂} {v₁₃ : X₁₃ ⟶ X₂₃} (s : IsPushout (h₁₁ ≫ h₁₂) v₁₁ v₁₃ (h₂₁ ≫ h₂₂))
(p : h₁₂ ≫ v₁₃ = v₁₂ ≫ h₂₂) (t : IsPushout h₁₁ v₁₁ v₁₂ h₂₁) : IsPushout h₁₂ v₁₂ v₁₃ h₂₂ :=
(of_top s.flip p.symm t.flip).flip
