-- Mathlib/CategoryTheory/Limits/ColimitLimit.lean
theorem ι_colimitLimitToLimitColimit_π_apply [Small.{v} J] [Small.{v} K] (F : J × K ⥤ Type v)
    (j : J) (k : K) (f) : limit.π (curry.obj F ⋙ colim) j
        (colimitLimitToLimitColimit F (colimit.ι (curry.obj (Prod.swap K J ⋙ F) ⋙ lim) k f)) =
      colimit.ι ((curry.obj F).obj j) k (limit.π ((curry.obj (Prod.swap K J ⋙ F)).obj k) j f)

Proof state:
J : Type u₁
K : Type u₂
inst✝³ : Category.{v₁, u₁} J
inst✝² : Category.{v₂, u₂} K
inst✝¹ : Small.{v, u₁} J
inst✝ : Small.{v, u₂} K
F : J × K ⥤ Type v
j : J
k : K
f : (curry.obj (Prod.swap K J ⋙ F) ⋙ lim).obj k
⊢ limit.π (curry.obj F ⋙ colim) j (colimitLimitToLimitColimit F (colimit.ι (curry.obj (Prod.swap K J ⋙ F) ⋙ lim) k f)) =
    colimit.ι ((curry.obj F).obj j) k (limit.π ((curry.obj (Prod.swap K J ⋙ F)).obj k) j f)

Tactic:
dsimp [colimitLimitToLimitColimit]

Result:
J : Type u₁
K : Type u₂
inst✝³ : Category.{v₁, u₁} J
inst✝² : Category.{v₂, u₂} K
inst✝¹ : Small.{v, u₁} J
inst✝ : Small.{v, u₂} K
F : J × K ⥤ Type v
j : J
k : K
f : (curry.obj (Prod.swap K J ⋙ F) ⋙ lim).obj k
⊢ limit.π (curry.obj F ⋙ colim) j
      (limit.lift (curry.obj F ⋙ colim)
        { pt := colimit (curry.obj (Prod.swap K J ⋙ F) ⋙ lim),
          π :=
            {
              app := fun j =>
                colimit.desc (curry.obj (Prod.swap K J ⋙ F) ⋙ lim)
                  { pt := colimit ((curry.obj F).obj j),
                    ι :=
                      {
                        app := fun k =>
                          limit.π ((curry.obj (Prod.swap K J ⋙ F)).obj k) j ≫ colimit.ι ((curry.obj F).obj j) k,
                        naturality := ⋯ } },
              naturality := ⋯ } }
        (colimit.ι (curry.obj (Prod.swap K J ⋙ F) ⋙ lim) k f)) =
    colimit.ι ((curry.obj F).obj j) k (limit.π ((curry.obj (Prod.swap K J ⋙ F)).obj k) j f)

Proof state:
J : Type u₁
K : Type u₂
inst✝³ : Category.{v₁, u₁} J
inst✝² : Category.{v₂, u₂} K
inst✝¹ : Small.{v, u₁} J
inst✝ : Small.{v, u₂} K
F : J × K ⥤ Type v
j : J
k : K
f : (curry.obj (Prod.swap K J ⋙ F) ⋙ lim).obj k
⊢ { pt := colimit (curry.obj (Prod.swap K J ⋙ F) ⋙ lim),
            π :=
              {
                app := fun j =>
                  colimit.desc (curry.obj (Prod.swap K J ⋙ F) ⋙ lim)
                    { pt := colimit ((curry.obj F).obj j),
                      ι :=
                        {
                          app := fun k =>
                            limit.π ((curry.obj (Prod.swap K J ⋙ F)).obj k) j ≫ colimit.ι ((curry.obj F).obj j) k,
                          naturality := ⋯ } },
                naturality := ⋯ } }.π.app
      j (colimit.ι (curry.obj (Prod.swap K J ⋙ F) ⋙ lim) k f) =
    colimit.ι ((curry.obj F).obj j) k (limit.π ((curry.obj (Prod.swap K J ⋙ F)).obj k) j f)

Tactic:
dsimp only

Result:
J : Type u₁
K : Type u₂
inst✝³ : Category.{v₁, u₁} J
inst✝² : Category.{v₂, u₂} K
inst✝¹ : Small.{v, u₁} J
inst✝ : Small.{v, u₂} K
F : J × K ⥤ Type v
j : J
k : K
f : (curry.obj (Prod.swap K J ⋙ F) ⋙ lim).obj k
⊢ colimit.desc (curry.obj (Prod.swap K J ⋙ F) ⋙ lim)
      { pt := colimit ((curry.obj F).obj j),
        ι :=
          { app := fun k => limit.π ((curry.obj (Prod.swap K J ⋙ F)).obj k) j ≫ colimit.ι ((curry.obj F).obj j) k,
            naturality := ⋯ } }
      (colimit.ι (curry.obj (Prod.swap K J ⋙ F) ⋙ lim) k f) =
    colimit.ι ((curry.obj F).obj j) k (limit.π ((curry.obj (Prod.swap K J ⋙ F)).obj k) j f)

Proof state:
J : Type u₁
K : Type u₂
inst✝³ : Category.{v₁, u₁} J
inst✝² : Category.{v₂, u₂} K
inst✝¹ : Small.{v, u₁} J
inst✝ : Small.{v, u₂} K
F : J × K ⥤ Type v
j : J
k : K
f : (curry.obj (Prod.swap K J ⋙ F) ⋙ lim).obj k
⊢ limit.π (curry.obj F ⋙ colim) j
      (limit.lift (curry.obj F ⋙ colim)
        { pt := colimit (curry.obj (Prod.swap K J ⋙ F) ⋙ lim),
          π :=
            {
              app := fun j =>
                colimit.desc (curry.obj (Prod.swap K J ⋙ F) ⋙ lim)
                  { pt := colimit ((curry.obj F).obj j),
                    ι :=
                      {
                        app := fun k =>
                          limit.π ((curry.obj (Prod.swap K J ⋙ F)).obj k) j ≫ colimit.ι ((curry.obj F).obj j) k,
                        naturality := ⋯ } },
              naturality := ⋯ } }
        (colimit.ι (curry.obj (Prod.swap K J ⋙ F) ⋙ lim) k f)) =
    colimit.ι ((curry.obj F).obj j) k (limit.π ((curry.obj (Prod.swap K J ⋙ F)).obj k) j f)

Tactic:
rw [Types.Limit.lift_π_apply]

Result:
J : Type u₁
K : Type u₂
inst✝³ : Category.{v₁, u₁} J
inst✝² : Category.{v₂, u₂} K
inst✝¹ : Small.{v, u₁} J
inst✝ : Small.{v, u₂} K
F : J × K ⥤ Type v
j : J
k : K
f : (curry.obj (Prod.swap K J ⋙ F) ⋙ lim).obj k
⊢ { pt := colimit (curry.obj (Prod.swap K J ⋙ F) ⋙ lim),
            π :=
              {
                app := fun j =>
                  colimit.desc (curry.obj (Prod.swap K J ⋙ F) ⋙ lim)
                    { pt := colimit ((curry.obj F).obj j),
                      ι :=
                        {
                          app := fun k =>
                            limit.π ((curry.obj (Prod.swap K J ⋙ F)).obj k) j ≫ colimit.ι ((curry.obj F).obj j) k,
                          naturality := ⋯ } },
                naturality := ⋯ } }.π.app
      j (colimit.ι (curry.obj (Prod.swap K J ⋙ F) ⋙ lim) k f) =
    colimit.ι ((curry.obj F).obj j) k (limit.π ((curry.obj (Prod.swap K J ⋙ F)).obj k) j f)

Proof state:
J : Type u₁
K : Type u₂
inst✝³ : Category.{v₁, u₁} J
inst✝² : Category.{v₂, u₂} K
inst✝¹ : Small.{v, u₁} J
inst✝ : Small.{v, u₂} K
F : J × K ⥤ Type v
j : J
k : K
f : (curry.obj (Prod.swap K J ⋙ F) ⋙ lim).obj k
⊢ { pt := colimit ((curry.obj F).obj j),
            ι :=
              { app := fun k => limit.π ((curry.obj (Prod.swap K J ⋙ F)).obj k) j ≫ colimit.ι ((curry.obj F).obj j) k,
                naturality := ⋯ } }.ι.app
      k f =
    colimit.ι ((curry.obj F).obj j) k (limit.π ((curry.obj (Prod.swap K J ⋙ F)).obj k) j f)

Tactic:
dsimp

Result:
no goals

Proof state:
J : Type u₁
K : Type u₂
inst✝³ : Category.{v₁, u₁} J
inst✝² : Category.{v₂, u₂} K
inst✝¹ : Small.{v, u₁} J
inst✝ : Small.{v, u₂} K
F : J × K ⥤ Type v
j : J
k : K
f : (curry.obj (Prod.swap K J ⋙ F) ⋙ lim).obj k
⊢ colimit.desc (curry.obj (Prod.swap K J ⋙ F) ⋙ lim)
      { pt := colimit ((curry.obj F).obj j),
        ι :=
          { app := fun k => limit.π ((curry.obj (Prod.swap K J ⋙ F)).obj k) j ≫ colimit.ι ((curry.obj F).obj j) k,
            naturality := ⋯ } }
      (colimit.ι (curry.obj (Prod.swap K J ⋙ F) ⋙ lim) k f) =
    colimit.ι ((curry.obj F).obj j) k (limit.π ((curry.obj (Prod.swap K J ⋙ F)).obj k) j f)

Tactic:
rw [Types.Colimit.ι_desc_apply]

Result:
J : Type u₁
K : Type u₂
inst✝³ : Category.{v₁, u₁} J
inst✝² : Category.{v₂, u₂} K
inst✝¹ : Small.{v, u₁} J
inst✝ : Small.{v, u₂} K
F : J × K ⥤ Type v
j : J
k : K
f : (curry.obj (Prod.swap K J ⋙ F) ⋙ lim).obj k
⊢ { pt := colimit ((curry.obj F).obj j),
            ι :=
              { app := fun k => limit.π ((curry.obj (Prod.swap K J ⋙ F)).obj k) j ≫ colimit.ι ((curry.obj F).obj j) k,
                naturality := ⋯ } }.ι.app
      k f =
    colimit.ι ((curry.obj F).obj j) k (limit.π ((curry.obj (Prod.swap K J ⋙ F)).obj k) j f)