-- 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)
h :
  Eq (α := colimit (L ⋙ G) ⟶ colimit G) (colimit.pre G L : colimit (L ⋙ G) ⟶ colimit G)
    (CategoryStruct.comp (Y := colimit (grothendieckProj L ⋙ L ⋙ G))
        (Iso.hom (L.colimitIsoColimitGrothendieck (L ⋙ G)) : colimit (L ⋙ G) ⟶ colimit (grothendieckProj L ⋙ L ⋙ G))
        (CategoryStruct.comp (Y := colimit (Grothendieck.pre (functor L) R ⋙ grothendieckProj L ⋙ L ⋙ G))
            (Iso.inv (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))
            (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) :
          colimit (grothendieckProj L ⋙ L ⋙ G) ⟶ colimit G) :
      colimit (L ⋙ G) ⟶ colimit G)
⊢ colimit.pre G L = i.hom

Tactic:
simp only [Iso.trans_def, comp_obj, grothendieckProj_obj, Grothendieck.pre_obj_base,
    Grothendieck.pre_obj_fiber, Iso.trans_assoc, Iso.trans_hom, Iso.symm_hom, i]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Iso.symm_hom, CategoryTheory.Iso.trans_assoc, CategoryTheory.Iso.trans_def, CategoryTheory.Grothendieck.pre_obj_base, CategoryTheory.Iso.trans_hom, CategoryTheory.CostructuredArrow.grothendieckProj_obj, CategoryTheory.Grothendieck.pre_obj_fiber