awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Final
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.Final
E : Type u₃
inst_3 : Category.{v₃, u₃} E
G : Functor.{v₂, v₃, u₂, u₃} D E
B : Type u₄
inst_4 : Category.{v₄, u₄} B
H : Functor.{v₃, v₄, u₃, u₄} E B
inst_5 : PreservesColimit (F ⋙ G) H
c : Cocone G
hc : IsColimit c
hc' : IsColimit (H.mapCocone (Cocone.whisker F c)) :=
  isColimitOfPreserves H (((isColimitWhiskerEquiv F c).symm : (a : IsColimit c) → IsColimit (Cocone.whisker F c)) hc)
⊢ IsColimit (Cocone.whisker F (H.mapCocone c))

Tactic:
exact IsColimit.ofIsoColimit hc' (Cocone.ext (Iso.refl _) (by simp))

Premises used: CategoryTheory.Limits.Cocone.ext, CategoryTheory.Limits.IsColimit.ofIsoColimit, CategoryTheory.Iso.refl
-- Module: Mathlib.CategoryTheory.Limits.Final
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.Final
E : Type u₃
inst_3 : Category.{v₃, u₃} E
G : Functor.{v₂, v₃, u₂, u₃} D E
B : Type u₄
inst_4 : Category.{v₄, u₄} B
H : Functor.{v₃, v₄, u₃, u₄} E B
inst_5 : ReflectsColimit (F ⋙ G) H
c : Cocone G
hc : IsColimit (H.mapCocone c)
⊢ Nonempty (IsColimit c)

Tactic:
⟨isColimitWhiskerEquiv F _ (isColimitOfReflects H ?_)⟩

Premises used: Nonempty.intro, CategoryTheory.Limits.isColimitOfReflects, CategoryTheory.Functor.Final.isColimitWhiskerEquiv, DFunLike.coe
-- Module: Mathlib.CategoryTheory.Limits.Final
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.Final
E : Type u₃
inst_3 : Category.{v₃, u₃} E
G : Functor.{v₂, v₃, u₂, u₃} D E
B : Type u₄
inst_4 : Category.{v₄, u₄} B
H : Functor.{v₃, v₄, u₃, u₄} E B
inst_5 : ReflectsColimit (F ⋙ G) H
c : Cocone G
hc : IsColimit (H.mapCocone c)
refine : IsColimit (H.mapCocone (Cocone.whisker F c))
⊢ Nonempty (IsColimit c)

Tactic:
refine ⟨isColimitWhiskerEquiv F _ (isColimitOfReflects H ?_)⟩
-- Module: Mathlib.CategoryTheory.Limits.Final
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.Final
E : Type u₃
inst_3 : Category.{v₃, u₃} E
G : Functor.{v₂, v₃, u₂, u₃} D E
B : Type u₄
inst_4 : Category.{v₄, u₄} B
H : Functor.{v₃, v₄, u₃, u₄} E B
inst_5 : ReflectsColimit (F ⋙ G) H
c : Cocone G
hc : IsColimit (H.mapCocone c)
hc' : IsColimit (Cocone.whisker F (H.mapCocone c)) :=
  ((isColimitWhiskerEquiv F (H.mapCocone c)).symm :
      (a : IsColimit (H.mapCocone c)) → IsColimit (Cocone.whisker F (H.mapCocone c)))
    hc
⊢ ∀ (j : C),
    (Cocone.whisker F (H.mapCocone c)).ι.app j ≫ Iso.hom (Iso.refl (Cocone.whisker F (H.mapCocone c)).pt) =
      (H.mapCocone (Cocone.whisker F c)).ι.app j

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Final
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.Final
E : Type u₃
inst_3 : Category.{v₃, u₃} E
G : Functor.{v₂, v₃, u₂, u₃} D E
B : Type u₄
inst_4 : Category.{v₄, u₄} B
H : Functor.{v₃, v₄, u₃, u₄} E B
inst_5 : ReflectsColimit (F ⋙ G) H
c : Cocone G
hc : IsColimit (H.mapCocone c)
hc' : IsColimit (Cocone.whisker F (H.mapCocone c)) :=
  ((isColimitWhiskerEquiv F (H.mapCocone c)).symm :
      (a : IsColimit (H.mapCocone c)) → IsColimit (Cocone.whisker F (H.mapCocone c)))
    hc
⊢ IsColimit (H.mapCocone (Cocone.whisker F c))

Tactic:
exact IsColimit.ofIsoColimit hc' (Cocone.ext (Iso.refl _) (by simp))

Premises used: CategoryTheory.Limits.Cocone.ext, CategoryTheory.Limits.IsColimit.ofIsoColimit, CategoryTheory.Iso.refl
-- Module: Mathlib.CategoryTheory.Limits.Final
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.Final
E : Type u₃
inst_3 : Category.{v₃, u₃} E
G : Functor.{v₂, v₃, u₂, u₃} D E
B : Type u₄
inst_4 : Category.{v₄, u₄} B
H : Functor.{v₃, v₄, u₃, u₄} E B
inst_5 : CreatesColimit (F ⋙ G) H
c : Cocone (G ⋙ H)
hc : IsColimit c
refine :
  H.mapCocone
      (obj (C := Cocone (F ⋙ G)) extendCocone
        (liftColimit.{v₁, u₁, v₃, v₄, u₃, u₄} (D := B) (F := H) (c := Cocone.whisker F c)
          (((isColimitWhiskerEquiv F c).symm : (a : IsColimit c) → IsColimit (Cocone.whisker F c)) hc))) ≅
    c
⊢ LiftableCocone G H c

Tactic:
refine ⟨(extendCocone (F := F)).obj (liftColimit ((isColimitWhiskerEquiv F _).symm hc)), ?_⟩
-- Module: Mathlib.CategoryTheory.Limits.Final
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.Final
E : Type u₃
inst_3 : Category.{v₃, u₃} E
G : Functor.{v₂, v₃, u₂, u₃} D E
B : Type u₄
inst_4 : Category.{v₄, u₄} B
H : Functor.{v₃, v₄, u₃, u₄} E B
inst_5 : CreatesColimit (F ⋙ G) H
c : Cocone (G ⋙ H)
hc : IsColimit c
i : H.mapCocone
    (liftColimit.{v₁, u₁, v₃, v₄, u₃, u₄} (D := B) (F := H) (c := Cocone.whisker F c)
      (((isColimitWhiskerEquiv F c).symm : (a : IsColimit c) → IsColimit (Cocone.whisker F c)) hc)) ≅
  Cocone.whisker F c :=
  liftedColimitMapsToOriginal
    (((isColimitWhiskerEquiv F c).symm : (a : IsColimit c) → IsColimit (Cocone.whisker F c)) hc)
refine :
  H.mapCocone
      (obj (C := Cocone (F ⋙ G)) extendCocone
        (liftColimit.{v₁, u₁, v₃, v₄, u₃, u₄} (D := B) (F := H) (c := Cocone.whisker F c)
          (((isColimitWhiskerEquiv F c).symm : (a : IsColimit c) → IsColimit (Cocone.whisker F c)) hc))) ≅
    obj (C := Cocone (F ⋙ G ⋙ H)) extendCocone
      (H.mapCocone
        (liftColimit.{v₁, u₁, v₃, v₄, u₃, u₄} (D := B) (F := H) (c := Cocone.whisker F c)
          (((isColimitWhiskerEquiv F c).symm : (a : IsColimit c) → IsColimit (Cocone.whisker F c)) hc)))
⊢ H.mapCocone
      (obj (C := Cocone (F ⋙ G)) extendCocone
        (liftColimit.{v₁, u₁, v₃, v₄, u₃, u₄} (D := B) (F := H) (c := Cocone.whisker F c)
          (((isColimitWhiskerEquiv F c).symm : (a : IsColimit c) → IsColimit (Cocone.whisker F c)) hc))) ≅
    c

Tactic:
refine ?_ ≪≫ ((extendCocone (F := F)).mapIso i) ≪≫ ((coconesEquiv F (G ⋙ H)).counitIso.app _)

Premises used: CategoryTheory.Functor.Final.extendCocone, CategoryTheory.Functor.comp, CategoryTheory.Iso.app, CategoryTheory.Functor.mapIso, CategoryTheory.Equivalence.counitIso, CategoryTheory.Functor.Final.coconesEquiv
-- Module: Mathlib.CategoryTheory.Limits.Final
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.Final
E : Type u₃
inst_3 : Category.{v₃, u₃} E
G : Functor.{v₂, v₃, u₂, u₃} D E
B : Type u₄
inst_4 : Category.{v₄, u₄} B
H : Functor.{v₃, v₄, u₃, u₄} E B
inst_5 : CreatesColimit (F ⋙ G) H
c : Cocone (G ⋙ H)
hc : IsColimit c
i : H.mapCocone
    (liftColimit.{v₁, u₁, v₃, v₄, u₃, u₄} (D := B) (F := H) (c := Cocone.whisker F c)
      (((isColimitWhiskerEquiv F c).symm : (a : IsColimit c) → IsColimit (Cocone.whisker F c)) hc)) ≅
  Cocone.whisker F c :=
  liftedColimitMapsToOriginal
    (((isColimitWhiskerEquiv F c).symm : (a : IsColimit c) → IsColimit (Cocone.whisker F c)) hc)
⊢ H.mapCocone
      (obj (C := Cocone (F ⋙ G)) extendCocone
        (liftColimit.{v₁, u₁, v₃, v₄, u₃, u₄} (D := B) (F := H) (c := Cocone.whisker F c)
          (((isColimitWhiskerEquiv F c).symm : (a : IsColimit c) → IsColimit (Cocone.whisker F c)) hc))) ≅
    obj (C := Cocone (F ⋙ G ⋙ H)) extendCocone
      (H.mapCocone
        (liftColimit.{v₁, u₁, v₃, v₄, u₃, u₄} (D := B) (F := H) (c := Cocone.whisker F c)
          (((isColimitWhiskerEquiv F c).symm : (a : IsColimit c) → IsColimit (Cocone.whisker F c)) hc)))

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

Premises used: CategoryTheory.Limits.Cocone.ext, CategoryTheory.Iso.refl
-- Module: Mathlib.CategoryTheory.Limits.Final
Goal:
C : Type v
inst : Category.{v, v} C
D : Type u₁
inst_1 : Category.{v, u₁} D
F : C ⥤ D
d : D
f₁ f₂ x y : (X : C) × (d ⟶ F.obj X)
r : (F ⋙ obj coyoneda (op d)).ColimitTypeRel x y
rel :
  ∀
    (f :
      x.fst (β := fun (j : C) ↦ (F ⋙ obj coyoneda (op d)).obj j) ⟶
        y.fst (β := fun (j : C) ↦ (F ⋙ obj coyoneda (op d)).obj j))
    (w :
      y.snd (β := fun (j : C) ↦ (F ⋙ obj coyoneda (op d)).obj j) =
        (ConcreteCategory.hom (FC := TypeCat.Fun) ((F ⋙ obj coyoneda (op d)).map f) :
            (a : (fun (X : Type v) ↦ X) ((F ⋙ coyoneda.obj (op d)).obj x.fst)) →
              (fun (X : Type v) ↦ X) ((F ⋙ coyoneda.obj (op d)).obj y.fst))
          (x.snd (β := fun (j : C) ↦ (F ⋙ obj coyoneda (op d)).obj j))),
    Zigzag (StructuredArrow.mk (x.snd (β := fun (X : C) ↦ d ⟶ F.obj X)))
      (StructuredArrow.mk (y.snd (β := fun (X : C) ↦ d ⟶ F.obj X)))
⊢ Zigzag (StructuredArrow.mk (x.snd (β := fun (X : C) ↦ d ⟶ F.obj X)))
    (StructuredArrow.mk (y.snd (β := fun (X : C) ↦ d ⟶ F.obj X)))

Tactic:
obtain ⟨f, w⟩ := r
-- Module: Mathlib.CategoryTheory.Limits.Final
Goal:
C : Type v
inst : Category.{v, v} C
D : Type u₁
inst_1 : Category.{v, u₁} D
F : C ⥤ D
d : D
f₁ f₂ x y : (X : C) × (d ⟶ F.obj X)
f :
  x.fst (β := fun (j : C) ↦ (F ⋙ obj coyoneda (op d)).obj j) ⟶
    y.fst (β := fun (j : C) ↦ (F ⋙ obj coyoneda (op d)).obj j)
w :
  y.snd (β := fun (j : C) ↦ (F ⋙ obj coyoneda (op d)).obj j) =
    (ConcreteCategory.hom (FC := TypeCat.Fun) ((F ⋙ obj coyoneda (op d)).map f) :
        (a : (fun (X : Type v) ↦ X) ((F ⋙ coyoneda.obj (op d)).obj x.fst)) →
          (fun (X : Type v) ↦ X) ((F ⋙ coyoneda.obj (op d)).obj y.fst))
      (x.snd (β := fun (j : C) ↦ (F ⋙ obj coyoneda (op d)).obj j))
rel : StructuredArrow d F
rel₁ :
  Relation.ReflTransGen Zag (StructuredArrow.mk (x.snd (β := fun (X : C) ↦ d ⟶ F.obj X)))
    (StructuredArrow.mk (x.snd (β := fun (X : C) ↦ d ⟶ F.obj X)))
rel₂ :
  Zag (StructuredArrow.mk (x.snd (β := fun (X : C) ↦ d ⟶ F.obj X)))
    (StructuredArrow.mk (y.snd (β := fun (X : C) ↦ d ⟶ F.obj X)))
⊢ Zigzag (StructuredArrow.mk (x.snd (β := fun (X : C) ↦ d ⟶ F.obj X)))
    (StructuredArrow.mk (y.snd (β := fun (X : C) ↦ d ⟶ F.obj X)))

Tactic:
fconstructor
-- Module: Mathlib.CategoryTheory.Limits.Final
Goal:
C : Type v
inst : Category.{v, v} C
D : Type u₁
inst_1 : Category.{v, u₁} D
F : C ⥤ D
d : D
f₁ f₂ x y : (X : C) × (d ⟶ F.obj X)
f :
  x.fst (β := fun (j : C) ↦ (F ⋙ obj coyoneda (op d)).obj j) ⟶
    y.fst (β := fun (j : C) ↦ (F ⋙ obj coyoneda (op d)).obj j)
w :
  y.snd (β := fun (j : C) ↦ (F ⋙ obj coyoneda (op d)).obj j) =
    (ConcreteCategory.hom (FC := TypeCat.Fun) ((F ⋙ obj coyoneda (op d)).map f) :
        (a : (fun (X : Type v) ↦ X) ((F ⋙ coyoneda.obj (op d)).obj x.fst)) →
          (fun (X : Type v) ↦ X) ((F ⋙ coyoneda.obj (op d)).obj y.fst))
      (x.snd (β := fun (j : C) ↦ (F ⋙ obj coyoneda (op d)).obj j))
⊢ Relation.ReflTransGen Zag (StructuredArrow.mk (x.snd (β := fun (X : C) ↦ d ⟶ F.obj X)))
    (StructuredArrow.mk (x.snd (β := fun (X : C) ↦ d ⟶ F.obj X)))

Tactic:
fconstructor
-- Module: Mathlib.CategoryTheory.Limits.Final
Goal:
C : Type v
inst : Category.{v, v} C
D : Type u₁
inst_1 : Category.{v, u₁} D
F : C ⥤ D
d : D
f₁ f₂ x y : (X : C) × (d ⟶ F.obj X)
f :
  x.fst (β := fun (j : C) ↦ (F ⋙ obj coyoneda (op d)).obj j) ⟶
    y.fst (β := fun (j : C) ↦ (F ⋙ obj coyoneda (op d)).obj j)
w :
  y.snd (β := fun (j : C) ↦ (F ⋙ obj coyoneda (op d)).obj j) =
    (ConcreteCategory.hom (FC := TypeCat.Fun) ((F ⋙ obj coyoneda (op d)).map f) :
        (a : (fun (X : Type v) ↦ X) ((F ⋙ coyoneda.obj (op d)).obj x.fst)) →
          (fun (X : Type v) ↦ X) ((F ⋙ coyoneda.obj (op d)).obj y.fst))
      (x.snd (β := fun (j : C) ↦ (F ⋙ obj coyoneda (op d)).obj j))
rel :
  Nonempty.{v + 1}
    (StructuredArrow.mk (x.snd (β := fun (X : C) ↦ d ⟶ F.obj X)) ⟶
      StructuredArrow.mk (y.snd (β := fun (X : C) ↦ d ⟶ F.obj X)))
⊢ Zag (StructuredArrow.mk (x.snd (β := fun (X : C) ↦ d ⟶ F.obj X)))
    (StructuredArrow.mk (y.snd (β := fun (X : C) ↦ d ⟶ F.obj X)))

Tactic:
left
-- Module: Mathlib.CategoryTheory.Limits.Final
Goal:
C : Type v
inst : Category.{v, v} C
D : Type u₁
inst_1 : Category.{v, u₁} D
F : C ⥤ D
d : D
f₁ f₂ x y : (X : C) × (d ⟶ F.obj X)
f :
  x.fst (β := fun (j : C) ↦ (F ⋙ obj coyoneda (op d)).obj j) ⟶
    y.fst (β := fun (j : C) ↦ (F ⋙ obj coyoneda (op d)).obj j)
w :
  y.snd (β := fun (j : C) ↦ (F ⋙ obj coyoneda (op d)).obj j) =
    (ConcreteCategory.hom (FC := TypeCat.Fun) ((F ⋙ obj coyoneda (op d)).map f) :
        (a : (fun (X : Type v) ↦ X) ((F ⋙ coyoneda.obj (op d)).obj x.fst)) →
          (fun (X : Type v) ↦ X) ((F ⋙ coyoneda.obj (op d)).obj y.fst))
      (x.snd (β := fun (j : C) ↦ (F ⋙ obj coyoneda (op d)).obj j))
rel :
  StructuredArrow.mk (x.snd (β := fun (X : C) ↦ d ⟶ F.obj X)) ⟶
    StructuredArrow.mk (y.snd (β := fun (X : C) ↦ d ⟶ F.obj X))
⊢ Nonempty.{v + 1}
    (StructuredArrow.mk (x.snd (β := fun (X : C) ↦ d ⟶ F.obj X)) ⟶
      StructuredArrow.mk (y.snd (β := fun (X : C) ↦ d ⟶ F.obj X)))

Tactic:
fconstructor
-- Module: Mathlib.CategoryTheory.Limits.Final
Goal:
C : Type v
inst : Category.{v, v} C
D : Type u₁
inst_1 : Category.{v, u₁} D
F : C ⥤ D
d : D
f₁ f₂ x y : (X : C) × (d ⟶ F.obj X)
f :
  x.fst (β := fun (j : C) ↦ (F ⋙ obj coyoneda (op d)).obj j) ⟶
    y.fst (β := fun (j : C) ↦ (F ⋙ obj coyoneda (op d)).obj j)
w :
  y.snd (β := fun (j : C) ↦ (F ⋙ obj coyoneda (op d)).obj j) =
    (ConcreteCategory.hom (FC := TypeCat.Fun) ((F ⋙ obj coyoneda (op d)).map f) :
        (a : (fun (X : Type v) ↦ X) ((F ⋙ coyoneda.obj (op d)).obj x.fst)) →
          (fun (X : Type v) ↦ X) ((F ⋙ coyoneda.obj (op d)).obj y.fst))
      (x.snd (β := fun (j : C) ↦ (F ⋙ obj coyoneda (op d)).obj j))
⊢ StructuredArrow.mk (x.snd (β := fun (X : C) ↦ d ⟶ F.obj X)) ⟶
    StructuredArrow.mk (y.snd (β := fun (X : C) ↦ d ⟶ F.obj X))

Tactic:
exact StructuredArrow.homMk f

Premises used: CategoryTheory.StructuredArrow.homMk
-- Module: Mathlib.CategoryTheory.Limits.Final
Goal:
C : Type v
inst : Category.{v, v} C
D : Type u₁
inst_1 : Category.{v, u₁} D
F : C ⥤ D
d : D
f₁ f₂ x : (X : C) × (d ⟶ F.obj X)
⊢ Zigzag (StructuredArrow.mk (x.snd (β := fun (X : C) ↦ d ⟶ F.obj X)))
    (StructuredArrow.mk (x.snd (β := fun (X : C) ↦ d ⟶ F.obj X)))

Tactic:
fconstructor
-- Module: Mathlib.CategoryTheory.Limits.Final
Goal:
C : Type v
inst : Category.{v, v} C
D : Type u₁
inst_1 : Category.{v, u₁} D
F : C ⥤ D
d : D
f₁ f₂ x y : (X : C) × (d ⟶ F.obj X)
h : Relation.EqvGen (F ⋙ obj coyoneda (op d)).ColimitTypeRel x y
ih symm :
  Zigzag (StructuredArrow.mk (x.snd (β := fun (X : C) ↦ d ⟶ F.obj X)))
    (StructuredArrow.mk (y.snd (β := fun (X : C) ↦ d ⟶ F.obj X)))
⊢ Zigzag (StructuredArrow.mk (y.snd (β := fun (X : C) ↦ d ⟶ F.obj X)))
    (StructuredArrow.mk (x.snd (β := fun (X : C) ↦ d ⟶ F.obj X)))

Tactic:
apply zigzag_symmetric

Premises used: CategoryTheory.zigzag_symmetric
-- Module: Mathlib.CategoryTheory.Limits.Final
Goal:
C : Type v
inst : Category.{v, v} C
D : Type u₁
inst_1 : Category.{v, u₁} D
F : C ⥤ D
d : D
f₁ f₂ x y : (X : C) × (d ⟶ F.obj X)
h : Relation.EqvGen (F ⋙ obj coyoneda (op d)).ColimitTypeRel x y
ih :
  Zigzag (StructuredArrow.mk (x.snd (β := fun (X : C) ↦ d ⟶ F.obj X)))
    (StructuredArrow.mk (y.snd (β := fun (X : C) ↦ d ⟶ F.obj X)))
⊢ Zigzag (StructuredArrow.mk (x.snd (β := fun (X : C) ↦ d ⟶ F.obj X)))
    (StructuredArrow.mk (y.snd (β := fun (X : C) ↦ d ⟶ F.obj X)))

Tactic:
ih
-- Module: Mathlib.CategoryTheory.Limits.Final
Goal:
C : Type v
inst : Category.{v, v} C
D : Type u₁
inst_1 : Category.{v, u₁} D
F : C ⥤ D
d : D
f₁ f₂ x y : (X : C) × (d ⟶ F.obj X)
h : Relation.EqvGen (F ⋙ obj coyoneda (op d)).ColimitTypeRel x y
ih :
  Zigzag (StructuredArrow.mk (x.snd (β := fun (X : C) ↦ d ⟶ F.obj X)))
    (StructuredArrow.mk (y.snd (β := fun (X : C) ↦ d ⟶ F.obj X)))
⊢ Zigzag (StructuredArrow.mk (x.snd (β := fun (X : C) ↦ d ⟶ F.obj X)))
    (StructuredArrow.mk (y.snd (β := fun (X : C) ↦ d ⟶ F.obj X)))

Tactic:
exact ih
-- Module: Mathlib.CategoryTheory.Limits.Final
Goal:
C : Type v
inst : Category.{v, v} C
D : Type u₁
inst_1 : Category.{v, u₁} D
F : C ⥤ D
d : D
f₁ f₂ x y z : (X : C) × (d ⟶ F.obj X)
h : Relation.EqvGen (F ⋙ obj coyoneda (op d)).ColimitTypeRel x y
h_1 : Relation.EqvGen (F ⋙ obj coyoneda (op d)).ColimitTypeRel y z
ih₁ :
  Zigzag (StructuredArrow.mk (x.snd (β := fun (X : C) ↦ d ⟶ F.obj X)))
    (StructuredArrow.mk (y.snd (β := fun (X : C) ↦ d ⟶ F.obj X)))
ih₂ :
  Zigzag (StructuredArrow.mk (y.snd (β := fun (X : C) ↦ d ⟶ F.obj X)))
    (StructuredArrow.mk (z.snd (β := fun (X : C) ↦ d ⟶ F.obj X)))
trans :
  Relation.ReflTransGen Zag (StructuredArrow.mk (x.snd (β := fun (X : C) ↦ d ⟶ F.obj X)))
    (StructuredArrow.mk (y.snd (β := fun (X : C) ↦ d ⟶ F.obj X)))
trans₁ :
  Relation.ReflTransGen Zag (StructuredArrow.mk (y.snd (β := fun (X : C) ↦ d ⟶ F.obj X)))
    (StructuredArrow.mk (z.snd (β := fun (X : C) ↦ d ⟶ F.obj X)))
trans₂ : StructuredArrow d F
⊢ Zigzag (StructuredArrow.mk (x.snd (β := fun (X : C) ↦ d ⟶ F.obj X)))
    (StructuredArrow.mk (z.snd (β := fun (X : C) ↦ d ⟶ F.obj X)))

Tactic:
apply Relation.ReflTransGen.trans

Premises used: Relation.ReflTransGen.trans
-- Module: Mathlib.CategoryTheory.Limits.Final
Goal:
C : Type v
inst : Category.{v, v} C
D : Type u₁
inst_1 : Category.{v, u₁} D
F : C ⥤ D
d : D
f₁ f₂ x y z : (X : C) × (d ⟶ F.obj X)
h : Relation.EqvGen (F ⋙ obj coyoneda (op d)).ColimitTypeRel x y
h_1 : Relation.EqvGen (F ⋙ obj coyoneda (op d)).ColimitTypeRel y z
ih₁ :
  Zigzag (StructuredArrow.mk (x.snd (β := fun (X : C) ↦ d ⟶ F.obj X)))
    (StructuredArrow.mk (y.snd (β := fun (X : C) ↦ d ⟶ F.obj X)))
ih₂ :
  Zigzag (StructuredArrow.mk (y.snd (β := fun (X : C) ↦ d ⟶ F.obj X)))
    (StructuredArrow.mk (z.snd (β := fun (X : C) ↦ d ⟶ F.obj X)))
⊢ Relation.ReflTransGen Zag (StructuredArrow.mk (x.snd (β := fun (X : C) ↦ d ⟶ F.obj X)))
    (StructuredArrow.mk (y.snd (β := fun (X : C) ↦ d ⟶ F.obj X)))

Tactic:
ih₁

Premises used: CategoryTheory.Zigzag
-- Module: Mathlib.CategoryTheory.Limits.Final
Goal:
C : Type v
inst : Category.{v, v} C
D : Type u₁
inst_1 : Category.{v, u₁} D
F : C ⥤ D
d : D
f₁ f₂ x y z : (X : C) × (d ⟶ F.obj X)
h : Relation.EqvGen (F ⋙ obj coyoneda (op d)).ColimitTypeRel x y
h_1 : Relation.EqvGen (F ⋙ obj coyoneda (op d)).ColimitTypeRel y z
ih₁ :
  Zigzag (StructuredArrow.mk (x.snd (β := fun (X : C) ↦ d ⟶ F.obj X)))
    (StructuredArrow.mk (y.snd (β := fun (X : C) ↦ d ⟶ F.obj X)))
ih₂ :
  Zigzag (StructuredArrow.mk (y.snd (β := fun (X : C) ↦ d ⟶ F.obj X)))
    (StructuredArrow.mk (z.snd (β := fun (X : C) ↦ d ⟶ F.obj X)))
⊢ Relation.ReflTransGen Zag (StructuredArrow.mk (x.snd (β := fun (X : C) ↦ d ⟶ F.obj X)))
    (StructuredArrow.mk (y.snd (β := fun (X : C) ↦ d ⟶ F.obj X)))

Tactic:
exact ih₁
-- Module: Mathlib.CategoryTheory.Limits.Final
Goal:
C : Type v
inst : Category.{v, v} C
D : Type u₁
inst_1 : Category.{v, u₁} D
F : C ⥤ D
d : D
f₁ f₂ x y z : (X : C) × (d ⟶ F.obj X)
h : Relation.EqvGen (F ⋙ obj coyoneda (op d)).ColimitTypeRel x y
h_1 : Relation.EqvGen (F ⋙ obj coyoneda (op d)).ColimitTypeRel y z
ih₁ :
  Zigzag (StructuredArrow.mk (x.snd (β := fun (X : C) ↦ d ⟶ F.obj X)))
    (StructuredArrow.mk (y.snd (β := fun (X : C) ↦ d ⟶ F.obj X)))
ih₂ :
  Zigzag (StructuredArrow.mk (y.snd (β := fun (X : C) ↦ d ⟶ F.obj X)))
    (StructuredArrow.mk (z.snd (β := fun (X : C) ↦ d ⟶ F.obj X)))
⊢ Relation.ReflTransGen Zag (StructuredArrow.mk (y.snd (β := fun (X : C) ↦ d ⟶ F.obj X)))
    (StructuredArrow.mk (z.snd (β := fun (X : C) ↦ d ⟶ F.obj X)))

Tactic:
ih₂

Premises used: CategoryTheory.Zigzag
-- Module: Mathlib.CategoryTheory.Limits.Final
Goal:
C : Type v
inst : Category.{v, v} C
D : Type u₁
inst_1 : Category.{v, u₁} D
F : C ⥤ D
d : D
f₁ f₂ x y z : (X : C) × (d ⟶ F.obj X)
h : Relation.EqvGen (F ⋙ obj coyoneda (op d)).ColimitTypeRel x y
h_1 : Relation.EqvGen (F ⋙ obj coyoneda (op d)).ColimitTypeRel y z
ih₁ :
  Zigzag (StructuredArrow.mk (x.snd (β := fun (X : C) ↦ d ⟶ F.obj X)))
    (StructuredArrow.mk (y.snd (β := fun (X : C) ↦ d ⟶ F.obj X)))
ih₂ :
  Zigzag (StructuredArrow.mk (y.snd (β := fun (X : C) ↦ d ⟶ F.obj X)))
    (StructuredArrow.mk (z.snd (β := fun (X : C) ↦ d ⟶ F.obj X)))
⊢ Relation.ReflTransGen Zag (StructuredArrow.mk (y.snd (β := fun (X : C) ↦ d ⟶ F.obj X)))
    (StructuredArrow.mk (z.snd (β := fun (X : C) ↦ d ⟶ F.obj X)))

Tactic:
exact ih₂
-- Module: Mathlib.CategoryTheory.Limits.Final
Goal:
C : Type v
inst : Category.{v, v} C
D : Type u₁
inst_1 : Category.{v, u₁} D
F : C ⥤ D
d : D
f₁ f₂ : (X : C) × (d ⟶ F.obj X)
t : Relation.EqvGen (F ⋙ obj coyoneda (op d)).ColimitTypeRel f₁ f₂
rel :
  ∀ (x y : (X : C) × (d ⟶ F.obj X)) (r : (F ⋙ obj coyoneda (op d)).ColimitTypeRel x y),
    Zigzag (StructuredArrow.mk (x.snd (β := fun (X : C) ↦ d ⟶ F.obj X)))
      (StructuredArrow.mk (y.snd (β := fun (X : C) ↦ d ⟶ F.obj X)))
refl :
  ∀ (x : (X : C) × (d ⟶ F.obj X)),
    Zigzag (StructuredArrow.mk (x.snd (β := fun (X : C) ↦ d ⟶ F.obj X)))
      (StructuredArrow.mk (x.snd (β := fun (X : C) ↦ d ⟶ F.obj X)))
symm :
  ∀ (x y : (X : C) × (d ⟶ F.obj X)),
    Relation.EqvGen (F ⋙ obj coyoneda (op d)).ColimitTypeRel x y →
      ∀
        (ih :
          Zigzag (StructuredArrow.mk (x.snd (β := fun (X : C) ↦ d ⟶ F.obj X)))
            (StructuredArrow.mk (y.snd (β := fun (X : C) ↦ d ⟶ F.obj X)))),
        Zigzag (StructuredArrow.mk (y.snd (β := fun (X : C) ↦ d ⟶ F.obj X)))
          (StructuredArrow.mk (x.snd (β := fun (X : C) ↦ d ⟶ F.obj X)))
trans :
  ∀ (x y z : (X : C) × (d ⟶ F.obj X)),
    Relation.EqvGen (F ⋙ obj coyoneda (op d)).ColimitTypeRel x y →
      Relation.EqvGen (F ⋙ obj coyoneda (op d)).ColimitTypeRel y z →
        ∀
          (ih₁ :
            Zigzag (StructuredArrow.mk (x.snd (β := fun (X : C) ↦ d ⟶ F.obj X)))
              (StructuredArrow.mk (y.snd (β := fun (X : C) ↦ d ⟶ F.obj X))))
          (ih₂ :
            Zigzag (StructuredArrow.mk (y.snd (β := fun (X : C) ↦ d ⟶ F.obj X)))
              (StructuredArrow.mk (z.snd (β := fun (X : C) ↦ d ⟶ F.obj X)))),
          Zigzag (StructuredArrow.mk (x.snd (β := fun (X : C) ↦ d ⟶ F.obj X)))
            (StructuredArrow.mk (z.snd (β := fun (X : C) ↦ d ⟶ F.obj X)))
⊢ Zigzag (StructuredArrow.mk (f₁.snd (β := fun (X : C) ↦ d ⟶ F.obj X)))
    (StructuredArrow.mk (f₂.snd (β := fun (X : C) ↦ d ⟶ F.obj X)))

Tactic:
induction t with
  | rel x y r =>
    obtain ⟨f, w⟩ := r
    fconstructor
    swap
    · fconstructor
    left; fconstructor
    exact StructuredArrow.homMk f
  | refl => fconstructor
  | symm x y _ ih =>
    apply zigzag_symmetric
    exact ih
  | trans x y z _ _ ih₁ ih₂ =>
    apply Relation.ReflTransGen.trans
    · exact ih₁
    · exact ih₂

Premises used: Relation.ReflTransGen.trans, CategoryTheory.zigzag_symmetric, symm, refl
-- Module: Mathlib.CategoryTheory.Limits.Final
Goal:
C : Type v
inst : Category.{v, v} C
D : Type u₁
inst_1 : Category.{v, u₁} D
F : C ⥤ D
I : (d : D) → colimit (F ⋙ obj coyoneda (op d)) ≅ PUnit.{v + 1}
d : D
have : ∀ (this : (fun (X : Type v) ↦ X) (colimit (F ⋙ obj coyoneda (op d)))), Nonempty.{v + 1} (StructuredArrow d F)
⊢ Nonempty.{v + 1} (StructuredArrow d F)

Tactic:
have := (I d).inv PUnit.unit
-- Module: Mathlib.CategoryTheory.Limits.Final
Goal:
C : Type v
inst : Category.{v, v} C
D : Type u₁
inst_1 : Category.{v, u₁} D
F : C ⥤ D
I : (d : D) → colimit (F ⋙ obj coyoneda (op d)) ≅ PUnit.{v + 1}
d : D
this : (fun (X : Type v) ↦ X) (colimit (F ⋙ obj coyoneda (op d)))
obtain : ∀ (j : C) (y : (F ⋙ obj coyoneda (op d)).obj j), Nonempty.{v + 1} (StructuredArrow d F)
⊢ Nonempty.{v + 1} (StructuredArrow d F)

Tactic:
obtain ⟨j, y, rfl⟩ := Limits.Types.jointly_surjective'.{v, v} this

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Final
Goal:
C : Type v
inst : Category.{v, v} C
D : Type u₁
inst_1 : Category.{v, u₁} D
F : C ⥤ D
I : (d : D) → colimit (F ⋙ obj coyoneda (op d)) ≅ PUnit.{v + 1}
d : D
j : C
y : (F ⋙ obj coyoneda (op d)).obj j
⊢ Nonempty.{v + 1} (StructuredArrow d F)

Tactic:
⟨StructuredArrow.mk y⟩

Premises used: Nonempty.intro, CategoryTheory.StructuredArrow.mk
-- Module: Mathlib.CategoryTheory.Limits.Final
Goal:
C : Type v
inst : Category.{v, v} C
D : Type u₁
inst_1 : Category.{v, u₁} D
F : C ⥤ D
I : (d : D) → colimit (F ⋙ obj coyoneda (op d)) ≅ PUnit.{v + 1}
d : D
j : C
y : (F ⋙ obj coyoneda (op d)).obj j
⊢ Nonempty.{v + 1} (StructuredArrow d F)

Tactic:
exact ⟨StructuredArrow.mk y⟩