-- Mathlib/CategoryTheory/Limits/Preserves/Yoneda.lean
theorem yonedaYonedaColimit_app_inv {X : C} : ((yonedaYonedaColimit F).app (op X)).inv =
    (colimitObjIsoColimitCompEvaluation _ _).hom ≫
      (colimit.post F (coyoneda.obj (op (yoneda.obj X))))

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
J : Type u₂
inst✝² : Category.{v₂, u₂} J
inst✝¹ : HasColimitsOfShape J (Type v₁)
inst✝ : HasColimitsOfShape J (Type (max u₁ v₁))
F : J ⥤ Cᵒᵖ ⥤ Type v₁
X : C
⊢ (colimitObjIsoColimitCompEvaluation (F ⋙ yoneda) (op (yoneda.obj X))).hom ≫
      colimMap (whiskerLeft F (largeCurriedYonedaLemma.hom.app (op X))) ≫
        (preservesColimitIso uliftFunctor.{u₁, v₁} (F.flip.obj (op X))).inv ≫
          uliftFunctor.{u₁, v₁}.map (colimitObjIsoColimitCompEvaluation F (op X)).inv ≫
            (yonedaOpCompYonedaObj (colimit F)).inv.app (op X) =
    (colimitObjIsoColimitCompEvaluation (F ⋙ yoneda) (op (yoneda.obj X))).hom ≫
      colimit.post F (coyoneda.obj (op (yoneda.obj X)))

Tactic:
simp only [Category.id_comp, Iso.cancel_iso_hom_left]

Result:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
J : Type u₂
inst✝² : Category.{v₂, u₂} J
inst✝¹ : HasColimitsOfShape J (Type v₁)
inst✝ : HasColimitsOfShape J (Type (max u₁ v₁))
F : J ⥤ Cᵒᵖ ⥤ Type v₁
X : C
⊢ colimMap (whiskerLeft F (largeCurriedYonedaLemma.hom.app (op X))) ≫
      (preservesColimitIso uliftFunctor.{u₁, v₁} (F.flip.obj (op X))).inv ≫
        uliftFunctor.{u₁, v₁}.map (colimitObjIsoColimitCompEvaluation F (op X)).inv ≫
          (yonedaOpCompYonedaObj (colimit F)).inv.app (op X) =
    colimit.post F (coyoneda.obj (op (yoneda.obj X)))

Proof state:
case w
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
J : Type u₂
inst✝² : Category.{v₂, u₂} J
inst✝¹ : HasColimitsOfShape J (Type v₁)
inst✝ : HasColimitsOfShape J (Type (max u₁ v₁))
F : J ⥤ Cᵒᵖ ⥤ Type v₁
X : C
j : J
⊢ (whiskerLeft F (largeCurriedYonedaLemma.hom.app (op X))).app j ≫
      uliftFunctor.{u₁, v₁}.map (colimit.ι (F.flip.obj (op X)) j ≫ (colimitObjIsoColimitCompEvaluation F (op X)).inv) ≫
        (yonedaOpCompYonedaObj (colimit F)).inv.app (op X) =
    (coyoneda.obj (op (yoneda.obj X))).map (colimit.ι F j)

Tactic:
simp only [← comp_evaluation]

Result:
case w
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
J : Type u₂
inst✝² : Category.{v₂, u₂} J
inst✝¹ : HasColimitsOfShape J (Type v₁)
inst✝ : HasColimitsOfShape J (Type (max u₁ v₁))
F : J ⥤ Cᵒᵖ ⥤ Type v₁
X : C
j : J
⊢ (whiskerLeft F (largeCurriedYonedaLemma.hom.app (op X))).app j ≫
      uliftFunctor.{u₁, v₁}.map
          (colimit.ι (F ⋙ (evaluation Cᵒᵖ (Type v₁)).obj (op X)) j ≫
            (colimitObjIsoColimitCompEvaluation F (op X)).inv) ≫
        (yonedaOpCompYonedaObj (colimit F)).inv.app (op X) =
    (coyoneda.obj (op (yoneda.obj X))).map (colimit.ι F j)

Proof state:
case w.h.w.h.h
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
J : Type u₂
inst✝² : Category.{v₂, u₂} J
inst✝¹ : HasColimitsOfShape J (Type v₁)
inst✝ : HasColimitsOfShape J (Type (max u₁ v₁))
F : J ⥤ Cᵒᵖ ⥤ Type v₁
X : C
j : J
η : (F ⋙ coyoneda.obj (op (yoneda.obj X))).obj j
Y : Cᵒᵖ
f : (yoneda.obj X).obj Y
⊢ (((largeCurriedYonedaLemma.hom.app (op X)).app (F.obj j) ≫
            uliftFunctor.{u₁, v₁}.map ((colimit.ι F j).app (op X)) ≫ (yonedaOpCompYonedaObj (colimit F)).inv.app (op X))
          η).app
      Y f =
    ((coyoneda.obj (op (yoneda.obj X))).map (colimit.ι F j) η).app Y f

Tactic:
simp [largeCurriedYonedaLemma, yonedaOpCompYonedaObj, FunctorToTypes.colimit.map_ι_apply,
  map_yonedaEquiv]

Result:
no goals

Proof state:
case w
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
J : Type u₂
inst✝² : Category.{v₂, u₂} J
inst✝¹ : HasColimitsOfShape J (Type v₁)
inst✝ : HasColimitsOfShape J (Type (max u₁ v₁))
F : J ⥤ Cᵒᵖ ⥤ Type v₁
X : C
j : J
⊢ (whiskerLeft F (largeCurriedYonedaLemma.hom.app (op X))).app j ≫
      colimit.ι (F ⋙ (evaluation Cᵒᵖ (Type v₁)).obj (op X) ⋙ uliftFunctor.{u₁, v₁}) j ≫
        (preservesColimitIso uliftFunctor.{u₁, v₁} (F.flip.obj (op X))).inv ≫
          uliftFunctor.{u₁, v₁}.map (colimitObjIsoColimitCompEvaluation F (op X)).inv ≫
            (yonedaOpCompYonedaObj (colimit F)).inv.app (op X) =
    (coyoneda.obj (op (yoneda.obj X))).map (colimit.ι F j)

Tactic:
simp only [← CategoryTheory.Functor.assoc, comp_evaluation]

Result:
case w
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
J : Type u₂
inst✝² : Category.{v₂, u₂} J
inst✝¹ : HasColimitsOfShape J (Type v₁)
inst✝ : HasColimitsOfShape J (Type (max u₁ v₁))
F : J ⥤ Cᵒᵖ ⥤ Type v₁
X : C
j : J
⊢ (whiskerLeft F (largeCurriedYonedaLemma.hom.app (op X))).app j ≫
      colimit.ι (F.flip.obj (op X) ⋙ uliftFunctor.{u₁, v₁}) j ≫
        (preservesColimitIso uliftFunctor.{u₁, v₁} (F.flip.obj (op X))).inv ≫
          uliftFunctor.{u₁, v₁}.map (colimitObjIsoColimitCompEvaluation F (op X)).inv ≫
            (yonedaOpCompYonedaObj (colimit F)).inv.app (op X) =
    (coyoneda.obj (op (yoneda.obj X))).map (colimit.ι F j)

Proof state:
case w
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
J : Type u₂
inst✝² : Category.{v₂, u₂} J
inst✝¹ : HasColimitsOfShape J (Type v₁)
inst✝ : HasColimitsOfShape J (Type (max u₁ v₁))
F : J ⥤ Cᵒᵖ ⥤ Type v₁
X : C
⊢ ∀ (j : J),
    colimit.ι (F ⋙ coyoneda.obj (op (yoneda.obj X))) j ≫
        colimMap (whiskerLeft F (largeCurriedYonedaLemma.hom.app (op X))) ≫
          (preservesColimitIso uliftFunctor.{u₁, v₁} (F.flip.obj (op X))).inv ≫
            uliftFunctor.{u₁, v₁}.map (colimitObjIsoColimitCompEvaluation F (op X)).inv ≫
              (yonedaOpCompYonedaObj (colimit F)).inv.app (op X) =
      colimit.ι (F ⋙ coyoneda.obj (op (yoneda.obj X))) j ≫ colimit.post F (coyoneda.obj (op (yoneda.obj X)))

Tactic:
intro j

Result:
case w
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
J : Type u₂
inst✝² : Category.{v₂, u₂} J
inst✝¹ : HasColimitsOfShape J (Type v₁)
inst✝ : HasColimitsOfShape J (Type (max u₁ v₁))
F : J ⥤ Cᵒᵖ ⥤ Type v₁
X : C
j : J
⊢ colimit.ι (F ⋙ coyoneda.obj (op (yoneda.obj X))) j ≫
      colimMap (whiskerLeft F (largeCurriedYonedaLemma.hom.app (op X))) ≫
        (preservesColimitIso uliftFunctor.{u₁, v₁} (F.flip.obj (op X))).inv ≫
          uliftFunctor.{u₁, v₁}.map (colimitObjIsoColimitCompEvaluation F (op X)).inv ≫
            (yonedaOpCompYonedaObj (colimit F)).inv.app (op X) =
    colimit.ι (F ⋙ coyoneda.obj (op (yoneda.obj X))) j ≫ colimit.post F (coyoneda.obj (op (yoneda.obj X)))

Proof state:
case w
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
J : Type u₂
inst✝² : Category.{v₂, u₂} J
inst✝¹ : HasColimitsOfShape J (Type v₁)
inst✝ : HasColimitsOfShape J (Type (max u₁ v₁))
F : J ⥤ Cᵒᵖ ⥤ Type v₁
X : C
j : J
⊢ colimit.ι (F ⋙ coyoneda.obj (op (yoneda.obj X))) j ≫
      colimMap (whiskerLeft F (largeCurriedYonedaLemma.hom.app (op X))) ≫
        (preservesColimitIso uliftFunctor.{u₁, v₁} (F.flip.obj (op X))).inv ≫
          uliftFunctor.{u₁, v₁}.map (colimitObjIsoColimitCompEvaluation F (op X)).inv ≫
            (yonedaOpCompYonedaObj (colimit F)).inv.app (op X) =
    colimit.ι (F ⋙ coyoneda.obj (op (yoneda.obj X))) j ≫ colimit.post F (coyoneda.obj (op (yoneda.obj X)))

Tactic:
rw [colimit.ι_post, ι_colimMap_assoc]

Result:
case w
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
J : Type u₂
inst✝² : Category.{v₂, u₂} J
inst✝¹ : HasColimitsOfShape J (Type v₁)
inst✝ : HasColimitsOfShape J (Type (max u₁ v₁))
F : J ⥤ Cᵒᵖ ⥤ Type v₁
X : C
j : J
⊢ (whiskerLeft F (largeCurriedYonedaLemma.hom.app (op X))).app j ≫
      colimit.ι (F ⋙ (evaluation Cᵒᵖ (Type v₁)).obj (op X) ⋙ uliftFunctor.{u₁, v₁}) j ≫
        (preservesColimitIso uliftFunctor.{u₁, v₁} (F.flip.obj (op X))).inv ≫
          uliftFunctor.{u₁, v₁}.map (colimitObjIsoColimitCompEvaluation F (op X)).inv ≫
            (yonedaOpCompYonedaObj (colimit F)).inv.app (op X) =
    (coyoneda.obj (op (yoneda.obj X))).map (colimit.ι F j)