case w.h.h
C : Type u₁
inst✝¹ : SmallCategory C
ℰ : Type u₂
inst✝ : Category ℰ
A : C ⥤ ℰ
P₁ P₂ : Cᵒᵖ ⥤ Type u₁
α : P₁ ⟶ P₂
j : (Functor.Elements P₁)ᵒᵖ
T : Cᵒᵖ
f : ((functorToRepresentables P₁).obj j).obj T
⊢ ((coconeOfRepresentable P₁).ι.app j ≫ α).app T f =
    ((coconeOfRepresentable P₂).ι.app ((Functor.op (CategoryOfElements.map α)).obj j)).app T f
C : Type u₁
inst✝¹ : SmallCategory C
ℰ : Type u₂
inst✝ : Category ℰ
A : C ⥤ ℰ
P₁ P₂ : Cᵒᵖ ⥤ Type u₁
α : P₁ ⟶ P₂
j : (Functor.Elements P₁)ᵒᵖ
⊢ (coconeOfRepresentable P₁).ι.app j ≫ α =
    (coconeOfRepresentable P₂).ι.app ((Functor.op (CategoryOfElements.map α)).obj j)
ext T f
no goals
case w.h.h
C : Type u₁
inst✝¹ : SmallCategory C
ℰ : Type u₂
inst✝ : Category ℰ
A : C ⥤ ℰ
P₁ P₂ : Cᵒᵖ ⥤ Type u₁
α : P₁ ⟶ P₂
j : (Functor.Elements P₁)ᵒᵖ
T : Cᵒᵖ
f : ((functorToRepresentables P₁).obj j).obj T
⊢ ((coconeOfRepresentable P₁).ι.app j ≫ α).app T f =
    ((coconeOfRepresentable P₂).ι.app ((Functor.op (CategoryOfElements.map α)).obj j)).app T f
simpa [coconeOfRepresentable_ι_app] using FunctorToTypes.naturality _ _ α f.op _