awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Presheaf (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
G : (Cᵒᵖ ⥤ Type (max w v₁ v₂)) ⥤ Dᵒᵖ ⥤ Type (max w v₁ v₂)
φ : F ⋙ uliftYoneda.{max w v₁, v₂, u₂} ⟶ uliftYoneda.{max w v₂, v₁, u₁} ⋙ G
inst_2 : ∀ (P : Cᵒᵖ ⥤ Type (max w v₁ v₂)), F.op.HasLeftKanExtension P
X : C
⊢ presheafHom.{w, v₁, v₂, u₁, u₂} φ (Functor.obj uliftYoneda.{max w v₂, v₁, u₁} X) =
    NatTrans.app F.op.lanUnit (Functor.obj uliftYoneda.{max v₂ w, v₁, u₁} X) ≫
      F.op.whiskerLeft (NatTrans.app (Iso.inv (compULiftYonedaIsoULiftYonedaCompLan.{w, v₁, v₂, u₁, u₂} F)) X ≫ φ.app X)
have hγ : Eq (α := (F.op ⋙ G.obj (Functor.obj uliftYoneda.{max w v₂, v₁, u₁} X)).obj (op X))
  ((uliftYonedaEquiv :
        (a : uliftYoneda.{max v₂ w, v₁, u₁}.obj X ⟶ F.op ⋙ G.obj (uliftYoneda.{max w v₂, v₁, u₁}.obj X)) →
          (F.op ⋙ G.obj (uliftYoneda.{max w v₂, v₁, u₁}.obj X)).obj (op X))
      (presheafHom.{w, v₁, v₂, u₁, u₂} φ (Functor.obj uliftYoneda.{max w v₂, v₁, u₁} X)) :
    (F.op ⋙ G.obj (Functor.obj uliftYoneda.{max w v₂, v₁, u₁} X)).obj (op X))
  ((uliftYonedaEquiv :
        (a : uliftYoneda.{max v₂ w, v₁, u₁}.obj X ⟶ F.op ⋙ G.obj (uliftYoneda.{max w v₂, v₁, u₁}.obj X)) →
          (F.op ⋙ G.obj (uliftYoneda.{max w v₂, v₁, u₁}.obj X)).obj (op X))
      (NatTrans.app F.op.lanUnit (Functor.obj uliftYoneda.{max v₂ w, v₁, u₁} X) ≫
        F.op.whiskerLeft
          (NatTrans.app (Iso.inv (compULiftYonedaIsoULiftYonedaCompLan.{w, v₁, v₂, u₁, u₂} F)) X ≫ φ.app X)) :
    (F.op ⋙ G.obj (Functor.obj uliftYoneda.{max w v₂, v₁, u₁} X)).obj (op X))
Tactic: apply uliftYonedaEquiv.injective
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Presheaf (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
G : (Cᵒᵖ ⥤ Type (max w v₁ v₂)) ⥤ Dᵒᵖ ⥤ Type (max w v₁ v₂)
φ : F ⋙ uliftYoneda.{max w v₁, v₂, u₂} ⟶ uliftYoneda.{max w v₂, v₁, u₁} ⋙ G
inst_2 : ∀ (P : Cᵒᵖ ⥤ Type (max w v₁ v₂)), F.op.HasLeftKanExtension P
X : C
⊢ Eq (α := (F.op ⋙ G.obj (Functor.obj uliftYoneda.{max w v₂, v₁, u₁} X)).obj (op X))
    ((uliftYonedaEquiv :
          (a : uliftYoneda.{max v₂ w, v₁, u₁}.obj X ⟶ F.op ⋙ G.obj (uliftYoneda.{max w v₂, v₁, u₁}.obj X)) →
            (F.op ⋙ G.obj (uliftYoneda.{max w v₂, v₁, u₁}.obj X)).obj (op X))
        (presheafHom.{w, v₁, v₂, u₁, u₂} φ (Functor.obj uliftYoneda.{max w v₂, v₁, u₁} X)) :
      (F.op ⋙ G.obj (Functor.obj uliftYoneda.{max w v₂, v₁, u₁} X)).obj (op X))
    ((uliftYonedaEquiv :
          (a : uliftYoneda.{max v₂ w, v₁, u₁}.obj X ⟶ F.op ⋙ G.obj (uliftYoneda.{max w v₂, v₁, u₁}.obj X)) →
            (F.op ⋙ G.obj (uliftYoneda.{max w v₂, v₁, u₁}.obj X)).obj (op X))
        (NatTrans.app F.op.lanUnit (Functor.obj uliftYoneda.{max v₂ w, v₁, u₁} X) ≫
          F.op.whiskerLeft
            (NatTrans.app (Iso.inv (compULiftYonedaIsoULiftYonedaCompLan.{w, v₁, v₂, u₁, u₂} F)) X ≫ φ.app X)) :
      (F.op ⋙ G.obj (Functor.obj uliftYoneda.{max w v₂, v₁, u₁} X)).obj (op X))
have hγ : Eq (α := (F.op ⋙ G.obj (Functor.obj uliftYoneda.{max w v₂, v₁, u₁} X)).obj (op X))
  ((hom (FC := TypeCat.Fun) ((φ.app X).app (F.op.obj (op X))) :
        (a :
            (fun (X : Type (max (max v₁ v₂) w)) ↦ X)
              (((F ⋙ uliftYoneda.{max w v₁, v₂, u₂}).obj X).obj (F.op.obj (op X)))) →
          (fun (X : Type (max (max v₁ v₂) w)) ↦ X) (((uliftYoneda.{max w v₂, v₁, u₁} ⋙ G).obj X).obj (F.op.obj (op X))))
      { down := 𝟙 (unop (F.op.obj (op X))) } :
    (fun (X : Type (max (max v₁ v₂) w)) ↦ X) (((uliftYoneda.{max w v₂, v₁, u₁} ⋙ G).obj X).obj (F.op.obj (op X))))
  ((uliftYonedaEquiv :
        (a : uliftYoneda.{max v₂ w, v₁, u₁}.obj X ⟶ F.op ⋙ G.obj (uliftYoneda.{max w v₂, v₁, u₁}.obj X)) →
          (F.op ⋙ G.obj (uliftYoneda.{max w v₂, v₁, u₁}.obj X)).obj (op X))
      (NatTrans.app F.op.lanUnit (Functor.obj uliftYoneda.{max v₂ w, v₁, u₁} X) ≫
        F.op.whiskerLeft
          (NatTrans.app (Iso.inv (compULiftYonedaIsoULiftYonedaCompLan.{w, v₁, v₂, u₁, u₂} F)) X ≫ φ.app X)) :
    (F.op ⋙ G.obj (Functor.obj uliftYoneda.{max w v₂, v₁, u₁} X)).obj (op X))
Tactic: rw [uliftYonedaEquiv_presheafHom_uliftYoneda_obj]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Presheaf (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
ℰ : Type u₂
inst_1 : Category.{v₂, u₂} ℰ
A_1 A : Functor.{v₁, v₂, u₁, u₂} C ℰ
inst_2 : Functor.HasPointwiseLeftKanExtension uliftYoneda.{max w v₂, v₁, u₁} A
D : Type u₂
inst_3 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : ∀ (P : Cᵒᵖ ⥤ Type (max w v₁ v₂)), F.op.HasLeftKanExtension P
Φ : Functor.LeftExtension uliftYoneda.{max w v₂, v₁, u₁} (F ⋙ uliftYoneda.{max w v₁, v₂, u₂})
⊢ StructuredArrow.hom
        (Functor.LeftExtension.mk F.op.lan (Iso.hom (compULiftYonedaIsoULiftYonedaCompLan.{w, v₁, v₂, u₁, u₂} F))) ≫
      Functor.map
        (Functor.obj (Functor.whiskeringLeft C (Cᵒᵖ ⥤ Type (max (max w v₁) v₂)) (Dᵒᵖ ⥤ Type (max (max w v₁) v₂)))
          uliftYoneda.{max w v₂, v₁, u₁})
        (natTrans.{w, v₁, v₂, u₁, u₂} (StructuredArrow.hom Φ)) =
    StructuredArrow.hom Φ
have w : ∀ (X : C),
  (StructuredArrow.hom
            (Functor.LeftExtension.mk F.op.lan (Iso.hom (compULiftYonedaIsoULiftYonedaCompLan.{w, v₁, v₂, u₁, u₂} F))) ≫
          Functor.map
            (Functor.obj (Functor.whiskeringLeft C (Cᵒᵖ ⥤ Type (max (max w v₁) v₂)) (Dᵒᵖ ⥤ Type (max (max w v₁) v₂)))
              uliftYoneda.{max w v₂, v₁, u₁})
            (natTrans.{w, v₁, v₂, u₁, u₂} (StructuredArrow.hom Φ))).app
      X =
    (StructuredArrow.hom Φ).app X
Tactic: ext X : 2
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Presheaf (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
ℰ : Type u₂
inst_1 : Category.{v₂, u₂} ℰ
A_1 A : Functor.{v₁, v₂, u₁, u₂} C ℰ
inst_2 : Functor.HasPointwiseLeftKanExtension uliftYoneda.{max w v₂, v₁, u₁} A
D : Type u₂
inst_3 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : ∀ (P : Cᵒᵖ ⥤ Type (max w v₁ v₂)), F.op.HasLeftKanExtension P
Φ : Functor.LeftExtension uliftYoneda.{max w v₂, v₁, u₁} (F ⋙ uliftYoneda.{max w v₁, v₂, u₂})
X : C
⊢ (StructuredArrow.hom
            (Functor.LeftExtension.mk F.op.lan (Iso.hom (compULiftYonedaIsoULiftYonedaCompLan.{w, v₁, v₂, u₁, u₂} F))) ≫
          Functor.map
            (Functor.obj (Functor.whiskeringLeft C (Cᵒᵖ ⥤ Type (max (max w v₁) v₂)) (Dᵒᵖ ⥤ Type (max (max w v₁) v₂)))
              uliftYoneda.{max w v₂, v₁, u₁})
            (natTrans.{w, v₁, v₂, u₁, u₂} (StructuredArrow.hom Φ))).app
      X =
    (StructuredArrow.hom Φ).app X
have w : NatTrans.app (Iso.hom (compULiftYonedaIsoULiftYonedaCompLan.{w, v₁, v₂, u₁, u₂} F)) X ≫
    NatTrans.app (natTrans.{w, v₁, v₂, u₁, u₂} (StructuredArrow.hom Φ)) (Functor.obj uliftYoneda.{max w v₂, v₁, u₁} X) =
  (StructuredArrow.hom Φ).app X
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Presheaf (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
ℰ : Type u₂
inst_1 : Category.{v₂, u₂} ℰ
A_1 A : Functor.{v₁, v₂, u₁, u₂} C ℰ
inst_2 : Functor.HasPointwiseLeftKanExtension uliftYoneda.{max w v₂, v₁, u₁} A
D : Type u₂
inst_3 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : ∀ (P : Cᵒᵖ ⥤ Type (max w v₁ v₂)), F.op.HasLeftKanExtension P
Φ : Functor.LeftExtension uliftYoneda.{max w v₂, v₁, u₁} (F ⋙ uliftYoneda.{max w v₁, v₂, u₂})
X : C
⊢ NatTrans.app (Iso.hom (compULiftYonedaIsoULiftYonedaCompLan.{w, v₁, v₂, u₁, u₂} F)) X ≫
      NatTrans.app (natTrans.{w, v₁, v₂, u₁, u₂} (StructuredArrow.hom Φ))
        (Functor.obj uliftYoneda.{max w v₂, v₁, u₁} X) =
    (StructuredArrow.hom Φ).app X
have w : CategoryStruct.comp (Y := Functor.obj F.op.lan (Functor.obj uliftYoneda.{max w v₂, v₁, u₁} X))
    (NatTrans.app (Iso.hom (compULiftYonedaIsoULiftYonedaCompLan.{w, v₁, v₂, u₁, u₂} F)) X)
    (NatTrans.app (Iso.inv (compULiftYonedaIsoULiftYonedaCompLan.{w, v₁, v₂, u₁, u₂} F)) X ≫
      (StructuredArrow.hom Φ).app X) =
  (StructuredArrow.hom Φ).app X
Tactic: rw [natTrans_app_uliftYoneda_obj, Iso.hom_inv_id_app_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Presheaf (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
ℰ : Type u₂
inst_1 : Category.{v₂, u₂} ℰ
A_1 A : Functor.{v₁, v₂, u₁, u₂} C ℰ
inst_2 : Functor.HasPointwiseLeftKanExtension uliftYoneda.{max w v₂, v₁, u₁} A
D : Type u₂
inst_3 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : ∀ (P : Cᵒᵖ ⥤ Type (max w v₁ v₂)), F.op.HasLeftKanExtension P
Φ : Functor.LeftExtension uliftYoneda.{max w v₂, v₁, u₁} (F ⋙ uliftYoneda.{max w v₁, v₂, u₂})
X : C
w :
  CategoryStruct.comp (Y := Functor.obj F.op.lan (Functor.obj uliftYoneda.{max w v₂, v₁, u₁} X))
      (NatTrans.app (Iso.hom (compULiftYonedaIsoULiftYonedaCompLan.{w, v₁, v₂, u₁, u₂} F)) X)
      (NatTrans.app (Iso.inv (compULiftYonedaIsoULiftYonedaCompLan.{w, v₁, v₂, u₁, u₂} F)) X ≫
        (StructuredArrow.hom Φ).app X) =
    (StructuredArrow.hom Φ).app X
⊢ NatTrans.app (Iso.hom (compULiftYonedaIsoULiftYonedaCompLan.{w, v₁, v₂, u₁, u₂} F)) X ≫
      NatTrans.app (natTrans.{w, v₁, v₂, u₁, u₂} (StructuredArrow.hom Φ))
        (Functor.obj uliftYoneda.{max w v₂, v₁, u₁} X) =
    (StructuredArrow.hom Φ).app X
have w₁ : (StructuredArrow.hom Φ).app X = (StructuredArrow.hom Φ).app X
Tactic: rw [natTrans_app_uliftYoneda_obj, Iso.hom_inv_id_app_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Presheaf (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 : ∀ (P : Cᵒᵖ ⥤ Type (max w v₁ v₂)), F.op.HasLeftKanExtension P
Φ : Functor.LeftExtension uliftYoneda.{max w v₂, v₁, u₁} (F ⋙ uliftYoneda.{max w v₁, v₂, u₂})
f g : Functor.LeftExtension.mk F.op.lan (Iso.hom (compULiftYonedaIsoULiftYonedaCompLan.{w, v₁, v₂, u₁, u₂} F)) ⟶ Φ
⊢ f = g
have h : ∀ (P : Cᵒᵖ ⥤ Type (max (max w v₁) v₂)), (StructuredArrow.Hom.right f).app P = (StructuredArrow.Hom.right g).app P
Tactic: ext P : 3
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Presheaf (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 : ∀ (P : Cᵒᵖ ⥤ Type (max w v₁ v₂)), F.op.HasLeftKanExtension P
Φ : Functor.LeftExtension uliftYoneda.{max w v₂, v₁, u₁} (F ⋙ uliftYoneda.{max w v₁, v₂, u₂})
f g : Functor.LeftExtension.mk F.op.lan (Iso.hom (compULiftYonedaIsoULiftYonedaCompLan.{w, v₁, v₂, u₁, u₂} F)) ⟶ Φ
P : Cᵒᵖ ⥤ Type (max (max w v₁) v₂)
⊢ (StructuredArrow.Hom.right f).app P = (StructuredArrow.Hom.right g).app P
have h : NatTrans.app F.op.lanUnit P ≫ F.op.whiskerLeft ((StructuredArrow.Hom.right f).app P) =
  NatTrans.app F.op.lanUnit P ≫ F.op.whiskerLeft ((StructuredArrow.Hom.right g).app P)
Tactic: apply (F.op.lan.obj P).hom_ext_of_isLeftKanExtension (F.op.lanUnit.app P)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Presheaf (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 : ∀ (P : Cᵒᵖ ⥤ Type (max w v₁ v₂)), F.op.HasLeftKanExtension P
Φ : Functor.LeftExtension uliftYoneda.{max w v₂, v₁, u₁} (F ⋙ uliftYoneda.{max w v₁, v₂, u₂})
f g : Functor.LeftExtension.mk F.op.lan (Iso.hom (compULiftYonedaIsoULiftYonedaCompLan.{w, v₁, v₂, u₁, u₂} F)) ⟶ Φ
P : Cᵒᵖ ⥤ Type (max (max w v₁) v₂)
⊢ NatTrans.app F.op.lanUnit P ≫ F.op.whiskerLeft ((StructuredArrow.Hom.right f).app P) =
    NatTrans.app F.op.lanUnit P ≫ F.op.whiskerLeft ((StructuredArrow.Hom.right g).app P)
have h : ∀ (j : P.Elementsᵒᵖ),
  (coconeOfRepresentable P).ι.app j ≫
      NatTrans.app F.op.lanUnit P ≫ F.op.whiskerLeft ((StructuredArrow.Hom.right f).app P) =
    (coconeOfRepresentable P).ι.app j ≫
      NatTrans.app F.op.lanUnit P ≫ F.op.whiskerLeft ((StructuredArrow.Hom.right g).app P)
Tactic: apply (colimitOfRepresentable.{max w v₂} P).hom_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Presheaf (hypothesis)
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 : ∀ (P : Cᵒᵖ ⥤ Type (max w v₁ v₂)), F.op.HasLeftKanExtension P
Φ : Functor.LeftExtension uliftYoneda.{max w v₂, v₁, u₁} (F ⋙ uliftYoneda.{max w v₁, v₂, u₂})
f g : Functor.LeftExtension.mk F.op.lan (Iso.hom (compULiftYonedaIsoULiftYonedaCompLan.{w, v₁, v₂, u₁, u₂} F)) ⟶ Φ
P : Cᵒᵖ ⥤ Type (max (max w v₁) v₂)
x : P.Elementsᵒᵖ
⊢ (coconeOfRepresentable P).ι.app x ≫
      NatTrans.app F.op.lanUnit P ≫ F.op.whiskerLeft ((StructuredArrow.Hom.right f).app P) =
    (coconeOfRepresentable P).ι.app x ≫
      NatTrans.app F.op.lanUnit P ≫ F.op.whiskerLeft ((StructuredArrow.Hom.right g).app P)
have eq : Eq (α :=
  Functor.obj (𝟭 (Cᵒᵖ ⥤ Type (max (max w v₂) v₁))) (Functor.obj uliftYoneda.{max w v₂, v₁, u₁} (unop (unop x).1)) ⟶
    Functor.obj (F.op.lan ⋙ Functor.obj (Functor.whiskeringLeft Cᵒᵖ Dᵒᵖ (Type (max (max w v₂) v₁))) F.op) P)
  (Functor.map (𝟭 (Cᵒᵖ ⥤ Type (max (max w v₂) v₁)))
        ((Equiv.symm uliftYonedaEquiv :
            (a : P.obj (op (unop (unop x).1))) → uliftYoneda.{max w v₂, v₁, u₁}.obj (unop (unop x).1) ⟶ P)
          ((unop x).snd (β := fun (c : Cᵒᵖ) ↦ P.obj c))) ≫
      NatTrans.app F.op.lanUnit P :
    Functor.obj (𝟭 (Cᵒᵖ ⥤ Type (max (max w v₂) v₁))) (Functor.obj uliftYoneda.{max w v₂, v₁, u₁} (unop (unop x).1)) ⟶
      Functor.obj (F.op.lan ⋙ Functor.obj (Functor.whiskeringLeft Cᵒᵖ Dᵒᵖ (Type (max (max w v₂) v₁))) F.op) P)
  (NatTrans.app F.op.lanUnit (Functor.obj uliftYoneda.{max w v₂, v₁, u₁} (unop (unop x).1)) ≫
      Functor.map (F.op.lan ⋙ Functor.obj (Functor.whiskeringLeft Cᵒᵖ Dᵒᵖ (Type (max (max w v₂) v₁))) F.op)
        ((Equiv.symm uliftYonedaEquiv :
            (a : P.obj (op (unop (unop x).1))) → uliftYoneda.{max w v₂, v₁, u₁}.obj (unop (unop x).1) ⟶ P)
          ((unop x).snd (β := fun (c : Cᵒᵖ) ↦ P.obj c))) :
    Functor.obj (𝟭 (Cᵒᵖ ⥤ Type (max (max w v₂) v₁))) (Functor.obj uliftYoneda.{max w v₂, v₁, u₁} (unop (unop x).1)) ⟶
      Functor.obj (F.op.lan ⋙ Functor.obj (Functor.whiskeringLeft Cᵒᵖ Dᵒᵖ (Type (max (max w v₂) v₁))) F.op) P)
Tactic: have eq := F.op.lanUnit.naturality (uliftYonedaEquiv.{max w v₂}.symm x.unop.2)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Presheaf (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
I : Type v₁
inst_1 : SmallCategory I
F : I ⥤ C
c : Cocone (F ⋙ yoneda)
hc : IsColimit c
⊢ (c.toCostructuredArrow ⋙ CostructuredArrow.pre F yoneda c.pt).Final
have h : IsTerminal (colimit ((c.toCostructuredArrow ⋙ CostructuredArrow.pre F yoneda c.pt) ⋙ yoneda))
Tactic: apply Functor.final_of_isTerminal_colimit_comp_yoneda
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Presheaf (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
I : Type v₁
inst_1 : SmallCategory I
F : I ⥤ C
c : Cocone (F ⋙ yoneda)
hc : IsColimit c
this :
  IsTerminal
    (colimit ((c.toCostructuredArrow ⋙ CostructuredArrow.pre F yoneda c.pt) ⋙ CostructuredArrow.toOver yoneda c.pt))
⊢ IsTerminal (colimit ((c.toCostructuredArrow ⋙ CostructuredArrow.pre F yoneda c.pt) ⋙ yoneda))
have l : IsTerminal
  ((overEquivPresheafCostructuredArrow c.pt).inverse.obj
    (colimit ((c.toCostructuredArrow ⋙ CostructuredArrow.pre F yoneda c.pt) ⋙ yoneda)))
Tactic: apply IsTerminal.isTerminalOfObj (overEquivPresheafCostructuredArrow c.pt).inverse
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Presheaf (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
I : Type v₁
inst_1 : SmallCategory I
F : I ⥤ C
c : Cocone (F ⋙ yoneda)
hc : IsColimit c
this :
  IsTerminal
    (colimit ((c.toCostructuredArrow ⋙ CostructuredArrow.pre F yoneda c.pt) ⋙ CostructuredArrow.toOver yoneda c.pt))
⊢ IsTerminal
    ((overEquivPresheafCostructuredArrow c.pt).inverse.obj
      (colimit ((c.toCostructuredArrow ⋙ CostructuredArrow.pre F yoneda c.pt) ⋙ yoneda)))
have l : colimit ((c.toCostructuredArrow ⋙ CostructuredArrow.pre F yoneda c.pt) ⋙ CostructuredArrow.toOver yoneda c.pt) ≅
  (overEquivPresheafCostructuredArrow c.pt).inverse.obj
    (colimit ((c.toCostructuredArrow ⋙ CostructuredArrow.pre F yoneda c.pt) ⋙ yoneda))
Tactic: apply IsTerminal.ofIso this
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Presheaf (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
I : Type v₁
inst_1 : SmallCategory I
F : I ⥤ C
c : Cocone (F ⋙ yoneda)
hc : IsColimit c
this :
  IsTerminal
    (colimit ((c.toCostructuredArrow ⋙ CostructuredArrow.pre F yoneda c.pt) ⋙ CostructuredArrow.toOver yoneda c.pt))
⊢ colimit ((c.toCostructuredArrow ⋙ CostructuredArrow.pre F yoneda c.pt) ⋙ CostructuredArrow.toOver yoneda c.pt) ≅
    (overEquivPresheafCostructuredArrow c.pt).inverse.obj
      (colimit ((c.toCostructuredArrow ⋙ CostructuredArrow.pre F yoneda c.pt) ⋙ yoneda))
have l : colimit ((c.toCostructuredArrow ⋙ CostructuredArrow.pre F yoneda c.pt) ⋙ CostructuredArrow.toOver yoneda c.pt) ≅
  colimit
    (((c.toCostructuredArrow ⋙ CostructuredArrow.pre F yoneda c.pt) ⋙ yoneda) ⋙
      (overEquivPresheafCostructuredArrow c.pt).inverse)
Tactic: refine ?_ ≪≫ (preservesColimitIso (overEquivPresheafCostructuredArrow c.pt).inverse _).symm
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Presheaf (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
I : Type v₁
inst_1 : SmallCategory I
F : I ⥤ C
c : Cocone (F ⋙ yoneda)
hc : IsColimit c
this :
  IsTerminal
    (colimit ((c.toCostructuredArrow ⋙ CostructuredArrow.pre F yoneda c.pt) ⋙ CostructuredArrow.toOver yoneda c.pt))
⊢ colimit ((c.toCostructuredArrow ⋙ CostructuredArrow.pre F yoneda c.pt) ⋙ CostructuredArrow.toOver yoneda c.pt) ≅
    colimit
      (((c.toCostructuredArrow ⋙ CostructuredArrow.pre F yoneda c.pt) ⋙ yoneda) ⋙
        (overEquivPresheafCostructuredArrow c.pt).inverse)
have l : (c.toCostructuredArrow ⋙ CostructuredArrow.pre F yoneda c.pt) ⋙ CostructuredArrow.toOver yoneda c.pt ≅
  ((c.toCostructuredArrow ⋙ CostructuredArrow.pre F yoneda c.pt) ⋙ yoneda) ⋙
    (overEquivPresheafCostructuredArrow c.pt).inverse
Tactic: apply HasColimit.isoOfNatIso
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Presheaf (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
I : Type v₁
inst_1 : SmallCategory I
F : I ⥤ C
c : Cocone (F ⋙ yoneda)
hc : IsColimit c
⊢ IsTerminal (colimit ((c.toCostructuredArrow ⋙ CostructuredArrow.pre F yoneda c.pt) ⋙ yoneda))
have h : IsTerminal
  (colimit ((c.toCostructuredArrow ⋙ CostructuredArrow.pre F yoneda c.pt) ⋙ CostructuredArrow.toOver yoneda c.pt))
Tactic: suffices IsTerminal (colimit ((c.toCostructuredArrow ⋙ CostructuredArrow.pre F yoneda c.pt) ⋙
      CostructuredArrow.toOver yoneda c.pt)) by
    apply IsTerminal.isTerminalOfObj (overEquivPresheafCostructuredArrow c.pt).inverse
    apply IsTerminal.ofIso this
    refine ?_ ≪≫ (preservesColimitIso (overEquivPresheafCostructuredArrow c.pt).inverse _).symm
    apply HasColimit.isoOfNatIso
    exact Functor.isoWhiskerLeft _
      (CostructuredArrow.toOverCompOverEquivPresheafCostructuredArrow c.pt).isoCompInverse
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Presheaf (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
I : Type v₁
inst_1 : SmallCategory I
F : I ⥤ C
c : Cocone (F ⋙ yoneda)
hc : IsColimit c
⊢ IsTerminal
    (colimit ((c.toCostructuredArrow ⋙ CostructuredArrow.pre F yoneda c.pt) ⋙ CostructuredArrow.toOver yoneda c.pt))
have h : Over.mk (𝟙 c.pt) ≅
  colimit ((c.toCostructuredArrow ⋙ CostructuredArrow.pre F yoneda c.pt) ⋙ CostructuredArrow.toOver yoneda c.pt)
Tactic: apply IsTerminal.ofIso Over.mkIdTerminal
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Presheaf (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : LocallySmall.{w, v₁, u₁} C
F : Functor.{v₁, w, u₁, w + 1} C (Type w)
X : C
⊢ IsColimit (F := (CategoryOfElements.π F).op ⋙ obj shrinkYoneda.{w, v₁, u₁} X) (coconeπOpCompShrinkYonedaObj F X)
have refine_1 : Function.Injective (β :=
  CoconeTypes.pt (J := F.Elementsᵒᵖ) (F := (CategoryOfElements.π F).op ⋙ obj shrinkYoneda.{w, v₁, u₁} X)
    ((((CategoryOfElements.π F).op ⋙ obj shrinkYoneda.{w, v₁, u₁} X).coconeTypesEquiv.symm :
        (a : Cocone ((CategoryOfElements.π F).op ⋙ shrinkYoneda.{w, v₁, u₁}.obj X)) →
          ((CategoryOfElements.π F).op ⋙ shrinkYoneda.{w, v₁, u₁}.obj X).CoconeTypes)
      (coconeπOpCompShrinkYonedaObj F X)))
  (((CategoryOfElements.π F).op ⋙ obj shrinkYoneda.{w, v₁, u₁} X).descColimitType
    ((((CategoryOfElements.π F).op ⋙ obj shrinkYoneda.{w, v₁, u₁} X).coconeTypesEquiv.symm :
        (a : Cocone ((CategoryOfElements.π F).op ⋙ shrinkYoneda.{w, v₁, u₁}.obj X)) →
          ((CategoryOfElements.π F).op ⋙ shrinkYoneda.{w, v₁, u₁}.obj X).CoconeTypes)
      (coconeπOpCompShrinkYonedaObj F X)))
Tactic: refine Nonempty.some ((Types.isColimit_iff_coconeTypesIsColimit _).2
    ⟨?_, fun x ↦ ?_⟩)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Presheaf (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : LocallySmall.{w, v₁, u₁} C
F : Functor.{v₁, w, u₁, w + 1} C (Type w)
X : C
refine_1 :
  Function.Injective (β :=
    CoconeTypes.pt (J := F.Elementsᵒᵖ) (F := (CategoryOfElements.π F).op ⋙ obj shrinkYoneda.{w, v₁, u₁} X)
      ((((CategoryOfElements.π F).op ⋙ obj shrinkYoneda.{w, v₁, u₁} X).coconeTypesEquiv.symm :
          (a : Cocone ((CategoryOfElements.π F).op ⋙ shrinkYoneda.{w, v₁, u₁}.obj X)) →
            ((CategoryOfElements.π F).op ⋙ shrinkYoneda.{w, v₁, u₁}.obj X).CoconeTypes)
        (coconeπOpCompShrinkYonedaObj F X)))
    (((CategoryOfElements.π F).op ⋙ obj shrinkYoneda.{w, v₁, u₁} X).descColimitType
      ((((CategoryOfElements.π F).op ⋙ obj shrinkYoneda.{w, v₁, u₁} X).coconeTypesEquiv.symm :
          (a : Cocone ((CategoryOfElements.π F).op ⋙ shrinkYoneda.{w, v₁, u₁}.obj X)) →
            ((CategoryOfElements.π F).op ⋙ shrinkYoneda.{w, v₁, u₁}.obj X).CoconeTypes)
        (coconeπOpCompShrinkYonedaObj F X)))
⊢ IsColimit (F := (CategoryOfElements.π F).op ⋙ obj shrinkYoneda.{w, v₁, u₁} X) (coconeπOpCompShrinkYonedaObj F X)
have refine_2 : ∀
  (x :
    CoconeTypes.pt (J := F.Elementsᵒᵖ) (F := (CategoryOfElements.π F).op ⋙ obj shrinkYoneda.{w, v₁, u₁} X)
      ((((CategoryOfElements.π F).op ⋙ obj shrinkYoneda.{w, v₁, u₁} X).coconeTypesEquiv.symm :
          (a : Cocone ((CategoryOfElements.π F).op ⋙ shrinkYoneda.{w, v₁, u₁}.obj X)) →
            ((CategoryOfElements.π F).op ⋙ shrinkYoneda.{w, v₁, u₁}.obj X).CoconeTypes)
        (coconeπOpCompShrinkYonedaObj F X))),
  ∃ (a : ((CategoryOfElements.π F).op ⋙ obj shrinkYoneda.{w, v₁, u₁} X).ColimitType),
    ((CategoryOfElements.π F).op ⋙ obj shrinkYoneda.{w, v₁, u₁} X).descColimitType
        ((((CategoryOfElements.π F).op ⋙ obj shrinkYoneda.{w, v₁, u₁} X).coconeTypesEquiv.symm :
            (a : Cocone ((CategoryOfElements.π F).op ⋙ shrinkYoneda.{w, v₁, u₁}.obj X)) →
              ((CategoryOfElements.π F).op ⋙ shrinkYoneda.{w, v₁, u₁}.obj X).CoconeTypes)
          (coconeπOpCompShrinkYonedaObj F X))
        a =
      x
Tactic: refine Nonempty.some ((Types.isColimit_iff_coconeTypesIsColimit _).2
    ⟨?_, fun x ↦ ?_⟩)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Presheaf (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : LocallySmall.{w, v₁, u₁} C
F : Functor.{v₁, w, u₁, w + 1} C (Type w)
X : C
G : F.Elementsᵒᵖ ⥤ Type w := (CategoryOfElements.π F).op ⋙ obj shrinkYoneda.{w, v₁, u₁} X
c : G.CoconeTypes := (G.coconeTypesEquiv.symm : (a : Cocone G) → G.CoconeTypes) (coconeπOpCompShrinkYonedaObj F X)
u : G.ColimitType
x : F.obj X
h : G.descColimitType c u = x
⊢ G.ιColimitType (op (F.elementsMk X x))
      ((Equiv.symm shrinkYonedaObjObjEquiv :
          (a : unop ((CategoryOfElements.π F).op.obj (op (F.elementsMk X x))) ⟶ X) →
            (shrinkYoneda.{w, v₁, u₁}.obj X).obj ((CategoryOfElements.π F).op.obj (op (F.elementsMk X x))))
        (𝟙 X)) =
    u
have obtain : ∀ (u : F.Elements) (v : G.obj (op u)) (h : G.descColimitType c (G.ιColimitType (op u) v) = x),
  G.ιColimitType (op (F.elementsMk X x))
      ((Equiv.symm shrinkYonedaObjObjEquiv :
          (a : unop ((CategoryOfElements.π F).op.obj (op (F.elementsMk X x))) ⟶ X) →
            (shrinkYoneda.{w, v₁, u₁}.obj X).obj ((CategoryOfElements.π F).op.obj (op (F.elementsMk X x))))
        (𝟙 X)) =
    G.ιColimitType (op u) v
Tactic: obtain ⟨⟨u⟩, v, rfl⟩ := Functor.ιColimitType_jointly_surjective _ u
Cleared hypotheses: u, h