-- Lean 4 proof step from Mathlib.Algebra.Homology.LeftResolution.Basic (goal)
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 : ℕ
hn :
  Eq (α := HomologicalComplex.X (Λ.chainComplex X) (n + 1) ⟶ HomologicalComplex.X (Λ.chainComplex Z) (n + 1))
    (HomologicalComplex.Hom.f (Λ.chainComplexMap (f ≫ g)) (n + 1))
    (HomologicalComplex.Hom.f (Λ.chainComplexMap f ≫ Λ.chainComplexMap g) (n + 1))
⊢ Eq (α :=
    Λ.F.obj
        (kernel (X := ι.obj (HomologicalComplex.X (Λ.chainComplex X) (n + 1)))
          (ι.map (HomologicalComplex.d (Λ.chainComplex X) (n + 1) n))) ⟶
      Λ.F.obj
        (kernel (X := ι.obj (HomologicalComplex.X (Λ.chainComplex Z) (n + 1)))
          (ι.map (HomologicalComplex.d (Λ.chainComplex Z) (n + 1) n))))
    (Λ.F.map
      (kernel.map (ι.map (HomologicalComplex.d (Λ.chainComplex X) (n + 1) n))
        (ι.map (HomologicalComplex.d (Λ.chainComplex Z) (n + 1) n))
        (ι.map (HomologicalComplex.Hom.f (Λ.chainComplexMap (f ≫ g)) (n + 1)))
        (ι.map (HomologicalComplex.Hom.f (Λ.chainComplexMap (f ≫ g)) n)) ⋯))
    (Λ.F.map
      (CategoryStruct.comp (Y :=
        kernel (X := ι.obj (HomologicalComplex.X (Λ.chainComplex Y) (n + 1)))
          (ι.map (HomologicalComplex.d (Λ.chainComplex Y) (n + 1) n)))
        (kernel.map (ι.map (HomologicalComplex.d (Λ.chainComplex X) (n + 1) n))
          (ι.map (HomologicalComplex.d (Λ.chainComplex Y) (n + 1) n))
          (ι.map (HomologicalComplex.Hom.f (Λ.chainComplexMap f) (n + 1)))
          (ι.map (HomologicalComplex.Hom.f (Λ.chainComplexMap f) n)) ⋯)
        (kernel.map (ι.map (HomologicalComplex.d (Λ.chainComplex Y) (n + 1) n))
          (ι.map (HomologicalComplex.d (Λ.chainComplex Z) (n + 1) n))
          (ι.map (HomologicalComplex.Hom.f (Λ.chainComplexMap g) (n + 1)))
          (ι.map (HomologicalComplex.Hom.f (Λ.chainComplexMap g) n)) ⋯)))
have h : Eq (α :=
  kernel (X := ι.obj (HomologicalComplex.X (Λ.chainComplex X) (n + 1)))
      (ι.map (HomologicalComplex.d (Λ.chainComplex X) (n + 1) n)) ⟶
    kernel (X := ι.obj (HomologicalComplex.X (Λ.chainComplex Z) (n + 1)))
      (ι.map (HomologicalComplex.d (Λ.chainComplex Z) (n + 1) n)))
  (kernel.map (ι.map (HomologicalComplex.d (Λ.chainComplex X) (n + 1) n))
    (ι.map (HomologicalComplex.d (Λ.chainComplex Z) (n + 1) n))
    (ι.map (HomologicalComplex.Hom.f (Λ.chainComplexMap (f ≫ g)) (n + 1)))
    (ι.map (HomologicalComplex.Hom.f (Λ.chainComplexMap (f ≫ g)) n)) sorry)
  (CategoryStruct.comp (Y :=
    kernel (X := ι.obj (HomologicalComplex.X (Λ.chainComplex Y) (n + 1)))
      (ι.map (HomologicalComplex.d (Λ.chainComplex Y) (n + 1) n)))
    (kernel.map (ι.map (HomologicalComplex.d (Λ.chainComplex X) (n + 1) n))
      (ι.map (HomologicalComplex.d (Λ.chainComplex Y) (n + 1) n))
      (ι.map (HomologicalComplex.Hom.f (Λ.chainComplexMap f) (n + 1)))
      (ι.map (HomologicalComplex.Hom.f (Λ.chainComplexMap f) n)) sorry)
    (kernel.map (ι.map (HomologicalComplex.d (Λ.chainComplex Y) (n + 1) n))
      (ι.map (HomologicalComplex.d (Λ.chainComplex Z) (n + 1) n))
      (ι.map (HomologicalComplex.Hom.f (Λ.chainComplexMap g) (n + 1)))
      (ι.map (HomologicalComplex.Hom.f (Λ.chainComplexMap g) n)) sorry))
Tactic: congr 1