-- 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 : ℕ
e_3 :
  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))
e_4 :
  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))))
have h : 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) ⟶
    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.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)))) ≫
    kernel.ι
      (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)))
Tactic: rw [← cancel_mono (kernel.ι _), kernel.lift_ι]