-- Mathlib/CategoryTheory/Limits/IsLimit.lean
theorem coconeOfHom_fac {Y : C} (f : X ⟶ Y) : coconeOfHom h f = (colimitCocone h).extend f

Proof state:
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
X : C
h : coyoneda.obj (op X) ⋙ uliftFunctor.{u₁, v₃} ≅ F.cocones
Y : C
f : X ⟶ Y
⊢ coconeOfHom h f = (colimitCocone h).extend f

Tactic:
dsimp [coconeOfHom, colimitCocone, Cocone.extend]

Result:
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
X : C
h : coyoneda.obj (op X) ⋙ uliftFunctor.{u₁, v₃} ≅ F.cocones
Y : C
f : X ⟶ Y
⊢ { pt := Y, ι := h.hom.app Y { down := f } } = { pt := Y, ι := h.hom.app X { down := 𝟙 X } ≫ (const J).map f }

Proof state:
case e_ι.w.h
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
X : C
h : coyoneda.obj (op X) ⋙ uliftFunctor.{u₁, v₃} ≅ F.cocones
Y : C
f : X ⟶ Y
j : J
⊢ (h.hom.app Y { down := f }).app j = (h.hom.app X { down := 𝟙 X } ≫ (const J).map f).app j

Tactic:
have t := congrFun (h.hom.naturality f) ⟨𝟙 X⟩

Result:
case e_ι.w.h
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
X : C
h : coyoneda.obj (op X) ⋙ uliftFunctor.{u₁, v₃} ≅ F.cocones
Y : C
f : X ⟶ Y
j : J
t :
  ((coyoneda.obj (op X) ⋙ uliftFunctor.{u₁, v₃}).map f ≫ h.hom.app Y) { down := 𝟙 X } =
    (h.hom.app X ≫ F.cocones.map f) { down := 𝟙 X }
⊢ (h.hom.app Y { down := f }).app j = (h.hom.app X { down := 𝟙 X } ≫ (const J).map f).app j

Proof state:
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
X : C
h : coyoneda.obj (op X) ⋙ uliftFunctor.{u₁, v₃} ≅ F.cocones
Y : C
f : X ⟶ Y
⊢ { pt := Y, ι := h.hom.app Y { down := f } } = { pt := Y, ι := h.hom.app X { down := 𝟙 X } ≫ (const J).map f }

Tactic:
congr with j

Result:
case e_ι.w.h
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
X : C
h : coyoneda.obj (op X) ⋙ uliftFunctor.{u₁, v₃} ≅ F.cocones
Y : C
f : X ⟶ Y
j : J
⊢ (h.hom.app Y { down := f }).app j = (h.hom.app X { down := 𝟙 X } ≫ (const J).map f).app j

Proof state:
case e_ι.w.h
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
X : C
h : coyoneda.obj (op X) ⋙ uliftFunctor.{u₁, v₃} ≅ F.cocones
Y : C
f : X ⟶ Y
j : J
t :
  ((coyoneda.obj (op X) ⋙ uliftFunctor.{u₁, v₃}).map f ≫ h.hom.app Y) { down := 𝟙 X } =
    (h.hom.app X ≫ F.cocones.map f) { down := 𝟙 X }
⊢ (h.hom.app Y { down := f }).app j = (h.hom.app X { down := 𝟙 X } ≫ (const J).map f).app j

Tactic:
dsimp at t

Result:
case e_ι.w.h
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
X : C
h : coyoneda.obj (op X) ⋙ uliftFunctor.{u₁, v₃} ≅ F.cocones
Y : C
f : X ⟶ Y
j : J
t : h.hom.app Y { down := 𝟙 X ≫ f } = F.cocones.map f (h.hom.app X { down := 𝟙 X })
⊢ (h.hom.app Y { down := f }).app j = (h.hom.app X { down := 𝟙 X } ≫ (const J).map f).app j

Proof state:
case e_ι.w.h
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
X : C
h : coyoneda.obj (op X) ⋙ uliftFunctor.{u₁, v₃} ≅ F.cocones
Y : C
f : X ⟶ Y
j : J
t : h.hom.app Y { down := f } = F.cocones.map f (h.hom.app X { down := 𝟙 X })
⊢ (F.cocones.map f (h.hom.app X { down := 𝟙 X })).app j = (h.hom.app X { down := 𝟙 X } ≫ (const J).map f).app j

Tactic:
rfl

Result:
no goals

Proof state:
case e_ι.w.h
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
X : C
h : coyoneda.obj (op X) ⋙ uliftFunctor.{u₁, v₃} ≅ F.cocones
Y : C
f : X ⟶ Y
j : J
t : h.hom.app Y { down := f } = F.cocones.map f (h.hom.app X { down := 𝟙 X })
⊢ (h.hom.app Y { down := f }).app j = (h.hom.app X { down := 𝟙 X } ≫ (const J).map f).app j

Tactic:
rw [congrFun (congrArg NatTrans.app t) j]

Result:
case e_ι.w.h
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
X : C
h : coyoneda.obj (op X) ⋙ uliftFunctor.{u₁, v₃} ≅ F.cocones
Y : C
f : X ⟶ Y
j : J
t : h.hom.app Y { down := f } = F.cocones.map f (h.hom.app X { down := 𝟙 X })
⊢ (F.cocones.map f (h.hom.app X { down := 𝟙 X })).app j = (h.hom.app X { down := 𝟙 X } ≫ (const J).map f).app j

Proof state:
case e_ι.w.h
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
X : C
h : coyoneda.obj (op X) ⋙ uliftFunctor.{u₁, v₃} ≅ F.cocones
Y : C
f : X ⟶ Y
j : J
t : h.hom.app Y { down := 𝟙 X ≫ f } = F.cocones.map f (h.hom.app X { down := 𝟙 X })
⊢ (h.hom.app Y { down := f }).app j = (h.hom.app X { down := 𝟙 X } ≫ (const J).map f).app j

Tactic:
simp only [id_comp] at t

Result:
case e_ι.w.h
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
X : C
h : coyoneda.obj (op X) ⋙ uliftFunctor.{u₁, v₃} ≅ F.cocones
Y : C
f : X ⟶ Y
j : J
t : h.hom.app Y { down := f } = F.cocones.map f (h.hom.app X { down := 𝟙 X })
⊢ (h.hom.app Y { down := f }).app j = (h.hom.app X { down := 𝟙 X } ≫ (const J).map f).app j