English
If two morphisms f,g: A → (mappingCone φ).X_i have the same image under the projections to the fst and snd components of the mapping cone (with the appropriate degree indices), then f and g are equal.
Русский
Пусть два морфизма f,g: A → (mappingCone φ).X_i совпадают после проекции на fst φ и snd φ в соответствующих степенях; значит f = g.
LaTeX
$$$\forall i,j\in \mathbb{Z},\ hij: i+1=j,\ A,\ f,g:\, A\to (mappingCone(\varphi))X_i:\ (f\circ (fst\varphi)_{i,j,hij})=(g\circ (fst\varphi)_{i,j,hij})\land( f\circ (snd\varphi)_{i,i})=(g\circ (snd\varphi)_{i,i})\Rightarrow f=g.$$$
Lean4
theorem ext_to (i j : ℤ) (hij : i + 1 = j) {A : C} {f g : A ⟶ (mappingCone φ).X i}
(h₁ : f ≫ (fst φ).1.v i j hij = g ≫ (fst φ).1.v i j hij)
(h₂ : f ≫ (snd φ).v i i (add_zero i) = g ≫ (snd φ).v i i (add_zero i)) : f = g :=
homotopyCofiber.ext_to_X φ i j hij h₁ (by simpa [snd] using h₂)
