English
Let f: S → X1 and g: S → X2, and consider pushout cocones c and c' of f and g. If there is an isomorphism e: c ≅ c' and elements x1 ∈ X1, x2 ∈ X2 such that c.inl x1 = c.inr x2, then the corresponding elements in c' are also identified: c'.inl x1 = c'.inr x2.
Русский
Пусть f: S → X1 и g: S → X2, и рассмотрим пушаут-коконы c и c' над f и g. Если существует изоморфизм e: c ≅ c' и элементы x1 ∈ X1, x2 ∈ X2 такие, что c.inl x1 = c.inr x2, то соответствующие образы в c' удовлетворяют c'.inl x1 = c'.inr x2.
LaTeX
$$$\\forall f:S \\to X_1\\,\\forall g:S \\to X_2\\,\\forall c,c':PushoutCocone f g\\, (e:c\\cong c')\\,\\forall x_1:X_1\\,\\forall x_2:X_2:\\; c.inl x_1 = c.inr x_2 \\Rightarrow c'.inl x_1 = c'.inr x_2$$$
Lean4
theorem pushoutCocone_inl_eq_inr_imp_of_iso {c c' : PushoutCocone f g} (e : c ≅ c') (x₁ : X₁) (x₂ : X₂)
(h : c.inl x₁ = c.inr x₂) : c'.inl x₁ = c'.inr x₂ :=
by
convert congr_arg e.hom.hom h
· exact congr_fun (e.hom.w WalkingSpan.left).symm x₁
· exact congr_fun (e.hom.w WalkingSpan.right).symm x₂
