-- 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))
⊢ 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 : ∀ (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))
Tactic: rcases Concrete.colimit_exists_of_rep_eq.{u, u, u} S.X₃ _ _ hx with ⟨k, e₁, e₂, hk⟩