English
If a pushout is formed by composing maps on the left, the right square inherits a pushout property.
Русский
Если пушаут образован за счёт композиции левых стрелок, правая часть квадрата сохраняет свойство пушаута.
LaTeX
$$$\operatorname{IsPushout}(h_{11}\circ h_{12}, v_{11}, v_{13}, h_{21}\circ h_{22})$ with t and p conditions$$
Lean4
/-- Variant of `IsPushout.of_right` where `h₂₂` is induced from a morphism `h₂₃ : X₂₁ ⟶ X₂₃`, and
the universal property of the left 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₂₃)
(t : IsPushout h₁₁ v₁₁ v₁₂ h₂₁) : IsPushout h₁₂ v₁₂ v₁₃ (t.desc (h₁₂ ≫ v₁₃) h₂₃ (by rw [← Category.assoc, s.w])) :=
of_left ((t.inr_desc _ _ _).symm ▸ s) (by simp only [inl_desc]) t
