-- Mathlib/Algebra/Homology/HomotopyCofiber.lean
lemma ext_to_X (i j : ι) (hij : c.Rel i j) {A : C} {f g : A ⟶ X φ i}
    (h₁ : f ≫ fstX φ i j hij = g ≫ fstX φ i j hij) (h₂ : f ≫ sndX φ i = g ≫ sndX φ i) :
    f = g

Proof state:
case h₁
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G : HomologicalComplex C c
φ : F ⟶ G
inst✝¹ : HasHomotopyCofiber φ
inst✝ : DecidableRel c.Rel
i : ι
A : C
f g : A ⟶ X φ i
h₂ : f ≫ sndX φ i = g ≫ sndX φ i
hij : c.Rel i (c.next i)
h₁ : f ≫ fstX φ i (c.next i) hij = g ≫ fstX φ i (c.next i) hij
this : HasBinaryBiproduct (F.X (c.next i)) (G.X i)
⊢ (f ≫ (XIsoBiprod φ i (c.next i) hij).hom) ≫ biprod.snd = (g ≫ (XIsoBiprod φ i (c.next i) hij).hom) ≫ biprod.snd

Tactic:
simpa [sndX, dif_pos hij] using h₂

Result:
no goals

Proof state:
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G : HomologicalComplex C c
φ : F ⟶ G
inst✝¹ : HasHomotopyCofiber φ
inst✝ : DecidableRel c.Rel
i j : ι
hij : c.Rel i j
A : C
f g : A ⟶ X φ i
h₁ : f ≫ fstX φ i j hij = g ≫ fstX φ i j hij
h₂ : f ≫ sndX φ i = g ≫ sndX φ i
this : HasBinaryBiproduct (F.X j) (G.X i)
⊢ f = g

Tactic:
rw [← cancel_mono (XIsoBiprod φ i j hij).hom]

Result:
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G : HomologicalComplex C c
φ : F ⟶ G
inst✝¹ : HasHomotopyCofiber φ
inst✝ : DecidableRel c.Rel
i j : ι
hij : c.Rel i j
A : C
f g : A ⟶ X φ i
h₁ : f ≫ fstX φ i j hij = g ≫ fstX φ i j hij
h₂ : f ≫ sndX φ i = g ≫ sndX φ i
this : HasBinaryBiproduct (F.X j) (G.X i)
⊢ f ≫ (XIsoBiprod φ i j hij).hom = g ≫ (XIsoBiprod φ i j hij).hom

Proof state:
case h₁
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G : HomologicalComplex C c
φ : F ⟶ G
inst✝¹ : HasHomotopyCofiber φ
inst✝ : DecidableRel c.Rel
i j : ι
hij : c.Rel i j
A : C
f g : A ⟶ X φ i
h₁ : f ≫ fstX φ i j hij = g ≫ fstX φ i j hij
h₂ : f ≫ sndX φ i = g ≫ sndX φ i
this : HasBinaryBiproduct (F.X j) (G.X i)
⊢ (f ≫ (XIsoBiprod φ i j hij).hom) ≫ biprod.snd = (g ≫ (XIsoBiprod φ i j hij).hom) ≫ biprod.snd

Tactic:
obtain rfl := c.next_eq' hij

Result:
case h₁
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G : HomologicalComplex C c
φ : F ⟶ G
inst✝¹ : HasHomotopyCofiber φ
inst✝ : DecidableRel c.Rel
i : ι
A : C
f g : A ⟶ X φ i
h₂ : f ≫ sndX φ i = g ≫ sndX φ i
hij : c.Rel i (c.next i)
h₁ : f ≫ fstX φ i (c.next i) hij = g ≫ fstX φ i (c.next i) hij
this : HasBinaryBiproduct (F.X (c.next i)) (G.X i)
⊢ (f ≫ (XIsoBiprod φ i (c.next i) hij).hom) ≫ biprod.snd = (g ≫ (XIsoBiprod φ i (c.next i) hij).hom) ≫ biprod.snd

Proof state:
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G : HomologicalComplex C c
φ : F ⟶ G
inst✝¹ : HasHomotopyCofiber φ
inst✝ : DecidableRel c.Rel
i j : ι
hij : c.Rel i j
A : C
f g : A ⟶ X φ i
h₁ : f ≫ fstX φ i j hij = g ≫ fstX φ i j hij
h₂ : f ≫ sndX φ i = g ≫ sndX φ i
this : HasBinaryBiproduct (F.X j) (G.X i)
⊢ f ≫ (XIsoBiprod φ i j hij).hom = g ≫ (XIsoBiprod φ i j hij).hom

Tactic:
apply biprod.hom_ext

Result:
case h₀
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G : HomologicalComplex C c
φ : F ⟶ G
inst✝¹ : HasHomotopyCofiber φ
inst✝ : DecidableRel c.Rel
i j : ι
hij : c.Rel i j
A : C
f g : A ⟶ X φ i
h₁ : f ≫ fstX φ i j hij = g ≫ fstX φ i j hij
h₂ : f ≫ sndX φ i = g ≫ sndX φ i
this : HasBinaryBiproduct (F.X j) (G.X i)
⊢ (f ≫ (XIsoBiprod φ i j hij).hom) ≫ biprod.fst = (g ≫ (XIsoBiprod φ i j hij).hom) ≫ biprod.fst

case h₁
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G : HomologicalComplex C c
φ : F ⟶ G
inst✝¹ : HasHomotopyCofiber φ
inst✝ : DecidableRel c.Rel
i j : ι
hij : c.Rel i j
A : C
f g : A ⟶ X φ i
h₁ : f ≫ fstX φ i j hij = g ≫ fstX φ i j hij
h₂ : f ≫ sndX φ i = g ≫ sndX φ i
this : HasBinaryBiproduct (F.X j) (G.X i)
⊢ (f ≫ (XIsoBiprod φ i j hij).hom) ≫ biprod.snd = (g ≫ (XIsoBiprod φ i j hij).hom) ≫ biprod.snd

Proof state:
case h₀
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G : HomologicalComplex C c
φ : F ⟶ G
inst✝¹ : HasHomotopyCofiber φ
inst✝ : DecidableRel c.Rel
i j : ι
hij : c.Rel i j
A : C
f g : A ⟶ X φ i
h₁ : f ≫ fstX φ i j hij = g ≫ fstX φ i j hij
h₂ : f ≫ sndX φ i = g ≫ sndX φ i
this : HasBinaryBiproduct (F.X j) (G.X i)
⊢ (f ≫ (XIsoBiprod φ i j hij).hom) ≫ biprod.fst = (g ≫ (XIsoBiprod φ i j hij).hom) ≫ biprod.fst

Tactic:
simpa using h₁

Result:
no goals

Proof state:
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G : HomologicalComplex C c
φ : F ⟶ G
inst✝¹ : HasHomotopyCofiber φ
inst✝ : DecidableRel c.Rel
i j : ι
hij : c.Rel i j
A : C
f g : A ⟶ X φ i
h₁ : f ≫ fstX φ i j hij = g ≫ fstX φ i j hij
h₂ : f ≫ sndX φ i = g ≫ sndX φ i
⊢ f = g

Tactic:
haveI := HasHomotopyCofiber.hasBinaryBiproduct φ _ _ hij

Result:
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G : HomologicalComplex C c
φ : F ⟶ G
inst✝¹ : HasHomotopyCofiber φ
inst✝ : DecidableRel c.Rel
i j : ι
hij : c.Rel i j
A : C
f g : A ⟶ X φ i
h₁ : f ≫ fstX φ i j hij = g ≫ fstX φ i j hij
h₂ : f ≫ sndX φ i = g ≫ sndX φ i
this : HasBinaryBiproduct (F.X j) (G.X i)
⊢ f = g