-- Mathlib/CategoryTheory/Limits/IndYoneda.lean
@[simp]
lemma colimitCoyonedaHomIsoLimit_π_apply (f : colimit (D.rightOp ⋙ coyoneda) ⟶ F) (i : I) :
    limit.π (D ⋙ F ⋙ uliftFunctor.{u₁}) (op i) ((colimitCoyonedaHomIsoLimit D F).hom f) =
      ⟨f.app (D.obj (op i)) ((colimit.ι (D.rightOp ⋙ coyoneda) i).app (D.obj (op i))
          (𝟙 (D.obj (op 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.rightOp ⋙ coyoneda)
inst✝ : HasLimitsOfShape Iᵒᵖ (Type (max u₁ u₂))
f : colimit (D.rightOp ⋙ coyoneda) ⟶ F
i : I
⊢ limit.π (D ⋙ F ⋙ uliftFunctor.{u₁, u₂}) (op i) ((colimitCoyonedaHomIsoLimit D F).hom f) =
    { down := f.app (D.obj (op i)) ((colimit.ι (D.rightOp ⋙ coyoneda) i).app (D.obj (op i)) (𝟙 (D.obj (op i)))) }

Tactic:
change ((colimitCoyonedaHomIsoLimit D F).hom ≫ (limit.π (D ⋙ F ⋙ uliftFunctor.{u₁}) (op 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.rightOp ⋙ coyoneda)
inst✝ : HasLimitsOfShape Iᵒᵖ (Type (max u₁ u₂))
f : colimit (D.rightOp ⋙ coyoneda) ⟶ F
i : I
⊢ ((colimitCoyonedaHomIsoLimit D F).hom ≫ limit.π (D ⋙ F ⋙ uliftFunctor.{u₁, u₂}) (op i)) f =
    { down := f.app (D.obj (op i)) ((colimit.ι (D.rightOp ⋙ coyoneda) i).app (D.obj (op i)) (𝟙 (D.obj (op 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.rightOp ⋙ coyoneda)
inst✝ : HasLimitsOfShape Iᵒᵖ (Type (max u₁ u₂))
f : colimit (D.rightOp ⋙ coyoneda) ⟶ F
i : I
⊢ Equiv.ulift.symm (coyonedaEquiv (colimit.ι (D.rightOp ⋙ coyoneda) i ≫ f)) =
    { down := f.app (D.obj (op i)) ((colimit.ι (D.rightOp ⋙ coyoneda) i).app (D.obj (op i)) (𝟙 (D.obj (op i)))) }

Tactic:
erw [coyonedaEquiv_comp, coyonedaEquiv_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.rightOp ⋙ coyoneda)
inst✝ : HasLimitsOfShape Iᵒᵖ (Type (max u₁ u₂))
f : colimit (D.rightOp ⋙ coyoneda) ⟶ F
i : I
⊢ Equiv.ulift.symm (f.app (D.obj (op i)) ((colimit.ι (D.rightOp ⋙ coyoneda) i).app (D.obj (op i)) (𝟙 (D.obj (op i))))) =
    { down := f.app (D.obj (op i)) ((colimit.ι (D.rightOp ⋙ coyoneda) i).app (D.obj (op i)) (𝟙 (D.obj (op 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.rightOp ⋙ coyoneda)
inst✝ : HasLimitsOfShape Iᵒᵖ (Type (max u₁ u₂))
f : colimit (D.rightOp ⋙ coyoneda) ⟶ F
i : I
⊢ ((colimitCoyonedaHomIsoLimit D F).hom ≫ limit.π (D ⋙ F ⋙ uliftFunctor.{u₁, u₂}) (op i)) f =
    { down := f.app (D.obj (op i)) ((colimit.ι (D.rightOp ⋙ coyoneda) i).app (D.obj (op i)) (𝟙 (D.obj (op i)))) }

Tactic:
simp only [colimitCoyonedaHomIsoLimit, 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.rightOp ⋙ coyoneda)
inst✝ : HasLimitsOfShape Iᵒᵖ (Type (max u₁ u₂))
f : colimit (D.rightOp ⋙ coyoneda) ⟶ F
i : I
⊢ ((colimitHomIsoLimitYoneda (D.rightOp ⋙ coyoneda) F).hom ≫
        limit.π ((D.rightOp ⋙ coyoneda).op ⋙ yoneda.obj F) (op i) ≫
          (isoWhiskerLeft (D ⋙ Prod.sectL C F) (coyonedaLemma C)).hom.app (op i))
      f =
    { down := f.app (D.obj (op i)) ((colimit.ι (D.rightOp ⋙ coyoneda) i).app (D.obj (op i)) (𝟙 (D.obj (op 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.rightOp ⋙ coyoneda)
inst✝ : HasLimitsOfShape Iᵒᵖ (Type (max u₁ u₂))
f : colimit (D.rightOp ⋙ coyoneda) ⟶ F
i : I
⊢ ((coyoneda.map (colimit.ι (D.rightOp ⋙ coyoneda) i).op).app F ≫
        (isoWhiskerLeft (D ⋙ Prod.sectL C F) (coyonedaLemma C)).hom.app (op i))
      f =
    { down := f.app (D.obj (op i)) ((colimit.ι (D.rightOp ⋙ coyoneda) i).app (D.obj (op i)) (𝟙 (D.obj (op i)))) }

Tactic:
dsimp [coyonedaLemma, types_comp_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.rightOp ⋙ coyoneda)
inst✝ : HasLimitsOfShape Iᵒᵖ (Type (max u₁ u₂))
f : colimit (D.rightOp ⋙ coyoneda) ⟶ F
i : I
⊢ Equiv.ulift.symm (coyonedaEquiv (colimit.ι (D.rightOp ⋙ coyoneda) i ≫ f)) =
    { down := f.app (D.obj (op i)) ((colimit.ι (D.rightOp ⋙ coyoneda) i).app (D.obj (op i)) (𝟙 (D.obj (op 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.rightOp ⋙ coyoneda)
inst✝ : HasLimitsOfShape Iᵒᵖ (Type (max u₁ u₂))
f : colimit (D.rightOp ⋙ coyoneda) ⟶ F
i : I
⊢ ((colimitHomIsoLimitYoneda (D.rightOp ⋙ coyoneda) F).hom ≫
        limit.π ((D.rightOp ⋙ coyoneda).op ⋙ yoneda.obj F) (op i) ≫
          (isoWhiskerLeft (D ⋙ Prod.sectL C F) (coyonedaLemma C)).hom.app (op i))
      f =
    { down := f.app (D.obj (op i)) ((colimit.ι (D.rightOp ⋙ coyoneda) i).app (D.obj (op i)) (𝟙 (D.obj (op 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.rightOp ⋙ coyoneda)
inst✝ : HasLimitsOfShape Iᵒᵖ (Type (max u₁ u₂))
f : colimit (D.rightOp ⋙ coyoneda) ⟶ F
i : I
⊢ ((coyoneda.map (colimit.ι (D.rightOp ⋙ coyoneda) i).op).app F ≫
        (isoWhiskerLeft (D ⋙ Prod.sectL C F) (coyonedaLemma C)).hom.app (op i))
      f =
    { down := f.app (D.obj (op i)) ((colimit.ι (D.rightOp ⋙ coyoneda) i).app (D.obj (op i)) (𝟙 (D.obj (op 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.rightOp ⋙ coyoneda)
inst✝ : HasLimitsOfShape Iᵒᵖ (Type (max u₁ u₂))
f : colimit (D.rightOp ⋙ coyoneda) ⟶ F
i : I
⊢ Equiv.ulift.symm (f.app (D.obj (op i)) ((colimit.ι (D.rightOp ⋙ coyoneda) i).app (D.obj (op i)) (𝟙 (D.obj (op i))))) =
    { down := f.app (D.obj (op i)) ((colimit.ι (D.rightOp ⋙ coyoneda) i).app (D.obj (op i)) (𝟙 (D.obj (op i)))) }

Tactic:
rfl

Result:
no goals