awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.HomotopyCofiber
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex.{v_1, u_1, u_2} C c
inst_2 : DecidableRel c.Rel
inst_3 : ∀ (i : ι), HasBinaryBiproduct.{v_1, u_1} (K.X i) (K.X i)
inst_4 : K.HasCylinder
i j : ι
hij : c.Rel j i
pos :
  ∀ (hj : ∃ (k : ι), c.Rel k j),
    CategoryStruct.comp (Y := homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j)
        (inlX K i j hij : K.X i ⟶ K.cylinder.X j)
        (Hom.f
          (Homotopy.nullHomotopicMap' fun (i j : ι) (hij : c.Rel j i) ↦
            homotopyCofiber.sndX (biprod.lift (𝟙 K) (-𝟙 K)) i ≫ Hom.f biprod.snd i ≫ inlX K i j hij)
          j) =
      inlX K i j hij ≫
        HSub.hSub (α :=
          homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j ⟶
            homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j)
          (Hom.f (π K) j ≫ Hom.f (ι₀ K) j) (𝟙 (homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j))
neg :
  ∀ (hj : ∀ (k : ι), ¬c.Rel k j),
    CategoryStruct.comp (Y := homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j)
        (inlX K i j hij : K.X i ⟶ K.cylinder.X j)
        (Hom.f
          (Homotopy.nullHomotopicMap' fun (i j : ι) (hij : c.Rel j i) ↦
            homotopyCofiber.sndX (biprod.lift (𝟙 K) (-𝟙 K)) i ≫ Hom.f biprod.snd i ≫ inlX K i j hij)
          j) =
      inlX K i j hij ≫
        HSub.hSub (α :=
          homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j ⟶
            homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j)
          (Hom.f (π K) j ≫ Hom.f (ι₀ K) j) (𝟙 (homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j))
⊢ CategoryStruct.comp (Y := homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j)
      (inlX K i j hij : K.X i ⟶ K.cylinder.X j)
      (Hom.f
        (Homotopy.nullHomotopicMap' fun (i j : ι) (hij : c.Rel j i) ↦
          homotopyCofiber.sndX (biprod.lift (𝟙 K) (-𝟙 K)) i ≫ Hom.f biprod.snd i ≫ inlX K i j hij)
        j) =
    inlX K i j hij ≫
      HSub.hSub (α :=
        homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j ⟶
          homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j)
        (Hom.f (π K) j ≫ Hom.f (ι₀ K) j) (𝟙 (homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j))

Tactic:
by_cases! hj : ∃ (k : ι), c.Rel k j
-- Module: Mathlib.Algebra.Homology.HomotopyCofiber
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex.{v_1, u_1, u_2} C c
inst_2 : DecidableRel c.Rel
inst_3 : ∀ (i : ι), HasBinaryBiproduct.{v_1, u_1} (K.X i) (K.X i)
inst_4 : K.HasCylinder
i j : ι
hij : c.Rel j i
hj : ∃ (k : ι), c.Rel k j
pos :
  ∀ (k : ι) (hjk : c.Rel k j),
    CategoryStruct.comp (Y := homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j)
        (inlX K i j hij : K.X i ⟶ K.cylinder.X j)
        (Hom.f
          (Homotopy.nullHomotopicMap' fun (i j : ι) (hij : c.Rel j i) ↦
            homotopyCofiber.sndX (biprod.lift (𝟙 K) (-𝟙 K)) i ≫ Hom.f biprod.snd i ≫ inlX K i j hij)
          j) =
      inlX K i j hij ≫
        HSub.hSub (α :=
          homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j ⟶
            homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j)
          (Hom.f (π K) j ≫ Hom.f (ι₀ K) j) (𝟙 (homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j))
⊢ CategoryStruct.comp (Y := homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j)
      (inlX K i j hij : K.X i ⟶ K.cylinder.X j)
      (Hom.f
        (Homotopy.nullHomotopicMap' fun (i j : ι) (hij : c.Rel j i) ↦
          homotopyCofiber.sndX (biprod.lift (𝟙 K) (-𝟙 K)) i ≫ Hom.f biprod.snd i ≫ inlX K i j hij)
        j) =
    inlX K i j hij ≫
      HSub.hSub (α :=
        homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j ⟶
          homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j)
        (Hom.f (π K) j ≫ Hom.f (ι₀ K) j) (𝟙 (homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j))

Tactic:
obtain ⟨k, hjk⟩ := hj
-- Module: Mathlib.Algebra.Homology.HomotopyCofiber
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex.{v_1, u_1, u_2} C c
inst_2 : DecidableRel c.Rel
inst_3 : ∀ (i : ι), HasBinaryBiproduct.{v_1, u_1} (K.X i) (K.X i)
inst_4 : K.HasCylinder
i j : ι
hij : c.Rel j i
k : ι
hjk : c.Rel k j
⊢ CategoryStruct.comp (Y := homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j)
      (inlX K i j hij : K.X i ⟶ K.cylinder.X j)
      (Hom.f
        (Homotopy.nullHomotopicMap' fun (i j : ι) (hij : c.Rel j i) ↦
          homotopyCofiber.sndX (biprod.lift (𝟙 K) (-𝟙 K)) i ≫ Hom.f biprod.snd i ≫ inlX K i j hij)
        j) =
    inlX K i j hij ≫
      HSub.hSub (α :=
        homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j ⟶
          homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j)
        (Hom.f (π K) j ≫ Hom.f (ι₀ K) j) (𝟙 (homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j))

Tactic:
simp only [assoc, Homotopy.nullHomotopicMap'_f hjk hij, homotopyCofiber_X, homotopyCofiber_d,
      homotopyCofiber.d_sndX_assoc _ _ _ hij, add_comp, comp_add, homotopyCofiber.inlX_fstX_assoc,
      homotopyCofiber.inlX_sndX_assoc, zero_comp, add_zero, comp_sub, inlX_π_assoc, comp_id,
      zero_sub, ← HomologicalComplex.comp_f_assoc, biprod.lift_snd, neg_f_apply, id_f,
      neg_comp, id_comp]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.biprod.lift_snd, HomologicalComplex.homotopyCofiber_X, HomologicalComplex.homotopyCofiber.inlX_sndX_assoc, HomologicalComplex.id_f, CategoryTheory.Category.comp_id, HomologicalComplex.cylinder.inlX_π_assoc, CategoryTheory.Preadditive.add_comp, HomologicalComplex.homotopyCofiber.inlX_fstX_assoc, CategoryTheory.Preadditive.comp_add, CategoryTheory.Preadditive.neg_comp, HomologicalComplex.homotopyCofiber_d, CategoryTheory.Limits.zero_comp, Homotopy.nullHomotopicMap'_f, add_zero, CategoryTheory.Preadditive.comp_sub, HomologicalComplex.homotopyCofiber.d_sndX_assoc, HomologicalComplex.neg_f_apply, HomologicalComplex.comp_f_assoc, zero_sub, CategoryTheory.Category.id_comp
-- Module: Mathlib.Algebra.Homology.HomotopyCofiber
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex.{v_1, u_1, u_2} C c
inst_2 : DecidableRel c.Rel
inst_3 : ∀ (i : ι), HasBinaryBiproduct.{v_1, u_1} (K.X i) (K.X i)
inst_4 : K.HasCylinder
i j : ι
hij : c.Rel j i
hj : ∀ (k : ι), ¬c.Rel k j
⊢ CategoryStruct.comp (Y := homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j)
      (inlX K i j hij : K.X i ⟶ K.cylinder.X j)
      (Hom.f
        (Homotopy.nullHomotopicMap' fun (i j : ι) (hij : c.Rel j i) ↦
          homotopyCofiber.sndX (biprod.lift (𝟙 K) (-𝟙 K)) i ≫ Hom.f biprod.snd i ≫ inlX K i j hij)
        j) =
    inlX K i j hij ≫
      HSub.hSub (α :=
        homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j ⟶
          homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j)
        (Hom.f (π K) j ≫ Hom.f (ι₀ K) j) (𝟙 (homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j))

Tactic:
simp only [Homotopy.nullHomotopicMap'_f_of_not_rel_right hij hj,
      homotopyCofiber_X, homotopyCofiber_d, assoc, comp_sub, comp_id,
      homotopyCofiber.d_sndX_assoc _ _ _ hij, add_comp, comp_add, zero_comp, add_zero,
      homotopyCofiber.inlX_fstX_assoc, homotopyCofiber.inlX_sndX_assoc,
      ← HomologicalComplex.comp_f_assoc, biprod.lift_snd, neg_f_apply, id_f, neg_comp,
      id_comp, inlX_π_assoc, zero_sub]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.biprod.lift_snd, HomologicalComplex.homotopyCofiber_X, HomologicalComplex.homotopyCofiber.inlX_sndX_assoc, HomologicalComplex.id_f, CategoryTheory.Category.comp_id, HomologicalComplex.cylinder.inlX_π_assoc, CategoryTheory.Preadditive.add_comp, HomologicalComplex.homotopyCofiber.inlX_fstX_assoc, CategoryTheory.Preadditive.comp_add, CategoryTheory.Preadditive.neg_comp, HomologicalComplex.homotopyCofiber_d, CategoryTheory.Limits.zero_comp, Homotopy.nullHomotopicMap'_f_of_not_rel_right, add_zero, CategoryTheory.Preadditive.comp_sub, HomologicalComplex.homotopyCofiber.d_sndX_assoc, HomologicalComplex.neg_f_apply, HomologicalComplex.comp_f_assoc, zero_sub, CategoryTheory.Category.id_comp
-- Module: Mathlib.Algebra.Homology.HomotopyCofiber
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex.{v_1, u_1, u_2} C c
inst_2 : DecidableRel c.Rel
inst_3 : ∀ (i : ι), HasBinaryBiproduct.{v_1, u_1} (K.X i) (K.X i)
inst_4 : K.HasCylinder
hc : ∀ (j : ι), ∃ (i : ι), c.Rel i j
j : ι
⊢ CategoryStruct.comp (Y := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) biprod.fst =
    HSub.hSub (α := K ⟶ K ⊞ K) biprod.inl biprod.inr ≫ biprod.fst

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.HomotopyCofiber
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex.{v_1, u_1, u_2} C c
inst_2 : DecidableRel c.Rel
inst_3 : ∀ (i : ι), HasBinaryBiproduct.{v_1, u_1} (K.X i) (K.X i)
inst_4 : K.HasCylinder
hc : ∀ (j : ι), ∃ (i : ι), c.Rel i j
j : ι
⊢ CategoryStruct.comp (Y := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) biprod.snd =
    HSub.hSub (α := K ⟶ K ⊞ K) biprod.inl biprod.inr ≫ biprod.snd

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.HomotopyCofiber
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex.{v_1, u_1, u_2} C c
inst_2 : DecidableRel c.Rel
inst_3 : ∀ (i : ι), HasBinaryBiproduct.{v_1, u_1} (K.X i) (K.X i)
inst_4 : K.HasCylinder
hc : ∀ (j : ι), ∃ (i : ι), c.Rel i j
j : ι
⊢ biprod.lift (𝟙 K) (-𝟙 K) = HSub.hSub (α := K ⟶ K ⊞ K) biprod.inl biprod.inr

Tactic:
have : biprod.lift (𝟙 K) (-𝟙 K) = biprod.inl - biprod.inr :=
    biprod.hom_ext _ _ (by simp) (by simp)
-- Module: Mathlib.Algebra.Homology.HomotopyCofiber
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex.{v_1, u_1, u_2} C c
inst_2 : DecidableRel c.Rel
inst_3 : ∀ (i : ι), HasBinaryBiproduct.{v_1, u_1} (K.X i) (K.X i)
inst_4 : K.HasCylinder
hc : ∀ (j : ι), ∃ (i : ι), c.Rel i j
j : ι
this : biprod.lift (𝟙 K) (-𝟙 K) = HSub.hSub (α := K ⟶ K ⊞ K) biprod.inl biprod.inr
obtain :
  ∀ (i : ι) (hij : c.Rel i j), inrX K j ≫ Hom.f (nullHomotopicMap K) j = inrX K j ≫ (π K ≫ ι₀ K - 𝟙 K.cylinder).f j
⊢ inrX K j ≫ Hom.f (nullHomotopicMap K) j = inrX K j ≫ (π K ≫ ι₀ K - 𝟙 K.cylinder).f j

Tactic:
obtain ⟨i, hij⟩ := hc j
-- Module: Mathlib.Algebra.Homology.HomotopyCofiber
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex.{v_1, u_1, u_2} C c
inst_2 : DecidableRel c.Rel
inst_3 : ∀ (i : ι), HasBinaryBiproduct.{v_1, u_1} (K.X i) (K.X i)
inst_4 : K.HasCylinder
hc : ∀ (j : ι), ∃ (i : ι), c.Rel i j
j : ι
this : biprod.lift (𝟙 K) (-𝟙 K) = HSub.hSub (α := K ⟶ K ⊞ K) biprod.inl biprod.inr
i : ι
hij : c.Rel i j
dsimp :
  CategoryStruct.comp (Y := homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j)
      (inrX K j : (K ⊞ K).X j ⟶ K.cylinder.X j)
      (Hom.f
        (Homotopy.nullHomotopicMap' fun (i j : ι) (hij : c.Rel j i) ↦
          homotopyCofiber.sndX (biprod.lift (𝟙 K) (-𝟙 K)) i ≫ Hom.f biprod.snd i ≫ inlX K i j hij)
        j) =
    inrX K j ≫
      HSub.hSub (α :=
        homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j ⟶
          homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j)
        (Hom.f (π K) j ≫ Hom.f (ι₀ K) j) (𝟙 (homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j))
⊢ inrX K j ≫ Hom.f (nullHomotopicMap K) j = inrX K j ≫ (π K ≫ ι₀ K - 𝟙 K.cylinder).f j

Tactic:
dsimp [nullHomotopicMap]

Premises used: HomologicalComplex.cylinder.πCompι₀Homotopy.nullHomotopicMap
-- Module: Mathlib.Algebra.Homology.HomotopyCofiber
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex.{v_1, u_1, u_2} C c
inst_2 : DecidableRel c.Rel
inst_3 : ∀ (i : ι), HasBinaryBiproduct.{v_1, u_1} (K.X i) (K.X i)
inst_4 : K.HasCylinder
hc : ∀ (j : ι), ∃ (i : ι), c.Rel i j
j : ι
this : biprod.lift (𝟙 K) (-𝟙 K) = HSub.hSub (α := K ⟶ K ⊞ K) biprod.inl biprod.inr
i : ι
hij : c.Rel i j
pos :
  ∀ (hj : ∃ (k : ι), c.Rel j k),
    CategoryStruct.comp (Y := homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j)
        (inrX K j : (K ⊞ K).X j ⟶ K.cylinder.X j)
        (Hom.f
          (Homotopy.nullHomotopicMap' fun (i j : ι) (hij : c.Rel j i) ↦
            homotopyCofiber.sndX (biprod.lift (𝟙 K) (-𝟙 K)) i ≫ Hom.f biprod.snd i ≫ inlX K i j hij)
          j) =
      inrX K j ≫
        HSub.hSub (α :=
          homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j ⟶
            homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j)
          (Hom.f (π K) j ≫ Hom.f (ι₀ K) j) (𝟙 (homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j))
neg :
  ∀ (hj : ¬∃ (k : ι), c.Rel j k),
    CategoryStruct.comp (Y := homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j)
        (inrX K j : (K ⊞ K).X j ⟶ K.cylinder.X j)
        (Hom.f
          (Homotopy.nullHomotopicMap' fun (i j : ι) (hij : c.Rel j i) ↦
            homotopyCofiber.sndX (biprod.lift (𝟙 K) (-𝟙 K)) i ≫ Hom.f biprod.snd i ≫ inlX K i j hij)
          j) =
      inrX K j ≫
        HSub.hSub (α :=
          homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j ⟶
            homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j)
          (Hom.f (π K) j ≫ Hom.f (ι₀ K) j) (𝟙 (homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j))
⊢ CategoryStruct.comp (Y := homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j)
      (inrX K j : (K ⊞ K).X j ⟶ K.cylinder.X j)
      (Hom.f
        (Homotopy.nullHomotopicMap' fun (i j : ι) (hij : c.Rel j i) ↦
          homotopyCofiber.sndX (biprod.lift (𝟙 K) (-𝟙 K)) i ≫ Hom.f biprod.snd i ≫ inlX K i j hij)
        j) =
    inrX K j ≫
      HSub.hSub (α :=
        homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j ⟶
          homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j)
        (Hom.f (π K) j ≫ Hom.f (ι₀ K) j) (𝟙 (homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j))

Tactic:
by_cases hj : ∃ (k : ι), c.Rel j k
-- Module: Mathlib.Algebra.Homology.HomotopyCofiber
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex.{v_1, u_1, u_2} C c
inst_2 : DecidableRel c.Rel
inst_3 : ∀ (i : ι), HasBinaryBiproduct.{v_1, u_1} (K.X i) (K.X i)
inst_4 : K.HasCylinder
hc : ∀ (j : ι), ∃ (i : ι), c.Rel i j
j : ι
this : biprod.lift (𝟙 K) (-𝟙 K) = HSub.hSub (α := K ⟶ K ⊞ K) biprod.inl biprod.inr
i : ι
hij : c.Rel i j
hj : ∃ (k : ι), c.Rel j k
pos :
  ∀ (k : ι) (hjk : c.Rel j k),
    CategoryStruct.comp (Y := homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j)
        (inrX K j : (K ⊞ K).X j ⟶ K.cylinder.X j)
        (Hom.f
          (Homotopy.nullHomotopicMap' fun (i j : ι) (hij : c.Rel j i) ↦
            homotopyCofiber.sndX (biprod.lift (𝟙 K) (-𝟙 K)) i ≫ Hom.f biprod.snd i ≫ inlX K i j hij)
          j) =
      inrX K j ≫
        HSub.hSub (α :=
          homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j ⟶
            homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j)
          (Hom.f (π K) j ≫ Hom.f (ι₀ K) j) (𝟙 (homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j))
⊢ CategoryStruct.comp (Y := homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j)
      (inrX K j : (K ⊞ K).X j ⟶ K.cylinder.X j)
      (Hom.f
        (Homotopy.nullHomotopicMap' fun (i j : ι) (hij : c.Rel j i) ↦
          homotopyCofiber.sndX (biprod.lift (𝟙 K) (-𝟙 K)) i ≫ Hom.f biprod.snd i ≫ inlX K i j hij)
        j) =
    inrX K j ≫
      HSub.hSub (α :=
        homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j ⟶
          homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j)
        (Hom.f (π K) j ≫ Hom.f (ι₀ K) j) (𝟙 (homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j))

Tactic:
obtain ⟨k, hjk⟩ := hj
-- Module: Mathlib.Algebra.Homology.HomotopyCofiber
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex.{v_1, u_1, u_2} C c
inst_2 : DecidableRel c.Rel
inst_3 : ∀ (i : ι), HasBinaryBiproduct.{v_1, u_1} (K.X i) (K.X i)
inst_4 : K.HasCylinder
hc : ∀ (j : ι), ∃ (i : ι), c.Rel i j
j : ι
this : biprod.lift (𝟙 K) (-𝟙 K) = HSub.hSub (α := K ⟶ K ⊞ K) biprod.inl biprod.inr
i : ι
hij : c.Rel i j
k : ι
hjk : c.Rel j k
pos :
  Hom.f biprod.snd j ≫ Hom.f (biprod.lift (𝟙 K) (-𝟙 K)) j ≫ homotopyCofiber.inrX (biprod.lift (𝟙 K) (-𝟙 K)) j =
    HSub.hSub (α := (K ⊞ K).X j ⟶ homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j) (β :=
      (K ⊞ K).X j ⟶ homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j)
      (Hom.f (biprod.desc (𝟙 K) (𝟙 K)) j ≫ Hom.f (ι₀ K) j :
        (K ⊞ K).X j ⟶ homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j)
      (inrX K j : (K ⊞ K).X j ⟶ K.cylinder.X j)
⊢ CategoryStruct.comp (Y := homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j)
      (inrX K j : (K ⊞ K).X j ⟶ K.cylinder.X j)
      (Hom.f
        (Homotopy.nullHomotopicMap' fun (i j : ι) (hij : c.Rel j i) ↦
          homotopyCofiber.sndX (biprod.lift (𝟙 K) (-𝟙 K)) i ≫ Hom.f biprod.snd i ≫ inlX K i j hij)
        j) =
    inrX K j ≫
      HSub.hSub (α :=
        homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j ⟶
          homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j)
        (Hom.f (π K) j ≫ Hom.f (ι₀ K) j) (𝟙 (homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j))

Tactic:
simp only [Homotopy.nullHomotopicMap'_f hij hjk,
      homotopyCofiber_X, homotopyCofiber_d, assoc, comp_add,
      homotopyCofiber.inrX_d_assoc, homotopyCofiber.inrX_sndX_assoc, comp_sub,
      inrX_π_assoc, comp_id, ← Hom.comm_assoc, homotopyCofiber.inlX_d _ _ _ _ _ hjk,
      comp_neg, add_neg_cancel_left]

Premises used: CategoryTheory.Category.assoc, add_neg_cancel_left, HomologicalComplex.homotopyCofiber.inrX_sndX_assoc, HomologicalComplex.homotopyCofiber_X, HomologicalComplex.homotopyCofiber.inrX_d_assoc, CategoryTheory.Preadditive.comp_neg, CategoryTheory.Category.comp_id, HomologicalComplex.cylinder.inrX_π_assoc, HomologicalComplex.homotopyCofiber.inlX_d, CategoryTheory.Preadditive.comp_add, HomologicalComplex.Hom.comm_assoc, HomologicalComplex.homotopyCofiber_d, Homotopy.nullHomotopicMap'_f, CategoryTheory.Preadditive.comp_sub
-- Module: Mathlib.Algebra.Homology.HomotopyCofiber
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex.{v_1, u_1, u_2} C c
inst_2 : DecidableRel c.Rel
inst_3 : ∀ (i : ι), HasBinaryBiproduct.{v_1, u_1} (K.X i) (K.X i)
inst_4 : K.HasCylinder
hc : ∀ (j : ι), ∃ (i : ι), c.Rel i j
j : ι
this : biprod.lift (𝟙 K) (-𝟙 K) = HSub.hSub (α := K ⟶ K ⊞ K) biprod.inl biprod.inr
i : ι
hij : c.Rel i j
k : ι
hjk : c.Rel j k
pos :
  Eq (α := biprod.{v_1, u_1} (K.X j) (K.X j) ⟶ homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j)
    (Iso.inv (K.biprodXIso K j) ≫
      Hom.f biprod.snd j ≫ Hom.f (biprod.lift (𝟙 K) (-𝟙 K)) j ≫ homotopyCofiber.inrX (biprod.lift (𝟙 K) (-𝟙 K)) j)
    (Iso.inv (K.biprodXIso K j) ≫
      HSub.hSub (α := (K ⊞ K).X j ⟶ homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j) (β :=
        (K ⊞ K).X j ⟶ homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j)
        (Hom.f (biprod.desc (𝟙 K) (𝟙 K)) j ≫ Hom.f (ι₀ K) j :
          (K ⊞ K).X j ⟶ homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j)
        (inrX K j : (K ⊞ K).X j ⟶ K.cylinder.X j))
⊢ Hom.f biprod.snd j ≫ Hom.f (biprod.lift (𝟙 K) (-𝟙 K)) j ≫ homotopyCofiber.inrX (biprod.lift (𝟙 K) (-𝟙 K)) j =
    HSub.hSub (α := (K ⊞ K).X j ⟶ homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j) (β :=
      (K ⊞ K).X j ⟶ homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j)
      (Hom.f (biprod.desc (𝟙 K) (𝟙 K)) j ≫ Hom.f (ι₀ K) j :
        (K ⊞ K).X j ⟶ homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j)
      (inrX K j : (K ⊞ K).X j ⟶ K.cylinder.X j)

Tactic:
rw [← cancel_epi (biprodXIso K K j).inv]

Premises used: HomologicalComplex.biprodXIso, CategoryTheory.cancel_epi, CategoryTheory.Iso.inv
-- Module: Mathlib.Algebra.Homology.HomotopyCofiber
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex.{v_1, u_1, u_2} C c
inst_2 : DecidableRel c.Rel
inst_3 : ∀ (i : ι), HasBinaryBiproduct.{v_1, u_1} (K.X i) (K.X i)
inst_4 : K.HasCylinder
hc : ∀ (j : ι), ∃ (i : ι), c.Rel i j
j : ι
this : biprod.lift (𝟙 K) (-𝟙 K) = HSub.hSub (α := K ⟶ K ⊞ K) biprod.inl biprod.inr
i : ι
hij : c.Rel i j
k : ι
hjk : c.Rel j k
pos :
  CategoryStruct.comp (Y := biprod.{v_1, u_1} (K.X j) (K.X j)) biprod.inl
      (Iso.inv (K.biprodXIso K j) ≫
        Hom.f biprod.snd j ≫ Hom.f (biprod.lift (𝟙 K) (-𝟙 K)) j ≫ homotopyCofiber.inrX (biprod.lift (𝟙 K) (-𝟙 K)) j) =
    CategoryStruct.comp (Y := biprod.{v_1, u_1} (K.X j) (K.X j)) biprod.inl
      (Iso.inv (K.biprodXIso K j) ≫
        HSub.hSub (α := (K ⊞ K).X j ⟶ homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j) (β :=
          (K ⊞ K).X j ⟶ homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j)
          (Hom.f (biprod.desc (𝟙 K) (𝟙 K)) j ≫ Hom.f (ι₀ K) j :
            (K ⊞ K).X j ⟶ homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j)
          (inrX K j : (K ⊞ K).X j ⟶ K.cylinder.X j))
pos₁ :
  CategoryStruct.comp (Y := biprod.{v_1, u_1} (K.X j) (K.X j)) biprod.inr
      (Iso.inv (K.biprodXIso K j) ≫
        Hom.f biprod.snd j ≫ Hom.f (biprod.lift (𝟙 K) (-𝟙 K)) j ≫ homotopyCofiber.inrX (biprod.lift (𝟙 K) (-𝟙 K)) j) =
    CategoryStruct.comp (Y := biprod.{v_1, u_1} (K.X j) (K.X j)) biprod.inr
      (Iso.inv (K.biprodXIso K j) ≫
        HSub.hSub (α := (K ⊞ K).X j ⟶ homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j) (β :=
          (K ⊞ K).X j ⟶ homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j)
          (Hom.f (biprod.desc (𝟙 K) (𝟙 K)) j ≫ Hom.f (ι₀ K) j :
            (K ⊞ K).X j ⟶ homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j)
          (inrX K j : (K ⊞ K).X j ⟶ K.cylinder.X j))
⊢ Eq (α := biprod.{v_1, u_1} (K.X j) (K.X j) ⟶ homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j)
    (Iso.inv (K.biprodXIso K j) ≫
      Hom.f biprod.snd j ≫ Hom.f (biprod.lift (𝟙 K) (-𝟙 K)) j ≫ homotopyCofiber.inrX (biprod.lift (𝟙 K) (-𝟙 K)) j)
    (Iso.inv (K.biprodXIso K j) ≫
      HSub.hSub (α := (K ⊞ K).X j ⟶ homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j) (β :=
        (K ⊞ K).X j ⟶ homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j)
        (Hom.f (biprod.desc (𝟙 K) (𝟙 K)) j ≫ Hom.f (ι₀ K) j :
          (K ⊞ K).X j ⟶ homotopyCofiber.X (G := K ⊞ K) (biprod.lift (𝟙 K) (-𝟙 K)) j)
        (inrX K j : (K ⊞ K).X j ⟶ K.cylinder.X j))

Tactic:
ext