awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCofiber (goal)
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 ι
F G K : HomologicalComplex.{v_1, u_1, u_2} C c
φ : F ⟶ G
inst_2 : HasHomotopyCofiber φ
inst_3 : DecidableRel c.Rel
i j k : ι
hij : c.Rel i j
hjk : c.Rel j k
⊢ Eq (α := F.X j ⟶ homotopyCofiber.X φ k)
    (homotopyCofiber.inlX φ j i hij ≫ homotopyCofiber.d φ i j ≫ homotopyCofiber.d φ j k)
    (CategoryStruct.comp (Y := homotopyCofiber.X φ i) (homotopyCofiber.inlX φ j i hij) 0)
have h₁ : HAdd.hAdd (α := F.X j ⟶ homotopyCofiber.X φ k) (-F.d j k ≫ homotopyCofiber.inlX φ k j hjk ≫ homotopyCofiber.d φ j k)
    (F.d j k ≫ φ.f k ≫ homotopyCofiber.inrX φ k) =
  0
Tactic: simp only [comp_zero, homotopyCofiber.inlX_d_assoc φ i j k hij hjk,
        add_comp, assoc, homotopyCofiber.inrX_d, Hom.comm_assoc, neg_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCofiber (goal)
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 ι
F G K : HomologicalComplex.{v_1, u_1, u_2} C c
φ : F ⟶ G
inst_2 : HasHomotopyCofiber φ
inst_3 : DecidableRel c.Rel
i j k : ι
hij : c.Rel i j
hjk : c.Rel j k
⊢ HAdd.hAdd (α := F.X j ⟶ homotopyCofiber.X φ k) (-F.d j k ≫ homotopyCofiber.inlX φ k j hjk ≫ homotopyCofiber.d φ j k)
      (F.d j k ≫ φ.f k ≫ homotopyCofiber.inrX φ k) =
    0
have pos : ∀ (hk : c.Rel k (c.next k)),
  HAdd.hAdd (α := F.X j ⟶ homotopyCofiber.X φ k) (-F.d j k ≫ homotopyCofiber.inlX φ k j hjk ≫ homotopyCofiber.d φ j k)
      (F.d j k ≫ φ.f k ≫ homotopyCofiber.inrX φ k) =
    0
Tactic: by_cases hk : c.Rel k (c.next k)
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCofiber (goal)
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 ι
F G K : HomologicalComplex.{v_1, u_1, u_2} C c
φ : F ⟶ G
inst_2 : HasHomotopyCofiber φ
inst_3 : DecidableRel c.Rel
i j k : ι
hij : c.Rel i j
hjk : c.Rel j k
pos :
  ∀ (hk : c.Rel k (c.next k)),
    HAdd.hAdd (α := F.X j ⟶ homotopyCofiber.X φ k) (-F.d j k ≫ homotopyCofiber.inlX φ k j hjk ≫ homotopyCofiber.d φ j k)
        (F.d j k ≫ φ.f k ≫ homotopyCofiber.inrX φ k) =
      0
⊢ HAdd.hAdd (α := F.X j ⟶ homotopyCofiber.X φ k) (-F.d j k ≫ homotopyCofiber.inlX φ k j hjk ≫ homotopyCofiber.d φ j k)
      (F.d j k ≫ φ.f k ≫ homotopyCofiber.inrX φ k) =
    0
have neg : ∀ (hk : ¬c.Rel k (c.next k)),
  HAdd.hAdd (α := F.X j ⟶ homotopyCofiber.X φ k) (-F.d j k ≫ homotopyCofiber.inlX φ k j hjk ≫ homotopyCofiber.d φ j k)
      (F.d j k ≫ φ.f k ≫ homotopyCofiber.inrX φ k) =
    0
Tactic: by_cases hk : c.Rel k (c.next k)
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCofiber (goal)
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 ι
F G K : HomologicalComplex.{v_1, u_1, u_2} C c
φ : F ⟶ G
inst_2 : HasHomotopyCofiber φ
inst_3 : DecidableRel c.Rel
hc : ∀ (j : ι), ∃ (i : ι), c.Rel i j
j : ι
⊢ Hom.f (φ ≫ inr φ) j =
    HAdd.hAdd (α := F.X j ⟶ (homotopyCofiber φ).X j)
        ((dNext j : (a : (i j : ι) → F.X i ⟶ (homotopyCofiber φ).X j) → F.X j ⟶ (homotopyCofiber φ).X j) fun (i j : ι) ↦
          if hij : c.Rel j i then inlX φ i j hij else 0)
        ((prevD j : (a : (i j : ι) → F.X i ⟶ (homotopyCofiber φ).X j) → F.X j ⟶ (homotopyCofiber φ).X j) fun (i j : ι) ↦
          if hij : c.Rel j i then inlX φ i j hij else 0) +
      Hom.f 0 j
have obtain : ∀ (i : ι) (hij : c.Rel i j),
  Hom.f (φ ≫ inr φ) j =
    HAdd.hAdd (α := F.X j ⟶ (homotopyCofiber φ).X j)
        ((dNext j : (a : (i j : ι) → F.X i ⟶ (homotopyCofiber φ).X j) → F.X j ⟶ (homotopyCofiber φ).X j) fun (i j : ι) ↦
          if hij : c.Rel j i then inlX φ i j hij else 0)
        ((prevD j : (a : (i j : ι) → F.X i ⟶ (homotopyCofiber φ).X j) → F.X j ⟶ (homotopyCofiber φ).X j) fun (i j : ι) ↦
          if hij : c.Rel j i then inlX φ i j hij else 0) +
      Hom.f 0 j
Tactic: obtain ⟨i, hij⟩ := hc j
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCofiber (goal)
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 ι
F G K : HomologicalComplex.{v_1, u_1, u_2} C c
φ : F ⟶ G
inst_2 : HasHomotopyCofiber φ
inst_3 : DecidableRel c.Rel
hc : ∀ (j : ι), ∃ (i : ι), c.Rel i j
j i : ι
hij : c.Rel i j
⊢ Hom.f (φ ≫ inr φ) j =
    HAdd.hAdd (α := F.X j ⟶ (homotopyCofiber φ).X j)
        ((dNext j : (a : (i j : ι) → F.X i ⟶ (homotopyCofiber φ).X j) → F.X j ⟶ (homotopyCofiber φ).X j) fun (i j : ι) ↦
          if hij : c.Rel j i then inlX φ i j hij else 0)
        ((prevD j : (a : (i j : ι) → F.X i ⟶ (homotopyCofiber φ).X j) → F.X j ⟶ (homotopyCofiber φ).X j) fun (i j : ι) ↦
          if hij : c.Rel j i then inlX φ i j hij else 0) +
      Hom.f 0 j
have rw : Hom.f (φ ≫ inr φ) j =
  ((dNext j : (a : (i j : ι) → F.X i ⟶ (homotopyCofiber φ).X j) → F.X j ⟶ (homotopyCofiber φ).X j) fun (i j : ι) ↦
        if hij : c.Rel j i then inlX φ i j hij else 0) +
      inlX φ j i hij ≫ (homotopyCofiber φ).d i j +
    Hom.f 0 j
Tactic: rw [prevD_eq _ hij, dif_pos hij]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCofiber (goal)
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 ι
F G K : HomologicalComplex.{v_1, u_1, u_2} C c
φ : F ⟶ G
inst_2 : HasHomotopyCofiber φ
inst_3 : DecidableRel c.Rel
hc : ∀ (j : ι), ∃ (i : ι), c.Rel i j
j i : ι
hij : c.Rel i j
⊢ Hom.f (φ ≫ inr φ) j =
    ((dNext j : (a : (i j : ι) → F.X i ⟶ (homotopyCofiber φ).X j) → F.X j ⟶ (homotopyCofiber φ).X j) fun (i j : ι) ↦
          if hij : c.Rel j i then inlX φ i j hij else 0) +
        inlX φ j i hij ≫ (homotopyCofiber φ).d i j +
      Hom.f 0 j
have pos : ∀ (hj : c.Rel j (c.next j)),
  Hom.f (φ ≫ inr φ) j =
    ((dNext j : (a : (i j : ι) → F.X i ⟶ (homotopyCofiber φ).X j) → F.X j ⟶ (homotopyCofiber φ).X j) fun (i j : ι) ↦
          if hij : c.Rel j i then inlX φ i j hij else 0) +
        inlX φ j i hij ≫ (homotopyCofiber φ).d i j +
      Hom.f 0 j
Tactic: by_cases hj : c.Rel j (c.next j)
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCofiber (goal)
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 ι
F G K : HomologicalComplex.{v_1, u_1, u_2} C c
φ : F ⟶ G
inst_2 : HasHomotopyCofiber φ
inst_3 : DecidableRel c.Rel
hc : ∀ (j : ι), ∃ (i : ι), c.Rel i j
j i : ι
hij : c.Rel i j
pos :
  ∀ (hj : c.Rel j (c.next j)),
    Hom.f (φ ≫ inr φ) j =
      ((dNext j : (a : (i j : ι) → F.X i ⟶ (homotopyCofiber φ).X j) → F.X j ⟶ (homotopyCofiber φ).X j) fun (i j : ι) ↦
            if hij : c.Rel j i then inlX φ i j hij else 0) +
          inlX φ j i hij ≫ (homotopyCofiber φ).d i j +
        Hom.f 0 j
⊢ Hom.f (φ ≫ inr φ) j =
    ((dNext j : (a : (i j : ι) → F.X i ⟶ (homotopyCofiber φ).X j) → F.X j ⟶ (homotopyCofiber φ).X j) fun (i j : ι) ↦
          if hij : c.Rel j i then inlX φ i j hij else 0) +
        inlX φ j i hij ≫ (homotopyCofiber φ).d i j +
      Hom.f 0 j
have neg : ∀ (hj : ¬c.Rel j (c.next j)),
  Hom.f (φ ≫ inr φ) j =
    ((dNext j : (a : (i j : ι) → F.X i ⟶ (homotopyCofiber φ).X j) → F.X j ⟶ (homotopyCofiber φ).X j) fun (i j : ι) ↦
          if hij : c.Rel j i then inlX φ i j hij else 0) +
        inlX φ j i hij ≫ (homotopyCofiber φ).d i j +
      Hom.f 0 j
Tactic: by_cases hj : c.Rel j (c.next j)
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCofiber (goal)
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 ι
F G K : HomologicalComplex.{v_1, u_1, u_2} C c
φ : F ⟶ G
inst_2 : HasHomotopyCofiber φ
inst_3 : DecidableRel c.Rel
hc : ∀ (j : ι), ∃ (i : ι), c.Rel i j
j i : ι
hij : c.Rel i j
hj : ¬c.Rel j (c.next j)
⊢ Hom.f (φ ≫ inr φ) j =
    ((dNext j : (a : (i j : ι) → F.X i ⟶ (homotopyCofiber φ).X j) → F.X j ⟶ (homotopyCofiber φ).X j) fun (i j : ι) ↦
          if hij : c.Rel j i then inlX φ i j hij else 0) +
        inlX φ j i hij ≫ (homotopyCofiber φ).d i j +
      Hom.f 0 j
have neg : Hom.f (φ ≫ inr φ) j = 0 + inlX φ j i hij ≫ (homotopyCofiber φ).d i j + Hom.f 0 j
Tactic: rw [dNext_eq_zero _ _ hj, zero_add, zero_f, add_zero, homotopyCofiber_d,
        inlX_d' _ _ _ _ hj, comp_f, inr_f]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCofiber (goal)
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 ι
F G K : HomologicalComplex.{v_1, u_1, u_2} C c
φ : F ⟶ G
inst_2 : HasHomotopyCofiber φ
inst_3 : DecidableRel c.Rel
hc : ∀ (j : ι), ∃ (i : ι), c.Rel i j
j i : ι
hij : c.Rel i j
hj : ¬c.Rel j (c.next j)
neg : Hom.f (φ ≫ inr φ) j = 0 + inlX φ j i hij ≫ (homotopyCofiber φ).d i j + Hom.f 0 j
⊢ Hom.f (φ ≫ inr φ) j =
    ((dNext j : (a : (i j : ι) → F.X i ⟶ (homotopyCofiber φ).X j) → F.X j ⟶ (homotopyCofiber φ).X j) fun (i j : ι) ↦
          if hij : c.Rel j i then inlX φ i j hij else 0) +
        inlX φ j i hij ≫ (homotopyCofiber φ).d i j +
      Hom.f 0 j
have neg₁ : Hom.f (φ ≫ inr φ) j = inlX φ j i hij ≫ (homotopyCofiber φ).d i j + Hom.f 0 j
Tactic: rw [dNext_eq_zero _ _ hj, zero_add, zero_f, add_zero, homotopyCofiber_d,
        inlX_d' _ _ _ _ hj, comp_f, inr_f]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCofiber (goal)
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 ι
F G K : HomologicalComplex.{v_1, u_1, u_2} C c
φ : F ⟶ G
inst_2 : HasHomotopyCofiber φ
inst_3 : DecidableRel c.Rel
hc : ∀ (j : ι), ∃ (i : ι), c.Rel i j
j i : ι
hij : c.Rel i j
hj : ¬c.Rel j (c.next j)
neg : Hom.f (φ ≫ inr φ) j = 0 + inlX φ j i hij ≫ (homotopyCofiber φ).d i j + Hom.f 0 j
neg₁ : Hom.f (φ ≫ inr φ) j = inlX φ j i hij ≫ (homotopyCofiber φ).d i j + Hom.f 0 j
⊢ Hom.f (φ ≫ inr φ) j =
    ((dNext j : (a : (i j : ι) → F.X i ⟶ (homotopyCofiber φ).X j) → F.X j ⟶ (homotopyCofiber φ).X j) fun (i j : ι) ↦
          if hij : c.Rel j i then inlX φ i j hij else 0) +
        inlX φ j i hij ≫ (homotopyCofiber φ).d i j +
      Hom.f 0 j
have neg₂ : Hom.f (φ ≫ inr φ) j = inlX φ j i hij ≫ (homotopyCofiber φ).d i j + 0
Tactic: rw [dNext_eq_zero _ _ hj, zero_add, zero_f, add_zero, homotopyCofiber_d,
        inlX_d' _ _ _ _ hj, comp_f, inr_f]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCofiber (goal)
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 ι
F G K : HomologicalComplex.{v_1, u_1, u_2} C c
φ : F ⟶ G
inst_2 : HasHomotopyCofiber φ
inst_3 : DecidableRel c.Rel
hc : ∀ (j : ι), ∃ (i : ι), c.Rel i j
j i : ι
hij : c.Rel i j
hj : ¬c.Rel j (c.next j)
neg : Hom.f (φ ≫ inr φ) j = 0 + inlX φ j i hij ≫ (homotopyCofiber φ).d i j + Hom.f 0 j
neg₁ : Hom.f (φ ≫ inr φ) j = inlX φ j i hij ≫ (homotopyCofiber φ).d i j + Hom.f 0 j
neg₂ : Hom.f (φ ≫ inr φ) j = inlX φ j i hij ≫ (homotopyCofiber φ).d i j + 0
⊢ Hom.f (φ ≫ inr φ) j =
    ((dNext j : (a : (i j : ι) → F.X i ⟶ (homotopyCofiber φ).X j) → F.X j ⟶ (homotopyCofiber φ).X j) fun (i j : ι) ↦
          if hij : c.Rel j i then inlX φ i j hij else 0) +
        inlX φ j i hij ≫ (homotopyCofiber φ).d i j +
      Hom.f 0 j
have neg₃ : Hom.f (φ ≫ inr φ) j = inlX φ j i hij ≫ (homotopyCofiber φ).d i j
Tactic: rw [dNext_eq_zero _ _ hj, zero_add, zero_f, add_zero, homotopyCofiber_d,
        inlX_d' _ _ _ _ hj, comp_f, inr_f]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCofiber (goal)
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 ι
F G K : HomologicalComplex.{v_1, u_1, u_2} C c
φ : F ⟶ G
inst_2 : HasHomotopyCofiber φ
inst_3 : DecidableRel c.Rel
hc : ∀ (j : ι), ∃ (i : ι), c.Rel i j
j i : ι
hij : c.Rel i j
hj : ¬c.Rel j (c.next j)
neg : Hom.f (φ ≫ inr φ) j = 0 + inlX φ j i hij ≫ (homotopyCofiber φ).d i j + Hom.f 0 j
neg₁ : Hom.f (φ ≫ inr φ) j = inlX φ j i hij ≫ (homotopyCofiber φ).d i j + Hom.f 0 j
neg₂ : Hom.f (φ ≫ inr φ) j = inlX φ j i hij ≫ (homotopyCofiber φ).d i j + 0
neg₃ : Hom.f (φ ≫ inr φ) j = inlX φ j i hij ≫ (homotopyCofiber φ).d i j
⊢ Hom.f (φ ≫ inr φ) j =
    ((dNext j : (a : (i j : ι) → F.X i ⟶ (homotopyCofiber φ).X j) → F.X j ⟶ (homotopyCofiber φ).X j) fun (i j : ι) ↦
          if hij : c.Rel j i then inlX φ i j hij else 0) +
        inlX φ j i hij ≫ (homotopyCofiber φ).d i j +
      Hom.f 0 j
have neg₄ : Eq (α := F.X j ⟶ (homotopyCofiber φ).X j) (Hom.f (φ ≫ inr φ) j)
  (CategoryStruct.comp (Y := (homotopyCofiber φ).X i) (inlX φ j i hij : F.X j ⟶ X φ i) (d φ i j))
Tactic: rw [dNext_eq_zero _ _ hj, zero_add, zero_f, add_zero, homotopyCofiber_d,
        inlX_d' _ _ _ _ hj, comp_f, inr_f]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCofiber (goal)
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 ι
F G K : HomologicalComplex.{v_1, u_1, u_2} C c
φ : F ⟶ G
inst_2 : HasHomotopyCofiber φ
inst_3 : DecidableRel c.Rel
hc : ∀ (j : ι), ∃ (i : ι), c.Rel i j
j i : ι
hij : c.Rel i j
hj : ¬c.Rel j (c.next j)
neg : Hom.f (φ ≫ inr φ) j = 0 + inlX φ j i hij ≫ (homotopyCofiber φ).d i j + Hom.f 0 j
neg₁ : Hom.f (φ ≫ inr φ) j = inlX φ j i hij ≫ (homotopyCofiber φ).d i j + Hom.f 0 j
neg₂ : Hom.f (φ ≫ inr φ) j = inlX φ j i hij ≫ (homotopyCofiber φ).d i j + 0
neg₃ : Hom.f (φ ≫ inr φ) j = inlX φ j i hij ≫ (homotopyCofiber φ).d i j
neg₄ :
  Eq (α := F.X j ⟶ (homotopyCofiber φ).X j) (Hom.f (φ ≫ inr φ) j)
    (CategoryStruct.comp (Y := (homotopyCofiber φ).X i) (inlX φ j i hij : F.X j ⟶ X φ i) (d φ i j))
⊢ Hom.f (φ ≫ inr φ) j =
    ((dNext j : (a : (i j : ι) → F.X i ⟶ (homotopyCofiber φ).X j) → F.X j ⟶ (homotopyCofiber φ).X j) fun (i j : ι) ↦
          if hij : c.Rel j i then inlX φ i j hij else 0) +
        inlX φ j i hij ≫ (homotopyCofiber φ).d i j +
      Hom.f 0 j
have neg₅ : Eq (α := F.X j ⟶ (homotopyCofiber φ).X j) (Hom.f (φ ≫ inr φ) j) (φ.f j ≫ inrX φ j)
Tactic: rw [dNext_eq_zero _ _ hj, zero_add, zero_f, add_zero, homotopyCofiber_d,
        inlX_d' _ _ _ _ hj, comp_f, inr_f]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCofiber (goal)
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 ι
F G K : HomologicalComplex.{v_1, u_1, u_2} C c
φ : F ⟶ G
inst_2 : HasHomotopyCofiber φ
inst_3 : DecidableRel c.Rel
hc : ∀ (j : ι), ∃ (i : ι), c.Rel i j
j i : ι
hij : c.Rel i j
hj : ¬c.Rel j (c.next j)
neg : Hom.f (φ ≫ inr φ) j = 0 + inlX φ j i hij ≫ (homotopyCofiber φ).d i j + Hom.f 0 j
neg₁ : Hom.f (φ ≫ inr φ) j = inlX φ j i hij ≫ (homotopyCofiber φ).d i j + Hom.f 0 j
neg₂ : Hom.f (φ ≫ inr φ) j = inlX φ j i hij ≫ (homotopyCofiber φ).d i j + 0
neg₃ : Hom.f (φ ≫ inr φ) j = inlX φ j i hij ≫ (homotopyCofiber φ).d i j
neg₄ :
  Eq (α := F.X j ⟶ (homotopyCofiber φ).X j) (Hom.f (φ ≫ inr φ) j)
    (CategoryStruct.comp (Y := (homotopyCofiber φ).X i) (inlX φ j i hij : F.X j ⟶ X φ i) (d φ i j))
neg₅ : Eq (α := F.X j ⟶ (homotopyCofiber φ).X j) (Hom.f (φ ≫ inr φ) j) (φ.f j ≫ inrX φ j)
⊢ Hom.f (φ ≫ inr φ) j =
    ((dNext j : (a : (i j : ι) → F.X i ⟶ (homotopyCofiber φ).X j) → F.X j ⟶ (homotopyCofiber φ).X j) fun (i j : ι) ↦
          if hij : c.Rel j i then inlX φ i j hij else 0) +
        inlX φ j i hij ≫ (homotopyCofiber φ).d i j +
      Hom.f 0 j
have neg₆ : Eq (α := F.X j ⟶ (homotopyCofiber φ).X j) (φ.f j ≫ Hom.f (inr φ) j) (φ.f j ≫ inrX φ j)
Tactic: rw [dNext_eq_zero _ _ hj, zero_add, zero_f, add_zero, homotopyCofiber_d,
        inlX_d' _ _ _ _ hj, comp_f, inr_f]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCofiber (goal)
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 ι
F G K : HomologicalComplex.{v_1, u_1, u_2} C c
φ : F ⟶ G
inst_2 : HasHomotopyCofiber φ
inst_3 : DecidableRel c.Rel
hc : ∀ (j : ι), ∃ (i : ι), c.Rel i j
j i : ι
hij : c.Rel i j
hj : ¬c.Rel j (c.next j)
neg : Hom.f (φ ≫ inr φ) j = 0 + inlX φ j i hij ≫ (homotopyCofiber φ).d i j + Hom.f 0 j
neg₁ : Hom.f (φ ≫ inr φ) j = inlX φ j i hij ≫ (homotopyCofiber φ).d i j + Hom.f 0 j
neg₂ : Hom.f (φ ≫ inr φ) j = inlX φ j i hij ≫ (homotopyCofiber φ).d i j + 0
neg₃ : Hom.f (φ ≫ inr φ) j = inlX φ j i hij ≫ (homotopyCofiber φ).d i j
neg₄ :
  Eq (α := F.X j ⟶ (homotopyCofiber φ).X j) (Hom.f (φ ≫ inr φ) j)
    (CategoryStruct.comp (Y := (homotopyCofiber φ).X i) (inlX φ j i hij : F.X j ⟶ X φ i) (d φ i j))
neg₅ : Eq (α := F.X j ⟶ (homotopyCofiber φ).X j) (Hom.f (φ ≫ inr φ) j) (φ.f j ≫ inrX φ j)
neg₆ : Eq (α := F.X j ⟶ (homotopyCofiber φ).X j) (φ.f j ≫ Hom.f (inr φ) j) (φ.f j ≫ inrX φ j)
⊢ Hom.f (φ ≫ inr φ) j =
    ((dNext j : (a : (i j : ι) → F.X i ⟶ (homotopyCofiber φ).X j) → F.X j ⟶ (homotopyCofiber φ).X j) fun (i j : ι) ↦
          if hij : c.Rel j i then inlX φ i j hij else 0) +
        inlX φ j i hij ≫ (homotopyCofiber φ).d i j +
      Hom.f 0 j
have neg₇ : Eq (α := F.X j ⟶ (homotopyCofiber φ).X j) (φ.f j ≫ inrX φ j : F.X j ⟶ (homotopyCofiber φ).X j)
  (φ.f j ≫ inrX φ j : F.X j ⟶ X φ j)
Tactic: rw [dNext_eq_zero _ _ hj, zero_add, zero_f, add_zero, homotopyCofiber_d,
        inlX_d' _ _ _ _ hj, comp_f, inr_f]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCofiber (goal)
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 ι
F G K : HomologicalComplex.{v_1, u_1, u_2} C c
φ : F ⟶ G
inst_2 : HasHomotopyCofiber φ
inst_3 : DecidableRel c.Rel
α : G ⟶ K
hα : Homotopy (φ ≫ α) 0
j k : ι
hjk : c.Rel j k
⊢ (if hj : c.Rel j (c.next j) then
        HAdd.hAdd (α := X φ j ⟶ K.X j) (fstX φ j (c.next j) hj ≫ hα.hom (c.next j) j) (sndX φ j ≫ α.f j)
      else sndX φ j ≫ α.f j) ≫
      K.d j k =
    (homotopyCofiber φ).d j k ≫
      if hj : c.Rel k (c.next k) then
        HAdd.hAdd (α := X φ k ⟶ K.X k) (fstX φ k (c.next k) hj ≫ hα.hom (c.next k) k) (sndX φ k ≫ α.f k)
      else sndX φ k ≫ α.f k
have obtain : ∀ (hjk : c.Rel j (c.next j)),
  Eq (α := (homotopyCofiber φ).X j ⟶ K.X (c.next j))
    ((if hj : c.Rel j (c.next j) then
        HAdd.hAdd (α := X φ j ⟶ K.X j) (fstX φ j (c.next j) hj ≫ hα.hom (c.next j) j) (sndX φ j ≫ α.f j)
      else sndX φ j ≫ α.f j) ≫
      K.d j (c.next j))
    (CategoryStruct.comp (Y := (homotopyCofiber φ).X (c.next j)) ((homotopyCofiber φ).d j (c.next j))
      (if hj : c.Rel (c.next j) (c.next (c.next j)) then
        HAdd.hAdd (α := X φ (c.next j) ⟶ K.X (c.next j))
          (fstX φ (c.next j) (c.next (c.next j)) hj ≫ hα.hom (c.next (c.next j)) (c.next j))
          (sndX φ (c.next j) ≫ α.f (c.next j))
      else sndX φ (c.next j) ≫ α.f (c.next j)))
Tactic: obtain rfl := c.next_eq' hjk
Cleared hypotheses: k, hjk
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCofiber (goal)
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 ι
F G K : HomologicalComplex.{v_1, u_1, u_2} C c
φ : F ⟶ G
inst_2 : HasHomotopyCofiber φ
inst_3 : DecidableRel c.Rel
α : G ⟶ K
hα : Homotopy (φ ≫ α) 0
j : ι
hjk : c.Rel j (c.next j)
⊢ Eq (α := (homotopyCofiber φ).X j ⟶ K.X (c.next j))
    ((if hj : c.Rel j (c.next j) then
        HAdd.hAdd (α := X φ j ⟶ K.X j) (fstX φ j (c.next j) hj ≫ hα.hom (c.next j) j) (sndX φ j ≫ α.f j)
      else sndX φ j ≫ α.f j) ≫
      K.d j (c.next j))
    (CategoryStruct.comp (Y := (homotopyCofiber φ).X (c.next j)) ((homotopyCofiber φ).d j (c.next j))
      (if hj : c.Rel (c.next j) (c.next (c.next j)) then
        HAdd.hAdd (α := X φ (c.next j) ⟶ K.X (c.next j))
          (fstX φ (c.next j) (c.next (c.next j)) hj ≫ hα.hom (c.next (c.next j)) (c.next j))
          (sndX φ (c.next j) ≫ α.f (c.next j))
      else sndX φ (c.next j) ≫ α.f (c.next j)))
have simp : HAdd.hAdd (α := X φ j ⟶ K.X (c.next j)) (fstX φ j (c.next j) sorry ≫ hα.hom (c.next j) j ≫ K.d j (c.next j))
    (sndX φ j ≫ G.d j (c.next j) ≫ α.f (c.next j)) =
  CategoryStruct.comp (Y := X φ (c.next j)) (d φ j (c.next j))
    (if h : c.Rel (c.next j) (c.next (c.next j)) then
      HAdd.hAdd (α := X φ (c.next j) ⟶ K.X (c.next j))
        (fstX φ (c.next j) (c.next (c.next j)) sorry ≫ hα.hom (c.next (c.next j)) (c.next j))
        (sndX φ (c.next j) ≫ α.f (c.next j))
    else sndX φ (c.next j) ≫ α.f (c.next j))
Tactic: simp [dif_pos hjk]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCofiber (hypothesis)
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 ι
F G K : HomologicalComplex.{v_1, u_1, u_2} C c
φ : F ⟶ G
inst_2 : HasHomotopyCofiber φ
inst_3 : DecidableRel c.Rel
α : G ⟶ K
hα : Homotopy (φ ≫ α) 0
j : ι
hjk : c.Rel j (c.next j)
⊢ HAdd.hAdd (α := X φ j ⟶ K.X (c.next j)) (fstX φ j (c.next j) ⋯ ≫ hα.hom (c.next j) j ≫ K.d j (c.next j))
      (sndX φ j ≫ G.d j (c.next j) ≫ α.f (c.next j)) =
    CategoryStruct.comp (Y := X φ (c.next j)) (d φ j (c.next j))
      (if h : c.Rel (c.next j) (c.next (c.next j)) then
        HAdd.hAdd (α := X φ (c.next j) ⟶ K.X (c.next j))
          (fstX φ (c.next j) (c.next (c.next j)) ⋯ ≫ hα.hom (c.next (c.next j)) (c.next j))
          (sndX φ (c.next j) ≫ α.f (c.next j))
      else sndX φ (c.next j) ≫ α.f (c.next j))
have H : (φ ≫ α).f (c.next j) =
  HAdd.hAdd (α := F.X (c.next j) ⟶ K.X (c.next j)) (β := F.X (c.next j) ⟶ K.X (c.next j))
      ((dNext (c.next j) : (a : (i j : ι) → F.X i ⟶ K.X j) → F.X (c.next j) ⟶ K.X (c.next j)) hα.hom :
        F.X (c.next j) ⟶ K.X (c.next j))
      ((prevD (c.next j) : (a : (i j : ι) → F.X i ⟶ K.X j) → F.X (c.next j) ⟶ K.X (c.next j)) hα.hom :
        F.X (c.next j) ⟶ K.X (c.next j)) +
    Hom.f 0 (c.next j)
Tactic: have H := hα.comm (c.next j)
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCofiber (hypothesis)
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 ι
F G K : HomologicalComplex.{v_1, u_1, u_2} C c
φ : F ⟶ G
inst_2 : HasHomotopyCofiber φ
inst_3 : DecidableRel c.Rel
α : G ⟶ K
hα : Homotopy (φ ≫ α) 0
j : ι
hjk : c.Rel j (c.next j)
H :
  (φ ≫ α).f (c.next j) =
    HAdd.hAdd (α := F.X (c.next j) ⟶ K.X (c.next j)) (β := F.X (c.next j) ⟶ K.X (c.next j))
        ((dNext (c.next j) : (a : (i j : ι) → F.X i ⟶ K.X j) → F.X (c.next j) ⟶ K.X (c.next j)) hα.hom :
          F.X (c.next j) ⟶ K.X (c.next j))
        ((prevD (c.next j) : (a : (i j : ι) → F.X i ⟶ K.X j) → F.X (c.next j) ⟶ K.X (c.next j)) hα.hom :
          F.X (c.next j) ⟶ K.X (c.next j)) +
      Hom.f 0 (c.next j)
⊢ HAdd.hAdd (α := X φ j ⟶ K.X (c.next j)) (fstX φ j (c.next j) ⋯ ≫ hα.hom (c.next j) j ≫ K.d j (c.next j))
      (sndX φ j ≫ G.d j (c.next j) ≫ α.f (c.next j)) =
    CategoryStruct.comp (Y := X φ (c.next j)) (d φ j (c.next j))
      (if h : c.Rel (c.next j) (c.next (c.next j)) then
        HAdd.hAdd (α := X φ (c.next j) ⟶ K.X (c.next j))
          (fstX φ (c.next j) (c.next (c.next j)) ⋯ ≫ hα.hom (c.next (c.next j)) (c.next j))
          (sndX φ (c.next j) ≫ α.f (c.next j))
      else sndX φ (c.next j) ≫ α.f (c.next j))
have H₁ : φ.f (c.next j) ≫ α.f (c.next j) =
  HAdd.hAdd (α := F.X (c.next j) ⟶ K.X (c.next j)) (β := F.X (c.next j) ⟶ K.X (c.next j))
    ((dNext (c.next j) : (a : (i j : ι) → F.X i ⟶ K.X j) → F.X (c.next j) ⟶ K.X (c.next j)) hα.hom :
      F.X (c.next j) ⟶ K.X (c.next j))
    (hα.hom (c.next j) j ≫ K.d j (c.next j))
Tactic: simp only [comp_f, zero_f, add_zero, prevD_eq _ hjk] at H
Cleared hypotheses: H