-- Mathlib/CategoryTheory/Limits/Fubini.lean
theorem limitCurrySwapCompLimIsoLimitCurryCompLim_hom_π_π {j} {k} :
    (limitCurrySwapCompLimIsoLimitCurryCompLim G).hom ≫ limit.π _ j ≫ limit.π _ k =
      (limit.π _ k ≫ limit.π _ j : limit (_ ⋙ lim) ⟶ _)

Proof state:
J : Type u_1
K : Type u_2
inst✝⁵ : Category.{u_6, u_1} J
inst✝⁴ : Category.{u_5, u_2} K
C : Type u_3
inst✝³ : Category.{u_4, u_3} C
G : J × K ⥤ C
inst✝² : HasLimitsOfShape K C
inst✝¹ : HasLimitsOfShape J C
inst✝ : HasLimit (curry.obj G ⋙ lim)
j : J
k : K
⊢ (limitIsoLimitCurryCompLim (Prod.swap K J ⋙ G)).inv ≫
      limit.π (Prod.swap K J ⋙ G) ((Prod.braiding K J).inverse.obj (j, k)) ≫
        (Iso.refl (Prod.swap K J ⋙ G)).inv.app ((Prod.braiding K J).inverse.obj (j, k)) ≫
          G.map ((Prod.braiding K J).counit.app (j, k)) =
    limit.π (curry.obj (Prod.swap K J ⋙ G) ⋙ lim) k ≫ limit.π ((curry.obj (Prod.swap K J ⋙ G)).obj k) j

Tactic:
dsimp [Equivalence.counit]

Result:
J : Type u_1
K : Type u_2
inst✝⁵ : Category.{u_6, u_1} J
inst✝⁴ : Category.{u_5, u_2} K
C : Type u_3
inst✝³ : Category.{u_4, u_3} C
G : J × K ⥤ C
inst✝² : HasLimitsOfShape K C
inst✝¹ : HasLimitsOfShape J C
inst✝ : HasLimit (curry.obj G ⋙ lim)
j : J
k : K
⊢ (limitIsoLimitCurryCompLim (Prod.swap K J ⋙ G)).inv ≫
      limit.π (Prod.swap K J ⋙ G) (k, j) ≫ 𝟙 (G.obj (j, k)) ≫ G.map (𝟙 j, 𝟙 k) =
    limit.π (curry.obj (Prod.swap K J ⋙ G) ⋙ lim) k ≫ limit.π ((curry.obj (Prod.swap K J ⋙ G)).obj k) j

Proof state:
J : Type u_1
K : Type u_2
inst✝⁵ : Category.{u_6, u_1} J
inst✝⁴ : Category.{u_5, u_2} K
C : Type u_3
inst✝³ : Category.{u_4, u_3} C
G : J × K ⥤ C
inst✝² : HasLimitsOfShape K C
inst✝¹ : HasLimitsOfShape J C
inst✝ : HasLimit (curry.obj G ⋙ lim)
j : J
k : K
⊢ (limitCurrySwapCompLimIsoLimitCurryCompLim G).hom ≫ limit.π (curry.obj G ⋙ lim) j ≫ limit.π ((curry.obj G).obj j) k =
    limit.π (curry.obj (Prod.swap K J ⋙ G) ⋙ lim) k ≫ limit.π ((curry.obj (Prod.swap K J ⋙ G)).obj k) j

Tactic:
dsimp [limitCurrySwapCompLimIsoLimitCurryCompLim, Equivalence.counit]

Result:
J : Type u_1
K : Type u_2
inst✝⁵ : Category.{u_6, u_1} J
inst✝⁴ : Category.{u_5, u_2} K
C : Type u_3
inst✝³ : Category.{u_4, u_3} C
G : J × K ⥤ C
inst✝² : HasLimitsOfShape K C
inst✝¹ : HasLimitsOfShape J C
inst✝ : HasLimit (curry.obj G ⋙ lim)
j : J
k : K
⊢ (((limitIsoLimitCurryCompLim (Prod.swap K J ⋙ G)).inv ≫
          (HasLimit.isoOfEquivalence (Prod.braiding K J) (Iso.refl (Prod.swap K J ⋙ G))).hom) ≫
        (limitIsoLimitCurryCompLim G).hom) ≫
      limit.π (curry.obj G ⋙ lim) j ≫ limit.π ((curry.obj G).obj j) k =
    limit.π (curry.obj (Prod.swap K J ⋙ G) ⋙ lim) k ≫ limit.π ((curry.obj (Prod.swap K J ⋙ G)).obj k) j

Proof state:
J : Type u_1
K : Type u_2
inst✝⁵ : Category.{u_6, u_1} J
inst✝⁴ : Category.{u_5, u_2} K
C : Type u_3
inst✝³ : Category.{u_4, u_3} C
G : J × K ⥤ C
inst✝² : HasLimitsOfShape K C
inst✝¹ : HasLimitsOfShape J C
inst✝ : HasLimit (curry.obj G ⋙ lim)
j : J
k : K
⊢ (limitIsoLimitCurryCompLim (Prod.swap K J ⋙ G)).inv ≫
      limit.π (Prod.swap K J ⋙ G) (k, j) ≫ 𝟙 (G.obj (j, k)) ≫ 𝟙 (G.obj (j, k)) =
    limit.π (curry.obj (Prod.swap K J ⋙ G) ⋙ lim) k ≫ limit.π ((curry.obj (Prod.swap K J ⋙ G)).obj k) j

Tactic:
simp

Result:
no goals

Proof state:
J : Type u_1
K : Type u_2
inst✝⁵ : Category.{u_6, u_1} J
inst✝⁴ : Category.{u_5, u_2} K
C : Type u_3
inst✝³ : Category.{u_4, u_3} C
G : J × K ⥤ C
inst✝² : HasLimitsOfShape K C
inst✝¹ : HasLimitsOfShape J C
inst✝ : HasLimit (curry.obj G ⋙ lim)
j : J
k : K
⊢ (((limitIsoLimitCurryCompLim (Prod.swap K J ⋙ G)).inv ≫
          (HasLimit.isoOfEquivalence (Prod.braiding K J) (Iso.refl (Prod.swap K J ⋙ G))).hom) ≫
        (limitIsoLimitCurryCompLim G).hom) ≫
      limit.π (curry.obj G ⋙ lim) j ≫ limit.π ((curry.obj G).obj j) k =
    limit.π (curry.obj (Prod.swap K J ⋙ G) ⋙ lim) k ≫ limit.π ((curry.obj (Prod.swap K J ⋙ G)).obj k) j

Tactic:
rw [Category.assoc, Category.assoc, limitIsoLimitCurryCompLim_hom_π_π,
  HasLimit.isoOfEquivalence_hom_π]

Result:
J : Type u_1
K : Type u_2
inst✝⁵ : Category.{u_6, u_1} J
inst✝⁴ : Category.{u_5, u_2} K
C : Type u_3
inst✝³ : Category.{u_4, u_3} C
G : J × K ⥤ C
inst✝² : HasLimitsOfShape K C
inst✝¹ : HasLimitsOfShape J C
inst✝ : HasLimit (curry.obj G ⋙ lim)
j : J
k : K
⊢ (limitIsoLimitCurryCompLim (Prod.swap K J ⋙ G)).inv ≫
      limit.π (Prod.swap K J ⋙ G) ((Prod.braiding K J).inverse.obj (j, k)) ≫
        (Iso.refl (Prod.swap K J ⋙ G)).inv.app ((Prod.braiding K J).inverse.obj (j, k)) ≫
          G.map ((Prod.braiding K J).counit.app (j, k)) =
    limit.π (curry.obj (Prod.swap K J ⋙ G) ⋙ lim) k ≫ limit.π ((curry.obj (Prod.swap K J ⋙ G)).obj k) j

Proof state:
J : Type u_1
K : Type u_2
inst✝⁵ : Category.{u_6, u_1} J
inst✝⁴ : Category.{u_5, u_2} K
C : Type u_3
inst✝³ : Category.{u_4, u_3} C
G : J × K ⥤ C
inst✝² : HasLimitsOfShape K C
inst✝¹ : HasLimitsOfShape J C
inst✝ : HasLimit (curry.obj G ⋙ lim)
j : J
k : K
⊢ (limitIsoLimitCurryCompLim (Prod.swap K J ⋙ G)).inv ≫
      limit.π (Prod.swap K J ⋙ G) (k, j) ≫ 𝟙 (G.obj (j, k)) ≫ G.map (𝟙 j, 𝟙 k) =
    limit.π (curry.obj (Prod.swap K J ⋙ G) ⋙ lim) k ≫ limit.π ((curry.obj (Prod.swap K J ⋙ G)).obj k) j

Tactic:
rw [← prod_id, G.map_id]

Result:
J : Type u_1
K : Type u_2
inst✝⁵ : Category.{u_6, u_1} J
inst✝⁴ : Category.{u_5, u_2} K
C : Type u_3
inst✝³ : Category.{u_4, u_3} C
G : J × K ⥤ C
inst✝² : HasLimitsOfShape K C
inst✝¹ : HasLimitsOfShape J C
inst✝ : HasLimit (curry.obj G ⋙ lim)
j : J
k : K
⊢ (limitIsoLimitCurryCompLim (Prod.swap K J ⋙ G)).inv ≫
      limit.π (Prod.swap K J ⋙ G) (k, j) ≫ 𝟙 (G.obj (j, k)) ≫ 𝟙 (G.obj (j, k)) =
    limit.π (curry.obj (Prod.swap K J ⋙ G) ⋙ lim) k ≫ limit.π ((curry.obj (Prod.swap K J ⋙ G)).obj k) j