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 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))
hj : c.Rel (c.next j) (c.next (c.next j))
pos :
  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)) =
    -fstX φ j (c.next j) hjk ≫
          CategoryStruct.comp (Y := F.X (c.next (c.next j))) (F.d (c.next j) (c.next (c.next j)))
            (hα.hom (c.next (c.next j)) (c.next j)) +
      (HAdd.hAdd (α := X φ j ⟶ K.X (c.next j))
          (fstX φ j (c.next j) hjk ≫
            CategoryStruct.comp (Y := F.X (c.next (c.next j))) (F.d (c.next j) (c.next (c.next j)))
              (hα.hom (c.next (c.next j)) (c.next j)))
          (fstX φ j (c.next j) hjk ≫ hα.hom (c.next j) j ≫ K.d j (c.next j)) +
        sndX φ j ≫ G.d j (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)) =
    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))

Tactic:
simp only [comp_add, d_sndX_assoc _ _ _ hjk, add_comp, assoc, H,
        d_fstX_assoc _ _ _ _ hjk, neg_comp, dNext, AddMonoidHom.mk'_apply]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Preadditive.add_comp, dNext, CategoryTheory.Preadditive.comp_add, CategoryTheory.Preadditive.neg_comp, AddMonoidHom.mk'_apply, HomologicalComplex.homotopyCofiber.d_sndX_assoc, HomologicalComplex.homotopyCofiber.d_fstX_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
α : 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))
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)) =
    -fstX φ j (c.next j) hjk ≫
          CategoryStruct.comp (Y := F.X (c.next (c.next j))) (F.d (c.next j) (c.next (c.next j)))
            (hα.hom (c.next (c.next j)) (c.next j)) +
      (HAdd.hAdd (α := X φ j ⟶ K.X (c.next j))
          (fstX φ j (c.next j) hjk ≫
            CategoryStruct.comp (Y := F.X (c.next (c.next j))) (F.d (c.next j) (c.next (c.next j)))
              (hα.hom (c.next (c.next j)) (c.next j)))
          (fstX φ j (c.next j) hjk ≫ hα.hom (c.next j) j ≫ K.d j (c.next j)) +
        sndX φ j ≫ G.d j (c.next j) ≫ α.f (c.next j))

Tactic:
abel
-- 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))
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)

Tactic:
simp only [d_sndX_assoc _ _ _ hjk, add_comp, assoc, H, dNext_eq_zero _ _ hj, zero_add]

Premises used: CategoryTheory.Category.assoc, zero_add, CategoryTheory.Preadditive.add_comp, HomologicalComplex.homotopyCofiber.d_sndX_assoc, dNext_eq_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 k : ι
hjk : c.Rel j k
obtain :
  ∀ (hjk : c.Rel j (c.next j)),
    Hom.f (desc φ α hα) j =
      HAdd.hAdd (α := X φ j ⟶ K.X j) (fstX φ j (c.next j) hjk ≫ hα.hom (c.next j) j) (sndX φ j ≫ α.f j)
⊢ Hom.f (desc φ α hα) j = HAdd.hAdd (α := X φ j ⟶ K.X j) (fstX φ j k hjk ≫ hα.hom k j) (sndX φ j ≫ α.f j)

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)
⊢ Hom.f (desc φ α hα) j =
    HAdd.hAdd (α := X φ j ⟶ K.X j) (fstX φ j (c.next j) hjk ≫ hα.hom (c.next j) j) (sndX φ j ≫ α.f j)

Tactic:
apply 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 : ι
hj : ¬c.Rel j (c.next j)
⊢ Eq (α := (homotopyCofiber φ).X j ⟶ K.X j) (Hom.f (desc φ α hα) j) (sndX φ j ≫ α.f j)

Tactic:
apply dif_neg hj

Premises used: dif_neg
-- 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
i j : ι
hjk : c.Rel j i
obtain :
  ∀ (hjk : c.Rel j (c.next j)),
    CategoryStruct.comp (Y := X φ j) (inlX φ (c.next j) j hjk) (Hom.f (desc φ α hα) j) = hα.hom (c.next j) j
⊢ CategoryStruct.comp (Y := X φ j) (inlX φ i j hjk) (Hom.f (desc φ α hα) j) = hα.hom i j

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)
dsimp :
  CategoryStruct.comp (Y := X φ j) (inlX φ (c.next j) j hjk)
      (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) =
    hα.hom (c.next j) j
⊢ CategoryStruct.comp (Y := X φ j) (inlX φ (c.next j) j hjk) (Hom.f (desc φ α hα) j) = hα.hom (c.next j) j

Tactic:
dsimp [desc]

Premises used: HomologicalComplex.homotopyCofiber.desc
-- 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)
rw :
  inlX φ (c.next j) j hjk ≫
      HAdd.hAdd (α := X φ j ⟶ K.X j) (fstX φ j (c.next j) hjk ≫ hα.hom (c.next j) j) (sndX φ j ≫ α.f j) =
    hα.hom (c.next j) j
rw₁ :
  CategoryStruct.comp (Y := X φ j) (inlX φ (c.next j) j hjk) (fstX φ j (c.next j) hjk ≫ hα.hom (c.next j) j) +
      CategoryStruct.comp (Y := X φ j) (inlX φ (c.next j) j hjk) (sndX φ j ≫ α.f j) =
    hα.hom (c.next j) j
rw₂ :
  hα.hom (c.next j) j + CategoryStruct.comp (Y := X φ j) (inlX φ (c.next j) j hjk) (sndX φ j ≫ α.f j) =
    hα.hom (c.next j) j
rw₃ : HAdd.hAdd (α := F.X (c.next j) ⟶ K.X j) (hα.hom (c.next j) j) (0 ≫ α.f j) = hα.hom (c.next j) j
rw₄ : HAdd.hAdd (α := F.X (c.next j) ⟶ K.X j) (hα.hom (c.next j) j) 0 = hα.hom (c.next j) j
rw₅ rw₆ : Eq (α := F.X (c.next j) ⟶ K.X j) (hα.hom (c.next j) j) (hα.hom (c.next j) j)
⊢ CategoryStruct.comp (Y := X φ j) (inlX φ (c.next j) j hjk)
      (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) =
    hα.hom (c.next j) j

Tactic:
rw [dif_pos hjk, comp_add, inlX_fstX_assoc, inlX_sndX_assoc, zero_comp, add_zero]

Premises used: HomologicalComplex.homotopyCofiber.inlX_sndX_assoc, dif_pos, HomologicalComplex.homotopyCofiber.inlX_fstX_assoc, CategoryTheory.Preadditive.comp_add, CategoryTheory.Limits.zero_comp, 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
i : ι
dsimp :
  CategoryStruct.comp (Y := X φ i) (inrX φ i)
      (if hj : c.Rel i (c.next i) then
        HAdd.hAdd (α := X φ i ⟶ K.X i) (fstX φ i (c.next i) hj ≫ hα.hom (c.next i) i) (sndX φ i ≫ α.f i)
      else sndX φ i ≫ α.f i) =
    α.f i
⊢ CategoryStruct.comp (Y := X φ i) (inrX φ i) (Hom.f (desc φ α hα) i) = α.f i

Tactic:
dsimp [desc]

Premises used: HomologicalComplex.homotopyCofiber.desc
-- 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
i : ι
pos :
  ∀ (h : c.Rel i (c.next i)),
    inrX φ i ≫ HAdd.hAdd (α := X φ i ⟶ K.X i) (fstX φ i (c.next i) h ≫ hα.hom (c.next i) i) (sndX φ i ≫ α.f i) = α.f i
neg : ¬c.Rel i (c.next i) → CategoryStruct.comp (Y := X φ i) (inrX φ i) (sndX φ i ≫ α.f i) = α.f i
⊢ CategoryStruct.comp (Y := X φ i) (inrX φ i)
      (if hj : c.Rel i (c.next i) then
        HAdd.hAdd (α := X φ i ⟶ K.X i) (fstX φ i (c.next i) hj ≫ hα.hom (c.next i) i) (sndX φ i ≫ α.f i)
      else sndX φ i ≫ α.f i) =
    α.f i

Tactic:
split_ifs
-- 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
i : ι
h : c.Rel i (c.next i)
⊢ inrX φ i ≫ HAdd.hAdd (α := X φ i ⟶ K.X i) (fstX φ i (c.next i) h ≫ hα.hom (c.next i) i) (sndX φ i ≫ α.f i) = α.f i

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
α : G ⟶ K
hα : Homotopy (φ ≫ α) 0
i : ι
h : ¬c.Rel i (c.next i)
⊢ CategoryStruct.comp (Y := X φ i) (inrX φ i) (sndX φ i ≫ α.f i) = α.f i

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
α : G ⟶ K
hα : Homotopy (φ ≫ α) 0
hc : ∀ (j : ι), ∃ (i : ι), c.Rel i j
i j : ι
pos :
  ∀ (hij : c.Rel j i),
    CategoryStruct.comp (Y := (homotopyCofiber φ).X j) (Homotopy.hom (inrCompHomotopy φ hc) i j)
        (Hom.f (desc φ α hα) j) =
      hα.hom i j
neg :
  ∀ (hij : ¬c.Rel j i),
    CategoryStruct.comp (Y := (homotopyCofiber φ).X j) (Homotopy.hom (inrCompHomotopy φ hc) i j)
        (Hom.f (desc φ α hα) j) =
      hα.hom i j
⊢ CategoryStruct.comp (Y := (homotopyCofiber φ).X j) (Homotopy.hom (inrCompHomotopy φ hc) i j) (Hom.f (desc φ α hα) j) =
    hα.hom i j

Tactic:
by_cases hij : c.Rel j i

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 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
hc : ∀ (j : ι), ∃ (i : ι), c.Rel i j
i j : ι
hij : c.Rel j i
pos :
  CategoryStruct.comp (Y := X φ j) (Homotopy.hom (inrCompHomotopy φ hc) i j : F.X i ⟶ (homotopyCofiber φ).X j)
      (Hom.f (desc φ α hα) j) =
    hα.hom i j
⊢ CategoryStruct.comp (Y := (homotopyCofiber φ).X j) (Homotopy.hom (inrCompHomotopy φ hc) i j) (Hom.f (desc φ α hα) j) =
    hα.hom i j

Tactic:
dsimp
-- 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
hc : ∀ (j : ι), ∃ (i : ι), c.Rel i j
i j : ι
hij : c.Rel j i
⊢ CategoryStruct.comp (Y := X φ j) (Homotopy.hom (inrCompHomotopy φ hc) i j : F.X i ⟶ (homotopyCofiber φ).X j)
      (Hom.f (desc φ α hα) j) =
    hα.hom i j

Tactic:
simp only [inrCompHomotopy_hom φ hc i j hij, desc_f φ α hα _ _ hij,
      comp_add, inlX_fstX_assoc, inlX_sndX_assoc, zero_comp, add_zero]

Premises used: HomologicalComplex.homotopyCofiber.inrCompHomotopy_hom, HomologicalComplex.homotopyCofiber.inlX_sndX_assoc, HomologicalComplex.homotopyCofiber.inlX_fstX_assoc, CategoryTheory.Preadditive.comp_add, HomologicalComplex.homotopyCofiber.desc_f, CategoryTheory.Limits.zero_comp, 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
hc : ∀ (j : ι), ∃ (i : ι), c.Rel i j
i j : ι
hij : ¬c.Rel j i
⊢ CategoryStruct.comp (Y := (homotopyCofiber φ).X j) (Homotopy.hom (inrCompHomotopy φ hc) i j) (Hom.f (desc φ α hα) j) =
    hα.hom i j

Tactic:
simp only [Homotopy.zero _ _ _ hij, zero_comp]

Premises used: Homotopy.zero, CategoryTheory.Limits.zero_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 ι
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
f : homotopyCofiber φ ⟶ K
hc : ∀ (j : ι), ∃ (i : ι), c.Rel i j
⊢ φ ≫ inr φ ≫ f = (φ ≫ inr φ) ≫ f

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
α : G ⟶ K
hα : Homotopy (φ ≫ α) 0
f : homotopyCofiber φ ⟶ K
hc : ∀ (j : ι), ∃ (i : ι), c.Rel i j
⊢ Eq (α := F ⟶ K) (0 ≫ f) 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
f : homotopyCofiber φ ⟶ K
hc : ∀ (j : ι), ∃ (i : ι), c.Rel i j
h :
  ∀ (j : ι),
    f.f j =
      Hom.f
        (desc φ (inr φ ≫ f)
          ((Homotopy.ofEq ⋯).trans ((Homotopy.compRight (inrCompHomotopy φ hc) f).trans (Homotopy.ofEq ⋯))))
        j
⊢ f =
    desc φ (inr φ ≫ f) ((Homotopy.ofEq ⋯).trans ((Homotopy.compRight (inrCompHomotopy φ hc) f).trans (Homotopy.ofEq ⋯)))

Tactic:
ext 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
f : homotopyCofiber φ ⟶ K
hc : ∀ (j : ι), ∃ (i : ι), c.Rel i j
j : ι
pos :
  ∀ (hj : c.Rel j (c.next j)),
    f.f j =
      Hom.f
        (desc φ (inr φ ≫ f)
          ((Homotopy.ofEq ⋯).trans ((Homotopy.compRight (inrCompHomotopy φ hc) f).trans (Homotopy.ofEq ⋯))))
        j
neg :
  ∀ (hj : ¬c.Rel j (c.next j)),
    f.f j =
      Hom.f
        (desc φ (inr φ ≫ f)
          ((Homotopy.ofEq ⋯).trans ((Homotopy.compRight (inrCompHomotopy φ hc) f).trans (Homotopy.ofEq ⋯))))
        j
⊢ f.f j =
    Hom.f
      (desc φ (inr φ ≫ f)
        ((Homotopy.ofEq ⋯).trans ((Homotopy.compRight (inrCompHomotopy φ hc) f).trans (Homotopy.ofEq ⋯))))
      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
f : homotopyCofiber φ ⟶ K
hc : ∀ (j : ι), ∃ (i : ι), c.Rel i j
j : ι
hj : c.Rel j (c.next j)
pos :
  inlX φ (c.next j) j hj ≫ f.f j =
    CategoryStruct.comp (Y := X φ j) (inlX φ (c.next j) j hj)
      (Hom.f
        (desc φ (inr φ ≫ f)
          ((Homotopy.ofEq ⋯).trans ((Homotopy.compRight (inrCompHomotopy φ hc) f).trans (Homotopy.ofEq ⋯))))
        j)
pos₁ :
  inrX φ j ≫ f.f j =
    CategoryStruct.comp (Y := X φ j) (inrX φ j)
      (Hom.f
        (desc φ (inr φ ≫ f)
          ((Homotopy.ofEq ⋯).trans ((Homotopy.compRight (inrCompHomotopy φ hc) f).trans (Homotopy.ofEq ⋯))))
        j)
⊢ f.f j =
    Hom.f
      (desc φ (inr φ ≫ f)
        ((Homotopy.ofEq ⋯).trans ((Homotopy.compRight (inrCompHomotopy φ hc) f).trans (Homotopy.ofEq ⋯))))
      j

Tactic:
apply ext_from_X φ _ _ hj

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
f : homotopyCofiber φ ⟶ K
hc : ∀ (j : ι), ∃ (i : ι), c.Rel i j
j : ι
hj : c.Rel j (c.next j)
⊢ inlX φ (c.next j) j hj ≫ f.f j =
    CategoryStruct.comp (Y := X φ j) (inlX φ (c.next j) j hj)
      (Hom.f
        (desc φ (inr φ ≫ f)
          ((Homotopy.ofEq ⋯).trans ((Homotopy.compRight (inrCompHomotopy φ hc) f).trans (Homotopy.ofEq ⋯))))
        j)

Tactic:
simp [inrCompHomotopy_hom _ _ _ _ hj]

Premises used: HomologicalComplex.homotopyCofiber.inrCompHomotopy_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 K : HomologicalComplex.{v_1, u_1, u_2} C c
φ : F ⟶ G
inst_2 : HasHomotopyCofiber φ
inst_3 : DecidableRel c.Rel
f : homotopyCofiber φ ⟶ K
hc : ∀ (j : ι), ∃ (i : ι), c.Rel i j
j : ι
hj : c.Rel j (c.next j)
⊢ inrX φ j ≫ f.f j =
    CategoryStruct.comp (Y := X φ j) (inrX φ j)
      (Hom.f
        (desc φ (inr φ ≫ f)
          ((Homotopy.ofEq ⋯).trans ((Homotopy.compRight (inrCompHomotopy φ hc) f).trans (Homotopy.ofEq ⋯))))
        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 K : HomologicalComplex.{v_1, u_1, u_2} C c
φ : F ⟶ G
inst_2 : HasHomotopyCofiber φ
inst_3 : DecidableRel c.Rel
f : homotopyCofiber φ ⟶ K
hc : ∀ (j : ι), ∃ (i : ι), c.Rel i j
j : ι
hj : ¬c.Rel j (c.next j)
neg :
  inrX φ j ≫ f.f j =
    CategoryStruct.comp (Y := X φ j) (inrX φ j)
      (Hom.f
        (desc φ (inr φ ≫ f)
          ((Homotopy.ofEq ⋯).trans ((Homotopy.compRight (inrCompHomotopy φ hc) f).trans (Homotopy.ofEq ⋯))))
        j)
⊢ f.f j =
    Hom.f
      (desc φ (inr φ ≫ f)
        ((Homotopy.ofEq ⋯).trans ((Homotopy.compRight (inrCompHomotopy φ hc) f).trans (Homotopy.ofEq ⋯))))
      j

Tactic:
apply ext_from_X' φ _ hj

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
f : homotopyCofiber φ ⟶ K
hc : ∀ (j : ι), ∃ (i : ι), c.Rel i j
j : ι
hj : ¬c.Rel j (c.next j)
⊢ inrX φ j ≫ f.f j =
    CategoryStruct.comp (Y := X φ j) (inrX φ j)
      (Hom.f
        (desc φ (inr φ ≫ f)
          ((Homotopy.ofEq ⋯).trans ((Homotopy.compRight (inrCompHomotopy φ hc) f).trans (Homotopy.ofEq ⋯))))
        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
K : HomologicalComplex.{v_1, u_1, u_2} C c
x y : (α : G ⟶ K) × Homotopy (φ ≫ α) 0
mp :
  x = y →
    x.fst (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0) = y.fst (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0) ∧
      ∀ (i j : ι),
        c.Rel j i →
          x.snd (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0).hom i j =
            y.snd (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0).hom i j
mpr :
  (x.fst (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0) = y.fst (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0) ∧
      ∀ (i j : ι),
        c.Rel j i →
          x.snd (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0).hom i j =
            y.snd (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0).hom i j) →
    x = y
⊢ x = y ↔
    x.fst (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0) = y.fst (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0) ∧
      ∀ (i j : ι),
        c.Rel j i →
          x.snd (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0).hom i j =
            y.snd (β := fun (α : G ⟶ K) ↦ Homotopy (φ ≫ α) 0).hom i j

Tactic:
constructor