-- Module: Mathlib.Algebra.Homology.LeftResolution.Basic
Goal:
A : Type u_1
C : Type u_2
inst : Category.{v_1, u_2} C
inst_1 : Category.{v_2, u_1} A
ι : Functor.{v_1, v_2, u_2, u_1} C A
Λ : LeftResolution ι
X Y Z : A
f : X ⟶ Y
g : Y ⟶ Z
inst_2 : ι.Full
inst_3 : ι.Faithful
inst_4 : HasZeroMorphisms.{v_1, u_2} C
inst_5 : Abelian.{v_2, u_1} A
n : ℕ
p :
  (f : HomologicalComplex.X (Λ.chainComplex X) n ⟶ HomologicalComplex.X (Λ.chainComplex Y) n) ×'
    (f' : HomologicalComplex.X (Λ.chainComplex X) (n + 1) ⟶ HomologicalComplex.X (Λ.chainComplex Y) (n + 1)) ×'
      f' ≫ HomologicalComplex.d (Λ.chainComplex Y) (n + 1) n = HomologicalComplex.d (Λ.chainComplex X) (n + 1) n ≫ f
⊢ ι.map
      ((Iso.hom (Λ.chainComplexXIso X n) ≫
          Λ.F.map
              (kernel.map (ι.map (HomologicalComplex.d (Λ.chainComplex X) (n + 1) n))
                (ι.map (HomologicalComplex.d (Λ.chainComplex Y) (n + 1) n))
                (ι.map
                  (p.snd (β :=
                        fun
                          (f : HomologicalComplex.X (Λ.chainComplex X) n ⟶ HomologicalComplex.X (Λ.chainComplex Y) n) ↦
                        (f' :
                          HomologicalComplex.X (Λ.chainComplex X) (n + 1) ⟶
                            HomologicalComplex.X (Λ.chainComplex Y) (n + 1)) ×'
                          f' ≫ HomologicalComplex.d (Λ.chainComplex Y) (n + 1) n =
                            HomologicalComplex.d (Λ.chainComplex X) (n + 1) n ≫ f).fst
                    (β :=
                    fun
                      (f' :
                        HomologicalComplex.X (Λ.chainComplex X) (n + 1) ⟶
                          HomologicalComplex.X (Λ.chainComplex Y) (n + 1)) ↦
                    f' ≫ HomologicalComplex.d (Λ.chainComplex Y) (n + 1) n =
                      HomologicalComplex.d (Λ.chainComplex X) (n + 1) n ≫
                        p.fst (β :=
                          fun
                            (f :
                              HomologicalComplex.X (Λ.chainComplex X) n ⟶ HomologicalComplex.X (Λ.chainComplex Y) n) ↦
                          (f' :
                            HomologicalComplex.X (Λ.chainComplex X) (n + 1) ⟶
                              HomologicalComplex.X (Λ.chainComplex Y) (n + 1)) ×'
                            f' ≫ HomologicalComplex.d (Λ.chainComplex Y) (n + 1) n =
                              HomologicalComplex.d (Λ.chainComplex X) (n + 1) n ≫ f))))
                (ι.map
                  (p.fst (β :=
                    fun (f : HomologicalComplex.X (Λ.chainComplex X) n ⟶ HomologicalComplex.X (Λ.chainComplex Y) n) ↦
                    (f' :
                      HomologicalComplex.X (Λ.chainComplex X) (n + 1) ⟶
                        HomologicalComplex.X (Λ.chainComplex Y) (n + 1)) ×'
                      f' ≫ HomologicalComplex.d (Λ.chainComplex Y) (n + 1) n =
                        HomologicalComplex.d (Λ.chainComplex X) (n + 1) n ≫ f)))
                ⋯) ≫
            Iso.inv (Λ.chainComplexXIso Y n)) ≫
        HomologicalComplex.d (Λ.chainComplex Y) (n + 2) (n + 1)) =
    ι.map
      (HomologicalComplex.d (Λ.chainComplex X) (n + 2) (n + 1) ≫
        p.snd (β := fun (f : HomologicalComplex.X (Λ.chainComplex X) n ⟶ HomologicalComplex.X (Λ.chainComplex Y) n) ↦
              (f' :
                HomologicalComplex.X (Λ.chainComplex X) (n + 1) ⟶ HomologicalComplex.X (Λ.chainComplex Y) (n + 1)) ×'
                f' ≫ HomologicalComplex.d (Λ.chainComplex Y) (n + 1) n =
                  HomologicalComplex.d (Λ.chainComplex X) (n + 1) n ≫ f).fst
          (β :=
          fun (f' : HomologicalComplex.X (Λ.chainComplex X) (n + 1) ⟶ HomologicalComplex.X (Λ.chainComplex Y) (n + 1)) ↦
          f' ≫ HomologicalComplex.d (Λ.chainComplex Y) (n + 1) n =
            HomologicalComplex.d (Λ.chainComplex X) (n + 1) n ≫
              p.fst (β :=
                fun (f : HomologicalComplex.X (Λ.chainComplex X) n ⟶ HomologicalComplex.X (Λ.chainComplex Y) n) ↦
                (f' :
                  HomologicalComplex.X (Λ.chainComplex X) (n + 1) ⟶ HomologicalComplex.X (Λ.chainComplex Y) (n + 1)) ×'
                  f' ≫ HomologicalComplex.d (Λ.chainComplex Y) (n + 1) n =
                    HomologicalComplex.d (Λ.chainComplex X) (n + 1) n ≫ f)))

Tactic:
simp [map_chainComplex_d]

Premises used: CategoryTheory.Abelian.LeftResolution.map_chainComplex_d