Lean4
/-- Given
```
X₁ - f₁ -> X₂ - f₂ -> X₃
| | |
i₁ i₂ i₃
∨ ∨ ∨
Y₁ - g₁ -> Y₂ - g₂ -> Y₃
```
Then the big square is a pushout if both the small squares are.
-/
def pasteHorizIsPushout (H : IsColimit t₁) (H' : IsColimit t₂) : IsColimit (t₁.pasteHoriz t₂ hi₂) :=
by
apply PushoutCocone.isColimitAux'
intro s
obtain ⟨l₁, hl₁, hl₁'⟩ := PushoutCocone.IsColimit.desc' H s.inl (f₂ ≫ s.inr) (by rw [s.condition, Category.assoc])
obtain ⟨l₂, hl₂, hl₂'⟩ := PushoutCocone.IsColimit.desc' H' l₁ s.inr (by rw [← hl₁', hi₂])
refine
⟨l₂, by simp [hl₂, hl₁], hl₂', ?_⟩
-- Uniqueness also follows from the universal property of both the small squares.
intro m hm₁ hm₂
apply PushoutCocone.IsColimit.hom_ext H' _ (by simpa [hl₂'] using hm₂)
simp only [PushoutCocone.mk_pt, PushoutCocone.mk_ι_app, Category.assoc] at hm₁ hm₂
apply PushoutCocone.IsColimit.hom_ext H
· rw [hm₁, ← hl₁, hl₂]
· rw [← hi₂, reassoc_of% t₂.condition, reassoc_of% t₂.condition, hm₂, hl₂']
