-- 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
⊢ ((yonedaYonedaColimit F).app (op X)).inv =
    (colimitObjIsoColimitCompEvaluation (F ⋙ yoneda) (yoneda.op.obj (op X))).hom ≫
      colimit.post F (coyoneda.obj (op (yoneda.obj X)))

Tactic:
dsimp [yonedaYonedaColimit]

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
⊢ (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)))

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.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)

Tactic:
rw [ι_preservesColimitIso_inv_assoc, ← Functor.map_comp_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 ≫
      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)

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
⊢ (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) =
    (coyoneda.obj (op (yoneda.obj X))).map (colimit.ι F j)

Tactic:
ext η Y f

Result:
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

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
⊢ 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)))

Tactic:
apply colimit.hom_ext

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
⊢ (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)

Tactic:
rw [colimitObjIsoColimitCompEvaluation_ι_inv, whiskerLeft_app]

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
⊢ (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) =
    (coyoneda.obj (op (yoneda.obj X))).map (colimit.ι F j)