-- Mathlib/CategoryTheory/Limits/FilteredColimitCommutesFiniteLimit.lean
theorem ι_colimitLimitIso_limit_π (F : J ⥤ K ⥤ C) (a) (b) :
    colimit.ι (limit F) a ≫ (colimitLimitIso F).hom ≫ limit.π (colimit F.flip) b =
      (limit.π F b).app a ≫ (colimit.ι F.flip a).app b

Proof state:
C : Type u
inst✝⁵ : Category.{v, u} C
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
inst✝² : HasLimitsOfShape J C
inst✝¹ : HasColimitsOfShape K C
inst✝ : PreservesLimitsOfShape J colim
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 F.flip b).inv =
    (limit.π F b).app a ≫ (colimit.ι F.flip a).app b

Tactic:
congr 1

Result:
case e_a
C : Type u
inst✝⁵ : Category.{v, u} C
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
inst✝² : HasLimitsOfShape J C
inst✝¹ : HasColimitsOfShape K C
inst✝ : PreservesLimitsOfShape J colim
F : J ⥤ K ⥤ C
a : K
b : J
⊢ colimit.ι (F.obj b) a ≫
      (HasColimit.isoOfNatIso (flipCompEvaluation F b)).inv ≫ (colimitObjIsoColimitCompEvaluation F.flip b).inv =
    (colimit.ι F.flip a).app b

Proof state:
case e_a
C : Type u
inst✝⁵ : Category.{v, u} C
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
inst✝² : HasLimitsOfShape J C
inst✝¹ : HasColimitsOfShape K C
inst✝ : PreservesLimitsOfShape J colim
F : J ⥤ K ⥤ C
a : K
b : J
⊢ colimit.ι (F.obj b) a ≫
      (HasColimit.isoOfNatIso (flipCompEvaluation F b)).inv ≫ (colimitObjIsoColimitCompEvaluation F.flip b).inv =
    (colimit.ι F.flip a).app b

Tactic:
simp only [← Category.assoc, Iso.comp_inv_eq,
  Limits.colimitObjIsoColimitCompEvaluation_ι_app_hom,
  Limits.HasColimit.isoOfNatIso_ι_hom, NatIso.ofComponents_hom_app]

Result:
case e_a
C : Type u
inst✝⁵ : Category.{v, u} C
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
inst✝² : HasLimitsOfShape J C
inst✝¹ : HasColimitsOfShape K C
inst✝ : PreservesLimitsOfShape J colim
F : J ⥤ K ⥤ C
a : K
b : J
⊢ colimit.ι (F.obj b) a = (flipCompEvaluation F b).hom.app a ≫ colimit.ι (F.obj b) a

Proof state:
C : Type u
inst✝⁵ : Category.{v, u} C
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
inst✝² : HasLimitsOfShape J C
inst✝¹ : HasColimitsOfShape K C
inst✝ : PreservesLimitsOfShape J colim
F : J ⥤ K ⥤ C
a : K
b : J
⊢ colimit.ι (limit F) a ≫
      (((isLimitOfPreserves colim (limit.isLimit F)).conePointUniqueUpToIso (limit.isLimit (F ⋙ colim))).hom ≫
          (HasLimit.isoOfNatIso (colimitFlipIsoCompColim F).symm).hom) ≫
        limit.π (colimit F.flip) b =
    (limit.π F b).app a ≫ (colimit.ι F.flip a).app b

Tactic:
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_π]

Result:
C : Type u
inst✝⁵ : Category.{v, u} C
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
inst✝² : HasLimitsOfShape J C
inst✝¹ : HasColimitsOfShape K C
inst✝ : PreservesLimitsOfShape J colim
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 F.flip b).inv =
    (limit.π F b).app a ≫ (colimit.ι F.flip a).app b

Proof state:
case e_a
C : Type u
inst✝⁵ : Category.{v, u} C
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
inst✝² : HasLimitsOfShape J C
inst✝¹ : HasColimitsOfShape K C
inst✝ : PreservesLimitsOfShape J colim
F : J ⥤ K ⥤ C
a : K
b : J
⊢ colimit.ι (F.obj b) a = 𝟙 ((F.obj b).obj a) ≫ colimit.ι (F.obj b) a

Tactic:
simp

Result:
no goals

Proof state:
C : Type u
inst✝⁵ : Category.{v, u} C
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
inst✝² : HasLimitsOfShape J C
inst✝¹ : HasColimitsOfShape K C
inst✝ : PreservesLimitsOfShape J colim
F : J ⥤ K ⥤ C
a : K
b : J
⊢ colimit.ι (limit F) a ≫ (colimitLimitIso F).hom ≫ limit.π (colimit F.flip) b =
    (limit.π F b).app a ≫ (colimit.ι F.flip a).app b

Tactic:
dsimp [colimitLimitIso]

Result:
C : Type u
inst✝⁵ : Category.{v, u} C
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
inst✝² : HasLimitsOfShape J C
inst✝¹ : HasColimitsOfShape K C
inst✝ : PreservesLimitsOfShape J colim
F : J ⥤ K ⥤ C
a : K
b : J
⊢ colimit.ι (limit F) a ≫
      (((isLimitOfPreserves colim (limit.isLimit F)).conePointUniqueUpToIso (limit.isLimit (F ⋙ colim))).hom ≫
          (HasLimit.isoOfNatIso (colimitFlipIsoCompColim F).symm).hom) ≫
        limit.π (colimit F.flip) b =
    (limit.π F b).app a ≫ (colimit.ι F.flip a).app b

Proof state:
case e_a
C : Type u
inst✝⁵ : Category.{v, u} C
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
inst✝² : HasLimitsOfShape J C
inst✝¹ : HasColimitsOfShape K C
inst✝ : PreservesLimitsOfShape J colim
F : J ⥤ K ⥤ C
a : K
b : J
⊢ colimit.ι (F.obj b) a = (flipCompEvaluation F b).hom.app a ≫ colimit.ι (F.obj b) a

Tactic:
dsimp

Result:
case e_a
C : Type u
inst✝⁵ : Category.{v, u} C
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
inst✝² : HasLimitsOfShape J C
inst✝¹ : HasColimitsOfShape K C
inst✝ : PreservesLimitsOfShape J colim
F : J ⥤ K ⥤ C
a : K
b : J
⊢ colimit.ι (F.obj b) a = 𝟙 ((F.obj b).obj a) ≫ colimit.ι (F.obj b) a