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
j : ι
hij : c.Rel j (c.next j)
⊢ CategoryStruct.comp (Y := X φ j) (inlX φ (c.next j) j hij) (sndX φ j) = 0

Tactic:
simp [inlX, sndX, dif_pos hij]

Premises used: dif_pos, HomologicalComplex.homotopyCofiber.sndX, HomologicalComplex.homotopyCofiber.inlX
-- 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
obtain : ∀ (hij : c.Rel i (c.next i)), CategoryStruct.comp (Y := X φ i) (inrX φ i) (fstX φ i (c.next i) hij) = 0
⊢ CategoryStruct.comp (Y := X φ i) (inrX φ i) (fstX φ i j hij) = 0

Tactic:
obtain rfl := c.next_eq' hij

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

Tactic:
simp [inrX, fstX, dif_pos hij]

Premises used: dif_pos, HomologicalComplex.homotopyCofiber.inrX, HomologicalComplex.homotopyCofiber.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
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
⊢ HasBinaryBiproduct.{v_1, u_1} (F.X j) (G.X i)

Tactic:
haveI := HasHomotopyCofiber.hasBinaryBiproduct φ _ _ hij
-- 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
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.{v_1, u_1} (F.X j) (G.X i)
rw :
  Eq (α := A ⟶ biprod.{v_1, u_1} (F.X j) (G.X i)) (f ≫ Iso.hom (XIsoBiprod φ i j hij))
    (g ≫ Iso.hom (XIsoBiprod φ i j hij))
⊢ f = g

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

Premises used: CategoryTheory.cancel_mono, HomologicalComplex.homotopyCofiber.XIsoBiprod, CategoryTheory.Iso.hom
-- 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
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.{v_1, u_1} (F.X j) (G.X i)
h₀ :
  CategoryStruct.comp (Y := biprod.{v_1, u_1} (F.X j) (G.X i)) (f ≫ Iso.hom (XIsoBiprod φ i j hij)) biprod.fst =
    CategoryStruct.comp (Y := biprod.{v_1, u_1} (F.X j) (G.X i)) (g ≫ Iso.hom (XIsoBiprod φ i j hij)) biprod.fst
h₃ :
  CategoryStruct.comp (Y := biprod.{v_1, u_1} (F.X j) (G.X i)) (f ≫ Iso.hom (XIsoBiprod φ i j hij)) biprod.snd =
    CategoryStruct.comp (Y := biprod.{v_1, u_1} (F.X j) (G.X i)) (g ≫ Iso.hom (XIsoBiprod φ i j hij)) biprod.snd
⊢ Eq (α := A ⟶ biprod.{v_1, u_1} (F.X j) (G.X i)) (f ≫ Iso.hom (XIsoBiprod φ i j hij))
    (g ≫ Iso.hom (XIsoBiprod φ i j hij))

Tactic:
apply biprod.hom_ext

Premises used: CategoryTheory.Limits.biprod.hom_ext
-- 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
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.{v_1, u_1} (F.X j) (G.X i)
⊢ CategoryStruct.comp (Y := biprod.{v_1, u_1} (F.X j) (G.X i)) (f ≫ Iso.hom (XIsoBiprod φ i j hij)) biprod.fst =
    CategoryStruct.comp (Y := biprod.{v_1, u_1} (F.X j) (G.X i)) (g ≫ Iso.hom (XIsoBiprod φ i j hij)) biprod.fst

Tactic:
simpa using h₁
-- 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
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.{v_1, u_1} (F.X j) (G.X i)
h₃ :
  ∀ (hij : c.Rel i (c.next i)) (h₁ : f ≫ fstX φ i (c.next i) hij = g ≫ fstX φ i (c.next i) hij)
    (this : HasBinaryBiproduct.{v_1, u_1} (F.X (c.next i)) (G.X i)),
    CategoryStruct.comp (Y := biprod.{v_1, u_1} (F.X (c.next i)) (G.X i)) (f ≫ Iso.hom (XIsoBiprod φ i (c.next i) hij))
        biprod.snd =
      CategoryStruct.comp (Y := biprod.{v_1, u_1} (F.X (c.next i)) (G.X i))
        (g ≫ Iso.hom (XIsoBiprod φ i (c.next i) hij)) biprod.snd
⊢ CategoryStruct.comp (Y := biprod.{v_1, u_1} (F.X j) (G.X i)) (f ≫ Iso.hom (XIsoBiprod φ i j hij)) biprod.snd =
    CategoryStruct.comp (Y := biprod.{v_1, u_1} (F.X j) (G.X i)) (g ≫ Iso.hom (XIsoBiprod φ i j hij)) biprod.snd

Tactic:
obtain rfl := c.next_eq' hij

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 : HomologicalComplex.{v_1, u_1, u_2} C c
φ : F ⟶ G
inst_2 : HasHomotopyCofiber φ
inst_3 : 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.{v_1, u_1} (F.X (c.next i)) (G.X i)
⊢ CategoryStruct.comp (Y := biprod.{v_1, u_1} (F.X (c.next i)) (G.X i)) (f ≫ Iso.hom (XIsoBiprod φ i (c.next i) hij))
      biprod.snd =
    CategoryStruct.comp (Y := biprod.{v_1, u_1} (F.X (c.next i)) (G.X i)) (g ≫ Iso.hom (XIsoBiprod φ i (c.next i) hij))
      biprod.snd

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

Premises used: dif_pos, HomologicalComplex.homotopyCofiber.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 : ι
hi : ¬c.Rel i (c.next i)
A : C
f g : A ⟶ X φ i
h : f ≫ sndX φ i = g ≫ sndX φ i
rw : f ≫ Iso.hom (XIso φ i hi) = g ≫ Iso.hom (XIso φ i hi)
⊢ f = g

Tactic:
rw [← cancel_mono (XIso φ i hi).hom]

Premises used: CategoryTheory.cancel_mono, HomologicalComplex.homotopyCofiber.XIso, CategoryTheory.Iso.hom
-- 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 : ι
hi : ¬c.Rel i (c.next i)
A : C
f g : A ⟶ X φ i
h : f ≫ sndX φ i = g ≫ sndX φ i
⊢ f ≫ Iso.hom (XIso φ i hi) = g ≫ Iso.hom (XIso φ i hi)

Tactic:
simpa only [sndX, dif_neg hi] using h

Premises used: dif_neg, HomologicalComplex.homotopyCofiber.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 j i
A : C
f g : X φ j ⟶ A
h₁ : inlX φ i j hij ≫ f = inlX φ i j hij ≫ g
h₂ : inrX φ j ≫ f = inrX φ j ≫ g
⊢ HasBinaryBiproduct.{v_1, u_1} (F.X i) (G.X j)

Tactic:
haveI := HasHomotopyCofiber.hasBinaryBiproduct φ _ _ hij
-- 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 j i
A : C
f g : X φ j ⟶ A
h₁ : inlX φ i j hij ≫ f = inlX φ i j hij ≫ g
h₂ : inrX φ j ≫ f = inrX φ j ≫ g
this : HasBinaryBiproduct.{v_1, u_1} (F.X i) (G.X j)
rw :
  Eq (α := biprod.{v_1, u_1} (F.X i) (G.X j) ⟶ A) (Iso.inv (XIsoBiprod φ j i hij) ≫ f)
    (Iso.inv (XIsoBiprod φ j i hij) ≫ g)
⊢ f = g

Tactic:
rw [← cancel_epi (XIsoBiprod φ j i hij).inv]

Premises used: HomologicalComplex.homotopyCofiber.XIsoBiprod, 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 ι
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 j i
A : C
f g : X φ j ⟶ A
h₁ : inlX φ i j hij ≫ f = inlX φ i j hij ≫ g
h₂ : inrX φ j ≫ f = inrX φ j ≫ g
this : HasBinaryBiproduct.{v_1, u_1} (F.X i) (G.X j)
h₀ :
  CategoryStruct.comp (Y := biprod.{v_1, u_1} (F.X i) (G.X j)) biprod.inl (Iso.inv (XIsoBiprod φ j i hij) ≫ f) =
    CategoryStruct.comp (Y := biprod.{v_1, u_1} (F.X i) (G.X j)) biprod.inl (Iso.inv (XIsoBiprod φ j i hij) ≫ g)
h₃ :
  CategoryStruct.comp (Y := biprod.{v_1, u_1} (F.X i) (G.X j)) biprod.inr (Iso.inv (XIsoBiprod φ j i hij) ≫ f) =
    CategoryStruct.comp (Y := biprod.{v_1, u_1} (F.X i) (G.X j)) biprod.inr (Iso.inv (XIsoBiprod φ j i hij) ≫ g)
⊢ Eq (α := biprod.{v_1, u_1} (F.X i) (G.X j) ⟶ A) (Iso.inv (XIsoBiprod φ j i hij) ≫ f)
    (Iso.inv (XIsoBiprod φ j i hij) ≫ g)

Tactic:
apply biprod.hom_ext'

Premises used: CategoryTheory.Limits.biprod.hom_ext'
-- 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 j i
A : C
f g : X φ j ⟶ A
h₁ : inlX φ i j hij ≫ f = inlX φ i j hij ≫ g
h₂ : inrX φ j ≫ f = inrX φ j ≫ g
this : HasBinaryBiproduct.{v_1, u_1} (F.X i) (G.X j)
⊢ CategoryStruct.comp (Y := biprod.{v_1, u_1} (F.X i) (G.X j)) biprod.inl (Iso.inv (XIsoBiprod φ j i hij) ≫ f) =
    CategoryStruct.comp (Y := biprod.{v_1, u_1} (F.X i) (G.X j)) biprod.inl (Iso.inv (XIsoBiprod φ j i hij) ≫ g)

Tactic:
simpa [inlX] using h₁

Premises used: HomologicalComplex.homotopyCofiber.inlX
-- 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 j i
A : C
f g : X φ j ⟶ A
h₁ : inlX φ i j hij ≫ f = inlX φ i j hij ≫ g
h₂ : inrX φ j ≫ f = inrX φ j ≫ g
this : HasBinaryBiproduct.{v_1, u_1} (F.X i) (G.X j)
h₃ :
  ∀ (hij : c.Rel j (c.next j)) (h₁ : inlX φ (c.next j) j hij ≫ f = inlX φ (c.next j) j hij ≫ g)
    (this : HasBinaryBiproduct.{v_1, u_1} (F.X (c.next j)) (G.X j)),
    CategoryStruct.comp (Y := biprod.{v_1, u_1} (F.X (c.next j)) (G.X j)) biprod.inr
        (Iso.inv (XIsoBiprod φ j (c.next j) hij) ≫ f) =
      CategoryStruct.comp (Y := biprod.{v_1, u_1} (F.X (c.next j)) (G.X j)) biprod.inr
        (Iso.inv (XIsoBiprod φ j (c.next j) hij) ≫ g)
⊢ CategoryStruct.comp (Y := biprod.{v_1, u_1} (F.X i) (G.X j)) biprod.inr (Iso.inv (XIsoBiprod φ j i hij) ≫ f) =
    CategoryStruct.comp (Y := biprod.{v_1, u_1} (F.X i) (G.X j)) biprod.inr (Iso.inv (XIsoBiprod φ j i hij) ≫ g)

Tactic:
obtain rfl := c.next_eq' hij

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 : HomologicalComplex.{v_1, u_1, u_2} C c
φ : F ⟶ G
inst_2 : HasHomotopyCofiber φ
inst_3 : DecidableRel c.Rel
j : ι
A : C
f g : X φ j ⟶ A
h₂ : inrX φ j ≫ f = inrX φ j ≫ g
hij : c.Rel j (c.next j)
h₁ : inlX φ (c.next j) j hij ≫ f = inlX φ (c.next j) j hij ≫ g
this : HasBinaryBiproduct.{v_1, u_1} (F.X (c.next j)) (G.X j)
⊢ CategoryStruct.comp (Y := biprod.{v_1, u_1} (F.X (c.next j)) (G.X j)) biprod.inr
      (Iso.inv (XIsoBiprod φ j (c.next j) hij) ≫ f) =
    CategoryStruct.comp (Y := biprod.{v_1, u_1} (F.X (c.next j)) (G.X j)) biprod.inr
      (Iso.inv (XIsoBiprod φ j (c.next j) hij) ≫ g)

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

Premises used: dif_pos, HomologicalComplex.homotopyCofiber.inrX
-- 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 : ι
hi : ¬c.Rel i (c.next i)
A : C
f g : X φ i ⟶ A
h : inrX φ i ≫ f = inrX φ i ≫ g
rw : Iso.inv (XIso φ i hi) ≫ f = Iso.inv (XIso φ i hi) ≫ g
⊢ f = g

Tactic:
rw [← cancel_epi (XIso φ i hi).inv]

Premises used: HomologicalComplex.homotopyCofiber.XIso, 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 ι
F G : HomologicalComplex.{v_1, u_1, u_2} C c
φ : F ⟶ G
inst_2 : HasHomotopyCofiber φ
inst_3 : DecidableRel c.Rel
i : ι
hi : ¬c.Rel i (c.next i)
A : C
f g : X φ i ⟶ A
h : inrX φ i ≫ f = inrX φ i ≫ g
⊢ Iso.inv (XIso φ i hi) ≫ f = Iso.inv (XIso φ i hi) ≫ g

Tactic:
simpa only [inrX, dif_neg hi] using h

Premises used: dif_neg, HomologicalComplex.homotopyCofiber.inrX
-- 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 k : ι
hij : c.Rel i j
hjk : c.Rel j k
obtain :
  ∀ (hjk : c.Rel j (c.next j)),
    Eq (α := X φ i ⟶ F.X (c.next j)) (d φ i j ≫ fstX φ j (c.next j) hjk) (-fstX φ i j hij ≫ F.d j (c.next j))
⊢ Eq (α := X φ i ⟶ F.X k) (d φ i j ≫ fstX φ j k hjk) (-fstX φ i j hij ≫ F.d j 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 : 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
hjk : c.Rel j (c.next j)
⊢ Eq (α := X φ i ⟶ F.X (c.next j)) (d φ i j ≫ fstX φ j (c.next j) hjk) (-fstX φ i j hij ≫ F.d j (c.next j))

Tactic:
simp [d, dif_pos hij, dif_pos hjk]

Premises used: dif_pos, HomologicalComplex.homotopyCofiber.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 : 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
dsimp :
  CategoryStruct.comp (Y := X φ j)
      (if hij : c.Rel i j then
        HAdd.hAdd (α := X φ i ⟶ X φ j)
            (if hj : c.Rel j (c.next j) then -fstX φ i j hij ≫ F.d j (c.next j) ≫ inlX φ (c.next j) j hj else 0)
            (fstX φ i j hij ≫ φ.f j ≫ inrX φ j) +
          sndX φ i ≫ G.d i j ≫ inrX φ j
      else 0)
      (sndX φ j) =
    HAdd.hAdd (α := X φ i ⟶ G.X j) (fstX φ i j hij ≫ φ.f j) (sndX φ i ≫ G.d i j)
⊢ d φ i j ≫ sndX φ j = HAdd.hAdd (α := X φ i ⟶ G.X j) (fstX φ i j hij ≫ φ.f j) (sndX φ i ≫ G.d i j)

Tactic:
dsimp [d]

Premises used: HomologicalComplex.homotopyCofiber.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 : 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
pos :
  ∀ (hij_1 : c.Rel j (c.next j)),
    (HAdd.hAdd (α := X φ i ⟶ X φ j) (-fstX φ i j hij ≫ F.d j (c.next j) ≫ inlX φ (c.next j) j hij_1)
            (fstX φ i j hij ≫ φ.f j ≫ inrX φ j) +
          sndX φ i ≫ G.d i j ≫ inrX φ j) ≫
        sndX φ j =
      HAdd.hAdd (α := X φ i ⟶ G.X j) (fstX φ i j hij ≫ φ.f j) (sndX φ i ≫ G.d i j)
neg :
  ∀ (hij_1 : ¬c.Rel j (c.next j)),
    (HAdd.hAdd (α := X φ i ⟶ X φ j) 0 (fstX φ i j hij ≫ φ.f j ≫ inrX φ j) + sndX φ i ≫ G.d i j ≫ inrX φ j) ≫ sndX φ j =
      HAdd.hAdd (α := X φ i ⟶ G.X j) (fstX φ i j hij ≫ φ.f j) (sndX φ i ≫ G.d i j)
⊢ CategoryStruct.comp (Y := X φ j)
      (if hij : c.Rel i j then
        HAdd.hAdd (α := X φ i ⟶ X φ j)
            (if hj : c.Rel j (c.next j) then -fstX φ i j hij ≫ F.d j (c.next j) ≫ inlX φ (c.next j) j hj else 0)
            (fstX φ i j hij ≫ φ.f j ≫ inrX φ j) +
          sndX φ i ≫ G.d i j ≫ inrX φ j
      else 0)
      (sndX φ j) =
    HAdd.hAdd (α := X φ i ⟶ G.X j) (fstX φ i j hij ≫ φ.f j) (sndX φ i ≫ G.d i j)

Tactic:
split_ifs with hij
-- 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_1 : c.Rel i j
hij : c.Rel j (c.next j)
⊢ (HAdd.hAdd (α := X φ i ⟶ X φ j) (-fstX φ i j hij_1 ≫ F.d j (c.next j) ≫ inlX φ (c.next j) j hij)
          (fstX φ i j hij_1 ≫ φ.f j ≫ inrX φ j) +
        sndX φ i ≫ G.d i j ≫ inrX φ j) ≫
      sndX φ j =
    HAdd.hAdd (α := X φ i ⟶ G.X j) (fstX φ i j hij_1 ≫ φ.f j) (sndX φ i ≫ G.d i j)

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 : HomologicalComplex.{v_1, u_1, u_2} C c
φ : F ⟶ G
inst_2 : HasHomotopyCofiber φ
inst_3 : DecidableRel c.Rel
i j : ι
hij_1 : c.Rel i j
hij : ¬c.Rel j (c.next j)
⊢ (HAdd.hAdd (α := X φ i ⟶ X φ j) 0 (fstX φ i j hij_1 ≫ φ.f j ≫ inrX φ j) + sndX φ i ≫ G.d i j ≫ inrX φ j) ≫ sndX φ j =
    HAdd.hAdd (α := X φ i ⟶ G.X j) (fstX φ i j hij_1 ≫ φ.f j) (sndX φ i ≫ G.d i j)

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 : 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₁ :
  CategoryStruct.comp (Y := X φ j) (inlX φ j i hij ≫ d φ i j) (fstX φ j k hjk) =
    HAdd.hAdd (α := F.X j ⟶ X φ j) (-F.d j k ≫ inlX φ k j hjk) (φ.f j ≫ inrX φ j) ≫ fstX φ j k hjk
h₂ :
  CategoryStruct.comp (Y := X φ j) (inlX φ j i hij ≫ d φ i j) (sndX φ j) =
    HAdd.hAdd (α := F.X j ⟶ X φ j) (-F.d j k ≫ inlX φ k j hjk) (φ.f j ≫ inrX φ j) ≫ sndX φ j
⊢ inlX φ j i hij ≫ d φ i j = HAdd.hAdd (α := F.X j ⟶ X φ j) (-F.d j k ≫ inlX φ k j hjk) (φ.f j ≫ inrX φ j)

Tactic:
apply ext_to_X φ j k hjk

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 k : ι
hij : c.Rel i j
hjk : c.Rel j k
⊢ CategoryStruct.comp (Y := X φ j) (inlX φ j i hij ≫ d φ i j) (fstX φ j k hjk) =
    HAdd.hAdd (α := F.X j ⟶ X φ j) (-F.d j k ≫ inlX φ k j hjk) (φ.f j ≫ inrX φ j) ≫ fstX φ j k hjk

Tactic:
simp [d_fstX φ _ _ _ hij hjk]

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 k : ι
hij : c.Rel i j
hjk : c.Rel j k
⊢ CategoryStruct.comp (Y := X φ j) (inlX φ j i hij ≫ d φ i j) (sndX φ j) =
    HAdd.hAdd (α := F.X j ⟶ X φ j) (-F.d j k ≫ inlX φ k j hjk) (φ.f 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)
apply :
  CategoryStruct.comp (Y := X φ j) (inlX φ j i hij ≫ d φ i j) (sndX φ j) =
    CategoryStruct.comp (Y := X φ j) (φ.f j ≫ inrX φ j) (sndX φ j)
⊢ Eq (α := F.X j ⟶ X φ j) (inlX φ j i hij ≫ d φ i j) (φ.f 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) (inlX φ j i hij ≫ d φ i j) (sndX φ j) =
    CategoryStruct.comp (Y := X φ j) (φ.f j ≫ inrX φ j) (sndX φ j)

Tactic:
simp [d_sndX φ i j 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
⊢ Eq (α := X φ i ⟶ X φ j) (d φ i j) 0

Tactic:
dif_neg hij

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

Tactic:
by_cases hij : c.Rel i j

Premises used: 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 : 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
pos : ∀ (hj : c.Rel j (c.next j)), Eq (α := G.X i ⟶ X φ j) (inrX φ i ≫ d φ i j) (G.d i j ≫ inrX φ j)
neg : ∀ (hj : ¬c.Rel j (c.next j)), Eq (α := G.X i ⟶ X φ j) (inrX φ i ≫ d φ i j) (G.d i j ≫ inrX φ j)
⊢ Eq (α := G.X i ⟶ X φ j) (inrX φ i ≫ d φ i j) (G.d i j ≫ inrX φ j)

Tactic:
by_cases hj : c.Rel j (c.next j)

Premises used: ComplexShape.next, ComplexShape.Rel