-- Mathlib/CategoryTheory/Comma/StructuredArrow/Final.lean
/-- The version of `final_of_final_costructuredArrowToOver` on small categories used to prove the
full statement. -/
private lemma final_of_final_costructuredArrowToOver_small (L : A ⥤ T) (R : B ⥤ T) [Final R]
    [∀ b : B, Final (CostructuredArrow.toOver L (R.obj b))] : Final L

Proof state:
case h.e'_5
A : Type u₁
inst✝⁴ : SmallCategory A
B : Type u₁
inst✝³ : SmallCategory B
T : Type u₁
inst✝² : SmallCategory T
L : A ⥤ T
R : B ⥤ T
inst✝¹ : R.Final
inst✝ : ∀ (b : B), (CostructuredArrow.toOver L (R.obj b)).Final
G : T ⥤ Type u₁
this : ∀ (b : B), Final ((whiskerLeft R (preFunctor L (𝟭 T))).app b)
i : colimit (L ⋙ G) ≅ colimit G :=
  Trans.trans
    (Trans.trans
      (Trans.trans
        (Trans.trans
          (Trans.trans
            (Trans.trans (L.colimitIsoColimitGrothendieck (L ⋙ G))
              (Final.colimitIso (Grothendieck.pre (functor L) R) (grothendieckProj L ⋙ L ⋙ G)).symm)
            (HasColimit.isoOfNatIso
              (NatIso.ofComponents
                (fun x => Iso.refl ((Grothendieck.pre (functor L) R ⋙ grothendieckProj L ⋙ L ⋙ G).obj x)) ⋯)))
          (Final.colimitIso (Grothendieck.map (whiskerLeft R (preFunctor L (𝟭 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)))
    ((𝟭 T).colimitIsoColimitGrothendieck G).symm
⊢ colimit.pre G L = i.hom

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

Result:
case h.e'_5
A : Type u₁
inst✝⁴ : SmallCategory A
B : Type u₁
inst✝³ : SmallCategory B
T : Type u₁
inst✝² : SmallCategory T
L : A ⥤ T
R : B ⥤ T
inst✝¹ : R.Final
inst✝ : ∀ (b : B), (CostructuredArrow.toOver L (R.obj b)).Final
G : T ⥤ Type u₁
this : ∀ (b : B), Final ((whiskerLeft R (preFunctor L (𝟭 T))).app b)
i : colimit (L ⋙ G) ≅ colimit G :=
  Trans.trans
    (Trans.trans
      (Trans.trans
        (Trans.trans
          (Trans.trans
            (Trans.trans (L.colimitIsoColimitGrothendieck (L ⋙ G))
              (Final.colimitIso (Grothendieck.pre (functor L) R) (grothendieckProj L ⋙ L ⋙ G)).symm)
            (HasColimit.isoOfNatIso
              (NatIso.ofComponents
                (fun x => Iso.refl ((Grothendieck.pre (functor L) R ⋙ grothendieckProj L ⋙ L ⋙ G).obj x)) ⋯)))
          (Final.colimitIso (Grothendieck.map (whiskerLeft R (preFunctor L (𝟭 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)))
    ((𝟭 T).colimitIsoColimitGrothendieck G).symm
⊢ colimit.pre G L =
    (L.colimitIsoColimitGrothendieck (L ⋙ G)).hom ≫
      (Final.colimitIso (Grothendieck.pre (functor L) R) (grothendieckProj L ⋙ L ⋙ G)).inv ≫
        (HasColimit.isoOfNatIso (NatIso.ofComponents (fun x => Iso.refl (G.obj (L.obj x.fiber.left))) ⋯)).hom ≫
          (Final.colimitIso (Grothendieck.map (whiskerLeft R (preFunctor L (𝟭 T))))
                (grothendieckPrecompFunctorToComma (𝟭 T) R ⋙ Comma.fst (𝟭 T) R ⋙ G)).hom ≫
            (HasColimit.isoOfNatIso
                  (Iso.refl (grothendieckPrecompFunctorToComma (𝟭 T) R ⋙ Comma.fst (𝟭 T) R ⋙ G))).hom ≫
              (Final.colimitIso (Grothendieck.pre (functor (𝟭 T)) R) (grothendieckProj (𝟭 T) ⋙ G)).hom ≫
                ((𝟭 T).colimitIsoColimitGrothendieck G).inv

Proof state:
A : Type u₁
inst✝⁴ : SmallCategory A
B : Type u₁
inst✝³ : SmallCategory B
T : Type u₁
inst✝² : SmallCategory T
L : A ⥤ T
R : B ⥤ T
inst✝¹ : R.Final
inst✝ : ∀ (b : B), (CostructuredArrow.toOver L (R.obj b)).Final
G : T ⥤ Type u₁
this : ∀ (b : B), Final ((whiskerLeft R (preFunctor L (𝟭 T))).app b)
i : colimit (L ⋙ G) ≅ colimit G :=
  Trans.trans
    (Trans.trans
      (Trans.trans
        (Trans.trans
          (Trans.trans
            (Trans.trans (L.colimitIsoColimitGrothendieck (L ⋙ G))
              (Final.colimitIso (Grothendieck.pre (functor L) R) (grothendieckProj L ⋙ L ⋙ G)).symm)
            (HasColimit.isoOfNatIso
              (NatIso.ofComponents
                (fun x => Iso.refl ((Grothendieck.pre (functor L) R ⋙ grothendieckProj L ⋙ L ⋙ G).obj x)) ⋯)))
          (Final.colimitIso (Grothendieck.map (whiskerLeft R (preFunctor L (𝟭 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)))
    ((𝟭 T).colimitIsoColimitGrothendieck G).symm
x✝ : Grothendieck (R ⋙ functor L)
⊢ colimit.ι (Grothendieck.pre (functor L) R ⋙ grothendieckProj L ⋙ L ⋙ G) x✝ ≫
      (Final.colimitIso (Grothendieck.pre (functor L) R) (grothendieckProj L ⋙ L ⋙ G)).hom ≫
        (L.colimitIsoColimitGrothendieck (L ⋙ G)).inv ≫ colimit.pre G L =
    colimit.ι (Grothendieck.pre (functor L) R ⋙ grothendieckProj L ⋙ L ⋙ G) x✝ ≫
      (HasColimit.isoOfNatIso (NatIso.ofComponents (fun x => Iso.refl (G.obj (L.obj x.fiber.left))) ⋯)).hom ≫
        (Final.colimitIso (Grothendieck.map (whiskerLeft R (preFunctor L (𝟭 T))))
              (grothendieckPrecompFunctorToComma (𝟭 T) R ⋙ Comma.fst (𝟭 T) R ⋙ G)).hom ≫
          (HasColimit.isoOfNatIso (Iso.refl (grothendieckPrecompFunctorToComma (𝟭 T) R ⋙ Comma.fst (𝟭 T) R ⋙ G))).hom ≫
            (Final.colimitIso (Grothendieck.pre (functor (𝟭 T)) R) (grothendieckProj (𝟭 T) ⋙ G)).hom ≫
              ((𝟭 T).colimitIsoColimitGrothendieck G).inv

Tactic:
simp

Result:
no goals