awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.Additive (goal)
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
W : Type u_2
inst_2 : Category.{v_1, u_2} W
inst_3 : Preadditive.{v_1, u_2} W
W₁ : Type u_3
W₂ : Type u_4
inst_4 : Category.{v_2, u_3} W₁
inst_5 : Category.{v_3, u_4} W₂
inst_6 : HasZeroMorphisms.{v_2, u_3} W₁
inst_7 : HasZeroMorphisms.{v_3, u_4} W₂
c_1 : ComplexShape ι
C D : HomologicalComplex.{v, u, u_1} V c_1
f : C ⟶ D
i_1 : ι
inst_8 : HasZeroObject.{v_2, u_3} W₁
inst_9 : HasZeroObject.{v_3, u_4} W₂
F : CategoryTheory.Functor.{v_2, v_3, u_3, u_4} W₁ W₂
inst_10 : F.PreservesZeroMorphisms
c : ComplexShape ι
inst_11 : DecidableEq ι
j : ι
X : W₁
i : ι
pos :
  ∀ (h : i = j),
    Eq.{v_3 + 1} (α :=
      F.obj (HomologicalComplex.X.{v_2, u_3, u_1} (Functor.obj (single W₁ c j) X) i) ⟶
        F.obj (HomologicalComplex.X.{v_2, u_3, u_1} (Functor.obj (single W₁ c j) X) i))
      (CategoryStruct.comp (Y := HomologicalComplex.X.{v_3, u_4, u_1} (Functor.obj (single W₂ c j) (F.obj X)) i)
          (eqToHom ⋯) (eqToHom ⋯) :
        F.obj (HomologicalComplex.X.{v_2, u_3, u_1} (Functor.obj (single W₁ c j) X) i) ⟶
          F.obj (HomologicalComplex.X.{v_2, u_3, u_1} (Functor.obj (single W₁ c j) X) i))
      (𝟙 (F.obj (HomologicalComplex.X.{v_2, u_3, u_1} (Functor.obj (single W₁ c j) X) i)) :
        F.obj (HomologicalComplex.X.{v_2, u_3, u_1} (Functor.obj (single W₁ c j) X) i) ⟶
          F.obj (HomologicalComplex.X.{v_2, u_3, u_1} (Functor.obj (single W₁ c j) X) i))
⊢ Eq.{v_3 + 1} (α :=
    F.obj (HomologicalComplex.X.{v_2, u_3, u_1} (Functor.obj (single W₁ c j) X) i) ⟶
      F.obj (HomologicalComplex.X.{v_2, u_3, u_1} (Functor.obj (single W₁ c j) X) i))
    (CategoryStruct.comp (Y := HomologicalComplex.X.{v_3, u_4, u_1} (Functor.obj (single W₂ c j) (F.obj X)) i)
      (if h : i = j then eqToHom ⋯ else 0) (if h : i = j then eqToHom ⋯ else 0))
    (𝟙 (F.obj (HomologicalComplex.X.{v_2, u_3, u_1} (Functor.obj (single W₁ c j) X) i)))
have neg : ∀ (h : ¬i = j),
  Eq.{v_3 + 1} (α :=
    F.obj (HomologicalComplex.X.{v_2, u_3, u_1} (Functor.obj (single W₁ c j) X) i) ⟶
      F.obj (HomologicalComplex.X.{v_2, u_3, u_1} (Functor.obj (single W₁ c j) X) i))
    (CategoryStruct.comp (Y := HomologicalComplex.X.{v_3, u_4, u_1} (Functor.obj (single W₂ c j) (F.obj X)) i) 0 0)
    (𝟙 (F.obj (HomologicalComplex.X.{v_2, u_3, u_1} (Functor.obj (single W₁ c j) X) i)))
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Algebra.Homology.Additive (goal)
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
W : Type u_2
inst_2 : Category.{v_1, u_2} W
inst_3 : Preadditive.{v_1, u_2} W
W₁ : Type u_3
W₂ : Type u_4
inst_4 : Category.{v_2, u_3} W₁
inst_5 : Category.{v_3, u_4} W₂
inst_6 : HasZeroMorphisms.{v_2, u_3} W₁
inst_7 : HasZeroMorphisms.{v_3, u_4} W₂
c_1 : ComplexShape ι
C D : HomologicalComplex.{v, u, u_1} V c_1
f : C ⟶ D
i_1 : ι
inst_8 : HasZeroObject.{v_2, u_3} W₁
inst_9 : HasZeroObject.{v_3, u_4} W₂
F : CategoryTheory.Functor.{v_2, v_3, u_3, u_4} W₁ W₂
inst_10 : F.PreservesZeroMorphisms
c : ComplexShape ι
inst_11 : DecidableEq ι
j : ι
X : W₁
i : ι
h : ¬i = j
⊢ Eq.{v_3 + 1} (α :=
    F.obj (HomologicalComplex.X.{v_2, u_3, u_1} (Functor.obj (single W₁ c j) X) i) ⟶
      F.obj (HomologicalComplex.X.{v_2, u_3, u_1} (Functor.obj (single W₁ c j) X) i))
    (CategoryStruct.comp (Y := HomologicalComplex.X.{v_3, u_4, u_1} (Functor.obj (single W₂ c j) (F.obj X)) i) 0 0)
    (𝟙 (F.obj (HomologicalComplex.X.{v_2, u_3, u_1} (Functor.obj (single W₁ c j) X) i)))
have neg : Eq.{v_3 + 1} (α :=
  F.obj (HomologicalComplex.X.{v_2, u_3, u_1} (Functor.obj (single W₁ c j) X) i) ⟶
    F.obj (HomologicalComplex.X.{v_2, u_3, u_1} (Functor.obj (single W₁ c j) X) i))
  0 (𝟙 (F.obj (HomologicalComplex.X.{v_2, u_3, u_1} (Functor.obj (single W₁ c j) X) i)))
Tactic: rw [zero_comp, ← F.map_id,
              (isZero_single_obj_X c j X _ h).eq_of_src (𝟙 _) 0, F.map_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Additive (goal)
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
W : Type u_2
inst_2 : Category.{v_1, u_2} W
inst_3 : Preadditive.{v_1, u_2} W
W₁ : Type u_3
W₂ : Type u_4
inst_4 : Category.{v_2, u_3} W₁
inst_5 : Category.{v_3, u_4} W₂
inst_6 : HasZeroMorphisms.{v_2, u_3} W₁
inst_7 : HasZeroMorphisms.{v_3, u_4} W₂
c_1 : ComplexShape ι
C D : HomologicalComplex.{v, u, u_1} V c_1
f : C ⟶ D
i_1 : ι
inst_8 : HasZeroObject.{v_2, u_3} W₁
inst_9 : HasZeroObject.{v_3, u_4} W₂
F : CategoryTheory.Functor.{v_2, v_3, u_3, u_4} W₁ W₂
inst_10 : F.PreservesZeroMorphisms
c : ComplexShape ι
inst_11 : DecidableEq ι
j : ι
X : W₁
i : ι
h : ¬i = j
neg :
  Eq.{v_3 + 1} (α :=
    F.obj (HomologicalComplex.X.{v_2, u_3, u_1} (Functor.obj (single W₁ c j) X) i) ⟶
      F.obj (HomologicalComplex.X.{v_2, u_3, u_1} (Functor.obj (single W₁ c j) X) i))
    0 (𝟙 (F.obj (HomologicalComplex.X.{v_2, u_3, u_1} (Functor.obj (single W₁ c j) X) i)))
⊢ Eq.{v_3 + 1} (α :=
    F.obj (HomologicalComplex.X.{v_2, u_3, u_1} (Functor.obj (single W₁ c j) X) i) ⟶
      F.obj (HomologicalComplex.X.{v_2, u_3, u_1} (Functor.obj (single W₁ c j) X) i))
    (CategoryStruct.comp (Y := HomologicalComplex.X.{v_3, u_4, u_1} (Functor.obj (single W₂ c j) (F.obj X)) i) 0 0)
    (𝟙 (F.obj (HomologicalComplex.X.{v_2, u_3, u_1} (Functor.obj (single W₁ c j) X) i)))
have neg₁ : 0 = F.map (𝟙 (HomologicalComplex.X.{v_2, u_3, u_1} (Functor.obj (single W₁ c j) X) i))
Tactic: rw [zero_comp, ← F.map_id,
              (isZero_single_obj_X c j X _ h).eq_of_src (𝟙 _) 0, F.map_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Additive (goal)
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
W : Type u_2
inst_2 : Category.{v_1, u_2} W
inst_3 : Preadditive.{v_1, u_2} W
W₁ : Type u_3
W₂ : Type u_4
inst_4 : Category.{v_2, u_3} W₁
inst_5 : Category.{v_3, u_4} W₂
inst_6 : HasZeroMorphisms.{v_2, u_3} W₁
inst_7 : HasZeroMorphisms.{v_3, u_4} W₂
c_1 : ComplexShape ι
C D : HomologicalComplex.{v, u, u_1} V c_1
f : C ⟶ D
i_1 : ι
inst_8 : HasZeroObject.{v_2, u_3} W₁
inst_9 : HasZeroObject.{v_3, u_4} W₂
F : CategoryTheory.Functor.{v_2, v_3, u_3, u_4} W₁ W₂
inst_10 : F.PreservesZeroMorphisms
c : ComplexShape ι
inst_11 : DecidableEq ι
j : ι
X : W₁
i : ι
h : ¬i = j
neg :
  Eq.{v_3 + 1} (α :=
    F.obj (HomologicalComplex.X.{v_2, u_3, u_1} (Functor.obj (single W₁ c j) X) i) ⟶
      F.obj (HomologicalComplex.X.{v_2, u_3, u_1} (Functor.obj (single W₁ c j) X) i))
    0 (𝟙 (F.obj (HomologicalComplex.X.{v_2, u_3, u_1} (Functor.obj (single W₁ c j) X) i)))
neg₁ : 0 = F.map (𝟙 (HomologicalComplex.X.{v_2, u_3, u_1} (Functor.obj (single W₁ c j) X) i))
⊢ Eq.{v_3 + 1} (α :=
    F.obj (HomologicalComplex.X.{v_2, u_3, u_1} (Functor.obj (single W₁ c j) X) i) ⟶
      F.obj (HomologicalComplex.X.{v_2, u_3, u_1} (Functor.obj (single W₁ c j) X) i))
    (CategoryStruct.comp (Y := HomologicalComplex.X.{v_3, u_4, u_1} (Functor.obj (single W₂ c j) (F.obj X)) i) 0 0)
    (𝟙 (F.obj (HomologicalComplex.X.{v_2, u_3, u_1} (Functor.obj (single W₁ c j) X) i)))
have neg₂ : Eq (α :=
  F.obj (HomologicalComplex.X.{v_2, u_3, u_1} (Functor.obj (single W₁ c j) X) i) ⟶
    F.obj (HomologicalComplex.X.{v_2, u_3, u_1} (Functor.obj (single W₁ c j) X) i))
  0 (F.map 0)
Tactic: rw [zero_comp, ← F.map_id,
              (isZero_single_obj_X c j X _ h).eq_of_src (𝟙 _) 0, F.map_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Additive (goal)
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
W : Type u_2
inst_2 : Category.{v_1, u_2} W
inst_3 : Preadditive.{v_1, u_2} W
W₁ : Type u_3
W₂ : Type u_4
inst_4 : Category.{v_2, u_3} W₁
inst_5 : Category.{v_3, u_4} W₂
inst_6 : HasZeroMorphisms.{v_2, u_3} W₁
inst_7 : HasZeroMorphisms.{v_3, u_4} W₂
c_1 : ComplexShape ι
C D : HomologicalComplex.{v, u, u_1} V c_1
f : C ⟶ D
i_1 : ι
inst_8 : HasZeroObject.{v_2, u_3} W₁
inst_9 : HasZeroObject.{v_3, u_4} W₂
F : CategoryTheory.Functor.{v_2, v_3, u_3, u_4} W₁ W₂
inst_10 : F.PreservesZeroMorphisms
c : ComplexShape ι
inst_11 : DecidableEq ι
j : ι
X : W₁
i : ι
h : ¬i = j
neg :
  Eq.{v_3 + 1} (α :=
    F.obj (HomologicalComplex.X.{v_2, u_3, u_1} (Functor.obj (single W₁ c j) X) i) ⟶
      F.obj (HomologicalComplex.X.{v_2, u_3, u_1} (Functor.obj (single W₁ c j) X) i))
    0 (𝟙 (F.obj (HomologicalComplex.X.{v_2, u_3, u_1} (Functor.obj (single W₁ c j) X) i)))
neg₁ : 0 = F.map (𝟙 (HomologicalComplex.X.{v_2, u_3, u_1} (Functor.obj (single W₁ c j) X) i))
neg₂ :
  Eq (α :=
    F.obj (HomologicalComplex.X.{v_2, u_3, u_1} (Functor.obj (single W₁ c j) X) i) ⟶
      F.obj (HomologicalComplex.X.{v_2, u_3, u_1} (Functor.obj (single W₁ c j) X) i))
    0 (F.map 0)
⊢ Eq.{v_3 + 1} (α :=
    F.obj (HomologicalComplex.X.{v_2, u_3, u_1} (Functor.obj (single W₁ c j) X) i) ⟶
      F.obj (HomologicalComplex.X.{v_2, u_3, u_1} (Functor.obj (single W₁ c j) X) i))
    (CategoryStruct.comp (Y := HomologicalComplex.X.{v_3, u_4, u_1} (Functor.obj (single W₂ c j) (F.obj X)) i) 0 0)
    (𝟙 (F.obj (HomologicalComplex.X.{v_2, u_3, u_1} (Functor.obj (single W₁ c j) X) i)))
have neg₃ : Eq.{v_3 + 1} (α :=
  F.obj (HomologicalComplex.X.{v_2, u_3, u_1} (Functor.obj (single W₁ c j) X) i) ⟶
    F.obj (HomologicalComplex.X.{v_2, u_3, u_1} (Functor.obj (single W₁ c j) X) i))
  0 0
Tactic: rw [zero_comp, ← F.map_id,
              (isZero_single_obj_X c j X _ h).eq_of_src (𝟙 _) 0, F.map_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Additive (goal)
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
W : Type u_2
inst_2 : Category.{v_1, u_2} W
inst_3 : Preadditive.{v_1, u_2} W
W₁ : Type u_3
W₂ : Type u_4
inst_4 : Category.{v_2, u_3} W₁
inst_5 : Category.{v_3, u_4} W₂
inst_6 : HasZeroMorphisms.{v_2, u_3} W₁
inst_7 : HasZeroMorphisms.{v_3, u_4} W₂
c_1 : ComplexShape ι
C D : HomologicalComplex.{v, u, u_1} V c_1
f : C ⟶ D
i : ι
inst_8 : HasZeroObject.{v_2, u_3} W₁
inst_9 : HasZeroObject.{v_3, u_4} W₂
F : CategoryTheory.Functor.{v_2, v_3, u_3, u_4} W₁ W₂
inst_10 : F.PreservesZeroMorphisms
c : ComplexShape ι
inst_11 : DecidableEq ι
j : ι
X : W₁
⊢ Eq (α :=
    Quiver.Hom (V := HomologicalComplex.{v_3, u_4, u_1} W₂ c) (Functor.obj (F ⋙ single W₂ c j) X)
      (Functor.obj (F ⋙ single W₂ c j) X))
    (CategoryStruct.comp (Y :=
      Functor.obj
        (Functor.comp (D := HomologicalComplex.{v_2, u_3, u_1} W₁ c) (single W₁ c j) (F.mapHomologicalComplex c)) X)
      { f := fun (i : ι) ↦ if h : i = j then eqToHom ⋯ else 0, comm' := ⋯ }
      { f := fun (i : ι) ↦ if h : i = j then eqToHom ⋯ else 0, comm' := ⋯ })
    (𝟙 (Functor.obj (F ⋙ single W₂ c j) X))
have h : ∀ (i : ι),
  Eq (α :=
    HomologicalComplex.X (Functor.obj (F ⋙ single W₂ c j) X) i ⟶
      HomologicalComplex.X (Functor.obj (F ⋙ single W₂ c j) X) i)
    (Hom.f
      (CategoryStruct.comp (Y :=
        Functor.obj
          (Functor.comp (D := HomologicalComplex.{v_2, u_3, u_1} W₁ c) (single W₁ c j) (F.mapHomologicalComplex c)) X)
        { f := fun (i : ι) ↦ if h : i = j then eqToHom sorry else 0, comm' := sorry }
        { f := fun (i : ι) ↦ if h : i = j then eqToHom sorry else 0, comm' := sorry })
      i)
    (Hom.f (𝟙 (Functor.obj (F ⋙ single W₂ c j) X)) i)
Tactic: ext i
-- Lean 4 proof step from Mathlib.Algebra.Homology.Additive (goal)
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
W : Type u_2
inst_2 : Category.{v_1, u_2} W
inst_3 : Preadditive.{v_1, u_2} W
W₁ : Type u_3
W₂ : Type u_4
inst_4 : Category.{v_2, u_3} W₁
inst_5 : Category.{v_3, u_4} W₂
inst_6 : HasZeroMorphisms.{v_2, u_3} W₁
inst_7 : HasZeroMorphisms.{v_3, u_4} W₂
c_1 : ComplexShape ι
C D : HomologicalComplex.{v, u, u_1} V c_1
f : C ⟶ D
i_1 : ι
inst_8 : HasZeroObject.{v_2, u_3} W₁
inst_9 : HasZeroObject.{v_3, u_4} W₂
F : CategoryTheory.Functor.{v_2, v_3, u_3, u_4} W₁ W₂
inst_10 : F.PreservesZeroMorphisms
c : ComplexShape ι
inst_11 : DecidableEq ι
j : ι
X : W₁
i : ι
⊢ Eq (α :=
    HomologicalComplex.X (Functor.obj (F ⋙ single W₂ c j) X) i ⟶
      HomologicalComplex.X (Functor.obj (F ⋙ single W₂ c j) X) i)
    (Hom.f
      (CategoryStruct.comp (Y :=
        Functor.obj
          (Functor.comp (D := HomologicalComplex.{v_2, u_3, u_1} W₁ c) (single W₁ c j) (F.mapHomologicalComplex c)) X)
        { f := fun (i : ι) ↦ if h : i = j then eqToHom ⋯ else 0, comm' := ⋯ }
        { f := fun (i : ι) ↦ if h : i = j then eqToHom ⋯ else 0, comm' := ⋯ })
      i)
    (Hom.f (𝟙 (Functor.obj (F ⋙ single W₂ c j) X)) i)
have h : Eq.{v_3 + 1} (α :=
  HomologicalComplex.X.{v_3, u_4, u_1} (Functor.obj (single W₂ c j) (F.obj X)) i ⟶
    HomologicalComplex.X.{v_3, u_4, u_1} (Functor.obj (single W₂ c j) (F.obj X)) i)
  (CategoryStruct.comp (Y := F.obj (HomologicalComplex.X.{v_2, u_3, u_1} (Functor.obj (single W₁ c j) X) i))
    (if h : i = j then eqToHom sorry else 0) (if h : i = j then eqToHom sorry else 0))
  (𝟙 (HomologicalComplex.X.{v_3, u_4, u_1} (Functor.obj (single W₂ c j) (F.obj X)) i))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Homology.Additive (goal)
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
W : Type u_2
inst_2 : Category.{v_1, u_2} W
inst_3 : Preadditive.{v_1, u_2} W
W₁ : Type u_3
W₂ : Type u_4
inst_4 : Category.{v_2, u_3} W₁
inst_5 : Category.{v_3, u_4} W₂
inst_6 : HasZeroMorphisms.{v_2, u_3} W₁
inst_7 : HasZeroMorphisms.{v_3, u_4} W₂
c_1 : ComplexShape ι
C D : HomologicalComplex.{v, u, u_1} V c_1
f : C ⟶ D
i_1 : ι
inst_8 : HasZeroObject.{v_2, u_3} W₁
inst_9 : HasZeroObject.{v_3, u_4} W₂
F : CategoryTheory.Functor.{v_2, v_3, u_3, u_4} W₁ W₂
inst_10 : F.PreservesZeroMorphisms
c : ComplexShape ι
inst_11 : DecidableEq ι
j : ι
X : W₁
i : ι
⊢ Eq.{v_3 + 1} (α :=
    HomologicalComplex.X.{v_3, u_4, u_1} (Functor.obj (single W₂ c j) (F.obj X)) i ⟶
      HomologicalComplex.X.{v_3, u_4, u_1} (Functor.obj (single W₂ c j) (F.obj X)) i)
    (CategoryStruct.comp (Y := F.obj (HomologicalComplex.X.{v_2, u_3, u_1} (Functor.obj (single W₁ c j) X) i))
      (if h : i = j then eqToHom ⋯ else 0) (if h : i = j then eqToHom ⋯ else 0))
    (𝟙 (HomologicalComplex.X.{v_3, u_4, u_1} (Functor.obj (single W₂ c j) (F.obj X)) i))
have pos : ∀ (h : i = j),
  Eq.{v_3 + 1} (α :=
    HomologicalComplex.X.{v_3, u_4, u_1} (Functor.obj (single W₂ c j) (F.obj X)) i ⟶
      HomologicalComplex.X.{v_3, u_4, u_1} (Functor.obj (single W₂ c j) (F.obj X)) i)
    (CategoryStruct.comp (Y := F.obj (HomologicalComplex.X.{v_2, u_3, u_1} (Functor.obj (single W₁ c j) X) i))
      (eqToHom sorry :
        HomologicalComplex.X.{v_3, u_4, u_1} (Functor.obj (single W₂ c j) (F.obj X)) i ⟶
          F.obj (HomologicalComplex.X.{v_2, u_3, u_1} (Functor.obj (single W₁ c j) X) i))
      (eqToHom sorry :
        F.obj (HomologicalComplex.X.{v_2, u_3, u_1} (Functor.obj (single W₁ c j) X) i) ⟶
          HomologicalComplex.X.{v_3, u_4, u_1} (Functor.obj (single W₂ c j) (F.obj X)) i))
    (𝟙 (HomologicalComplex.X.{v_3, u_4, u_1} (Functor.obj (single W₂ c j) (F.obj X)) i))
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Algebra.Homology.Additive (goal)
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
W : Type u_2
inst_2 : Category.{v_1, u_2} W
inst_3 : Preadditive.{v_1, u_2} W
W₁ : Type u_3
W₂ : Type u_4
inst_4 : Category.{v_2, u_3} W₁
inst_5 : Category.{v_3, u_4} W₂
inst_6 : HasZeroMorphisms.{v_2, u_3} W₁
inst_7 : HasZeroMorphisms.{v_3, u_4} W₂
c_1 : ComplexShape ι
C D : HomologicalComplex.{v, u, u_1} V c_1
f : C ⟶ D
i_1 : ι
inst_8 : HasZeroObject.{v_2, u_3} W₁
inst_9 : HasZeroObject.{v_3, u_4} W₂
F : CategoryTheory.Functor.{v_2, v_3, u_3, u_4} W₁ W₂
inst_10 : F.PreservesZeroMorphisms
c : ComplexShape ι
inst_11 : DecidableEq ι
j : ι
X : W₁
i : ι
pos :
  ∀ (h : i = j),
    Eq.{v_3 + 1} (α :=
      HomologicalComplex.X.{v_3, u_4, u_1} (Functor.obj (single W₂ c j) (F.obj X)) i ⟶
        HomologicalComplex.X.{v_3, u_4, u_1} (Functor.obj (single W₂ c j) (F.obj X)) i)
      (CategoryStruct.comp (Y := F.obj (HomologicalComplex.X.{v_2, u_3, u_1} (Functor.obj (single W₁ c j) X) i))
        (eqToHom ⋯ :
          HomologicalComplex.X.{v_3, u_4, u_1} (Functor.obj (single W₂ c j) (F.obj X)) i ⟶
            F.obj (HomologicalComplex.X.{v_2, u_3, u_1} (Functor.obj (single W₁ c j) X) i))
        (eqToHom ⋯ :
          F.obj (HomologicalComplex.X.{v_2, u_3, u_1} (Functor.obj (single W₁ c j) X) i) ⟶
            HomologicalComplex.X.{v_3, u_4, u_1} (Functor.obj (single W₂ c j) (F.obj X)) i))
      (𝟙 (HomologicalComplex.X.{v_3, u_4, u_1} (Functor.obj (single W₂ c j) (F.obj X)) i))
⊢ Eq.{v_3 + 1} (α :=
    HomologicalComplex.X.{v_3, u_4, u_1} (Functor.obj (single W₂ c j) (F.obj X)) i ⟶
      HomologicalComplex.X.{v_3, u_4, u_1} (Functor.obj (single W₂ c j) (F.obj X)) i)
    (CategoryStruct.comp (Y := F.obj (HomologicalComplex.X.{v_2, u_3, u_1} (Functor.obj (single W₁ c j) X) i))
      (if h : i = j then eqToHom ⋯ else 0) (if h : i = j then eqToHom ⋯ else 0))
    (𝟙 (HomologicalComplex.X.{v_3, u_4, u_1} (Functor.obj (single W₂ c j) (F.obj X)) i))
have neg : ∀ (h : ¬i = j),
  Eq.{v_3 + 1} (α :=
    HomologicalComplex.X.{v_3, u_4, u_1} (Functor.obj (single W₂ c j) (F.obj X)) i ⟶
      HomologicalComplex.X.{v_3, u_4, u_1} (Functor.obj (single W₂ c j) (F.obj X)) i)
    (CategoryStruct.comp (Y := F.obj (HomologicalComplex.X.{v_2, u_3, u_1} (Functor.obj (single W₁ c j) X) i)) 0 0)
    (𝟙 (HomologicalComplex.X.{v_3, u_4, u_1} (Functor.obj (single W₂ c j) (F.obj X)) i))
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Algebra.Homology.Additive (goal)
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
W : Type u_2
inst_2 : Category.{v_1, u_2} W
inst_3 : Preadditive.{v_1, u_2} W
W₁ : Type u_3
W₂ : Type u_4
inst_4 : Category.{v_2, u_3} W₁
inst_5 : Category.{v_3, u_4} W₂
inst_6 : HasZeroMorphisms.{v_2, u_3} W₁
inst_7 : HasZeroMorphisms.{v_3, u_4} W₂
c_1 : ComplexShape ι
C D : HomologicalComplex.{v, u, u_1} V c_1
f_1 : C ⟶ D
i_1 : ι
inst_8 : HasZeroObject.{v_2, u_3} W₁
inst_9 : HasZeroObject.{v_3, u_4} W₂
F : CategoryTheory.Functor.{v_2, v_3, u_3, u_4} W₁ W₂
inst_10 : F.PreservesZeroMorphisms
c : ComplexShape ι
inst_11 : DecidableEq ι
j : ι
X Y : W₁
f : X ⟶ Y
i : ι
⊢ Eq (α :=
    HomologicalComplex.X
        (Functor.obj
          (Functor.comp (D := HomologicalComplex.{v_2, u_3, u_1} W₁ c) (single W₁ c j) (F.mapHomologicalComplex c)) X)
        i ⟶
      HomologicalComplex.X (Functor.obj (F ⋙ single W₂ c j) Y) i)
    (Hom.f
      (CategoryTheory.Functor.map
          (Functor.comp (D := HomologicalComplex.{v_2, u_3, u_1} W₁ c) (single W₁ c j) (F.mapHomologicalComplex c)) f ≫
        Iso.hom
          ((fun (X : W₁) ↦
              ({ hom := { f := fun (i : ι) ↦ if h : i = j then eqToHom ⋯ else 0, comm' := ⋯ },
                  inv := { f := fun (i : ι) ↦ if h : i = j then eqToHom ⋯ else 0, comm' := ⋯ }, hom_inv_id := ⋯,
                  inv_hom_id := ⋯ } :
                Iso (C := HomologicalComplex.{v_3, u_4, u_1} W₂ c)
                  (Functor.obj
                    (Functor.comp (D := HomologicalComplex.{v_2, u_3, u_1} W₁ c) (single W₁ c j)
                      (F.mapHomologicalComplex c))
                    X)
                  (Functor.obj (F ⋙ single W₂ c j) X)))
            Y))
      i)
    (Hom.f
      (Iso.hom
          ((fun (X : W₁) ↦
              ({ hom := { f := fun (i : ι) ↦ if h : i = j then eqToHom ⋯ else 0, comm' := ⋯ },
                  inv := { f := fun (i : ι) ↦ if h : i = j then eqToHom ⋯ else 0, comm' := ⋯ }, hom_inv_id := ⋯,
                  inv_hom_id := ⋯ } :
                Iso (C := HomologicalComplex.{v_3, u_4, u_1} W₂ c)
                  (Functor.obj
                    (Functor.comp (D := HomologicalComplex.{v_2, u_3, u_1} W₁ c) (single W₁ c j)
                      (F.mapHomologicalComplex c))
                    X)
                  (Functor.obj (F ⋙ single W₂ c j) X)))
            X) ≫
        CategoryTheory.Functor.map (F ⋙ single W₂ c j) f)
      i)
have h : Eq (α :=
  F.obj (HomologicalComplex.X.{v_2, u_3, u_1} (Functor.obj (single W₁ c j) X) i) ⟶
    HomologicalComplex.X.{v_3, u_4, u_1} (Functor.obj (single W₂ c j) (F.obj Y)) i)
  (F.map (Hom.f (CategoryTheory.Functor.map (single W₁ c j) f) i) ≫ if h : i = j then eqToHom sorry else 0)
  ((if h : i = j then eqToHom sorry else 0) ≫ Hom.f (CategoryTheory.Functor.map (single W₂ c j) (F.map f)) i)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Homology.Additive (goal)
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
W : Type u_2
inst_2 : Category.{v_1, u_2} W
inst_3 : Preadditive.{v_1, u_2} W
W₁ : Type u_3
W₂ : Type u_4
inst_4 : Category.{v_2, u_3} W₁
inst_5 : Category.{v_3, u_4} W₂
inst_6 : HasZeroMorphisms.{v_2, u_3} W₁
inst_7 : HasZeroMorphisms.{v_3, u_4} W₂
c_1 : ComplexShape ι
C D : HomologicalComplex.{v, u, u_1} V c_1
f_1 : C ⟶ D
i_1 : ι
inst_8 : HasZeroObject.{v_2, u_3} W₁
inst_9 : HasZeroObject.{v_3, u_4} W₂
F : CategoryTheory.Functor.{v_2, v_3, u_3, u_4} W₁ W₂
inst_10 : F.PreservesZeroMorphisms
c : ComplexShape ι
inst_11 : DecidableEq ι
j : ι
X Y : W₁
f : X ⟶ Y
i : ι
⊢ Eq (α :=
    F.obj (HomologicalComplex.X.{v_2, u_3, u_1} (Functor.obj (single W₁ c j) X) i) ⟶
      HomologicalComplex.X.{v_3, u_4, u_1} (Functor.obj (single W₂ c j) (F.obj Y)) i)
    (F.map (Hom.f (CategoryTheory.Functor.map (single W₁ c j) f) i) ≫ if h : i = j then eqToHom ⋯ else 0)
    ((if h : i = j then eqToHom ⋯ else 0) ≫ Hom.f (CategoryTheory.Functor.map (single W₂ c j) (F.map f)) i)
have pos : ∀ (h : i = j),
  Eq (α :=
    F.obj (HomologicalComplex.X.{v_2, u_3, u_1} (Functor.obj (single W₁ c j) X) i) ⟶
      HomologicalComplex.X.{v_3, u_4, u_1} (Functor.obj (single W₂ c j) (F.obj Y)) i)
    (F.map (Hom.f (CategoryTheory.Functor.map (single W₁ c j) f) i) ≫ eqToHom sorry)
    (CategoryStruct.comp (Y := HomologicalComplex.X.{v_3, u_4, u_1} (Functor.obj (single W₂ c j) (F.obj X)) i)
      (eqToHom sorry) (Hom.f (CategoryTheory.Functor.map (single W₂ c j) (F.map f)) i))
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Algebra.Homology.Additive (goal)
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
W : Type u_2
inst_2 : Category.{v_1, u_2} W
inst_3 : Preadditive.{v_1, u_2} W
W₁ : Type u_3
W₂ : Type u_4
inst_4 : Category.{v_2, u_3} W₁
inst_5 : Category.{v_3, u_4} W₂
inst_6 : HasZeroMorphisms.{v_2, u_3} W₁
inst_7 : HasZeroMorphisms.{v_3, u_4} W₂
c_1 : ComplexShape ι
C D : HomologicalComplex.{v, u, u_1} V c_1
f_1 : C ⟶ D
i_1 : ι
inst_8 : HasZeroObject.{v_2, u_3} W₁
inst_9 : HasZeroObject.{v_3, u_4} W₂
F : CategoryTheory.Functor.{v_2, v_3, u_3, u_4} W₁ W₂
inst_10 : F.PreservesZeroMorphisms
c : ComplexShape ι
inst_11 : DecidableEq ι
j : ι
X Y : W₁
f : X ⟶ Y
i : ι
pos :
  ∀ (h : i = j),
    Eq (α :=
      F.obj (HomologicalComplex.X.{v_2, u_3, u_1} (Functor.obj (single W₁ c j) X) i) ⟶
        HomologicalComplex.X.{v_3, u_4, u_1} (Functor.obj (single W₂ c j) (F.obj Y)) i)
      (F.map (Hom.f (CategoryTheory.Functor.map (single W₁ c j) f) i) ≫ eqToHom ⋯)
      (CategoryStruct.comp (Y := HomologicalComplex.X.{v_3, u_4, u_1} (Functor.obj (single W₂ c j) (F.obj X)) i)
        (eqToHom ⋯) (Hom.f (CategoryTheory.Functor.map (single W₂ c j) (F.map f)) i))
⊢ Eq (α :=
    F.obj (HomologicalComplex.X.{v_2, u_3, u_1} (Functor.obj (single W₁ c j) X) i) ⟶
      HomologicalComplex.X.{v_3, u_4, u_1} (Functor.obj (single W₂ c j) (F.obj Y)) i)
    (F.map (Hom.f (CategoryTheory.Functor.map (single W₁ c j) f) i) ≫ if h : i = j then eqToHom ⋯ else 0)
    ((if h : i = j then eqToHom ⋯ else 0) ≫ Hom.f (CategoryTheory.Functor.map (single W₂ c j) (F.map f)) i)
have neg : ∀ (h : ¬i = j),
  Eq (α :=
    F.obj (HomologicalComplex.X.{v_2, u_3, u_1} (Functor.obj (single W₁ c j) X) i) ⟶
      HomologicalComplex.X.{v_3, u_4, u_1} (Functor.obj (single W₂ c j) (F.obj Y)) i)
    (F.map (Hom.f (CategoryTheory.Functor.map (single W₁ c j) f) i) ≫ 0)
    (0 ≫ Hom.f (CategoryTheory.Functor.map (single W₂ c j) (F.map f)) i)
Tactic: split_ifs with h