awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.Additive
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))
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)))
⊢ 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)))

Tactic:
split_ifs with h
-- Module: Mathlib.Algebra.Homology.Additive
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)
        (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))

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.Additive
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)
neg₃ 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
⊢ 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:
rw [zero_comp, ← F.map_id,
              (isZero_single_obj_X c j X _ h).eq_of_src (𝟙 _) 0, F.map_zero]

Premises used: HomologicalComplex.isZero_single_obj_X, CategoryTheory.Functor.map_zero, CategoryTheory.CategoryStruct.id, CategoryTheory.Functor.map_id, CategoryTheory.Limits.IsZero.eq_of_src, CategoryTheory.Limits.zero_comp, OfNat.ofNat
-- Module: Mathlib.Algebra.Homology.Additive
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₁
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 ⋯ 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)
⊢ 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))

Tactic:
ext i
-- Module: Mathlib.Algebra.Homology.Additive
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 :
  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))
⊢ 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)

Tactic:
dsimp
-- Module: Mathlib.Algebra.Homology.Additive
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))
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))
⊢ 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))

Tactic:
split_ifs with h
-- Module: Mathlib.Algebra.Homology.Additive
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} (α :=
    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))

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.Additive
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} (α :=
    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:
apply (isZero_single_obj_X c j _ _ h).eq_of_src

Premises used: HomologicalComplex.isZero_single_obj_X, CategoryTheory.Limits.IsZero.eq_of_src
-- Module: Mathlib.Algebra.Homology.Additive
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 : ι
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 ⋯ else 0)
    ((if h : i = j then eqToHom ⋯ else 0) ≫ Hom.f (CategoryTheory.Functor.map (single W₂ c j) (F.map f)) 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)

Tactic:
dsimp
-- Module: Mathlib.Algebra.Homology.Additive
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))
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)
⊢ 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)

Tactic:
split_ifs with h
-- Module: Mathlib.Algebra.Homology.Additive
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 : ι
h : i = j
pos :
  Eq (α :=
    F.obj (HomologicalComplex.X.{v_2, u_3, u_1} (Functor.obj (single W₁ c i) X) i) ⟶
      HomologicalComplex.X.{v_3, u_4, u_1} (Functor.obj (single W₂ c i) (F.obj Y)) i)
    (F.map (Hom.f (CategoryTheory.Functor.map (single W₁ c i) f) i) ≫ eqToHom ⋯)
    (CategoryStruct.comp (Y := HomologicalComplex.X.{v_3, u_4, u_1} (Functor.obj (single W₂ c i) (F.obj X)) i)
      (eqToHom ⋯) (Hom.f (CategoryTheory.Functor.map (single W₂ c i) (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) ≫ 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))

Tactic:
subst h
-- Module: Mathlib.Algebra.Homology.Additive
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 ι
X Y : W₁
f : X ⟶ Y
i : ι
⊢ Eq (α :=
    F.obj (HomologicalComplex.X.{v_2, u_3, u_1} (Functor.obj (single W₁ c i) X) i) ⟶
      HomologicalComplex.X.{v_3, u_4, u_1} (Functor.obj (single W₂ c i) (F.obj Y)) i)
    (F.map (Hom.f (CategoryTheory.Functor.map (single W₁ c i) f) i) ≫ eqToHom ⋯)
    (CategoryStruct.comp (Y := HomologicalComplex.X.{v_3, u_4, u_1} (Functor.obj (single W₂ c i) (F.obj X)) i)
      (eqToHom ⋯) (Hom.f (CategoryTheory.Functor.map (single W₂ c i) (F.map f)) i))

Tactic:
simp [single_map_f_self, singleObjXSelf, singleObjXIsoOfEq, eqToHom_map]

Premises used: CategoryTheory.eqToHom_map, HomologicalComplex.singleObjXIsoOfEq, HomologicalComplex.single_map_f_self, HomologicalComplex.singleObjXSelf
-- Module: Mathlib.Algebra.Homology.Additive
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 : ι
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:
apply (isZero_single_obj_X c j _ _ h).eq_of_tgt

Premises used: HomologicalComplex.isZero_single_obj_X, CategoryTheory.Limits.IsZero.eq_of_tgt