[GOAL]
J K : Type v
inst✝² : SmallCategory J
inst✝¹ : SmallCategory K
C : Type u
inst✝ : Category.{v, u} C
F : J ⥤ K ⥤ C
D : DiagramOfCones F
Q : (j : J) → IsLimit (DiagramOfCones.obj D j)
c : Cone (uncurry.obj F)
j : J
k k' : K
f : k ⟶ k'
⊢ ((Functor.const K).obj c.pt).map f ≫ (fun k => NatTrans.app c.π (j, k)) k' =
    (fun k => NatTrans.app c.π (j, k)) k ≫ (F.obj j).map f
[PROOFSTEP]
dsimp
[GOAL]
J K : Type v
inst✝² : SmallCategory J
inst✝¹ : SmallCategory K
C : Type u
inst✝ : Category.{v, u} C
F : J ⥤ K ⥤ C
D : DiagramOfCones F
Q : (j : J) → IsLimit (DiagramOfCones.obj D j)
c : Cone (uncurry.obj F)
j : J
k k' : K
f : k ⟶ k'
⊢ 𝟙 c.pt ≫ NatTrans.app c.π (j, k') = NatTrans.app c.π (j, k) ≫ (F.obj j).map f
[PROOFSTEP]
simp only [Category.id_comp]
[GOAL]
J K : Type v
inst✝² : SmallCategory J
inst✝¹ : SmallCategory K
C : Type u
inst✝ : Category.{v, u} C
F : J ⥤ K ⥤ C
D : DiagramOfCones F
Q : (j : J) → IsLimit (DiagramOfCones.obj D j)
c : Cone (uncurry.obj F)
j : J
k k' : K
f : k ⟶ k'
⊢ NatTrans.app c.π (j, k') = NatTrans.app c.π (j, k) ≫ (F.obj j).map f
[PROOFSTEP]
have := @NatTrans.naturality _ _ _ _ _ _ c.π (j, k) (j, k') (𝟙 j, f)
[GOAL]
J K : Type v
inst✝² : SmallCategory J
inst✝¹ : SmallCategory K
C : Type u
inst✝ : Category.{v, u} C
F : J ⥤ K ⥤ C
D : DiagramOfCones F
Q : (j : J) → IsLimit (DiagramOfCones.obj D j)
c : Cone (uncurry.obj F)
j : J
k k' : K
f : k ⟶ k'
this :
  ((Functor.const (J × K)).obj c.pt).map (𝟙 j, f) ≫ NatTrans.app c.π (j, k') =
    NatTrans.app c.π (j, k) ≫ (uncurry.obj F).map (𝟙 j, f)
⊢ NatTrans.app c.π (j, k') = NatTrans.app c.π (j, k) ≫ (F.obj j).map f
[PROOFSTEP]
dsimp at this 
[GOAL]
J K : Type v
inst✝² : SmallCategory J
inst✝¹ : SmallCategory K
C : Type u
inst✝ : Category.{v, u} C
F : J ⥤ K ⥤ C
D : DiagramOfCones F
Q : (j : J) → IsLimit (DiagramOfCones.obj D j)
c : Cone (uncurry.obj F)
j : J
k k' : K
f : k ⟶ k'
this : 𝟙 c.pt ≫ NatTrans.app c.π (j, k') = NatTrans.app c.π (j, k) ≫ NatTrans.app (F.map (𝟙 j)) k ≫ (F.obj j).map f
⊢ NatTrans.app c.π (j, k') = NatTrans.app c.π (j, k) ≫ (F.obj j).map f
[PROOFSTEP]
simp?  at this  says simp only [Category.id_comp, Functor.map_id, NatTrans.id_app] at this 
[GOAL]
J K : Type v
inst✝² : SmallCategory J
inst✝¹ : SmallCategory K
C : Type u
inst✝ : Category.{v, u} C
F : J ⥤ K ⥤ C
D : DiagramOfCones F
Q : (j : J) → IsLimit (DiagramOfCones.obj D j)
c : Cone (uncurry.obj F)
j : J
k k' : K
f : k ⟶ k'
this : 𝟙 c.pt ≫ NatTrans.app c.π (j, k') = NatTrans.app c.π (j, k) ≫ NatTrans.app (F.map (𝟙 j)) k ≫ (F.obj j).map f
⊢ NatTrans.app c.π (j, k') = NatTrans.app c.π (j, k) ≫ (F.obj j).map f
[PROOFSTEP]
simp only [Category.id_comp, Functor.map_id, NatTrans.id_app] at this 
[GOAL]
J K : Type v
inst✝² : SmallCategory J
inst✝¹ : SmallCategory K
C : Type u
inst✝ : Category.{v, u} C
F : J ⥤ K ⥤ C
D : DiagramOfCones F
Q : (j : J) → IsLimit (DiagramOfCones.obj D j)
c : Cone (uncurry.obj F)
j : J
k k' : K
f : k ⟶ k'
this : NatTrans.app c.π (j, k') = NatTrans.app c.π (j, k) ≫ (F.obj j).map f
⊢ NatTrans.app c.π (j, k') = NatTrans.app c.π (j, k) ≫ (F.obj j).map f
[PROOFSTEP]
exact this
[GOAL]
J K : Type v
inst✝² : SmallCategory J
inst✝¹ : SmallCategory K
C : Type u
inst✝ : Category.{v, u} C
F : J ⥤ K ⥤ C
D : DiagramOfCones F
Q : (j : J) → IsLimit (DiagramOfCones.obj D j)
c : Cone (uncurry.obj F)
j j' : J
f : j ⟶ j'
⊢ ∀ (j_1 : K),
    (((Functor.const J).obj c.pt).map f ≫
          (fun j => IsLimit.lift (Q j) { pt := c.pt, π := NatTrans.mk fun k => NatTrans.app c.π (j, k) }) j') ≫
        NatTrans.app (DiagramOfCones.obj D j').π j_1 =
      ((fun j => IsLimit.lift (Q j) { pt := c.pt, π := NatTrans.mk fun k => NatTrans.app c.π (j, k) }) j ≫
          (DiagramOfCones.conePoints D).map f) ≫
        NatTrans.app (DiagramOfCones.obj D j').π j_1
[PROOFSTEP]
dsimp
[GOAL]
J K : Type v
inst✝² : SmallCategory J
inst✝¹ : SmallCategory K
C : Type u
inst✝ : Category.{v, u} C
F : J ⥤ K ⥤ C
D : DiagramOfCones F
Q : (j : J) → IsLimit (DiagramOfCones.obj D j)
c : Cone (uncurry.obj F)
j j' : J
f : j ⟶ j'
⊢ ∀ (j_1 : K),
    (𝟙 c.pt ≫ IsLimit.lift (Q j') { pt := c.pt, π := NatTrans.mk fun k => NatTrans.app c.π (j', k) }) ≫
        NatTrans.app (DiagramOfCones.obj D j').π j_1 =
      (IsLimit.lift (Q j) { pt := c.pt, π := NatTrans.mk fun k => NatTrans.app c.π (j, k) } ≫
          (DiagramOfCones.map D f).Hom) ≫
        NatTrans.app (DiagramOfCones.obj D j').π j_1
[PROOFSTEP]
intro k
[GOAL]
J K : Type v
inst✝² : SmallCategory J
inst✝¹ : SmallCategory K
C : Type u
inst✝ : Category.{v, u} C
F : J ⥤ K ⥤ C
D : DiagramOfCones F
Q : (j : J) → IsLimit (DiagramOfCones.obj D j)
c : Cone (uncurry.obj F)
j j' : J
f : j ⟶ j'
k : K
⊢ (𝟙 c.pt ≫ IsLimit.lift (Q j') { pt := c.pt, π := NatTrans.mk fun k => NatTrans.app c.π (j', k) }) ≫
      NatTrans.app (DiagramOfCones.obj D j').π k =
    (IsLimit.lift (Q j) { pt := c.pt, π := NatTrans.mk fun k => NatTrans.app c.π (j, k) } ≫
        (DiagramOfCones.map D f).Hom) ≫
      NatTrans.app (DiagramOfCones.obj D j').π k
[PROOFSTEP]
simp only [Limits.ConeMorphism.w, Limits.Cones.postcompose_obj_π, Limits.IsLimit.fac_assoc, Limits.IsLimit.fac,
  NatTrans.comp_app, Category.id_comp, Category.assoc]
[GOAL]
J K : Type v
inst✝² : SmallCategory J
inst✝¹ : SmallCategory K
C : Type u
inst✝ : Category.{v, u} C
F : J ⥤ K ⥤ C
D : DiagramOfCones F
Q : (j : J) → IsLimit (DiagramOfCones.obj D j)
c : Cone (uncurry.obj F)
j j' : J
f : j ⟶ j'
k : K
⊢ NatTrans.app c.π (j', k) = NatTrans.app c.π (j, k) ≫ NatTrans.app (F.map f) k
[PROOFSTEP]
have := @NatTrans.naturality _ _ _ _ _ _ c.π (j, k) (j', k) (f, 𝟙 k)
[GOAL]
J K : Type v
inst✝² : SmallCategory J
inst✝¹ : SmallCategory K
C : Type u
inst✝ : Category.{v, u} C
F : J ⥤ K ⥤ C
D : DiagramOfCones F
Q : (j : J) → IsLimit (DiagramOfCones.obj D j)
c : Cone (uncurry.obj F)
j j' : J
f : j ⟶ j'
k : K
this :
  ((Functor.const (J × K)).obj c.pt).map (f, 𝟙 k) ≫ NatTrans.app c.π (j', k) =
    NatTrans.app c.π (j, k) ≫ (uncurry.obj F).map (f, 𝟙 k)
⊢ NatTrans.app c.π (j', k) = NatTrans.app c.π (j, k) ≫ NatTrans.app (F.map f) k
[PROOFSTEP]
dsimp at this 
[GOAL]
J K : Type v
inst✝² : SmallCategory J
inst✝¹ : SmallCategory K
C : Type u
inst✝ : Category.{v, u} C
F : J ⥤ K ⥤ C
D : DiagramOfCones F
Q : (j : J) → IsLimit (DiagramOfCones.obj D j)
c : Cone (uncurry.obj F)
j j' : J
f : j ⟶ j'
k : K
this : 𝟙 c.pt ≫ NatTrans.app c.π (j', k) = NatTrans.app c.π (j, k) ≫ NatTrans.app (F.map f) k ≫ (F.obj j').map (𝟙 k)
⊢ NatTrans.app c.π (j', k) = NatTrans.app c.π (j, k) ≫ NatTrans.app (F.map f) k
[PROOFSTEP]
simp only [Category.id_comp, Category.comp_id, CategoryTheory.Functor.map_id, NatTrans.id_app] at this 
[GOAL]
J K : Type v
inst✝² : SmallCategory J
inst✝¹ : SmallCategory K
C : Type u
inst✝ : Category.{v, u} C
F : J ⥤ K ⥤ C
D : DiagramOfCones F
Q : (j : J) → IsLimit (DiagramOfCones.obj D j)
c : Cone (uncurry.obj F)
j j' : J
f : j ⟶ j'
k : K
this : NatTrans.app c.π (j', k) = NatTrans.app c.π (j, k) ≫ NatTrans.app (F.map f) k
⊢ NatTrans.app c.π (j', k) = NatTrans.app c.π (j, k) ≫ NatTrans.app (F.map f) k
[PROOFSTEP]
exact this
[GOAL]
J K : Type v
inst✝² : SmallCategory J
inst✝¹ : SmallCategory K
C : Type u
inst✝ : Category.{v, u} C
F : J ⥤ K ⥤ C
D : DiagramOfCones F
Q : (j : J) → IsLimit (DiagramOfCones.obj D j)
c : Cone (uncurry.obj F)
P : IsLimit c
s : Cone (DiagramOfCones.conePoints D)
p p' : J × K
f : p ⟶ p'
⊢ ((Functor.const (J × K)).obj s.pt).map f ≫
      (fun p => NatTrans.app s.π p.fst ≫ NatTrans.app (DiagramOfCones.obj D p.fst).π p.snd) p' =
    (fun p => NatTrans.app s.π p.fst ≫ NatTrans.app (DiagramOfCones.obj D p.fst).π p.snd) p ≫ (uncurry.obj F).map f
[PROOFSTEP]
dsimp
[GOAL]
J K : Type v
inst✝² : SmallCategory J
inst✝¹ : SmallCategory K
C : Type u
inst✝ : Category.{v, u} C
F : J ⥤ K ⥤ C
D : DiagramOfCones F
Q : (j : J) → IsLimit (DiagramOfCones.obj D j)
c : Cone (uncurry.obj F)
P : IsLimit c
s : Cone (DiagramOfCones.conePoints D)
p p' : J × K
f : p ⟶ p'
⊢ 𝟙 s.pt ≫ NatTrans.app s.π p'.fst ≫ NatTrans.app (DiagramOfCones.obj D p'.fst).π p'.snd =
    (NatTrans.app s.π p.fst ≫ NatTrans.app (DiagramOfCones.obj D p.fst).π p.snd) ≫
      NatTrans.app (F.map f.fst) p.snd ≫ (F.obj p'.fst).map f.snd
[PROOFSTEP]
simp only [Category.id_comp, Category.assoc]
[GOAL]
J K : Type v
inst✝² : SmallCategory J
inst✝¹ : SmallCategory K
C : Type u
inst✝ : Category.{v, u} C
F : J ⥤ K ⥤ C
D : DiagramOfCones F
Q : (j : J) → IsLimit (DiagramOfCones.obj D j)
c : Cone (uncurry.obj F)
P : IsLimit c
s : Cone (DiagramOfCones.conePoints D)
p p' : J × K
f : p ⟶ p'
⊢ NatTrans.app s.π p'.fst ≫ NatTrans.app (DiagramOfCones.obj D p'.fst).π p'.snd =
    NatTrans.app s.π p.fst ≫
      NatTrans.app (DiagramOfCones.obj D p.fst).π p.snd ≫ NatTrans.app (F.map f.fst) p.snd ≫ (F.obj p'.fst).map f.snd
[PROOFSTEP]
rcases p with ⟨j, k⟩
[GOAL]
case mk
J K : Type v
inst✝² : SmallCategory J
inst✝¹ : SmallCategory K
C : Type u
inst✝ : Category.{v, u} C
F : J ⥤ K ⥤ C
D : DiagramOfCones F
Q : (j : J) → IsLimit (DiagramOfCones.obj D j)
c : Cone (uncurry.obj F)
P : IsLimit c
s : Cone (DiagramOfCones.conePoints D)
p' : J × K
j : J
k : K
f : (j, k) ⟶ p'
⊢ NatTrans.app s.π p'.fst ≫ NatTrans.app (DiagramOfCones.obj D p'.fst).π p'.snd =
    NatTrans.app s.π (j, k).fst ≫
      NatTrans.app (DiagramOfCones.obj D (j, k).fst).π (j, k).snd ≫
        NatTrans.app (F.map f.fst) (j, k).snd ≫ (F.obj p'.fst).map f.snd
[PROOFSTEP]
rcases p' with ⟨j', k'⟩
[GOAL]
case mk.mk
J K : Type v
inst✝² : SmallCategory J
inst✝¹ : SmallCategory K
C : Type u
inst✝ : Category.{v, u} C
F : J ⥤ K ⥤ C
D : DiagramOfCones F
Q : (j : J) → IsLimit (DiagramOfCones.obj D j)
c : Cone (uncurry.obj F)
P : IsLimit c
s : Cone (DiagramOfCones.conePoints D)
j : J
k : K
j' : J
k' : K
f : (j, k) ⟶ (j', k')
⊢ NatTrans.app s.π (j', k').fst ≫ NatTrans.app (DiagramOfCones.obj D (j', k').fst).π (j', k').snd =
    NatTrans.app s.π (j, k).fst ≫
      NatTrans.app (DiagramOfCones.obj D (j, k).fst).π (j, k).snd ≫
        NatTrans.app (F.map f.fst) (j, k).snd ≫ (F.obj (j', k').fst).map f.snd
[PROOFSTEP]
rcases f with ⟨fj, fk⟩
[GOAL]
case mk.mk.mk
J K : Type v
inst✝² : SmallCategory J
inst✝¹ : SmallCategory K
C : Type u
inst✝ : Category.{v, u} C
F : J ⥤ K ⥤ C
D : DiagramOfCones F
Q : (j : J) → IsLimit (DiagramOfCones.obj D j)
c : Cone (uncurry.obj F)
P : IsLimit c
s : Cone (DiagramOfCones.conePoints D)
j : J
k : K
j' : J
k' : K
fj : (j, k).fst ⟶ (j', k').fst
fk : (j, k).snd ⟶ (j', k').snd
⊢ NatTrans.app s.π (j', k').fst ≫ NatTrans.app (DiagramOfCones.obj D (j', k').fst).π (j', k').snd =
    NatTrans.app s.π (j, k).fst ≫
      NatTrans.app (DiagramOfCones.obj D (j, k).fst).π (j, k).snd ≫
        NatTrans.app (F.map (fj, fk).fst) (j, k).snd ≫ (F.obj (j', k').fst).map (fj, fk).snd
[PROOFSTEP]
dsimp
[GOAL]
case mk.mk.mk
J K : Type v
inst✝² : SmallCategory J
inst✝¹ : SmallCategory K
C : Type u
inst✝ : Category.{v, u} C
F : J ⥤ K ⥤ C
D : DiagramOfCones F
Q : (j : J) → IsLimit (DiagramOfCones.obj D j)
c : Cone (uncurry.obj F)
P : IsLimit c
s : Cone (DiagramOfCones.conePoints D)
j : J
k : K
j' : J
k' : K
fj : (j, k).fst ⟶ (j', k').fst
fk : (j, k).snd ⟶ (j', k').snd
⊢ NatTrans.app s.π j' ≫ NatTrans.app (DiagramOfCones.obj D j').π k' =
    NatTrans.app s.π j ≫ NatTrans.app (DiagramOfCones.obj D j).π k ≫ NatTrans.app (F.map fj) k ≫ (F.obj j').map fk
[PROOFSTEP]
slice_rhs 3 4 => rw [← NatTrans.naturality]
[GOAL]
case a.a
J K : Type v
inst✝² : SmallCategory J
inst✝¹ : SmallCategory K
C : Type u
inst✝ : Category.{v, u} C
F : J ⥤ K ⥤ C
D : DiagramOfCones F
Q : (j : J) → IsLimit (DiagramOfCones.obj D j)
c : Cone (uncurry.obj F)
P : IsLimit c
s : Cone (DiagramOfCones.conePoints D)
j : J
k : K
j' : J
k' : K
fj : (j, k).fst ⟶ (j', k').fst
fk : (j, k).snd ⟶ (j', k').snd
| NatTrans.app (F.map fj) k ≫ (F.obj j').map fk
case a
J K : Type v
inst✝² : SmallCategory J
inst✝¹ : SmallCategory K
C : Type u
inst✝ : Category.{v, u} C
F : J ⥤ K ⥤ C
D : DiagramOfCones F
Q : (j : J) → IsLimit (DiagramOfCones.obj D j)
c : Cone (uncurry.obj F)
P : IsLimit c
s : Cone (DiagramOfCones.conePoints D)
j : J
k : K
j' : J
k' : K
fj : (j, k).fst ⟶ (j', k').fst
fk : (j, k).snd ⟶ (j', k').snd
| NatTrans.app s.π j
case a.a
J K : Type v
inst✝² : SmallCategory J
inst✝¹ : SmallCategory K
C : Type u
inst✝ : Category.{v, u} C
F : J ⥤ K ⥤ C
D : DiagramOfCones F
Q : (j : J) → IsLimit (DiagramOfCones.obj D j)
c : Cone (uncurry.obj F)
P : IsLimit c
s : Cone (DiagramOfCones.conePoints D)
j : J
k : K
j' : J
k' : K
fj : (j, k).fst ⟶ (j', k').fst
fk : (j, k).snd ⟶ (j', k').snd
| NatTrans.app (DiagramOfCones.obj D j).π k
[PROOFSTEP]
rw [← NatTrans.naturality]
[GOAL]
case a.a
J K : Type v
inst✝² : SmallCategory J
inst✝¹ : SmallCategory K
C : Type u
inst✝ : Category.{v, u} C
F : J ⥤ K ⥤ C
D : DiagramOfCones F
Q : (j : J) → IsLimit (DiagramOfCones.obj D j)
c : Cone (uncurry.obj F)
P : IsLimit c
s : Cone (DiagramOfCones.conePoints D)
j : J
k : K
j' : J
k' : K
fj : (j, k).fst ⟶ (j', k').fst
fk : (j, k).snd ⟶ (j', k').snd
| NatTrans.app (F.map fj) k ≫ (F.obj j').map fk
case a
J K : Type v
inst✝² : SmallCategory J
inst✝¹ : SmallCategory K
C : Type u
inst✝ : Category.{v, u} C
F : J ⥤ K ⥤ C
D : DiagramOfCones F
Q : (j : J) → IsLimit (DiagramOfCones.obj D j)
c : Cone (uncurry.obj F)
P : IsLimit c
s : Cone (DiagramOfCones.conePoints D)
j : J
k : K
j' : J
k' : K
fj : (j, k).fst ⟶ (j', k').fst
fk : (j, k).snd ⟶ (j', k').snd
| NatTrans.app s.π j
case a.a
J K : Type v
inst✝² : SmallCategory J
inst✝¹ : SmallCategory K
C : Type u
inst✝ : Category.{v, u} C
F : J ⥤ K ⥤ C
D : DiagramOfCones F
Q : (j : J) → IsLimit (DiagramOfCones.obj D j)
c : Cone (uncurry.obj F)
P : IsLimit c
s : Cone (DiagramOfCones.conePoints D)
j : J
k : K
j' : J
k' : K
fj : (j, k).fst ⟶ (j', k').fst
fk : (j, k).snd ⟶ (j', k').snd
| NatTrans.app (DiagramOfCones.obj D j).π k
[PROOFSTEP]
rw [← NatTrans.naturality]
[GOAL]
case a.a
J K : Type v
inst✝² : SmallCategory J
inst✝¹ : SmallCategory K
C : Type u
inst✝ : Category.{v, u} C
F : J ⥤ K ⥤ C
D : DiagramOfCones F
Q : (j : J) → IsLimit (DiagramOfCones.obj D j)
c : Cone (uncurry.obj F)
P : IsLimit c
s : Cone (DiagramOfCones.conePoints D)
j : J
k : K
j' : J
k' : K
fj : (j, k).fst ⟶ (j', k').fst
fk : (j, k).snd ⟶ (j', k').snd
| NatTrans.app (F.map fj) k ≫ (F.obj j').map fk
case a
J K : Type v
inst✝² : SmallCategory J
inst✝¹ : SmallCategory K
C : Type u
inst✝ : Category.{v, u} C
F : J ⥤ K ⥤ C
D : DiagramOfCones F
Q : (j : J) → IsLimit (DiagramOfCones.obj D j)
c : Cone (uncurry.obj F)
P : IsLimit c
s : Cone (DiagramOfCones.conePoints D)
j : J
k : K
j' : J
k' : K
fj : (j, k).fst ⟶ (j', k').fst
fk : (j, k).snd ⟶ (j', k').snd
| NatTrans.app s.π j
case a.a
J K : Type v
inst✝² : SmallCategory J
inst✝¹ : SmallCategory K
C : Type u
inst✝ : Category.{v, u} C
F : J ⥤ K ⥤ C
D : DiagramOfCones F
Q : (j : J) → IsLimit (DiagramOfCones.obj D j)
c : Cone (uncurry.obj F)
P : IsLimit c
s : Cone (DiagramOfCones.conePoints D)
j : J
k : K
j' : J
k' : K
fj : (j, k).fst ⟶ (j', k').fst
fk : (j, k).snd ⟶ (j', k').snd
| NatTrans.app (DiagramOfCones.obj D j).π k
[PROOFSTEP]
rw [← NatTrans.naturality]
[GOAL]
case mk.mk.mk
J K : Type v
inst✝² : SmallCategory J
inst✝¹ : SmallCategory K
C : Type u
inst✝ : Category.{v, u} C
F : J ⥤ K ⥤ C
D : DiagramOfCones F
Q : (j : J) → IsLimit (DiagramOfCones.obj D j)
c : Cone (uncurry.obj F)
P : IsLimit c
s : Cone (DiagramOfCones.conePoints D)
j : J
k : K
j' : J
k' : K
fj : (j, k).fst ⟶ (j', k').fst
fk : (j, k).snd ⟶ (j', k').snd
⊢ NatTrans.app s.π j' ≫ NatTrans.app (DiagramOfCones.obj D j').π k' =
    NatTrans.app s.π j ≫ NatTrans.app (DiagramOfCones.obj D j).π k ≫ (F.obj j).map fk ≫ NatTrans.app (F.map fj) k'
[PROOFSTEP]
slice_rhs 2 3 => rw [← (D.obj j).π.naturality]
[GOAL]
case a.a
J K : Type v
inst✝² : SmallCategory J
inst✝¹ : SmallCategory K
C : Type u
inst✝ : Category.{v, u} C
F : J ⥤ K ⥤ C
D : DiagramOfCones F
Q : (j : J) → IsLimit (DiagramOfCones.obj D j)
c : Cone (uncurry.obj F)
P : IsLimit c
s : Cone (DiagramOfCones.conePoints D)
j : J
k : K
j' : J
k' : K
fj : (j, k).fst ⟶ (j', k').fst
fk : (j, k).snd ⟶ (j', k').snd
| NatTrans.app (DiagramOfCones.obj D j).π k ≫ (F.obj j).map fk
case a.a
J K : Type v
inst✝² : SmallCategory J
inst✝¹ : SmallCategory K
C : Type u
inst✝ : Category.{v, u} C
F : J ⥤ K ⥤ C
D : DiagramOfCones F
Q : (j : J) → IsLimit (DiagramOfCones.obj D j)
c : Cone (uncurry.obj F)
P : IsLimit c
s : Cone (DiagramOfCones.conePoints D)
j : J
k : K
j' : J
k' : K
fj : (j, k).fst ⟶ (j', k').fst
fk : (j, k).snd ⟶ (j', k').snd
| NatTrans.app (F.map fj) k'
case a
J K : Type v
inst✝² : SmallCategory J
inst✝¹ : SmallCategory K
C : Type u
inst✝ : Category.{v, u} C
F : J ⥤ K ⥤ C
D : DiagramOfCones F
Q : (j : J) → IsLimit (DiagramOfCones.obj D j)
c : Cone (uncurry.obj F)
P : IsLimit c
s : Cone (DiagramOfCones.conePoints D)
j : J
k : K
j' : J
k' : K
fj : (j, k).fst ⟶ (j', k').fst
fk : (j, k).snd ⟶ (j', k').snd
| NatTrans.app s.π j
[PROOFSTEP]
rw [← (D.obj j).π.naturality]
[GOAL]
case a.a
J K : Type v
inst✝² : SmallCategory J
inst✝¹ : SmallCategory K
C : Type u
inst✝ : Category.{v, u} C
F : J ⥤ K ⥤ C
D : DiagramOfCones F
Q : (j : J) → IsLimit (DiagramOfCones.obj D j)
c : Cone (uncurry.obj F)
P : IsLimit c
s : Cone (DiagramOfCones.conePoints D)
j : J
k : K
j' : J
k' : K
fj : (j, k).fst ⟶ (j', k').fst
fk : (j, k).snd ⟶ (j', k').snd
| NatTrans.app (DiagramOfCones.obj D j).π k ≫ (F.obj j).map fk
case a.a
J K : Type v
inst✝² : SmallCategory J
inst✝¹ : SmallCategory K
C : Type u
inst✝ : Category.{v, u} C
F : J ⥤ K ⥤ C
D : DiagramOfCones F
Q : (j : J) → IsLimit (DiagramOfCones.obj D j)
c : Cone (uncurry.obj F)
P : IsLimit c
s : Cone (DiagramOfCones.conePoints D)
j : J
k : K
j' : J
k' : K
fj : (j, k).fst ⟶ (j', k').fst
fk : (j, k).snd ⟶ (j', k').snd
| NatTrans.app (F.map fj) k'
case a
J K : Type v
inst✝² : SmallCategory J
inst✝¹ : SmallCategory K
C : Type u
inst✝ : Category.{v, u} C
F : J ⥤ K ⥤ C
D : DiagramOfCones F
Q : (j : J) → IsLimit (DiagramOfCones.obj D j)
c : Cone (uncurry.obj F)
P : IsLimit c
s : Cone (DiagramOfCones.conePoints D)
j : J
k : K
j' : J
k' : K
fj : (j, k).fst ⟶ (j', k').fst
fk : (j, k).snd ⟶ (j', k').snd
| NatTrans.app s.π j
[PROOFSTEP]
rw [← (D.obj j).π.naturality]
[GOAL]
case a.a
J K : Type v
inst✝² : SmallCategory J
inst✝¹ : SmallCategory K
C : Type u
inst✝ : Category.{v, u} C
F : J ⥤ K ⥤ C
D : DiagramOfCones F
Q : (j : J) → IsLimit (DiagramOfCones.obj D j)
c : Cone (uncurry.obj F)
P : IsLimit c
s : Cone (DiagramOfCones.conePoints D)
j : J
k : K
j' : J
k' : K
fj : (j, k).fst ⟶ (j', k').fst
fk : (j, k).snd ⟶ (j', k').snd
| NatTrans.app (DiagramOfCones.obj D j).π k ≫ (F.obj j).map fk
case a.a
J K : Type v
inst✝² : SmallCategory J
inst✝¹ : SmallCategory K
C : Type u
inst✝ : Category.{v, u} C
F : J ⥤ K ⥤ C
D : DiagramOfCones F
Q : (j : J) → IsLimit (DiagramOfCones.obj D j)
c : Cone (uncurry.obj F)
P : IsLimit c
s : Cone (DiagramOfCones.conePoints D)
j : J
k : K
j' : J
k' : K
fj : (j, k).fst ⟶ (j', k').fst
fk : (j, k).snd ⟶ (j', k').snd
| NatTrans.app (F.map fj) k'
case a
J K : Type v
inst✝² : SmallCategory J
inst✝¹ : SmallCategory K
C : Type u
inst✝ : Category.{v, u} C
F : J ⥤ K ⥤ C
D : DiagramOfCones F
Q : (j : J) → IsLimit (DiagramOfCones.obj D j)
c : Cone (uncurry.obj F)
P : IsLimit c
s : Cone (DiagramOfCones.conePoints D)
j : J
k : K
j' : J
k' : K
fj : (j, k).fst ⟶ (j', k').fst
fk : (j, k).snd ⟶ (j', k').snd
| NatTrans.app s.π j
[PROOFSTEP]
rw [← (D.obj j).π.naturality]
[GOAL]
case mk.mk.mk
J K : Type v
inst✝² : SmallCategory J
inst✝¹ : SmallCategory K
C : Type u
inst✝ : Category.{v, u} C
F : J ⥤ K ⥤ C
D : DiagramOfCones F
Q : (j : J) → IsLimit (DiagramOfCones.obj D j)
c : Cone (uncurry.obj F)
P : IsLimit c
s : Cone (DiagramOfCones.conePoints D)
j : J
k : K
j' : J
k' : K
fj : (j, k).fst ⟶ (j', k').fst
fk : (j, k).snd ⟶ (j', k').snd
⊢ NatTrans.app s.π j' ≫ NatTrans.app (DiagramOfCones.obj D j').π k' =
    NatTrans.app s.π j ≫
      (((Functor.const K).obj (DiagramOfCones.obj D j).pt).map fk ≫ NatTrans.app (DiagramOfCones.obj D j).π k') ≫
        NatTrans.app (F.map fj) k'
[PROOFSTEP]
simp only [Functor.const_obj_map, Category.id_comp, Category.assoc]
[GOAL]
case mk.mk.mk
J K : Type v
inst✝² : SmallCategory J
inst✝¹ : SmallCategory K
C : Type u
inst✝ : Category.{v, u} C
F : J ⥤ K ⥤ C
D : DiagramOfCones F
Q : (j : J) → IsLimit (DiagramOfCones.obj D j)
c : Cone (uncurry.obj F)
P : IsLimit c
s : Cone (DiagramOfCones.conePoints D)
j : J
k : K
j' : J
k' : K
fj : (j, k).fst ⟶ (j', k').fst
fk : (j, k).snd ⟶ (j', k').snd
⊢ NatTrans.app s.π j' ≫ NatTrans.app (DiagramOfCones.obj D j').π k' =
    NatTrans.app s.π j ≫ NatTrans.app (DiagramOfCones.obj D j).π k' ≫ NatTrans.app (F.map fj) k'
[PROOFSTEP]
have w := (D.map fj).w k'
[GOAL]
case mk.mk.mk
J K : Type v
inst✝² : SmallCategory J
inst✝¹ : SmallCategory K
C : Type u
inst✝ : Category.{v, u} C
F : J ⥤ K ⥤ C
D : DiagramOfCones F
Q : (j : J) → IsLimit (DiagramOfCones.obj D j)
c : Cone (uncurry.obj F)
P : IsLimit c
s : Cone (DiagramOfCones.conePoints D)
j : J
k : K
j' : J
k' : K
fj : (j, k).fst ⟶ (j', k').fst
fk : (j, k).snd ⟶ (j', k').snd
w :
  (DiagramOfCones.map D fj).Hom ≫ NatTrans.app (DiagramOfCones.obj D (j', k').fst).π k' =
    NatTrans.app ((Cones.postcompose (F.map fj)).obj (DiagramOfCones.obj D (j, k).fst)).π k'
⊢ NatTrans.app s.π j' ≫ NatTrans.app (DiagramOfCones.obj D j').π k' =
    NatTrans.app s.π j ≫ NatTrans.app (DiagramOfCones.obj D j).π k' ≫ NatTrans.app (F.map fj) k'
[PROOFSTEP]
dsimp at w 
[GOAL]
case mk.mk.mk
J K : Type v
inst✝² : SmallCategory J
inst✝¹ : SmallCategory K
C : Type u
inst✝ : Category.{v, u} C
F : J ⥤ K ⥤ C
D : DiagramOfCones F
Q : (j : J) → IsLimit (DiagramOfCones.obj D j)
c : Cone (uncurry.obj F)
P : IsLimit c
s : Cone (DiagramOfCones.conePoints D)
j : J
k : K
j' : J
k' : K
fj : (j, k).fst ⟶ (j', k').fst
fk : (j, k).snd ⟶ (j', k').snd
w :
  (DiagramOfCones.map D fj).Hom ≫ NatTrans.app (DiagramOfCones.obj D j').π k' =
    NatTrans.app (DiagramOfCones.obj D j).π k' ≫ NatTrans.app (F.map fj) k'
⊢ NatTrans.app s.π j' ≫ NatTrans.app (DiagramOfCones.obj D j').π k' =
    NatTrans.app s.π j ≫ NatTrans.app (DiagramOfCones.obj D j).π k' ≫ NatTrans.app (F.map fj) k'
[PROOFSTEP]
rw [← w]
[GOAL]
case mk.mk.mk
J K : Type v
inst✝² : SmallCategory J
inst✝¹ : SmallCategory K
C : Type u
inst✝ : Category.{v, u} C
F : J ⥤ K ⥤ C
D : DiagramOfCones F
Q : (j : J) → IsLimit (DiagramOfCones.obj D j)
c : Cone (uncurry.obj F)
P : IsLimit c
s : Cone (DiagramOfCones.conePoints D)
j : J
k : K
j' : J
k' : K
fj : (j, k).fst ⟶ (j', k').fst
fk : (j, k).snd ⟶ (j', k').snd
w :
  (DiagramOfCones.map D fj).Hom ≫ NatTrans.app (DiagramOfCones.obj D j').π k' =
    NatTrans.app (DiagramOfCones.obj D j).π k' ≫ NatTrans.app (F.map fj) k'
⊢ NatTrans.app s.π j' ≫ NatTrans.app (DiagramOfCones.obj D j').π k' =
    NatTrans.app s.π j ≫ (DiagramOfCones.map D fj).Hom ≫ NatTrans.app (DiagramOfCones.obj D j').π k'
[PROOFSTEP]
have n := s.π.naturality fj
[GOAL]
case mk.mk.mk
J K : Type v
inst✝² : SmallCategory J
inst✝¹ : SmallCategory K
C : Type u
inst✝ : Category.{v, u} C
F : J ⥤ K ⥤ C
D : DiagramOfCones F
Q : (j : J) → IsLimit (DiagramOfCones.obj D j)
c : Cone (uncurry.obj F)
P : IsLimit c
s : Cone (DiagramOfCones.conePoints D)
j : J
k : K
j' : J
k' : K
fj : (j, k).fst ⟶ (j', k').fst
fk : (j, k).snd ⟶ (j', k').snd
w :
  (DiagramOfCones.map D fj).Hom ≫ NatTrans.app (DiagramOfCones.obj D j').π k' =
    NatTrans.app (DiagramOfCones.obj D j).π k' ≫ NatTrans.app (F.map fj) k'
n :
  ((Functor.const J).obj s.pt).map fj ≫ NatTrans.app s.π (j', k').fst =
    NatTrans.app s.π (j, k).fst ≫ (DiagramOfCones.conePoints D).map fj
⊢ NatTrans.app s.π j' ≫ NatTrans.app (DiagramOfCones.obj D j').π k' =
    NatTrans.app s.π j ≫ (DiagramOfCones.map D fj).Hom ≫ NatTrans.app (DiagramOfCones.obj D j').π k'
[PROOFSTEP]
dsimp at n 
[GOAL]
case mk.mk.mk
J K : Type v
inst✝² : SmallCategory J
inst✝¹ : SmallCategory K
C : Type u
inst✝ : Category.{v, u} C
F : J ⥤ K ⥤ C
D : DiagramOfCones F
Q : (j : J) → IsLimit (DiagramOfCones.obj D j)
c : Cone (uncurry.obj F)
P : IsLimit c
s : Cone (DiagramOfCones.conePoints D)
j : J
k : K
j' : J
k' : K
fj : (j, k).fst ⟶ (j', k').fst
fk : (j, k).snd ⟶ (j', k').snd
w :
  (DiagramOfCones.map D fj).Hom ≫ NatTrans.app (DiagramOfCones.obj D j').π k' =
    NatTrans.app (DiagramOfCones.obj D j).π k' ≫ NatTrans.app (F.map fj) k'
n : 𝟙 s.pt ≫ NatTrans.app s.π j' = NatTrans.app s.π j ≫ (DiagramOfCones.map D fj).Hom
⊢ NatTrans.app s.π j' ≫ NatTrans.app (DiagramOfCones.obj D j').π k' =
    NatTrans.app s.π j ≫ (DiagramOfCones.map D fj).Hom ≫ NatTrans.app (DiagramOfCones.obj D j').π k'
[PROOFSTEP]
simp only [Category.id_comp] at n 
[GOAL]
case mk.mk.mk
J K : Type v
inst✝² : SmallCategory J
inst✝¹ : SmallCategory K
C : Type u
inst✝ : Category.{v, u} C
F : J ⥤ K ⥤ C
D : DiagramOfCones F
Q : (j : J) → IsLimit (DiagramOfCones.obj D j)
c : Cone (uncurry.obj F)
P : IsLimit c
s : Cone (DiagramOfCones.conePoints D)
j : J
k : K
j' : J
k' : K
fj : (j, k).fst ⟶ (j', k').fst
fk : (j, k).snd ⟶ (j', k').snd
w :
  (DiagramOfCones.map D fj).Hom ≫ NatTrans.app (DiagramOfCones.obj D j').π k' =
    NatTrans.app (DiagramOfCones.obj D j).π k' ≫ NatTrans.app (F.map fj) k'
n : NatTrans.app s.π j' = NatTrans.app s.π j ≫ (DiagramOfCones.map D fj).Hom
⊢ NatTrans.app s.π j' ≫ NatTrans.app (DiagramOfCones.obj D j').π k' =
    NatTrans.app s.π j ≫ (DiagramOfCones.map D fj).Hom ≫ NatTrans.app (DiagramOfCones.obj D j').π k'
[PROOFSTEP]
rw [n]
[GOAL]
case mk.mk.mk
J K : Type v
inst✝² : SmallCategory J
inst✝¹ : SmallCategory K
C : Type u
inst✝ : Category.{v, u} C
F : J ⥤ K ⥤ C
D : DiagramOfCones F
Q : (j : J) → IsLimit (DiagramOfCones.obj D j)
c : Cone (uncurry.obj F)
P : IsLimit c
s : Cone (DiagramOfCones.conePoints D)
j : J
k : K
j' : J
k' : K
fj : (j, k).fst ⟶ (j', k').fst
fk : (j, k).snd ⟶ (j', k').snd
w :
  (DiagramOfCones.map D fj).Hom ≫ NatTrans.app (DiagramOfCones.obj D j').π k' =
    NatTrans.app (DiagramOfCones.obj D j).π k' ≫ NatTrans.app (F.map fj) k'
n : NatTrans.app s.π j' = NatTrans.app s.π j ≫ (DiagramOfCones.map D fj).Hom
⊢ (NatTrans.app s.π j ≫ (DiagramOfCones.map D fj).Hom) ≫ NatTrans.app (DiagramOfCones.obj D j').π k' =
    NatTrans.app s.π j ≫ (DiagramOfCones.map D fj).Hom ≫ NatTrans.app (DiagramOfCones.obj D j').π k'
[PROOFSTEP]
simp
[GOAL]
J K : Type v
inst✝² : SmallCategory J
inst✝¹ : SmallCategory K
C : Type u
inst✝ : Category.{v, u} C
F : J ⥤ K ⥤ C
D : DiagramOfCones F
Q : (j : J) → IsLimit (DiagramOfCones.obj D j)
c : Cone (uncurry.obj F)
P : IsLimit c
s : Cone (DiagramOfCones.conePoints D)
j : J
⊢ (fun s =>
          IsLimit.lift P
            { pt := s.pt,
              π := NatTrans.mk fun p => NatTrans.app s.π p.fst ≫ NatTrans.app (DiagramOfCones.obj D p.fst).π p.snd })
        s ≫
      NatTrans.app (coneOfConeUncurry Q c).π j =
    NatTrans.app s.π j
[PROOFSTEP]
apply (Q j).hom_ext
[GOAL]
J K : Type v
inst✝² : SmallCategory J
inst✝¹ : SmallCategory K
C : Type u
inst✝ : Category.{v, u} C
F : J ⥤ K ⥤ C
D : DiagramOfCones F
Q : (j : J) → IsLimit (DiagramOfCones.obj D j)
c : Cone (uncurry.obj F)
P : IsLimit c
s : Cone (DiagramOfCones.conePoints D)
j : J
⊢ ∀ (j_1 : K),
    ((fun s =>
              IsLimit.lift P
                { pt := s.pt,
                  π :=
                    NatTrans.mk fun p => NatTrans.app s.π p.fst ≫ NatTrans.app (DiagramOfCones.obj D p.fst).π p.snd })
            s ≫
          NatTrans.app (coneOfConeUncurry Q c).π j) ≫
        NatTrans.app (DiagramOfCones.obj D j).π j_1 =
      NatTrans.app s.π j ≫ NatTrans.app (DiagramOfCones.obj D j).π j_1
[PROOFSTEP]
intro k
[GOAL]
J K : Type v
inst✝² : SmallCategory J
inst✝¹ : SmallCategory K
C : Type u
inst✝ : Category.{v, u} C
F : J ⥤ K ⥤ C
D : DiagramOfCones F
Q : (j : J) → IsLimit (DiagramOfCones.obj D j)
c : Cone (uncurry.obj F)
P : IsLimit c
s : Cone (DiagramOfCones.conePoints D)
j : J
k : K
⊢ ((fun s =>
            IsLimit.lift P
              { pt := s.pt,
                π := NatTrans.mk fun p => NatTrans.app s.π p.fst ≫ NatTrans.app (DiagramOfCones.obj D p.fst).π p.snd })
          s ≫
        NatTrans.app (coneOfConeUncurry Q c).π j) ≫
      NatTrans.app (DiagramOfCones.obj D j).π k =
    NatTrans.app s.π j ≫ NatTrans.app (DiagramOfCones.obj D j).π k
[PROOFSTEP]
simp
[GOAL]
J K : Type v
inst✝² : SmallCategory J
inst✝¹ : SmallCategory K
C : Type u
inst✝ : Category.{v, u} C
F : J ⥤ K ⥤ C
D : DiagramOfCones F
Q : (j : J) → IsLimit (DiagramOfCones.obj D j)
c : Cone (uncurry.obj F)
P : IsLimit c
s : Cone (DiagramOfCones.conePoints D)
m : s.pt ⟶ (coneOfConeUncurry Q c).pt
w : ∀ (j : J), m ≫ NatTrans.app (coneOfConeUncurry Q c).π j = NatTrans.app s.π j
⊢ m =
    (fun s =>
        IsLimit.lift P
          { pt := s.pt,
            π := NatTrans.mk fun p => NatTrans.app s.π p.fst ≫ NatTrans.app (DiagramOfCones.obj D p.fst).π p.snd })
      s
[PROOFSTEP]
refine'
  P.uniq
    { pt := s.pt
      π := _ } m _
[GOAL]
J K : Type v
inst✝² : SmallCategory J
inst✝¹ : SmallCategory K
C : Type u
inst✝ : Category.{v, u} C
F : J ⥤ K ⥤ C
D : DiagramOfCones F
Q : (j : J) → IsLimit (DiagramOfCones.obj D j)
c : Cone (uncurry.obj F)
P : IsLimit c
s : Cone (DiagramOfCones.conePoints D)
m : s.pt ⟶ (coneOfConeUncurry Q c).pt
w : ∀ (j : J), m ≫ NatTrans.app (coneOfConeUncurry Q c).π j = NatTrans.app s.π j
⊢ ∀ (j : J × K),
    m ≫ NatTrans.app c.π j =
      NatTrans.app
        { pt := s.pt,
            π := NatTrans.mk fun p => NatTrans.app s.π p.fst ≫ NatTrans.app (DiagramOfCones.obj D p.fst).π p.snd }.π
        j
[PROOFSTEP]
rintro ⟨j, k⟩
[GOAL]
case mk
J K : Type v
inst✝² : SmallCategory J
inst✝¹ : SmallCategory K
C : Type u
inst✝ : Category.{v, u} C
F : J ⥤ K ⥤ C
D : DiagramOfCones F
Q : (j : J) → IsLimit (DiagramOfCones.obj D j)
c : Cone (uncurry.obj F)
P : IsLimit c
s : Cone (DiagramOfCones.conePoints D)
m : s.pt ⟶ (coneOfConeUncurry Q c).pt
w : ∀ (j : J), m ≫ NatTrans.app (coneOfConeUncurry Q c).π j = NatTrans.app s.π j
j : J
k : K
⊢ m ≫ NatTrans.app c.π (j, k) =
    NatTrans.app
      { pt := s.pt,
          π := NatTrans.mk fun p => NatTrans.app s.π p.fst ≫ NatTrans.app (DiagramOfCones.obj D p.fst).π p.snd }.π
      (j, k)
[PROOFSTEP]
dsimp
[GOAL]
case mk
J K : Type v
inst✝² : SmallCategory J
inst✝¹ : SmallCategory K
C : Type u
inst✝ : Category.{v, u} C
F : J ⥤ K ⥤ C
D : DiagramOfCones F
Q : (j : J) → IsLimit (DiagramOfCones.obj D j)
c : Cone (uncurry.obj F)
P : IsLimit c
s : Cone (DiagramOfCones.conePoints D)
m : s.pt ⟶ (coneOfConeUncurry Q c).pt
w : ∀ (j : J), m ≫ NatTrans.app (coneOfConeUncurry Q c).π j = NatTrans.app s.π j
j : J
k : K
⊢ m ≫ NatTrans.app c.π (j, k) = NatTrans.app s.π j ≫ NatTrans.app (DiagramOfCones.obj D j).π k
[PROOFSTEP]
rw [← w j]
[GOAL]
case mk
J K : Type v
inst✝² : SmallCategory J
inst✝¹ : SmallCategory K
C : Type u
inst✝ : Category.{v, u} C
F : J ⥤ K ⥤ C
D : DiagramOfCones F
Q : (j : J) → IsLimit (DiagramOfCones.obj D j)
c : Cone (uncurry.obj F)
P : IsLimit c
s : Cone (DiagramOfCones.conePoints D)
m : s.pt ⟶ (coneOfConeUncurry Q c).pt
w : ∀ (j : J), m ≫ NatTrans.app (coneOfConeUncurry Q c).π j = NatTrans.app s.π j
j : J
k : K
⊢ m ≫ NatTrans.app c.π (j, k) =
    (m ≫ NatTrans.app (coneOfConeUncurry Q c).π j) ≫ NatTrans.app (DiagramOfCones.obj D j).π k
[PROOFSTEP]
simp
[GOAL]
J K : Type v
inst✝⁵ : SmallCategory J
inst✝⁴ : SmallCategory K
C : Type u
inst✝³ : Category.{v, u} C
F : J ⥤ K ⥤ C
inst✝² : HasLimitsOfShape K C
inst✝¹ : HasLimit (uncurry.obj F)
inst✝ : HasLimit (F ⋙ lim)
⊢ limit (uncurry.obj F) ≅ limit (F ⋙ lim)
[PROOFSTEP]
let c := limit.cone (uncurry.obj F)
[GOAL]
J K : Type v
inst✝⁵ : SmallCategory J
inst✝⁴ : SmallCategory K
C : Type u
inst✝³ : Category.{v, u} C
F : J ⥤ K ⥤ C
inst✝² : HasLimitsOfShape K C
inst✝¹ : HasLimit (uncurry.obj F)
inst✝ : HasLimit (F ⋙ lim)
c : Cone (uncurry.obj F) := limit.cone (uncurry.obj F)
⊢ limit (uncurry.obj F) ≅ limit (F ⋙ lim)
[PROOFSTEP]
let P : IsLimit c := limit.isLimit _
[GOAL]
J K : Type v
inst✝⁵ : SmallCategory J
inst✝⁴ : SmallCategory K
C : Type u
inst✝³ : Category.{v, u} C
F : J ⥤ K ⥤ C
inst✝² : HasLimitsOfShape K C
inst✝¹ : HasLimit (uncurry.obj F)
inst✝ : HasLimit (F ⋙ lim)
c : Cone (uncurry.obj F) := limit.cone (uncurry.obj F)
P : IsLimit c := limit.isLimit (uncurry.obj F)
⊢ limit (uncurry.obj F) ≅ limit (F ⋙ lim)
[PROOFSTEP]
let G := DiagramOfCones.mkOfHasLimits F
[GOAL]
J K : Type v
inst✝⁵ : SmallCategory J
inst✝⁴ : SmallCategory K
C : Type u
inst✝³ : Category.{v, u} C
F : J ⥤ K ⥤ C
inst✝² : HasLimitsOfShape K C
inst✝¹ : HasLimit (uncurry.obj F)
inst✝ : HasLimit (F ⋙ lim)
c : Cone (uncurry.obj F) := limit.cone (uncurry.obj F)
P : IsLimit c := limit.isLimit (uncurry.obj F)
G : DiagramOfCones F := DiagramOfCones.mkOfHasLimits F
⊢ limit (uncurry.obj F) ≅ limit (F ⋙ lim)
[PROOFSTEP]
let Q : ∀ j, IsLimit (G.obj j) := fun j => limit.isLimit _
[GOAL]
J K : Type v
inst✝⁵ : SmallCategory J
inst✝⁴ : SmallCategory K
C : Type u
inst✝³ : Category.{v, u} C
F : J ⥤ K ⥤ C
inst✝² : HasLimitsOfShape K C
inst✝¹ : HasLimit (uncurry.obj F)
inst✝ : HasLimit (F ⋙ lim)
c : Cone (uncurry.obj F) := limit.cone (uncurry.obj F)
P : IsLimit c := limit.isLimit (uncurry.obj F)
G : DiagramOfCones F := DiagramOfCones.mkOfHasLimits F
Q : (j : J) → IsLimit (DiagramOfCones.obj G j) := fun j => limit.isLimit (F.obj j)
⊢ limit (uncurry.obj F) ≅ limit (F ⋙ lim)
[PROOFSTEP]
have Q' := coneOfConeUncurryIsLimit Q P
[GOAL]
J K : Type v
inst✝⁵ : SmallCategory J
inst✝⁴ : SmallCategory K
C : Type u
inst✝³ : Category.{v, u} C
F : J ⥤ K ⥤ C
inst✝² : HasLimitsOfShape K C
inst✝¹ : HasLimit (uncurry.obj F)
inst✝ : HasLimit (F ⋙ lim)
c : Cone (uncurry.obj F) := limit.cone (uncurry.obj F)
P : IsLimit c := limit.isLimit (uncurry.obj F)
G : DiagramOfCones F := DiagramOfCones.mkOfHasLimits F
Q : (j : J) → IsLimit (DiagramOfCones.obj G j) := fun j => limit.isLimit (F.obj j)
Q' : IsLimit (coneOfConeUncurry Q c)
⊢ limit (uncurry.obj F) ≅ limit (F ⋙ lim)
[PROOFSTEP]
have Q'' := limit.isLimit (F ⋙ lim)
[GOAL]
J K : Type v
inst✝⁵ : SmallCategory J
inst✝⁴ : SmallCategory K
C : Type u
inst✝³ : Category.{v, u} C
F : J ⥤ K ⥤ C
inst✝² : HasLimitsOfShape K C
inst✝¹ : HasLimit (uncurry.obj F)
inst✝ : HasLimit (F ⋙ lim)
c : Cone (uncurry.obj F) := limit.cone (uncurry.obj F)
P : IsLimit c := limit.isLimit (uncurry.obj F)
G : DiagramOfCones F := DiagramOfCones.mkOfHasLimits F
Q : (j : J) → IsLimit (DiagramOfCones.obj G j) := fun j => limit.isLimit (F.obj j)
Q' : IsLimit (coneOfConeUncurry Q c)
Q'' : IsLimit (limit.cone (F ⋙ lim))
⊢ limit (uncurry.obj F) ≅ limit (F ⋙ lim)
[PROOFSTEP]
exact IsLimit.conePointUniqueUpToIso Q' Q''
[GOAL]
J K : Type v
inst✝⁵ : SmallCategory J
inst✝⁴ : SmallCategory K
C : Type u
inst✝³ : Category.{v, u} C
F : J ⥤ K ⥤ C
inst✝² : HasLimitsOfShape K C
inst✝¹ : HasLimit (uncurry.obj F)
inst✝ : HasLimit (F ⋙ lim)
j : J
k : K
⊢ (limitUncurryIsoLimitCompLim F).hom ≫ limit.π (F ⋙ lim) j ≫ limit.π (F.obj j) k = limit.π (uncurry.obj F) (j, k)
[PROOFSTEP]
dsimp [limitUncurryIsoLimitCompLim, IsLimit.conePointUniqueUpToIso, IsLimit.uniqueUpToIso]
[GOAL]
J K : Type v
inst✝⁵ : SmallCategory J
inst✝⁴ : SmallCategory K
C : Type u
inst✝³ : Category.{v, u} C
F : J ⥤ K ⥤ C
inst✝² : HasLimitsOfShape K C
inst✝¹ : HasLimit (uncurry.obj F)
inst✝ : HasLimit (F ⋙ lim)
j : J
k : K
⊢ limit.lift (F ⋙ lim) (coneOfConeUncurry (fun j => limit.isLimit (F.obj j)) (limit.cone (uncurry.obj F))) ≫
      limit.π (F ⋙ lim) j ≫ limit.π (F.obj j) k =
    limit.π (uncurry.obj F) (j, k)
[PROOFSTEP]
simp
[GOAL]
J K : Type v
inst✝⁵ : SmallCategory J
inst✝⁴ : SmallCategory K
C : Type u
inst✝³ : Category.{v, u} C
F : J ⥤ K ⥤ C
inst✝² : HasLimitsOfShape K C
inst✝¹ : HasLimit (uncurry.obj F)
inst✝ : HasLimit (F ⋙ lim)
j : J
k : K
⊢ (limitUncurryIsoLimitCompLim F).inv ≫ limit.π (uncurry.obj F) (j, k) = limit.π (F ⋙ lim) j ≫ limit.π (F.obj j) k
[PROOFSTEP]
rw [← cancel_epi (limitUncurryIsoLimitCompLim F).hom]
[GOAL]
J K : Type v
inst✝⁵ : SmallCategory J
inst✝⁴ : SmallCategory K
C : Type u
inst✝³ : Category.{v, u} C
F : J ⥤ K ⥤ C
inst✝² : HasLimitsOfShape K C
inst✝¹ : HasLimit (uncurry.obj F)
inst✝ : HasLimit (F ⋙ lim)
j : J
k : K
⊢ (limitUncurryIsoLimitCompLim F).hom ≫ (limitUncurryIsoLimitCompLim F).inv ≫ limit.π (uncurry.obj F) (j, k) =
    (limitUncurryIsoLimitCompLim F).hom ≫ limit.π (F ⋙ lim) j ≫ limit.π (F.obj j) k
[PROOFSTEP]
simp
[GOAL]
J K : Type v
inst✝⁶ : SmallCategory J
inst✝⁵ : SmallCategory K
C : Type u
inst✝⁴ : Category.{v, u} C
F : J ⥤ K ⥤ C
inst✝³ : HasLimitsOfShape J C
inst✝² : HasLimitsOfShape K C
inst✝¹ : HasLimitsOfShape (J × K) C
inst✝ : HasLimitsOfShape (K × J) C
x✝ : K × J
⊢ ((Prod.braiding K J).functor ⋙ uncurry.obj F).obj x✝ ≅ (Prod.swap K J ⋙ uncurry.obj F).obj x✝
[PROOFSTEP]
rfl
[GOAL]
J K : Type v
inst✝⁶ : SmallCategory J
inst✝⁵ : SmallCategory K
C : Type u
inst✝⁴ : Category.{v, u} C
F : J ⥤ K ⥤ C
inst✝³ : HasLimitsOfShape J C
inst✝² : HasLimitsOfShape K C
inst✝¹ : HasLimitsOfShape (J × K) C
inst✝ : HasLimitsOfShape (K × J) C
j : J
k : K
⊢ (limitFlipCompLimIsoLimitCompLim F).hom ≫ limit.π (F ⋙ lim) j ≫ limit.π (F.obj j) k =
    limit.π (Functor.flip F ⋙ lim) k ≫ limit.π ((Functor.flip F).obj k) j
[PROOFSTEP]
dsimp [limitFlipCompLimIsoLimitCompLim]
[GOAL]
J K : Type v
inst✝⁶ : SmallCategory J
inst✝⁵ : SmallCategory K
C : Type u
inst✝⁴ : Category.{v, u} C
F : J ⥤ K ⥤ C
inst✝³ : HasLimitsOfShape J C
inst✝² : HasLimitsOfShape K C
inst✝¹ : HasLimitsOfShape (J × K) C
inst✝ : HasLimitsOfShape (K × J) C
j : J
k : K
⊢ ((limitUncurryIsoLimitCompLim (Functor.flip F)).inv ≫
        (HasLimit.isoOfNatIso (uncurryObjFlip F)).hom ≫
          (HasLimit.isoOfEquivalence (Prod.braiding K J)
                (NatIso.ofComponents fun x => Iso.refl ((F.obj x.snd).obj x.fst))).hom ≫
            (limitUncurryIsoLimitCompLim F).hom) ≫
      limit.π (F ⋙ lim) j ≫ limit.π (F.obj j) k =
    limit.π (Functor.flip F ⋙ lim) k ≫ limit.π ((Functor.flip F).obj k) j
[PROOFSTEP]
simp
[GOAL]
J K : Type v
inst✝⁶ : SmallCategory J
inst✝⁵ : SmallCategory K
C : Type u
inst✝⁴ : Category.{v, u} C
F : J ⥤ K ⥤ C
inst✝³ : HasLimitsOfShape J C
inst✝² : HasLimitsOfShape K C
inst✝¹ : HasLimitsOfShape (J × K) C
inst✝ : HasLimitsOfShape (K × J) C
k : K
j : J
⊢ (limitFlipCompLimIsoLimitCompLim F).inv ≫ limit.π (Functor.flip F ⋙ lim) k ≫ limit.π ((Functor.flip F).obj k) j =
    limit.π (F ⋙ lim) j ≫ limit.π (F.obj j) k
[PROOFSTEP]
dsimp [limitFlipCompLimIsoLimitCompLim]
[GOAL]
J K : Type v
inst✝⁶ : SmallCategory J
inst✝⁵ : SmallCategory K
C : Type u
inst✝⁴ : Category.{v, u} C
F : J ⥤ K ⥤ C
inst✝³ : HasLimitsOfShape J C
inst✝² : HasLimitsOfShape K C
inst✝¹ : HasLimitsOfShape (J × K) C
inst✝ : HasLimitsOfShape (K × J) C
k : K
j : J
⊢ ((((limitUncurryIsoLimitCompLim F).inv ≫
            (HasLimit.isoOfEquivalence (Prod.braiding K J)
                (NatIso.ofComponents fun x => Iso.refl ((F.obj x.snd).obj x.fst))).inv) ≫
          (HasLimit.isoOfNatIso (uncurryObjFlip F)).inv) ≫
        (limitUncurryIsoLimitCompLim (Functor.flip F)).hom) ≫
      limit.π (Functor.flip F ⋙ lim) k ≫ limit.π ((Functor.flip F).obj k) j =
    limit.π (F ⋙ lim) j ≫ limit.π (F.obj j) k
[PROOFSTEP]
simp
[GOAL]
J K : Type v
inst✝⁵ : SmallCategory J
inst✝⁴ : SmallCategory K
C : Type u
inst✝³ : Category.{v, u} C
F : J ⥤ K ⥤ C
G : J × K ⥤ C
inst✝² : HasLimitsOfShape K C
inst✝¹ : HasLimit G
inst✝ : HasLimit (curry.obj G ⋙ lim)
⊢ limit G ≅ limit (curry.obj G ⋙ lim)
[PROOFSTEP]
have i : G ≅ uncurry.obj ((@curry J _ K _ C _).obj G) := currying.symm.unitIso.app G
[GOAL]
J K : Type v
inst✝⁵ : SmallCategory J
inst✝⁴ : SmallCategory K
C : Type u
inst✝³ : Category.{v, u} C
F : J ⥤ K ⥤ C
G : J × K ⥤ C
inst✝² : HasLimitsOfShape K C
inst✝¹ : HasLimit G
inst✝ : HasLimit (curry.obj G ⋙ lim)
i : G ≅ uncurry.obj (curry.obj G)
⊢ limit G ≅ limit (curry.obj G ⋙ lim)
[PROOFSTEP]
haveI : Limits.HasLimit (uncurry.obj ((@curry J _ K _ C _).obj G)) := hasLimitOfIso i
[GOAL]
J K : Type v
inst✝⁵ : SmallCategory J
inst✝⁴ : SmallCategory K
C : Type u
inst✝³ : Category.{v, u} C
F : J ⥤ K ⥤ C
G : J × K ⥤ C
inst✝² : HasLimitsOfShape K C
inst✝¹ : HasLimit G
inst✝ : HasLimit (curry.obj G ⋙ lim)
i : G ≅ uncurry.obj (curry.obj G)
this : HasLimit (uncurry.obj (curry.obj G))
⊢ limit G ≅ limit (curry.obj G ⋙ lim)
[PROOFSTEP]
trans limit (uncurry.obj ((@curry J _ K _ C _).obj G))
[GOAL]
J K : Type v
inst✝⁵ : SmallCategory J
inst✝⁴ : SmallCategory K
C : Type u
inst✝³ : Category.{v, u} C
F : J ⥤ K ⥤ C
G : J × K ⥤ C
inst✝² : HasLimitsOfShape K C
inst✝¹ : HasLimit G
inst✝ : HasLimit (curry.obj G ⋙ lim)
i : G ≅ uncurry.obj (curry.obj G)
this : HasLimit (uncurry.obj (curry.obj G))
⊢ limit G ≅ limit (uncurry.obj (curry.obj G))
J K : Type v
inst✝⁵ : SmallCategory J
inst✝⁴ : SmallCategory K
C : Type u
inst✝³ : Category.{v, u} C
F : J ⥤ K ⥤ C
G : J × K ⥤ C
inst✝² : HasLimitsOfShape K C
inst✝¹ : HasLimit G
inst✝ : HasLimit (curry.obj G ⋙ lim)
i : G ≅ uncurry.obj (curry.obj G)
this : HasLimit (uncurry.obj (curry.obj G))
⊢ limit (uncurry.obj (curry.obj G)) ≅ limit (curry.obj G ⋙ lim)
[PROOFSTEP]
apply HasLimit.isoOfNatIso i
[GOAL]
J K : Type v
inst✝⁵ : SmallCategory J
inst✝⁴ : SmallCategory K
C : Type u
inst✝³ : Category.{v, u} C
F : J ⥤ K ⥤ C
G : J × K ⥤ C
inst✝² : HasLimitsOfShape K C
inst✝¹ : HasLimit G
inst✝ : HasLimit (curry.obj G ⋙ lim)
i : G ≅ uncurry.obj (curry.obj G)
this : HasLimit (uncurry.obj (curry.obj G))
⊢ limit (uncurry.obj (curry.obj G)) ≅ limit (curry.obj G ⋙ lim)
[PROOFSTEP]
exact limitUncurryIsoLimitCompLim ((@curry J _ K _ C _).obj G)
[GOAL]
J K : Type v
inst✝⁵ : SmallCategory J
inst✝⁴ : SmallCategory K
C : Type u
inst✝³ : Category.{v, u} C
F : J ⥤ K ⥤ C
G : J × K ⥤ C
inst✝² : HasLimitsOfShape K C
inst✝¹ : HasLimit G
inst✝ : HasLimit (curry.obj G ⋙ lim)
j : J
k : K
⊢ (limitIsoLimitCurryCompLim G).hom ≫ limit.π (curry.obj G ⋙ lim) j ≫ limit.π ((curry.obj G).obj j) k = limit.π G (j, k)
[PROOFSTEP]
simp [limitIsoLimitCurryCompLim, Trans.simple, HasLimit.isoOfNatIso, limitUncurryIsoLimitCompLim]
[GOAL]
J K : Type v
inst✝⁵ : SmallCategory J
inst✝⁴ : SmallCategory K
C : Type u
inst✝³ : Category.{v, u} C
F : J ⥤ K ⥤ C
G : J × K ⥤ C
inst✝² : HasLimitsOfShape K C
inst✝¹ : HasLimit G
inst✝ : HasLimit (curry.obj G ⋙ lim)
j : J
k : K
⊢ (limitIsoLimitCurryCompLim G).inv ≫ limit.π G (j, k) = limit.π (curry.obj G ⋙ lim) j ≫ limit.π ((curry.obj G).obj j) k
[PROOFSTEP]
rw [← cancel_epi (limitIsoLimitCurryCompLim G).hom]
[GOAL]
J K : Type v
inst✝⁵ : SmallCategory J
inst✝⁴ : SmallCategory K
C : Type u
inst✝³ : Category.{v, u} C
F : J ⥤ K ⥤ C
G : J × K ⥤ C
inst✝² : HasLimitsOfShape K C
inst✝¹ : HasLimit G
inst✝ : HasLimit (curry.obj G ⋙ lim)
j : J
k : K
⊢ (limitIsoLimitCurryCompLim G).hom ≫ (limitIsoLimitCurryCompLim G).inv ≫ limit.π G (j, k) =
    (limitIsoLimitCurryCompLim G).hom ≫ limit.π (curry.obj G ⋙ lim) j ≫ limit.π ((curry.obj G).obj j) k
[PROOFSTEP]
simp
[GOAL]
J K : Type v
inst✝³ : SmallCategory J
inst✝² : SmallCategory K
C : Type u
inst✝¹ : Category.{v, u} C
F : J ⥤ K ⥤ C
G : J × K ⥤ C
inst✝ : HasLimits C
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
[PROOFSTEP]
dsimp [limitCurrySwapCompLimIsoLimitCurryCompLim]
[GOAL]
J K : Type v
inst✝³ : SmallCategory J
inst✝² : SmallCategory K
C : Type u
inst✝¹ : Category.{v, u} C
F : J ⥤ K ⥤ C
G : J × K ⥤ C
inst✝ : HasLimits C
j : J
k : K
⊢ (((limitIsoLimitCurryCompLim (Prod.swap K J ⋙ G)).inv ≫
          (HasLimit.isoOfEquivalence (Prod.braiding K J) (Iso.refl ((Prod.braiding K J).functor ⋙ 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
[PROOFSTEP]
simp only [Iso.refl_hom, Prod.braiding_counitIso_hom_app, Limits.HasLimit.isoOfEquivalence_hom_π, Iso.refl_inv,
  limitIsoLimitCurryCompLim_hom_π_π, eqToIso_refl, Category.assoc]
[GOAL]
J K : Type v
inst✝³ : SmallCategory J
inst✝² : SmallCategory K
C : Type u
inst✝¹ : Category.{v, u} C
F : J ⥤ K ⥤ C
G : J × K ⥤ C
inst✝ : HasLimits C
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)) ≫
        NatTrans.app (𝟙 ((Prod.braiding K J).functor ⋙ G)) ((Prod.braiding K J).inverse.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
[PROOFSTEP]
erw [NatTrans.id_app]
  -- Why can't `simp` do this?
[GOAL]
J K : Type v
inst✝³ : SmallCategory J
inst✝² : SmallCategory K
C : Type u
inst✝¹ : Category.{v, u} C
F : J ⥤ K ⥤ C
G : J × K ⥤ C
inst✝ : HasLimits C
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)) ≫
        𝟙 ((Prod.swap K J ⋙ G).obj ((Prod.braiding K J).inverse.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
[PROOFSTEP]
dsimp
  -- porting note: the original proof only had `simp`.
    -- However, now `CategoryTheory.Bifunctor.map_id` does not get used by `simp`
[GOAL]
J K : Type v
inst✝³ : SmallCategory J
inst✝² : SmallCategory K
C : Type u
inst✝¹ : Category.{v, u} C
F : J ⥤ K ⥤ C
G : J × K ⥤ C
inst✝ : HasLimits C
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
[PROOFSTEP]
rw [CategoryTheory.Bifunctor.map_id]
[GOAL]
J K : Type v
inst✝³ : SmallCategory J
inst✝² : SmallCategory K
C : Type u
inst✝¹ : Category.{v, u} C
F : J ⥤ K ⥤ C
G : J × K ⥤ C
inst✝ : HasLimits C
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
[PROOFSTEP]
simp
[GOAL]
J K : Type v
inst✝³ : SmallCategory J
inst✝² : SmallCategory K
C : Type u
inst✝¹ : Category.{v, u} C
F : J ⥤ K ⥤ C
G : J × K ⥤ C
inst✝ : HasLimits C
j : J
k : K
⊢ (limitCurrySwapCompLimIsoLimitCurryCompLim G).inv ≫
      limit.π (curry.obj (Prod.swap K J ⋙ G) ⋙ lim) k ≫ limit.π ((curry.obj (Prod.swap K J ⋙ G)).obj k) j =
    limit.π (curry.obj G ⋙ lim) j ≫ limit.π ((curry.obj G).obj j) k
[PROOFSTEP]
dsimp [limitCurrySwapCompLimIsoLimitCurryCompLim]
[GOAL]
J K : Type v
inst✝³ : SmallCategory J
inst✝² : SmallCategory K
C : Type u
inst✝¹ : Category.{v, u} C
F : J ⥤ K ⥤ C
G : J × K ⥤ C
inst✝ : HasLimits C
j : J
k : K
⊢ ((limitIsoLimitCurryCompLim G).inv ≫
        (HasLimit.isoOfEquivalence (Prod.braiding K J) (Iso.refl ((Prod.braiding K J).functor ⋙ G))).inv ≫
          (limitIsoLimitCurryCompLim (Prod.swap K J ⋙ G)).hom) ≫
      limit.π (curry.obj (Prod.swap K J ⋙ G) ⋙ lim) k ≫ limit.π ((curry.obj (Prod.swap K J ⋙ G)).obj k) j =
    limit.π (curry.obj G ⋙ lim) j ≫ limit.π ((curry.obj G).obj j) k
[PROOFSTEP]
simp only [Iso.refl_hom, Prod.braiding_counitIso_hom_app, Limits.HasLimit.isoOfEquivalence_inv_π, Iso.refl_inv,
  limitIsoLimitCurryCompLim_hom_π_π, eqToIso_refl, Category.assoc]
[GOAL]
J K : Type v
inst✝³ : SmallCategory J
inst✝² : SmallCategory K
C : Type u
inst✝¹ : Category.{v, u} C
F : J ⥤ K ⥤ C
G : J × K ⥤ C
inst✝ : HasLimits C
j : J
k : K
⊢ (limitIsoLimitCurryCompLim G).inv ≫
      limit.π G ((Prod.braiding K J).functor.obj (k, j)) ≫ NatTrans.app (𝟙 ((Prod.braiding K J).functor ⋙ G)) (k, j) =
    limit.π (curry.obj G ⋙ lim) j ≫ limit.π ((curry.obj G).obj j) k
[PROOFSTEP]
erw [NatTrans.id_app]
  -- Porting note: `simp` can do this in lean 4.
[GOAL]
J K : Type v
inst✝³ : SmallCategory J
inst✝² : SmallCategory K
C : Type u
inst✝¹ : Category.{v, u} C
F : J ⥤ K ⥤ C
G : J × K ⥤ C
inst✝ : HasLimits C
j : J
k : K
⊢ (limitIsoLimitCurryCompLim G).inv ≫
      limit.π G ((Prod.braiding K J).functor.obj (k, j)) ≫ 𝟙 (((Prod.braiding K J).functor ⋙ G).obj (k, j)) =
    limit.π (curry.obj G ⋙ lim) j ≫ limit.π ((curry.obj G).obj j) k
[PROOFSTEP]
simp
