-- 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 : A
inst_2 : ι.Full
inst_3 : ι.Faithful
inst_4 : HasZeroMorphisms.{v_1, u_2} C
inst_5 : Abelian.{v_2, u_1} A
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))
      ⋯)
have 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))
        sorry)
      (ι.map (Iso.hom (Λ.chainComplexXIso X n)) ≫
        Λ.π.app
          (kernel (X := ι.obj (HomologicalComplex.X (Λ.chainComplex X) (n + 1)))
            (ι.map (HomologicalComplex.d (Λ.chainComplex X) (n + 1) n))))
Tactic: convert! epi_comp (ι.map (Λ.chainComplexXIso X n).hom) (Λ.π.app _)