-- Mathlib/CategoryTheory/Comma/Final.lean
private lemma final_fst_small [R.Final] : (fst L R).Final

Proof state:
A : Type v₁
inst✝³ : Category.{v₁, v₁} A
B : Type v₁
inst✝² : Category.{v₁, v₁} B
T : Type v₁
inst✝¹ : Category.{v₁, v₁} T
L : A ⥤ T
R : B ⥤ T
inst✝ : R.Final
⊢ ∀ (G : A ⥤ Type v₁), IsIso (colimit.pre G (fst L R))

Tactic:
intro G

Result:
A : Type v₁
inst✝³ : Category.{v₁, v₁} A
B : Type v₁
inst✝² : Category.{v₁, v₁} B
T : Type v₁
inst✝¹ : Category.{v₁, v₁} T
L : A ⥤ T
R : B ⥤ T
inst✝ : R.Final
G : A ⥤ Type v₁
⊢ IsIso (colimit.pre G (fst L R))

Proof state:
case h.e'_5.w
A : Type v₁
inst✝³ : Category.{v₁, v₁} A
B : Type v₁
inst✝² : Category.{v₁, v₁} B
T : Type v₁
inst✝¹ : Category.{v₁, v₁} T
L : A ⥤ T
R : B ⥤ T
inst✝ : R.Final
G : A ⥤ Type v₁
i : colimit G ≅ colimit (fst L R ⋙ G) :=
  L.colimitIsoColimitGrothendieck G ≪≫
    (Final.colimitIso (Grothendieck.pre (functor L) R) (grothendieckProj L ⋙ G)).symm ≪≫
      HasColimit.isoOfNatIso (Iso.refl (Grothendieck.pre (functor L) R ⋙ grothendieckProj L ⋙ G)) ≪≫
        Final.colimitIso (grothendieckPrecompFunctorEquivalence L R).functor (fst L R ⋙ G)
a : A
b : B
f : L.obj a ⟶ R.obj b
⊢ colimit.ι (fst L R ⋙ G) { left := a, right := b, hom := f } ≫ colimit.pre G (fst L R) =
    colimit.ι (fst L R ⋙ G) { left := a, right := b, hom := f } ≫ i.inv

Tactic:
simp only [colimit.ι_pre, comp_obj, fst_obj, grothendieckPrecompFunctorEquivalence_functor,
  Iso.trans_inv, Iso.symm_inv, Category.assoc, i]

Result:
case h.e'_5.w
A : Type v₁
inst✝³ : Category.{v₁, v₁} A
B : Type v₁
inst✝² : Category.{v₁, v₁} B
T : Type v₁
inst✝¹ : Category.{v₁, v₁} T
L : A ⥤ T
R : B ⥤ T
inst✝ : R.Final
G : A ⥤ Type v₁
i : colimit G ≅ colimit (fst L R ⋙ G) :=
  L.colimitIsoColimitGrothendieck G ≪≫
    (Final.colimitIso (Grothendieck.pre (functor L) R) (grothendieckProj L ⋙ G)).symm ≪≫
      HasColimit.isoOfNatIso (Iso.refl (Grothendieck.pre (functor L) R ⋙ grothendieckProj L ⋙ G)) ≪≫
        Final.colimitIso (grothendieckPrecompFunctorEquivalence L R).functor (fst L R ⋙ G)
a : A
b : B
f : L.obj a ⟶ R.obj b
⊢ colimit.ι G a =
    colimit.ι (fst L R ⋙ G) { left := a, right := b, hom := f } ≫
      (Final.colimitIso (grothendieckPrecompFunctorToComma L R) (fst L R ⋙ G)).inv ≫
        (HasColimit.isoOfNatIso (Iso.refl (Grothendieck.pre (functor L) R ⋙ grothendieckProj L ⋙ G))).inv ≫
          (Final.colimitIso (Grothendieck.pre (functor L) R) (grothendieckProj L ⋙ G)).hom ≫
            (L.colimitIsoColimitGrothendieck G).inv

Proof state:
A : Type v₁
inst✝³ : Category.{v₁, v₁} A
B : Type v₁
inst✝² : Category.{v₁, v₁} B
T : Type v₁
inst✝¹ : Category.{v₁, v₁} T
L : A ⥤ T
R : B ⥤ T
inst✝ : R.Final
⊢ (fst L R).Final

Tactic:
rw  [Functor.final_iff_isIso_colimit_pre]

Result:
A : Type v₁
inst✝³ : Category.{v₁, v₁} A
B : Type v₁
inst✝² : Category.{v₁, v₁} B
T : Type v₁
inst✝¹ : Category.{v₁, v₁} T
L : A ⥤ T
R : B ⥤ T
inst✝ : R.Final
⊢ ∀ (G : A ⥤ Type v₁), IsIso (colimit.pre G (fst L R))

Proof state:
A : Type v₁
inst✝³ : Category.{v₁, v₁} A
B : Type v₁
inst✝² : Category.{v₁, v₁} B
T : Type v₁
inst✝¹ : Category.{v₁, v₁} T
L : A ⥤ T
R : B ⥤ T
inst✝ : R.Final
G : A ⥤ Type v₁
i : colimit G ≅ colimit (fst L R ⋙ G) :=
  L.colimitIsoColimitGrothendieck G ≪≫
    (Final.colimitIso (Grothendieck.pre (functor L) R) (grothendieckProj L ⋙ G)).symm ≪≫
      HasColimit.isoOfNatIso (Iso.refl (Grothendieck.pre (functor L) R ⋙ grothendieckProj L ⋙ G)) ≪≫
        Final.colimitIso (grothendieckPrecompFunctorEquivalence L R).functor (fst L R ⋙ G)
⊢ IsIso (colimit.pre G (fst L R))

Tactic:
convert i.isIso_inv

Result:
case h.e'_5
A : Type v₁
inst✝³ : Category.{v₁, v₁} A
B : Type v₁
inst✝² : Category.{v₁, v₁} B
T : Type v₁
inst✝¹ : Category.{v₁, v₁} T
L : A ⥤ T
R : B ⥤ T
inst✝ : R.Final
G : A ⥤ Type v₁
i : colimit G ≅ colimit (fst L R ⋙ G) :=
  L.colimitIsoColimitGrothendieck G ≪≫
    (Final.colimitIso (Grothendieck.pre (functor L) R) (grothendieckProj L ⋙ G)).symm ≪≫
      HasColimit.isoOfNatIso (Iso.refl (Grothendieck.pre (functor L) R ⋙ grothendieckProj L ⋙ G)) ≪≫
        Final.colimitIso (grothendieckPrecompFunctorEquivalence L R).functor (fst L R ⋙ G)
⊢ colimit.pre G (fst L R) = i.inv

Proof state:
case h.e'_5.w
A : Type v₁
inst✝³ : Category.{v₁, v₁} A
B : Type v₁
inst✝² : Category.{v₁, v₁} B
T : Type v₁
inst✝¹ : Category.{v₁, v₁} T
L : A ⥤ T
R : B ⥤ T
inst✝ : R.Final
G : A ⥤ Type v₁
i : colimit G ≅ colimit (fst L R ⋙ G) :=
  L.colimitIsoColimitGrothendieck G ≪≫
    (Final.colimitIso (Grothendieck.pre (functor L) R) (grothendieckProj L ⋙ G)).symm ≪≫
      HasColimit.isoOfNatIso (Iso.refl (Grothendieck.pre (functor L) R ⋙ grothendieckProj L ⋙ G)) ≪≫
        Final.colimitIso (grothendieckPrecompFunctorEquivalence L R).functor (fst L R ⋙ G)
a : A
b : B
f : L.obj a ⟶ R.obj b
⊢ colimit.ι G a =
    colimit.ι (fst L R ⋙ G) { left := a, right := b, hom := f } ≫
      (Final.colimitIso (grothendieckPrecompFunctorToComma L R) (fst L R ⋙ G)).inv ≫
        (HasColimit.isoOfNatIso (Iso.refl (Grothendieck.pre (functor L) R ⋙ grothendieckProj L ⋙ G))).inv ≫
          (Final.colimitIso (Grothendieck.pre (functor L) R) (grothendieckProj L ⋙ G)).hom ≫
            (L.colimitIsoColimitGrothendieck G).inv

Tactic:
change _ = colimit.ι (fst L R ⋙ G)
  ((grothendieckPrecompFunctorToComma L R).obj ⟨b, CostructuredArrow.mk f⟩) ≫ _

Result:
case h.e'_5.w
A : Type v₁
inst✝³ : Category.{v₁, v₁} A
B : Type v₁
inst✝² : Category.{v₁, v₁} B
T : Type v₁
inst✝¹ : Category.{v₁, v₁} T
L : A ⥤ T
R : B ⥤ T
inst✝ : R.Final
G : A ⥤ Type v₁
i : colimit G ≅ colimit (fst L R ⋙ G) :=
  L.colimitIsoColimitGrothendieck G ≪≫
    (Final.colimitIso (Grothendieck.pre (functor L) R) (grothendieckProj L ⋙ G)).symm ≪≫
      HasColimit.isoOfNatIso (Iso.refl (Grothendieck.pre (functor L) R ⋙ grothendieckProj L ⋙ G)) ≪≫
        Final.colimitIso (grothendieckPrecompFunctorEquivalence L R).functor (fst L R ⋙ G)
a : A
b : B
f : L.obj a ⟶ R.obj b
⊢ colimit.ι G a =
    colimit.ι (fst L R ⋙ G)
        ((grothendieckPrecompFunctorToComma L R).obj { base := b, fiber := CostructuredArrow.mk f }) ≫
      (Final.colimitIso (grothendieckPrecompFunctorToComma L R) (fst L R ⋙ G)).inv ≫
        (HasColimit.isoOfNatIso (Iso.refl (Grothendieck.pre (functor L) R ⋙ grothendieckProj L ⋙ G))).inv ≫
          (Final.colimitIso (Grothendieck.pre (functor L) R) (grothendieckProj L ⋙ G)).hom ≫
            (L.colimitIsoColimitGrothendieck G).inv

Proof state:
case h.e'_5
A : Type v₁
inst✝³ : Category.{v₁, v₁} A
B : Type v₁
inst✝² : Category.{v₁, v₁} B
T : Type v₁
inst✝¹ : Category.{v₁, v₁} T
L : A ⥤ T
R : B ⥤ T
inst✝ : R.Final
G : A ⥤ Type v₁
i : colimit G ≅ colimit (fst L R ⋙ G) :=
  L.colimitIsoColimitGrothendieck G ≪≫
    (Final.colimitIso (Grothendieck.pre (functor L) R) (grothendieckProj L ⋙ G)).symm ≪≫
      HasColimit.isoOfNatIso (Iso.refl (Grothendieck.pre (functor L) R ⋙ grothendieckProj L ⋙ G)) ≪≫
        Final.colimitIso (grothendieckPrecompFunctorEquivalence L R).functor (fst L R ⋙ G)
⊢ colimit.pre G (fst L R) = i.inv

Tactic:
apply colimit.hom_ext

Result:
case h.e'_5.w
A : Type v₁
inst✝³ : Category.{v₁, v₁} A
B : Type v₁
inst✝² : Category.{v₁, v₁} B
T : Type v₁
inst✝¹ : Category.{v₁, v₁} T
L : A ⥤ T
R : B ⥤ T
inst✝ : R.Final
G : A ⥤ Type v₁
i : colimit G ≅ colimit (fst L R ⋙ G) :=
  L.colimitIsoColimitGrothendieck G ≪≫
    (Final.colimitIso (Grothendieck.pre (functor L) R) (grothendieckProj L ⋙ G)).symm ≪≫
      HasColimit.isoOfNatIso (Iso.refl (Grothendieck.pre (functor L) R ⋙ grothendieckProj L ⋙ G)) ≪≫
        Final.colimitIso (grothendieckPrecompFunctorEquivalence L R).functor (fst L R ⋙ G)
⊢ ∀ (j : Comma L R), colimit.ι (fst L R ⋙ G) j ≫ colimit.pre G (fst L R) = colimit.ι (fst L R ⋙ G) j ≫ i.inv