-- Module: Mathlib.CategoryTheory.Comma.Final
Goal:
A : Type v₁
inst : Category.{v₁, v₁} A
B : Type v₁
inst_1 : Category.{v₁, v₁} B
T : Type v₁
inst_2 : Category.{v₁, v₁} T
L : A ⥤ T
R : B ⥤ T
inst_3 : R.Final
G : A ⥤ Type v₁
i : colimit G ≅ colimit (fst L R ⋙ G) :=
  Iso.trans (Y := colimit (grothendieckProj L ⋙ G))
    (L.colimitIsoColimitGrothendieck G : colimit G ≅ colimit (grothendieckProj L ⋙ G))
    (Iso.trans (Y := colimit (Grothendieck.pre (functor L) R ⋙ grothendieckProj L ⋙ G))
        (Iso.symm (Final.colimitIso (Grothendieck.pre (functor L) R) (grothendieckProj L ⋙ G)) :
          colimit (grothendieckProj L ⋙ G) ≅ colimit (Grothendieck.pre (functor L) R ⋙ grothendieckProj L ⋙ G))
        (Iso.trans (Y := colimit (Grothendieck.pre (functor L) R ⋙ grothendieckProj L ⋙ G))
            (HasColimit.isoOfNatIso (Iso.refl (Grothendieck.pre (functor L) R ⋙ grothendieckProj L ⋙ G)) :
              colimit (Grothendieck.pre (functor L) R ⋙ grothendieckProj L ⋙ G) ≅
                colimit (Grothendieck.pre (functor L) R ⋙ grothendieckProj L ⋙ G))
            (Final.colimitIso (grothendieckPrecompFunctorEquivalence L R).functor (fst L R ⋙ G) :
              colimit ((grothendieckPrecompFunctorEquivalence L R).functor ⋙ fst L R ⋙ G) ≅ colimit (fst L R ⋙ G)) :
          colimit (Grothendieck.pre (functor L) R ⋙ grothendieckProj L ⋙ G) ≅ colimit (fst L R ⋙ G)) :
      colimit (grothendieckProj L ⋙ G) ≅ colimit (fst L R ⋙ G))
a : A
b : B
f : L.obj a ⟶ R.obj b
h :
  Eq (α :=
    (fst L R ⋙ G).obj
        ((grothendieckPrecompFunctorToComma L R).obj
          { base := b, fiber := CostructuredArrow.mk f : Grothendieck (R ⋙ functor L) }) ⟶
      colimit G)
    (colimit.ι G a)
    (CategoryStruct.comp (Y := colimit (fst L R ⋙ G))
      (colimit.ι (fst L R ⋙ G)
        ((grothendieckPrecompFunctorToComma L R).obj { base := b, fiber := CostructuredArrow.mk f }))
      (CategoryStruct.comp (Y := colimit (Grothendieck.pre (functor L) R ⋙ grothendieckProj L ⋙ G))
        (Iso.inv (Final.colimitIso (grothendieckPrecompFunctorToComma L R) (fst L R ⋙ G)) :
          colimit (fst L R ⋙ G) ⟶ colimit (Grothendieck.pre (functor L) R ⋙ grothendieckProj L ⋙ G))
        (CategoryStruct.comp (Y := colimit (Grothendieck.pre (functor L) R ⋙ grothendieckProj L ⋙ G))
            (Iso.inv (HasColimit.isoOfNatIso (Iso.refl (Grothendieck.pre (functor L) R ⋙ grothendieckProj L ⋙ G))) :
              colimit (Grothendieck.pre (functor L) R ⋙ grothendieckProj L ⋙ G) ⟶
                colimit (Grothendieck.pre (functor L) R ⋙ grothendieckProj L ⋙ G))
            (CategoryStruct.comp (Y := colimit (grothendieckProj L ⋙ G))
                (Iso.hom (Final.colimitIso (Grothendieck.pre (functor L) R) (grothendieckProj L ⋙ G)) :
                  colimit (Grothendieck.pre (functor L) R ⋙ grothendieckProj L ⋙ G) ⟶ colimit (grothendieckProj L ⋙ G))
                (Iso.inv (L.colimitIsoColimitGrothendieck G) : colimit (grothendieckProj L ⋙ G) ⟶ colimit G) :
              colimit (Grothendieck.pre (functor L) R ⋙ grothendieckProj L ⋙ G) ⟶ colimit G) :
          colimit (Grothendieck.pre (functor L) R ⋙ grothendieckProj L ⋙ G) ⟶ colimit G)))
⊢ Eq (α := G.obj a ⟶ colimit G) (colimit.ι G a)
    (CategoryStruct.comp (Y := colimit (fst L R ⋙ G)) (colimit.ι (fst L R ⋙ G) { left := a, right := b, hom := f })
      (CategoryStruct.comp (Y := colimit (Grothendieck.pre (functor L) R ⋙ grothendieckProj L ⋙ G))
        (Iso.inv (Final.colimitIso (grothendieckPrecompFunctorToComma L R) (fst L R ⋙ G)) :
          colimit (fst L R ⋙ G) ⟶ colimit (Grothendieck.pre (functor L) R ⋙ grothendieckProj L ⋙ G))
        (CategoryStruct.comp (Y := colimit (Grothendieck.pre (functor L) R ⋙ grothendieckProj L ⋙ G))
            (Iso.inv (HasColimit.isoOfNatIso (Iso.refl (Grothendieck.pre (functor L) R ⋙ grothendieckProj L ⋙ G))) :
              colimit (Grothendieck.pre (functor L) R ⋙ grothendieckProj L ⋙ G) ⟶
                colimit (Grothendieck.pre (functor L) R ⋙ grothendieckProj L ⋙ G))
            (CategoryStruct.comp (Y := colimit (grothendieckProj L ⋙ G))
                (Iso.hom (Final.colimitIso (Grothendieck.pre (functor L) R) (grothendieckProj L ⋙ G)) :
                  colimit (Grothendieck.pre (functor L) R ⋙ grothendieckProj L ⋙ G) ⟶ colimit (grothendieckProj L ⋙ G))
                (Iso.inv (L.colimitIsoColimitGrothendieck G) : colimit (grothendieckProj L ⋙ G) ⟶ colimit G) :
              colimit (Grothendieck.pre (functor L) R ⋙ grothendieckProj L ⋙ G) ⟶ colimit G) :
          colimit (Grothendieck.pre (functor L) R ⋙ grothendieckProj L ⋙ G) ⟶ colimit G)))

Tactic:
change _ = colimit.ι (fst L R ⋙ G)
    ((grothendieckPrecompFunctorToComma L R).obj ⟨b, CostructuredArrow.mk f⟩) ≫ _

Premises used: CategoryTheory.CostructuredArrow.grothendieckPrecompFunctorToComma, CategoryTheory.Comma.fst, CategoryTheory.Functor.comp, CategoryTheory.Grothendieck.mk, CategoryTheory.CostructuredArrow.mk, CategoryTheory.Functor.obj, CategoryTheory.Limits.colimit.ι