-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.StructuredArrow.Final (goal)
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)
⊢ colimit.pre G L = i.hom
have 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)))) sorry)) :
                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)
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]