-- 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)
⊢ 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)
have h : 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))))
              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)
Tactic: rw [← Iso.inv_comp_eq, Iso.eq_inv_comp]