awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Injective.Resolution (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
Y Z : C
I : InjectiveResolution.{v, u} Y
J : InjectiveResolution.{v, u} Z
f : I.cocomplex ⟶ J.cocomplex
comm : I.ι ≫ f = 0
⊢ (ShortComplex.mk (X₁ := I.cocomplex.X 0) (X₂ := I.cocomplex.X (HAdd.hAdd (α := ℕ) 0 1)) (X₃ :=
          I.cocomplex.X (HAdd.hAdd (α := ℕ) 0 2)) (I.cocomplex.d 0 (HAdd.hAdd (α := ℕ) 0 1))
          (I.cocomplex.d (HAdd.hAdd (α := ℕ) 0 1) (HAdd.hAdd (α := ℕ) 0 2)) ⋯).f ≫
      (f.f 1 - descHomotopyZeroZero f comm ≫ J.cocomplex.d 0 1) =
    0
have rw : (ShortComplex.mk (X₁ := I.cocomplex.X 0) (X₂ := I.cocomplex.X (HAdd.hAdd (α := ℕ) 0 1)) (X₃ :=
          I.cocomplex.X (HAdd.hAdd (α := ℕ) 0 2)) (I.cocomplex.d 0 (HAdd.hAdd (α := ℕ) 0 1))
          (I.cocomplex.d (HAdd.hAdd (α := ℕ) 0 1) (HAdd.hAdd (α := ℕ) 0 2)) sorry).f ≫
      f.f 1 -
    (ShortComplex.mk (X₁ := I.cocomplex.X 0) (X₂ := I.cocomplex.X (HAdd.hAdd (α := ℕ) 0 1)) (X₃ :=
          I.cocomplex.X (HAdd.hAdd (α := ℕ) 0 2)) (I.cocomplex.d 0 (HAdd.hAdd (α := ℕ) 0 1))
          (I.cocomplex.d (HAdd.hAdd (α := ℕ) 0 1) (HAdd.hAdd (α := ℕ) 0 2)) sorry).f ≫
      descHomotopyZeroZero f comm ≫ J.cocomplex.d 0 1 =
  0
Tactic: rw [Preadditive.comp_sub, comp_descHomotopyZeroZero_assoc f comm,
          HomologicalComplex.Hom.comm, sub_self]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Injective.Resolution (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
Y Z : C
I : InjectiveResolution.{v, u} Y
J : InjectiveResolution.{v, u} Z
f : I.cocomplex ⟶ J.cocomplex
comm : I.ι ≫ f = 0
rw :
  (ShortComplex.mk (X₁ := I.cocomplex.X 0) (X₂ := I.cocomplex.X (HAdd.hAdd (α := ℕ) 0 1)) (X₃ :=
            I.cocomplex.X (HAdd.hAdd (α := ℕ) 0 2)) (I.cocomplex.d 0 (HAdd.hAdd (α := ℕ) 0 1))
            (I.cocomplex.d (HAdd.hAdd (α := ℕ) 0 1) (HAdd.hAdd (α := ℕ) 0 2)) ⋯).f ≫
        f.f 1 -
      (ShortComplex.mk (X₁ := I.cocomplex.X 0) (X₂ := I.cocomplex.X (HAdd.hAdd (α := ℕ) 0 1)) (X₃ :=
            I.cocomplex.X (HAdd.hAdd (α := ℕ) 0 2)) (I.cocomplex.d 0 (HAdd.hAdd (α := ℕ) 0 1))
            (I.cocomplex.d (HAdd.hAdd (α := ℕ) 0 1) (HAdd.hAdd (α := ℕ) 0 2)) ⋯).f ≫
        descHomotopyZeroZero f comm ≫ J.cocomplex.d 0 1 =
    0
⊢ (ShortComplex.mk (X₁ := I.cocomplex.X 0) (X₂ := I.cocomplex.X (HAdd.hAdd (α := ℕ) 0 1)) (X₃ :=
          I.cocomplex.X (HAdd.hAdd (α := ℕ) 0 2)) (I.cocomplex.d 0 (HAdd.hAdd (α := ℕ) 0 1))
          (I.cocomplex.d (HAdd.hAdd (α := ℕ) 0 1) (HAdd.hAdd (α := ℕ) 0 2)) ⋯).f ≫
      (f.f 1 - descHomotopyZeroZero f comm ≫ J.cocomplex.d 0 1) =
    0
have rw₁ : (ShortComplex.mk (X₁ := I.cocomplex.X 0) (X₂ := I.cocomplex.X (HAdd.hAdd (α := ℕ) 0 1)) (X₃ :=
          I.cocomplex.X (HAdd.hAdd (α := ℕ) 0 2)) (I.cocomplex.d 0 (HAdd.hAdd (α := ℕ) 0 1))
          (I.cocomplex.d (HAdd.hAdd (α := ℕ) 0 1) (HAdd.hAdd (α := ℕ) 0 2)) sorry).f ≫
      f.f 1 -
    f.f 0 ≫ J.cocomplex.d 0 1 =
  0
Tactic: rw [Preadditive.comp_sub, comp_descHomotopyZeroZero_assoc f comm,
          HomologicalComplex.Hom.comm, sub_self]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Injective.Resolution (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
Y Z : C
I : InjectiveResolution.{v, u} Y
J : InjectiveResolution.{v, u} Z
f : I.cocomplex ⟶ J.cocomplex
comm : I.ι ≫ f = 0
rw :
  (ShortComplex.mk (X₁ := I.cocomplex.X 0) (X₂ := I.cocomplex.X (HAdd.hAdd (α := ℕ) 0 1)) (X₃ :=
            I.cocomplex.X (HAdd.hAdd (α := ℕ) 0 2)) (I.cocomplex.d 0 (HAdd.hAdd (α := ℕ) 0 1))
            (I.cocomplex.d (HAdd.hAdd (α := ℕ) 0 1) (HAdd.hAdd (α := ℕ) 0 2)) ⋯).f ≫
        f.f 1 -
      (ShortComplex.mk (X₁ := I.cocomplex.X 0) (X₂ := I.cocomplex.X (HAdd.hAdd (α := ℕ) 0 1)) (X₃ :=
            I.cocomplex.X (HAdd.hAdd (α := ℕ) 0 2)) (I.cocomplex.d 0 (HAdd.hAdd (α := ℕ) 0 1))
            (I.cocomplex.d (HAdd.hAdd (α := ℕ) 0 1) (HAdd.hAdd (α := ℕ) 0 2)) ⋯).f ≫
        descHomotopyZeroZero f comm ≫ J.cocomplex.d 0 1 =
    0
rw₁ :
  (ShortComplex.mk (X₁ := I.cocomplex.X 0) (X₂ := I.cocomplex.X (HAdd.hAdd (α := ℕ) 0 1)) (X₃ :=
            I.cocomplex.X (HAdd.hAdd (α := ℕ) 0 2)) (I.cocomplex.d 0 (HAdd.hAdd (α := ℕ) 0 1))
            (I.cocomplex.d (HAdd.hAdd (α := ℕ) 0 1) (HAdd.hAdd (α := ℕ) 0 2)) ⋯).f ≫
        f.f 1 -
      f.f 0 ≫ J.cocomplex.d 0 1 =
    0
⊢ (ShortComplex.mk (X₁ := I.cocomplex.X 0) (X₂ := I.cocomplex.X (HAdd.hAdd (α := ℕ) 0 1)) (X₃ :=
          I.cocomplex.X (HAdd.hAdd (α := ℕ) 0 2)) (I.cocomplex.d 0 (HAdd.hAdd (α := ℕ) 0 1))
          (I.cocomplex.d (HAdd.hAdd (α := ℕ) 0 1) (HAdd.hAdd (α := ℕ) 0 2)) ⋯).f ≫
      (f.f 1 - descHomotopyZeroZero f comm ≫ J.cocomplex.d 0 1) =
    0
have rw₂ : (ShortComplex.mk (X₁ := I.cocomplex.X 0) (X₂ := I.cocomplex.X (HAdd.hAdd (α := ℕ) 0 1)) (X₃ :=
          I.cocomplex.X (HAdd.hAdd (α := ℕ) 0 2)) (I.cocomplex.d 0 (HAdd.hAdd (α := ℕ) 0 1))
          (I.cocomplex.d (HAdd.hAdd (α := ℕ) 0 1) (HAdd.hAdd (α := ℕ) 0 2)) sorry).f ≫
      f.f 1 -
    I.cocomplex.d 0 1 ≫ f.f 1 =
  0
Tactic: rw [Preadditive.comp_sub, comp_descHomotopyZeroZero_assoc f comm,
          HomologicalComplex.Hom.comm, sub_self]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Injective.Resolution (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
Y Z : C
I : InjectiveResolution.{v, u} Y
J : InjectiveResolution.{v, u} Z
f : I.cocomplex ⟶ J.cocomplex
comm : I.ι ≫ f = 0
rw :
  (ShortComplex.mk (X₁ := I.cocomplex.X 0) (X₂ := I.cocomplex.X (HAdd.hAdd (α := ℕ) 0 1)) (X₃ :=
            I.cocomplex.X (HAdd.hAdd (α := ℕ) 0 2)) (I.cocomplex.d 0 (HAdd.hAdd (α := ℕ) 0 1))
            (I.cocomplex.d (HAdd.hAdd (α := ℕ) 0 1) (HAdd.hAdd (α := ℕ) 0 2)) ⋯).f ≫
        f.f 1 -
      (ShortComplex.mk (X₁ := I.cocomplex.X 0) (X₂ := I.cocomplex.X (HAdd.hAdd (α := ℕ) 0 1)) (X₃ :=
            I.cocomplex.X (HAdd.hAdd (α := ℕ) 0 2)) (I.cocomplex.d 0 (HAdd.hAdd (α := ℕ) 0 1))
            (I.cocomplex.d (HAdd.hAdd (α := ℕ) 0 1) (HAdd.hAdd (α := ℕ) 0 2)) ⋯).f ≫
        descHomotopyZeroZero f comm ≫ J.cocomplex.d 0 1 =
    0
rw₁ :
  (ShortComplex.mk (X₁ := I.cocomplex.X 0) (X₂ := I.cocomplex.X (HAdd.hAdd (α := ℕ) 0 1)) (X₃ :=
            I.cocomplex.X (HAdd.hAdd (α := ℕ) 0 2)) (I.cocomplex.d 0 (HAdd.hAdd (α := ℕ) 0 1))
            (I.cocomplex.d (HAdd.hAdd (α := ℕ) 0 1) (HAdd.hAdd (α := ℕ) 0 2)) ⋯).f ≫
        f.f 1 -
      f.f 0 ≫ J.cocomplex.d 0 1 =
    0
rw₂ :
  (ShortComplex.mk (X₁ := I.cocomplex.X 0) (X₂ := I.cocomplex.X (HAdd.hAdd (α := ℕ) 0 1)) (X₃ :=
            I.cocomplex.X (HAdd.hAdd (α := ℕ) 0 2)) (I.cocomplex.d 0 (HAdd.hAdd (α := ℕ) 0 1))
            (I.cocomplex.d (HAdd.hAdd (α := ℕ) 0 1) (HAdd.hAdd (α := ℕ) 0 2)) ⋯).f ≫
        f.f 1 -
      I.cocomplex.d 0 1 ≫ f.f 1 =
    0
⊢ (ShortComplex.mk (X₁ := I.cocomplex.X 0) (X₂ := I.cocomplex.X (HAdd.hAdd (α := ℕ) 0 1)) (X₃ :=
          I.cocomplex.X (HAdd.hAdd (α := ℕ) 0 2)) (I.cocomplex.d 0 (HAdd.hAdd (α := ℕ) 0 1))
          (I.cocomplex.d (HAdd.hAdd (α := ℕ) 0 1) (HAdd.hAdd (α := ℕ) 0 2)) ⋯).f ≫
      (f.f 1 - descHomotopyZeroZero f comm ≫ J.cocomplex.d 0 1) =
    0
have rw₃ : Eq.{v + 1} (α :=
  (ShortComplex.mk (X₁ := I.cocomplex.X 0) (X₂ := I.cocomplex.X (HAdd.hAdd (α := ℕ) 0 1)) (X₃ :=
        I.cocomplex.X (HAdd.hAdd (α := ℕ) 0 2)) (I.cocomplex.d 0 (HAdd.hAdd (α := ℕ) 0 1))
        (I.cocomplex.d (HAdd.hAdd (α := ℕ) 0 1) (HAdd.hAdd (α := ℕ) 0 2)) sorry).X₁ ⟶
    J.cocomplex.X 1)
  0 0
Tactic: rw [Preadditive.comp_sub, comp_descHomotopyZeroZero_assoc f comm,
          HomologicalComplex.Hom.comm, sub_self]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Injective.Resolution (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
Y Z : C
I : InjectiveResolution.{v, u} Y
J : InjectiveResolution.{v, u} Z
f : I.cocomplex ⟶ J.cocomplex
n : ℕ
g : I.cocomplex.X (n + 1) ⟶ J.cocomplex.X n
g' : I.cocomplex.X (n + 2) ⟶ J.cocomplex.X (n + 1)
w : f.f (n + 1) = I.cocomplex.d (n + 1) (n + 2) ≫ g' + g ≫ J.cocomplex.d n (n + 1)
⊢ (ShortComplex.mk (X₁ := I.cocomplex.X (n + 1)) (X₂ := I.cocomplex.X (n + 1 + 1)) (X₃ := I.cocomplex.X (n + 1 + 2))
          (I.cocomplex.d (n + 1) (n + 1 + 1)) (I.cocomplex.d (n + 1 + 1) (n + 1 + 2)) ⋯).f ≫
      (f.f (n + 2) - g' ≫ J.cocomplex.d (n + 1) (n + 2)) =
    0
have dsimp : Eq (α := I.cocomplex.X (n + 1) ⟶ J.cocomplex.X (n + 2))
  (I.cocomplex.d (n + 1) (n + 1 + 1) ≫ (f.f (n + 2) - g' ≫ J.cocomplex.d (n + 1) (n + 2))) 0
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Injective.Resolution (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
Y Z : C
I : InjectiveResolution.{v, u} Y
J : InjectiveResolution.{v, u} Z
f : I.cocomplex ⟶ J.cocomplex
n : ℕ
g : I.cocomplex.X (n + 1) ⟶ J.cocomplex.X n
g' : I.cocomplex.X (n + 2) ⟶ J.cocomplex.X (n + 1)
w : f.f (n + 1) = I.cocomplex.d (n + 1) (n + 2) ≫ g' + g ≫ J.cocomplex.d n (n + 1)
⊢ Eq (α := I.cocomplex.X (n + 1) ⟶ J.cocomplex.X (n + 2))
    (I.cocomplex.d (n + 1) (n + 1 + 1) ≫ (f.f (n + 2) - g' ≫ J.cocomplex.d (n + 1) (n + 2))) 0
have rw : HSub.hSub (α := I.cocomplex.X (n + 1) ⟶ J.cocomplex.X (n + 2)) (I.cocomplex.d (n + 1) (n + 1 + 1) ≫ f.f (n + 2))
    (I.cocomplex.d (n + 1) (n + 1 + 1) ≫ g' ≫ J.cocomplex.d (n + 1) (n + 2)) =
  0
Tactic: rw [Preadditive.comp_sub, ← HomologicalComplex.Hom.comm, w, Preadditive.add_comp,
        Category.assoc, Category.assoc, HomologicalComplex.d_comp_d, comp_zero,
        add_zero, sub_self]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Injective.Resolution (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
Y Z : C
I : InjectiveResolution.{v, u} Y
J : InjectiveResolution.{v, u} Z
f : I.cocomplex ⟶ J.cocomplex
n : ℕ
g : I.cocomplex.X (n + 1) ⟶ J.cocomplex.X n
g' : I.cocomplex.X (n + 2) ⟶ J.cocomplex.X (n + 1)
w : f.f (n + 1) = I.cocomplex.d (n + 1) (n + 2) ≫ g' + g ≫ J.cocomplex.d n (n + 1)
rw :
  HSub.hSub (α := I.cocomplex.X (n + 1) ⟶ J.cocomplex.X (n + 2)) (I.cocomplex.d (n + 1) (n + 1 + 1) ≫ f.f (n + 2))
      (I.cocomplex.d (n + 1) (n + 1 + 1) ≫ g' ≫ J.cocomplex.d (n + 1) (n + 2)) =
    0
⊢ Eq (α := I.cocomplex.X (n + 1) ⟶ J.cocomplex.X (n + 2))
    (I.cocomplex.d (n + 1) (n + 1 + 1) ≫ (f.f (n + 2) - g' ≫ J.cocomplex.d (n + 1) (n + 2))) 0
have rw₁ : HSub.hSub (α := I.cocomplex.X (n + 1) ⟶ J.cocomplex.X (n + 2)) (f.f (n + 1) ≫ J.cocomplex.d (n + 1) (n + 1 + 1))
    (I.cocomplex.d (n + 1) (n + 1 + 1) ≫ g' ≫ J.cocomplex.d (n + 1) (n + 2)) =
  0
Tactic: rw [Preadditive.comp_sub, ← HomologicalComplex.Hom.comm, w, Preadditive.add_comp,
        Category.assoc, Category.assoc, HomologicalComplex.d_comp_d, comp_zero,
        add_zero, sub_self]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Injective.Resolution (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
Y Z : C
I : InjectiveResolution.{v, u} Y
J : InjectiveResolution.{v, u} Z
f : I.cocomplex ⟶ J.cocomplex
n : ℕ
g : I.cocomplex.X (n + 1) ⟶ J.cocomplex.X n
g' : I.cocomplex.X (n + 2) ⟶ J.cocomplex.X (n + 1)
w : f.f (n + 1) = I.cocomplex.d (n + 1) (n + 2) ≫ g' + g ≫ J.cocomplex.d n (n + 1)
rw :
  HSub.hSub (α := I.cocomplex.X (n + 1) ⟶ J.cocomplex.X (n + 2)) (I.cocomplex.d (n + 1) (n + 1 + 1) ≫ f.f (n + 2))
      (I.cocomplex.d (n + 1) (n + 1 + 1) ≫ g' ≫ J.cocomplex.d (n + 1) (n + 2)) =
    0
rw₁ :
  HSub.hSub (α := I.cocomplex.X (n + 1) ⟶ J.cocomplex.X (n + 2)) (f.f (n + 1) ≫ J.cocomplex.d (n + 1) (n + 1 + 1))
      (I.cocomplex.d (n + 1) (n + 1 + 1) ≫ g' ≫ J.cocomplex.d (n + 1) (n + 2)) =
    0
⊢ Eq (α := I.cocomplex.X (n + 1) ⟶ J.cocomplex.X (n + 2))
    (I.cocomplex.d (n + 1) (n + 1 + 1) ≫ (f.f (n + 2) - g' ≫ J.cocomplex.d (n + 1) (n + 2))) 0
have rw₂ : HSub.hSub (α := I.cocomplex.X (n + 1) ⟶ J.cocomplex.X (n + 2))
    ((I.cocomplex.d (n + 1) (n + 2) ≫ g' + g ≫ J.cocomplex.d n (n + 1)) ≫ J.cocomplex.d (n + 1) (n + 1 + 1))
    (I.cocomplex.d (n + 1) (n + 1 + 1) ≫ g' ≫ J.cocomplex.d (n + 1) (n + 2)) =
  0
Tactic: rw [Preadditive.comp_sub, ← HomologicalComplex.Hom.comm, w, Preadditive.add_comp,
        Category.assoc, Category.assoc, HomologicalComplex.d_comp_d, comp_zero,
        add_zero, sub_self]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Injective.Resolution (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
Y Z : C
I : InjectiveResolution.{v, u} Y
J : InjectiveResolution.{v, u} Z
f : I.cocomplex ⟶ J.cocomplex
n : ℕ
g : I.cocomplex.X (n + 1) ⟶ J.cocomplex.X n
g' : I.cocomplex.X (n + 2) ⟶ J.cocomplex.X (n + 1)
w : f.f (n + 1) = I.cocomplex.d (n + 1) (n + 2) ≫ g' + g ≫ J.cocomplex.d n (n + 1)
rw :
  HSub.hSub (α := I.cocomplex.X (n + 1) ⟶ J.cocomplex.X (n + 2)) (I.cocomplex.d (n + 1) (n + 1 + 1) ≫ f.f (n + 2))
      (I.cocomplex.d (n + 1) (n + 1 + 1) ≫ g' ≫ J.cocomplex.d (n + 1) (n + 2)) =
    0
rw₁ :
  HSub.hSub (α := I.cocomplex.X (n + 1) ⟶ J.cocomplex.X (n + 2)) (f.f (n + 1) ≫ J.cocomplex.d (n + 1) (n + 1 + 1))
      (I.cocomplex.d (n + 1) (n + 1 + 1) ≫ g' ≫ J.cocomplex.d (n + 1) (n + 2)) =
    0
rw₂ :
  HSub.hSub (α := I.cocomplex.X (n + 1) ⟶ J.cocomplex.X (n + 2))
      ((I.cocomplex.d (n + 1) (n + 2) ≫ g' + g ≫ J.cocomplex.d n (n + 1)) ≫ J.cocomplex.d (n + 1) (n + 1 + 1))
      (I.cocomplex.d (n + 1) (n + 1 + 1) ≫ g' ≫ J.cocomplex.d (n + 1) (n + 2)) =
    0
⊢ Eq (α := I.cocomplex.X (n + 1) ⟶ J.cocomplex.X (n + 2))
    (I.cocomplex.d (n + 1) (n + 1 + 1) ≫ (f.f (n + 2) - g' ≫ J.cocomplex.d (n + 1) (n + 2))) 0
have rw₃ : HAdd.hAdd (α := I.cocomplex.X (n + 1) ⟶ J.cocomplex.X (n + 1 + 1))
      ((I.cocomplex.d (n + 1) (n + 2) ≫ g') ≫ J.cocomplex.d (n + 1) (n + 1 + 1))
      (CategoryStruct.comp (Y := J.cocomplex.X (n + 1)) (g ≫ J.cocomplex.d n (n + 1))
        (J.cocomplex.d (n + 1) (n + 1 + 1))) -
    I.cocomplex.d (n + 1) (n + 1 + 1) ≫ g' ≫ J.cocomplex.d (n + 1) (n + 2) =
  0
Tactic: rw [Preadditive.comp_sub, ← HomologicalComplex.Hom.comm, w, Preadditive.add_comp,
        Category.assoc, Category.assoc, HomologicalComplex.d_comp_d, comp_zero,
        add_zero, sub_self]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Injective.Resolution (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
Y Z : C
I : InjectiveResolution.{v, u} Y
J : InjectiveResolution.{v, u} Z
f : I.cocomplex ⟶ J.cocomplex
n : ℕ
g : I.cocomplex.X (n + 1) ⟶ J.cocomplex.X n
g' : I.cocomplex.X (n + 2) ⟶ J.cocomplex.X (n + 1)
w : f.f (n + 1) = I.cocomplex.d (n + 1) (n + 2) ≫ g' + g ≫ J.cocomplex.d n (n + 1)
rw :
  HSub.hSub (α := I.cocomplex.X (n + 1) ⟶ J.cocomplex.X (n + 2)) (I.cocomplex.d (n + 1) (n + 1 + 1) ≫ f.f (n + 2))
      (I.cocomplex.d (n + 1) (n + 1 + 1) ≫ g' ≫ J.cocomplex.d (n + 1) (n + 2)) =
    0
rw₁ :
  HSub.hSub (α := I.cocomplex.X (n + 1) ⟶ J.cocomplex.X (n + 2)) (f.f (n + 1) ≫ J.cocomplex.d (n + 1) (n + 1 + 1))
      (I.cocomplex.d (n + 1) (n + 1 + 1) ≫ g' ≫ J.cocomplex.d (n + 1) (n + 2)) =
    0
rw₂ :
  HSub.hSub (α := I.cocomplex.X (n + 1) ⟶ J.cocomplex.X (n + 2))
      ((I.cocomplex.d (n + 1) (n + 2) ≫ g' + g ≫ J.cocomplex.d n (n + 1)) ≫ J.cocomplex.d (n + 1) (n + 1 + 1))
      (I.cocomplex.d (n + 1) (n + 1 + 1) ≫ g' ≫ J.cocomplex.d (n + 1) (n + 2)) =
    0
rw₃ :
  HAdd.hAdd (α := I.cocomplex.X (n + 1) ⟶ J.cocomplex.X (n + 1 + 1))
        ((I.cocomplex.d (n + 1) (n + 2) ≫ g') ≫ J.cocomplex.d (n + 1) (n + 1 + 1))
        (CategoryStruct.comp (Y := J.cocomplex.X (n + 1)) (g ≫ J.cocomplex.d n (n + 1))
          (J.cocomplex.d (n + 1) (n + 1 + 1))) -
      I.cocomplex.d (n + 1) (n + 1 + 1) ≫ g' ≫ J.cocomplex.d (n + 1) (n + 2) =
    0
⊢ Eq (α := I.cocomplex.X (n + 1) ⟶ J.cocomplex.X (n + 2))
    (I.cocomplex.d (n + 1) (n + 1 + 1) ≫ (f.f (n + 2) - g' ≫ J.cocomplex.d (n + 1) (n + 2))) 0
have rw₄ : HAdd.hAdd (α := I.cocomplex.X (n + 1) ⟶ J.cocomplex.X (n + 1 + 1))
      (I.cocomplex.d (n + 1) (n + 2) ≫ g' ≫ J.cocomplex.d (n + 1) (n + 1 + 1))
      (CategoryStruct.comp (Y := J.cocomplex.X (n + 1)) (g ≫ J.cocomplex.d n (n + 1))
        (J.cocomplex.d (n + 1) (n + 1 + 1))) -
    I.cocomplex.d (n + 1) (n + 1 + 1) ≫ g' ≫ J.cocomplex.d (n + 1) (n + 2) =
  0
Tactic: rw [Preadditive.comp_sub, ← HomologicalComplex.Hom.comm, w, Preadditive.add_comp,
        Category.assoc, Category.assoc, HomologicalComplex.d_comp_d, comp_zero,
        add_zero, sub_self]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Injective.Resolution (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
Y Z : C
I : InjectiveResolution.{v, u} Y
J : InjectiveResolution.{v, u} Z
f : I.cocomplex ⟶ J.cocomplex
n : ℕ
g : I.cocomplex.X (n + 1) ⟶ J.cocomplex.X n
g' : I.cocomplex.X (n + 2) ⟶ J.cocomplex.X (n + 1)
w : f.f (n + 1) = I.cocomplex.d (n + 1) (n + 2) ≫ g' + g ≫ J.cocomplex.d n (n + 1)
rw :
  HSub.hSub (α := I.cocomplex.X (n + 1) ⟶ J.cocomplex.X (n + 2)) (I.cocomplex.d (n + 1) (n + 1 + 1) ≫ f.f (n + 2))
      (I.cocomplex.d (n + 1) (n + 1 + 1) ≫ g' ≫ J.cocomplex.d (n + 1) (n + 2)) =
    0
rw₁ :
  HSub.hSub (α := I.cocomplex.X (n + 1) ⟶ J.cocomplex.X (n + 2)) (f.f (n + 1) ≫ J.cocomplex.d (n + 1) (n + 1 + 1))
      (I.cocomplex.d (n + 1) (n + 1 + 1) ≫ g' ≫ J.cocomplex.d (n + 1) (n + 2)) =
    0
rw₂ :
  HSub.hSub (α := I.cocomplex.X (n + 1) ⟶ J.cocomplex.X (n + 2))
      ((I.cocomplex.d (n + 1) (n + 2) ≫ g' + g ≫ J.cocomplex.d n (n + 1)) ≫ J.cocomplex.d (n + 1) (n + 1 + 1))
      (I.cocomplex.d (n + 1) (n + 1 + 1) ≫ g' ≫ J.cocomplex.d (n + 1) (n + 2)) =
    0
rw₃ :
  HAdd.hAdd (α := I.cocomplex.X (n + 1) ⟶ J.cocomplex.X (n + 1 + 1))
        ((I.cocomplex.d (n + 1) (n + 2) ≫ g') ≫ J.cocomplex.d (n + 1) (n + 1 + 1))
        (CategoryStruct.comp (Y := J.cocomplex.X (n + 1)) (g ≫ J.cocomplex.d n (n + 1))
          (J.cocomplex.d (n + 1) (n + 1 + 1))) -
      I.cocomplex.d (n + 1) (n + 1 + 1) ≫ g' ≫ J.cocomplex.d (n + 1) (n + 2) =
    0
rw₄ :
  HAdd.hAdd (α := I.cocomplex.X (n + 1) ⟶ J.cocomplex.X (n + 1 + 1))
        (I.cocomplex.d (n + 1) (n + 2) ≫ g' ≫ J.cocomplex.d (n + 1) (n + 1 + 1))
        (CategoryStruct.comp (Y := J.cocomplex.X (n + 1)) (g ≫ J.cocomplex.d n (n + 1))
          (J.cocomplex.d (n + 1) (n + 1 + 1))) -
      I.cocomplex.d (n + 1) (n + 1 + 1) ≫ g' ≫ J.cocomplex.d (n + 1) (n + 2) =
    0
⊢ Eq (α := I.cocomplex.X (n + 1) ⟶ J.cocomplex.X (n + 2))
    (I.cocomplex.d (n + 1) (n + 1 + 1) ≫ (f.f (n + 2) - g' ≫ J.cocomplex.d (n + 1) (n + 2))) 0
have rw₅ : HAdd.hAdd (α := I.cocomplex.X (n + 1) ⟶ J.cocomplex.X (n + 1 + 1))
      (I.cocomplex.d (n + 1) (n + 2) ≫ g' ≫ J.cocomplex.d (n + 1) (n + 1 + 1))
      (g ≫
        CategoryStruct.comp (Y := J.cocomplex.X (n + 1)) (J.cocomplex.d n (n + 1))
          (J.cocomplex.d (n + 1) (n + 1 + 1))) -
    I.cocomplex.d (n + 1) (n + 1 + 1) ≫ g' ≫ J.cocomplex.d (n + 1) (n + 2) =
  0
Tactic: rw [Preadditive.comp_sub, ← HomologicalComplex.Hom.comm, w, Preadditive.add_comp,
        Category.assoc, Category.assoc, HomologicalComplex.d_comp_d, comp_zero,
        add_zero, sub_self]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Injective.Resolution (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
Y Z : C
I : InjectiveResolution.{v, u} Y
J : InjectiveResolution.{v, u} Z
f : I.cocomplex ⟶ J.cocomplex
n : ℕ
g : I.cocomplex.X (n + 1) ⟶ J.cocomplex.X n
g' : I.cocomplex.X (n + 2) ⟶ J.cocomplex.X (n + 1)
w : f.f (n + 1) = I.cocomplex.d (n + 1) (n + 2) ≫ g' + g ≫ J.cocomplex.d n (n + 1)
rw :
  HSub.hSub (α := I.cocomplex.X (n + 1) ⟶ J.cocomplex.X (n + 2)) (I.cocomplex.d (n + 1) (n + 1 + 1) ≫ f.f (n + 2))
      (I.cocomplex.d (n + 1) (n + 1 + 1) ≫ g' ≫ J.cocomplex.d (n + 1) (n + 2)) =
    0
rw₁ :
  HSub.hSub (α := I.cocomplex.X (n + 1) ⟶ J.cocomplex.X (n + 2)) (f.f (n + 1) ≫ J.cocomplex.d (n + 1) (n + 1 + 1))
      (I.cocomplex.d (n + 1) (n + 1 + 1) ≫ g' ≫ J.cocomplex.d (n + 1) (n + 2)) =
    0
rw₂ :
  HSub.hSub (α := I.cocomplex.X (n + 1) ⟶ J.cocomplex.X (n + 2))
      ((I.cocomplex.d (n + 1) (n + 2) ≫ g' + g ≫ J.cocomplex.d n (n + 1)) ≫ J.cocomplex.d (n + 1) (n + 1 + 1))
      (I.cocomplex.d (n + 1) (n + 1 + 1) ≫ g' ≫ J.cocomplex.d (n + 1) (n + 2)) =
    0
rw₃ :
  HAdd.hAdd (α := I.cocomplex.X (n + 1) ⟶ J.cocomplex.X (n + 1 + 1))
        ((I.cocomplex.d (n + 1) (n + 2) ≫ g') ≫ J.cocomplex.d (n + 1) (n + 1 + 1))
        (CategoryStruct.comp (Y := J.cocomplex.X (n + 1)) (g ≫ J.cocomplex.d n (n + 1))
          (J.cocomplex.d (n + 1) (n + 1 + 1))) -
      I.cocomplex.d (n + 1) (n + 1 + 1) ≫ g' ≫ J.cocomplex.d (n + 1) (n + 2) =
    0
rw₄ :
  HAdd.hAdd (α := I.cocomplex.X (n + 1) ⟶ J.cocomplex.X (n + 1 + 1))
        (I.cocomplex.d (n + 1) (n + 2) ≫ g' ≫ J.cocomplex.d (n + 1) (n + 1 + 1))
        (CategoryStruct.comp (Y := J.cocomplex.X (n + 1)) (g ≫ J.cocomplex.d n (n + 1))
          (J.cocomplex.d (n + 1) (n + 1 + 1))) -
      I.cocomplex.d (n + 1) (n + 1 + 1) ≫ g' ≫ J.cocomplex.d (n + 1) (n + 2) =
    0
rw₅ :
  HAdd.hAdd (α := I.cocomplex.X (n + 1) ⟶ J.cocomplex.X (n + 1 + 1))
        (I.cocomplex.d (n + 1) (n + 2) ≫ g' ≫ J.cocomplex.d (n + 1) (n + 1 + 1))
        (g ≫
          CategoryStruct.comp (Y := J.cocomplex.X (n + 1)) (J.cocomplex.d n (n + 1))
            (J.cocomplex.d (n + 1) (n + 1 + 1))) -
      I.cocomplex.d (n + 1) (n + 1 + 1) ≫ g' ≫ J.cocomplex.d (n + 1) (n + 2) =
    0
⊢ Eq (α := I.cocomplex.X (n + 1) ⟶ J.cocomplex.X (n + 2))
    (I.cocomplex.d (n + 1) (n + 1 + 1) ≫ (f.f (n + 2) - g' ≫ J.cocomplex.d (n + 1) (n + 2))) 0
have rw₆ : HAdd.hAdd (α := I.cocomplex.X (n + 1) ⟶ J.cocomplex.X (n + 1 + 1))
      (I.cocomplex.d (n + 1) (n + 2) ≫ g' ≫ J.cocomplex.d (n + 1) (n + 1 + 1)) (g ≫ 0) -
    I.cocomplex.d (n + 1) (n + 1 + 1) ≫ g' ≫ J.cocomplex.d (n + 1) (n + 2) =
  0
Tactic: rw [Preadditive.comp_sub, ← HomologicalComplex.Hom.comm, w, Preadditive.add_comp,
        Category.assoc, Category.assoc, HomologicalComplex.d_comp_d, comp_zero,
        add_zero, sub_self]