awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.IndYoneda
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
I : Type v₁
inst_1 : Category.{v₂, v₁} I
F : Functor.{v₂, u₂, v₁, u₁} Iᵒᵖ C
inst_2 : HasColimit F
i : I
rw :
  Eq (α := limit (F.rightOp ⋙ coyoneda) ⟶ Functor.obj coyoneda (op (F.obj (op i))))
    (CategoryStruct.comp (Y := Functor.obj coyoneda (op (colimit F))) (Iso.inv (coyonedaOpColimitIsoLimitCoyoneda' F))
        (Iso.hom (coyonedaOpColimitIsoLimitCoyoneda' F) ≫ limit.π (F.rightOp ⋙ coyoneda) i) :
      limit (F.rightOp ⋙ coyoneda) ⟶ Functor.obj coyoneda (op (F.obj (op i))))
    (limit.π (F.rightOp ⋙ coyoneda) i : limit (F.rightOp ⋙ coyoneda) ⟶ (F.rightOp ⋙ coyoneda).obj i)
rw₁ :
  Eq (α := limit (F.rightOp ⋙ coyoneda) ⟶ Functor.obj coyoneda (op (F.obj (op i))))
    (CategoryStruct.comp (Y := limit (F.rightOp ⋙ coyoneda))
        (CategoryStruct.comp (Y := Functor.obj coyoneda (op (colimit F)))
            (Iso.inv (coyonedaOpColimitIsoLimitCoyoneda' F)) (Iso.hom (coyonedaOpColimitIsoLimitCoyoneda' F)) :
          limit (F.rightOp ⋙ coyoneda) ⟶ limit (F.rightOp ⋙ coyoneda))
        (limit.π (F.rightOp ⋙ coyoneda) i : limit (F.rightOp ⋙ coyoneda) ⟶ (F.rightOp ⋙ coyoneda).obj i) :
      limit (F.rightOp ⋙ coyoneda) ⟶ Functor.obj coyoneda (op (F.obj (op i))))
    (limit.π (F.rightOp ⋙ coyoneda) i : limit (F.rightOp ⋙ coyoneda) ⟶ (F.rightOp ⋙ coyoneda).obj i)
rw₂ : 𝟙 (limit (F.rightOp ⋙ coyoneda)) ≫ limit.π (F.rightOp ⋙ coyoneda) i = limit.π (F.rightOp ⋙ coyoneda) i
rw₃ rw₄ :
  Eq (α := limit (F.rightOp ⋙ coyoneda) ⟶ Functor.obj coyoneda (op (F.obj (op i)))) (limit.π (F.rightOp ⋙ coyoneda) i)
    (limit.π (F.rightOp ⋙ coyoneda) i)
⊢ Eq (α := limit (F.rightOp ⋙ coyoneda) ⟶ Functor.obj coyoneda (op (F.obj (op i))))
    (CategoryStruct.comp (Y := Functor.obj coyoneda (op (colimit F))) (Iso.inv (coyonedaOpColimitIsoLimitCoyoneda' F))
        (Functor.map coyoneda (Quiver.Hom.op (colimit.ι F (op i)))) :
      limit (F.rightOp ⋙ coyoneda) ⟶ Functor.obj coyoneda (op (F.obj (op i))))
    (limit.π (F.rightOp ⋙ coyoneda) i : limit (F.rightOp ⋙ coyoneda) ⟶ (F.rightOp ⋙ coyoneda).obj i)

Tactic:
rw [← coyonedaOpColimitIsoLimitCoyoneda'_hom_comp_π, ← Category.assoc,
    Iso.inv_hom_id, Category.id_comp]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.inv_hom_id, CategoryTheory.Limits.coyonedaOpColimitIsoLimitCoyoneda'_hom_comp_π, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Limits.IndYoneda
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
I : Type v₁
inst_1 : Category.{v₂, v₁} I
F : Functor.{v₂, u₂, v₁, u₁} Iᵒᵖ C
inst_2 : HasColimit F
inst_3 : HasLimitsOfShape.{v₂, v₁, u₂, u₂ + 1} I (Type u₂)
A : C
i : I
simp :
  Eq (α := (colimit F ⟶ A) ⟶ (F.rightOp ⋙ Functor.obj yoneda A).obj i)
    (NatTrans.app (Iso.hom (coyonedaOpColimitIsoLimitCoyoneda' F)) A ≫
      CategoryStruct.comp (Y := limit (F.rightOp ⋙ Functor.obj yoneda A))
        (Iso.hom (limitObjIsoLimitCompEvaluation (F.rightOp ⋙ coyoneda) A) :
          (limit (F.rightOp ⋙ coyoneda)).obj A ⟶ limit (F.rightOp ⋙ Functor.obj yoneda A))
        (limit.π (F.rightOp ⋙ Functor.obj yoneda A) i :
          limit (F.rightOp ⋙ Functor.obj yoneda A) ⟶ (F.rightOp ⋙ Functor.obj yoneda A).obj i))
    (Functor.map (Functor.obj yoneda A) (Quiver.Hom.op (colimit.ι F (op i))))
⊢ Eq (α := (colimit F ⟶ A) ⟶ (F.rightOp ⋙ Functor.obj yoneda A).obj i)
    (Iso.hom (colimitHomIsoLimitYoneda' F A) ≫ limit.π (F.rightOp ⋙ Functor.obj yoneda A) i)
    (Functor.map (Functor.obj yoneda A) (Quiver.Hom.op (colimit.ι F (op i))))

Tactic:
simp only [colimitHomIsoLimitYoneda', Iso.trans_hom,
    Iso.app_hom, Category.assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.app_hom, CategoryTheory.Iso.trans_hom, CategoryTheory.Limits.colimitHomIsoLimitYoneda'
-- Module: Mathlib.CategoryTheory.Limits.IndYoneda
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
I : Type v₁
inst_1 : Category.{v₂, v₁} I
F : Functor.{v₂, u₂, v₁, u₁} Iᵒᵖ C
inst_2 : HasColimit F
inst_3 : HasLimitsOfShape.{v₂, v₁, u₂, u₂ + 1} I (Type u₂)
A : C
i : I
erw :
  Eq (α := (colimit F ⟶ A) ⟶ (F.rightOp ⋙ Functor.obj yoneda A).obj i)
    (NatTrans.app (Iso.hom (coyonedaOpColimitIsoLimitCoyoneda' F)) A ≫
      NatTrans.app (limit.π (F.rightOp ⋙ coyoneda) i) A)
    (Functor.map (Functor.obj yoneda A) (Quiver.Hom.op (colimit.ι F (op i))))
⊢ Eq (α := (colimit F ⟶ A) ⟶ (F.rightOp ⋙ Functor.obj yoneda A).obj i)
    (NatTrans.app (Iso.hom (coyonedaOpColimitIsoLimitCoyoneda' F)) A ≫
      CategoryStruct.comp (Y := limit (F.rightOp ⋙ Functor.obj yoneda A))
        (Iso.hom (limitObjIsoLimitCompEvaluation (F.rightOp ⋙ coyoneda) A) :
          (limit (F.rightOp ⋙ coyoneda)).obj A ⟶ limit (F.rightOp ⋙ Functor.obj yoneda A))
        (limit.π (F.rightOp ⋙ Functor.obj yoneda A) i :
          limit (F.rightOp ⋙ Functor.obj yoneda A) ⟶ (F.rightOp ⋙ Functor.obj yoneda A).obj i))
    (Functor.map (Functor.obj yoneda A) (Quiver.Hom.op (colimit.ι F (op i))))

Tactic:
erw [limitObjIsoLimitCompEvaluation_hom_π]

Premises used: CategoryTheory.Limits.limitObjIsoLimitCompEvaluation_hom_π
-- Module: Mathlib.CategoryTheory.Limits.IndYoneda
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
I : Type v₁
inst_1 : Category.{v₂, v₁} I
F : Functor.{v₂, u₂, v₁, u₁} Iᵒᵖ C
inst_2 : HasColimit F
inst_3 : HasLimitsOfShape.{v₂, v₁, u₂, u₂ + 1} I (Type u₂)
A : C
i : I
change :
  Eq (α := Functor.obj (Functor.obj coyoneda (op (colimit F))) A ⟶ ((F.rightOp ⋙ coyoneda).obj i).obj A)
    (NatTrans.app (Iso.hom (coyonedaOpColimitIsoLimitCoyoneda' F) ≫ limit.π (F.rightOp ⋙ coyoneda) i) A)
    (Functor.map (Functor.obj yoneda A) (Quiver.Hom.op (colimit.ι F (op i))))
⊢ Eq (α := (colimit F ⟶ A) ⟶ (F.rightOp ⋙ Functor.obj yoneda A).obj i)
    (NatTrans.app (Iso.hom (coyonedaOpColimitIsoLimitCoyoneda' F)) A ≫
      NatTrans.app (limit.π (F.rightOp ⋙ coyoneda) i) A)
    (Functor.map (Functor.obj yoneda A) (Quiver.Hom.op (colimit.ι F (op i))))

Tactic:
change ((coyonedaOpColimitIsoLimitCoyoneda' F).hom ≫ _).app A = _

Premises used: CategoryTheory.Limits.coyonedaOpColimitIsoLimitCoyoneda', CategoryTheory.CategoryStruct.comp, CategoryTheory.Iso.hom, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.Limits.IndYoneda
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
I : Type v₁
inst_1 : Category.{v₂, v₁} I
F : Functor.{v₂, u₂, v₁, u₁} Iᵒᵖ C
inst_2 : HasColimit F
inst_3 : HasLimitsOfShape.{v₂, v₁, u₂, u₂ + 1} I (Type u₂)
A : C
i : I
rw :
  Eq (α := Functor.obj (Functor.obj coyoneda (op (colimit F))) A ⟶ ((F.rightOp ⋙ coyoneda).obj i).obj A)
    (NatTrans.app (Functor.map coyoneda (Quiver.Hom.op (colimit.ι F (op i)))) A)
    (Functor.map (Functor.obj yoneda A) (Quiver.Hom.op (colimit.ι F (op i))))
rw₁ rw₂ :
  Eq (α := Functor.obj (Functor.obj coyoneda (op (colimit F))) A ⟶ ((F.rightOp ⋙ coyoneda).obj i).obj A)
    (Functor.map (Functor.obj yoneda A) (Quiver.Hom.op (colimit.ι F (op i))) :
      Functor.obj (Functor.obj yoneda A) (op (colimit F)) ⟶ Functor.obj (Functor.obj yoneda A) (op (F.obj (op i))))
    (Functor.map (Functor.obj yoneda A) (Quiver.Hom.op (colimit.ι F (op i))))
⊢ Eq (α := Functor.obj (Functor.obj coyoneda (op (colimit F))) A ⟶ ((F.rightOp ⋙ coyoneda).obj i).obj A)
    (NatTrans.app (Iso.hom (coyonedaOpColimitIsoLimitCoyoneda' F) ≫ limit.π (F.rightOp ⋙ coyoneda) i) A)
    (Functor.map (Functor.obj yoneda A) (Quiver.Hom.op (colimit.ι F (op i))))

Tactic:
rw [coyonedaOpColimitIsoLimitCoyoneda'_hom_comp_π, Functor.flip_map_app]

Premises used: CategoryTheory.Limits.coyonedaOpColimitIsoLimitCoyoneda'_hom_comp_π, CategoryTheory.Functor.flip_map_app
-- Module: Mathlib.CategoryTheory.Limits.IndYoneda
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
I : Type v₁
inst_1 : Category.{v₂, v₁} I
F : Functor.{v₂, u₂, v₁, u₁} Iᵒᵖ C
inst_2 : HasColimit F
inst_3 : HasLimitsOfShape.{v₂, v₁, u₂, u₂ + 1} I (Type u₂)
A : C
i : I
rw :
  Eq (α := limit (F.rightOp ⋙ Functor.obj yoneda A) ⟶ F.obj (op i) ⟶ A)
    (CategoryStruct.comp (Y := colimit F ⟶ A) (Iso.inv (colimitHomIsoLimitYoneda' F A))
        (Iso.hom (colimitHomIsoLimitYoneda' F A) ≫ limit.π (F.rightOp ⋙ Functor.obj yoneda A) i) :
      limit (F.rightOp ⋙ Functor.obj yoneda A) ⟶ F.obj (op i) ⟶ A)
    (limit.π (F.rightOp ⋙ Functor.obj yoneda A) i :
      limit (F.rightOp ⋙ Functor.obj yoneda A) ⟶ (F.rightOp ⋙ Functor.obj yoneda A).obj i)
rw₁ :
  Eq (α := limit (F.rightOp ⋙ Functor.obj yoneda A) ⟶ F.obj (op i) ⟶ A)
    (CategoryStruct.comp (Y := limit (F.rightOp ⋙ Functor.obj yoneda A))
        (CategoryStruct.comp (Y := colimit F ⟶ A) (Iso.inv (colimitHomIsoLimitYoneda' F A))
            (Iso.hom (colimitHomIsoLimitYoneda' F A)) :
          limit (F.rightOp ⋙ Functor.obj yoneda A) ⟶ limit (F.rightOp ⋙ Functor.obj yoneda A))
        (limit.π (F.rightOp ⋙ Functor.obj yoneda A) i :
          limit (F.rightOp ⋙ Functor.obj yoneda A) ⟶ (F.rightOp ⋙ Functor.obj yoneda A).obj i) :
      limit (F.rightOp ⋙ Functor.obj yoneda A) ⟶ F.obj (op i) ⟶ A)
    (limit.π (F.rightOp ⋙ Functor.obj yoneda A) i :
      limit (F.rightOp ⋙ Functor.obj yoneda A) ⟶ (F.rightOp ⋙ Functor.obj yoneda A).obj i)
rw₂ :
  𝟙 (limit (F.rightOp ⋙ Functor.obj yoneda A)) ≫ limit.π (F.rightOp ⋙ Functor.obj yoneda A) i =
    limit.π (F.rightOp ⋙ Functor.obj yoneda A) i
rw₃ rw₄ :
  Eq (α := limit (F.rightOp ⋙ Functor.obj yoneda A) ⟶ F.obj (op i) ⟶ A) (limit.π (F.rightOp ⋙ Functor.obj yoneda A) i)
    (limit.π (F.rightOp ⋙ Functor.obj yoneda A) i)
⊢ Eq (α := limit (F.rightOp ⋙ Functor.obj yoneda A) ⟶ F.obj (op i) ⟶ A)
    (CategoryStruct.comp (Y := colimit F ⟶ A) (Iso.inv (colimitHomIsoLimitYoneda' F A))
        (↾fun (g : colimit F ⟶ A) ↦ colimit.ι F (op i) ≫ g) :
      limit (F.rightOp ⋙ Functor.obj yoneda A) ⟶ F.obj (op i) ⟶ A)
    (limit.π (F.rightOp ⋙ Functor.obj yoneda A) i :
      limit (F.rightOp ⋙ Functor.obj yoneda A) ⟶ (F.rightOp ⋙ Functor.obj yoneda A).obj i)

Tactic:
rw [← dsimp% colimitHomIsoLimitYoneda'_hom_comp_π, ← Category.assoc,
    Iso.inv_hom_id, Category.id_comp]

Premises used: CategoryTheory.Limits.colimitHomIsoLimitYoneda'_hom_comp_π, CategoryTheory.Category.assoc, CategoryTheory.Iso.inv_hom_id, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Limits.IndYoneda
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.rightOp ⋙ coyoneda)
inst_3 : HasLimitsOfShape Iᵒᵖ (Type (max u₁ u₂))
f : colimit (D.rightOp ⋙ coyoneda) ⟶ F
i : I
rw :
  Eq (α := (D ⋙ F ⋙ uliftFunctor.{u₁, u₂}).obj (op i))
    (((@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
              (CategoryStruct.comp (Y := ((D.rightOp ⋙ coyoneda).op ⋙ Functor.obj yoneda F).obj (op i))
                (Functor.map (Functor.obj yoneda F) (Quiver.Hom.op (colimit.ι (D.rightOp ⋙ coyoneda) i)))
                (NatTrans.app (Iso.hom (Functor.isoWhiskerLeft (D ⋙ Prod.sectL C F) (coyonedaLemma C))) (op i))) :
            TypeCat.Fun (colimit (D.rightOp ⋙ coyoneda) ⟶ F) ((D ⋙ F ⋙ uliftFunctor.{u₁, u₂}).obj (op i))) :
          (a : colimit (D.rightOp ⋙ coyoneda) ⟶ F) → (D ⋙ F ⋙ uliftFunctor.{u₁, u₂}).obj (op i))
        f :
      (D ⋙ F ⋙ uliftFunctor.{u₁, u₂}).obj (op i))
    ({
        down :=
          (ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (D.obj (op i))) :
              (a : (colimit (D.rightOp ⋙ coyoneda)).obj (D.obj (op i))) → F.obj (D.obj (op i)))
            ((ConcreteCategory.hom (FC := TypeCat.Fun)
                    (NatTrans.app (colimit.ι (D.rightOp ⋙ coyoneda) i) (D.obj (op i))) :
                  (a : D.obj (op i) ⟶ D.obj (op i)) → (colimit (D.rightOp ⋙ coyoneda)).obj (D.obj (op i)))
                (𝟙 (D.obj (op i))) :
              (colimit (D.rightOp ⋙ coyoneda)).obj (D.obj (op i))) } :
      ULift.{u₁, u₂} (F.obj (D.obj (op i))))
⊢ Eq (α := (D ⋙ F ⋙ uliftFunctor.{u₁, u₂}).obj (op i))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (Iso.hom (colimitHomIsoLimitYoneda (D.rightOp ⋙ coyoneda) F) ≫
              CategoryStruct.comp (Y := ((D.rightOp ⋙ coyoneda).op ⋙ Functor.obj yoneda F).obj (op i))
                (limit.π ((D.rightOp ⋙ coyoneda).op ⋙ Functor.obj yoneda F) (op i))
                (NatTrans.app (Iso.hom (Functor.isoWhiskerLeft (D ⋙ Prod.sectL C F) (coyonedaLemma C))) (op i))) :
          (a : colimit (D.rightOp ⋙ coyoneda) ⟶ F) → (D ⋙ F ⋙ uliftFunctor.{u₁, u₂}).obj (op i))
        f :
      (D ⋙ F ⋙ uliftFunctor.{u₁, u₂}).obj (op i))
    ({
        down :=
          (ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (D.obj (op i))) :
              (a : (colimit (D.rightOp ⋙ coyoneda)).obj (D.obj (op i))) → F.obj (D.obj (op i)))
            ((ConcreteCategory.hom (FC := TypeCat.Fun)
                    (NatTrans.app (colimit.ι (D.rightOp ⋙ coyoneda) i) (D.obj (op i))) :
                  (a : D.obj (op i) ⟶ D.obj (op i)) → (colimit (D.rightOp ⋙ coyoneda)).obj (D.obj (op i)))
                (𝟙 (D.obj (op i))) :
              (colimit (D.rightOp ⋙ coyoneda)).obj (D.obj (op i))) } :
      ULift.{u₁, u₂} (F.obj (D.obj (op i))))

Tactic:
rw [← Category.assoc, colimitHomIsoLimitYoneda_hom_comp_π]

Premises used: CategoryTheory.Limits.colimitHomIsoLimitYoneda_hom_comp_π, CategoryTheory.Category.assoc
-- Module: Mathlib.CategoryTheory.Limits.IndYoneda
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.rightOp ⋙ coyoneda)
inst_3 : HasLimitsOfShape Iᵒᵖ (Type (max u₁ u₂))
f : colimit (D.rightOp ⋙ coyoneda) ⟶ F
i : I
⊢ Eq (α := (D ⋙ F ⋙ uliftFunctor.{u₁, u₂}).obj (op i))
    (((@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
              (NatTrans.app
                (Iso.hom
                  (Functor.isoWhiskerLeft (D ⋙ Prod.sectL C F)
                    (NatIso.ofComponents
                      (fun (x : C × (C ⥤ Type u₂)) ↦ Equiv.toIso (Equiv.trans coyonedaEquiv (Equiv.symm Equiv.ulift)))
                      ⋯)))
                (op i)) :
            TypeCat.Fun (((D.rightOp ⋙ coyoneda).op ⋙ Functor.obj yoneda F).obj (op i))
              ((D ⋙ F ⋙ uliftFunctor.{u₁, u₂}).obj (op i))) :
          (a : ((D.rightOp ⋙ coyoneda).op ⋙ yoneda.obj F).obj (op i)) → (D ⋙ F ⋙ uliftFunctor.{u₁, u₂}).obj (op i))
        (((@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
                (Functor.map (Functor.obj yoneda F) (Quiver.Hom.op (colimit.ι (D.rightOp ⋙ coyoneda) i))) :
              TypeCat.Fun (colimit (D.rightOp ⋙ coyoneda) ⟶ F)
                (((D.rightOp ⋙ coyoneda).op ⋙ Functor.obj yoneda F).obj (op i))) :
            (a : colimit (D.rightOp ⋙ coyoneda) ⟶ F) → ((D.rightOp ⋙ coyoneda).op ⋙ yoneda.obj F).obj (op i))
          f) :
      (D ⋙ F ⋙ uliftFunctor.{u₁, u₂}).obj (op i))
    ({
        down :=
          (ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (D.obj (op i))) :
              (a : (colimit (D.rightOp ⋙ coyoneda)).obj (D.obj (op i))) → F.obj (D.obj (op i)))
            ((ConcreteCategory.hom (FC := TypeCat.Fun)
                    (NatTrans.app (colimit.ι (D.rightOp ⋙ coyoneda) i) (D.obj (op i))) :
                  (a : D.obj (op i) ⟶ D.obj (op i)) → (colimit (D.rightOp ⋙ coyoneda)).obj (D.obj (op i)))
                (𝟙 (D.obj (op i))) :
              (colimit (D.rightOp ⋙ coyoneda)).obj (D.obj (op i))) } :
      ULift.{u₁, u₂} (F.obj (D.obj (op i))))

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.IndYoneda
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 ⋙ coyoneda)
inst_3 : HasLimitsOfShape Iᵒᵖ (Type (max u₁ u₂))
f : colimit (D ⋙ coyoneda) ⟶ F
i : I
⊢ Eq (α := ULift.{u₁, u₂} (F.obj (unop (D.obj i))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (limit.π (D.leftOp ⋙ F ⋙ uliftFunctor.{u₁, u₂}) (op i)) :
          (a : limit (D.leftOp ⋙ F ⋙ uliftFunctor.{u₁, u₂})) → ULift.{u₁, u₂} (F.obj (unop (D.obj i))))
        (((ConcreteCategory.hom (FC := TypeCat.Fun) (Iso.hom (colimitCoyonedaHomIsoLimitLeftOp D F)) :
              TypeCat.Fun (colimit (D ⋙ coyoneda) ⟶ F) (limit (D.leftOp ⋙ F ⋙ uliftFunctor.{u₁, u₂}))) :
            (a : colimit (D ⋙ coyoneda) ⟶ F) → limit (D.leftOp ⋙ F ⋙ uliftFunctor.{u₁, u₂}))
          f) :
      ULift.{u₁, u₂} (F.obj (unop (D.obj i))))
    ({
        down :=
          (ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (unop (D.obj i))) :
              (a : (colimit (D ⋙ coyoneda)).obj (unop (D.obj i))) → F.obj (unop (D.obj i)))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (colimit.ι (D ⋙ coyoneda) i) (unop (D.obj i))) :
                  (a : unop (D.obj i) ⟶ unop (D.obj i)) → (colimit (D ⋙ coyoneda)).obj (unop (D.obj i)))
                (𝟙 (unop (D.obj i))) :
              (colimit (D ⋙ coyoneda)).obj (unop (D.obj i))) } :
      ULift.{u₁, u₂} (F.obj (unop (D.obj i))))

Tactic:
haveI : HasColimit (D.leftOp.rightOp ⋙ coyoneda) :=
    inferInstanceAs <| HasColimit (D ⋙ coyoneda)
  colimitCoyonedaHomIsoLimit_π_apply _ _ _ _

Premises used: Quiver.Hom.op, Quiver.Hom.unop, CategoryTheory.Limits.colimitCoyonedaHomIsoLimit_π_apply, CategoryTheory.Functor.rightOp, CategoryTheory.Functor.leftOp
-- Module: Mathlib.CategoryTheory.Limits.IndYoneda
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.unop ⋙ yoneda)
inst_3 : HasLimitsOfShape Iᵒᵖ (Type (max u₁ u₂))
f : colimit (D.unop ⋙ yoneda) ⟶ F
i : Iᵒᵖ
simp :
  Eq (α := (D ⋙ F ⋙ uliftFunctor.{u₁, u₂}).obj i)
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (Iso.hom (colimitHomIsoLimitYoneda (D.unop ⋙ yoneda) F) ≫
              limit.π ((D.unop ⋙ yoneda).op ⋙ Functor.obj yoneda F) i ≫
                NatTrans.app (Iso.hom (Functor.isoWhiskerLeft (D ⋙ Prod.sectL Cᵒᵖ F) (yonedaLemma C))) i) :
          (a : colimit (D.unop ⋙ 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.unop ⋙ yoneda)).obj (D.obj i)) → F.obj (D.obj i))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (colimit.ι (D.unop ⋙ yoneda) (unop i)) (D.obj i)) :
                  (a : unop (D.obj i) ⟶ unop (D.obj i)) → (colimit (D.unop ⋙ yoneda)).obj (D.obj i))
                (𝟙 (unop (D.obj i))) :
              (colimit (D.unop ⋙ yoneda)).obj (D.obj i)) } :
      ULift.{u₁, u₂} (F.obj (D.obj 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.unop ⋙ 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.unop ⋙ 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.unop ⋙ yoneda)).obj (D.obj i)) → F.obj (D.obj i))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (colimit.ι (D.unop ⋙ yoneda) (unop i)) (D.obj i)) :
                  (a : unop (D.obj i) ⟶ unop (D.obj i)) → (colimit (D.unop ⋙ yoneda)).obj (D.obj i))
                (𝟙 (unop (D.obj i))) :
              (colimit (D.unop ⋙ 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_π]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.colimitYonedaHomIsoLimit, CategoryTheory.Iso.trans_hom, CategoryTheory.Limits.HasLimit.isoOfNatIso_hom_π
-- Module: Mathlib.CategoryTheory.Limits.IndYoneda
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.unop ⋙ yoneda)
inst_3 : HasLimitsOfShape Iᵒᵖ (Type (max u₁ u₂))
f : colimit (D.unop ⋙ yoneda) ⟶ F
i : Iᵒᵖ
rw :
  Eq (α := (D ⋙ F ⋙ uliftFunctor.{u₁, u₂}).obj i)
    (((@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
              (CategoryStruct.comp (Y := ((D.unop ⋙ yoneda).op ⋙ Functor.obj yoneda F).obj i)
                (Functor.map (Functor.obj yoneda F) (Quiver.Hom.op (colimit.ι (D.unop ⋙ yoneda) (unop i))))
                (NatTrans.app (Iso.hom (Functor.isoWhiskerLeft (D ⋙ Prod.sectL Cᵒᵖ F) (yonedaLemma C))) i)) :
            TypeCat.Fun (colimit (D.unop ⋙ yoneda) ⟶ F) ((D ⋙ F ⋙ uliftFunctor.{u₁, u₂}).obj i)) :
          (a : colimit (D.unop ⋙ 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.unop ⋙ yoneda)).obj (D.obj i)) → F.obj (D.obj i))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (colimit.ι (D.unop ⋙ yoneda) (unop i)) (D.obj i)) :
                  (a : unop (D.obj i) ⟶ unop (D.obj i)) → (colimit (D.unop ⋙ yoneda)).obj (D.obj i))
                (𝟙 (unop (D.obj i))) :
              (colimit (D.unop ⋙ yoneda)).obj (D.obj i)) } :
      ULift.{u₁, u₂} (F.obj (D.obj i)))
⊢ Eq (α := (D ⋙ F ⋙ uliftFunctor.{u₁, u₂}).obj i)
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (Iso.hom (colimitHomIsoLimitYoneda (D.unop ⋙ yoneda) F) ≫
              limit.π ((D.unop ⋙ yoneda).op ⋙ Functor.obj yoneda F) i ≫
                NatTrans.app (Iso.hom (Functor.isoWhiskerLeft (D ⋙ Prod.sectL Cᵒᵖ F) (yonedaLemma C))) i) :
          (a : colimit (D.unop ⋙ 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.unop ⋙ yoneda)).obj (D.obj i)) → F.obj (D.obj i))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (colimit.ι (D.unop ⋙ yoneda) (unop i)) (D.obj i)) :
                  (a : unop (D.obj i) ⟶ unop (D.obj i)) → (colimit (D.unop ⋙ yoneda)).obj (D.obj i))
                (𝟙 (unop (D.obj i))) :
              (colimit (D.unop ⋙ yoneda)).obj (D.obj i)) } :
      ULift.{u₁, u₂} (F.obj (D.obj i)))

Tactic:
rw [← Category.assoc, colimitHomIsoLimitYoneda_hom_comp_π]

Premises used: CategoryTheory.Limits.colimitHomIsoLimitYoneda_hom_comp_π, CategoryTheory.Category.assoc