-- Mathlib/CategoryTheory/Limits/IndYoneda.lean
@[simp]
lemma colimitYonedaHomIsoLimit'_π_apply (f : colimit (D.leftOp ⋙ yoneda) ⟶ F) (i : I) :
    limit.π (D ⋙ F ⋙ uliftFunctor.{u₁}) i ((colimitYonedaHomIsoLimit' D F).hom f) =
      ⟨f.app (D.obj i)
        ((colimit.ι (D.leftOp ⋙ yoneda) (op i)).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.leftOp ⋙ yoneda)
inst✝ : HasLimitsOfShape I (Type (max u₁ u₂))
f : colimit (D.leftOp ⋙ yoneda) ⟶ F
i : I
⊢ ((coyoneda.map (colimit.ι (D.leftOp ⋙ yoneda) (op i)).op).app F ≫
        (isoWhiskerLeft (D ⋙ Prod.sectL Cᵒᵖ F) (yonedaLemma C)).hom.app i)
      f =
    { down := f.app (D.obj i) ((colimit.ι (D.leftOp ⋙ yoneda) (op 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.leftOp ⋙ yoneda)
inst✝ : HasLimitsOfShape I (Type (max u₁ u₂))
f : colimit (D.leftOp ⋙ yoneda) ⟶ F
i : I
⊢ Equiv.ulift.symm (yonedaEquiv (colimit.ι (D.leftOp ⋙ yoneda) (op i) ≫ f)) =
    { down := f.app (D.obj i) ((colimit.ι (D.leftOp ⋙ yoneda) (op 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.leftOp ⋙ yoneda)
inst✝ : HasLimitsOfShape I (Type (max u₁ u₂))
f : colimit (D.leftOp ⋙ yoneda) ⟶ F
i : I
⊢ ((colimitHomIsoLimitYoneda' (D.leftOp ⋙ yoneda) F).hom ≫
        limit.π ((D.leftOp ⋙ yoneda).rightOp ⋙ yoneda.obj F) i ≫
          (isoWhiskerLeft (D ⋙ Prod.sectL Cᵒᵖ F) (yonedaLemma C)).hom.app i)
      f =
    { down := f.app (D.obj i) ((colimit.ι (D.leftOp ⋙ yoneda) (op 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.leftOp ⋙ yoneda)
inst✝ : HasLimitsOfShape I (Type (max u₁ u₂))
f : colimit (D.leftOp ⋙ yoneda) ⟶ F
i : I
⊢ ((coyoneda.map (colimit.ι (D.leftOp ⋙ yoneda) (op i)).op).app F ≫
        (isoWhiskerLeft (D ⋙ Prod.sectL Cᵒᵖ F) (yonedaLemma C)).hom.app i)
      f =
    { down := f.app (D.obj i) ((colimit.ι (D.leftOp ⋙ yoneda) (op 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.leftOp ⋙ yoneda)
inst✝ : HasLimitsOfShape I (Type (max u₁ u₂))
f : colimit (D.leftOp ⋙ yoneda) ⟶ F
i : I
⊢ limit.π (D ⋙ F ⋙ uliftFunctor.{u₁, u₂}) i ((colimitYonedaHomIsoLimit' D F).hom f) =
    { down := f.app (D.obj i) ((colimit.ι (D.leftOp ⋙ yoneda) (op 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.leftOp ⋙ yoneda)
inst✝ : HasLimitsOfShape I (Type (max u₁ u₂))
f : colimit (D.leftOp ⋙ yoneda) ⟶ F
i : I
⊢ ((colimitYonedaHomIsoLimit' D F).hom ≫ limit.π (D ⋙ F ⋙ uliftFunctor.{u₁, u₂}) i) f =
    { down := f.app (D.obj i) ((colimit.ι (D.leftOp ⋙ yoneda) (op 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.leftOp ⋙ yoneda)
inst✝ : HasLimitsOfShape I (Type (max u₁ u₂))
f : colimit (D.leftOp ⋙ yoneda) ⟶ F
i : I
⊢ Equiv.ulift.symm (yonedaEquiv (colimit.ι (D.leftOp ⋙ yoneda) (op i) ≫ f)) =
    { down := f.app (D.obj i) ((colimit.ι (D.leftOp ⋙ yoneda) (op 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.leftOp ⋙ yoneda)
inst✝ : HasLimitsOfShape I (Type (max u₁ u₂))
f : colimit (D.leftOp ⋙ yoneda) ⟶ F
i : I
⊢ Equiv.ulift.symm
      (f.app (op (unop (D.obj i)))
        ((colimit.ι (D.leftOp ⋙ yoneda) (op i)).app (op (unop (D.obj i))) (𝟙 (unop (D.obj i))))) =
    { down := f.app (D.obj i) ((colimit.ι (D.leftOp ⋙ yoneda) (op 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.leftOp ⋙ yoneda)
inst✝ : HasLimitsOfShape I (Type (max u₁ u₂))
f : colimit (D.leftOp ⋙ yoneda) ⟶ F
i : I
⊢ ((colimitYonedaHomIsoLimit' D F).hom ≫ limit.π (D ⋙ F ⋙ uliftFunctor.{u₁, u₂}) i) f =
    { down := f.app (D.obj i) ((colimit.ι (D.leftOp ⋙ yoneda) (op 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.leftOp ⋙ yoneda)
inst✝ : HasLimitsOfShape I (Type (max u₁ u₂))
f : colimit (D.leftOp ⋙ yoneda) ⟶ F
i : I
⊢ ((colimitHomIsoLimitYoneda' (D.leftOp ⋙ yoneda) F).hom ≫
        limit.π ((D.leftOp ⋙ yoneda).rightOp ⋙ yoneda.obj F) i ≫
          (isoWhiskerLeft (D ⋙ Prod.sectL Cᵒᵖ F) (yonedaLemma C)).hom.app i)
      f =
    { down := f.app (D.obj i) ((colimit.ι (D.leftOp ⋙ yoneda) (op 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.leftOp ⋙ yoneda)
inst✝ : HasLimitsOfShape I (Type (max u₁ u₂))
f : colimit (D.leftOp ⋙ yoneda) ⟶ F
i : I
⊢ Equiv.ulift.symm
      (f.app (op (unop (D.obj i)))
        ((colimit.ι (D.leftOp ⋙ yoneda) (op i)).app (op (unop (D.obj i))) (𝟙 (unop (D.obj i))))) =
    { down := f.app (D.obj i) ((colimit.ι (D.leftOp ⋙ yoneda) (op i)).app (D.obj i) (𝟙 (unop (D.obj i)))) }

Tactic:
rfl

Result:
no goals