awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.IndYoneda (goal)
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
I : Type v₁
inst_1 : Category.{v₂, v₁} I
D : Functor.{v₂, u₂, v₁, u₁} I C
F : C ⥤ Type u₂
inst_2 : HasColimit (D.op ⋙ coyoneda)
inst_3 : HasLimitsOfShape I (Type (max u₁ u₂))
f : colimit (D.op ⋙ coyoneda) ⟶ F
i : I
⊢ Eq (α := (D ⋙ F ⋙ uliftFunctor.{u₁, u₂}).obj i)
    (((@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
              (CategoryStruct.comp (Y := ((D.op ⋙ coyoneda).rightOp ⋙ Functor.obj yoneda F).obj i)
                (Functor.map (Functor.obj yoneda F) (Quiver.Hom.op (colimit.ι (D.op ⋙ coyoneda) (op i))))
                (NatTrans.app (Iso.hom (Functor.isoWhiskerLeft (D ⋙ Prod.sectL C F) (coyonedaLemma C))) i)) :
            TypeCat.Fun (colimit (D.op ⋙ coyoneda) ⟶ F) ((D ⋙ F ⋙ uliftFunctor.{u₁, u₂}).obj i)) :
          (a : colimit (D.op ⋙ coyoneda) ⟶ F) → (D ⋙ F ⋙ uliftFunctor.{u₁, u₂}).obj i)
        f :
      (D ⋙ F ⋙ uliftFunctor.{u₁, u₂}).obj i)
    ({
        down :=
          (ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (D.obj i)) :
              (a : (colimit (D.op ⋙ coyoneda)).obj (D.obj i)) → F.obj (D.obj i))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (colimit.ι (D.op ⋙ coyoneda) (op i)) (D.obj i)) :
                  (a : D.obj i ⟶ D.obj i) → (colimit (D.op ⋙ coyoneda)).obj (D.obj i))
                (𝟙 (D.obj i)) :
              (colimit (D.op ⋙ coyoneda)).obj (D.obj i)) } :
      ULift.{u₁, u₂} (F.obj (D.obj i)))
have dsimp : Eq (α := ULift.{u₁, u₂} (F.obj (D.obj i)))
  ((ConcreteCategory.hom (FC := TypeCat.Fun)
          ((↾fun (g : colimit (D.op ⋙ coyoneda) ⟶ F) ↦ colimit.ι (D.op ⋙ coyoneda) (op i) ≫ g) ≫
            Iso.hom (Equiv.toIso (Equiv.trans coyonedaEquiv (Equiv.symm Equiv.ulift)))) :
        (a : colimit (D.op ⋙ coyoneda) ⟶ F) → ULift.{u₁, u₂} (F.obj (D.obj i)))
      f :
    ULift.{u₁, u₂} (F.obj (D.obj i)))
  ({
      down :=
        (ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (D.obj i)) :
            (a : (colimit (D.op ⋙ coyoneda)).obj (D.obj i)) → F.obj (D.obj i))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (colimit.ι (D.op ⋙ coyoneda) (op i)) (D.obj i)) :
                (a : D.obj i ⟶ D.obj i) → (colimit (D.op ⋙ coyoneda)).obj (D.obj i))
              (𝟙 (D.obj i)) :
            (colimit (D.op ⋙ coyoneda)).obj (D.obj i)) } :
    ULift.{u₁, u₂} (F.obj (D.obj i)))
Tactic: dsimp [coyonedaLemma]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.IndYoneda (goal)
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
I : Type v₁
inst_1 : Category.{v₂, v₁} I
D : Functor.{v₂, u₂, v₁, u₁} I Cᵒᵖ
F : Functor.{u₂, u₂, u₁, u₂ + 1} Cᵒᵖ (Type u₂)
inst_2 : HasColimit (D.leftOp ⋙ yoneda)
inst_3 : HasLimitsOfShape I (Type (max u₁ u₂))
f : colimit (D.leftOp ⋙ yoneda) ⟶ F
i : I
⊢ Eq (α := (fun (X : Type (max u₁ u₂)) ↦ X) ((D ⋙ F ⋙ uliftFunctor.{u₁, u₂}).obj i))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (CategoryStruct.comp (Y := limit (D ⋙ F ⋙ uliftFunctor.{u₁, u₂}))
              (Iso.hom (colimitYonedaHomIsoLimit' D F) :
                (colimit (D.leftOp ⋙ yoneda) ⟶ F) ⟶ limit (D ⋙ F ⋙ uliftFunctor.{u₁, u₂}))
              (limit.π (D ⋙ F ⋙ uliftFunctor.{u₁, u₂}) i :
                limit (D ⋙ F ⋙ uliftFunctor.{u₁, u₂}) ⟶ (D ⋙ F ⋙ uliftFunctor.{u₁, u₂}).obj i)) :
          (a : (fun (X : Type (max u₁ u₂)) ↦ X) (colimit (D.leftOp ⋙ yoneda) ⟶ F)) →
            (fun (X : Type (max u₁ u₂)) ↦ X) ((D ⋙ F ⋙ uliftFunctor.{u₁, u₂}).obj i))
        f :
      (fun (X : Type (max u₁ u₂)) ↦ X) ((D ⋙ F ⋙ uliftFunctor.{u₁, u₂}).obj i))
    ({
        down :=
          (ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (D.obj i)) :
              (a : (colimit (D.leftOp ⋙ yoneda)).obj (D.obj i)) → F.obj (D.obj i))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (colimit.ι (D.leftOp ⋙ yoneda) (op i)) (D.obj i)) :
                  (a : unop (D.obj i) ⟶ unop (D.obj i)) → (colimit (D.leftOp ⋙ yoneda)).obj (D.obj i))
                (𝟙 (unop (D.obj i))) :
              (colimit (D.leftOp ⋙ yoneda)).obj (D.obj i)) } :
      ULift.{u₁, u₂} (F.obj (D.obj i)))
have simp : Eq (α := (D ⋙ F ⋙ uliftFunctor.{u₁, u₂}).obj i)
  ((ConcreteCategory.hom (FC := TypeCat.Fun)
          (Iso.hom (colimitHomIsoLimitYoneda' (D.leftOp ⋙ yoneda) F) ≫
            limit.π ((D.leftOp ⋙ yoneda).rightOp ⋙ Functor.obj yoneda F) i ≫
              NatTrans.app (Iso.hom (Functor.isoWhiskerLeft (D ⋙ Prod.sectL Cᵒᵖ F) (yonedaLemma C))) i) :
        (a : colimit (D.leftOp ⋙ yoneda) ⟶ F) → (D ⋙ F ⋙ uliftFunctor.{u₁, u₂}).obj i)
      f :
    (D ⋙ F ⋙ uliftFunctor.{u₁, u₂}).obj i)
  ({
      down :=
        (ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (D.obj i)) :
            (a : (colimit (D.leftOp ⋙ yoneda)).obj (D.obj i)) → F.obj (D.obj i))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (colimit.ι (D.leftOp ⋙ yoneda) (op i)) (D.obj i)) :
                (a : unop (D.obj i) ⟶ unop (D.obj i)) → (colimit (D.leftOp ⋙ yoneda)).obj (D.obj i))
              (𝟙 (unop (D.obj i))) :
            (colimit (D.leftOp ⋙ yoneda)).obj (D.obj i)) } :
    ULift.{u₁, u₂} (F.obj (D.obj i)))
Tactic: simp only [colimitYonedaHomIsoLimit', Iso.trans_hom, Category.assoc, HasLimit.isoOfNatIso_hom_π]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.IndYoneda (goal)
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
I : Type v₁
inst_1 : Category.{v₂, v₁} I
D : Functor.{v₂, u₂, v₁, u₁} I Cᵒᵖ
F : Functor.{u₂, u₂, u₁, u₂ + 1} Cᵒᵖ (Type u₂)
inst_2 : HasColimit (D.leftOp ⋙ yoneda)
inst_3 : HasLimitsOfShape I (Type (max u₁ u₂))
f : colimit (D.leftOp ⋙ yoneda) ⟶ F
i : I
⊢ Eq (α := (D ⋙ F ⋙ uliftFunctor.{u₁, u₂}).obj i)
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (Iso.hom (colimitHomIsoLimitYoneda' (D.leftOp ⋙ yoneda) F) ≫
              limit.π ((D.leftOp ⋙ yoneda).rightOp ⋙ Functor.obj yoneda F) i ≫
                NatTrans.app (Iso.hom (Functor.isoWhiskerLeft (D ⋙ Prod.sectL Cᵒᵖ F) (yonedaLemma C))) i) :
          (a : colimit (D.leftOp ⋙ yoneda) ⟶ F) → (D ⋙ F ⋙ uliftFunctor.{u₁, u₂}).obj i)
        f :
      (D ⋙ F ⋙ uliftFunctor.{u₁, u₂}).obj i)
    ({
        down :=
          (ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (D.obj i)) :
              (a : (colimit (D.leftOp ⋙ yoneda)).obj (D.obj i)) → F.obj (D.obj i))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (colimit.ι (D.leftOp ⋙ yoneda) (op i)) (D.obj i)) :
                  (a : unop (D.obj i) ⟶ unop (D.obj i)) → (colimit (D.leftOp ⋙ yoneda)).obj (D.obj i))
                (𝟙 (unop (D.obj i))) :
              (colimit (D.leftOp ⋙ yoneda)).obj (D.obj i)) } :
      ULift.{u₁, u₂} (F.obj (D.obj i)))
have rw : Eq (α := (D ⋙ F ⋙ uliftFunctor.{u₁, u₂}).obj i)
  (((@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
            (CategoryStruct.comp (Y := ((D.leftOp ⋙ yoneda).rightOp ⋙ Functor.obj yoneda F).obj i)
              (Functor.map (Functor.obj yoneda F) (Quiver.Hom.op (colimit.ι (D.leftOp ⋙ yoneda) (op i))))
              (NatTrans.app (Iso.hom (Functor.isoWhiskerLeft (D ⋙ Prod.sectL Cᵒᵖ F) (yonedaLemma C))) i)) :
          TypeCat.Fun (colimit (D.leftOp ⋙ yoneda) ⟶ F) ((D ⋙ F ⋙ uliftFunctor.{u₁, u₂}).obj i)) :
        (a : colimit (D.leftOp ⋙ yoneda) ⟶ F) → (D ⋙ F ⋙ uliftFunctor.{u₁, u₂}).obj i)
      f :
    (D ⋙ F ⋙ uliftFunctor.{u₁, u₂}).obj i)
  ({
      down :=
        (ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (D.obj i)) :
            (a : (colimit (D.leftOp ⋙ yoneda)).obj (D.obj i)) → F.obj (D.obj i))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (colimit.ι (D.leftOp ⋙ yoneda) (op i)) (D.obj i)) :
                (a : unop (D.obj i) ⟶ unop (D.obj i)) → (colimit (D.leftOp ⋙ yoneda)).obj (D.obj i))
              (𝟙 (unop (D.obj i))) :
            (colimit (D.leftOp ⋙ yoneda)).obj (D.obj i)) } :
    ULift.{u₁, u₂} (F.obj (D.obj i)))
Tactic: rw [← Category.assoc, colimitHomIsoLimitYoneda'_hom_comp_π]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.IndYoneda (goal)
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
I : Type v₁
inst_1 : Category.{v₂, v₁} I
D : Functor.{v₂, u₂, v₁, u₁} I Cᵒᵖ
F : Functor.{u₂, u₂, u₁, u₂ + 1} Cᵒᵖ (Type u₂)
inst_2 : HasColimit (D.leftOp ⋙ yoneda)
inst_3 : HasLimitsOfShape I (Type (max u₁ u₂))
f : colimit (D.leftOp ⋙ yoneda) ⟶ F
i : I
⊢ Eq (α := (D ⋙ F ⋙ uliftFunctor.{u₁, u₂}).obj i)
    (((@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
              (CategoryStruct.comp (Y := ((D.leftOp ⋙ yoneda).rightOp ⋙ Functor.obj yoneda F).obj i)
                (Functor.map (Functor.obj yoneda F) (Quiver.Hom.op (colimit.ι (D.leftOp ⋙ yoneda) (op i))))
                (NatTrans.app (Iso.hom (Functor.isoWhiskerLeft (D ⋙ Prod.sectL Cᵒᵖ F) (yonedaLemma C))) i)) :
            TypeCat.Fun (colimit (D.leftOp ⋙ yoneda) ⟶ F) ((D ⋙ F ⋙ uliftFunctor.{u₁, u₂}).obj i)) :
          (a : colimit (D.leftOp ⋙ yoneda) ⟶ F) → (D ⋙ F ⋙ uliftFunctor.{u₁, u₂}).obj i)
        f :
      (D ⋙ F ⋙ uliftFunctor.{u₁, u₂}).obj i)
    ({
        down :=
          (ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (D.obj i)) :
              (a : (colimit (D.leftOp ⋙ yoneda)).obj (D.obj i)) → F.obj (D.obj i))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (colimit.ι (D.leftOp ⋙ yoneda) (op i)) (D.obj i)) :
                  (a : unop (D.obj i) ⟶ unop (D.obj i)) → (colimit (D.leftOp ⋙ yoneda)).obj (D.obj i))
                (𝟙 (unop (D.obj i))) :
              (colimit (D.leftOp ⋙ yoneda)).obj (D.obj i)) } :
      ULift.{u₁, u₂} (F.obj (D.obj i)))
have dsimp : Eq (α := ULift.{u₁, u₂} (F.obj (D.obj i)))
  ((ConcreteCategory.hom (FC := TypeCat.Fun)
          ((↾fun (g : colimit (D.leftOp ⋙ yoneda) ⟶ F) ↦ colimit.ι (D.leftOp ⋙ yoneda) (op i) ≫ g) ≫
            Iso.hom (Equiv.toIso (Equiv.trans yonedaEquiv (Equiv.symm Equiv.ulift)))) :
        (a : colimit (D.leftOp ⋙ yoneda) ⟶ F) → ULift.{u₁, u₂} (F.obj (D.obj i)))
      f :
    ULift.{u₁, u₂} (F.obj (D.obj i)))
  ({
      down :=
        (ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (D.obj i)) :
            (a : (colimit (D.leftOp ⋙ yoneda)).obj (D.obj i)) → F.obj (D.obj i))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (colimit.ι (D.leftOp ⋙ yoneda) (op i)) (D.obj i)) :
                (a : unop (D.obj i) ⟶ unop (D.obj i)) → (colimit (D.leftOp ⋙ yoneda)).obj (D.obj i))
              (𝟙 (unop (D.obj i))) :
            (colimit (D.leftOp ⋙ yoneda)).obj (D.obj i)) } :
    ULift.{u₁, u₂} (F.obj (D.obj i)))
Tactic: dsimp [yonedaLemma]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Indization.Category (goal)
Goal:
C : Type u
inst : Category.{v, u} C
⊢ RepresentablyCoflat (C := C) Ind.yoneda
have refine : ∀ (X : Ind.{v, u} C), IsFiltered (CostructuredArrow Ind.yoneda X)
Tactic: refine ⟨fun X => ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Indization.Category (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X : Ind.{v, u} C
⊢ IsFiltered (CostructuredArrow Ind.yoneda X)
have suffices : IsFiltered (CostructuredArrow yoneda (obj (Ind.inclusion C) X))
Tactic: suffices IsFiltered (CostructuredArrow yoneda ((Ind.inclusion C).obj X)) from
    IsFiltered.of_equivalence
      ((CostructuredArrow.post Ind.yoneda (Ind.inclusion C) X).asEquivalence.trans
      (CostructuredArrow.mapNatIso Ind.yonedaCompInclusion)).symm
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Indization.Category (goal)
Goal:
C : Type u
inst : Category.{v, u} C
α : Type v
inst_1 : Finite α
inst_2 : HasColimitsOfShape.{v, v, v, u} (Discrete α) C
⊢ HasColimitsOfShape (Discrete α) (Ind.{v, u} C)
have refine : ∀ (F : Discrete α ⥤ Ind.{v, u} C), HasColimit F
Tactic: refine ⟨fun F => ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Indization.Category (goal)
Goal:
C : Type u
inst : Category.{v, u} C
α : Type v
inst_1 : Finite α
inst_2 : HasColimitsOfShape.{v, v, v, u} (Discrete α) C
F : Discrete α ⥤ Ind.{v, u} C
I : α → Type v := fun (s : α) ↦ (F.obj { as := s : Discrete α }).presentation.I
G : (s : α) → Functor.{v, v, v, u} (I s) C := fun (s : α) ↦ (F.obj { as := s }).presentation.F
⊢ comp (D := Functor.{v, v, v, u} ((i : α) → I i) C) (Discrete.functor fun (s : α) ↦ Pi.eval I s ⋙ G s)
      (obj (whiskeringRight ((i : α) → I i) C (Ind.{v, u} C)) Ind.yoneda ⋙ colim) ≅
    F
have refine : (s : Discrete α) →
  obj
      (comp (D := Functor.{v, v, v, u} ((i : α) → I i) C) (Discrete.functor fun (s : α) ↦ Pi.eval I s ⋙ G s)
        (obj (whiskeringRight ((i : α) → I i) C (Ind.{v, u} C)) Ind.yoneda ⋙ colim))
      s ≅
    F.obj s
Tactic: refine Discrete.natIso (fun s => ?_)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Indization.Category (goal)
Goal:
C : Type u
inst : Category.{v, u} C
α : Type v
inst_1 : Finite α
inst_2 : HasColimitsOfShape.{v, v, v, u} (Discrete α) C
F : Discrete α ⥤ Ind.{v, u} C
I : α → Type v := fun (s : α) ↦ (F.obj { as := s : Discrete α }).presentation.I
G : (s : α) → Functor.{v, v, v, u} (I s) C := fun (s : α) ↦ (F.obj { as := s }).presentation.F
s : Discrete α
⊢ obj
      (comp (D := Functor.{v, v, v, u} ((i : α) → I i) C) (Discrete.functor fun (s : α) ↦ Pi.eval I s ⋙ G s)
        (obj (whiskeringRight ((i : α) → I i) C (Ind.{v, u} C)) Ind.yoneda ⋙ colim))
      s ≅
    F.obj s
have refine : colimit (J := I s.as) (G s.as ⋙ Ind.yoneda) ≅ F.obj s
Tactic: refine (Functor.Final.colimitIso (Pi.eval I s.as) (G s.as ⋙ Ind.yoneda)) ≪≫ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Indization.Category (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasColimitsOfShape.{0, 0, v, u} WalkingParallelPair C
⊢ HasColimitsOfShape WalkingParallelPair (Ind.{v, u} C)
have refine : ∀ (F : WalkingParallelPair ⥤ Ind.{v, u} C), HasColimit F
Tactic: refine ⟨fun F => ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Indization.Category (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasColimitsOfShape.{0, 0, v, u} WalkingParallelPair C
F : WalkingParallelPair ⥤ Ind.{v, u} C
⊢ HasColimit F
have obtain : ∀
  (P :
    IndParallelPairPresentation (A := (F.obj WalkingParallelPair.zero).obj (P := IsIndObject)) (B :=
      (F.obj WalkingParallelPair.one).obj (P := IsIndObject))
      (map (Ind.inclusion C) (F.map WalkingParallelPairHom.left) :
        Quiver.Hom (V := Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)) (obj (Ind.inclusion C) (F.1 WalkingParallelPair.zero))
          (obj (Ind.inclusion C) (F.1 WalkingParallelPair.one)))
      (map (Ind.inclusion C) (F.map WalkingParallelPairHom.right))),
  HasColimit F
Tactic: obtain ⟨P⟩ := nonempty_indParallelPairPresentation (F.obj WalkingParallelPair.zero).2
    (F.obj WalkingParallelPair.one).2 (Ind.inclusion _ |>.map <| F.map WalkingParallelPairHom.left)
    (Ind.inclusion _ |>.map <| F.map WalkingParallelPairHom.right)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Indization.Category (goal)
Goal:
C : Type u
inst : Category.{v, u} C
A B : Ind.{v, u} C
f : A ⟶ B
⊢ ∃ (I : Type v) (x : SmallCategory I) (x_1 : IsFiltered I) (F : I ⥤ C) (G : I ⥤ C) (φ : F ⟶ G),
    Nonempty.{v + 1} (Arrow.mk f ≅ Arrow.mk (X := obj (Ind.lim I) F) (map (Ind.lim I) φ))
have obtain : ∀
  (P :
    IndParallelPairPresentation (A := A.obj (P := IsIndObject)) (B := B.obj (P := IsIndObject))
      (map (Ind.inclusion C) f : obj (Ind.inclusion C) A ⟶ obj (Ind.inclusion C) B) (map (Ind.inclusion C) f)),
  ∃ (I : Type v) (x : SmallCategory I) (x_1 : IsFiltered I) (F : I ⥤ C) (G : I ⥤ C) (φ : F ⟶ G),
    Nonempty.{v + 1} (Arrow.mk f ≅ Arrow.mk (X := obj (Ind.lim I) F) (map (Ind.lim I) φ))
Tactic: obtain ⟨P⟩ := nonempty_indParallelPairPresentation A.2 B.2
    (Ind.inclusion _ |>.map f) (Ind.inclusion _ |>.map f)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Indization.Category (goal)
Goal:
C : Type u
inst : Category.{v, u} C
A B : Ind.{v, u} C
f : A ⟶ B
P :
  IndParallelPairPresentation (A := A.obj (P := IsIndObject)) (B := B.obj (P := IsIndObject))
    (map (Ind.inclusion C) f : obj (Ind.inclusion C) A ⟶ obj (Ind.inclusion C) B) (map (Ind.inclusion C) f)
⊢ ∃ (I : Type v) (x : SmallCategory I) (x_1 : IsFiltered I) (F : I ⥤ C) (G : I ⥤ C) (φ : F ⟶ G),
    Nonempty.{v + 1} (Arrow.mk f ≅ Arrow.mk (X := obj (Ind.lim I) F) (map (Ind.lim I) φ))
have refine_1 : (Arrow.mk f).left ≅ (Arrow.mk (X := obj (Ind.lim P.I) P.F₁) (map (Ind.lim P.I) P.φ)).left
Tactic: refine ⟨P.I, inferInstance, inferInstance, P.F₁, P.F₂, P.φ, ⟨Arrow.isoMk ?_ ?_ ?_⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Indization.Category (goal)
Goal:
C : Type u
inst : Category.{v, u} C
A B : Ind.{v, u} C
f : A ⟶ B
P :
  IndParallelPairPresentation (A := A.obj (P := IsIndObject)) (B := B.obj (P := IsIndObject))
    (map (Ind.inclusion C) f : obj (Ind.inclusion C) A ⟶ obj (Ind.inclusion C) B) (map (Ind.inclusion C) f)
refine_1 : (Arrow.mk f).left ≅ (Arrow.mk (X := obj (Ind.lim P.I) P.F₁) (map (Ind.lim P.I) P.φ)).left
⊢ ∃ (I : Type v) (x : SmallCategory I) (x_1 : IsFiltered I) (F : I ⥤ C) (G : I ⥤ C) (φ : F ⟶ G),
    Nonempty.{v + 1} (Arrow.mk f ≅ Arrow.mk (X := obj (Ind.lim I) F) (map (Ind.lim I) φ))
have refine_2 : (Arrow.mk f).right ≅ (Arrow.mk (X := obj (Ind.lim P.I) P.F₁) (map (Ind.lim P.I) P.φ)).right
Tactic: refine ⟨P.I, inferInstance, inferInstance, P.F₁, P.F₂, P.φ, ⟨Arrow.isoMk ?_ ?_ ?_⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Indization.Category (goal)
Goal:
C : Type u
inst : Category.{v, u} C
A B : Ind.{v, u} C
f : A ⟶ B
P :
  IndParallelPairPresentation (A := A.obj (P := IsIndObject)) (B := B.obj (P := IsIndObject))
    (map (Ind.inclusion C) f : obj (Ind.inclusion C) A ⟶ obj (Ind.inclusion C) B) (map (Ind.inclusion C) f)
refine_1 : (Arrow.mk f).left ≅ (Arrow.mk (X := obj (Ind.lim P.I) P.F₁) (map (Ind.lim P.I) P.φ)).left
refine_2 : (Arrow.mk f).right ≅ (Arrow.mk (X := obj (Ind.lim P.I) P.F₁) (map (Ind.lim P.I) P.φ)).right
⊢ ∃ (I : Type v) (x : SmallCategory I) (x_1 : IsFiltered I) (F : I ⥤ C) (G : I ⥤ C) (φ : F ⟶ G),
    Nonempty.{v + 1} (Arrow.mk f ≅ Arrow.mk (X := obj (Ind.lim I) F) (map (Ind.lim I) φ))
have refine_3 : (P.parallelPairIsoParallelPairCompIndYoneda.app WalkingParallelPair.zero).hom ≫
    (Arrow.mk (X := obj (Ind.lim P.I) P.F₁) (map (Ind.lim P.I) P.φ)).hom =
  (Arrow.mk f).hom ≫ (P.parallelPairIsoParallelPairCompIndYoneda.app WalkingParallelPair.one).hom
Tactic: refine ⟨P.I, inferInstance, inferInstance, P.F₁, P.F₂, P.φ, ⟨Arrow.isoMk ?_ ?_ ?_⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Indization.Category (goal)
Goal:
C_1 : Type u
inst : Category.{v, u} C_1
C : Type u
inst_1 : SmallCategory C
inst_2 : HasFiniteColimits C
⊢ Eq (α := ObjectProperty (Cᵒᵖ ⥤ Type u)) IsIndObject (leftExactFunctor Cᵒᵖ (Type u))
have h : ∀ (x : Cᵒᵖ ⥤ Type u), IsIndObject x ↔ leftExactFunctor Cᵒᵖ (Type u) x
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Indization.Equalizers (goal)
Goal:
C : Type u
inst : Category.{v, u} C
I : Type v
inst_1 : SmallCategory I
inst_2 : IsFiltered I
J : Type
inst_3 : SmallCategory J
inst_4 : FinCategory J
F : J ⥤ I ⥤ C
hF : ∀ (i : I), IsIndObject (limit (F.flip.obj i ⋙ yoneda))
G : J ⥤ I ⥤ Functor.{v, v, u, v + 1} Cᵒᵖ (Type v) :=
  F ⋙ Functor.obj (Functor.whiskeringRight I C (Functor.{v, v, u, v + 1} Cᵒᵖ (Type v))) yoneda
⊢ IsIndObject
    (limit (F ⋙ Functor.obj (Functor.whiskeringRight I C (Functor.{v, v, u, v + 1} Cᵒᵖ (Type v))) yoneda ⋙ colim))
have apply : IsIndObject (limit (colimit G.flip))
Tactic: apply IsIndObject.map (HasLimit.isoOfNatIso (colimitFlipIsoCompColim G)).hom
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Indization.Equalizers (goal)
Goal:
C : Type u
inst : Category.{v, u} C
I : Type v
inst_1 : SmallCategory I
inst_2 : IsFiltered I
J : Type
inst_3 : SmallCategory J
inst_4 : FinCategory J
F : J ⥤ I ⥤ C
hF : ∀ (i : I), IsIndObject (limit (F.flip.obj i ⋙ yoneda))
G : J ⥤ I ⥤ Functor.{v, v, u, v + 1} Cᵒᵖ (Type v) :=
  F ⋙ Functor.obj (Functor.whiskeringRight I C (Functor.{v, v, u, v + 1} Cᵒᵖ (Type v))) yoneda
⊢ IsIndObject (limit (colimit G.flip))
have apply : IsIndObject (colimit (limit G))
Tactic: apply IsIndObject.map (colimitLimitIso G).hom
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Indization.Equalizers (goal)
Goal:
C : Type u
inst : Category.{v, u} C
I : Type v
inst_1 : SmallCategory I
inst_2 : IsFiltered I
J : Type
inst_3 : SmallCategory J
inst_4 : FinCategory J
F : J ⥤ I ⥤ C
hF : ∀ (i : I), IsIndObject (limit (F.flip.obj i ⋙ yoneda))
G : J ⥤ I ⥤ Functor.{v, v, u, v + 1} Cᵒᵖ (Type v) :=
  F ⋙ Functor.obj (Functor.whiskeringRight I C (Functor.{v, v, u, v + 1} Cᵒᵖ (Type v))) yoneda
⊢ IsIndObject (colimit (limit G))
have hF₁ : ∀ (i : I), IsIndObject ((limit G).obj i)
Tactic: apply isIndObject_colimit
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Indization.Equalizers (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasEqualizers.{v, u} C
F : WalkingParallelPair ⥤ Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)
inst_2 : HasLimit F
h : ∀ (j : WalkingParallelPair), IsIndObject (F.obj j)
⊢ IsIndObject (limit F)
have obtain : ∀ (P : IndParallelPairPresentation (F.map WalkingParallelPairHom.left) (F.map WalkingParallelPairHom.right)),
  IsIndObject (limit F)
Tactic: obtain ⟨P⟩ := nonempty_indParallelPairPresentation (h WalkingParallelPair.zero)
      (h WalkingParallelPair.one) (F.map WalkingParallelPairHom.left)
      (F.map WalkingParallelPairHom.right)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Indization.FilteredColimits (goal)
Goal:
C : Type u
inst : Category.{v, u} C
I : Type v
inst_1 : SmallCategory I
F : I ⥤ Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)
J : Type v
inst_2 : SmallCategory J
inst_3 : FinCategory J
G : J ⥤ CostructuredArrow yoneda (colimit F)
K : Type v
inst_4 : SmallCategory K
H : K ⥤ Over (colimit F)
inst_5 : IsFiltered K
h : Nonempty (limit ((G.op ⋙ Functor.op (CostructuredArrow.toOver yoneda (colimit F))) ⋙ obj yoneda (colimit H)))
⊢ ∃ (k : K), Nonempty (limit ((G.op ⋙ Functor.op (CostructuredArrow.toOver yoneda (colimit F))) ⋙ obj yoneda (H.obj k)))
have obtain : ∀ (t : limit ((G.op ⋙ Functor.op (CostructuredArrow.toOver yoneda (colimit F))) ⋙ obj yoneda (colimit H))),
  ∃ (k : K), Nonempty (limit ((G.op ⋙ Functor.op (CostructuredArrow.toOver yoneda (colimit F))) ⋙ obj yoneda (H.obj k)))
Tactic: obtain ⟨t⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Indization.FilteredColimits (goal)
Goal:
C : Type u
inst : Category.{v, u} C
I : Type v
inst_1 : SmallCategory I
F : I ⥤ Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)
J : Type v
inst_2 : SmallCategory J
inst_3 : FinCategory J
G : J ⥤ CostructuredArrow yoneda (colimit F)
K : Type v
inst_4 : SmallCategory K
H : K ⥤ Over (colimit F)
inst_5 : IsFiltered K
c : Cocone H
hc : IsColimit c
T : Over (colimit F)
hT : c.pt ≅ T
h : Nonempty (limit ((G.op ⋙ Functor.op (CostructuredArrow.toOver yoneda (colimit F))) ⋙ obj yoneda T))
⊢ ∃ (k : K), Nonempty (limit ((G.op ⋙ Functor.op (CostructuredArrow.toOver yoneda (colimit F))) ⋙ obj yoneda (H.obj k)))
have refine : Nonempty (limit ((G.op ⋙ Functor.op (CostructuredArrow.toOver yoneda (colimit F))) ⋙ obj yoneda (colimit H)))
Tactic: refine exists_nonempty_limit_obj_of_colimit F G H ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Indization.FilteredColimits (goal)
Goal:
C : Type u
inst : Category.{v, u} C
I : Type v
inst_1 : SmallCategory I
F : I ⥤ Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)
J : Type v
inst_2 : SmallCategory J
inst_3 : FinCategory J
G : J ⥤ CostructuredArrow yoneda (colimit F)
K : Type v
inst_4 : SmallCategory K
H : K ⥤ Over (colimit F)
inst_5 : IsFiltered K
c : Cocone H
hc : IsColimit c
T : Over (colimit F)
hT : c.pt ≅ T
h : Nonempty (limit ((G.op ⋙ Functor.op (CostructuredArrow.toOver yoneda (colimit F))) ⋙ obj yoneda T))
⊢ Nonempty (limit ((G.op ⋙ Functor.op (CostructuredArrow.toOver yoneda (colimit F))) ⋙ obj yoneda (colimit H)))
have suffices : T ≅ colimit H
Tactic: suffices T ≅ colimit H from Nonempty.map (lim.map (whiskerLeft 𝒢 (yoneda.map this.hom))) h