-- Lean 4 proof step from Mathlib.Algebra.Category.Grp.AB (hypothesis)
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.X₃.map e₁) :
          (a : (↑(S.X₃.obj j) : 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.g.app j) :
              (a : (↑(S.X₂.obj j) : Type u)) → (↑(S.X₃.obj j) : Type u))
            y :
          (↑(S.X₃.obj j) : 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))
        0 :
      (↑(S.X₃.obj k) : Type u))
⊢ Membership.mem (α := (↑(ShortComplex.X₂ (S.map colim)) : Type u)) (γ :=
    AddSubgroup (↑(ShortComplex.X₂ (S.map colim)) : Type u))
    (AddMonoidHom.range (AddCommGrpCat.Hom.hom (ShortComplex.f (S.map colim))))
    ((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 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))
Tactic: rw [map_zero, ← ConcreteCategory.comp_apply, ← NatTrans.naturality, ConcreteCategory.comp_apply]
      at hk
Cleared hypotheses: hk