-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.AB (goal)
Goal:
J : Type u
inst : SmallCategory J
inst_1 : IsFiltered J
S : ShortComplex (J ⥤ AddCommGrpCat)
hS :
  ∀ (j : J),
    LE.le (α := AddSubgroup (↑(ShortComplex.X₂ (S.map (Functor.obj (evaluation J AddCommGrpCat) j))) : Type u))
      (AddMonoidHom.ker (AddCommGrpCat.Hom.hom (ShortComplex.g (S.map (Functor.obj (evaluation J AddCommGrpCat) j)))))
      (AddMonoidHom.range (AddCommGrpCat.Hom.hom (ShortComplex.f (S.map (Functor.obj (evaluation J AddCommGrpCat) j)))))
j : J
y :
  ToType (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC := AddCommGrpCat.carrier)
    (S.X₂.obj j)
hx :
  Eq (α := (↑(colimit S.X₃) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
            AddCommGrpCat.carrier) (Y := colimit S.X₃) (colimit.ι S.X₃ j) :
          (a : (↑(S.X₃.obj j) : Type u)) → (↑(colimit S.X₃) : Type u))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
                AddCommGrpCat.carrier) (S.g.app j) :
              (a : (↑(S.X₂.obj j) : Type u)) → (↑(S.X₃.obj j) : Type u))
            y :
          (↑(S.X₃.obj j) : Type u)) :
      (↑(colimit S.X₃) : Type u))
    ((AddCommGrpCat.Hom.hom (colimit.ι S.X₃ j) : (a : (↑(S.X₃.obj j) : Type u)) → (↑(colimit S.X₃) : Type u)) 0 :
      (↑(colimit S.X₃) : Type u))
k : J
e₁ e₂ : j ⟶ k
hk :
  Eq (α := (↑(S.X₃.obj k) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
            AddCommGrpCat.carrier) (S.g.app k) :
          (a : (↑(S.X₂.obj k) : Type u)) → (↑(S.X₃.obj k) : Type u))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
                AddCommGrpCat.carrier) (S.X₂.map e₁) :
              (a : (↑(S.X₂.obj j) : Type u)) → (↑(S.X₂.obj k) : Type u))
            y :
          (↑(S.X₂.obj k) : Type u)) :
      (↑(S.X₃.obj k) : Type u))
    (0 : (↑(S.X₃.obj k) : Type u))
t : (↑(ShortComplex.X₁ (S.map (Functor.obj (evaluation J AddCommGrpCat) k))) : Type u)
ht :
  Eq (α := (↑(ShortComplex.X₂ (S.map (Functor.obj (evaluation J AddCommGrpCat) k))) : Type u))
    ((AddCommGrpCat.Hom.hom (ShortComplex.f (S.map (Functor.obj (evaluation J AddCommGrpCat) k))) :
          (a : (↑(S.map ((evaluation J AddCommGrpCat).obj k)).X₁ : Type u)) →
            (↑(S.map ((evaluation J AddCommGrpCat).obj k)).X₂ : Type u))
        t :
      (↑(ShortComplex.X₂ (S.map (Functor.obj (evaluation J AddCommGrpCat) k))) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
            AddCommGrpCat.carrier) (S.X₂.map e₁) :
          (a : (↑(S.X₂.obj j) : Type u)) → (↑(S.X₂.obj k) : Type u))
        y :
      (↑(S.X₂.obj k) : Type u))
⊢ Eq (α := (↑(ShortComplex.X₂ (S.map colim)) : Type u))
    ((AddCommGrpCat.Hom.hom (ShortComplex.f (S.map colim)) :
          (a : (↑(S.map colim).X₁ : Type u)) → (↑(S.map colim).X₂ : Type u))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
                AddCommGrpCat.carrier) (Y := colimit S.X₁) (colimit.ι S.X₁ k) :
              (a : (↑(S.X₁.obj k) : Type u)) → (↑(colimit S.X₁) : Type u))
            t :
          (↑(colimit S.X₁) : Type u)) :
      (↑(ShortComplex.X₂ (S.map colim)) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
            AddCommGrpCat.carrier) (Y := colimit S.X₂) (colimit.ι S.X₂ j) :
          (a : (↑(S.X₂.obj j) : Type u)) → (↑(colimit S.X₂) : Type u))
        y :
      (↑(colimit S.X₂) : Type u))
have h : Eq (α := (↑(ShortComplex.X₂ (S.map colim)) : Type u))
  ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
          AddCommGrpCat.carrier) (Y := ShortComplex.X₂ (S.map colim)) (colimit.ι S.X₂ k) :
        (a : (↑(S.X₂.obj k) : Type u)) → (↑(S.map colim).X₂ : Type u))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
              AddCommGrpCat.carrier) (S.X₂.map e₁) :
            (a : (↑(S.X₂.obj j) : Type u)) → (↑(S.X₂.obj k) : Type u))
          y :
        (↑(S.X₂.obj k) : Type u)) :
    (↑(ShortComplex.X₂ (S.map colim)) : Type u))
  ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
          AddCommGrpCat.carrier) (Y := colimit S.X₂) (colimit.ι S.X₂ j) :
        (a : (↑(S.X₂.obj j) : Type u)) → (↑(colimit S.X₂) : Type u))
      y :
    (↑(colimit S.X₂) : Type u))
Tactic: erw [← ConcreteCategory.comp_apply, colimit.ι_map, ConcreteCategory.comp_apply, ht]