-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.Filtered (goal)
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 α))
⊢ 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)
have 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 α))
Tactic: convert!
      IsColimit.comp_coconePointUniqueUpToIso_hom
        (liftToFinsetColimitCocone (Discrete.functor f)).isColimit (colimit.isColimit _) j