awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
inst_2 : IsFiltered I
F : I ⥤ Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)
hF : ∀ (i : I), IsIndObject (F.obj i)
this : IsFiltered (CostructuredArrow yoneda (colimit F))
s : (i : I) → Set (CostructuredArrow yoneda (F.obj i))
hs : ∀ (i : I), Small.{v, max u v} (↑(s i) : Type (max u v))
j : (i : I) → (i_1 : CostructuredArrow yoneda (F.obj i)) → CostructuredArrow yoneda (F.obj i)
hjs : ∀ (i : I) (i_1 : CostructuredArrow yoneda (F.obj i)), j i i_1 ∈ s i
hj : ∀ (i : I) (i_1 : CostructuredArrow yoneda (F.obj i)), Nonempty.{v + 1} (i_1 ⟶ j i i_1)
A : CostructuredArrow yoneda (colimit F)
i : I
y : (F.obj i).obj (Opposite.op A.left)
hy :
  Eq.{v + 1} (α := (colimit F).obj (Opposite.op A.left))
    ((yonedaEquiv : (a : yoneda.obj A.left ⟶ colimit F) → (colimit F).obj (Opposite.op A.left)) A.hom :
      (colimit F).obj (Opposite.op A.left))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (colimit.ι F i) (Opposite.op A.left)) :
          (a : (fun (X : Type v) ↦ X) ((F.obj i).obj (Opposite.op A.left))) →
            (fun (X : Type v) ↦ X) ((colimit F).obj (Opposite.op A.left)))
        y :
      (fun (X : Type v) ↦ X) ((colimit F).obj (Opposite.op A.left)))
y' : CostructuredArrow yoneda (F.obj i) :=
  CostructuredArrow.mk (Y := A.left)
    ((Equiv.symm yonedaEquiv : (a : (F.obj i).obj (Opposite.op A.left)) → yoneda.obj A.left ⟶ F.obj i) y)
x : y' ⟶ j i y'
⊢ A ⟶ obj (CostructuredArrow.map (colimit.ι F i)) (j i y')
have refine_2 : A ⟶ obj (CostructuredArrow.map (colimit.ι F i)) y'
Tactic: refine ?_ ≫ (map (colimit.ι F i)).map x
-- 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
inst_2 : IsFiltered I
F : I ⥤ Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)
hF : ∀ (i : I), IsIndObject (F.obj i)
this : IsFiltered (CostructuredArrow yoneda (colimit F))
s : (i : I) → Set (CostructuredArrow yoneda (F.obj i))
hs : ∀ (i : I), Small.{v, max u v} (↑(s i) : Type (max u v))
j : (i : I) → (i_1 : CostructuredArrow yoneda (F.obj i)) → CostructuredArrow yoneda (F.obj i)
hjs : ∀ (i : I) (i_1 : CostructuredArrow yoneda (F.obj i)), j i i_1 ∈ s i
hj : ∀ (i : I) (i_1 : CostructuredArrow yoneda (F.obj i)), Nonempty.{v + 1} (i_1 ⟶ j i i_1)
A : CostructuredArrow yoneda (colimit F)
i : I
y : (F.obj i).obj (Opposite.op A.left)
hy :
  Eq.{v + 1} (α := (colimit F).obj (Opposite.op A.left))
    ((yonedaEquiv : (a : yoneda.obj A.left ⟶ colimit F) → (colimit F).obj (Opposite.op A.left)) A.hom :
      (colimit F).obj (Opposite.op A.left))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (colimit.ι F i) (Opposite.op A.left)) :
          (a : (fun (X : Type v) ↦ X) ((F.obj i).obj (Opposite.op A.left))) →
            (fun (X : Type v) ↦ X) ((colimit F).obj (Opposite.op A.left)))
        y :
      (fun (X : Type v) ↦ X) ((colimit F).obj (Opposite.op A.left)))
y' : CostructuredArrow yoneda (F.obj i) :=
  CostructuredArrow.mk (Y := A.left)
    ((Equiv.symm yonedaEquiv : (a : (F.obj i).obj (Opposite.op A.left)) → yoneda.obj A.left ⟶ F.obj i) y)
x : y' ⟶ j i y'
⊢ A ⟶ obj (CostructuredArrow.map (colimit.ι F i)) y'
have refine_2 : Eq.{v + 1} (α := (colimit F).obj (Opposite.op A.left))
  ((yonedaEquiv : (a : yoneda.obj A.left ⟶ colimit F) → (colimit F).obj (Opposite.op A.left))
      (Functor.map yoneda (𝟙 A.left) ≫ CostructuredArrow.hom (obj (CostructuredArrow.map (colimit.ι F i)) y')) :
    (colimit F).obj (Opposite.op A.left))
  ((yonedaEquiv : (a : yoneda.obj A.left ⟶ colimit F) → (colimit F).obj (Opposite.op A.left)) A.hom :
    (colimit F).obj (Opposite.op A.left))
Tactic: refine homMk (𝟙 A.left) (yonedaEquiv.injective ?_)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Indization.IndObject (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
A : Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)
inst_1 : IsFiltered (CostructuredArrow yoneda A)
inst_2 : FinallySmall (CostructuredArrow yoneda A)
⊢ IsIndObject A
have h₁ : Functor.Final (C := FinalModel (CostructuredArrow yoneda A))
  (Functor.comp (D :=
    IsFiltered.SmallFilteredIntermediate (C := CostructuredArrow yoneda A) (D :=
      FinalModel (CostructuredArrow yoneda A)) (fromFinalModel (CostructuredArrow yoneda A)))
    (factoring (fromFinalModel (CostructuredArrow yoneda A))) (inclusion (fromFinalModel (CostructuredArrow yoneda A))))
Tactic: have h₁ : (factoring (fromFinalModel (CostructuredArrow yoneda A)) ⋙
      inclusion (fromFinalModel (CostructuredArrow yoneda A))).Final := Functor.final_of_natIso
    (factoringCompInclusion (fromFinalModel <| CostructuredArrow yoneda A)).symm
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Indization.IndObject (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
A : Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)
inst_1 : IsFiltered (CostructuredArrow yoneda A)
inst_2 : FinallySmall (CostructuredArrow yoneda A)
h₁ :
  Functor.Final (C := FinalModel (CostructuredArrow yoneda A))
    (Functor.comp (D :=
      IsFiltered.SmallFilteredIntermediate (C := CostructuredArrow yoneda A) (D :=
        FinalModel (CostructuredArrow yoneda A)) (fromFinalModel (CostructuredArrow yoneda A)))
      (factoring (fromFinalModel (CostructuredArrow yoneda A)))
      (inclusion (fromFinalModel (CostructuredArrow yoneda A))))
⊢ IsIndObject A
have h₂ : Functor.Final (C :=
  IsFiltered.SmallFilteredIntermediate (C := CostructuredArrow yoneda A) (D := FinalModel (CostructuredArrow yoneda A))
    (fromFinalModel (CostructuredArrow yoneda A)))
  (inclusion (fromFinalModel (CostructuredArrow yoneda A)))
Tactic: have h₂ : Functor.Final (inclusion (fromFinalModel (CostructuredArrow yoneda A))) :=
    Functor.final_of_comp_full_faithful' (factoring _) (inclusion _)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Indization.IndObject (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
A : Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)
inst_1 : IsFiltered (CostructuredArrow yoneda A)
inst_2 : FinallySmall (CostructuredArrow yoneda A)
h₁ :
  Functor.Final (C := FinalModel (CostructuredArrow yoneda A))
    (Functor.comp (D :=
      IsFiltered.SmallFilteredIntermediate (C := CostructuredArrow yoneda A) (D :=
        FinalModel (CostructuredArrow yoneda A)) (fromFinalModel (CostructuredArrow yoneda A)))
      (factoring (fromFinalModel (CostructuredArrow yoneda A)))
      (inclusion (fromFinalModel (CostructuredArrow yoneda A))))
h₂ :
  Functor.Final (C :=
    IsFiltered.SmallFilteredIntermediate (C := CostructuredArrow yoneda A) (D :=
      FinalModel (CostructuredArrow yoneda A)) (fromFinalModel (CostructuredArrow yoneda A)))
    (inclusion (fromFinalModel (CostructuredArrow yoneda A)))
c : Cocone (J :=
  IsFiltered.SmallFilteredIntermediate (C := CostructuredArrow yoneda A) (D := FinalModel (CostructuredArrow yoneda A))
    (fromFinalModel (CostructuredArrow yoneda A)))
  (inclusion (fromFinalModel (CostructuredArrow yoneda A)) ⋙ CostructuredArrow.proj yoneda A ⋙ yoneda) :=
  Cocone.whisker (inclusion (fromFinalModel (CostructuredArrow yoneda A))) (Presheaf.tautologicalCocone A)
hc : IsColimit c :=
  (Equiv.symm
        (Functor.Final.isColimitWhiskerEquiv (inclusion (fromFinalModel (CostructuredArrow yoneda A)))
          (Presheaf.tautologicalCocone A)) :
      (a : IsColimit (Presheaf.tautologicalCocone A)) →
        IsColimit
          (Cocone.whisker (inclusion (fromFinalModel (CostructuredArrow yoneda A))) (Presheaf.tautologicalCocone A)))
    (Presheaf.isColimitTautologicalCocone A)
⊢ IsIndObject A
have hq : Nonempty.{v + 1} (FinalModel (CostructuredArrow yoneda A))
Tactic: have hq : Nonempty (FinalModel (CostructuredArrow yoneda A)) := Nonempty.map
    (Functor.Final.lift (fromFinalModel (CostructuredArrow yoneda A))) IsFiltered.nonempty
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Indization.IndObject (goal)
Goal:
C : Type u
inst : SmallCategory C
inst_1 : HasFiniteColimits C
A : Cᵒᵖ ⥤ Type u
⊢ IsFiltered.{u, u} (CostructuredArrow yoneda A) ∧ FinallySmall.{u, u, u} (CostructuredArrow yoneda A) ↔
    PreservesFiniteLimits A
have refine_1 : IsFiltered.{u, u} (CostructuredArrow yoneda A) ∧ FinallySmall.{u, u, u} (CostructuredArrow yoneda A) →
  ∀ (h₁ : IsFiltered.{u, u} (CostructuredArrow yoneda A)) (h₂ : FinallySmall.{u, u, u} (CostructuredArrow yoneda A)),
    PreservesFiniteLimits A
Tactic: refine ⟨fun ⟨h₁, h₂⟩ => ?_, fun h => ⟨?_, ?_⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Indization.IndObject (goal)
Goal:
C : Type u
inst : SmallCategory C
inst_1 : HasFiniteColimits C
A : Cᵒᵖ ⥤ Type u
refine_1 :
  IsFiltered.{u, u} (CostructuredArrow yoneda A) ∧ FinallySmall.{u, u, u} (CostructuredArrow yoneda A) →
    ∀ (h₁ : IsFiltered.{u, u} (CostructuredArrow yoneda A)) (h₂ : FinallySmall.{u, u, u} (CostructuredArrow yoneda A)),
      PreservesFiniteLimits A
⊢ IsFiltered.{u, u} (CostructuredArrow yoneda A) ∧ FinallySmall.{u, u, u} (CostructuredArrow yoneda A) ↔
    PreservesFiniteLimits A
have refine_2 : ∀ (h : PreservesFiniteLimits A), IsFiltered.{u, u} (CostructuredArrow yoneda A)
Tactic: refine ⟨fun ⟨h₁, h₂⟩ => ?_, fun h => ⟨?_, ?_⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Indization.IndObject (goal)
Goal:
C : Type u
inst : SmallCategory C
inst_1 : HasFiniteColimits C
A : Cᵒᵖ ⥤ Type u
refine_1 :
  IsFiltered.{u, u} (CostructuredArrow yoneda A) ∧ FinallySmall.{u, u, u} (CostructuredArrow yoneda A) →
    ∀ (h₁ : IsFiltered.{u, u} (CostructuredArrow yoneda A)) (h₂ : FinallySmall.{u, u, u} (CostructuredArrow yoneda A)),
      PreservesFiniteLimits A
refine_2 : ∀ (h : PreservesFiniteLimits A), IsFiltered.{u, u} (CostructuredArrow yoneda A)
⊢ IsFiltered.{u, u} (CostructuredArrow yoneda A) ∧ FinallySmall.{u, u, u} (CostructuredArrow yoneda A) ↔
    PreservesFiniteLimits A
have refine_3 : ∀ (h : PreservesFiniteLimits A), FinallySmall.{u, u, u} (CostructuredArrow yoneda A)
Tactic: refine ⟨fun ⟨h₁, h₂⟩ => ?_, fun h => ⟨?_, ?_⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Indization.IndObject (hypothesis)
Goal:
C : Type u
inst : SmallCategory C
inst_1 : HasFiniteColimits C
A : Cᵒᵖ ⥤ Type u
h : PreservesFiniteLimits A
⊢ FinallySmall.{u, u, u} (CostructuredArrow yoneda A)
have this : EssentiallySmall.{u, u, u} (CostructuredArrow yoneda A)
Tactic: have := essentiallySmallSelf (CostructuredArrow yoneda A)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Indization.LocallySmall (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
I : Type u₁
inst_1 : Category.{v₁, u₁} I
inst_2 : HasColimitsOfShape.{v₁, u₁, v, v + 1} I (Type v)
inst_3 : HasLimitsOfShape.{v₁, u₁, v, v + 1} Iᵒᵖ (Type v)
inst_4 : HasLimitsOfShape Iᵒᵖ (Type (max u v))
F : Functor.{v₁, v, u₁, u} I C
G : Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)
η : colimit (F ⋙ yoneda) ⟶ G
i : Iᵒᵖ
⊢ Eq (α := G.obj (op (F.obj (unop i))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (limit.π (F.op ⋙ G) i) :
          (a : limit (F.op ⋙ G)) → G.obj (op (F.obj (unop i))))
        (ULift.down.{u, v}
          (((ConcreteCategory.hom (FC := TypeCat.Fun) (Iso.inv (preservesLimitIso uliftFunctor.{u, v} (F.op ⋙ G))) :
                TypeCat.Fun (limit ((F.op ⋙ G) ⋙ uliftFunctor.{u, v})) (ULift.{u, v} (limit (F.op ⋙ G)))) :
              (a : limit ((F.op ⋙ G) ⋙ uliftFunctor.{u, v})) → ULift.{u, v} (limit (F.op ⋙ G)))
            ((ConcreteCategory.hom (FC := TypeCat.Fun)
                  (Iso.hom (HasLimit.isoOfNatIso (F.op.associator G uliftFunctor.{u, v}).symm)) :
                (a : limit (F.op ⋙ G ⋙ uliftFunctor.{u, v})) → limit ((F.op ⋙ G) ⋙ uliftFunctor.{u, v}))
              (((ConcreteCategory.hom (FC := TypeCat.Fun) (Iso.hom (colimitYonedaHomIsoLimitOp F G)) :
                    TypeCat.Fun (colimit (F ⋙ yoneda) ⟶ G) (limit (F.op ⋙ G ⋙ uliftFunctor.{u, v}))) :
                  (a : colimit (F ⋙ yoneda) ⟶ G) → limit (F.op ⋙ G ⋙ uliftFunctor.{u, v}))
                η)))) :
      G.obj (op (F.obj (unop i))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (η.app (op (F.obj (unop i)))) :
          (a : (colimit (F ⋙ yoneda)).obj (op (F.obj (unop i)))) → G.obj (op (F.obj (unop i))))
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
                (NatTrans.app (colimit.ι (F ⋙ yoneda) (unop i)) (op (F.obj (unop i)))) :
              (a : F.obj (unop i) ⟶ F.obj (unop i)) → (colimit (F ⋙ yoneda)).obj (op (F.obj (unop i))))
            (𝟙 (F.obj (unop i))) :
          (colimit (F ⋙ yoneda)).obj (op (F.obj (unop i)))) :
      G.obj (op (F.obj (unop i))))
have this : ∀ (a : limit ((F.op ⋙ G) ⋙ uliftFunctor.{u, v})),
  Eq.{v + 1} (α := (F.op ⋙ G).obj i)
    (ULift.down.{u, v}
      (((ConcreteCategory.hom (FC := TypeCat.Fun)
              (CategoryStruct.comp (Y := uliftFunctor.{u, v}.obj (limit (F.op ⋙ G)))
                (Iso.inv (preservesLimitIso uliftFunctor.{u, v} (F.op ⋙ G)))
                (uliftFunctor.{u, v}.map (limit.π (F.op ⋙ G) i))) :
            TypeCat.Fun (limit ((F.op ⋙ G) ⋙ uliftFunctor.{u, v})) (uliftFunctor.{u, v}.obj ((F.op ⋙ G).obj i))) :
          (a : limit ((F.op ⋙ G) ⋙ uliftFunctor.{u, v})) → uliftFunctor.{u, v}.obj ((F.op ⋙ G).obj i))
        a))
    (ULift.down.{u, v}
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (limit.π ((F.op ⋙ G) ⋙ uliftFunctor.{u, v}) i) :
          (a : limit ((F.op ⋙ G) ⋙ uliftFunctor.{u, v})) → uliftFunctor.{u, v}.obj ((F.op ⋙ G).obj i))
        a))
Tactic: have (a : limit ((F.op ⋙ G) ⋙ uliftFunctor.{u, v})) := congrArg ULift.down
    (ConcreteCategory.congr_hom (preservesLimitIso_inv_π uliftFunctor.{u, v} (F.op ⋙ G) i) a)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Indization.LocallySmall (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : ObjectProperty.FullSubcategory (C := Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)) IsIndObject
⊢ Small.{v, max u v} (X ⟶ Y)
have obtain : ∀ (P : IndObjectPresentation (X.obj (P := IsIndObject))), Small.{v, max u v} (X ⟶ Y)
Tactic: obtain ⟨⟨P⟩⟩ := X.2
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Indization.LocallySmall (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : ObjectProperty.FullSubcategory (C := Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)) IsIndObject
P : IndObjectPresentation (X.obj (P := IsIndObject))
⊢ Small.{v, max u v} (X ⟶ Y)
have obtain : ∀ (Q : IndObjectPresentation (Y.obj (P := IsIndObject))), Small.{v, max u v} (X ⟶ Y)
Tactic: obtain ⟨⟨Q⟩⟩ := Y.2
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Indization.ParallelPair (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A B : Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)
f g : A ⟶ B
P₁ : IndObjectPresentation A
P₂ : IndObjectPresentation B
x x_1 : K f g P₁ P₂
h : x ⟶ x_1
⊢ (F₁ f g P₁ P₂).map h ≫ x_1.hom.1.left = x.hom.1.left ≫ (F₂ f g P₁ P₂).map h
have this : ((P₁.toCostructuredArrow ⋙ CostructuredArrow.map f).prod' (P₁.toCostructuredArrow ⋙ CostructuredArrow.map g)).map
      h.left ≫
    x_1.hom =
  x.hom ≫ (P₂.toCostructuredArrow.prod' P₂.toCostructuredArrow).map h.right
Tactic: have := h.w
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Indization.ParallelPair (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A B : Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)
f g : A ⟶ B
P₁ : IndObjectPresentation A
P₂ : IndObjectPresentation B
x x_1 : K f g P₁ P₂
h : x ⟶ x_1
this :
  ((P₁.toCostructuredArrow ⋙ CostructuredArrow.map f).prod' (P₁.toCostructuredArrow ⋙ CostructuredArrow.map g)).map
        h.left ≫
      x_1.hom =
    x.hom ≫ (P₂.toCostructuredArrow.prod' P₂.toCostructuredArrow).map h.right
⊢ (F₁ f g P₁ P₂).map h ≫ x_1.hom.1.left = x.hom.1.left ≫ (F₂ f g P₁ P₂).map h
have this₁ : P₁.F.map h.left ≫ x_1.hom.1.left =
    (x.hom ≫ Prod.mkHom (P₂.toCostructuredArrow.map h.right) (P₂.toCostructuredArrow.map h.right)).1.left ∧
  P₁.F.map h.left ≫ x_1.hom.2.left =
    (x.hom ≫ Prod.mkHom (P₂.toCostructuredArrow.map h.right) (P₂.toCostructuredArrow.map h.right)).2.left
Tactic: simp only [prod'_obj, comp_obj, prod'_map, Functor.comp_map, prod_comp, Prod.hom_ext_iff,
      CostructuredArrow.hom_eq_iff, CostructuredArrow.map_obj_left,
      IndObjectPresentation.toCostructuredArrow_obj_left, CostructuredArrow.comp_left,
      CostructuredArrow.map_map_left, IndObjectPresentation.toCostructuredArrow_map_left] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Indization.ParallelPair (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A B : Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)
f g : A ⟶ B
P₁ : IndObjectPresentation A
P₂ : IndObjectPresentation B
⊢ f = (isColimit₁ f g P₁ P₂).map { pt := B, ι := ι₂ f g P₁ P₂ } (whiskerRight (ϕ f g P₁ P₂) yoneda)
have refine : ∀ (i : K f g P₁ P₂),
  { pt := A, ι := ι₁ f g P₁ P₂ : Cocone (F₁ f g P₁ P₂ ⋙ yoneda) }.ι.app i ≫ f =
    { pt := A, ι := ι₁ f g P₁ P₂ : Cocone (F₁ f g P₁ P₂ ⋙ yoneda) }.ι.app i ≫
      (isColimit₁ f g P₁ P₂).map { pt := B, ι := ι₂ f g P₁ P₂ } (whiskerRight (ϕ f g P₁ P₂) yoneda)
Tactic: refine (isColimit₁ f g P₁ P₂).hom_ext (fun i => ?_)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Indization.ParallelPair (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A B : Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)
f g : A ⟶ B
P₁ : IndObjectPresentation A
P₂ : IndObjectPresentation B
i : K f g P₁ P₂
⊢ { pt := A, ι := ι₁ f g P₁ P₂ : Cocone (F₁ f g P₁ P₂ ⋙ yoneda) }.ι.app i ≫ f =
    { pt := A, ι := ι₁ f g P₁ P₂ : Cocone (F₁ f g P₁ P₂ ⋙ yoneda) }.ι.app i ≫
      (isColimit₁ f g P₁ P₂).map { pt := B, ι := ι₂ f g P₁ P₂ } (whiskerRight (ϕ f g P₁ P₂) yoneda)
have rw : { pt := A, ι := ι₁ f g P₁ P₂ : Cocone (F₁ f g P₁ P₂ ⋙ yoneda) }.ι.app i ≫ f =
  (whiskerRight (ϕ f g P₁ P₂) yoneda).app i ≫ { pt := B, ι := ι₂ f g P₁ P₂ }.ι.app i
Tactic: rw [IsColimit.ι_map]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Indization.ParallelPair (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A B : Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)
f g : A ⟶ B
P₁ : IndObjectPresentation A
P₂ : IndObjectPresentation B
x x_1 : K f g P₁ P₂
h : x ⟶ x_1
⊢ (F₁ f g P₁ P₂).map h ≫ x_1.hom.2.left = x.hom.2.left ≫ (F₂ f g P₁ P₂).map h
have this : ((P₁.toCostructuredArrow ⋙ CostructuredArrow.map f).prod' (P₁.toCostructuredArrow ⋙ CostructuredArrow.map g)).map
      h.left ≫
    x_1.hom =
  x.hom ≫ (P₂.toCostructuredArrow.prod' P₂.toCostructuredArrow).map h.right
Tactic: have := h.w
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Indization.ParallelPair (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A B : Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)
f g : A ⟶ B
P₁ : IndObjectPresentation A
P₂ : IndObjectPresentation B
x x_1 : K f g P₁ P₂
h : x ⟶ x_1
this :
  ((P₁.toCostructuredArrow ⋙ CostructuredArrow.map f).prod' (P₁.toCostructuredArrow ⋙ CostructuredArrow.map g)).map
        h.left ≫
      x_1.hom =
    x.hom ≫ (P₂.toCostructuredArrow.prod' P₂.toCostructuredArrow).map h.right
⊢ (F₁ f g P₁ P₂).map h ≫ x_1.hom.2.left = x.hom.2.left ≫ (F₂ f g P₁ P₂).map h
have this₁ : P₁.F.map h.left ≫ x_1.hom.1.left =
    (x.hom ≫ Prod.mkHom (P₂.toCostructuredArrow.map h.right) (P₂.toCostructuredArrow.map h.right)).1.left ∧
  P₁.F.map h.left ≫ x_1.hom.2.left =
    (x.hom ≫ Prod.mkHom (P₂.toCostructuredArrow.map h.right) (P₂.toCostructuredArrow.map h.right)).2.left
Tactic: simp only [prod'_obj, comp_obj, prod'_map, Functor.comp_map, prod_comp, Prod.hom_ext_iff,
      CostructuredArrow.hom_eq_iff, CostructuredArrow.map_obj_left,
      IndObjectPresentation.toCostructuredArrow_obj_left, CostructuredArrow.comp_left,
      CostructuredArrow.map_map_left, IndObjectPresentation.toCostructuredArrow_map_left] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Indization.ParallelPair (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A B : Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)
f g : A ⟶ B
P₁ : IndObjectPresentation A
P₂ : IndObjectPresentation B
⊢ g = (isColimit₁ f g P₁ P₂).map { pt := B, ι := ι₂ f g P₁ P₂ } (whiskerRight (ψ f g P₁ P₂) yoneda)
have refine : ∀ (i : K f g P₁ P₂),
  { pt := A, ι := ι₁ f g P₁ P₂ : Cocone (F₁ f g P₁ P₂ ⋙ yoneda) }.ι.app i ≫ g =
    { pt := A, ι := ι₁ f g P₁ P₂ : Cocone (F₁ f g P₁ P₂ ⋙ yoneda) }.ι.app i ≫
      (isColimit₁ f g P₁ P₂).map { pt := B, ι := ι₂ f g P₁ P₂ } (whiskerRight (ψ f g P₁ P₂) yoneda)
Tactic: refine (isColimit₁ f g P₁ P₂).hom_ext (fun i => ?_)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Indization.ParallelPair (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A B : Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)
f g : A ⟶ B
P₁ : IndObjectPresentation A
P₂ : IndObjectPresentation B
i : K f g P₁ P₂
⊢ { pt := A, ι := ι₁ f g P₁ P₂ : Cocone (F₁ f g P₁ P₂ ⋙ yoneda) }.ι.app i ≫ g =
    { pt := A, ι := ι₁ f g P₁ P₂ : Cocone (F₁ f g P₁ P₂ ⋙ yoneda) }.ι.app i ≫
      (isColimit₁ f g P₁ P₂).map { pt := B, ι := ι₂ f g P₁ P₂ } (whiskerRight (ψ f g P₁ P₂) yoneda)
have rw : { pt := A, ι := ι₁ f g P₁ P₂ : Cocone (F₁ f g P₁ P₂ ⋙ yoneda) }.ι.app i ≫ g =
  (whiskerRight (ψ f g P₁ P₂) yoneda).app i ≫ { pt := B, ι := ι₂ f g P₁ P₂ }.ι.app i
Tactic: rw [IsColimit.ι_map]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Indization.Products (goal)
Goal:
C : Type u
inst : Category.{v, u} C
α : Type v
h : ∀ (g : α → C), IsIndObject.{v, u} (∏ᶜ Functor.obj yoneda ∘ g)
f : α → Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)
hf : ∀ (a : α), IsIndObject (f a)
F : (a : α) → ⋯.presentation.I ⥤ Functor.{v, v, u, v + 1} Cᵒᵖ (Type v) := fun (a : α) ↦ ⋯.presentation.F ⋙ yoneda
⊢ IsIndObject (∏ᶜ f)
have suffices : ∏ᶜ f ≅ colimit (pointwiseProduct (I := fun (i : α) ↦ sorry.presentation.I) F)
Tactic: suffices (∏ᶜ f ≅ colimit (pointwiseProduct F)) from
    (isIndObject_colimit _ _ (fun i => h _)).map this.inv
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Indization.Products (goal)
Goal:
C : Type u
inst : Category.{v, u} C
α : Type v
h : ∀ (g : α → C), IsIndObject.{v, u} (∏ᶜ Functor.obj yoneda ∘ g)
f : α → Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)
hf : ∀ (a : α), IsIndObject (f a)
F : (a : α) → ⋯.presentation.I ⥤ Functor.{v, v, u, v + 1} Cᵒᵖ (Type v) := fun (a : α) ↦ ⋯.presentation.F ⋙ yoneda
⊢ ∏ᶜ f ≅ colimit (pointwiseProduct (I := fun (i : α) ↦ ⋯.presentation.I) F)
have refine : (s : α) → f s ≅ colimit (F s)
Tactic: refine Pi.mapIso (fun s => ?_) ≪≫ (asIso (colimitPointwiseProductToProductColimit F)).symm
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.IsConnected (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsConnected.{v, u} C
s : Cocone.{v, w, u, w + 1} (constPUnitFunctor C)
j : C
⊢ CategoryStruct.comp (Y :=
      Functor.obj.{v, w, u, w + 1} (Functor.obj (Functor.const C) (Cocone.pt.{v, w, u, w + 1} (pUnitCocone C))) j)
      (NatTrans.app (Cocone.ι (pUnitCocone C)) j) (s.ι.app Classical.ofNonempty) =
    s.ι.app j
have h : TypeCat.Fun.toFun
    (ConcreteCategory.hom (FC := TypeCat.Fun)
      (CategoryStruct.comp (Y :=
        Functor.obj.{v, w, u, w + 1} (Functor.obj (Functor.const C) (Cocone.pt.{v, w, u, w + 1} (pUnitCocone C))) j)
        (NatTrans.app (Cocone.ι (pUnitCocone C)) j) (s.ι.app Classical.ofNonempty)))
    PUnit.unit =
  (ConcreteCategory.hom (FC := TypeCat.Fun) (s.ι.app j)).toFun PUnit.unit
Tactic: ext ⟨⟩