J K : Type v
inst✝¹⁰ : SmallCategory J
inst✝⁹ : SmallCategory K
F✝ : J × K ⥤ Type v
inst✝⁸ : IsFiltered K
inst✝⁷ : FinCategory J
C : Type u
inst✝⁶ : Category C
inst✝⁵ : ConcreteCategory C
inst✝⁴ : HasLimitsOfShape J C
inst✝³ : HasColimitsOfShape K C
inst✝² : ReflectsLimitsOfShape J (forget C)
inst✝¹ : PreservesColimitsOfShape K (forget C)
inst✝ : PreservesLimitsOfShape J (forget C)
F : J ⥤ K ⥤ C
a : K
b : J
⊢ colimit.ι (limit F) a ≫
      ((IsLimit.conePointUniqueUpToIso (isLimitOfPreserves colim (limit.isLimit F)) (limit.isLimit (F ⋙ colim))).hom ≫
          (HasLimit.isoOfNatIso (colimitFlipIsoCompColim F).symm).hom) ≫
        limit.π (colimit (Functor.flip F)) b =
    (limit.π F b).app a ≫ (colimit.ι (Functor.flip F) a).app b
J K : Type v
inst✝¹⁰ : SmallCategory J
inst✝⁹ : SmallCategory K
F✝ : J × K ⥤ Type v
inst✝⁸ : IsFiltered K
inst✝⁷ : FinCategory J
C : Type u
inst✝⁶ : Category C
inst✝⁵ : ConcreteCategory C
inst✝⁴ : HasLimitsOfShape J C
inst✝³ : HasColimitsOfShape K C
inst✝² : ReflectsLimitsOfShape J (forget C)
inst✝¹ : PreservesColimitsOfShape K (forget C)
inst✝ : PreservesLimitsOfShape J (forget C)
F : J ⥤ K ⥤ C
a : K
b : J
⊢ colimit.ι (limit F) a ≫ (colimitLimitIso F).hom ≫ limit.π (colimit (Functor.flip F)) b =
    (limit.π F b).app a ≫ (colimit.ι (Functor.flip F) a).app b
dsimp [colimitLimitIso]
J K : Type v
inst✝¹⁰ : SmallCategory J
inst✝⁹ : SmallCategory K
F✝ : J × K ⥤ Type v
inst✝⁸ : IsFiltered K
inst✝⁷ : FinCategory J
C : Type u
inst✝⁶ : Category C
inst✝⁵ : ConcreteCategory C
inst✝⁴ : HasLimitsOfShape J C
inst✝³ : HasColimitsOfShape K C
inst✝² : ReflectsLimitsOfShape J (forget C)
inst✝¹ : PreservesColimitsOfShape K (forget C)
inst✝ : PreservesLimitsOfShape J (forget C)
F : J ⥤ K ⥤ C
a : K
b : J
⊢ (limit.π F b).app a ≫
      colimit.ι (F.obj b) a ≫
        (HasColimit.isoOfNatIso (flipCompEvaluation F b)).inv ≫
          (colimitObjIsoColimitCompEvaluation (Functor.flip F) b).inv =
    (limit.π F b).app a ≫ (colimit.ι (Functor.flip F) a).app b
J K : Type v
inst✝¹⁰ : SmallCategory J
inst✝⁹ : SmallCategory K
F✝ : J × K ⥤ Type v
inst✝⁸ : IsFiltered K
inst✝⁷ : FinCategory J
C : Type u
inst✝⁶ : Category C
inst✝⁵ : ConcreteCategory C
inst✝⁴ : HasLimitsOfShape J C
inst✝³ : HasColimitsOfShape K C
inst✝² : ReflectsLimitsOfShape J (forget C)
inst✝¹ : PreservesColimitsOfShape K (forget C)
inst✝ : PreservesLimitsOfShape J (forget C)
F : J ⥤ K ⥤ C
a : K
b : J
⊢ colimit.ι (limit F) a ≫
      ((IsLimit.conePointUniqueUpToIso (isLimitOfPreserves colim (limit.isLimit F)) (limit.isLimit (F ⋙ colim))).hom ≫
          (HasLimit.isoOfNatIso (colimitFlipIsoCompColim F).symm).hom) ≫
        limit.π (colimit (Functor.flip F)) b =
    (limit.π F b).app a ≫ (colimit.ι (Functor.flip F) a).app b
simp only [Functor.mapCone_π_app, Iso.symm_hom,
  Limits.limit.conePointUniqueUpToIso_hom_comp_assoc, Limits.limit.cone_π,
  Limits.colimit.ι_map_assoc, Limits.colimitFlipIsoCompColim_inv_app, assoc,
  Limits.HasLimit.isoOfNatIso_hom_π]
case e_a
J K : Type v
inst✝¹⁰ : SmallCategory J
inst✝⁹ : SmallCategory K
F✝ : J × K ⥤ Type v
inst✝⁸ : IsFiltered K
inst✝⁷ : FinCategory J
C : Type u
inst✝⁶ : Category C
inst✝⁵ : ConcreteCategory C
inst✝⁴ : HasLimitsOfShape J C
inst✝³ : HasColimitsOfShape K C
inst✝² : ReflectsLimitsOfShape J (forget C)
inst✝¹ : PreservesColimitsOfShape K (forget C)
inst✝ : PreservesLimitsOfShape J (forget C)
F : J ⥤ K ⥤ C
a : K
b : J
⊢ colimit.ι (F.obj b) a ≫
      (HasColimit.isoOfNatIso (flipCompEvaluation F b)).inv ≫
        (colimitObjIsoColimitCompEvaluation (Functor.flip F) b).inv =
    (colimit.ι (Functor.flip F) a).app b
J K : Type v
inst✝¹⁰ : SmallCategory J
inst✝⁹ : SmallCategory K
F✝ : J × K ⥤ Type v
inst✝⁸ : IsFiltered K
inst✝⁷ : FinCategory J
C : Type u
inst✝⁶ : Category C
inst✝⁵ : ConcreteCategory C
inst✝⁴ : HasLimitsOfShape J C
inst✝³ : HasColimitsOfShape K C
inst✝² : ReflectsLimitsOfShape J (forget C)
inst✝¹ : PreservesColimitsOfShape K (forget C)
inst✝ : PreservesLimitsOfShape J (forget C)
F : J ⥤ K ⥤ C
a : K
b : J
⊢ (limit.π F b).app a ≫
      colimit.ι (F.obj b) a ≫
        (HasColimit.isoOfNatIso (flipCompEvaluation F b)).inv ≫
          (colimitObjIsoColimitCompEvaluation (Functor.flip F) b).inv =
    (limit.π F b).app a ≫ (colimit.ι (Functor.flip F) a).app b
congr 1
case e_a
J K : Type v
inst✝¹⁰ : SmallCategory J
inst✝⁹ : SmallCategory K
F✝ : J × K ⥤ Type v
inst✝⁸ : IsFiltered K
inst✝⁷ : FinCategory J
C : Type u
inst✝⁶ : Category C
inst✝⁵ : ConcreteCategory C
inst✝⁴ : HasLimitsOfShape J C
inst✝³ : HasColimitsOfShape K C
inst✝² : ReflectsLimitsOfShape J (forget C)
inst✝¹ : PreservesColimitsOfShape K (forget C)
inst✝ : PreservesLimitsOfShape J (forget C)
F : J ⥤ K ⥤ C
a : K
b : J
⊢ colimit.ι (F.obj b) a = (flipCompEvaluation F b).hom.app a ≫ colimit.ι (F.obj b) a
case e_a
J K : Type v
inst✝¹⁰ : SmallCategory J
inst✝⁹ : SmallCategory K
F✝ : J × K ⥤ Type v
inst✝⁸ : IsFiltered K
inst✝⁷ : FinCategory J
C : Type u
inst✝⁶ : Category C
inst✝⁵ : ConcreteCategory C
inst✝⁴ : HasLimitsOfShape J C
inst✝³ : HasColimitsOfShape K C
inst✝² : ReflectsLimitsOfShape J (forget C)
inst✝¹ : PreservesColimitsOfShape K (forget C)
inst✝ : PreservesLimitsOfShape J (forget C)
F : J ⥤ K ⥤ C
a : K
b : J
⊢ colimit.ι (F.obj b) a ≫
      (HasColimit.isoOfNatIso (flipCompEvaluation F b)).inv ≫
        (colimitObjIsoColimitCompEvaluation (Functor.flip F) b).inv =
    (colimit.ι (Functor.flip F) a).app b
simp only [← Category.assoc, Iso.comp_inv_eq,
  Limits.colimitObjIsoColimitCompEvaluation_ι_app_hom,
  Limits.HasColimit.isoOfNatIso_ι_hom, NatIso.ofComponents_hom_app]
case e_a
J K : Type v
inst✝¹⁰ : SmallCategory J
inst✝⁹ : SmallCategory K
F✝ : J × K ⥤ Type v
inst✝⁸ : IsFiltered K
inst✝⁷ : FinCategory J
C : Type u
inst✝⁶ : Category C
inst✝⁵ : ConcreteCategory C
inst✝⁴ : HasLimitsOfShape J C
inst✝³ : HasColimitsOfShape K C
inst✝² : ReflectsLimitsOfShape J (forget C)
inst✝¹ : PreservesColimitsOfShape K (forget C)
inst✝ : PreservesLimitsOfShape J (forget C)
F : J ⥤ K ⥤ C
a : K
b : J
⊢ colimit.ι (F.obj b) a = 𝟙 ((F.obj b).obj a) ≫ colimit.ι (F.obj b) a
case e_a
J K : Type v
inst✝¹⁰ : SmallCategory J
inst✝⁹ : SmallCategory K
F✝ : J × K ⥤ Type v
inst✝⁸ : IsFiltered K
inst✝⁷ : FinCategory J
C : Type u
inst✝⁶ : Category C
inst✝⁵ : ConcreteCategory C
inst✝⁴ : HasLimitsOfShape J C
inst✝³ : HasColimitsOfShape K C
inst✝² : ReflectsLimitsOfShape J (forget C)
inst✝¹ : PreservesColimitsOfShape K (forget C)
inst✝ : PreservesLimitsOfShape J (forget C)
F : J ⥤ K ⥤ C
a : K
b : J
⊢ colimit.ι (F.obj b) a = (flipCompEvaluation F b).hom.app a ≫ colimit.ι (F.obj b) a
dsimp
no goals
case e_a
J K : Type v
inst✝¹⁰ : SmallCategory J
inst✝⁹ : SmallCategory K
F✝ : J × K ⥤ Type v
inst✝⁸ : IsFiltered K
inst✝⁷ : FinCategory J
C : Type u
inst✝⁶ : Category C
inst✝⁵ : ConcreteCategory C
inst✝⁴ : HasLimitsOfShape J C
inst✝³ : HasColimitsOfShape K C
inst✝² : ReflectsLimitsOfShape J (forget C)
inst✝¹ : PreservesColimitsOfShape K (forget C)
inst✝ : PreservesLimitsOfShape J (forget C)
F : J ⥤ K ⥤ C
a : K
b : J
⊢ colimit.ι (F.obj b) a = 𝟙 ((F.obj b).obj a) ≫ colimit.ι (F.obj b) a
simp