Lean4
/-- Given
```
X₁ - f₁ -> X₂ - f₂ -> X₃
| | |
i₁ i₂ i₃
↓ ↓ ↓
Y₁ - g₁ -> Y₂ - g₂ -> Y₃
```
Then the big square is a pullback if both the small squares are.
-/
def pasteHorizIsPullback (H : IsLimit t₂) (H' : IsLimit t₁) : IsLimit (t₂.pasteHoriz t₁ hi₂) :=
by
apply PullbackCone.isLimitAux'
intro s
obtain ⟨l₂, hl₂, hl₂'⟩ := PullbackCone.IsLimit.lift' H (s.fst ≫ g₁) s.snd (by rw [← s.condition, Category.assoc])
obtain ⟨l₁, hl₁, hl₁'⟩ := PullbackCone.IsLimit.lift' H' s.fst l₂ (by rw [← hl₂, hi₂])
refine
⟨l₁, hl₁, by simp [reassoc_of% hl₁', hl₂'], ?_⟩
-- Uniqueness also follows from the universal property of both the small squares.
intro m hm₁ hm₂
apply PullbackCone.IsLimit.hom_ext H' (by simpa [hl₁] using hm₁)
apply PullbackCone.IsLimit.hom_ext H
· dsimp at hm₁
rw [Category.assoc, ← hi₂, ← t₁.condition, reassoc_of% hm₁, hl₁', hi₂, hl₂]
· simpa [hl₁', hl₂'] using hm₂
