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 ι
F G : HomologicalComplex.{v_1, u_1, u_2} C c
φ : F ⟶ G
inst_2 : HasHomotopyCofiber φ
inst_3 : DecidableRel c.Rel
i j : ι
hij : c.Rel i j
hj : c.Rel j (c.next j)
pos :
  CategoryStruct.comp (Y := X φ j) (inrX φ i ≫ d φ i j) (fstX φ j (c.next j) hj) =
    CategoryStruct.comp (Y := X φ j) (G.d i j ≫ inrX φ j) (fstX φ j (c.next j) hj)
pos₁ :
  CategoryStruct.comp (Y := X φ j) (inrX φ i ≫ d φ i j) (sndX φ j) =
    CategoryStruct.comp (Y := X φ j) (G.d i j ≫ inrX φ j) (sndX φ j)
⊢ Eq (α := G.X i ⟶ X φ j) (inrX φ i ≫ d φ i j) (G.d i j ≫ inrX φ j)

Tactic:
apply ext_to_X _ _ _ hj

Premises used: HomologicalComplex.homotopyCofiber.ext_to_X
-- 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 ι
F G : HomologicalComplex.{v_1, u_1, u_2} C c
φ : F ⟶ G
inst_2 : HasHomotopyCofiber φ
inst_3 : DecidableRel c.Rel
i j : ι
hij : c.Rel i j
hj : c.Rel j (c.next j)
⊢ CategoryStruct.comp (Y := X φ j) (inrX φ i ≫ d φ i j) (fstX φ j (c.next j) hj) =
    CategoryStruct.comp (Y := X φ j) (G.d i j ≫ inrX φ j) (fstX φ j (c.next j) hj)

Tactic:
simp [d_fstX φ _ _ _ hij]

Premises used: HomologicalComplex.homotopyCofiber.d_fstX
-- 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 ι
F G : HomologicalComplex.{v_1, u_1, u_2} C c
φ : F ⟶ G
inst_2 : HasHomotopyCofiber φ
inst_3 : DecidableRel c.Rel
i j : ι
hij : c.Rel i j
hj : c.Rel j (c.next j)
⊢ CategoryStruct.comp (Y := X φ j) (inrX φ i ≫ d φ i j) (sndX φ j) =
    CategoryStruct.comp (Y := X φ j) (G.d i j ≫ inrX φ j) (sndX φ j)

Tactic:
simp [d_sndX φ _ _ hij]

Premises used: HomologicalComplex.homotopyCofiber.d_sndX
-- 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 ι
F G : HomologicalComplex.{v_1, u_1, u_2} C c
φ : F ⟶ G
inst_2 : HasHomotopyCofiber φ
inst_3 : DecidableRel c.Rel
i j : ι
hij : c.Rel i j
hj : ¬c.Rel j (c.next j)
neg :
  CategoryStruct.comp (Y := X φ j) (inrX φ i ≫ d φ i j) (sndX φ j) =
    CategoryStruct.comp (Y := X φ j) (G.d i j ≫ inrX φ j) (sndX φ j)
⊢ Eq (α := G.X i ⟶ X φ j) (inrX φ i ≫ d φ i j) (G.d i j ≫ inrX φ j)

Tactic:
apply ext_to_X' _ _ hj

Premises used: HomologicalComplex.homotopyCofiber.ext_to_X'
-- 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 ι
F G : HomologicalComplex.{v_1, u_1, u_2} C c
φ : F ⟶ G
inst_2 : HasHomotopyCofiber φ
inst_3 : DecidableRel c.Rel
i j : ι
hij : c.Rel i j
hj : ¬c.Rel j (c.next j)
⊢ CategoryStruct.comp (Y := X φ j) (inrX φ i ≫ d φ i j) (sndX φ j) =
    CategoryStruct.comp (Y := X φ j) (G.d i j ≫ inrX φ j) (sndX φ j)

Tactic:
simp [d_sndX φ _ _ hij]

Premises used: HomologicalComplex.homotopyCofiber.d_sndX
-- 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 ι
F G : HomologicalComplex.{v_1, u_1, u_2} C c
φ : F ⟶ G
inst_2 : HasHomotopyCofiber φ
inst_3 : DecidableRel c.Rel
i j : ι
hij : ¬c.Rel i j
neg : Eq (α := G.X i ⟶ X φ j) (CategoryStruct.comp (Y := X φ i) (inrX φ i) 0) (G.d i j ≫ inrX φ j)
neg₁ : Eq (α := G.X i ⟶ X φ j) (CategoryStruct.comp (Y := X φ i) (inrX φ i) 0) (0 ≫ inrX φ j)
neg₂ : Eq (α := G.X i ⟶ X φ j) (CategoryStruct.comp (Y := X φ i) (inrX φ i) 0) 0
neg₃ neg₄ : Eq.{v_1 + 1} (α := G.X i ⟶ X φ j) 0 0
⊢ Eq (α := G.X i ⟶ X φ j) (inrX φ i ≫ d φ i j) (G.d i j ≫ inrX φ j)

Tactic:
rw [shape φ _ _ hij, G.shape _ _ hij, zero_comp, comp_zero]

Premises used: CategoryTheory.Limits.comp_zero, HomologicalComplex.homotopyCofiber.shape, CategoryTheory.Limits.zero_comp, HomologicalComplex.shape
-- 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 ι
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
h₁ :
  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)
h₂ :
  Eq (α := G.X i ⟶ homotopyCofiber.X φ k) (homotopyCofiber.inrX φ i ≫ homotopyCofiber.d φ i j ≫ homotopyCofiber.d φ j k)
    (CategoryStruct.comp (Y := homotopyCofiber.X φ i) (homotopyCofiber.inrX φ i) 0)
⊢ Eq (α := homotopyCofiber.X φ i ⟶ homotopyCofiber.X φ k) (homotopyCofiber.d φ i j ≫ homotopyCofiber.d φ j k) 0

Tactic:
apply homotopyCofiber.ext_from_X φ j i hij

Premises used: HomologicalComplex.homotopyCofiber.ext_from_X
-- 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 ι
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
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
⊢ 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)

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]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.comp_zero, CategoryTheory.Preadditive.add_comp, HomologicalComplex.Hom.comm_assoc, CategoryTheory.Preadditive.neg_comp, HomologicalComplex.homotopyCofiber.inrX_d, HomologicalComplex.homotopyCofiber.inlX_d_assoc
-- 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 ι
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
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
⊢ 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)

Premises used: ComplexShape.next, ComplexShape.Rel
-- 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 ι
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
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:
simp [homotopyCofiber.inlX_d φ j k _ hjk hk]

Premises used: HomologicalComplex.homotopyCofiber.inlX_d
-- 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 ι
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
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:
simp [homotopyCofiber.inlX_d' φ j k hjk hk]

Premises used: HomologicalComplex.homotopyCofiber.inlX_d'
-- 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 ι
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 (α := G.X i ⟶ homotopyCofiber.X φ k) (homotopyCofiber.inrX φ i ≫ homotopyCofiber.d φ i j ≫ homotopyCofiber.d φ j k)
    (CategoryStruct.comp (Y := homotopyCofiber.X φ i) (homotopyCofiber.inrX φ i) 0)

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 ι
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 : ι
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
⊢ 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
-- 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 ι
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
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
⊢ 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:
rw [prevD_eq _ hij, dif_pos hij]

Premises used: dif_pos, prevD_eq
-- 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 ι
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
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
⊢ 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)

Premises used: ComplexShape.next, ComplexShape.Rel
-- 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 ι
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

Tactic:
simp only [comp_f, homotopyCofiber_d, zero_f, add_zero,
        inlX_d φ i j _ hij hj, dNext_eq _ hj, dif_pos hj,
        add_neg_cancel_left, inr_f]

Premises used: add_neg_cancel_left, dif_pos, HomologicalComplex.comp_f, HomologicalComplex.zero_f, HomologicalComplex.homotopyCofiber.inlX_d, dNext_eq, HomologicalComplex.homotopyCofiber_d, add_zero, HomologicalComplex.homotopyCofiber.inr_f
-- 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 ι
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)
neg₇ 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)
⊢ 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 [dNext_eq_zero _ _ hj, zero_add, zero_f, add_zero, homotopyCofiber_d,
        inlX_d' _ _ _ _ hj, comp_f, inr_f]

Premises used: HomologicalComplex.comp_f, zero_add, HomologicalComplex.zero_f, HomologicalComplex.homotopyCofiber.inlX_d', HomologicalComplex.homotopyCofiber_d, add_zero, dNext_eq_zero, HomologicalComplex.homotopyCofiber.inr_f
-- 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 ι
F G : 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
i j : ι
hij : c.Rel j i
⊢ Eq (α := F.X i ⟶ (homotopyCofiber φ).X j) (Homotopy.hom (inrCompHomotopy φ hc) i j) (inlX φ i j hij)

Tactic:
dif_pos hij

Premises used: dif_pos, dite
-- 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 ι
F G : 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
i j : ι
hij : ¬c.Rel j i
⊢ Eq (α := F.X i ⟶ (homotopyCofiber φ).X j) (Homotopy.hom (inrCompHomotopy φ hc) i j) 0

Tactic:
dif_neg hij

Premises used: dif_neg, dite
-- 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 ι
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
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)))
⊢ (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

Tactic:
obtain rfl := c.next_eq' hjk

Premises used: rfl, ComplexShape.next_eq'
-- 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 ι
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)
simp :
  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))
⊢ 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:
simp [dif_pos hjk]

Premises used: dif_pos
-- 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 ι
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)
⊢ (φ ≫ α).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)
-- 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 ι
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)
⊢ φ.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

Premises used: prevD_eq, HomologicalComplex.comp_f, HomologicalComplex.zero_f, add_zero
-- 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 ι
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) ≫ α.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))
pos :
  ∀ (hj : c.Rel (c.next j) (c.next (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)) =
      d φ j (c.next j) ≫
        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))
neg :
  ∀ (hj : ¬c.Rel (c.next j) (c.next (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)) =
      d φ j (c.next j) ≫ sndX φ (c.next j) ≫ α.f (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))

Tactic:
split_ifs with hj