-- Mathlib/CategoryTheory/Limits/Final.lean
/-- This is the small version of the more general lemma `Grothendieck.final_map` below. -/
private lemma Grothendieck.final_map_small {C : Type u₁} [SmallCategory C] {F G : C ⥤ Cat.{u₁, u₁}}
    (α : F ⟶ G) [hα : ∀ X, Final (α.app X)] : Final (map α)

Proof state:
C : Type u₁
inst✝ : SmallCategory C
F G : C ⥤ Cat
α : F ⟶ G
hα : ∀ (X : C), Final (α.app X)
H : Grothendieck G ⥤ Type u₁
⊢ IsIso (colimit.pre H (map α))

Tactic:
let i := (colimitFiberwiseColimitIso _).symm ≪≫
  HasColimit.isoOfNatIso (fiberwiseColimitMapCompEquivalence α H) ≪≫ colimitFiberwiseColimitIso _

Result:
C : Type u₁
inst✝ : SmallCategory C
F G : C ⥤ Cat
α : F ⟶ G
hα : ∀ (X : C), Final (α.app X)
H : Grothendieck G ⥤ Type u₁
i : colimit (map α ⋙ H) ≅ colimit H :=
  (colimitFiberwiseColimitIso (map α ⋙ H)).symm ≪≫
    HasColimit.isoOfNatIso (fiberwiseColimitMapCompEquivalence α H) ≪≫ colimitFiberwiseColimitIso H
⊢ IsIso (colimit.pre H (map α))

Proof state:
case h.e'_5.w
C : Type u₁
inst✝ : SmallCategory C
F G : C ⥤ Cat
α : F ⟶ G
hα : ∀ (X : C), Final (α.app X)
H : Grothendieck G ⥤ Type u₁
i : colimit (map α ⋙ H) ≅ colimit H :=
  (colimitFiberwiseColimitIso (map α ⋙ H)).symm ≪≫
    HasColimit.isoOfNatIso (fiberwiseColimitMapCompEquivalence α H) ≪≫ colimitFiberwiseColimitIso H
⊢ ∀ (j : Grothendieck F), colimit.ι (map α ⋙ H) j ≫ colimit.pre H (map α) = colimit.ι (map α ⋙ H) j ≫ i.hom

Tactic:
intro X

Result:
case h.e'_5.w
C : Type u₁
inst✝ : SmallCategory C
F G : C ⥤ Cat
α : F ⟶ G
hα : ∀ (X : C), Final (α.app X)
H : Grothendieck G ⥤ Type u₁
i : colimit (map α ⋙ H) ≅ colimit H :=
  (colimitFiberwiseColimitIso (map α ⋙ H)).symm ≪≫
    HasColimit.isoOfNatIso (fiberwiseColimitMapCompEquivalence α H) ≪≫ colimitFiberwiseColimitIso H
X : Grothendieck F
⊢ colimit.ι (map α ⋙ H) X ≫ colimit.pre H (map α) = colimit.ι (map α ⋙ H) X ≫ i.hom

Proof state:
case h.e'_5.w
C : Type u₁
inst✝ : SmallCategory C
F G : C ⥤ Cat
α : F ⟶ G
hα : ∀ (X : C), Final (α.app X)
H : Grothendieck G ⥤ Type u₁
i : colimit (map α ⋙ H) ≅ colimit H :=
  (colimitFiberwiseColimitIso (map α ⋙ H)).symm ≪≫
    HasColimit.isoOfNatIso (fiberwiseColimitMapCompEquivalence α H) ≪≫ colimitFiberwiseColimitIso H
X : Grothendieck F
⊢ colimit.ι (map α ⋙ H) X ≫ colimit.pre H (map α) = colimit.ι (map α ⋙ H) X ≫ i.hom

Tactic:
simp [i, fiberwiseColimitMapCompEquivalence]

Result:
no goals

Proof state:
C : Type u₁
inst✝ : SmallCategory C
F G : C ⥤ Cat
α : F ⟶ G
hα : ∀ (X : C), Final (α.app X)
⊢ (map α).Final

Tactic:
rw [final_iff_isIso_colimit_pre]

Result:
C : Type u₁
inst✝ : SmallCategory C
F G : C ⥤ Cat
α : F ⟶ G
hα : ∀ (X : C), Final (α.app X)
⊢ ∀ (G_1 : Grothendieck G ⥤ Type u₁), IsIso (colimit.pre G_1 (map α))

Proof state:
C : Type u₁
inst✝ : SmallCategory C
F G : C ⥤ Cat
α : F ⟶ G
hα : ∀ (X : C), Final (α.app X)
⊢ ∀ (G_1 : Grothendieck G ⥤ Type u₁), IsIso (colimit.pre G_1 (map α))

Tactic:
intro H

Result:
C : Type u₁
inst✝ : SmallCategory C
F G : C ⥤ Cat
α : F ⟶ G
hα : ∀ (X : C), Final (α.app X)
H : Grothendieck G ⥤ Type u₁
⊢ IsIso (colimit.pre H (map α))

Proof state:
case h.e'_5
C : Type u₁
inst✝ : SmallCategory C
F G : C ⥤ Cat
α : F ⟶ G
hα : ∀ (X : C), Final (α.app X)
H : Grothendieck G ⥤ Type u₁
i : colimit (map α ⋙ H) ≅ colimit H :=
  (colimitFiberwiseColimitIso (map α ⋙ H)).symm ≪≫
    HasColimit.isoOfNatIso (fiberwiseColimitMapCompEquivalence α H) ≪≫ colimitFiberwiseColimitIso H
⊢ colimit.pre H (map α) = i.hom

Tactic:
apply colimit.hom_ext

Result:
case h.e'_5.w
C : Type u₁
inst✝ : SmallCategory C
F G : C ⥤ Cat
α : F ⟶ G
hα : ∀ (X : C), Final (α.app X)
H : Grothendieck G ⥤ Type u₁
i : colimit (map α ⋙ H) ≅ colimit H :=
  (colimitFiberwiseColimitIso (map α ⋙ H)).symm ≪≫
    HasColimit.isoOfNatIso (fiberwiseColimitMapCompEquivalence α H) ≪≫ colimitFiberwiseColimitIso H
⊢ ∀ (j : Grothendieck F), colimit.ι (map α ⋙ H) j ≫ colimit.pre H (map α) = colimit.ι (map α ⋙ H) j ≫ i.hom

Proof state:
C : Type u₁
inst✝ : SmallCategory C
F G : C ⥤ Cat
α : F ⟶ G
hα : ∀ (X : C), Final (α.app X)
H : Grothendieck G ⥤ Type u₁
i : colimit (map α ⋙ H) ≅ colimit H :=
  (colimitFiberwiseColimitIso (map α ⋙ H)).symm ≪≫
    HasColimit.isoOfNatIso (fiberwiseColimitMapCompEquivalence α H) ≪≫ colimitFiberwiseColimitIso H
⊢ IsIso (colimit.pre H (map α))

Tactic:
convert Iso.isIso_hom i

Result:
case h.e'_5
C : Type u₁
inst✝ : SmallCategory C
F G : C ⥤ Cat
α : F ⟶ G
hα : ∀ (X : C), Final (α.app X)
H : Grothendieck G ⥤ Type u₁
i : colimit (map α ⋙ H) ≅ colimit H :=
  (colimitFiberwiseColimitIso (map α ⋙ H)).symm ≪≫
    HasColimit.isoOfNatIso (fiberwiseColimitMapCompEquivalence α H) ≪≫ colimitFiberwiseColimitIso H
⊢ colimit.pre H (map α) = i.hom