-- Mathlib/CategoryTheory/Limits/IndYoneda.lean
@[simp]
lemma colimitYonedaHomIsoLimit_π_apply (f : colimit (D.unop ⋙ yoneda) ⟶ F) (i : Iᵒᵖ) :
    limit.π (D ⋙ F ⋙ uliftFunctor.{u₁}) i ((colimitYonedaHomIsoLimit D F).hom f) =
      ⟨f.app (D.obj i)
        ((colimit.ι (D.unop ⋙ yoneda) i.unop).app (D.obj i) (𝟙 (D.obj i).unop))⟩

Proof state:
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
I : Type v₁
inst✝² : Category.{v₂, v₁} I
D : Iᵒᵖ ⥤ Cᵒᵖ
F : Cᵒᵖ ⥤ Type u₂
inst✝¹ : HasColimit (D.unop ⋙ yoneda)
inst✝ : HasLimitsOfShape Iᵒᵖ (Type (max u₁ u₂))
f : colimit (D.unop ⋙ yoneda) ⟶ F
i : Iᵒᵖ
⊢ Equiv.ulift.symm (yonedaEquiv (colimit.ι (D.unop ⋙ yoneda) (unop i) ≫ f)) =
    { down := f.app (D.obj i) ((colimit.ι (D.unop ⋙ yoneda) (unop i)).app (D.obj i) (𝟙 (unop (D.obj i)))) }

Tactic:
erw [yonedaEquiv_comp, yonedaEquiv_apply]

Result:
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
I : Type v₁
inst✝² : Category.{v₂, v₁} I
D : Iᵒᵖ ⥤ Cᵒᵖ
F : Cᵒᵖ ⥤ Type u₂
inst✝¹ : HasColimit (D.unop ⋙ yoneda)
inst✝ : HasLimitsOfShape Iᵒᵖ (Type (max u₁ u₂))
f : colimit (D.unop ⋙ yoneda) ⟶ F
i : Iᵒᵖ
⊢ Equiv.ulift.symm
      (f.app (op (unop (D.obj i)))
        ((colimit.ι (D.unop ⋙ yoneda) (unop i)).app (op (unop (D.obj i))) (𝟙 (unop (D.obj i))))) =
    { down := f.app (D.obj i) ((colimit.ι (D.unop ⋙ yoneda) (unop i)).app (D.obj i) (𝟙 (unop (D.obj i)))) }

Proof state:
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
I : Type v₁
inst✝² : Category.{v₂, v₁} I
D : Iᵒᵖ ⥤ Cᵒᵖ
F : Cᵒᵖ ⥤ Type u₂
inst✝¹ : HasColimit (D.unop ⋙ yoneda)
inst✝ : HasLimitsOfShape Iᵒᵖ (Type (max u₁ u₂))
f : colimit (D.unop ⋙ yoneda) ⟶ F
i : Iᵒᵖ
⊢ ((colimitYonedaHomIsoLimit D F).hom ≫ limit.π (D ⋙ F ⋙ uliftFunctor.{u₁, u₂}) i) f =
    { down := f.app (D.obj i) ((colimit.ι (D.unop ⋙ yoneda) (unop i)).app (D.obj i) (𝟙 (unop (D.obj i)))) }

Tactic:
simp only [colimitYonedaHomIsoLimit, Iso.trans_hom, Category.assoc, HasLimit.isoOfNatIso_hom_π]

Result:
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
I : Type v₁
inst✝² : Category.{v₂, v₁} I
D : Iᵒᵖ ⥤ Cᵒᵖ
F : Cᵒᵖ ⥤ Type u₂
inst✝¹ : HasColimit (D.unop ⋙ yoneda)
inst✝ : HasLimitsOfShape Iᵒᵖ (Type (max u₁ u₂))
f : colimit (D.unop ⋙ yoneda) ⟶ F
i : Iᵒᵖ
⊢ ((colimitHomIsoLimitYoneda (D.unop ⋙ yoneda) F).hom ≫
        limit.π ((D.unop ⋙ yoneda).op ⋙ yoneda.obj F) i ≫
          (isoWhiskerLeft (D ⋙ Prod.sectL Cᵒᵖ F) (yonedaLemma C)).hom.app i)
      f =
    { down := f.app (D.obj i) ((colimit.ι (D.unop ⋙ yoneda) (unop i)).app (D.obj i) (𝟙 (unop (D.obj i)))) }

Proof state:
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
I : Type v₁
inst✝² : Category.{v₂, v₁} I
D : Iᵒᵖ ⥤ Cᵒᵖ
F : Cᵒᵖ ⥤ Type u₂
inst✝¹ : HasColimit (D.unop ⋙ yoneda)
inst✝ : HasLimitsOfShape Iᵒᵖ (Type (max u₁ u₂))
f : colimit (D.unop ⋙ yoneda) ⟶ F
i : Iᵒᵖ
⊢ ((colimitHomIsoLimitYoneda (D.unop ⋙ yoneda) F).hom ≫
        limit.π ((D.unop ⋙ yoneda).op ⋙ yoneda.obj F) i ≫
          (isoWhiskerLeft (D ⋙ Prod.sectL Cᵒᵖ F) (yonedaLemma C)).hom.app i)
      f =
    { down := f.app (D.obj i) ((colimit.ι (D.unop ⋙ yoneda) (unop i)).app (D.obj i) (𝟙 (unop (D.obj i)))) }

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

Result:
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
I : Type v₁
inst✝² : Category.{v₂, v₁} I
D : Iᵒᵖ ⥤ Cᵒᵖ
F : Cᵒᵖ ⥤ Type u₂
inst✝¹ : HasColimit (D.unop ⋙ yoneda)
inst✝ : HasLimitsOfShape Iᵒᵖ (Type (max u₁ u₂))
f : colimit (D.unop ⋙ yoneda) ⟶ F
i : Iᵒᵖ
⊢ ((coyoneda.map (colimit.ι (D.unop ⋙ yoneda) (unop i)).op).app F ≫
        (isoWhiskerLeft (D ⋙ Prod.sectL Cᵒᵖ F) (yonedaLemma C)).hom.app i)
      f =
    { down := f.app (D.obj i) ((colimit.ι (D.unop ⋙ yoneda) (unop i)).app (D.obj i) (𝟙 (unop (D.obj i)))) }

Proof state:
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
I : Type v₁
inst✝² : Category.{v₂, v₁} I
D : Iᵒᵖ ⥤ Cᵒᵖ
F : Cᵒᵖ ⥤ Type u₂
inst✝¹ : HasColimit (D.unop ⋙ yoneda)
inst✝ : HasLimitsOfShape Iᵒᵖ (Type (max u₁ u₂))
f : colimit (D.unop ⋙ yoneda) ⟶ F
i : Iᵒᵖ
⊢ limit.π (D ⋙ F ⋙ uliftFunctor.{u₁, u₂}) i ((colimitYonedaHomIsoLimit D F).hom f) =
    { down := f.app (D.obj i) ((colimit.ι (D.unop ⋙ yoneda) (unop i)).app (D.obj i) (𝟙 (unop (D.obj i)))) }

Tactic:
change ((colimitYonedaHomIsoLimit D F).hom ≫ (limit.π (D ⋙ F ⋙ uliftFunctor.{u₁}) i)) f = _

Result:
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
I : Type v₁
inst✝² : Category.{v₂, v₁} I
D : Iᵒᵖ ⥤ Cᵒᵖ
F : Cᵒᵖ ⥤ Type u₂
inst✝¹ : HasColimit (D.unop ⋙ yoneda)
inst✝ : HasLimitsOfShape Iᵒᵖ (Type (max u₁ u₂))
f : colimit (D.unop ⋙ yoneda) ⟶ F
i : Iᵒᵖ
⊢ ((colimitYonedaHomIsoLimit D F).hom ≫ limit.π (D ⋙ F ⋙ uliftFunctor.{u₁, u₂}) i) f =
    { down := f.app (D.obj i) ((colimit.ι (D.unop ⋙ yoneda) (unop i)).app (D.obj i) (𝟙 (unop (D.obj i)))) }

Proof state:
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
I : Type v₁
inst✝² : Category.{v₂, v₁} I
D : Iᵒᵖ ⥤ Cᵒᵖ
F : Cᵒᵖ ⥤ Type u₂
inst✝¹ : HasColimit (D.unop ⋙ yoneda)
inst✝ : HasLimitsOfShape Iᵒᵖ (Type (max u₁ u₂))
f : colimit (D.unop ⋙ yoneda) ⟶ F
i : Iᵒᵖ
⊢ Equiv.ulift.symm
      (f.app (op (unop (D.obj i)))
        ((colimit.ι (D.unop ⋙ yoneda) (unop i)).app (op (unop (D.obj i))) (𝟙 (unop (D.obj i))))) =
    { down := f.app (D.obj i) ((colimit.ι (D.unop ⋙ yoneda) (unop i)).app (D.obj i) (𝟙 (unop (D.obj i)))) }

Tactic:
rfl

Result:
no goals

Proof state:
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
I : Type v₁
inst✝² : Category.{v₂, v₁} I
D : Iᵒᵖ ⥤ Cᵒᵖ
F : Cᵒᵖ ⥤ Type u₂
inst✝¹ : HasColimit (D.unop ⋙ yoneda)
inst✝ : HasLimitsOfShape Iᵒᵖ (Type (max u₁ u₂))
f : colimit (D.unop ⋙ yoneda) ⟶ F
i : Iᵒᵖ
⊢ ((coyoneda.map (colimit.ι (D.unop ⋙ yoneda) (unop i)).op).app F ≫
        (isoWhiskerLeft (D ⋙ Prod.sectL Cᵒᵖ F) (yonedaLemma C)).hom.app i)
      f =
    { down := f.app (D.obj i) ((colimit.ι (D.unop ⋙ yoneda) (unop i)).app (D.obj i) (𝟙 (unop (D.obj i)))) }

Tactic:
dsimp [yonedaLemma]

Result:
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
I : Type v₁
inst✝² : Category.{v₂, v₁} I
D : Iᵒᵖ ⥤ Cᵒᵖ
F : Cᵒᵖ ⥤ Type u₂
inst✝¹ : HasColimit (D.unop ⋙ yoneda)
inst✝ : HasLimitsOfShape Iᵒᵖ (Type (max u₁ u₂))
f : colimit (D.unop ⋙ yoneda) ⟶ F
i : Iᵒᵖ
⊢ Equiv.ulift.symm (yonedaEquiv (colimit.ι (D.unop ⋙ yoneda) (unop i) ≫ f)) =
    { down := f.app (D.obj i) ((colimit.ι (D.unop ⋙ yoneda) (unop i)).app (D.obj i) (𝟙 (unop (D.obj i)))) }