English
Horizontal paste of two pullbacks yields a pullback for the composed arrows h11∘h12 and v11∘v12.
Русский
Горизонтальная конкатенация двух вытягиваемых квадратов даёт вытягиваемый квадрат для составленных стрелок h11∘h12 и v11∘v12.
LaTeX
$$$IsPullback(h_{11} \circ h_{12}, v_{11}, v_{13}, h_{21} \circ h_{22})$$$
Lean4
/-- Paste two pullback squares "horizontally" to obtain another pullback 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 paste_horiz {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 : IsPullback h₁₁ v₁₁ v₁₂ h₂₁)
(t : IsPullback h₁₂ v₁₂ v₁₃ h₂₂) : IsPullback (h₁₁ ≫ h₁₂) v₁₁ v₁₃ (h₂₁ ≫ h₂₂) :=
(paste_vert s.flip t.flip).flip
