-- Mathlib/Algebra/Homology/Additive.lean
theorem map_chain_complex_of (F : W₁ ⥤ W₂) [F.PreservesZeroMorphisms] (X : α → W₁)
    (d : ∀ n, X (n + 1) ⟶ X n) (sq : ∀ n, d (n + 1) ≫ d n = 0) :
    (F.mapHomologicalComplex _).obj (ChainComplex.of X d sq) =
      ChainComplex.of (fun n => F.obj (X n)) (fun n => F.map (d n)) fun n => by
        rw [← F.map_comp, sq n, Functor.map_zero]

Proof state:
W₁ : Type u_3
W₂ : Type u_4
inst✝⁷ : Category.{u_6, u_3} W₁
inst✝⁶ : Category.{u_7, u_4} W₂
inst✝⁵ : HasZeroMorphisms W₁
inst✝⁴ : HasZeroMorphisms W₂
α : Type u_5
inst✝³ : AddRightCancelSemigroup α
inst✝² : One α
inst✝¹ : DecidableEq α
F : W₁ ⥤ W₂
inst✝ : F.PreservesZeroMorphisms
X : α → W₁
d : (n : α) → X (n + 1) ⟶ X n
sq : ∀ (n : α), d (n + 1) ≫ d n = 0
⊢ ∀ (i j : α),
    (ComplexShape.down α).Rel i j →
      ((F.mapHomologicalComplex (ComplexShape.down α)).obj (of X d sq)).d i j ≫ eqToHom ⋯ =
        eqToHom ⋯ ≫ (of (fun n => F.obj (X n)) (fun n => F.map (d n)) ⋯).d i j

Tactic:
rintro i j (rfl : j + 1 = i)

Result:
W₁ : Type u_3
W₂ : Type u_4
inst✝⁷ : Category.{u_6, u_3} W₁
inst✝⁶ : Category.{u_7, u_4} W₂
inst✝⁵ : HasZeroMorphisms W₁
inst✝⁴ : HasZeroMorphisms W₂
α : Type u_5
inst✝³ : AddRightCancelSemigroup α
inst✝² : One α
inst✝¹ : DecidableEq α
F : W₁ ⥤ W₂
inst✝ : F.PreservesZeroMorphisms
X : α → W₁
d : (n : α) → X (n + 1) ⟶ X n
sq : ∀ (n : α), d (n + 1) ≫ d n = 0
j : α
⊢ ((F.mapHomologicalComplex (ComplexShape.down α)).obj (of X d sq)).d (j + 1) j ≫ eqToHom ⋯ =
    eqToHom ⋯ ≫ (of (fun n => F.obj (X n)) (fun n => F.map (d n)) ⋯).d (j + 1) j

Proof state:
W₁ : Type u_3
W₂ : Type u_4
inst✝⁷ : Category.{u_6, u_3} W₁
inst✝⁶ : Category.{u_7, u_4} W₂
inst✝⁵ : HasZeroMorphisms W₁
inst✝⁴ : HasZeroMorphisms W₂
α : Type u_5
inst✝³ : AddRightCancelSemigroup α
inst✝² : One α
inst✝¹ : DecidableEq α
F : W₁ ⥤ W₂
inst✝ : F.PreservesZeroMorphisms
X : α → W₁
d : (n : α) → X (n + 1) ⟶ X n
sq : ∀ (n : α), d (n + 1) ≫ d n = 0
⊢ (F.mapHomologicalComplex (ComplexShape.down α)).obj (of X d sq) = of (fun n => F.obj (X n)) (fun n => F.map (d n)) ⋯

Tactic:
refine HomologicalComplex.ext rfl ?_

Result:
W₁ : Type u_3
W₂ : Type u_4
inst✝⁷ : Category.{u_6, u_3} W₁
inst✝⁶ : Category.{u_7, u_4} W₂
inst✝⁵ : HasZeroMorphisms W₁
inst✝⁴ : HasZeroMorphisms W₂
α : Type u_5
inst✝³ : AddRightCancelSemigroup α
inst✝² : One α
inst✝¹ : DecidableEq α
F : W₁ ⥤ W₂
inst✝ : F.PreservesZeroMorphisms
X : α → W₁
d : (n : α) → X (n + 1) ⟶ X n
sq : ∀ (n : α), d (n + 1) ≫ d n = 0
⊢ ∀ (i j : α),
    (ComplexShape.down α).Rel i j →
      ((F.mapHomologicalComplex (ComplexShape.down α)).obj (of X d sq)).d i j ≫ eqToHom ⋯ =
        eqToHom ⋯ ≫ (of (fun n => F.obj (X n)) (fun n => F.map (d n)) ⋯).d i j

Proof state:
ι : Type u_1
V : Type u
inst✝¹¹ : Category.{v, u} V
inst✝¹⁰ : Preadditive V
W : Type u_2
inst✝⁹ : Category.{?u.71678, u_2} W
inst✝⁸ : Preadditive W
W₁ : Type u_3
W₂ : Type u_4
inst✝⁷ : Category.{?u.71704, u_3} W₁
inst✝⁶ : Category.{?u.71708, u_4} W₂
inst✝⁵ : HasZeroMorphisms W₁
inst✝⁴ : HasZeroMorphisms W₂
c : ComplexShape ι
C D : HomologicalComplex V c
f : C ⟶ D
i : ι
α : Type u_5
inst✝³ : AddRightCancelSemigroup α
inst✝² : One α
inst✝¹ : DecidableEq α
F : W₁ ⥤ W₂
inst✝ : F.PreservesZeroMorphisms
X : α → W₁
d : (n : α) → X (n + 1) ⟶ X n
sq : ∀ (n : α), d (n + 1) ≫ d n = 0
n : α
⊢ (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]

Result:
no goals

Proof state:
W₁ : Type u_3
W₂ : Type u_4
inst✝⁷ : Category.{u_6, u_3} W₁
inst✝⁶ : Category.{u_7, u_4} W₂
inst✝⁵ : HasZeroMorphisms W₁
inst✝⁴ : HasZeroMorphisms W₂
α : Type u_5
inst✝³ : AddRightCancelSemigroup α
inst✝² : One α
inst✝¹ : DecidableEq α
F : W₁ ⥤ W₂
inst✝ : F.PreservesZeroMorphisms
X : α → W₁
d : (n : α) → X (n + 1) ⟶ X n
sq : ∀ (n : α), d (n + 1) ≫ d n = 0
j : α
⊢ ((F.mapHomologicalComplex (ComplexShape.down α)).obj (of X d sq)).d (j + 1) j ≫ eqToHom ⋯ =
    eqToHom ⋯ ≫ (of (fun n => F.obj (X n)) (fun n => F.map (d n)) ⋯).d (j + 1) j

Tactic:
simp only [CategoryTheory.Functor.mapHomologicalComplex_obj_d, of_d, eqToHom_refl, comp_id,
  id_comp]

Result:
no goals