[GOAL]
C : Type u
inst✝⁶ : Category.{v₁, u} C
D : Type u₂
inst✝⁵ : Category.{u, u₂} D
E : Type u
inst✝⁴ : Category.{v₂, u} E
inst✝³ : HasBinaryProducts D
inst✝² : HasColimits D
inst✝¹ : (X : D) → PreservesColimits (prod.functor.obj X)
F : C ⥤ D
J : Type u
inst✝ : Category.{u, u} J
K : J ⥤ C ⥤ D
c : Cocone K
t : IsColimit c
⊢ IsColimit ((prod.functor.obj F).mapCocone c)
[PROOFSTEP]
apply evaluationJointlyReflectsColimits _ fun {k} => ?_
[GOAL]
C : Type u
inst✝⁶ : Category.{v₁, u} C
D : Type u₂
inst✝⁵ : Category.{u, u₂} D
E : Type u
inst✝⁴ : Category.{v₂, u} E
inst✝³ : HasBinaryProducts D
inst✝² : HasColimits D
inst✝¹ : (X : D) → PreservesColimits (prod.functor.obj X)
F : C ⥤ D
J : Type u
inst✝ : Category.{u, u} J
K : J ⥤ C ⥤ D
c : Cocone K
t : IsColimit c
k : C
⊢ IsColimit (((evaluation C D).obj k).mapCocone ((prod.functor.obj F).mapCocone c))
[PROOFSTEP]
change IsColimit ((prod.functor.obj F ⋙ (evaluation _ _).obj k).mapCocone c)
[GOAL]
C : Type u
inst✝⁶ : Category.{v₁, u} C
D : Type u₂
inst✝⁵ : Category.{u, u₂} D
E : Type u
inst✝⁴ : Category.{v₂, u} E
inst✝³ : HasBinaryProducts D
inst✝² : HasColimits D
inst✝¹ : (X : D) → PreservesColimits (prod.functor.obj X)
F : C ⥤ D
J : Type u
inst✝ : Category.{u, u} J
K : J ⥤ C ⥤ D
c : Cocone K
t : IsColimit c
k : C
⊢ IsColimit ((prod.functor.obj F ⋙ (evaluation C D).obj k).mapCocone c)
[PROOFSTEP]
let this := isColimitOfPreserves ((evaluation C D).obj k ⋙ prod.functor.obj (F.obj k)) t
[GOAL]
C : Type u
inst✝⁶ : Category.{v₁, u} C
D : Type u₂
inst✝⁵ : Category.{u, u₂} D
E : Type u
inst✝⁴ : Category.{v₂, u} E
inst✝³ : HasBinaryProducts D
inst✝² : HasColimits D
inst✝¹ : (X : D) → PreservesColimits (prod.functor.obj X)
F : C ⥤ D
J : Type u
inst✝ : Category.{u, u} J
K : J ⥤ C ⥤ D
c : Cocone K
t : IsColimit c
k : C
this : IsColimit (((evaluation C D).obj k ⋙ prod.functor.obj (F.obj k)).mapCocone c) :=
  isColimitOfPreserves ((evaluation C D).obj k ⋙ prod.functor.obj (F.obj k)) t
⊢ IsColimit ((prod.functor.obj F ⋙ (evaluation C D).obj k).mapCocone c)
[PROOFSTEP]
apply IsColimit.mapCoconeEquiv _ this
[GOAL]
C : Type u
inst✝⁶ : Category.{v₁, u} C
D : Type u₂
inst✝⁵ : Category.{u, u₂} D
E : Type u
inst✝⁴ : Category.{v₂, u} E
inst✝³ : HasBinaryProducts D
inst✝² : HasColimits D
inst✝¹ : (X : D) → PreservesColimits (prod.functor.obj X)
F : C ⥤ D
J : Type u
inst✝ : Category.{u, u} J
K : J ⥤ C ⥤ D
c : Cocone K
t : IsColimit c
k : C
this : IsColimit (((evaluation C D).obj k ⋙ prod.functor.obj (F.obj k)).mapCocone c) :=
  isColimitOfPreserves ((evaluation C D).obj k ⋙ prod.functor.obj (F.obj k)) t
⊢ (evaluation C D).obj k ⋙ prod.functor.obj (F.obj k) ≅ prod.functor.obj F ⋙ (evaluation C D).obj k
[PROOFSTEP]
apply (NatIso.ofComponents _ _).symm
[GOAL]
C : Type u
inst✝⁶ : Category.{v₁, u} C
D : Type u₂
inst✝⁵ : Category.{u, u₂} D
E : Type u
inst✝⁴ : Category.{v₂, u} E
inst✝³ : HasBinaryProducts D
inst✝² : HasColimits D
inst✝¹ : (X : D) → PreservesColimits (prod.functor.obj X)
F : C ⥤ D
J : Type u
inst✝ : Category.{u, u} J
K : J ⥤ C ⥤ D
c : Cocone K
t : IsColimit c
k : C
this : IsColimit (((evaluation C D).obj k ⋙ prod.functor.obj (F.obj k)).mapCocone c) :=
  isColimitOfPreserves ((evaluation C D).obj k ⋙ prod.functor.obj (F.obj k)) t
⊢ (X : C ⥤ D) →
    (prod.functor.obj F ⋙ (evaluation C D).obj k).obj X ≅ ((evaluation C D).obj k ⋙ prod.functor.obj (F.obj k)).obj X
[PROOFSTEP]
intro G
[GOAL]
C : Type u
inst✝⁶ : Category.{v₁, u} C
D : Type u₂
inst✝⁵ : Category.{u, u₂} D
E : Type u
inst✝⁴ : Category.{v₂, u} E
inst✝³ : HasBinaryProducts D
inst✝² : HasColimits D
inst✝¹ : (X : D) → PreservesColimits (prod.functor.obj X)
F : C ⥤ D
J : Type u
inst✝ : Category.{u, u} J
K : J ⥤ C ⥤ D
c : Cocone K
t : IsColimit c
k : C
this : IsColimit (((evaluation C D).obj k ⋙ prod.functor.obj (F.obj k)).mapCocone c) :=
  isColimitOfPreserves ((evaluation C D).obj k ⋙ prod.functor.obj (F.obj k)) t
G : C ⥤ D
⊢ (prod.functor.obj F ⋙ (evaluation C D).obj k).obj G ≅ ((evaluation C D).obj k ⋙ prod.functor.obj (F.obj k)).obj G
[PROOFSTEP]
apply asIso (prodComparison ((evaluation C D).obj k) F G)
[GOAL]
C : Type u
inst✝⁶ : Category.{v₁, u} C
D : Type u₂
inst✝⁵ : Category.{u, u₂} D
E : Type u
inst✝⁴ : Category.{v₂, u} E
inst✝³ : HasBinaryProducts D
inst✝² : HasColimits D
inst✝¹ : (X : D) → PreservesColimits (prod.functor.obj X)
F : C ⥤ D
J : Type u
inst✝ : Category.{u, u} J
K : J ⥤ C ⥤ D
c : Cocone K
t : IsColimit c
k : C
this : IsColimit (((evaluation C D).obj k ⋙ prod.functor.obj (F.obj k)).mapCocone c) :=
  isColimitOfPreserves ((evaluation C D).obj k ⋙ prod.functor.obj (F.obj k)) t
⊢ ∀ {X Y : C ⥤ D} (f : X ⟶ Y),
    (prod.functor.obj F ⋙ (evaluation C D).obj k).map f ≫ (asIso (prodComparison ((evaluation C D).obj k) F Y)).hom =
      (asIso (prodComparison ((evaluation C D).obj k) F X)).hom ≫
        ((evaluation C D).obj k ⋙ prod.functor.obj (F.obj k)).map f
[PROOFSTEP]
intro G G'
[GOAL]
C : Type u
inst✝⁶ : Category.{v₁, u} C
D : Type u₂
inst✝⁵ : Category.{u, u₂} D
E : Type u
inst✝⁴ : Category.{v₂, u} E
inst✝³ : HasBinaryProducts D
inst✝² : HasColimits D
inst✝¹ : (X : D) → PreservesColimits (prod.functor.obj X)
F : C ⥤ D
J : Type u
inst✝ : Category.{u, u} J
K : J ⥤ C ⥤ D
c : Cocone K
t : IsColimit c
k : C
this : IsColimit (((evaluation C D).obj k ⋙ prod.functor.obj (F.obj k)).mapCocone c) :=
  isColimitOfPreserves ((evaluation C D).obj k ⋙ prod.functor.obj (F.obj k)) t
G G' : C ⥤ D
⊢ ∀ (f : G ⟶ G'),
    (prod.functor.obj F ⋙ (evaluation C D).obj k).map f ≫ (asIso (prodComparison ((evaluation C D).obj k) F G')).hom =
      (asIso (prodComparison ((evaluation C D).obj k) F G)).hom ≫
        ((evaluation C D).obj k ⋙ prod.functor.obj (F.obj k)).map f
[PROOFSTEP]
apply prodComparison_natural ((evaluation C D).obj k) (𝟙 F)
[GOAL]
C : Type u
inst✝³ : Category.{v₁, u} C
D : Type u₂
inst✝² : Category.{u, u₂} D
E : Type u
inst✝¹ : Category.{v₂, u} E
inst✝ : HasLimits D
F : C ⥤ E
J : Type u
hJ : Category.{u, u} J
K : J ⥤ E ⥤ D
c : Cone K
hc : IsLimit c
⊢ IsLimit (((whiskeringLeft C E D).obj F).mapCone c)
[PROOFSTEP]
apply evaluationJointlyReflectsLimits
[GOAL]
case t
C : Type u
inst✝³ : Category.{v₁, u} C
D : Type u₂
inst✝² : Category.{u, u₂} D
E : Type u
inst✝¹ : Category.{v₂, u} E
inst✝ : HasLimits D
F : C ⥤ E
J : Type u
hJ : Category.{u, u} J
K : J ⥤ E ⥤ D
c : Cone K
hc : IsLimit c
⊢ (k : C) → IsLimit (((evaluation C D).obj k).mapCone (((whiskeringLeft C E D).obj F).mapCone c))
[PROOFSTEP]
intro Y
[GOAL]
case t
C : Type u
inst✝³ : Category.{v₁, u} C
D : Type u₂
inst✝² : Category.{u, u₂} D
E : Type u
inst✝¹ : Category.{v₂, u} E
inst✝ : HasLimits D
F : C ⥤ E
J : Type u
hJ : Category.{u, u} J
K : J ⥤ E ⥤ D
c : Cone K
hc : IsLimit c
Y : C
⊢ IsLimit (((evaluation C D).obj Y).mapCone (((whiskeringLeft C E D).obj F).mapCone c))
[PROOFSTEP]
change IsLimit (((evaluation E D).obj (F.obj Y)).mapCone c)
[GOAL]
case t
C : Type u
inst✝³ : Category.{v₁, u} C
D : Type u₂
inst✝² : Category.{u, u₂} D
E : Type u
inst✝¹ : Category.{v₂, u} E
inst✝ : HasLimits D
F : C ⥤ E
J : Type u
hJ : Category.{u, u} J
K : J ⥤ E ⥤ D
c : Cone K
hc : IsLimit c
Y : C
⊢ IsLimit (((evaluation E D).obj (F.obj Y)).mapCone c)
[PROOFSTEP]
exact PreservesLimit.preserves hc
[GOAL]
C✝ : Type u
inst✝⁸ : Category.{v₁, u} C✝
D✝ : Type u₂
inst✝⁷ : Category.{u, u₂} D✝
E✝ : Type u
inst✝⁶ : Category.{v₂, u} E✝
C : Type u
inst✝⁵ : Category.{?u.25923, u} C
D : Type u_1
inst✝⁴ : Category.{u, u_1} D
E : Type u_2
inst✝³ : Category.{u, u_2} E
J : Type u
inst✝² : SmallCategory J
inst✝¹ : HasLimitsOfShape J D
F : D ⥤ E
inst✝ : PreservesLimitsOfShape J F
K : J ⥤ C ⥤ D
c : Cone K
hc : IsLimit c
⊢ IsLimit (((whiskeringRight C D E).obj F).mapCone c)
[PROOFSTEP]
apply evaluationJointlyReflectsLimits _ (fun k => ?_)
[GOAL]
C✝ : Type u
inst✝⁸ : Category.{v₁, u} C✝
D✝ : Type u₂
inst✝⁷ : Category.{u, u₂} D✝
E✝ : Type u
inst✝⁶ : Category.{v₂, u} E✝
C : Type u
inst✝⁵ : Category.{?u.25923, u} C
D : Type u_1
inst✝⁴ : Category.{u, u_1} D
E : Type u_2
inst✝³ : Category.{u, u_2} E
J : Type u
inst✝² : SmallCategory J
inst✝¹ : HasLimitsOfShape J D
F : D ⥤ E
inst✝ : PreservesLimitsOfShape J F
K : J ⥤ C ⥤ D
c : Cone K
hc : IsLimit c
k : C
⊢ IsLimit (((evaluation C E).obj k).mapCone (((whiskeringRight C D E).obj F).mapCone c))
[PROOFSTEP]
change IsLimit (((evaluation _ _).obj k ⋙ F).mapCone c)
[GOAL]
C✝ : Type u
inst✝⁸ : Category.{v₁, u} C✝
D✝ : Type u₂
inst✝⁷ : Category.{u, u₂} D✝
E✝ : Type u
inst✝⁶ : Category.{v₂, u} E✝
C : Type u
inst✝⁵ : Category.{?u.25923, u} C
D : Type u_1
inst✝⁴ : Category.{u, u_1} D
E : Type u_2
inst✝³ : Category.{u, u_2} E
J : Type u
inst✝² : SmallCategory J
inst✝¹ : HasLimitsOfShape J D
F : D ⥤ E
inst✝ : PreservesLimitsOfShape J F
K : J ⥤ C ⥤ D
c : Cone K
hc : IsLimit c
k : C
⊢ IsLimit (((evaluation C D).obj k ⋙ F).mapCone c)
[PROOFSTEP]
exact PreservesLimit.preserves hc
[GOAL]
C✝ : Type u
inst✝⁶ : Category.{v₁, u} C✝
D✝ : Type u₂
inst✝⁵ : Category.{u, u₂} D✝
E : Type u
inst✝⁴ : Category.{v₂, u} E
C D : Type u
inst✝³ : SmallCategory C
inst✝² : SmallCategory D
F : C ⥤ D
J : Type u
inst✝¹ : SmallCategory J
inst✝ : PreservesLimitsOfShape J (lan F.op)
⊢ PreservesLimitsOfShape J F
[PROOFSTEP]
apply @preservesLimitsOfShapeOfReflectsOfPreserves _ _ _ _ _ _ _ _ F yoneda ?_
[GOAL]
C✝ : Type u
inst✝⁶ : Category.{v₁, u} C✝
D✝ : Type u₂
inst✝⁵ : Category.{u, u₂} D✝
E : Type u
inst✝⁴ : Category.{v₂, u} E
C D : Type u
inst✝³ : SmallCategory C
inst✝² : SmallCategory D
F : C ⥤ D
J : Type u
inst✝¹ : SmallCategory J
inst✝ : PreservesLimitsOfShape J (lan F.op)
⊢ PreservesLimitsOfShape J (F ⋙ yoneda)
[PROOFSTEP]
exact preservesLimitsOfShapeOfNatIso (compYonedaIsoYonedaCompLan F).symm
