-- 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 : A
inst_2 : ι.Full
inst_3 : ι.Faithful
inst_4 : HasZeroMorphisms.{v_1, u_2} C
inst_5 : Abelian.{v_2, u_1} A
n : ℕ
h :
  ShortComplex.X₁
        (HomologicalComplex.sc'
          (Functor.obj (C := HomologicalComplex.{v_1, u_2, 0} C (ComplexShape.down ℕ))
            (ι.mapHomologicalComplex (ComplexShape.down ℕ)) (Λ.chainComplex X))
          (n + 2) (n + 1) n) =
      ι.obj (HomologicalComplex.X (Λ.chainComplex X) (n + 2)) →
    kernel (X :=
          ShortComplex.X₂
            (HomologicalComplex.sc'
              (Functor.obj (C := HomologicalComplex.{v_1, u_2, 0} C (ComplexShape.down ℕ))
                (ι.mapHomologicalComplex (ComplexShape.down ℕ)) (Λ.chainComplex X))
              (n + 2) (n + 1) n))
          (ShortComplex.g
            (HomologicalComplex.sc'
              (Functor.obj (C := HomologicalComplex.{v_1, u_2, 0} C (ComplexShape.down ℕ))
                (ι.mapHomologicalComplex (ComplexShape.down ℕ)) (Λ.chainComplex X))
              (n + 2) (n + 1) n)) =
        Functor.obj.{v_2, v_2, u_1, u_1} (𝟭 A)
          (kernel (X := ι.obj (HomologicalComplex.X (Λ.chainComplex X) (n + 1)))
            (ι.map (HomologicalComplex.d (Λ.chainComplex X) (n + 1) n))) →
      Eq (α :=
        ShortComplex.X₁
            (HomologicalComplex.sc'
              (Functor.obj (C := HomologicalComplex.{v_1, u_2, 0} C (ComplexShape.down ℕ))
                (ι.mapHomologicalComplex (ComplexShape.down ℕ)) (Λ.chainComplex X))
              (n + 2) (n + 1) n) ⟶
          kernel (X :=
            ShortComplex.X₂
              (HomologicalComplex.sc'
                (Functor.obj (C := HomologicalComplex.{v_1, u_2, 0} C (ComplexShape.down ℕ))
                  (ι.mapHomologicalComplex (ComplexShape.down ℕ)) (Λ.chainComplex X))
                (n + 2) (n + 1) n))
            (ShortComplex.g
              (HomologicalComplex.sc'
                (Functor.obj (C := HomologicalComplex.{v_1, u_2, 0} C (ComplexShape.down ℕ))
                  (ι.mapHomologicalComplex (ComplexShape.down ℕ)) (Λ.chainComplex X))
                (n + 2) (n + 1) n)))
        (kernel.lift
          (ShortComplex.g
            (HomologicalComplex.sc'
              (Functor.obj (C := HomologicalComplex.{v_1, u_2, 0} C (ComplexShape.down ℕ))
                (ι.mapHomologicalComplex (ComplexShape.down ℕ)) (Λ.chainComplex X))
              (n + 2) (n + 1) n))
          (ShortComplex.f
            (HomologicalComplex.sc'
              (Functor.obj (C := HomologicalComplex.{v_1, u_2, 0} C (ComplexShape.down ℕ))
                (ι.mapHomologicalComplex (ComplexShape.down ℕ)) (Λ.chainComplex X))
              (n + 2) (n + 1) n))
          ⋯)
        (ι.map (Iso.hom (Λ.chainComplexXIso X n)) ≫
          Λ.π.app
            (kernel (X := ι.obj (HomologicalComplex.X (Λ.chainComplex X) (n + 1)))
              (ι.map (HomologicalComplex.d (Λ.chainComplex X) (n + 1) n))))
⊢ Epi (X :=
    ShortComplex.X₁
      (HomologicalComplex.sc'
        (Functor.obj (C := HomologicalComplex.{v_1, u_2, 0} C (ComplexShape.down ℕ))
          (ι.mapHomologicalComplex (ComplexShape.down ℕ)) (Λ.chainComplex X))
        (n + 2) (n + 1) n))
    (Y :=
    kernel (X :=
      ShortComplex.X₂
        (HomologicalComplex.sc'
          (Functor.obj (C := HomologicalComplex.{v_1, u_2, 0} C (ComplexShape.down ℕ))
            (ι.mapHomologicalComplex (ComplexShape.down ℕ)) (Λ.chainComplex X))
          (n + 2) (n + 1) n))
      (ShortComplex.g
        (HomologicalComplex.sc'
          (Functor.obj (C := HomologicalComplex.{v_1, u_2, 0} C (ComplexShape.down ℕ))
            (ι.mapHomologicalComplex (ComplexShape.down ℕ)) (Λ.chainComplex X))
          (n + 2) (n + 1) n)))
    (kernel.lift
      (ShortComplex.g
        (HomologicalComplex.sc'
          (Functor.obj (C := HomologicalComplex.{v_1, u_2, 0} C (ComplexShape.down ℕ))
            (ι.mapHomologicalComplex (ComplexShape.down ℕ)) (Λ.chainComplex X))
          (n + 2) (n + 1) n))
      (ShortComplex.f
        (HomologicalComplex.sc'
          (Functor.obj (C := HomologicalComplex.{v_1, u_2, 0} C (ComplexShape.down ℕ))
            (ι.mapHomologicalComplex (ComplexShape.down ℕ)) (Λ.chainComplex X))
          (n + 2) (n + 1) n))
      ⋯)

Tactic:
convert! epi_comp (ι.map (Λ.chainComplexXIso X n).hom) (Λ.π.app _)

Premises used: CategoryTheory.epi_comp, CategoryTheory.Abelian.LeftResolution.chainComplexXIso, CategoryTheory.Abelian.LeftResolution.π, CategoryTheory.Functor.map, CategoryTheory.Iso.hom, CategoryTheory.NatTrans.app