awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Final (goal)
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 G H
c : Cocone (F ⋙ G)
hc : IsColimit c
⊢ Nonempty (IsColimit (H.mapCocone c))
have refine : IsColimit (obj extendCocone (H.mapCocone c))
Tactic: refine ⟨isColimitExtendCoconeEquiv (G := G ⋙ H) F (H.mapCocone c) ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Final (goal)
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 G H
c : Cocone (F ⋙ G)
hc : IsColimit (H.mapCocone c)
⊢ Nonempty (IsColimit c)
have refine : IsColimit (H.mapCocone (obj extendCocone c))
Tactic: refine ⟨isColimitExtendCoconeEquiv F _ (isColimitOfReflects H ?_)⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Final (goal)
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 G H
c : Cocone ((F ⋙ G) ⋙ H)
hc : IsColimit c
⊢ LiftableCocone (F ⋙ G) H c
have refine : H.mapCocone
    (Cocone.whisker F
      (liftColimit.{v₂, u₂, v₃, v₄, u₃, u₄} (D := B) (F := H) (c := obj extendCocone c)
        (((Equiv.symm (isColimitExtendCoconeEquiv F c) : IsColimit c ≃ IsColimit (obj extendCocone c)) :
            (a : IsColimit c) → IsColimit (extendCocone.obj c))
          hc))) ≅
  c
Tactic: refine ⟨(liftColimit ((isColimitExtendCoconeEquiv F (G := G ⋙ H) _).symm hc)).whisker F, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Final (goal)
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
inst_4 : HasColimit G
⊢ IsIso (X := colimit (F ⋙ G)) (Y := colimit G) (colimit.pre G F)
have simp : IsIso (X := colimit (F ⋙ G)) (Y := colimit G)
  (Iso.hom (colimit.isoColimitCocone (colimitCoconeComp F (getColimitCocone G))) ≫
    𝟙 (Cocone.whisker F (getColimitCocone G).cocone).pt ≫ Iso.inv (colimit.isoColimitCocone (getColimitCocone G)))
Tactic: simp only [colimit.pre_eq (colimitCoconeComp F (getColimitCocone G)) (getColimitCocone G),
    colimitCoconeComp_cocone, IsColimit.desc_self]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Final (goal)
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
inst_4 : HasColimitsOfShape.{v₂, u₂, v₃, u₃} D E
inst_5 : HasColimitsOfShape.{v₁, u₁, v₃, u₃} C E
X Y : Functor.{v₂, v₃, u₂, u₃} D E
f : X ⟶ Y
⊢ Eq (α := obj (obj (whiskeringLeft C D E) F ⋙ colim) X ⟶ obj colim Y)
    (map (obj (whiskeringLeft C D E) F ⋙ colim) f ≫
      Iso.hom ((fun (G : Functor.{v₂, v₃, u₂, u₃} D E) ↦ (colimitIso F G : colimit (F ⋙ G) ≅ colimit G)) Y))
    (Iso.hom ((fun (G : Functor.{v₂, v₃, u₂, u₃} D E) ↦ (colimitIso F G : colimit (F ⋙ G) ≅ colimit G)) X) ≫
      map colim f)
have simp : Eq (α := colimit (F ⋙ X) ⟶ colimit Y)
  (CategoryStruct.comp (Y := colimit (F ⋙ Y)) (colimMap (F.whiskerLeft f)) (colimit.pre Y F))
  (CategoryStruct.comp (Y := colimit X) (colimit.pre X F) (colimMap f))
Tactic: simp only [comp_obj, whiskeringLeft_obj_obj, colim_obj, comp_map, whiskeringLeft_obj_map,
      colim_map, colimitIso_hom]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Final (goal)
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
inst_4 : HasColimitsOfShape.{v₂, u₂, v₃, u₃} D E
inst_5 : HasColimitsOfShape.{v₁, u₁, v₃, u₃} C E
X Y : Functor.{v₂, v₃, u₂, u₃} D E
f : X ⟶ Y
⊢ Eq (α := colimit (F ⋙ X) ⟶ colimit Y)
    (CategoryStruct.comp (Y := colimit (F ⋙ Y)) (colimMap (F.whiskerLeft f)) (colimit.pre Y F))
    (CategoryStruct.comp (Y := colimit X) (colimit.pre X F) (colimMap f))
have w : ∀ (j : C),
  Eq (α := (F ⋙ X).obj j ⟶ colimit Y)
    (CategoryStruct.comp (Y := colimit (F ⋙ X)) (colimit.ι (F ⋙ X) j)
      (CategoryStruct.comp (Y := colimit (F ⋙ Y)) (colimMap (F.whiskerLeft f)) (colimit.pre Y F)))
    (CategoryStruct.comp (Y := colimit (F ⋙ X)) (colimit.ι (F ⋙ X) j)
      (CategoryStruct.comp (Y := colimit X) (colimit.pre X F) (colimMap f)))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Final (goal)
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
⊢ Nonempty (IsColimit (H.mapCocone c))
have refine : IsColimit (Cocone.whisker F (H.mapCocone c))
Tactic: refine ⟨isColimitWhiskerEquiv F _ ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Final (goal)
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)
have refine : IsColimit (H.mapCocone (Cocone.whisker F c))
Tactic: refine ⟨isColimitWhiskerEquiv F _ (isColimitOfReflects H ?_)⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Final (goal)
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
⊢ LiftableCocone G H c
have 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
Tactic: refine ⟨(extendCocone (F := F)).obj (liftColimit ((isColimitWhiskerEquiv F _).symm hc)), ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Final (goal)
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))) ≅
    c
have 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)))
Tactic: refine ?_ ≪≫ ((extendCocone (F := F)).mapIso i) ≪≫ ((coconesEquiv F (G ⋙ H)).counitIso.app _)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Final (goal)
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
⊢ Zigzag (StructuredArrow.mk (x.snd (β := fun (X : C) ↦ d ⟶ F.obj X)))
    (StructuredArrow.mk (y.snd (β := fun (X : C) ↦ d ⟶ F.obj X)))
have 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)))
Tactic: obtain ⟨f, w⟩ := r
Cleared hypotheses: r
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Final (goal)
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))
⊢ Zigzag (StructuredArrow.mk (x.snd (β := fun (X : C) ↦ d ⟶ F.obj X)))
    (StructuredArrow.mk (y.snd (β := fun (X : C) ↦ d ⟶ F.obj X)))
have rel : StructuredArrow d F
Tactic: fconstructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Final (goal)
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
⊢ Zigzag (StructuredArrow.mk (x.snd (β := fun (X : C) ↦ d ⟶ F.obj X)))
    (StructuredArrow.mk (y.snd (β := fun (X : C) ↦ d ⟶ F.obj X)))
have 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)))
Tactic: fconstructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Final (goal)
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)))
⊢ Zigzag (StructuredArrow.mk (x.snd (β := fun (X : C) ↦ d ⟶ F.obj X)))
    (StructuredArrow.mk (y.snd (β := fun (X : C) ↦ d ⟶ F.obj X)))
have rel₂ : Zag (StructuredArrow.mk (x.snd (β := fun (X : C) ↦ d ⟶ F.obj X)))
  (StructuredArrow.mk (y.snd (β := fun (X : C) ↦ d ⟶ F.obj X)))
Tactic: fconstructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Final (goal)
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))
⊢ Zag (StructuredArrow.mk (x.snd (β := fun (X : C) ↦ d ⟶ F.obj X)))
    (StructuredArrow.mk (y.snd (β := fun (X : C) ↦ d ⟶ F.obj X)))
have 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)))
Tactic: left
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Final (goal)
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))
⊢ 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)))
have rel : StructuredArrow.mk (x.snd (β := fun (X : C) ↦ d ⟶ F.obj X)) ⟶
  StructuredArrow.mk (y.snd (β := fun (X : C) ↦ d ⟶ F.obj X))
Tactic: fconstructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Final (goal)
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)))
⊢ Zigzag (StructuredArrow.mk (x.snd (β := fun (X : C) ↦ d ⟶ F.obj X)))
    (StructuredArrow.mk (z.snd (β := fun (X : C) ↦ d ⟶ F.obj X)))
have 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)))
Tactic: apply Relation.ReflTransGen.trans
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Final (goal)
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)))
⊢ Zigzag (StructuredArrow.mk (x.snd (β := fun (X : C) ↦ d ⟶ F.obj X)))
    (StructuredArrow.mk (z.snd (β := fun (X : C) ↦ d ⟶ F.obj X)))
have 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)))
Tactic: apply Relation.ReflTransGen.trans
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Final (goal)
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)))
⊢ Zigzag (StructuredArrow.mk (x.snd (β := fun (X : C) ↦ d ⟶ F.obj X)))
    (StructuredArrow.mk (z.snd (β := fun (X : C) ↦ d ⟶ F.obj X)))
have trans₂ : StructuredArrow d F
Tactic: apply Relation.ReflTransGen.trans
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Final (goal)
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₂
⊢ Zigzag (StructuredArrow.mk (f₁.snd (β := fun (X : C) ↦ d ⟶ F.obj X)))
    (StructuredArrow.mk (f₂.snd (β := fun (X : C) ↦ d ⟶ F.obj X)))
have 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)))
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₂
Cleared hypotheses: t
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Final (goal)
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)))
⊢ Zigzag (StructuredArrow.mk (f₁.snd (β := fun (X : C) ↦ d ⟶ F.obj X)))
    (StructuredArrow.mk (f₂.snd (β := fun (X : C) ↦ d ⟶ F.obj X)))
have 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)))
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₂
Cleared hypotheses: t
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Final (goal)
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)))
⊢ Zigzag (StructuredArrow.mk (f₁.snd (β := fun (X : C) ↦ d ⟶ F.obj X)))
    (StructuredArrow.mk (f₂.snd (β := fun (X : C) ↦ d ⟶ F.obj X)))
have 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)))
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₂
Cleared hypotheses: t
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Final (goal)
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)))
⊢ Zigzag (StructuredArrow.mk (f₁.snd (β := fun (X : C) ↦ d ⟶ F.obj X)))
    (StructuredArrow.mk (f₂.snd (β := fun (X : C) ↦ d ⟶ F.obj X)))
have 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)))
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₂
Cleared hypotheses: t