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_1 : C ⟶ D
i : ι
F : Functor.{v_2, v_3, u_3, u_4} W₁ W₂
inst_8 : F.PreservesZeroMorphisms
inst_9 : F.ReflectsIsomorphisms
c : ComplexShape ι
A B : HomologicalComplex.{v_2, u_3, u_1} W₁ c
f : A ⟶ B
inst_10 :
  IsIso (C := HomologicalComplex.{v_3, u_4, u_1} W₂ c) (X := obj (F.mapHomologicalComplex c) A)
    (map (F.mapHomologicalComplex c) f)
⊢ ∀ (n : ι), IsIso (F.map (f.f n))

Tactic:
haveI : ∀ n : ι, IsIso (F.map (f.f n)) := fun n =>
        ((HomologicalComplex.eval W₂ c n).mapIso
          (asIso ((F.mapHomologicalComplex c).map f))).isIso_hom
-- 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 : ι
F : Functor.{v_2, v_3, u_3, u_4} W₁ W₂
inst_8 : F.PreservesZeroMorphisms
inst_9 : F.ReflectsIsomorphisms
c : ComplexShape ι
A B : HomologicalComplex.{v_2, u_3, u_1} W₁ c
f : A ⟶ B
inst_10 :
  IsIso (C := HomologicalComplex.{v_3, u_4, u_1} W₂ c) (X := obj (F.mapHomologicalComplex c) A)
    (map (F.mapHomologicalComplex c) f)
this : ∀ (n : ι), IsIso (F.map (f.f n))
⊢ ∀ (n : ι), IsIso (f.f n)

Tactic:
haveI := fun n => isIso_of_reflects_iso (f.f n) F
-- 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 : ι
F : Functor.{v_2, v_3, u_3, u_4} W₁ W₂
inst_8 : F.PreservesZeroMorphisms
inst_9 : F.ReflectsIsomorphisms
c : ComplexShape ι
A B : HomologicalComplex.{v_2, u_3, u_1} W₁ c
f : A ⟶ B
inst_10 :
  IsIso (C := HomologicalComplex.{v_3, u_4, u_1} W₂ c) (X := obj (F.mapHomologicalComplex c) A)
    (map (F.mapHomologicalComplex c) f)
this_1 : ∀ (n : ι), IsIso (F.map (f.f n))
this : ∀ (n : ι), IsIso (f.f n)
⊢ IsIso f

Tactic:
HomologicalComplex.Hom.isIso_of_components f

Premises used: HomologicalComplex.Hom.isIso_of_components
-- 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 : ι
F : Functor.{v_2, v_3, u_3, u_4} W₁ W₂
inst_8 : F.PreservesZeroMorphisms
inst_9 : F.ReflectsIsomorphisms
c : ComplexShape ι
A B : HomologicalComplex.{v_2, u_3, u_1} W₁ c
f : A ⟶ B
inst_10 :
  IsIso (C := HomologicalComplex.{v_3, u_4, u_1} W₂ c) (X := obj (F.mapHomologicalComplex c) A)
    (map (F.mapHomologicalComplex c) f)
this_1 : ∀ (n : ι), IsIso (F.map (f.f n))
this : ∀ (n : ι), IsIso (f.f n)
⊢ IsIso f

Tactic:
exact HomologicalComplex.Hom.isIso_of_components f

Premises used: HomologicalComplex.Hom.isIso_of_components
-- Module: Mathlib.Algebra.Homology.Additive
Goal:
ι : Type u_1
W₁ : Type u_3
W₂ : Type u_4
inst : Category.{v_2, u_3} W₁
inst_1 : Category.{v_3, u_4} W₂
inst_2 : HasZeroMorphisms.{v_2, u_3} W₁
inst_3 : HasZeroMorphisms.{v_3, u_4} W₂
c : ComplexShape ι
F : Functor.{v_2, v_3, u_3, u_4} W₁ W₂
inst_4 : F.PreservesZeroMorphisms
cat_disch cat_disch₁ cat_disch₂ cat_disch₃ :
  Eq (α :=
    Quiver.Hom (V := HomologicalComplex.{v_2, u_3, u_1} W₁ c ⥤ HomologicalComplex.{v_3, u_4, u_1} W₂ c)
      (F.mapHomologicalComplex c) (F.mapHomologicalComplex c))
    (mapHomologicalComplex (𝟙 F) c) (𝟙 (F.mapHomologicalComplex c))
⊢ Eq (α :=
    Quiver.Hom (V := HomologicalComplex.{v_2, u_3, u_1} W₁ c ⥤ HomologicalComplex.{v_3, u_4, u_1} W₂ c)
      (F.mapHomologicalComplex c) (F.mapHomologicalComplex c))
    (mapHomologicalComplex (𝟙 F) c) (𝟙 (F.mapHomologicalComplex c))

Tactic:
cat_disch
-- Module: Mathlib.Algebra.Homology.Additive
Goal:
ι : Type u_1
W₁ : Type u_3
W₂ : Type u_4
inst : Category.{v_2, u_3} W₁
inst_1 : Category.{v_3, u_4} W₂
inst_2 : HasZeroMorphisms.{v_2, u_3} W₁
inst_3 : HasZeroMorphisms.{v_3, u_4} W₂
c : ComplexShape ι
F G H : Functor.{v_2, v_3, u_3, u_4} W₁ W₂
inst_4 : F.PreservesZeroMorphisms
inst_5 : G.PreservesZeroMorphisms
inst_6 : H.PreservesZeroMorphisms
α : F ⟶ G
β : G ⟶ H
cat_disch cat_disch₁ cat_disch₂ cat_disch₃ :
  Eq (α :=
    Quiver.Hom (V := HomologicalComplex.{v_2, u_3, u_1} W₁ c ⥤ HomologicalComplex.{v_3, u_4, u_1} W₂ c)
      (F.mapHomologicalComplex c) (H.mapHomologicalComplex c))
    (mapHomologicalComplex (α ≫ β) c)
    (CategoryStruct.comp (Y := G.mapHomologicalComplex c) (mapHomologicalComplex α c) (mapHomologicalComplex β c))
⊢ Eq (α :=
    Quiver.Hom (V := HomologicalComplex.{v_2, u_3, u_1} W₁ c ⥤ HomologicalComplex.{v_3, u_4, u_1} W₂ c)
      (F.mapHomologicalComplex c) (H.mapHomologicalComplex c))
    (mapHomologicalComplex (α ≫ β) c)
    (CategoryStruct.comp (Y := G.mapHomologicalComplex c) (mapHomologicalComplex α c) (mapHomologicalComplex β c))

Tactic:
cat_disch
-- Module: Mathlib.Algebra.Homology.Additive
Goal:
ι : Type u_1
W₁ : Type u_3
W₂ : Type u_4
inst : Category.{v_2, u_3} W₁
inst_1 : Category.{v_3, u_4} W₂
inst_2 : HasZeroMorphisms.{v_2, u_3} W₁
inst_3 : HasZeroMorphisms.{v_3, u_4} W₂
c : ComplexShape ι
F G : Functor.{v_2, v_3, u_3, u_4} W₁ W₂
inst_4 : F.PreservesZeroMorphisms
inst_5 : G.PreservesZeroMorphisms
α : F ⟶ G
C D : HomologicalComplex.{v_2, u_3, u_1} W₁ c
f : C ⟶ D
⊢ Eq (α :=
    Quiver.Hom (V := HomologicalComplex.{v_3, u_4, u_1} W₂ c) (Functor.obj (F.mapHomologicalComplex c) C)
      (Functor.obj (G.mapHomologicalComplex c) D))
    (Functor.map (F.mapHomologicalComplex c) f ≫ app (mapHomologicalComplex α c) D)
    (app (mapHomologicalComplex α c) C ≫ Functor.map (G.mapHomologicalComplex c) f)

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 : ι
F G : Functor.{v_2, v_3, u_3, u_4} W₁ W₂
inst_8 : F.PreservesZeroMorphisms
inst_9 : G.PreservesZeroMorphisms
α : F ≅ G
c : ComplexShape ι
⊢ Eq (α :=
    Quiver.Hom (V := HomologicalComplex.{v_2, u_3, u_1} W₁ c ⥤ HomologicalComplex.{v_3, u_4, u_1} W₂ c)
      (F.mapHomologicalComplex c) (F.mapHomologicalComplex c))
    (CategoryStruct.comp (Y := G.mapHomologicalComplex c) (NatTrans.mapHomologicalComplex α.hom c)
      (NatTrans.mapHomologicalComplex α.inv c))
    (𝟙 (F.mapHomologicalComplex c))

Tactic:
simp only [← NatTrans.mapHomologicalComplex_comp, α.hom_inv_id,
    NatTrans.mapHomologicalComplex_id]

Premises used: CategoryTheory.NatTrans.mapHomologicalComplex_id, CategoryTheory.NatTrans.mapHomologicalComplex_comp, CategoryTheory.Iso.hom_inv_id
-- 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 : ι
F G : Functor.{v_2, v_3, u_3, u_4} W₁ W₂
inst_8 : F.PreservesZeroMorphisms
inst_9 : G.PreservesZeroMorphisms
α : F ≅ G
c : ComplexShape ι
⊢ Eq (α :=
    Quiver.Hom (V := HomologicalComplex.{v_2, u_3, u_1} W₁ c ⥤ HomologicalComplex.{v_3, u_4, u_1} W₂ c)
      (G.mapHomologicalComplex c) (G.mapHomologicalComplex c))
    (CategoryStruct.comp (Y := F.mapHomologicalComplex c) (NatTrans.mapHomologicalComplex α.inv c)
      (NatTrans.mapHomologicalComplex α.hom c))
    (𝟙 (G.mapHomologicalComplex c))

Tactic:
simp only [← NatTrans.mapHomologicalComplex_comp, α.inv_hom_id,
    NatTrans.mapHomologicalComplex_id]

Premises used: CategoryTheory.Iso.inv_hom_id, CategoryTheory.NatTrans.mapHomologicalComplex_id, CategoryTheory.NatTrans.mapHomologicalComplex_comp
-- 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 : ComplexShape ι
C D : HomologicalComplex.{v, u, u_1} V c
f : C ⟶ D
i : ι
α : Type u_5
inst_8 : AddRightCancelSemigroup α
inst_9 : One α
inst_10 : DecidableEq α
F : CategoryTheory.Functor.{v_2, v_3, u_3, u_4} W₁ W₂
inst_11 : F.PreservesZeroMorphisms
X : α → W₁
d : (n : α) → X (n + 1) ⟶ X n
sq : ∀ (n : α), d (n + 1) ≫ d n = 0
n : α
rw : F.map (d (n + 1) ≫ d n) = 0
rw₁ :
  Eq (α := Quiver.Hom.{v_3, u_4} (V := W₂) ((fun (n : α) ↦ F.obj (X n)) (n + 1 + 1)) ((fun (n : α) ↦ F.obj (X n)) n))
    (F.map 0) 0
rw₂ rw₃ :
  Eq.{v_3 + 1} (α :=
    Quiver.Hom.{v_3, u_4} (V := W₂) ((fun (n : α) ↦ F.obj (X n)) (n + 1 + 1)) ((fun (n : α) ↦ F.obj (X n)) n)) 0 0
⊢ Eq.{v_3 + 1} (α :=
    Quiver.Hom.{v_3, u_4} (V := W₂) ((fun (n : α) ↦ F.obj (X n)) (n + 1 + 1)) ((fun (n : α) ↦ F.obj (X n)) n))
    (CategoryStruct.comp (Y := (fun (n : α) ↦ F.obj (X n)) (n + 1)) ((fun (n : α) ↦ F.map (d n)) (n + 1))
      ((fun (n : α) ↦ F.map (d n)) n))
    0

Tactic:
rw [← F.map_comp, sq n, Functor.map_zero]

Premises used: CategoryTheory.Functor.map_zero, CategoryTheory.Functor.map_comp
-- Module: Mathlib.Algebra.Homology.Additive
Goal:
W₁ : Type u_3
W₂ : Type u_4
inst : Category.{v_2, u_3} W₁
inst_1 : Category.{v_3, u_4} W₂
inst_2 : HasZeroMorphisms.{v_2, u_3} W₁
inst_3 : HasZeroMorphisms.{v_3, u_4} W₂
α : Type u_5
inst_4 : AddRightCancelSemigroup α
inst_5 : One α
inst_6 : DecidableEq α
F : CategoryTheory.Functor.{v_2, v_3, u_3, u_4} W₁ W₂
inst_7 : F.PreservesZeroMorphisms
X : α → W₁
d : (n : α) → X (n + 1) ⟶ X n
sq : ∀ (n : α), d (n + 1) ≫ d n = 0
⊢ Eq (α := HomologicalComplex.{v_3, u_4, u_5} W₂ (ComplexShape.down α))
    (Functor.obj (F.mapHomologicalComplex (ComplexShape.down α)) (of X d sq))
    (of (fun (n : α) ↦ F.obj (X n)) (fun (n : α) ↦ F.map (d n)) ⋯)

Tactic:
HomologicalComplex.ext rfl ?_

Premises used: HomologicalComplex.ext, rfl
-- Module: Mathlib.Algebra.Homology.Additive
Goal:
W₁ : Type u_3
W₂ : Type u_4
inst : Category.{v_2, u_3} W₁
inst_1 : Category.{v_3, u_4} W₂
inst_2 : HasZeroMorphisms.{v_2, u_3} W₁
inst_3 : HasZeroMorphisms.{v_3, u_4} W₂
α : Type u_5
inst_4 : AddRightCancelSemigroup α
inst_5 : One α
inst_6 : DecidableEq α
F : CategoryTheory.Functor.{v_2, v_3, u_3, u_4} W₁ W₂
inst_7 : F.PreservesZeroMorphisms
X : α → W₁
d : (n : α) → X (n + 1) ⟶ X n
sq : ∀ (n : α), d (n + 1) ≫ d n = 0
refine :
  ∀ (i j : α),
    (ComplexShape.down α).Rel i j →
      Eq (α :=
        HomologicalComplex.X (Functor.obj (F.mapHomologicalComplex (ComplexShape.down α)) (of X d sq)) i ⟶
          HomologicalComplex.X.{v_3, u_4, u_5} (c := ComplexShape.down α)
            (of (fun (n : α) ↦ F.obj (X n)) (fun (n : α) ↦ F.map (d n)) ⋯) j)
        (HomologicalComplex.d (Functor.obj (F.mapHomologicalComplex (ComplexShape.down α)) (of X d sq)) i j ≫ eqToHom ⋯)
        (eqToHom ⋯ ≫ HomologicalComplex.d (of (fun (n : α) ↦ F.obj (X n)) (fun (n : α) ↦ F.map (d n)) ⋯) i j)
⊢ Eq (α := HomologicalComplex.{v_3, u_4, u_5} W₂ (ComplexShape.down α))
    (Functor.obj (F.mapHomologicalComplex (ComplexShape.down α)) (of X d sq))
    (of (fun (n : α) ↦ F.obj (X n)) (fun (n : α) ↦ F.map (d n)) ⋯)

Tactic:
refine HomologicalComplex.ext rfl ?_

Premises used: HomologicalComplex.ext, rfl
-- Module: Mathlib.Algebra.Homology.Additive
Goal:
W₁ : Type u_3
W₂ : Type u_4
inst : Category.{v_2, u_3} W₁
inst_1 : Category.{v_3, u_4} W₂
inst_2 : HasZeroMorphisms.{v_2, u_3} W₁
inst_3 : HasZeroMorphisms.{v_3, u_4} W₂
α : Type u_5
inst_4 : AddRightCancelSemigroup α
inst_5 : One α
inst_6 : DecidableEq α
F : CategoryTheory.Functor.{v_2, v_3, u_3, u_4} W₁ W₂
inst_7 : F.PreservesZeroMorphisms
X : α → W₁
d : (n : α) → X (n + 1) ⟶ X n
sq : ∀ (n : α), d (n + 1) ≫ d n = 0
j : α
⊢ Eq (α :=
    HomologicalComplex.X (Functor.obj (F.mapHomologicalComplex (ComplexShape.down α)) (of X d sq)) (j + 1) ⟶
      HomologicalComplex.X.{v_3, u_4, u_5} (c := ComplexShape.down α)
        (of (fun (n : α) ↦ F.obj (X n)) (fun (n : α) ↦ F.map (d n)) ⋯) j)
    (HomologicalComplex.d (Functor.obj (F.mapHomologicalComplex (ComplexShape.down α)) (of X d sq)) (j + 1) j ≫
      eqToHom ⋯)
    (eqToHom ⋯ ≫ HomologicalComplex.d (of (fun (n : α) ↦ F.obj (X n)) (fun (n : α) ↦ F.map (d n)) ⋯) (j + 1) j)

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_1 : Type u_2
inst_2 : Category.{v_1, u_2} W_1
inst_3 : Preadditive.{v_1, u_2} W_1
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 : ComplexShape ι
C D : HomologicalComplex.{v, u, u_1} V c
f_1 : C ⟶ D
i : ι
inst_8 : HasZeroObject.{v_2, u_3} W₁
inst_9 : HasZeroObject.{v_3, u_4} W₂
W : Type u_5
inst_10 : Category.{v_4, u_5} W
inst_11 : Preadditive.{v_4, u_5} W
inst_12 : HasZeroObject.{v_4, u_5} W
inst_13 : DecidableEq ι
j : ι
x x_1 : W
f g : x ⟶ x_1
hfg :
  Hom.f (CategoryTheory.Functor.map (single W c j) (f + g)) j =
    (HAdd.hAdd (α :=
          Quiver.Hom (V := HomologicalComplex.{v_4, u_5, u_1} W c) (Functor.obj (single W c j) x)
            (Functor.obj (single W c j) x_1))
          (CategoryTheory.Functor.map (single W c j) f) (CategoryTheory.Functor.map (single W c j) g)).f
      j
⊢ CategoryTheory.Functor.map (single W c j) (f + g) =
    HAdd.hAdd (α :=
      Quiver.Hom (V := HomologicalComplex.{v_4, u_5, u_1} W c) (Functor.obj (single W c j) x)
        (Functor.obj (single W c j) x_1))
      (CategoryTheory.Functor.map (single W c j) f) (CategoryTheory.Functor.map (single W c j) g)

Tactic:
ext
-- Module: Mathlib.Algebra.Homology.Additive
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
W_1 : Type u_2
inst_2 : Category.{v_1, u_2} W_1
inst_3 : Preadditive.{v_1, u_2} W_1
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 : ComplexShape ι
C D : HomologicalComplex.{v, u, u_1} V c
f_1 : C ⟶ D
i : ι
inst_8 : HasZeroObject.{v_2, u_3} W₁
inst_9 : HasZeroObject.{v_3, u_4} W₂
W : Type u_5
inst_10 : Category.{v_4, u_5} W
inst_11 : Preadditive.{v_4, u_5} W
inst_12 : HasZeroObject.{v_4, u_5} W
inst_13 : DecidableEq ι
j : ι
x x_1 : W
f g : x ⟶ x_1
⊢ Hom.f (CategoryTheory.Functor.map (single W c j) (f + g)) j =
    (HAdd.hAdd (α :=
          Quiver.Hom (V := HomologicalComplex.{v_4, u_5, u_1} W c) (Functor.obj (single W c j) x)
            (Functor.obj (single W c j) x_1))
          (CategoryTheory.Functor.map (single W c j) f) (CategoryTheory.Functor.map (single W c j) g)).f
      j

Tactic:
simp [single]

Premises used: HomologicalComplex.single
-- 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
⊢ 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) X) i

Tactic:
simp [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
⊢ HomologicalComplex.X (Functor.obj (F ⋙ single W₂ c j) X) i =
    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

Tactic:
simp [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 : ι
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
            (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
            (Functor.comp (D := HomologicalComplex.{v_2, u_3, u_1} W₁ c) (single W₁ c j) (F.mapHomologicalComplex c)) X)
          i)
      (Hom.f
        (CategoryStruct.comp (Y := Functor.obj (F ⋙ single W₂ c j) 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
            (Functor.comp (D := HomologicalComplex.{v_2, u_3, u_1} W₁ c) (single W₁ c j) (F.mapHomologicalComplex c))
            X))
        i)
⊢ Eq (α :=
    Quiver.Hom (V := 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
        (Functor.comp (D := HomologicalComplex.{v_2, u_3, u_1} W₁ c) (single W₁ c j) (F.mapHomologicalComplex c)) X))
    (CategoryStruct.comp (Y := Functor.obj (F ⋙ single W₂ c j) 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
        (Functor.comp (D := HomologicalComplex.{v_2, u_3, u_1} W₁ c) (single W₁ c j) (F.mapHomologicalComplex c)) 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} (α :=
    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)))
⊢ 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
          (Functor.comp (D := HomologicalComplex.{v_2, u_3, u_1} W₁ c) (single W₁ c j) (F.mapHomologicalComplex c)) X)
        i)
    (Hom.f
      (CategoryStruct.comp (Y := Functor.obj (F ⋙ single W₂ c j) 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
          (Functor.comp (D := HomologicalComplex.{v_2, u_3, u_1} W₁ c) (single W₁ c j) (F.mapHomologicalComplex c)) X))
      i)

Tactic:
dsimp