-- 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))
⊢ 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 rcases : ∀ (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))),
  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))
Tactic: rcases hS k hk with ⟨t, ht⟩