awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Final
Goal:
C : Type u₁
inst : SmallCategory C
F G : C ⥤ Cat
α : F ⟶ G
hα : ∀ (X : C), (α.app X).toFunctor.Final
H : Grothendieck G ⥤ Type u₁
i : colimit (map α ⋙ H) ≅ colimit H :=
  Iso.trans (Y := colimit (fiberwiseColimit (map α ⋙ H))) (Iso.symm (colimitFiberwiseColimitIso (map α ⋙ H)))
    (Iso.trans (Y := colimit (fiberwiseColimit H)) (HasColimit.isoOfNatIso (fiberwiseColimitMapCompEquivalence α H))
      (colimitFiberwiseColimitIso H))
X : Grothendieck F
⊢ CategoryStruct.comp (Y := colimit (map α ⋙ H)) (colimit.ι (map α ⋙ H) X) (colimit.pre H (map α)) =
    colimit.ι (map α ⋙ H) X ≫ i.hom

Tactic:
simp [i, fiberwiseColimitMapCompEquivalence]

Premises used: CategoryTheory.Grothendieck.fiberwiseColimitMapCompEquivalence
-- Module: Mathlib.CategoryTheory.Limits.Final
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
F G : C ⥤ Cat
α : F ⟶ G
hα : ∀ (X : C), (α.app X).toFunctor.Final
sC : C ≌ AsSmall C := AsSmall.equiv
F' : AsSmall C ⥤ Cat := sC.inverse ⋙ F ⋙ Cat.asSmallFunctor
G' : AsSmall C ⥤ Cat := sC.inverse ⋙ G ⋙ Cat.asSmallFunctor
α' : F' ⟶ G' := sC.inverse.whiskerLeft (whiskerRight α Cat.asSmallFunctor)
⊢ ∀ (X : AsSmall C), (α'.app X).toFunctor.Final

Tactic:
have : ∀ X, Final (α'.app X).toFunctor := fun X =>
    inferInstanceAs (AsSmall.equiv.inverse ⋙ _ ⋙ AsSmall.equiv.functor).Final
-- Module: Mathlib.CategoryTheory.Limits.Final
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
F G : C ⥤ Cat
α : F ⟶ G
hα : ∀ (X : C), (α.app X).toFunctor.Final
sC : C ≌ AsSmall C := AsSmall.equiv
F' : AsSmall C ⥤ Cat := sC.inverse ⋙ F ⋙ Cat.asSmallFunctor
G' : AsSmall C ⥤ Cat := sC.inverse ⋙ G ⋙ Cat.asSmallFunctor
α' : F' ⟶ G' := sC.inverse.whiskerLeft (whiskerRight α Cat.asSmallFunctor)
this : ∀ (X : AsSmall C), (α'.app X).toFunctor.Final
hα' : (map (sC.symm.functor.whiskerLeft (whiskerRight α Cat.asSmallFunctor))).Final
have :
  ∀
    (i :
      map (sC.symm.functor.whiskerLeft (whiskerRight α Cat.asSmallFunctor)) ≅
        (preEquivalence (F ⋙ Cat.asSmallFunctor) sC.symm).functor ⋙
          ((compAsSmallFunctorEquivalence F).functor ⋙ map α ⋙ (compAsSmallFunctorEquivalence G).inverse) ⋙
            (preEquivalence (G ⋙ Cat.asSmallFunctor) sC.symm).inverse),
    (map α).Final
⊢ (map α).Final

Tactic:
have i := mapWhiskerLeftIsoConjPreMap sC.symm (whiskerRight α Cat.asSmallFunctor)
    ≪≫ isoWhiskerLeft _ (isoWhiskerRight (mapWhiskerRightAsSmallFunctor α) _)
-- Module: Mathlib.CategoryTheory.Limits.Final
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
F G : C ⥤ Cat
α : F ⟶ G
hα : ∀ (X : C), (α.app X).toFunctor.Final
sC : C ≌ AsSmall C := AsSmall.equiv
F' : AsSmall C ⥤ Cat := sC.inverse ⋙ F ⋙ Cat.asSmallFunctor
G' : AsSmall C ⥤ Cat := sC.inverse ⋙ G ⋙ Cat.asSmallFunctor
α' : F' ⟶ G' := sC.inverse.whiskerLeft (whiskerRight α Cat.asSmallFunctor)
this : ∀ (X : AsSmall C), (α'.app X).toFunctor.Final
hα' : (map (sC.symm.functor.whiskerLeft (whiskerRight α Cat.asSmallFunctor))).Final
i :
  map (sC.symm.functor.whiskerLeft (whiskerRight α Cat.asSmallFunctor)) ≅
    (preEquivalence (F ⋙ Cat.asSmallFunctor) sC.symm).functor ⋙
      ((compAsSmallFunctorEquivalence F).functor ⋙ map α ⋙ (compAsSmallFunctorEquivalence G).inverse) ⋙
        (preEquivalence (G ⋙ Cat.asSmallFunctor) sC.symm).inverse
⊢ ((preEquivalence (F ⋙ Cat.asSmallFunctor) sC.symm).functor ⋙
      ((compAsSmallFunctorEquivalence F).functor ⋙ map α ⋙ (compAsSmallFunctorEquivalence G).inverse) ⋙
        (preEquivalence (G ⋙ Cat.asSmallFunctor) sC.symm).inverse).Final

Tactic:
have := final_of_natIso i
-- Module: Mathlib.CategoryTheory.Limits.Final
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
F G : C ⥤ Cat
α : F ⟶ G
hα : ∀ (X : C), (α.app X).toFunctor.Final
sC : C ≌ AsSmall C := AsSmall.equiv
F' : AsSmall C ⥤ Cat := sC.inverse ⋙ F ⋙ Cat.asSmallFunctor
G' : AsSmall C ⥤ Cat := sC.inverse ⋙ G ⋙ Cat.asSmallFunctor
α' : F' ⟶ G' := sC.inverse.whiskerLeft (whiskerRight α Cat.asSmallFunctor)
this_1 : ∀ (X : AsSmall C), (α'.app X).toFunctor.Final
hα' : (map (sC.symm.functor.whiskerLeft (whiskerRight α Cat.asSmallFunctor))).Final
i :
  map (sC.symm.functor.whiskerLeft (whiskerRight α Cat.asSmallFunctor)) ≅
    (preEquivalence (F ⋙ Cat.asSmallFunctor) sC.symm).functor ⋙
      ((compAsSmallFunctorEquivalence F).functor ⋙ map α ⋙ (compAsSmallFunctorEquivalence G).inverse) ⋙
        (preEquivalence (G ⋙ Cat.asSmallFunctor) sC.symm).inverse
this :
  ((preEquivalence (F ⋙ Cat.asSmallFunctor) sC.symm).functor ⋙
      ((compAsSmallFunctorEquivalence F).functor ⋙ map α ⋙ (compAsSmallFunctorEquivalence G).inverse) ⋙
        (preEquivalence (G ⋙ Cat.asSmallFunctor) sC.symm).inverse).Final
rwa :
  ∀
    (this :
      (((compAsSmallFunctorEquivalence F).functor ⋙ map α ⋙ (compAsSmallFunctorEquivalence G).inverse) ⋙
          (preEquivalence (G ⋙ Cat.asSmallFunctor) sC.symm).inverse).Final),
    (map α).Final
rwa₁ :
  ∀ (this : ((compAsSmallFunctorEquivalence F).functor ⋙ map α ⋙ (compAsSmallFunctorEquivalence G).inverse).Final),
    (map α).Final
rwa₂ : ∀ (this : (map α ⋙ (compAsSmallFunctorEquivalence G).inverse).Final), (map α).Final
rwa₃ rwa₄ rwa₅ rwa₆ : ∀ (this : (map α).Final), (map α).Final
⊢ (map α).Final

Tactic:
rwa [← final_iff_equivalence_comp, ← final_iff_comp_equivalence,
    ← final_iff_equivalence_comp, ← final_iff_comp_equivalence] at this

Premises used: CategoryTheory.Functor.final_iff_comp_equivalence, CategoryTheory.Functor.final_iff_equivalence_comp
-- Module: Mathlib.CategoryTheory.Limits.Final
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : ObjectProperty.{v₁, u₁} C
h : ∀ (d : C), ¬P d → IsConnected (CostructuredArrow P.ι d)
d : C
pos : ∀ (hd : P d), IsConnected (CostructuredArrow P.ι d)
neg : ∀ (hd : ¬P d), IsConnected (CostructuredArrow P.ι d)
⊢ IsConnected (CostructuredArrow P.ι d)

Tactic:
by_cases hd : P d
-- Module: Mathlib.CategoryTheory.Limits.Final
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : ObjectProperty.{v₁, u₁} C
h : ∀ (d : C), ¬P d → IsConnected (CostructuredArrow P.ι d)
d : C
hd : P d
⊢ Nonempty (CostructuredArrow P.ι d)

Tactic:
have : Nonempty (CostructuredArrow P.ι d) := ⟨⟨d, hd⟩, ⟨⟨⟩⟩, 𝟙 _⟩
-- Module: Mathlib.CategoryTheory.Limits.Final
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : ObjectProperty.{v₁, u₁} C
h : ∀ (d : C), ¬P d → IsConnected (CostructuredArrow P.ι d)
d : C
hd : P d
this : Nonempty (CostructuredArrow P.ι d)
j₁ j₂ : CostructuredArrow P.ι d
⊢ CostructuredArrow P.ι d

Tactic:
exact CostructuredArrow.mk (Y := ⟨d, hd⟩) (𝟙 _)

Premises used: CategoryTheory.CategoryStruct.id, CategoryTheory.CostructuredArrow.mk
-- Module: Mathlib.CategoryTheory.Limits.Final
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : ObjectProperty.{v₁, u₁} C
h : ∀ (d : C), ¬P d → IsConnected (CostructuredArrow P.ι d)
d : C
hd : P d
this : Nonempty (CostructuredArrow P.ι d)
pos : (j₁ j₂ : CostructuredArrow P.ι d) → j₁ ⟶ CostructuredArrow.mk (𝟙 (P.ι.obj (FullSubcategory.mk (P := P) d hd)))
pos₁ : (j₁ j₂ : CostructuredArrow P.ι d) → j₂ ⟶ CostructuredArrow.mk (𝟙 (P.ι.obj (FullSubcategory.mk (P := P) d hd)))
⊢ IsConnected (CostructuredArrow P.ι d)

Tactic:
refine zigzag_isConnected (fun j₁ j₂ ↦ Zigzag.trans
      (j₂ := by exact CostructuredArrow.mk (Y := ⟨d, hd⟩) (𝟙 _)) (.of_hom ?_) (.of_inv ?_))

Premises used: CategoryTheory.zigzag_isConnected, CategoryTheory.Zigzag.trans, CategoryTheory.Zigzag.of_hom, CategoryTheory.Zigzag.of_inv
-- Module: Mathlib.CategoryTheory.Limits.Final
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : ObjectProperty.{v₁, u₁} C
h : ∀ (d : C), ¬P d → IsConnected (CostructuredArrow P.ι d)
d : C
hd : P d
this : Nonempty (CostructuredArrow P.ι d)
j₁ j₂ : CostructuredArrow P.ι d
⊢ j₁ ⟶ CostructuredArrow.mk (𝟙 (P.ι.obj (FullSubcategory.mk (P := P) d hd)))

Tactic:
exact CostructuredArrow.homMk (InducedCategory.homMk j₁.hom)

Premises used: CategoryTheory.InducedCategory.homMk, CategoryTheory.CostructuredArrow.homMk
-- Module: Mathlib.CategoryTheory.Limits.Final
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : ObjectProperty.{v₁, u₁} C
h : ∀ (d : C), ¬P d → IsConnected (CostructuredArrow P.ι d)
d : C
hd : P d
this : Nonempty (CostructuredArrow P.ι d)
j₁ j₂ : CostructuredArrow P.ι d
⊢ j₂ ⟶ CostructuredArrow.mk (𝟙 (P.ι.obj (FullSubcategory.mk (P := P) d hd)))

Tactic:
exact CostructuredArrow.homMk (InducedCategory.homMk j₂.hom)

Premises used: CategoryTheory.InducedCategory.homMk, CategoryTheory.CostructuredArrow.homMk
-- Module: Mathlib.CategoryTheory.Limits.Final
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : ObjectProperty.{v₁, u₁} C
h : ∀ (d : C), ¬P d → IsConnected (CostructuredArrow P.ι d)
d : C
hd : ¬P d
⊢ IsConnected (CostructuredArrow P.ι d)

Tactic:
h d hd
-- Module: Mathlib.CategoryTheory.Limits.Final
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : ObjectProperty.{v₁, u₁} C
h : ∀ (d : C), ¬P d → IsConnected (CostructuredArrow P.ι d)
d : C
hd : ¬P d
⊢ IsConnected (CostructuredArrow P.ι d)

Tactic:
exact h d hd
-- Module: Mathlib.CategoryTheory.Limits.Final
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
D : Functor.{v_1, v_2, u_1, u_2} J C
c : Cone D
hc : IsLimit c
j : J
inst_2 : Functor.Initial (C := Over.{v_1, u_1} j) (Over.forget j)
⊢ Nonempty (Over.{v_1, u_1} j)

Tactic:
haveI : Nonempty (Over j) := ⟨Over.mk (𝟙 j)⟩
-- Module: Mathlib.CategoryTheory.Limits.Final
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
D : Functor.{v_1, v_2, u_1, u_2} J C
c : Cone D
hc : IsLimit c
j : J
inst_2 : Functor.Initial (C := Over.{v_1, u_1} j) (Over.forget j)
this : Nonempty (Over.{v_1, u_1} j)
c'' : Cone
  (Over.lift (Over.forget j ⋙ D)
    (Functor.whiskerRight (Cocone.ι (Over.forgetCocone j)) D ≫
      Iso.hom (Functor.constComp (Over.{v_1, u_1} j) (Cocone.pt (J := Over.{v_1, u_1} j) (Over.forgetCocone j)) D))) :=
  Over.liftCone (Over.forget j ⋙ D)
    (Functor.whiskerRight (Cocone.ι (Over.forgetCocone j)) D ≫
      Iso.hom (Functor.constComp (Over.{v_1, u_1} j) (Cocone.pt (J := Over.{v_1, u_1} j) (Over.forgetCocone j)) D))
    (Cone.whisker (Over.forget j) c) (c.π.app j) ⋯
hc'' : IsLimit c'' :=
  Over.isLimitLiftCone (Over.forget j ⋙ D)
    (Functor.whiskerRight (Cocone.ι (Over.forgetCocone j)) D ≫
      Iso.hom (Functor.constComp (Over.{v_1, u_1} j) (Cocone.pt (J := Over.{v_1, u_1} j) (Over.forgetCocone j)) D))
    (Cone.whisker (Over.forget j) c) (c.π.app j) ⋯
    ((Equiv.symm (Functor.Initial.isLimitWhiskerEquiv (Over.forget j) c) :
        (a : IsLimit c) → IsLimit (Cone.whisker (Over.forget j) c))
      hc)
refine_1 :
  Over.lift (Over.forget j ⋙ D)
      (Functor.whiskerRight (Cocone.ι (Over.forgetCocone j)) D ≫
        Iso.hom (Functor.constComp (Over.{v_1, u_1} j) (Cocone.pt (J := Over.{v_1, u_1} j) (Over.forgetCocone j)) D)) ≅
    Over.post D
refine_2 :
  Functor.obj
      (Cone.postcompose
        (Iso.hom
          (NatIso.ofComponents
            (fun (k : Over.{v_1, u_1} j) ↦
              Over.isoMk
                (Iso.refl
                  ((Over.lift (Over.forget j ⋙ D)
                          (Functor.whiskerRight (Cocone.ι (Over.forgetCocone j)) D ≫
                            Iso.hom
                              (Functor.constComp (Over.{v_1, u_1} j)
                                (Cocone.pt (J := Over.{v_1, u_1} j) (Over.forgetCocone j)) D))).obj
                      k).left)
                ⋯)
            ⋯)))
      c'' ≅
    c.overPost j
⊢ IsLimit (c.overPost j)

Tactic:
refine IsLimit.equivOfNatIsoOfIso ?_ _ _ ?_ hc''

Premises used: DFunLike.coe, CategoryTheory.Limits.IsLimit.equivOfNatIsoOfIso
-- Module: Mathlib.CategoryTheory.Limits.Final
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
D : Functor.{v_1, v_2, u_1, u_2} J C
c : Cone D
hc : IsLimit c
j : J
inst_2 : Functor.Initial (C := Over.{v_1, u_1} j) (Over.forget j)
this : Nonempty (Over.{v_1, u_1} j)
c'' : Cone
  (Over.lift (Over.forget j ⋙ D)
    (Functor.whiskerRight (Cocone.ι (Over.forgetCocone j)) D ≫
      Iso.hom (Functor.constComp (Over.{v_1, u_1} j) (Cocone.pt (J := Over.{v_1, u_1} j) (Over.forgetCocone j)) D))) :=
  Over.liftCone (Over.forget j ⋙ D)
    (Functor.whiskerRight (Cocone.ι (Over.forgetCocone j)) D ≫
      Iso.hom (Functor.constComp (Over.{v_1, u_1} j) (Cocone.pt (J := Over.{v_1, u_1} j) (Over.forgetCocone j)) D))
    (Cone.whisker (Over.forget j) c) (c.π.app j) ⋯
hc'' : IsLimit c'' :=
  Over.isLimitLiftCone (Over.forget j ⋙ D)
    (Functor.whiskerRight (Cocone.ι (Over.forgetCocone j)) D ≫
      Iso.hom (Functor.constComp (Over.{v_1, u_1} j) (Cocone.pt (J := Over.{v_1, u_1} j) (Over.forgetCocone j)) D))
    (Cone.whisker (Over.forget j) c) (c.π.app j) ⋯
    ((Equiv.symm (Functor.Initial.isLimitWhiskerEquiv (Over.forget j) c) :
        (a : IsLimit c) → IsLimit (Cone.whisker (Over.forget j) c))
      hc)
⊢ Over.lift (Over.forget j ⋙ D)
      (Functor.whiskerRight (Cocone.ι (Over.forgetCocone j)) D ≫
        Iso.hom (Functor.constComp (Over.{v_1, u_1} j) (Cocone.pt (J := Over.{v_1, u_1} j) (Over.forgetCocone j)) D)) ≅
    Over.post D

Tactic:
exact NatIso.ofComponents (fun k ↦ CategoryTheory.Over.isoMk (Iso.refl _))

Premises used: CategoryTheory.Iso.refl, CategoryTheory.Over.left, CategoryTheory.Over.isoMk, CategoryTheory.Functor.obj, CategoryTheory.NatIso.ofComponents
-- Module: Mathlib.CategoryTheory.Limits.Final
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
D : Functor.{v_1, v_2, u_1, u_2} J C
c : Cone D
hc : IsLimit c
j : J
inst_2 : Functor.Initial (C := Over.{v_1, u_1} j) (Over.forget j)
this : Nonempty (Over.{v_1, u_1} j)
c'' : Cone
  (Over.lift (Over.forget j ⋙ D)
    (Functor.whiskerRight (Cocone.ι (Over.forgetCocone j)) D ≫
      Iso.hom (Functor.constComp (Over.{v_1, u_1} j) (Cocone.pt (J := Over.{v_1, u_1} j) (Over.forgetCocone j)) D))) :=
  Over.liftCone (Over.forget j ⋙ D)
    (Functor.whiskerRight (Cocone.ι (Over.forgetCocone j)) D ≫
      Iso.hom (Functor.constComp (Over.{v_1, u_1} j) (Cocone.pt (J := Over.{v_1, u_1} j) (Over.forgetCocone j)) D))
    (Cone.whisker (Over.forget j) c) (c.π.app j) ⋯
hc'' : IsLimit c'' :=
  Over.isLimitLiftCone (Over.forget j ⋙ D)
    (Functor.whiskerRight (Cocone.ι (Over.forgetCocone j)) D ≫
      Iso.hom (Functor.constComp (Over.{v_1, u_1} j) (Cocone.pt (J := Over.{v_1, u_1} j) (Over.forgetCocone j)) D))
    (Cone.whisker (Over.forget j) c) (c.π.app j) ⋯
    ((Equiv.symm (Functor.Initial.isLimitWhiskerEquiv (Over.forget j) c) :
        (a : IsLimit c) → IsLimit (Cone.whisker (Over.forget j) c))
      hc)
⊢ Functor.obj
      (Cone.postcompose
        (Iso.hom
          (NatIso.ofComponents
            (fun (k : Over.{v_1, u_1} j) ↦
              Over.isoMk
                (Iso.refl
                  ((Over.lift (Over.forget j ⋙ D)
                          (Functor.whiskerRight (Cocone.ι (Over.forgetCocone j)) D ≫
                            Iso.hom
                              (Functor.constComp (Over.{v_1, u_1} j)
                                (Cocone.pt (J := Over.{v_1, u_1} j) (Over.forgetCocone j)) D))).obj
                      k).left)
                ⋯)
            ⋯)))
      c'' ≅
    c.overPost j

Tactic:
exact Cone.ext (Iso.refl _)

Premises used: CategoryTheory.Iso.refl, CategoryTheory.Limits.Cone.ext
-- Module: Mathlib.CategoryTheory.Limits.Final
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
D : Functor.{v_1, v_2, u_1, u_2} J C
c : Cocone D
hc : IsColimit c
j : J
inst_2 : Functor.Final (C := Under.{v_1, u_1} j) (Under.forget j)
⊢ Nonempty (Under.{v_1, u_1} j)

Tactic:
haveI : Nonempty (Under j) := ⟨CategoryTheory.Under.mk (𝟙 j)⟩
-- Module: Mathlib.CategoryTheory.Limits.Final
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
D : Functor.{v_1, v_2, u_1, u_2} J C
c : Cocone D
hc : IsColimit c
j : J
inst_2 : Functor.Final (C := Under.{v_1, u_1} j) (Under.forget j)
this : Nonempty (Under.{v_1, u_1} j)
c'' : Cocone
  (Under.lift (Under.forget j ⋙ D)
    (Iso.inv (Functor.constComp (Under.{v_1, u_1} j) j D) ≫ Functor.whiskerRight (Cone.π (Under.forgetCone j)) D)) :=
  Under.liftCocone (Under.forget j ⋙ D)
    (Iso.inv (Functor.constComp (Under.{v_1, u_1} j) j D) ≫ Functor.whiskerRight (Cone.π (Under.forgetCone j)) D)
    (Cocone.whisker (Under.forget j) c) (c.ι.app j) ⋯
hc'' : IsColimit c'' :=
  Under.isColimitLiftCocone (Under.forget j ⋙ D)
    (Iso.inv (Functor.constComp (Under.{v_1, u_1} j) j D) ≫ Functor.whiskerRight (Cone.π (Under.forgetCone j)) D)
    (Cocone.whisker (Under.forget j) c) (c.ι.app j) ⋯
    ((Equiv.symm (Functor.Final.isColimitWhiskerEquiv (Under.forget j) c) :
        (a : IsColimit c) → IsColimit (Cocone.whisker (Under.forget j) c))
      hc)
refine_1 :
  Under.lift (Under.forget j ⋙ D)
      (Iso.inv (Functor.constComp (Under.{v_1, u_1} j) j D) ≫ Functor.whiskerRight (Cone.π (Under.forgetCone j)) D) ≅
    Under.post D
refine_2 :
  Functor.obj
      (Cocone.precompose
        (Iso.inv
          (NatIso.ofComponents
            (fun (k : Under.{v_1, u_1} j) ↦
              Under.isoMk
                (Iso.refl
                  ((Under.lift (Under.forget j ⋙ D)
                          (Iso.inv (Functor.constComp (Under.{v_1, u_1} j) j D) ≫
                            Functor.whiskerRight (Cone.π (Under.forgetCone j)) D)).obj
                      k).right)
                ⋯)
            ⋯)))
      c'' ≅
    c.underPost j
⊢ IsColimit (c.underPost j)

Tactic:
refine IsColimit.equivOfNatIsoOfIso ?_ _ _ ?_ hc''

Premises used: CategoryTheory.Limits.IsColimit.equivOfNatIsoOfIso, DFunLike.coe
-- Module: Mathlib.CategoryTheory.Limits.Final
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
D : Functor.{v_1, v_2, u_1, u_2} J C
c : Cocone D
hc : IsColimit c
j : J
inst_2 : Functor.Final (C := Under.{v_1, u_1} j) (Under.forget j)
this : Nonempty (Under.{v_1, u_1} j)
c'' : Cocone
  (Under.lift (Under.forget j ⋙ D)
    (Iso.inv (Functor.constComp (Under.{v_1, u_1} j) j D) ≫ Functor.whiskerRight (Cone.π (Under.forgetCone j)) D)) :=
  Under.liftCocone (Under.forget j ⋙ D)
    (Iso.inv (Functor.constComp (Under.{v_1, u_1} j) j D) ≫ Functor.whiskerRight (Cone.π (Under.forgetCone j)) D)
    (Cocone.whisker (Under.forget j) c) (c.ι.app j) ⋯
hc'' : IsColimit c'' :=
  Under.isColimitLiftCocone (Under.forget j ⋙ D)
    (Iso.inv (Functor.constComp (Under.{v_1, u_1} j) j D) ≫ Functor.whiskerRight (Cone.π (Under.forgetCone j)) D)
    (Cocone.whisker (Under.forget j) c) (c.ι.app j) ⋯
    ((Equiv.symm (Functor.Final.isColimitWhiskerEquiv (Under.forget j) c) :
        (a : IsColimit c) → IsColimit (Cocone.whisker (Under.forget j) c))
      hc)
⊢ Under.lift (Under.forget j ⋙ D)
      (Iso.inv (Functor.constComp (Under.{v_1, u_1} j) j D) ≫ Functor.whiskerRight (Cone.π (Under.forgetCone j)) D) ≅
    Under.post D

Tactic:
exact NatIso.ofComponents (fun k ↦ CategoryTheory.Under.isoMk (Iso.refl _))

Premises used: CategoryTheory.Iso.refl, CategoryTheory.Under.right, CategoryTheory.Under.isoMk, CategoryTheory.Functor.obj, CategoryTheory.NatIso.ofComponents
-- Module: Mathlib.CategoryTheory.Limits.Final
Goal:
J : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} C
D : Functor.{v_1, v_2, u_1, u_2} J C
c : Cocone D
hc : IsColimit c
j : J
inst_2 : Functor.Final (C := Under.{v_1, u_1} j) (Under.forget j)
this : Nonempty (Under.{v_1, u_1} j)
c'' : Cocone
  (Under.lift (Under.forget j ⋙ D)
    (Iso.inv (Functor.constComp (Under.{v_1, u_1} j) j D) ≫ Functor.whiskerRight (Cone.π (Under.forgetCone j)) D)) :=
  Under.liftCocone (Under.forget j ⋙ D)
    (Iso.inv (Functor.constComp (Under.{v_1, u_1} j) j D) ≫ Functor.whiskerRight (Cone.π (Under.forgetCone j)) D)
    (Cocone.whisker (Under.forget j) c) (c.ι.app j) ⋯
hc'' : IsColimit c'' :=
  Under.isColimitLiftCocone (Under.forget j ⋙ D)
    (Iso.inv (Functor.constComp (Under.{v_1, u_1} j) j D) ≫ Functor.whiskerRight (Cone.π (Under.forgetCone j)) D)
    (Cocone.whisker (Under.forget j) c) (c.ι.app j) ⋯
    ((Equiv.symm (Functor.Final.isColimitWhiskerEquiv (Under.forget j) c) :
        (a : IsColimit c) → IsColimit (Cocone.whisker (Under.forget j) c))
      hc)
⊢ Functor.obj
      (Cocone.precompose
        (Iso.inv
          (NatIso.ofComponents
            (fun (k : Under.{v_1, u_1} j) ↦
              Under.isoMk
                (Iso.refl
                  ((Under.lift (Under.forget j ⋙ D)
                          (Iso.inv (Functor.constComp (Under.{v_1, u_1} j) j D) ≫
                            Functor.whiskerRight (Cone.π (Under.forgetCone j)) D)).obj
                      k).right)
                ⋯)
            ⋯)))
      c'' ≅
    c.underPost j

Tactic:
exact Cocone.ext (Iso.refl _)

Premises used: CategoryTheory.Limits.Cocone.ext, CategoryTheory.Iso.refl
-- Module: Mathlib.CategoryTheory.Limits.Final
Goal:
C₀ : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} C₀
inst_1 : Category.{v_2, u_2} C
F : Functor.{v_1, v_2, u_1, u_2} C₀ C
X : C
inst_2 : F.Initial
Y : Over.{v_2, u_2} X
rw : IsConnected (CostructuredArrow F Y.left)
⊢ IsConnected (CostructuredArrow (CostructuredArrow.toOver F X) Y)

Tactic:
rw [isConnected_iff_of_equivalence
      (CostructuredArrow.costructuredArrowToOverEquivalence F Y)]

Premises used: CategoryTheory.isConnected_iff_of_equivalence, CategoryTheory.CostructuredArrow.costructuredArrowToOverEquivalence
-- Module: Mathlib.CategoryTheory.Limits.Final
Goal:
C₀ : Type u_1
C : Type u_2
inst : Category.{v_1, u_1} C₀
inst_1 : Category.{v_2, u_2} C
F : Functor.{v_1, v_2, u_1, u_2} C₀ C
X : C
inst_2 : F.Initial
Y : Over.{v_2, u_2} X
⊢ IsConnected (CostructuredArrow F Y.left)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Limits.FinallySmall
Goal:
J : Type u
inst : Category.{v, u} J
S : Type w
inst_1 : SmallCategory S
F : Functor.{w, v, w, u} S J
inst_2 : F.Final
⊢ FinallySmall.{w, v, u} J

Tactic:
⟨S, _, F, inferInstance⟩

Premises used: inferInstance, Exists.intro, CategoryTheory.FinallySmall.mk
-- Module: Mathlib.CategoryTheory.Limits.FinallySmall
Goal:
J : Type u
inst : Category.{v, u} J
inst_1 : FinallySmall.{w, v, u} J
⊢ Final.{w, v, w, u} (C := FinalModel.{w, v, u} J) (fromFinalModel J)

Tactic:
Classical.choose_spec (Classical.choose_spec (Classical.choose_spec
    (@FinallySmall.final_smallCategory J _ _)))

Premises used: CategoryTheory.FinalModel, CategoryTheory.fromFinalModel, Classical.choose_spec, CategoryTheory.FinallySmall.final_smallCategory
-- Module: Mathlib.CategoryTheory.Limits.FinallySmall
Goal:
J : Type u
inst : Category.{v, u} J
inst_1 : EssentiallySmall.{w, v, u} J
⊢ FinallySmall.{w, v, u} J

Tactic:
FinallySmall.mk' (equivSmallModel.{w} J).inverse

Premises used: CategoryTheory.FinallySmall.mk', CategoryTheory.equivSmallModel, CategoryTheory.Equivalence.inverse
-- Module: Mathlib.CategoryTheory.Limits.FinallySmall
Goal:
J : Type u
inst : Category.{v, u} J
K : Type u₁
inst_1 : Category.{v₁, u₁} K
inst_2 : FinallySmall.{w, v₁, u₁} K
F : Functor.{v₁, v, u₁, u} K J
inst_3 : F.Final
⊢ FinallySmall.{w, v, u} J

Tactic:
suffices Final ((fromFinalModel K) ⋙ F) from .mk' ((fromFinalModel K) ⋙ F)
  final_comp _ _

Premises used: CategoryTheory.Functor.comp, CategoryTheory.fromFinalModel, CategoryTheory.Functor.final_comp, CategoryTheory.FinallySmall.mk'
-- Module: Mathlib.CategoryTheory.Limits.FinallySmall
Goal:
J : Type u
inst : Category.{v, u} J
K : Type u₁
inst_1 : Category.{v₁, u₁} K
inst_2 : EssentiallySmall.{w, v₁, u₁} K
F : Functor.{v₁, v, u₁, u} K J
inst_3 : F.Final
⊢ FinallySmall.{w, v, u} J

Tactic:
have := finallySmall_of_essentiallySmall K
  finallySmall_of_final_of_finallySmall F

Premises used: CategoryTheory.finallySmall_of_final_of_finallySmall, CategoryTheory.finallySmall_of_essentiallySmall
-- Module: Mathlib.CategoryTheory.Limits.FinallySmall
Goal:
J : Type u
inst : Category.{v, u} J
K : Type u₁
inst_1 : Category.{v₁, u₁} K
inst_2 : Limits.HasTerminal.{v, u} J
⊢ FinallySmall.{w, v, u} J

Tactic:
have := Functor.final_const_terminal (C := PUnit.{w + 1}) (D := J)
  .mk' ((Functor.const PUnit.{w + 1}).obj (⊤_ J))

Premises used: CategoryTheory.Limits.terminal, PUnit, CategoryTheory.Functor.final_const_terminal, CategoryTheory.FinallySmall.mk', CategoryTheory.Functor.const, CategoryTheory.Functor.obj