-- 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 : colimit.pre G L = i.hom
⊢ IsIso (X := colimit (L ⋙ G)) (Y := colimit G) (colimit.pre G L)

Tactic:
convert! Iso.isIso_hom i

Premises used: CategoryTheory.Iso.isIso_hom