-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Final
Goal:
A : Type u₁
inst : SmallCategory A
B : Type u₁
inst_1 : SmallCategory B
T : Type u₁
inst_2 : SmallCategory T
L : A ⥤ T
R : B ⥤ T
inst_3 : R.Final
inst_4 : ∀ (b : B), Final (C := CostructuredArrow L (R.obj b)) (CostructuredArrow.toOver L (R.obj b))
G : T ⥤ Type u₁
this : ∀ (b : B), ((R.whiskerLeft (preFunctor L (𝟭 T))).app b).toFunctor.Final
i : colimit (L ⋙ G) ≅ colimit G :=
  Trans.trans (r := Iso) (s := Iso) (t := fun (x1 x2 : Type u₁) ↦ x1 ≅ x2) (b :=
    colimit (J := Grothendieck (functor (𝟭 T))) (grothendieckProj (𝟭 T) ⋙ G))
    (Trans.trans (r := Iso) (s := Iso) (t := fun (x1 x2 : Type u₁) ↦ x1 ≅ x2) (b :=
        colimit (J := Grothendieck (R ⋙ functor (𝟭 T)))
          (Grothendieck.pre (functor (𝟭 T)) R ⋙ grothendieckProj (𝟭 T) ⋙ G))
        (Trans.trans (r := Iso) (s := Iso) (t := fun (x1 x2 : Type u₁) ↦ x1 ≅ x2) (b :=
          colimit (J := Grothendieck (R ⋙ functor (𝟭 T)))
            (grothendieckPrecompFunctorToComma (𝟭 T) R ⋙ Comma.fst (𝟭 T) R ⋙ G))
          (Trans.trans (r := Iso) (s := Iso) (t := fun (x1 x2 : Type u₁) ↦ x1 ≅ x2) (b :=
            colimit
              (Grothendieck.map (R.whiskerLeft (preFunctor L (𝟭 T))) ⋙
                grothendieckPrecompFunctorToComma (𝟭 T) R ⋙ Comma.fst (𝟭 T) R ⋙ G))
            (Trans.trans (r := Iso) (s := Iso) (t := fun (x1 x2 : Type u₁) ↦ x1 ≅ x2) (b :=
                colimit (Grothendieck.pre (functor L) R ⋙ grothendieckProj L ⋙ L ⋙ G))
                (Trans.trans (r := Iso) (s := Iso) (t := fun (x1 x2 : Type u₁) ↦ x1 ≅ x2) (b :=
                    colimit (grothendieckProj L ⋙ L ⋙ G))
                    (L.colimitIsoColimitGrothendieck (L ⋙ G) : colimit (L ⋙ G) ≅ colimit (grothendieckProj L ⋙ L ⋙ G))
                    (Iso.symm (Final.colimitIso (Grothendieck.pre (functor L) R) (grothendieckProj L ⋙ L ⋙ G)) :
                      colimit (grothendieckProj L ⋙ L ⋙ G) ≅
                        colimit (Grothendieck.pre (functor L) R ⋙ grothendieckProj L ⋙ L ⋙ G)) :
                  colimit (L ⋙ G) ≅ colimit (Grothendieck.pre (functor L) R ⋙ grothendieckProj L ⋙ L ⋙ G))
                (HasColimit.isoOfNatIso
                    (NatIso.ofComponents
                      (fun (x : Grothendieck (R ⋙ functor L)) ↦
                        Iso.refl ((Grothendieck.pre (functor L) R ⋙ grothendieckProj L ⋙ L ⋙ G).obj x))
                      ⋯) :
                  colimit (Grothendieck.pre (functor L) R ⋙ grothendieckProj L ⋙ L ⋙ G) ≅
                    colimit
                      (Grothendieck.map (R.whiskerLeft (preFunctor L (𝟭 T))) ⋙
                        grothendieckPrecompFunctorToComma (𝟭 T) R ⋙ Comma.fst (𝟭 T) R ⋙ G)) :
              colimit (L ⋙ G) ≅
                colimit
                  (Grothendieck.map (R.whiskerLeft (preFunctor L (𝟭 T))) ⋙
                    grothendieckPrecompFunctorToComma (𝟭 T) R ⋙ Comma.fst (𝟭 T) R ⋙ G))
            (Final.colimitIso (Grothendieck.map (R.whiskerLeft (preFunctor L (𝟭 T))))
                (grothendieckPrecompFunctorToComma (𝟭 T) R ⋙ Comma.fst (𝟭 T) R ⋙ G) :
              colimit
                  (Grothendieck.map (R.whiskerLeft (preFunctor L (𝟭 T))) ⋙
                    grothendieckPrecompFunctorToComma (𝟭 T) R ⋙ Comma.fst (𝟭 T) R ⋙ G) ≅
                colimit (J := Grothendieck (R ⋙ functor (𝟭 T)))
                  (grothendieckPrecompFunctorToComma (𝟭 T) R ⋙ Comma.fst (𝟭 T) R ⋙ G)))
          (HasColimit.isoOfNatIso (Iso.refl (grothendieckPrecompFunctorToComma (𝟭 T) R ⋙ Comma.fst (𝟭 T) R ⋙ G))))
        (Final.colimitIso (Grothendieck.pre (functor (𝟭 T)) R) (grothendieckProj (𝟭 T) ⋙ G)) :
      colimit (L ⋙ G) ≅ colimit (J := Grothendieck (functor (𝟭 T))) (grothendieckProj (𝟭 T) ⋙ G))
    (Iso.symm (colimitIsoColimitGrothendieck (𝟭 T) G) :
      colimit (J := Grothendieck (functor (𝟭 T))) (grothendieckProj (𝟭 T) ⋙ G) ≅ colimit G)
⊢ Eq (α := colimit (Grothendieck.pre (functor L) R ⋙ grothendieckProj L ⋙ L ⋙ G) ⟶ colimit G)
    (CategoryStruct.comp (Y := colimit (grothendieckProj L ⋙ L ⋙ G))
        (Iso.hom (Final.colimitIso (Grothendieck.pre (functor L) R) (grothendieckProj L ⋙ L ⋙ G)) :
          colimit (Grothendieck.pre (functor L) R ⋙ grothendieckProj L ⋙ L ⋙ G) ⟶ colimit (grothendieckProj L ⋙ L ⋙ G))
        (CategoryStruct.comp (Y := colimit (L ⋙ G))
            (Iso.inv (L.colimitIsoColimitGrothendieck (L ⋙ G)) : colimit (grothendieckProj L ⋙ L ⋙ G) ⟶ colimit (L ⋙ G))
            (colimit.pre G L : colimit (L ⋙ G) ⟶ colimit G) :
          colimit (grothendieckProj L ⋙ L ⋙ G) ⟶ colimit G) :
      colimit (Grothendieck.pre (functor L) R ⋙ grothendieckProj L ⋙ L ⋙ G) ⟶ colimit G)
    (CategoryStruct.comp (Y :=
        colimit
          (Grothendieck.map (R.whiskerLeft (preFunctor L (𝟭 T))) ⋙
            grothendieckPrecompFunctorToComma (𝟭 T) R ⋙ Comma.fst (𝟭 T) R ⋙ G))
        (Iso.hom
            (HasColimit.isoOfNatIso
              (NatIso.ofComponents (fun (x : Grothendieck (R ⋙ functor L)) ↦ Iso.refl (G.obj (L.obj (left x.fiber))))
                ⋯)) :
          colimit (Grothendieck.pre (functor L) R ⋙ grothendieckProj L ⋙ L ⋙ G) ⟶
            colimit
              (Grothendieck.map (R.whiskerLeft (preFunctor L (𝟭 T))) ⋙
                grothendieckPrecompFunctorToComma (𝟭 T) R ⋙ Comma.fst (𝟭 T) R ⋙ G))
        (CategoryStruct.comp (Y :=
            colimit (J := Grothendieck (R ⋙ functor (𝟭 T)))
              (grothendieckPrecompFunctorToComma (𝟭 T) R ⋙ Comma.fst (𝟭 T) R ⋙ G))
            (Iso.hom
              (Final.colimitIso (Grothendieck.map (R.whiskerLeft (preFunctor L (𝟭 T))))
                (grothendieckPrecompFunctorToComma (𝟭 T) R ⋙ Comma.fst (𝟭 T) R ⋙ G)))
            (CategoryStruct.comp (Y :=
              colimit (J := Grothendieck (R ⋙ functor (𝟭 T)))
                (Grothendieck.pre (functor (𝟭 T)) R ⋙ grothendieckProj (𝟭 T) ⋙ G))
              (Iso.hom
                (HasColimit.isoOfNatIso (Iso.refl (grothendieckPrecompFunctorToComma (𝟭 T) R ⋙ Comma.fst (𝟭 T) R ⋙ G))))
              (CategoryStruct.comp (Y := colimit (J := Grothendieck (functor (𝟭 T))) (grothendieckProj (𝟭 T) ⋙ G))
                (Iso.hom (Final.colimitIso (Grothendieck.pre (functor (𝟭 T)) R) (grothendieckProj (𝟭 T) ⋙ G)) :
                  colimit (J := Grothendieck (R ⋙ functor (𝟭 T)))
                      (Grothendieck.pre (functor (𝟭 T)) R ⋙ grothendieckProj (𝟭 T) ⋙ G) ⟶
                    colimit (J := Grothendieck (functor (𝟭 T))) (grothendieckProj (𝟭 T) ⋙ G))
                (Iso.inv (colimitIsoColimitGrothendieck (𝟭 T) G) :
                  colimit (J := Grothendieck (functor (𝟭 T))) (grothendieckProj (𝟭 T) ⋙ G) ⟶ colimit G))) :
          colimit
              (Grothendieck.map (R.whiskerLeft (preFunctor L (𝟭 T))) ⋙
                grothendieckPrecompFunctorToComma (𝟭 T) R ⋙ Comma.fst (𝟭 T) R ⋙ G) ⟶
            colimit G) :
      colimit (Grothendieck.pre (functor L) R ⋙ grothendieckProj L ⋙ L ⋙ G) ⟶ colimit G)

Tactic:
apply colimit.hom_ext (fun _ => by simp)

Premises used: CategoryTheory.Limits.colimit.hom_ext