awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplex (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
R : Type u_1
inst_2 : Ring R
inst_3 : Linear.{u_1, v, u} R C
F G K L : CochainComplex.{v, u, 0} C ℤ
n m : ℤ
φ₁ φ₂ : F ⟶ G
z : { z : Cochain F G (-1) // ofHom φ₁ = δ (-1) 0 z + ofHom φ₂ }
p : ℤ
eq : (ofHom φ₁).v p p ⋯ = (δ (-1) 0 (↑z : Cochain F G (-1)) + ofHom φ₂).v p p ⋯
h₁ : (ComplexShape.up ℤ).Rel (p - 1) p
⊢ φ₁.f p =
    HAdd.hAdd (α := F.X p ⟶ G.X p) (β := F.X p ⟶ G.X p)
        ((dNext p : (a : (i j : ℤ) → F.X i ⟶ G.X j) → F.X p ⟶ G.X p) fun (i j : ℤ) ↦
            if hij : i + -1 = j then (↑z : Cochain F G (-1)).v i j hij else 0 :
          F.X p ⟶ G.X p)
        ((prevD p : (a : (i j : ℤ) → F.X i ⟶ G.X j) → F.X p ⟶ G.X p) fun (i j : ℤ) ↦
            if hij : i + -1 = j then (↑z : Cochain F G (-1)).v i j hij else 0 :
          F.X p ⟶ G.X p) +
      φ₂.f p
have h₂ : (ComplexShape.up ℤ).Rel p (p + 1)
Tactic: have h₂ : (ComplexShape.up ℤ).Rel p (p + 1) := by simp
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplex (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
R : Type u_1
inst_2 : Ring R
inst_3 : Linear.{u_1, v, u} R C
F G K L : CochainComplex.{v, u, 0} C ℤ
n m : ℤ
φ₁ φ₂ : F ⟶ G
z : { z : Cochain F G (-1) // ofHom φ₁ = δ (-1) 0 z + ofHom φ₂ }
p : ℤ
eq : (ofHom φ₁).v p p ⋯ = (δ (-1) 0 (↑z : Cochain F G (-1)) + ofHom φ₂).v p p ⋯
h₁ : (ComplexShape.up ℤ).Rel (p - 1) p
h₂ : (ComplexShape.up ℤ).Rel p (p + 1)
⊢ φ₁.f p =
    HAdd.hAdd (α := F.X p ⟶ G.X p) (β := F.X p ⟶ G.X p)
        ((dNext p : (a : (i j : ℤ) → F.X i ⟶ G.X j) → F.X p ⟶ G.X p) fun (i j : ℤ) ↦
            if hij : i + -1 = j then (↑z : Cochain F G (-1)).v i j hij else 0 :
          F.X p ⟶ G.X p)
        ((prevD p : (a : (i j : ℤ) → F.X i ⟶ G.X j) → F.X p ⟶ G.X p) fun (i j : ℤ) ↦
            if hij : i + -1 = j then (↑z : Cochain F G (-1)).v i j hij else 0 :
          F.X p ⟶ G.X p) +
      φ₂.f p
have eq₁ : φ₁.f p =
  F.d p (p + 1) ≫ (↑z : Cochain F G (-1)).v (p + 1) p sorry + (↑z : Cochain F G (-1)).v p (p - 1) sorry ≫ G.d (p - 1) p + φ₂.f p
Tactic: simp only [δ_neg_one_cochain, Cochain.ofHom_v, ComplexShape.up_Rel, Cochain.add_v,
          Homotopy.nullHomotopicMap'_f h₁ h₂] at eq
Cleared hypotheses: eq
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplex (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
R : Type u_1
inst_2 : Ring R
inst_3 : Linear.{u_1, v, u} R C
F G K L : CochainComplex.{v, u, 0} C ℤ
n m : ℤ
φ₁ φ₂ : F ⟶ G
z : { z : Cochain F G (-1) // ofHom φ₁ = δ (-1) 0 z + ofHom φ₂ }
p : ℤ
h₁ : (ComplexShape.up ℤ).Rel (p - 1) p
h₂ : (ComplexShape.up ℤ).Rel p (p + 1)
eq :
  φ₁.f p =
    F.d p (p + 1) ≫ (↑z : Cochain F G (-1)).v (p + 1) p ⋯ + (↑z : Cochain F G (-1)).v p (p - 1) ⋯ ≫ G.d (p - 1) p +
      φ₂.f p
⊢ φ₁.f p =
    HAdd.hAdd (α := F.X p ⟶ G.X p) (β := F.X p ⟶ G.X p)
        ((dNext p : (a : (i j : ℤ) → F.X i ⟶ G.X j) → F.X p ⟶ G.X p) fun (i j : ℤ) ↦
            if hij : i + -1 = j then (↑z : Cochain F G (-1)).v i j hij else 0 :
          F.X p ⟶ G.X p)
        ((prevD p : (a : (i j : ℤ) → F.X i ⟶ G.X j) → F.X p ⟶ G.X p) fun (i j : ℤ) ↦
            if hij : i + -1 = j then (↑z : Cochain F G (-1)).v i j hij else 0 :
          F.X p ⟶ G.X p) +
      φ₂.f p
have rw : φ₁.f p =
  HAdd.hAdd (α := F.X p ⟶ G.X p) (β := F.X p ⟶ G.X p)
      (CategoryStruct.comp (Y := F.X (p + 1)) (F.d p (p + 1))
        (if hij : p + 1 + -1 = p then (↑z : Cochain F G (-1)).v (p + 1) p hij else 0))
      ((prevD p : (a : (i j : ℤ) → F.X i ⟶ G.X j) → F.X p ⟶ G.X p) fun (i j : ℤ) ↦
          if hij : i + -1 = j then (↑z : Cochain F G (-1)).v i j hij else 0 :
        F.X p ⟶ G.X p) +
    φ₂.f p
Tactic: rw [dNext_eq _ h₂, prevD_eq _ h₁, eq, dif_pos, dif_pos]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplex (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
R : Type u_1
inst_2 : Ring R
inst_3 : Linear.{u_1, v, u} R C
F G K L : CochainComplex.{v, u, 0} C ℤ
n m : ℤ
φ₁ φ₂ : F ⟶ G
z : { z : Cochain F G (-1) // ofHom φ₁ = δ (-1) 0 z + ofHom φ₂ }
p : ℤ
h₁ : (ComplexShape.up ℤ).Rel (p - 1) p
h₂ : (ComplexShape.up ℤ).Rel p (p + 1)
eq :
  φ₁.f p =
    F.d p (p + 1) ≫ (↑z : Cochain F G (-1)).v (p + 1) p ⋯ + (↑z : Cochain F G (-1)).v p (p - 1) ⋯ ≫ G.d (p - 1) p +
      φ₂.f p
rw :
  φ₁.f p =
    HAdd.hAdd (α := F.X p ⟶ G.X p) (β := F.X p ⟶ G.X p)
        (CategoryStruct.comp (Y := F.X (p + 1)) (F.d p (p + 1))
          (if hij : p + 1 + -1 = p then (↑z : Cochain F G (-1)).v (p + 1) p hij else 0))
        ((prevD p : (a : (i j : ℤ) → F.X i ⟶ G.X j) → F.X p ⟶ G.X p) fun (i j : ℤ) ↦
            if hij : i + -1 = j then (↑z : Cochain F G (-1)).v i j hij else 0 :
          F.X p ⟶ G.X p) +
      φ₂.f p
⊢ φ₁.f p =
    HAdd.hAdd (α := F.X p ⟶ G.X p) (β := F.X p ⟶ G.X p)
        ((dNext p : (a : (i j : ℤ) → F.X i ⟶ G.X j) → F.X p ⟶ G.X p) fun (i j : ℤ) ↦
            if hij : i + -1 = j then (↑z : Cochain F G (-1)).v i j hij else 0 :
          F.X p ⟶ G.X p)
        ((prevD p : (a : (i j : ℤ) → F.X i ⟶ G.X j) → F.X p ⟶ G.X p) fun (i j : ℤ) ↦
            if hij : i + -1 = j then (↑z : Cochain F G (-1)).v i j hij else 0 :
          F.X p ⟶ G.X p) +
      φ₂.f p
have rw₁ : φ₁.f p =
  CategoryStruct.comp (Y := F.X (p + 1)) (F.d p (p + 1))
        (if hij : p + 1 + -1 = p then (↑z : Cochain F G (-1)).v (p + 1) p hij else 0) +
      CategoryStruct.comp (Y := G.X (p - 1))
        (if hij : p + -1 = p - 1 then (↑z : Cochain F G (-1)).v p (p - 1) hij else 0) (G.d (p - 1) p) +
    φ₂.f p
Tactic: rw [dNext_eq _ h₂, prevD_eq _ h₁, eq, dif_pos, dif_pos]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplex (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
R : Type u_1
inst_2 : Ring R
inst_3 : Linear.{u_1, v, u} R C
F G K L : CochainComplex.{v, u, 0} C ℤ
n m : ℤ
φ₁ φ₂ : F ⟶ G
z : { z : Cochain F G (-1) // ofHom φ₁ = δ (-1) 0 z + ofHom φ₂ }
p : ℤ
h₁ : (ComplexShape.up ℤ).Rel (p - 1) p
h₂ : (ComplexShape.up ℤ).Rel p (p + 1)
eq :
  φ₁.f p =
    F.d p (p + 1) ≫ (↑z : Cochain F G (-1)).v (p + 1) p ⋯ + (↑z : Cochain F G (-1)).v p (p - 1) ⋯ ≫ G.d (p - 1) p +
      φ₂.f p
rw :
  φ₁.f p =
    HAdd.hAdd (α := F.X p ⟶ G.X p) (β := F.X p ⟶ G.X p)
        (CategoryStruct.comp (Y := F.X (p + 1)) (F.d p (p + 1))
          (if hij : p + 1 + -1 = p then (↑z : Cochain F G (-1)).v (p + 1) p hij else 0))
        ((prevD p : (a : (i j : ℤ) → F.X i ⟶ G.X j) → F.X p ⟶ G.X p) fun (i j : ℤ) ↦
            if hij : i + -1 = j then (↑z : Cochain F G (-1)).v i j hij else 0 :
          F.X p ⟶ G.X p) +
      φ₂.f p
rw₁ :
  φ₁.f p =
    CategoryStruct.comp (Y := F.X (p + 1)) (F.d p (p + 1))
          (if hij : p + 1 + -1 = p then (↑z : Cochain F G (-1)).v (p + 1) p hij else 0) +
        CategoryStruct.comp (Y := G.X (p - 1))
          (if hij : p + -1 = p - 1 then (↑z : Cochain F G (-1)).v p (p - 1) hij else 0) (G.d (p - 1) p) +
      φ₂.f p
⊢ φ₁.f p =
    HAdd.hAdd (α := F.X p ⟶ G.X p) (β := F.X p ⟶ G.X p)
        ((dNext p : (a : (i j : ℤ) → F.X i ⟶ G.X j) → F.X p ⟶ G.X p) fun (i j : ℤ) ↦
            if hij : i + -1 = j then (↑z : Cochain F G (-1)).v i j hij else 0 :
          F.X p ⟶ G.X p)
        ((prevD p : (a : (i j : ℤ) → F.X i ⟶ G.X j) → F.X p ⟶ G.X p) fun (i j : ℤ) ↦
            if hij : i + -1 = j then (↑z : Cochain F G (-1)).v i j hij else 0 :
          F.X p ⟶ G.X p) +
      φ₂.f p
have rw₂ : F.d p (p + 1) ≫ (↑z : Cochain F G (-1)).v (p + 1) p sorry + (↑z : Cochain F G (-1)).v p (p - 1) sorry ≫ G.d (p - 1) p + φ₂.f p =
  CategoryStruct.comp (Y := F.X (p + 1)) (F.d p (p + 1))
        (if hij : p + 1 + -1 = p then (↑z : Cochain F G (-1)).v (p + 1) p hij else 0) +
      CategoryStruct.comp (Y := G.X (p - 1))
        (if hij : p + -1 = p - 1 then (↑z : Cochain F G (-1)).v p (p - 1) hij else 0) (G.d (p - 1) p) +
    φ₂.f p
Tactic: rw [dNext_eq _ h₂, prevD_eq _ h₁, eq, dif_pos, dif_pos]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplex (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
R : Type u_1
inst_2 : Ring R
inst_3 : Linear.{u_1, v, u} R C
F G K L : CochainComplex.{v, u, 0} C ℤ
n m : ℤ
φ₁ φ₂ : F ⟶ G
z : { z : Cochain F G (-1) // ofHom φ₁ = δ (-1) 0 z + ofHom φ₂ }
p : ℤ
h₁ : (ComplexShape.up ℤ).Rel (p - 1) p
h₂ : (ComplexShape.up ℤ).Rel p (p + 1)
eq :
  φ₁.f p =
    F.d p (p + 1) ≫ (↑z : Cochain F G (-1)).v (p + 1) p ⋯ + (↑z : Cochain F G (-1)).v p (p - 1) ⋯ ≫ G.d (p - 1) p +
      φ₂.f p
rw :
  φ₁.f p =
    HAdd.hAdd (α := F.X p ⟶ G.X p) (β := F.X p ⟶ G.X p)
        (CategoryStruct.comp (Y := F.X (p + 1)) (F.d p (p + 1))
          (if hij : p + 1 + -1 = p then (↑z : Cochain F G (-1)).v (p + 1) p hij else 0))
        ((prevD p : (a : (i j : ℤ) → F.X i ⟶ G.X j) → F.X p ⟶ G.X p) fun (i j : ℤ) ↦
            if hij : i + -1 = j then (↑z : Cochain F G (-1)).v i j hij else 0 :
          F.X p ⟶ G.X p) +
      φ₂.f p
rw₁ :
  φ₁.f p =
    CategoryStruct.comp (Y := F.X (p + 1)) (F.d p (p + 1))
          (if hij : p + 1 + -1 = p then (↑z : Cochain F G (-1)).v (p + 1) p hij else 0) +
        CategoryStruct.comp (Y := G.X (p - 1))
          (if hij : p + -1 = p - 1 then (↑z : Cochain F G (-1)).v p (p - 1) hij else 0) (G.d (p - 1) p) +
      φ₂.f p
rw₂ :
  F.d p (p + 1) ≫ (↑z : Cochain F G (-1)).v (p + 1) p ⋯ + (↑z : Cochain F G (-1)).v p (p - 1) ⋯ ≫ G.d (p - 1) p +
      φ₂.f p =
    CategoryStruct.comp (Y := F.X (p + 1)) (F.d p (p + 1))
          (if hij : p + 1 + -1 = p then (↑z : Cochain F G (-1)).v (p + 1) p hij else 0) +
        CategoryStruct.comp (Y := G.X (p - 1))
          (if hij : p + -1 = p - 1 then (↑z : Cochain F G (-1)).v p (p - 1) hij else 0) (G.d (p - 1) p) +
      φ₂.f p
⊢ φ₁.f p =
    HAdd.hAdd (α := F.X p ⟶ G.X p) (β := F.X p ⟶ G.X p)
        ((dNext p : (a : (i j : ℤ) → F.X i ⟶ G.X j) → F.X p ⟶ G.X p) fun (i j : ℤ) ↦
            if hij : i + -1 = j then (↑z : Cochain F G (-1)).v i j hij else 0 :
          F.X p ⟶ G.X p)
        ((prevD p : (a : (i j : ℤ) → F.X i ⟶ G.X j) → F.X p ⟶ G.X p) fun (i j : ℤ) ↦
            if hij : i + -1 = j then (↑z : Cochain F G (-1)).v i j hij else 0 :
          F.X p ⟶ G.X p) +
      φ₂.f p
have rw₃ : F.d p (p + 1) ≫ (↑z : Cochain F G (-1)).v (p + 1) p sorry + (↑z : Cochain F G (-1)).v p (p - 1) sorry ≫ G.d (p - 1) p + φ₂.f p =
  F.d p (p + 1) ≫ (↑z : Cochain F G (-1)).v (p + 1) p sorry +
      CategoryStruct.comp (Y := G.X (p - 1))
        (if hij : p + -1 = p - 1 then (↑z : Cochain F G (-1)).v p (p - 1) hij else 0) (G.d (p - 1) p) +
    φ₂.f p
Tactic: rw [dNext_eq _ h₂, prevD_eq _ h₁, eq, dif_pos, dif_pos]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplex (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
R : Type u_1
inst_2 : Ring R
inst_3 : Linear.{u_1, v, u} R C
F G K L : CochainComplex.{v, u, 0} C ℤ
n m : ℤ
φ₁ φ₂ : F ⟶ G
z : { z : Cochain F G (-1) // ofHom φ₁ = δ (-1) 0 z + ofHom φ₂ }
p : ℤ
h₁ : (ComplexShape.up ℤ).Rel (p - 1) p
h₂ : (ComplexShape.up ℤ).Rel p (p + 1)
eq :
  φ₁.f p =
    F.d p (p + 1) ≫ (↑z : Cochain F G (-1)).v (p + 1) p ⋯ + (↑z : Cochain F G (-1)).v p (p - 1) ⋯ ≫ G.d (p - 1) p +
      φ₂.f p
rw :
  φ₁.f p =
    HAdd.hAdd (α := F.X p ⟶ G.X p) (β := F.X p ⟶ G.X p)
        (CategoryStruct.comp (Y := F.X (p + 1)) (F.d p (p + 1))
          (if hij : p + 1 + -1 = p then (↑z : Cochain F G (-1)).v (p + 1) p hij else 0))
        ((prevD p : (a : (i j : ℤ) → F.X i ⟶ G.X j) → F.X p ⟶ G.X p) fun (i j : ℤ) ↦
            if hij : i + -1 = j then (↑z : Cochain F G (-1)).v i j hij else 0 :
          F.X p ⟶ G.X p) +
      φ₂.f p
rw₁ :
  φ₁.f p =
    CategoryStruct.comp (Y := F.X (p + 1)) (F.d p (p + 1))
          (if hij : p + 1 + -1 = p then (↑z : Cochain F G (-1)).v (p + 1) p hij else 0) +
        CategoryStruct.comp (Y := G.X (p - 1))
          (if hij : p + -1 = p - 1 then (↑z : Cochain F G (-1)).v p (p - 1) hij else 0) (G.d (p - 1) p) +
      φ₂.f p
rw₂ :
  F.d p (p + 1) ≫ (↑z : Cochain F G (-1)).v (p + 1) p ⋯ + (↑z : Cochain F G (-1)).v p (p - 1) ⋯ ≫ G.d (p - 1) p +
      φ₂.f p =
    CategoryStruct.comp (Y := F.X (p + 1)) (F.d p (p + 1))
          (if hij : p + 1 + -1 = p then (↑z : Cochain F G (-1)).v (p + 1) p hij else 0) +
        CategoryStruct.comp (Y := G.X (p - 1))
          (if hij : p + -1 = p - 1 then (↑z : Cochain F G (-1)).v p (p - 1) hij else 0) (G.d (p - 1) p) +
      φ₂.f p
rw₃ :
  F.d p (p + 1) ≫ (↑z : Cochain F G (-1)).v (p + 1) p ⋯ + (↑z : Cochain F G (-1)).v p (p - 1) ⋯ ≫ G.d (p - 1) p +
      φ₂.f p =
    F.d p (p + 1) ≫ (↑z : Cochain F G (-1)).v (p + 1) p ⋯ +
        CategoryStruct.comp (Y := G.X (p - 1))
          (if hij : p + -1 = p - 1 then (↑z : Cochain F G (-1)).v p (p - 1) hij else 0) (G.d (p - 1) p) +
      φ₂.f p
⊢ φ₁.f p =
    HAdd.hAdd (α := F.X p ⟶ G.X p) (β := F.X p ⟶ G.X p)
        ((dNext p : (a : (i j : ℤ) → F.X i ⟶ G.X j) → F.X p ⟶ G.X p) fun (i j : ℤ) ↦
            if hij : i + -1 = j then (↑z : Cochain F G (-1)).v i j hij else 0 :
          F.X p ⟶ G.X p)
        ((prevD p : (a : (i j : ℤ) → F.X i ⟶ G.X j) → F.X p ⟶ G.X p) fun (i j : ℤ) ↦
            if hij : i + -1 = j then (↑z : Cochain F G (-1)).v i j hij else 0 :
          F.X p ⟶ G.X p) +
      φ₂.f p
have hc : p + 1 + -1 = p
Tactic: rw [dNext_eq _ h₂, prevD_eq _ h₁, eq, dif_pos, dif_pos]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplex (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
R : Type u_1
inst_2 : Ring R
inst_3 : Linear.{u_1, v, u} R C
F G K L : CochainComplex.{v, u, 0} C ℤ
n m : ℤ
φ₁ φ₂ : F ⟶ G
z : { z : Cochain F G (-1) // ofHom φ₁ = δ (-1) 0 z + ofHom φ₂ }
p : ℤ
h₁ : (ComplexShape.up ℤ).Rel (p - 1) p
h₂ : (ComplexShape.up ℤ).Rel p (p + 1)
eq :
  φ₁.f p =
    F.d p (p + 1) ≫ (↑z : Cochain F G (-1)).v (p + 1) p ⋯ + (↑z : Cochain F G (-1)).v p (p - 1) ⋯ ≫ G.d (p - 1) p +
      φ₂.f p
rw :
  φ₁.f p =
    HAdd.hAdd (α := F.X p ⟶ G.X p) (β := F.X p ⟶ G.X p)
        (CategoryStruct.comp (Y := F.X (p + 1)) (F.d p (p + 1))
          (if hij : p + 1 + -1 = p then (↑z : Cochain F G (-1)).v (p + 1) p hij else 0))
        ((prevD p : (a : (i j : ℤ) → F.X i ⟶ G.X j) → F.X p ⟶ G.X p) fun (i j : ℤ) ↦
            if hij : i + -1 = j then (↑z : Cochain F G (-1)).v i j hij else 0 :
          F.X p ⟶ G.X p) +
      φ₂.f p
rw₁ :
  φ₁.f p =
    CategoryStruct.comp (Y := F.X (p + 1)) (F.d p (p + 1))
          (if hij : p + 1 + -1 = p then (↑z : Cochain F G (-1)).v (p + 1) p hij else 0) +
        CategoryStruct.comp (Y := G.X (p - 1))
          (if hij : p + -1 = p - 1 then (↑z : Cochain F G (-1)).v p (p - 1) hij else 0) (G.d (p - 1) p) +
      φ₂.f p
rw₂ :
  F.d p (p + 1) ≫ (↑z : Cochain F G (-1)).v (p + 1) p ⋯ + (↑z : Cochain F G (-1)).v p (p - 1) ⋯ ≫ G.d (p - 1) p +
      φ₂.f p =
    CategoryStruct.comp (Y := F.X (p + 1)) (F.d p (p + 1))
          (if hij : p + 1 + -1 = p then (↑z : Cochain F G (-1)).v (p + 1) p hij else 0) +
        CategoryStruct.comp (Y := G.X (p - 1))
          (if hij : p + -1 = p - 1 then (↑z : Cochain F G (-1)).v p (p - 1) hij else 0) (G.d (p - 1) p) +
      φ₂.f p
rw₃ :
  F.d p (p + 1) ≫ (↑z : Cochain F G (-1)).v (p + 1) p ⋯ + (↑z : Cochain F G (-1)).v p (p - 1) ⋯ ≫ G.d (p - 1) p +
      φ₂.f p =
    F.d p (p + 1) ≫ (↑z : Cochain F G (-1)).v (p + 1) p ⋯ +
        CategoryStruct.comp (Y := G.X (p - 1))
          (if hij : p + -1 = p - 1 then (↑z : Cochain F G (-1)).v p (p - 1) hij else 0) (G.d (p - 1) p) +
      φ₂.f p
hc : p + 1 + -1 = p
⊢ φ₁.f p =
    HAdd.hAdd (α := F.X p ⟶ G.X p) (β := F.X p ⟶ G.X p)
        ((dNext p : (a : (i j : ℤ) → F.X i ⟶ G.X j) → F.X p ⟶ G.X p) fun (i j : ℤ) ↦
            if hij : i + -1 = j then (↑z : Cochain F G (-1)).v i j hij else 0 :
          F.X p ⟶ G.X p)
        ((prevD p : (a : (i j : ℤ) → F.X i ⟶ G.X j) → F.X p ⟶ G.X p) fun (i j : ℤ) ↦
            if hij : i + -1 = j then (↑z : Cochain F G (-1)).v i j hij else 0 :
          F.X p ⟶ G.X p) +
      φ₂.f p
have rw₄ : F.d p (p + 1) ≫ (↑z : Cochain F G (-1)).v (p + 1) p sorry + (↑z : Cochain F G (-1)).v p (p - 1) sorry ≫ G.d (p - 1) p + φ₂.f p =
  F.d p (p + 1) ≫ (↑z : Cochain F G (-1)).v (p + 1) p sorry + (↑z : Cochain F G (-1)).v p (p - 1) sorry ≫ G.d (p - 1) p + φ₂.f p
Tactic: rw [dNext_eq _ h₂, prevD_eq _ h₁, eq, dif_pos, dif_pos]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplex (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
R : Type u_1
inst_2 : Ring R
inst_3 : Linear.{u_1, v, u} R C
F G K L : CochainComplex.{v, u, 0} C ℤ
n m : ℤ
φ₁ φ₂ : F ⟶ G
z : { z : Cochain F G (-1) // ofHom φ₁ = δ (-1) 0 z + ofHom φ₂ }
p : ℤ
h₁ : (ComplexShape.up ℤ).Rel (p - 1) p
h₂ : (ComplexShape.up ℤ).Rel p (p + 1)
eq :
  φ₁.f p =
    F.d p (p + 1) ≫ (↑z : Cochain F G (-1)).v (p + 1) p ⋯ + (↑z : Cochain F G (-1)).v p (p - 1) ⋯ ≫ G.d (p - 1) p +
      φ₂.f p
rw :
  φ₁.f p =
    HAdd.hAdd (α := F.X p ⟶ G.X p) (β := F.X p ⟶ G.X p)
        (CategoryStruct.comp (Y := F.X (p + 1)) (F.d p (p + 1))
          (if hij : p + 1 + -1 = p then (↑z : Cochain F G (-1)).v (p + 1) p hij else 0))
        ((prevD p : (a : (i j : ℤ) → F.X i ⟶ G.X j) → F.X p ⟶ G.X p) fun (i j : ℤ) ↦
            if hij : i + -1 = j then (↑z : Cochain F G (-1)).v i j hij else 0 :
          F.X p ⟶ G.X p) +
      φ₂.f p
rw₁ :
  φ₁.f p =
    CategoryStruct.comp (Y := F.X (p + 1)) (F.d p (p + 1))
          (if hij : p + 1 + -1 = p then (↑z : Cochain F G (-1)).v (p + 1) p hij else 0) +
        CategoryStruct.comp (Y := G.X (p - 1))
          (if hij : p + -1 = p - 1 then (↑z : Cochain F G (-1)).v p (p - 1) hij else 0) (G.d (p - 1) p) +
      φ₂.f p
rw₂ :
  F.d p (p + 1) ≫ (↑z : Cochain F G (-1)).v (p + 1) p ⋯ + (↑z : Cochain F G (-1)).v p (p - 1) ⋯ ≫ G.d (p - 1) p +
      φ₂.f p =
    CategoryStruct.comp (Y := F.X (p + 1)) (F.d p (p + 1))
          (if hij : p + 1 + -1 = p then (↑z : Cochain F G (-1)).v (p + 1) p hij else 0) +
        CategoryStruct.comp (Y := G.X (p - 1))
          (if hij : p + -1 = p - 1 then (↑z : Cochain F G (-1)).v p (p - 1) hij else 0) (G.d (p - 1) p) +
      φ₂.f p
rw₃ :
  F.d p (p + 1) ≫ (↑z : Cochain F G (-1)).v (p + 1) p ⋯ + (↑z : Cochain F G (-1)).v p (p - 1) ⋯ ≫ G.d (p - 1) p +
      φ₂.f p =
    F.d p (p + 1) ≫ (↑z : Cochain F G (-1)).v (p + 1) p ⋯ +
        CategoryStruct.comp (Y := G.X (p - 1))
          (if hij : p + -1 = p - 1 then (↑z : Cochain F G (-1)).v p (p - 1) hij else 0) (G.d (p - 1) p) +
      φ₂.f p
hc : p + 1 + -1 = p
rw₄ :
  F.d p (p + 1) ≫ (↑z : Cochain F G (-1)).v (p + 1) p ⋯ + (↑z : Cochain F G (-1)).v p (p - 1) ⋯ ≫ G.d (p - 1) p +
      φ₂.f p =
    F.d p (p + 1) ≫ (↑z : Cochain F G (-1)).v (p + 1) p ⋯ + (↑z : Cochain F G (-1)).v p (p - 1) ⋯ ≫ G.d (p - 1) p +
      φ₂.f p
⊢ φ₁.f p =
    HAdd.hAdd (α := F.X p ⟶ G.X p) (β := F.X p ⟶ G.X p)
        ((dNext p : (a : (i j : ℤ) → F.X i ⟶ G.X j) → F.X p ⟶ G.X p) fun (i j : ℤ) ↦
            if hij : i + -1 = j then (↑z : Cochain F G (-1)).v i j hij else 0 :
          F.X p ⟶ G.X p)
        ((prevD p : (a : (i j : ℤ) → F.X i ⟶ G.X j) → F.X p ⟶ G.X p) fun (i j : ℤ) ↦
            if hij : i + -1 = j then (↑z : Cochain F G (-1)).v i j hij else 0 :
          F.X p ⟶ G.X p) +
      φ₂.f p
have hc₁ : p + -1 = p - 1
Tactic: rw [dNext_eq _ h₂, prevD_eq _ h₁, eq, dif_pos, dif_pos]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplex (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
R : Type u_1
inst_2 : Ring R
inst_3 : Linear.{u_1, v, u} R C
F G K L : CochainComplex.{v, u, 0} C ℤ
n m : ℤ
φ₁ φ₂ : F ⟶ G
ho : Homotopy φ₁ φ₂
⊢ (fun (z : { z : Cochain F G (-1) // ofHom φ₁ = δ (-1) 0 z + ofHom φ₂ }) ↦
        ({ hom := fun (i j : ℤ) ↦ if hij : i + -1 = j then (↑z : Cochain F G (-1)).v i j hij else 0, zero := ⋯,
            comm := ⋯ } :
          Homotopy φ₁ φ₂))
      ((fun (ho : Homotopy φ₁ φ₂) ↦
          (Subtype.mk (p := fun (z : Cochain F G (-1)) ↦ ofHom φ₁ = δ (-1) 0 z + ofHom φ₂) (ofHomotopy ho) ⋯ :
            { z : Cochain F G (-1) // ofHom φ₁ = δ (-1) 0 z + ofHom φ₂ }))
        ho) =
    ho
have hom : ∀ (i j : ℤ),
  Homotopy.hom (f := φ₁) (g := φ₂)
      ((fun (z : { z : Cochain F G (-1) // ofHom φ₁ = δ (-1) 0 z + ofHom φ₂ }) ↦
          ({ hom := fun (i j : ℤ) ↦ if hij : i + -1 = j then (↑z : Cochain F G (-1)).v i j hij else 0, zero := sorry,
              comm := sorry } :
            Homotopy φ₁ φ₂))
        ((fun (ho : Homotopy φ₁ φ₂) ↦
            (Subtype.mk (p := fun (z : Cochain F G (-1)) ↦ ofHom φ₁ = δ (-1) 0 z + ofHom φ₂) (ofHomotopy ho) sorry :
              { z : Cochain F G (-1) // ofHom φ₁ = δ (-1) 0 z + ofHom φ₂ }))
          ho))
      i j =
    ho.hom i j
Tactic: ext i j
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplex (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
R : Type u_1
inst_2 : Ring R
inst_3 : Linear.{u_1, v, u} R C
F G K L : CochainComplex.{v, u, 0} C ℤ
n m : ℤ
φ₁ φ₂ : F ⟶ G
ho : Homotopy φ₁ φ₂
i j : ℤ
⊢ Homotopy.hom (f := φ₁) (g := φ₂)
      ((fun (z : { z : Cochain F G (-1) // ofHom φ₁ = δ (-1) 0 z + ofHom φ₂ }) ↦
          ({ hom := fun (i j : ℤ) ↦ if hij : i + -1 = j then (↑z : Cochain F G (-1)).v i j hij else 0, zero := ⋯,
              comm := ⋯ } :
            Homotopy φ₁ φ₂))
        ((fun (ho : Homotopy φ₁ φ₂) ↦
            (Subtype.mk (p := fun (z : Cochain F G (-1)) ↦ ofHom φ₁ = δ (-1) 0 z + ofHom φ₂) (ofHomotopy ho) ⋯ :
              { z : Cochain F G (-1) // ofHom φ₁ = δ (-1) 0 z + ofHom φ₂ }))
          ho))
      i j =
    ho.hom i j
have hom : (if hij : i + -1 = j then (ofHomotopy ho).v i j hij else 0) = ho.hom i j
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplex (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
R : Type u_1
inst_2 : Ring R
inst_3 : Linear.{u_1, v, u} R C
F G K L : CochainComplex.{v, u, 0} C ℤ
n m : ℤ
φ₁ φ₂ : F ⟶ G
ho : Homotopy φ₁ φ₂
i j : ℤ
⊢ (if hij : i + -1 = j then (ofHomotopy ho).v i j hij else 0) = ho.hom i j
have pos : ∀ (h : i + -1 = j), (ofHomotopy ho).v i j h = ho.hom i j
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplex (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
R : Type u_1
inst_2 : Ring R
inst_3 : Linear.{u_1, v, u} R C
F G K L : CochainComplex.{v, u, 0} C ℤ
n m : ℤ
φ₁ φ₂ : F ⟶ G
ho : Homotopy φ₁ φ₂
i j : ℤ
pos : ∀ (h : i + -1 = j), (ofHomotopy ho).v i j h = ho.hom i j
⊢ (if hij : i + -1 = j then (ofHomotopy ho).v i j hij else 0) = ho.hom i j
have neg : ∀ (h : ¬i + -1 = j), 0 = ho.hom i j
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplex (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
R : Type u_1
inst_2 : Ring R
inst_3 : Linear.{u_1, v, u} R C
F G K L : CochainComplex.{v, u, 0} C ℤ
n m : ℤ
φ₁ φ₂ : F ⟶ G
ho : Homotopy φ₁ φ₂
i j : ℤ
h : ¬i + -1 = j
⊢ 0 = ho.hom i j
have neg : Eq.{v + 1} (α := F.X i ⟶ G.X j) 0 0
Tactic: rw [ho.zero i j (fun h' => h (by dsimp at h'; lia))]