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
α : 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))
⊢ 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 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) 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)) =
    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)) sorry ≫ hα.hom (c.next (c.next j)) (c.next j))
        (sndX φ (c.next j) ≫ α.f (c.next j))
Tactic: split_ifs with hj
-- 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)
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))
⊢ 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 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) 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)) =
    d φ j (c.next j) ≫ sndX φ (c.next j) ≫ α.f (c.next j)
Tactic: split_ifs with hj
-- 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)
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) ≫
      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))
have pos : 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)) =
  -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: simp only [comp_add, d_sndX_assoc _ _ _ hjk, add_comp, assoc, H,
        d_fstX_assoc _ _ _ _ hjk, neg_comp, dNext, AddMonoidHom.mk'_apply]
-- 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
⊢ Hom.f (desc φ α hα) j = HAdd.hAdd (α := X φ j ⟶ K.X j) (fstX φ j k hjk ≫ hα.hom k j) (sndX φ j ≫ α.f j)
have 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)
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
i j : ι
hjk : c.Rel j i
⊢ CategoryStruct.comp (Y := X φ j) (inlX φ i j hjk) (Hom.f (desc φ α hα) j) = hα.hom i j
have 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
Tactic: obtain rfl := c.next_eq' hjk
Cleared hypotheses: i, 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)
⊢ CategoryStruct.comp (Y := X φ j) (inlX φ (c.next j) j hjk) (Hom.f (desc φ α hα) j) = hα.hom (c.next j) j
have 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
Tactic: dsimp [desc]
-- 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)
⊢ 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
have 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
Tactic: rw [dif_pos hjk, comp_add, inlX_fstX_assoc, inlX_sndX_assoc, zero_comp, add_zero]
-- 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)
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
⊢ 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
have 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
Tactic: rw [dif_pos hjk, comp_add, inlX_fstX_assoc, inlX_sndX_assoc, zero_comp, add_zero]
-- 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)
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
⊢ 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
have 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
Tactic: rw [dif_pos hjk, comp_add, inlX_fstX_assoc, inlX_sndX_assoc, zero_comp, add_zero]
-- 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)
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
⊢ 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
have 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
Tactic: rw [dif_pos hjk, comp_add, inlX_fstX_assoc, inlX_sndX_assoc, zero_comp, add_zero]
-- 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)
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
⊢ 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
have rw₄ : HAdd.hAdd (α := F.X (c.next j) ⟶ K.X j) (hα.hom (c.next j) j) 0 = hα.hom (c.next j) j
Tactic: rw [dif_pos hjk, comp_add, inlX_fstX_assoc, inlX_sndX_assoc, zero_comp, add_zero]
-- 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)
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
⊢ 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
have rw₅ : Eq (α := F.X (c.next j) ⟶ K.X j) (hα.hom (c.next j) j) (hα.hom (c.next j) j)
Tactic: rw [dif_pos hjk, comp_add, inlX_fstX_assoc, inlX_sndX_assoc, zero_comp, add_zero]
-- 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
i : ι
⊢ CategoryStruct.comp (Y := X φ i) (inrX φ i) (Hom.f (desc φ α hα) i) = α.f i
have 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
Tactic: dsimp [desc]
-- 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
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
have 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
Tactic: split_ifs
-- 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
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
⊢ 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
have neg : ¬c.Rel i (c.next i) → CategoryStruct.comp (Y := X φ i) (inrX φ i) (sndX φ i ≫ α.f i) = α.f i
Tactic: split_ifs
-- 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
hc : ∀ (j : ι), ∃ (i : ι), c.Rel i j
i j : ι
⊢ CategoryStruct.comp (Y := (homotopyCofiber φ).X j) (Homotopy.hom (inrCompHomotopy φ hc) i j) (Hom.f (desc φ α hα) j) =
    hα.hom i j
have 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
Tactic: by_cases hij : c.Rel j i
-- 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
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
⊢ CategoryStruct.comp (Y := (homotopyCofiber φ).X j) (Homotopy.hom (inrCompHomotopy φ hc) i j) (Hom.f (desc φ α hα) j) =
    hα.hom i j
have 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
Tactic: by_cases hij : c.Rel j i
-- 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
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
have 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
Tactic: dsimp
-- 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
f : homotopyCofiber φ ⟶ K
hc : ∀ (j : ι), ∃ (i : ι), c.Rel i j
⊢ f =
    desc φ (inr φ ≫ f) ((Homotopy.ofEq ⋯).trans ((Homotopy.compRight (inrCompHomotopy φ hc) f).trans (Homotopy.ofEq ⋯)))
have h : ∀ (j : ι),
  f.f j =
    Hom.f
      (desc φ (inr φ ≫ f)
        ((Homotopy.ofEq sorry).trans ((Homotopy.compRight (inrCompHomotopy φ hc) f).trans (Homotopy.ofEq sorry))))
      j
Tactic: ext 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
f : homotopyCofiber φ ⟶ K
hc : ∀ (j : ι), ∃ (i : ι), c.Rel i j
j : ι
⊢ f.f j =
    Hom.f
      (desc φ (inr φ ≫ f)
        ((Homotopy.ofEq ⋯).trans ((Homotopy.compRight (inrCompHomotopy φ hc) f).trans (Homotopy.ofEq ⋯))))
      j
have pos : ∀ (hj : c.Rel j (c.next j)),
  f.f j =
    Hom.f
      (desc φ (inr φ ≫ f)
        ((Homotopy.ofEq sorry).trans ((Homotopy.compRight (inrCompHomotopy φ hc) f).trans (Homotopy.ofEq sorry))))
      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
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
⊢ f.f j =
    Hom.f
      (desc φ (inr φ ≫ f)
        ((Homotopy.ofEq ⋯).trans ((Homotopy.compRight (inrCompHomotopy φ hc) f).trans (Homotopy.ofEq ⋯))))
      j
have neg : ∀ (hj : ¬c.Rel j (c.next j)),
  f.f j =
    Hom.f
      (desc φ (inr φ ≫ f)
        ((Homotopy.ofEq sorry).trans ((Homotopy.compRight (inrCompHomotopy φ hc) f).trans (Homotopy.ofEq sorry))))
      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
f : homotopyCofiber φ ⟶ K
hc : ∀ (j : ι), ∃ (i : ι), c.Rel i j
j : ι
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
have 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 sorry).trans ((Homotopy.compRight (inrCompHomotopy φ hc) f).trans (Homotopy.ofEq sorry))))
      j)
Tactic: apply ext_from_X φ _ _ hj
-- 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
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)
⊢ f.f j =
    Hom.f
      (desc φ (inr φ ≫ f)
        ((Homotopy.ofEq ⋯).trans ((Homotopy.compRight (inrCompHomotopy φ hc) f).trans (Homotopy.ofEq ⋯))))
      j
have pos₁ : inrX φ j ≫ f.f j =
  CategoryStruct.comp (Y := X φ j) (inrX φ j)
    (Hom.f
      (desc φ (inr φ ≫ f)
        ((Homotopy.ofEq sorry).trans ((Homotopy.compRight (inrCompHomotopy φ hc) f).trans (Homotopy.ofEq sorry))))
      j)
Tactic: apply ext_from_X φ _ _ hj