English
If f, g: X φ j → A satisfy inlX φ i j hij ≫ f = inlX φ i j hij ≫ g and inrX φ j ≫ f = inrX φ j ≫ g, then f = g.
Русский
Пусть f, g: X φ j → A удовлетворяют inlX φ i j hij ≫ f = inlX φ i j hij ≫ g и inrX φ j ≫ f = inrX φ j ≫ g, тогда f = g.
LaTeX
$$$ inlX\\,\\phi\\,i\\,j\\,hij \\circ f = inlX\\,\\phi\\,i\\,j\\,hij \\circ g \\;\\land\\; inrX\\,\\phi\\,j \\circ f = inrX\\,\\phi\\,j \\circ g \\Rightarrow f = g. $$$
Lean4
theorem ext_from_X (i j : ι) (hij : c.Rel j i) {A : C} {f g : X φ j ⟶ A} (h₁ : inlX φ i j hij ≫ f = inlX φ i j hij ≫ g)
(h₂ : inrX φ j ≫ f = inrX φ j ≫ g) : f = g :=
by
haveI := HasHomotopyCofiber.hasBinaryBiproduct φ _ _ hij
rw [← cancel_epi (XIsoBiprod φ j i hij).inv]
apply biprod.hom_ext'
· simpa [inlX] using h₁
· obtain rfl := c.next_eq' hij
simpa [inrX, dif_pos hij] using h₂
