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
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)
⊢ 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)
have rw₂ : 𝟙 (limit (F.rightOp ⋙ Functor.obj yoneda A)) ≫ limit.π (F.rightOp ⋙ Functor.obj yoneda A) i =
  limit.π (F.rightOp ⋙ Functor.obj yoneda A) i
Tactic: rw [← dsimp% colimitHomIsoLimitYoneda'_hom_comp_π, ← Category.assoc,
    Iso.inv_hom_id, Category.id_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
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
⊢ 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)
have 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)
Tactic: rw [← dsimp% colimitHomIsoLimitYoneda'_hom_comp_π, ← Category.assoc,
    Iso.inv_hom_id, Category.id_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 : 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 (α := (fun (X : Type (max u₁ u₂)) ↦ X) ((D ⋙ F ⋙ uliftFunctor.{u₁, u₂}).obj (op i)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (CategoryStruct.comp (Y := limit (D ⋙ F ⋙ uliftFunctor.{u₁, u₂}))
              (Iso.hom (colimitCoyonedaHomIsoLimit D F) :
                (colimit (D.rightOp ⋙ coyoneda) ⟶ F) ⟶ limit (D ⋙ F ⋙ uliftFunctor.{u₁, u₂}))
              (limit.π (D ⋙ F ⋙ uliftFunctor.{u₁, u₂}) (op i) :
                limit (D ⋙ F ⋙ uliftFunctor.{u₁, u₂}) ⟶ (D ⋙ F ⋙ uliftFunctor.{u₁, u₂}).obj (op i))) :
          (a : (fun (X : Type (max u₁ u₂)) ↦ X) (colimit (D.rightOp ⋙ coyoneda) ⟶ F)) →
            (fun (X : Type (max u₁ u₂)) ↦ X) ((D ⋙ F ⋙ uliftFunctor.{u₁, u₂}).obj (op i)))
        f :
      (fun (X : Type (max u₁ u₂)) ↦ X) ((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))))
have simp : 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: simp only [colimitCoyonedaHomIsoLimit, 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 : 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 (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))))
have 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))))
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.unop ⋙ yoneda)
inst_3 : HasLimitsOfShape Iᵒᵖ (Type (max u₁ u₂))
f : colimit (D.unop ⋙ 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.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)))
have 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)))
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.unop ⋙ yoneda)
inst_3 : HasLimitsOfShape Iᵒᵖ (Type (max u₁ u₂))
f : colimit (D.unop ⋙ yoneda) ⟶ F
i : 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)))
have 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)))
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.unop ⋙ yoneda)
inst_3 : HasLimitsOfShape Iᵒᵖ (Type (max u₁ u₂))
f : colimit (D.unop ⋙ yoneda) ⟶ F
i : Iᵒᵖ
⊢ 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)))
have dsimp : Eq (α := ULift.{u₁, u₂} (F.obj (D.obj i)))
  ((ConcreteCategory.hom (FC := TypeCat.Fun)
          ((↾fun (g : colimit (D.unop ⋙ yoneda) ⟶ F) ↦ colimit.ι (D.unop ⋙ yoneda) (unop i) ≫ g) ≫
            Iso.hom (Equiv.toIso (Equiv.trans yonedaEquiv (Equiv.symm Equiv.ulift)))) :
        (a : colimit (D.unop ⋙ 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.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: dsimp [yonedaLemma]
-- 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 (α := (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 (colimitCoyonedaHomIsoLimit' D F) :
                (colimit (D.op ⋙ coyoneda) ⟶ 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.op ⋙ coyoneda) ⟶ 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.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 simp : Eq (α := (D ⋙ F ⋙ uliftFunctor.{u₁, u₂}).obj i)
  ((ConcreteCategory.hom (FC := TypeCat.Fun)
          (Iso.hom (colimitHomIsoLimitYoneda' (D.op ⋙ coyoneda) F) ≫
            limit.π ((D.op ⋙ coyoneda).rightOp ⋙ Functor.obj yoneda F) i ≫
              NatTrans.app (Iso.hom (Functor.isoWhiskerLeft (D ⋙ Prod.sectL C F) (coyonedaLemma C))) 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)))
Tactic: simp only [colimitCoyonedaHomIsoLimit', 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 : 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 (FC := TypeCat.Fun)
            (Iso.hom (colimitHomIsoLimitYoneda' (D.op ⋙ coyoneda) F) ≫
              limit.π ((D.op ⋙ coyoneda).rightOp ⋙ Functor.obj yoneda F) i ≫
                NatTrans.app (Iso.hom (Functor.isoWhiskerLeft (D ⋙ Prod.sectL C F) (coyonedaLemma C))) 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 rw : 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)))
Tactic: rw [← Category.assoc, colimitHomIsoLimitYoneda'_hom_comp_π]