-- Module: Mathlib.CategoryTheory.Limits.Constructions.Filtered
Goal:
C : Type u
inst : Category.{v, u} C
α : Type w
inst_1 : HasFiniteCoproducts.{v, u} C
f : α → C
inst_2 : HasColimitsOfShape.{w, w, v, u} (Finset (Discrete α)) C
inst_3 : HasCoproduct.{w, v, u} f
S : Finset (Discrete α)
j : ↥S
h :
  (f (↑j : Discrete α).as ⟶ sigmaObj.{w, v, u} f) =
      (Functor.obj.{w, v, w, u} (Discrete.functor f) (↑j : Discrete α) ⟶
        Cocone.pt.{w, v, w, u} (F := Discrete.functor f) (colimit.cocone (Discrete.functor f))) →
    f (↑j : Discrete α).as = Functor.obj.{w, v, w, u} (Discrete.functor f) (↑j : Discrete α) →
      colimit.{w, w, v, u} (liftToFinsetObj (Discrete.functor f)) =
          Functor.obj.{w, v, w, u}
            (Functor.obj (Functor.const (Discrete α))
              (Cocone.pt.{w, v, w, u} (F := Discrete.functor f)
                (ColimitCocone.cocone (liftToFinsetColimitCocone (Discrete.functor f)))))
            (↑j : Discrete α) →
        Eq.{v + 1} (α := f (↑j : Discrete α).as ⟶ colimit.{w, w, v, u} (liftToFinsetObj (Discrete.functor f)))
          (Sigma.ι.{w, v, u} (C := C) (fun (x : ↥S) ↦ f (↑x : Discrete α).as) j ≫
              colimit.ι (liftToFinsetObj (Discrete.functor f)) S :
            f (↑j : Discrete α).as ⟶ colimit.{w, w, v, u} (liftToFinsetObj (Discrete.functor f)))
          (NatTrans.app (Cocone.ι (ColimitCocone.cocone (liftToFinsetColimitCocone (Discrete.functor f))))
              (↑j : Discrete α) :
            Functor.obj.{w, v, w, u} (Discrete.functor f) (↑j : Discrete α) ⟶
              Functor.obj.{w, v, w, u}
                (Functor.obj (Functor.const (Discrete α))
                  (Cocone.pt.{w, v, w, u} (F := Discrete.functor f)
                    (ColimitCocone.cocone (liftToFinsetColimitCocone (Discrete.functor f)))))
                (↑j : Discrete α))
h₁ :
  (f (↑j : Discrete α).as ⟶ sigmaObj.{w, v, u} f) =
      (Functor.obj.{w, v, w, u} (Discrete.functor f) (↑j : Discrete α) ⟶
        Cocone.pt.{w, v, w, u} (F := Discrete.functor f) (colimit.cocone (Discrete.functor f))) →
    Eq.{v + 1} (α := f (↑j : Discrete α).as ⟶ sigmaObj.{w, v, u} f)
      (CategoryStruct.comp (Y := sigmaObj.{w, v, u} fun (x : ↥S) ↦ f (↑x : Discrete α).as)
          (Sigma.ι.{w, v, u} (C := C) (fun (x : ↥S) ↦ f (↑x : Discrete α).as) j)
          (Sigma.desc fun (s : ↥S) ↦ Sigma.ι f (↑s : Discrete α).as) :
        f (↑j : Discrete α).as ⟶ sigmaObj.{w, v, u} f)
      (NatTrans.app (Cocone.ι (colimit.cocone (Discrete.functor f))) (↑j : Discrete α) :
        Functor.obj.{w, v, w, u} (Discrete.functor f) (↑j : Discrete α) ⟶
          Functor.obj.{w, v, w, u}
            (Functor.obj (Functor.const (Discrete α))
              (Cocone.pt.{w, v, w, u} (F := Discrete.functor f) (colimit.cocone (Discrete.functor f))))
            (↑j : Discrete α))
⊢ Eq.{v + 1} (α := f (↑j : Discrete α).as ⟶ sigmaObj.{w, v, u} f)
    (CategoryStruct.comp (Y := colimit.{w, w, v, u} (liftToFinsetObj (Discrete.functor f)))
        (Sigma.ι.{w, v, u} (C := C) (fun (x : ↥S) ↦ f (↑x : Discrete α).as) j ≫
            colimit.ι (liftToFinsetObj (Discrete.functor f)) S :
          f (↑j : Discrete α).as ⟶ colimit.{w, w, v, u} (liftToFinsetObj (Discrete.functor f)))
        (Iso.hom
            (IsColimit.coconePointUniqueUpToIso
              (ColimitCocone.isColimit (liftToFinsetColimitCocone (Discrete.functor f)))
              (colimit.isColimit (Discrete.functor f))) :
          colimit.{w, w, v, u} (liftToFinsetObj (Discrete.functor f)) ⟶ sigmaObj.{w, v, u} f) :
      f (↑j : Discrete α).as ⟶ sigmaObj.{w, v, u} f)
    (CategoryStruct.comp (Y := sigmaObj.{w, v, u} fun (x : ↥S) ↦ f (↑x : Discrete α).as)
        (Sigma.ι.{w, v, u} (C := C) (fun (x : ↥S) ↦ f (↑x : Discrete α).as) j)
        (Sigma.desc fun (s : ↥S) ↦ Sigma.ι f (↑s : Discrete α).as) :
      f (↑j : Discrete α).as ⟶ sigmaObj.{w, v, u} f)

Tactic:
convert!
      IsColimit.comp_coconePointUniqueUpToIso_hom
        (liftToFinsetColimitCocone (Discrete.functor f)).isColimit (colimit.isColimit _) j

Premises used: CategoryTheory.Limits.colimit.isColimit, CategoryTheory.Discrete.functor, CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinsetColimitCocone, CategoryTheory.Limits.IsColimit.comp_coconePointUniqueUpToIso_hom, CategoryTheory.Limits.ColimitCocone.isColimit, Subtype.val