[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


[GOAL]
J : Type v₁
⊢ IsConnected (WidePullbackShape J)
[PROOFSTEP]
apply IsConnected.of_induct
[GOAL]
case h
J : Type v₁
⊢ ∀ (p : Set (WidePullbackShape J)),
    ?j₀ ∈ p → (∀ {j₁ j₂ : WidePullbackShape J}, (j₁ ⟶ j₂) → (j₁ ∈ p ↔ j₂ ∈ p)) → ∀ (j : WidePullbackShape J), j ∈ p
case j₀ J : Type v₁ ⊢ WidePullbackShape J
[PROOFSTEP]
introv hp t
[GOAL]
case h
J : Type v₁
p : Set (WidePullbackShape J)
hp : ?j₀ ∈ p
t : ∀ {j₁ j₂ : WidePullbackShape J}, (j₁ ⟶ j₂) → (j₁ ∈ p ↔ j₂ ∈ p)
j : WidePullbackShape J
⊢ j ∈ p
case j₀ J : Type v₁ ⊢ WidePullbackShape J
[PROOFSTEP]
cases j
[GOAL]
case h.none
J : Type v₁
p : Set (WidePullbackShape J)
hp : ?j₀ ∈ p
t : ∀ {j₁ j₂ : WidePullbackShape J}, (j₁ ⟶ j₂) → (j₁ ∈ p ↔ j₂ ∈ p)
⊢ none ∈ p
[PROOFSTEP]
exact hp
[GOAL]
case h.some
J : Type v₁
p : Set (WidePullbackShape J)
hp : none ∈ p
t : ∀ {j₁ j₂ : WidePullbackShape J}, (j₁ ⟶ j₂) → (j₁ ∈ p ↔ j₂ ∈ p)
val✝ : J
⊢ some val✝ ∈ p
[PROOFSTEP]
rwa [t (WidePullbackShape.Hom.term _)]
[GOAL]
J : Type v₁
⊢ IsConnected (WidePushoutShape J)
[PROOFSTEP]
apply IsConnected.of_induct
[GOAL]
case h
J : Type v₁
⊢ ∀ (p : Set (WidePushoutShape J)),
    ?j₀ ∈ p → (∀ {j₁ j₂ : WidePushoutShape J}, (j₁ ⟶ j₂) → (j₁ ∈ p ↔ j₂ ∈ p)) → ∀ (j : WidePushoutShape J), j ∈ p
case j₀ J : Type v₁ ⊢ WidePushoutShape J
[PROOFSTEP]
introv hp t
[GOAL]
case h
J : Type v₁
p : Set (WidePushoutShape J)
hp : ?j₀ ∈ p
t : ∀ {j₁ j₂ : WidePushoutShape J}, (j₁ ⟶ j₂) → (j₁ ∈ p ↔ j₂ ∈ p)
j : WidePushoutShape J
⊢ j ∈ p
case j₀ J : Type v₁ ⊢ WidePushoutShape J
[PROOFSTEP]
cases j
[GOAL]
case h.none
J : Type v₁
p : Set (WidePushoutShape J)
hp : ?j₀ ∈ p
t : ∀ {j₁ j₂ : WidePushoutShape J}, (j₁ ⟶ j₂) → (j₁ ∈ p ↔ j₂ ∈ p)
⊢ none ∈ p
[PROOFSTEP]
exact hp
[GOAL]
case h.some
J : Type v₁
p : Set (WidePushoutShape J)
hp : none ∈ p
t : ∀ {j₁ j₂ : WidePushoutShape J}, (j₁ ⟶ j₂) → (j₁ ∈ p ↔ j₂ ∈ p)
val✝ : J
⊢ some val✝ ∈ p
[PROOFSTEP]
rwa [← t (WidePushoutShape.Hom.init _)]
[GOAL]
⊢ IsConnected WalkingParallelPair
[PROOFSTEP]
apply IsConnected.of_induct
[GOAL]
case h
⊢ ∀ (p : Set WalkingParallelPair),
    ?j₀ ∈ p → (∀ {j₁ j₂ : WalkingParallelPair}, (j₁ ⟶ j₂) → (j₁ ∈ p ↔ j₂ ∈ p)) → ∀ (j : WalkingParallelPair), j ∈ p
case j₀ ⊢ WalkingParallelPair
[PROOFSTEP]
introv _ t
[GOAL]
case h
p : Set WalkingParallelPair
a✝ : ?j₀ ∈ p
t : ∀ {j₁ j₂ : WalkingParallelPair}, (j₁ ⟶ j₂) → (j₁ ∈ p ↔ j₂ ∈ p)
j : WalkingParallelPair
⊢ j ∈ p
case j₀ ⊢ WalkingParallelPair
[PROOFSTEP]
cases j
[GOAL]
case h.zero
p : Set WalkingParallelPair
a✝ : ?j₀ ∈ p
t : ∀ {j₁ j₂ : WalkingParallelPair}, (j₁ ⟶ j₂) → (j₁ ∈ p ↔ j₂ ∈ p)
⊢ WalkingParallelPair.zero ∈ p
[PROOFSTEP]
rwa [t WalkingParallelPairHom.left]
[GOAL]
case h.one
p : Set WalkingParallelPair
a✝ : WalkingParallelPair.one ∈ p
t : ∀ {j₁ j₂ : WalkingParallelPair}, (j₁ ⟶ j₂) → (j₁ ∈ p ↔ j₂ ∈ p)
⊢ WalkingParallelPair.one ∈ p
[PROOFSTEP]
assumption
[GOAL]
C : Type u₂
inst✝³ : Category.{v₂, u₂} C
inst✝² : HasBinaryProducts C
J : Type v₂
inst✝¹ : SmallCategory J
inst✝ : IsConnected J
X : C
K : J ⥤ C
c : Cone K
l : IsLimit c
s : Cone (K ⋙ prod.functor.obj X)
j : J
⊢ (fun s => prod.lift (NatTrans.app s.π (Classical.arbitrary J) ≫ prod.fst) (IsLimit.lift l (forgetCone s))) s ≫
      NatTrans.app ((prod.functor.obj X).mapCone c).π j =
    NatTrans.app s.π j
[PROOFSTEP]
apply prod.hom_ext
[GOAL]
case h₁
C : Type u₂
inst✝³ : Category.{v₂, u₂} C
inst✝² : HasBinaryProducts C
J : Type v₂
inst✝¹ : SmallCategory J
inst✝ : IsConnected J
X : C
K : J ⥤ C
c : Cone K
l : IsLimit c
s : Cone (K ⋙ prod.functor.obj X)
j : J
⊢ ((fun s => prod.lift (NatTrans.app s.π (Classical.arbitrary J) ≫ prod.fst) (IsLimit.lift l (forgetCone s))) s ≫
        NatTrans.app ((prod.functor.obj X).mapCone c).π j) ≫
      prod.fst =
    NatTrans.app s.π j ≫ prod.fst
[PROOFSTEP]
erw [assoc, limMap_π, comp_id, limit.lift_π]
[GOAL]
case h₁
C : Type u₂
inst✝³ : Category.{v₂, u₂} C
inst✝² : HasBinaryProducts C
J : Type v₂
inst✝¹ : SmallCategory J
inst✝ : IsConnected J
X : C
K : J ⥤ C
c : Cone K
l : IsLimit c
s : Cone (K ⋙ prod.functor.obj X)
j : J
⊢ NatTrans.app (BinaryFan.mk (NatTrans.app s.π (Classical.arbitrary J) ≫ prod.fst) (IsLimit.lift l (forgetCone s))).π
      { as := WalkingPair.left } =
    NatTrans.app s.π j ≫ prod.fst
[PROOFSTEP]
exact (nat_trans_from_is_connected (s.π ≫ γ₁ X) j (Classical.arbitrary _)).symm
[GOAL]
case h₂
C : Type u₂
inst✝³ : Category.{v₂, u₂} C
inst✝² : HasBinaryProducts C
J : Type v₂
inst✝¹ : SmallCategory J
inst✝ : IsConnected J
X : C
K : J ⥤ C
c : Cone K
l : IsLimit c
s : Cone (K ⋙ prod.functor.obj X)
j : J
⊢ ((fun s => prod.lift (NatTrans.app s.π (Classical.arbitrary J) ≫ prod.fst) (IsLimit.lift l (forgetCone s))) s ≫
        NatTrans.app ((prod.functor.obj X).mapCone c).π j) ≫
      prod.snd =
    NatTrans.app s.π j ≫ prod.snd
[PROOFSTEP]
simp [← l.fac (forgetCone s) j]
[GOAL]
C : Type u₂
inst✝³ : Category.{v₂, u₂} C
inst✝² : HasBinaryProducts C
J : Type v₂
inst✝¹ : SmallCategory J
inst✝ : IsConnected J
X : C
K : J ⥤ C
c : Cone K
l : IsLimit c
s : Cone (K ⋙ prod.functor.obj X)
m : s.pt ⟶ ((prod.functor.obj X).mapCone c).pt
L : ∀ (j : J), m ≫ NatTrans.app ((prod.functor.obj X).mapCone c).π j = NatTrans.app s.π j
⊢ m = (fun s => prod.lift (NatTrans.app s.π (Classical.arbitrary J) ≫ prod.fst) (IsLimit.lift l (forgetCone s))) s
[PROOFSTEP]
apply prod.hom_ext
[GOAL]
case h₁
C : Type u₂
inst✝³ : Category.{v₂, u₂} C
inst✝² : HasBinaryProducts C
J : Type v₂
inst✝¹ : SmallCategory J
inst✝ : IsConnected J
X : C
K : J ⥤ C
c : Cone K
l : IsLimit c
s : Cone (K ⋙ prod.functor.obj X)
m : s.pt ⟶ ((prod.functor.obj X).mapCone c).pt
L : ∀ (j : J), m ≫ NatTrans.app ((prod.functor.obj X).mapCone c).π j = NatTrans.app s.π j
⊢ m ≫ prod.fst =
    (fun s => prod.lift (NatTrans.app s.π (Classical.arbitrary J) ≫ prod.fst) (IsLimit.lift l (forgetCone s))) s ≫
      prod.fst
[PROOFSTEP]
erw [limit.lift_π, ← L (Classical.arbitrary J), assoc, limMap_π, comp_id]
[GOAL]
case h₁
C : Type u₂
inst✝³ : Category.{v₂, u₂} C
inst✝² : HasBinaryProducts C
J : Type v₂
inst✝¹ : SmallCategory J
inst✝ : IsConnected J
X : C
K : J ⥤ C
c : Cone K
l : IsLimit c
s : Cone (K ⋙ prod.functor.obj X)
m : s.pt ⟶ ((prod.functor.obj X).mapCone c).pt
L : ∀ (j : J), m ≫ NatTrans.app ((prod.functor.obj X).mapCone c).π j = NatTrans.app s.π j
⊢ m ≫ prod.fst =
    NatTrans.app (BinaryFan.mk (m ≫ limit.π (pair X c.pt) { as := WalkingPair.left }) (IsLimit.lift l (forgetCone s))).π
      { as := WalkingPair.left }
[PROOFSTEP]
rfl
[GOAL]
case h₂
C : Type u₂
inst✝³ : Category.{v₂, u₂} C
inst✝² : HasBinaryProducts C
J : Type v₂
inst✝¹ : SmallCategory J
inst✝ : IsConnected J
X : C
K : J ⥤ C
c : Cone K
l : IsLimit c
s : Cone (K ⋙ prod.functor.obj X)
m : s.pt ⟶ ((prod.functor.obj X).mapCone c).pt
L : ∀ (j : J), m ≫ NatTrans.app ((prod.functor.obj X).mapCone c).π j = NatTrans.app s.π j
⊢ m ≫ prod.snd =
    (fun s => prod.lift (NatTrans.app s.π (Classical.arbitrary J) ≫ prod.fst) (IsLimit.lift l (forgetCone s))) s ≫
      prod.snd
[PROOFSTEP]
rw [limit.lift_π]
[GOAL]
case h₂
C : Type u₂
inst✝³ : Category.{v₂, u₂} C
inst✝² : HasBinaryProducts C
J : Type v₂
inst✝¹ : SmallCategory J
inst✝ : IsConnected J
X : C
K : J ⥤ C
c : Cone K
l : IsLimit c
s : Cone (K ⋙ prod.functor.obj X)
m : s.pt ⟶ ((prod.functor.obj X).mapCone c).pt
L : ∀ (j : J), m ≫ NatTrans.app ((prod.functor.obj X).mapCone c).π j = NatTrans.app s.π j
⊢ m ≫ prod.snd =
    NatTrans.app (BinaryFan.mk (NatTrans.app s.π (Classical.arbitrary J) ≫ prod.fst) (IsLimit.lift l (forgetCone s))).π
      { as := WalkingPair.right }
[PROOFSTEP]
apply l.uniq (forgetCone s)
[GOAL]
case h₂.x
C : Type u₂
inst✝³ : Category.{v₂, u₂} C
inst✝² : HasBinaryProducts C
J : Type v₂
inst✝¹ : SmallCategory J
inst✝ : IsConnected J
X : C
K : J ⥤ C
c : Cone K
l : IsLimit c
s : Cone (K ⋙ prod.functor.obj X)
m : s.pt ⟶ ((prod.functor.obj X).mapCone c).pt
L : ∀ (j : J), m ≫ NatTrans.app ((prod.functor.obj X).mapCone c).π j = NatTrans.app s.π j
⊢ ∀ (j : J), (m ≫ prod.snd) ≫ NatTrans.app c.π j = NatTrans.app (forgetCone s).π j
[PROOFSTEP]
intro j
[GOAL]
case h₂.x
C : Type u₂
inst✝³ : Category.{v₂, u₂} C
inst✝² : HasBinaryProducts C
J : Type v₂
inst✝¹ : SmallCategory J
inst✝ : IsConnected J
X : C
K : J ⥤ C
c : Cone K
l : IsLimit c
s : Cone (K ⋙ prod.functor.obj X)
m : s.pt ⟶ ((prod.functor.obj X).mapCone c).pt
L : ∀ (j : J), m ≫ NatTrans.app ((prod.functor.obj X).mapCone c).π j = NatTrans.app s.π j
j : J
⊢ (m ≫ prod.snd) ≫ NatTrans.app c.π j = NatTrans.app (forgetCone s).π j
[PROOFSTEP]
simp [← L j]


[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type w
inst✝¹ : Category.{w', w} J
K✝ K : J ⥤ C
F : C ⥤ D
inst✝ : ReflectsIsomorphisms F
h : (c : Cone (K ⋙ F)) → (t : IsLimit c) → LiftsToLimit K F c t
d : Cone K
hd : IsLimit (F.mapCone d)
⊢ IsLimit d
[PROOFSTEP]
let d' : Cone K := (h (F.mapCone d) hd).toLiftableCone.liftedCone
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type w
inst✝¹ : Category.{w', w} J
K✝ K : J ⥤ C
F : C ⥤ D
inst✝ : ReflectsIsomorphisms F
h : (c : Cone (K ⋙ F)) → (t : IsLimit c) → LiftsToLimit K F c t
d : Cone K
hd : IsLimit (F.mapCone d)
d' : Cone K := (h (F.mapCone d) hd).liftedCone
⊢ IsLimit d
[PROOFSTEP]
let i : F.mapCone d' ≅ F.mapCone d := (h (F.mapCone d) hd).toLiftableCone.validLift
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type w
inst✝¹ : Category.{w', w} J
K✝ K : J ⥤ C
F : C ⥤ D
inst✝ : ReflectsIsomorphisms F
h : (c : Cone (K ⋙ F)) → (t : IsLimit c) → LiftsToLimit K F c t
d : Cone K
hd : IsLimit (F.mapCone d)
d' : Cone K := (h (F.mapCone d) hd).liftedCone
i : F.mapCone d' ≅ F.mapCone d := (h (F.mapCone d) hd).validLift
⊢ IsLimit d
[PROOFSTEP]
let hd' : IsLimit d' := (h (F.mapCone d) hd).makesLimit
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type w
inst✝¹ : Category.{w', w} J
K✝ K : J ⥤ C
F : C ⥤ D
inst✝ : ReflectsIsomorphisms F
h : (c : Cone (K ⋙ F)) → (t : IsLimit c) → LiftsToLimit K F c t
d : Cone K
hd : IsLimit (F.mapCone d)
d' : Cone K := (h (F.mapCone d) hd).liftedCone
i : F.mapCone d' ≅ F.mapCone d := (h (F.mapCone d) hd).validLift
hd' : IsLimit d' := (h (F.mapCone d) hd).makesLimit
⊢ IsLimit d
[PROOFSTEP]
let f : d ⟶ d' := hd'.liftConeMorphism d
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type w
inst✝¹ : Category.{w', w} J
K✝ K : J ⥤ C
F : C ⥤ D
inst✝ : ReflectsIsomorphisms F
h : (c : Cone (K ⋙ F)) → (t : IsLimit c) → LiftsToLimit K F c t
d : Cone K
hd : IsLimit (F.mapCone d)
d' : Cone K := (h (F.mapCone d) hd).liftedCone
i : F.mapCone d' ≅ F.mapCone d := (h (F.mapCone d) hd).validLift
hd' : IsLimit d' := (h (F.mapCone d) hd).makesLimit
f : d ⟶ d' := IsLimit.liftConeMorphism hd' d
⊢ IsLimit d
[PROOFSTEP]
have : (Cones.functoriality K F).map f = i.inv := (hd.ofIsoLimit i.symm).uniq_cone_morphism
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type w
inst✝¹ : Category.{w', w} J
K✝ K : J ⥤ C
F : C ⥤ D
inst✝ : ReflectsIsomorphisms F
h : (c : Cone (K ⋙ F)) → (t : IsLimit c) → LiftsToLimit K F c t
d : Cone K
hd : IsLimit (F.mapCone d)
d' : Cone K := (h (F.mapCone d) hd).liftedCone
i : F.mapCone d' ≅ F.mapCone d := (h (F.mapCone d) hd).validLift
hd' : IsLimit d' := (h (F.mapCone d) hd).makesLimit
f : d ⟶ d' := IsLimit.liftConeMorphism hd' d
this : (Cones.functoriality K F).map f = i.inv
⊢ IsLimit d
[PROOFSTEP]
haveI : IsIso ((Cones.functoriality K F).map f) := by
  rw [this]
  infer_instance
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type w
inst✝¹ : Category.{w', w} J
K✝ K : J ⥤ C
F : C ⥤ D
inst✝ : ReflectsIsomorphisms F
h : (c : Cone (K ⋙ F)) → (t : IsLimit c) → LiftsToLimit K F c t
d : Cone K
hd : IsLimit (F.mapCone d)
d' : Cone K := (h (F.mapCone d) hd).liftedCone
i : F.mapCone d' ≅ F.mapCone d := (h (F.mapCone d) hd).validLift
hd' : IsLimit d' := (h (F.mapCone d) hd).makesLimit
f : d ⟶ d' := IsLimit.liftConeMorphism hd' d
this : (Cones.functoriality K F).map f = i.inv
⊢ IsIso ((Cones.functoriality K F).map f)
[PROOFSTEP]
rw [this]
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type w
inst✝¹ : Category.{w', w} J
K✝ K : J ⥤ C
F : C ⥤ D
inst✝ : ReflectsIsomorphisms F
h : (c : Cone (K ⋙ F)) → (t : IsLimit c) → LiftsToLimit K F c t
d : Cone K
hd : IsLimit (F.mapCone d)
d' : Cone K := (h (F.mapCone d) hd).liftedCone
i : F.mapCone d' ≅ F.mapCone d := (h (F.mapCone d) hd).validLift
hd' : IsLimit d' := (h (F.mapCone d) hd).makesLimit
f : d ⟶ d' := IsLimit.liftConeMorphism hd' d
this : (Cones.functoriality K F).map f = i.inv
⊢ IsIso i.inv
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type w
inst✝¹ : Category.{w', w} J
K✝ K : J ⥤ C
F : C ⥤ D
inst✝ : ReflectsIsomorphisms F
h : (c : Cone (K ⋙ F)) → (t : IsLimit c) → LiftsToLimit K F c t
d : Cone K
hd : IsLimit (F.mapCone d)
d' : Cone K := (h (F.mapCone d) hd).liftedCone
i : F.mapCone d' ≅ F.mapCone d := (h (F.mapCone d) hd).validLift
hd' : IsLimit d' := (h (F.mapCone d) hd).makesLimit
f : d ⟶ d' := IsLimit.liftConeMorphism hd' d
this✝ : (Cones.functoriality K F).map f = i.inv
this : IsIso ((Cones.functoriality K F).map f)
⊢ IsLimit d
[PROOFSTEP]
haveI : IsIso f := isIso_of_reflects_iso f (Cones.functoriality K F)
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type w
inst✝¹ : Category.{w', w} J
K✝ K : J ⥤ C
F : C ⥤ D
inst✝ : ReflectsIsomorphisms F
h : (c : Cone (K ⋙ F)) → (t : IsLimit c) → LiftsToLimit K F c t
d : Cone K
hd : IsLimit (F.mapCone d)
d' : Cone K := (h (F.mapCone d) hd).liftedCone
i : F.mapCone d' ≅ F.mapCone d := (h (F.mapCone d) hd).validLift
hd' : IsLimit d' := (h (F.mapCone d) hd).makesLimit
f : d ⟶ d' := IsLimit.liftConeMorphism hd' d
this✝¹ : (Cones.functoriality K F).map f = i.inv
this✝ : IsIso ((Cones.functoriality K F).map f)
this : IsIso f
⊢ IsLimit d
[PROOFSTEP]
exact IsLimit.ofIsoLimit hd' (asIso f).symm
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : Type w
inst✝² : Category.{w', w} J
K✝ K : J ⥤ C
F : C ⥤ D
inst✝¹ : Full F
inst✝ : Faithful F
l : Cone (K ⋙ F)
hl : IsLimit l
X : C
i : F.obj X ≅ l.pt
Y Z : J
f : Y ⟶ Z
⊢ F.map (((Functor.const J).obj X).map f ≫ (fun j => F.preimage (i.hom ≫ NatTrans.app l.π j)) Z) =
    F.map ((fun j => F.preimage (i.hom ≫ NatTrans.app l.π j)) Y ≫ K.map f)
[PROOFSTEP]
dsimp
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : Type w
inst✝² : Category.{w', w} J
K✝ K : J ⥤ C
F : C ⥤ D
inst✝¹ : Full F
inst✝ : Faithful F
l : Cone (K ⋙ F)
hl : IsLimit l
X : C
i : F.obj X ≅ l.pt
Y Z : J
f : Y ⟶ Z
⊢ F.map (𝟙 X ≫ F.preimage (i.hom ≫ NatTrans.app l.π Z)) = F.map (F.preimage (i.hom ≫ NatTrans.app l.π Y) ≫ K.map f)
[PROOFSTEP]
simpa using (l.w f).symm
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : Type w
inst✝² : Category.{w', w} J
K✝ K : J ⥤ C
F : C ⥤ D
inst✝¹ : Full F
inst✝ : Faithful F
l : Cone (K ⋙ F)
hl : IsLimit l
X : C
i : F.obj X ≅ l.pt
j : J
⊢ NatTrans.app (F.mapCone { pt := X, π := NatTrans.mk fun j => F.preimage (i.hom ≫ NatTrans.app l.π j) }).π j =
    i.hom ≫ NatTrans.app l.π j
[PROOFSTEP]
simp only [Functor.image_preimage, Functor.mapCone_π_app]
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type w
inst✝¹ : Category.{w', w} J
K✝ K : J ⥤ C
F : C ⥤ D
inst✝ : ReflectsIsomorphisms F
h : (c : Cocone (K ⋙ F)) → (t : IsColimit c) → LiftsToColimit K F c t
d : Cocone K
hd : IsColimit (F.mapCocone d)
⊢ IsColimit d
[PROOFSTEP]
let d' : Cocone K := (h (F.mapCocone d) hd).toLiftableCocone.liftedCocone
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type w
inst✝¹ : Category.{w', w} J
K✝ K : J ⥤ C
F : C ⥤ D
inst✝ : ReflectsIsomorphisms F
h : (c : Cocone (K ⋙ F)) → (t : IsColimit c) → LiftsToColimit K F c t
d : Cocone K
hd : IsColimit (F.mapCocone d)
d' : Cocone K := (h (F.mapCocone d) hd).liftedCocone
⊢ IsColimit d
[PROOFSTEP]
let i : F.mapCocone d' ≅ F.mapCocone d := (h (F.mapCocone d) hd).toLiftableCocone.validLift
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type w
inst✝¹ : Category.{w', w} J
K✝ K : J ⥤ C
F : C ⥤ D
inst✝ : ReflectsIsomorphisms F
h : (c : Cocone (K ⋙ F)) → (t : IsColimit c) → LiftsToColimit K F c t
d : Cocone K
hd : IsColimit (F.mapCocone d)
d' : Cocone K := (h (F.mapCocone d) hd).liftedCocone
i : F.mapCocone d' ≅ F.mapCocone d := (h (F.mapCocone d) hd).validLift
⊢ IsColimit d
[PROOFSTEP]
let hd' : IsColimit d' := (h (F.mapCocone d) hd).makesColimit
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type w
inst✝¹ : Category.{w', w} J
K✝ K : J ⥤ C
F : C ⥤ D
inst✝ : ReflectsIsomorphisms F
h : (c : Cocone (K ⋙ F)) → (t : IsColimit c) → LiftsToColimit K F c t
d : Cocone K
hd : IsColimit (F.mapCocone d)
d' : Cocone K := (h (F.mapCocone d) hd).liftedCocone
i : F.mapCocone d' ≅ F.mapCocone d := (h (F.mapCocone d) hd).validLift
hd' : IsColimit d' := (h (F.mapCocone d) hd).makesColimit
⊢ IsColimit d
[PROOFSTEP]
let f : d' ⟶ d := hd'.descCoconeMorphism d
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type w
inst✝¹ : Category.{w', w} J
K✝ K : J ⥤ C
F : C ⥤ D
inst✝ : ReflectsIsomorphisms F
h : (c : Cocone (K ⋙ F)) → (t : IsColimit c) → LiftsToColimit K F c t
d : Cocone K
hd : IsColimit (F.mapCocone d)
d' : Cocone K := (h (F.mapCocone d) hd).liftedCocone
i : F.mapCocone d' ≅ F.mapCocone d := (h (F.mapCocone d) hd).validLift
hd' : IsColimit d' := (h (F.mapCocone d) hd).makesColimit
f : d' ⟶ d := IsColimit.descCoconeMorphism hd' d
⊢ IsColimit d
[PROOFSTEP]
have : (Cocones.functoriality K F).map f = i.hom := (hd.ofIsoColimit i.symm).uniq_cocone_morphism
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type w
inst✝¹ : Category.{w', w} J
K✝ K : J ⥤ C
F : C ⥤ D
inst✝ : ReflectsIsomorphisms F
h : (c : Cocone (K ⋙ F)) → (t : IsColimit c) → LiftsToColimit K F c t
d : Cocone K
hd : IsColimit (F.mapCocone d)
d' : Cocone K := (h (F.mapCocone d) hd).liftedCocone
i : F.mapCocone d' ≅ F.mapCocone d := (h (F.mapCocone d) hd).validLift
hd' : IsColimit d' := (h (F.mapCocone d) hd).makesColimit
f : d' ⟶ d := IsColimit.descCoconeMorphism hd' d
this : (Cocones.functoriality K F).map f = i.hom
⊢ IsColimit d
[PROOFSTEP]
haveI : IsIso ((Cocones.functoriality K F).map f) := by
  rw [this]
  infer_instance
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type w
inst✝¹ : Category.{w', w} J
K✝ K : J ⥤ C
F : C ⥤ D
inst✝ : ReflectsIsomorphisms F
h : (c : Cocone (K ⋙ F)) → (t : IsColimit c) → LiftsToColimit K F c t
d : Cocone K
hd : IsColimit (F.mapCocone d)
d' : Cocone K := (h (F.mapCocone d) hd).liftedCocone
i : F.mapCocone d' ≅ F.mapCocone d := (h (F.mapCocone d) hd).validLift
hd' : IsColimit d' := (h (F.mapCocone d) hd).makesColimit
f : d' ⟶ d := IsColimit.descCoconeMorphism hd' d
this : (Cocones.functoriality K F).map f = i.hom
⊢ IsIso ((Cocones.functoriality K F).map f)
[PROOFSTEP]
rw [this]
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type w
inst✝¹ : Category.{w', w} J
K✝ K : J ⥤ C
F : C ⥤ D
inst✝ : ReflectsIsomorphisms F
h : (c : Cocone (K ⋙ F)) → (t : IsColimit c) → LiftsToColimit K F c t
d : Cocone K
hd : IsColimit (F.mapCocone d)
d' : Cocone K := (h (F.mapCocone d) hd).liftedCocone
i : F.mapCocone d' ≅ F.mapCocone d := (h (F.mapCocone d) hd).validLift
hd' : IsColimit d' := (h (F.mapCocone d) hd).makesColimit
f : d' ⟶ d := IsColimit.descCoconeMorphism hd' d
this : (Cocones.functoriality K F).map f = i.hom
⊢ IsIso i.hom
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type w
inst✝¹ : Category.{w', w} J
K✝ K : J ⥤ C
F : C ⥤ D
inst✝ : ReflectsIsomorphisms F
h : (c : Cocone (K ⋙ F)) → (t : IsColimit c) → LiftsToColimit K F c t
d : Cocone K
hd : IsColimit (F.mapCocone d)
d' : Cocone K := (h (F.mapCocone d) hd).liftedCocone
i : F.mapCocone d' ≅ F.mapCocone d := (h (F.mapCocone d) hd).validLift
hd' : IsColimit d' := (h (F.mapCocone d) hd).makesColimit
f : d' ⟶ d := IsColimit.descCoconeMorphism hd' d
this✝ : (Cocones.functoriality K F).map f = i.hom
this : IsIso ((Cocones.functoriality K F).map f)
⊢ IsColimit d
[PROOFSTEP]
haveI := isIso_of_reflects_iso f (Cocones.functoriality K F)
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type w
inst✝¹ : Category.{w', w} J
K✝ K : J ⥤ C
F : C ⥤ D
inst✝ : ReflectsIsomorphisms F
h : (c : Cocone (K ⋙ F)) → (t : IsColimit c) → LiftsToColimit K F c t
d : Cocone K
hd : IsColimit (F.mapCocone d)
d' : Cocone K := (h (F.mapCocone d) hd).liftedCocone
i : F.mapCocone d' ≅ F.mapCocone d := (h (F.mapCocone d) hd).validLift
hd' : IsColimit d' := (h (F.mapCocone d) hd).makesColimit
f : d' ⟶ d := IsColimit.descCoconeMorphism hd' d
this✝¹ : (Cocones.functoriality K F).map f = i.hom
this✝ : IsIso ((Cocones.functoriality K F).map f)
this : IsIso f
⊢ IsColimit d
[PROOFSTEP]
exact IsColimit.ofIsoColimit hd' (asIso f)
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : Type w
inst✝² : Category.{w', w} J
K✝ K : J ⥤ C
F : C ⥤ D
inst✝¹ : Full F
inst✝ : Faithful F
l : Cocone (K ⋙ F)
hl : IsColimit l
X : C
i : F.obj X ≅ l.pt
Y Z : J
f : Y ⟶ Z
⊢ F.map (K.map f ≫ (fun j => F.preimage (NatTrans.app l.ι j ≫ i.inv)) Z) =
    F.map ((fun j => F.preimage (NatTrans.app l.ι j ≫ i.inv)) Y ≫ ((Functor.const J).obj X).map f)
[PROOFSTEP]
dsimp
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : Type w
inst✝² : Category.{w', w} J
K✝ K : J ⥤ C
F : C ⥤ D
inst✝¹ : Full F
inst✝ : Faithful F
l : Cocone (K ⋙ F)
hl : IsColimit l
X : C
i : F.obj X ≅ l.pt
Y Z : J
f : Y ⟶ Z
⊢ F.map (K.map f ≫ F.preimage (NatTrans.app l.ι Z ≫ i.inv)) = F.map (F.preimage (NatTrans.app l.ι Y ≫ i.inv) ≫ 𝟙 X)
[PROOFSTEP]
simpa [← cancel_mono i.hom] using l.w f
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : Type w
inst✝² : Category.{w', w} J
K✝ K : J ⥤ C
F : C ⥤ D
inst✝¹ : Full F
inst✝ : Faithful F
l : Cocone (K ⋙ F)
hl : IsColimit l
X : C
i : F.obj X ≅ l.pt
j : J
⊢ NatTrans.app (F.mapCocone { pt := X, ι := NatTrans.mk fun j => F.preimage (NatTrans.app l.ι j ≫ i.inv) }).ι j ≫
      i.hom =
    NatTrans.app l.ι j
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type w
inst✝¹ : Category.{w', w} J
K K₁ K₂ : J ⥤ C
F : C ⥤ D
h : K₁ ≅ K₂
inst✝ : CreatesLimit K₁ F
src✝ : ReflectsLimit K₂ F := reflectsLimitOfIsoDiagram F h
c : Cone (K₂ ⋙ F)
t : IsLimit c
t' : (fun x => IsLimit ((Cones.postcompose (isoWhiskerRight h F).inv).obj c)) t :=
  ↑(IsLimit.postcomposeInvEquiv (isoWhiskerRight h F) c).symm t
j : J
⊢ NatTrans.app
      ((Cones.postcompose (isoWhiskerRight h F).hom).obj ((Cones.postcompose (isoWhiskerRight h F).inv).obj c)).π j =
    (Iso.refl
          ((Cones.postcompose (isoWhiskerRight h F).hom).obj
              ((Cones.postcompose (isoWhiskerRight h F).inv).obj c)).pt).hom ≫
      NatTrans.app c.π j
[PROOFSTEP]
dsimp
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type w
inst✝¹ : Category.{w', w} J
K K₁ K₂ : J ⥤ C
F : C ⥤ D
h : K₁ ≅ K₂
inst✝ : CreatesLimit K₁ F
src✝ : ReflectsLimit K₂ F := reflectsLimitOfIsoDiagram F h
c : Cone (K₂ ⋙ F)
t : IsLimit c
t' : (fun x => IsLimit ((Cones.postcompose (isoWhiskerRight h F).inv).obj c)) t :=
  ↑(IsLimit.postcomposeInvEquiv (isoWhiskerRight h F) c).symm t
j : J
⊢ (NatTrans.app c.π j ≫ F.map (NatTrans.app h.inv j)) ≫ F.map (NatTrans.app h.hom j) = 𝟙 c.pt ≫ NatTrans.app c.π j
[PROOFSTEP]
rw [Category.assoc, ← F.map_comp]
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type w
inst✝¹ : Category.{w', w} J
K K₁ K₂ : J ⥤ C
F : C ⥤ D
h : K₁ ≅ K₂
inst✝ : CreatesLimit K₁ F
src✝ : ReflectsLimit K₂ F := reflectsLimitOfIsoDiagram F h
c : Cone (K₂ ⋙ F)
t : IsLimit c
t' : (fun x => IsLimit ((Cones.postcompose (isoWhiskerRight h F).inv).obj c)) t :=
  ↑(IsLimit.postcomposeInvEquiv (isoWhiskerRight h F) c).symm t
j : J
⊢ NatTrans.app c.π j ≫ F.map (NatTrans.app h.inv j ≫ NatTrans.app h.hom j) = 𝟙 c.pt ≫ NatTrans.app c.π j
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type w
inst✝¹ : Category.{w', w} J
K : J ⥤ C
F G : C ⥤ D
h : F ≅ G
inst✝ : CreatesLimit K F
c : Cone (K ⋙ G)
t : IsLimit c
⊢ G.mapCone (liftLimit (↑(IsLimit.postcomposeInvEquiv (isoWhiskerLeft K h) c).symm t)) ≅ c
[PROOFSTEP]
refine' (IsLimit.mapConeEquiv h _).uniqueUpToIso t
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type w
inst✝¹ : Category.{w', w} J
K : J ⥤ C
F G : C ⥤ D
h : F ≅ G
inst✝ : CreatesLimit K F
c : Cone (K ⋙ G)
t : IsLimit c
⊢ IsLimit (F.mapCone (liftLimit (↑(IsLimit.postcomposeInvEquiv (isoWhiskerLeft K h) c).symm t)))
[PROOFSTEP]
apply IsLimit.ofIsoLimit _ (liftedLimitMapsToOriginal _).symm
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type w
inst✝¹ : Category.{w', w} J
K : J ⥤ C
F G : C ⥤ D
h : F ≅ G
inst✝ : CreatesLimit K F
c : Cone (K ⋙ G)
t : IsLimit c
⊢ IsLimit ((Cones.postcompose (isoWhiskerLeft K h).inv).obj c)
[PROOFSTEP]
apply (IsLimit.postcomposeInvEquiv _ _).symm t
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type w
inst✝¹ : Category.{w', w} J
K K₁ K₂ : J ⥤ C
F : C ⥤ D
h : K₁ ≅ K₂
inst✝ : CreatesColimit K₁ F
src✝ : ReflectsColimit K₂ F := reflectsColimitOfIsoDiagram F h
c : Cocone (K₂ ⋙ F)
t : IsColimit c
t' : (fun x => IsColimit ((Cocones.precompose (isoWhiskerRight h F).hom).obj c)) t :=
  ↑(IsColimit.precomposeHomEquiv (isoWhiskerRight h F) c).symm t
j : J
⊢ NatTrans.app
        ((Cocones.precompose (isoWhiskerRight h F).inv).obj ((Cocones.precompose (isoWhiskerRight h F).hom).obj c)).ι
        j ≫
      (Iso.refl
          ((Cocones.precompose (isoWhiskerRight h F).inv).obj
              ((Cocones.precompose (isoWhiskerRight h F).hom).obj c)).pt).hom =
    NatTrans.app c.ι j
[PROOFSTEP]
dsimp
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type w
inst✝¹ : Category.{w', w} J
K K₁ K₂ : J ⥤ C
F : C ⥤ D
h : K₁ ≅ K₂
inst✝ : CreatesColimit K₁ F
src✝ : ReflectsColimit K₂ F := reflectsColimitOfIsoDiagram F h
c : Cocone (K₂ ⋙ F)
t : IsColimit c
t' : (fun x => IsColimit ((Cocones.precompose (isoWhiskerRight h F).hom).obj c)) t :=
  ↑(IsColimit.precomposeHomEquiv (isoWhiskerRight h F) c).symm t
j : J
⊢ (F.map (NatTrans.app h.inv j) ≫ F.map (NatTrans.app h.hom j) ≫ NatTrans.app c.ι j) ≫ 𝟙 c.pt = NatTrans.app c.ι j
[PROOFSTEP]
rw [← F.map_comp_assoc]
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type w
inst✝¹ : Category.{w', w} J
K K₁ K₂ : J ⥤ C
F : C ⥤ D
h : K₁ ≅ K₂
inst✝ : CreatesColimit K₁ F
src✝ : ReflectsColimit K₂ F := reflectsColimitOfIsoDiagram F h
c : Cocone (K₂ ⋙ F)
t : IsColimit c
t' : (fun x => IsColimit ((Cocones.precompose (isoWhiskerRight h F).hom).obj c)) t :=
  ↑(IsColimit.precomposeHomEquiv (isoWhiskerRight h F) c).symm t
j : J
⊢ (F.map (NatTrans.app h.inv j ≫ NatTrans.app h.hom j) ≫ NatTrans.app c.ι j) ≫ 𝟙 c.pt = NatTrans.app c.ι j
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type w
inst✝¹ : Category.{w', w} J
K : J ⥤ C
F G : C ⥤ D
h : F ≅ G
inst✝ : CreatesColimit K F
c : Cocone (K ⋙ G)
t : IsColimit c
⊢ G.mapCocone (liftColimit (↑(IsColimit.precomposeHomEquiv (isoWhiskerLeft K h) c).symm t)) ≅ c
[PROOFSTEP]
refine' (IsColimit.mapCoconeEquiv h _).uniqueUpToIso t
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type w
inst✝¹ : Category.{w', w} J
K : J ⥤ C
F G : C ⥤ D
h : F ≅ G
inst✝ : CreatesColimit K F
c : Cocone (K ⋙ G)
t : IsColimit c
⊢ IsColimit (F.mapCocone (liftColimit (↑(IsColimit.precomposeHomEquiv (isoWhiskerLeft K h) c).symm t)))
[PROOFSTEP]
apply IsColimit.ofIsoColimit _ (liftedColimitMapsToOriginal _).symm
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type w
inst✝¹ : Category.{w', w} J
K : J ⥤ C
F G : C ⥤ D
h : F ≅ G
inst✝ : CreatesColimit K F
c : Cocone (K ⋙ G)
t : IsColimit c
⊢ IsColimit ((Cocones.precompose (isoWhiskerLeft K h).hom).obj c)
[PROOFSTEP]
apply (IsColimit.precomposeHomEquiv _ _).symm t
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : Type w
inst✝² : Category.{w', w} J
K : J ⥤ C
E : Type u₃
ℰ : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ E
inst✝¹ : CreatesLimit K F
inst✝ : CreatesLimit (K ⋙ F) G
c : Cone (K ⋙ F ⋙ G)
t : IsLimit c
⊢ LiftableCone K (F ⋙ G) c
[PROOFSTEP]
let c' : Cone ((K ⋙ F) ⋙ G) := c
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : Type w
inst✝² : Category.{w', w} J
K : J ⥤ C
E : Type u₃
ℰ : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ E
inst✝¹ : CreatesLimit K F
inst✝ : CreatesLimit (K ⋙ F) G
c : Cone (K ⋙ F ⋙ G)
t : IsLimit c
c' : Cone ((K ⋙ F) ⋙ G) := c
⊢ LiftableCone K (F ⋙ G) c
[PROOFSTEP]
let t' : IsLimit c' := t
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : Type w
inst✝² : Category.{w', w} J
K : J ⥤ C
E : Type u₃
ℰ : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ E
inst✝¹ : CreatesLimit K F
inst✝ : CreatesLimit (K ⋙ F) G
c : Cone (K ⋙ F ⋙ G)
t : IsLimit c
c' : Cone ((K ⋙ F) ⋙ G) := c
t' : IsLimit c' := t
⊢ LiftableCone K (F ⋙ G) c
[PROOFSTEP]
exact
  { liftedCone := liftLimit (liftedLimitIsLimit t')
    validLift :=
      (Cones.functoriality (K ⋙ F) G).mapIso (liftedLimitMapsToOriginal (liftedLimitIsLimit t')) ≪≫
        liftedLimitMapsToOriginal t' }


[GOAL]
I : Type v₁
C : I → Type u₁
inst✝¹ : (i : I) → Category.{v₁, u₁} (C i)
J : Type v₁
inst✝ : SmallCategory J
F : J ⥤ ((i : I) → C i)
c : (i : I) → Cone (F ⋙ Pi.eval C i)
j j' : J
f : j ⟶ j'
⊢ ((Functor.const J).obj fun i => (c i).pt).map f ≫ (fun j i => NatTrans.app (c i).π j) j' =
    (fun j i => NatTrans.app (c i).π j) j ≫ F.map f
[PROOFSTEP]
funext i
[GOAL]
case h
I : Type v₁
C : I → Type u₁
inst✝¹ : (i : I) → Category.{v₁, u₁} (C i)
J : Type v₁
inst✝ : SmallCategory J
F : J ⥤ ((i : I) → C i)
c : (i : I) → Cone (F ⋙ Pi.eval C i)
j j' : J
f : j ⟶ j'
i : I
⊢ (((Functor.const J).obj fun i => (c i).pt).map f ≫ (fun j i => NatTrans.app (c i).π j) j') i =
    ((fun j i => NatTrans.app (c i).π j) j ≫ F.map f) i
[PROOFSTEP]
exact (c i).π.naturality f
[GOAL]
I : Type v₁
C : I → Type u₁
inst✝¹ : (i : I) → Category.{v₁, u₁} (C i)
J : Type v₁
inst✝ : SmallCategory J
F : J ⥤ ((i : I) → C i)
c : (i : I) → Cocone (F ⋙ Pi.eval C i)
j j' : J
f : j ⟶ j'
⊢ F.map f ≫ (fun j i => NatTrans.app (c i).ι j) j' =
    (fun j i => NatTrans.app (c i).ι j) j ≫ ((Functor.const J).obj fun i => (c i).pt).map f
[PROOFSTEP]
funext i
[GOAL]
case h
I : Type v₁
C : I → Type u₁
inst✝¹ : (i : I) → Category.{v₁, u₁} (C i)
J : Type v₁
inst✝ : SmallCategory J
F : J ⥤ ((i : I) → C i)
c : (i : I) → Cocone (F ⋙ Pi.eval C i)
j j' : J
f : j ⟶ j'
i : I
⊢ (F.map f ≫ (fun j i => NatTrans.app (c i).ι j) j') i =
    ((fun j i => NatTrans.app (c i).ι j) j ≫ ((Functor.const J).obj fun i => (c i).pt).map f) i
[PROOFSTEP]
exact (c i).ι.naturality f
[GOAL]
I : Type v₁
C : I → Type u₁
inst✝¹ : (i : I) → Category.{v₁, u₁} (C i)
J : Type v₁
inst✝ : SmallCategory J
F : J ⥤ ((i : I) → C i)
c : (i : I) → Cone (F ⋙ Pi.eval C i)
P : (i : I) → IsLimit (c i)
s : Cone F
j : J
⊢ (fun s i => IsLimit.lift (P i) (coneCompEval s i)) s ≫ NatTrans.app (coneOfConeCompEval c).π j = NatTrans.app s.π j
[PROOFSTEP]
funext i
[GOAL]
case h
I : Type v₁
C : I → Type u₁
inst✝¹ : (i : I) → Category.{v₁, u₁} (C i)
J : Type v₁
inst✝ : SmallCategory J
F : J ⥤ ((i : I) → C i)
c : (i : I) → Cone (F ⋙ Pi.eval C i)
P : (i : I) → IsLimit (c i)
s : Cone F
j : J
i : I
⊢ ((fun s i => IsLimit.lift (P i) (coneCompEval s i)) s ≫ NatTrans.app (coneOfConeCompEval c).π j) i =
    NatTrans.app s.π j i
[PROOFSTEP]
exact (P i).fac (coneCompEval s i) j
[GOAL]
I : Type v₁
C : I → Type u₁
inst✝¹ : (i : I) → Category.{v₁, u₁} (C i)
J : Type v₁
inst✝ : SmallCategory J
F : J ⥤ ((i : I) → C i)
c : (i : I) → Cone (F ⋙ Pi.eval C i)
P : (i : I) → IsLimit (c i)
s : Cone F
m : s.pt ⟶ (coneOfConeCompEval c).pt
w : ∀ (j : J), m ≫ NatTrans.app (coneOfConeCompEval c).π j = NatTrans.app s.π j
⊢ m = (fun s i => IsLimit.lift (P i) (coneCompEval s i)) s
[PROOFSTEP]
funext i
[GOAL]
case h
I : Type v₁
C : I → Type u₁
inst✝¹ : (i : I) → Category.{v₁, u₁} (C i)
J : Type v₁
inst✝ : SmallCategory J
F : J ⥤ ((i : I) → C i)
c : (i : I) → Cone (F ⋙ Pi.eval C i)
P : (i : I) → IsLimit (c i)
s : Cone F
m : s.pt ⟶ (coneOfConeCompEval c).pt
w : ∀ (j : J), m ≫ NatTrans.app (coneOfConeCompEval c).π j = NatTrans.app s.π j
i : I
⊢ m i = (fun s i => IsLimit.lift (P i) (coneCompEval s i)) s i
[PROOFSTEP]
exact (P i).uniq (coneCompEval s i) (m i) fun j => congr_fun (w j) i
[GOAL]
I : Type v₁
C : I → Type u₁
inst✝¹ : (i : I) → Category.{v₁, u₁} (C i)
J : Type v₁
inst✝ : SmallCategory J
F : J ⥤ ((i : I) → C i)
c : (i : I) → Cocone (F ⋙ Pi.eval C i)
P : (i : I) → IsColimit (c i)
s : Cocone F
j : J
⊢ NatTrans.app (coconeOfCoconeCompEval c).ι j ≫ (fun s i => IsColimit.desc (P i) (coconeCompEval s i)) s =
    NatTrans.app s.ι j
[PROOFSTEP]
funext i
[GOAL]
case h
I : Type v₁
C : I → Type u₁
inst✝¹ : (i : I) → Category.{v₁, u₁} (C i)
J : Type v₁
inst✝ : SmallCategory J
F : J ⥤ ((i : I) → C i)
c : (i : I) → Cocone (F ⋙ Pi.eval C i)
P : (i : I) → IsColimit (c i)
s : Cocone F
j : J
i : I
⊢ (NatTrans.app (coconeOfCoconeCompEval c).ι j ≫ (fun s i => IsColimit.desc (P i) (coconeCompEval s i)) s) i =
    NatTrans.app s.ι j i
[PROOFSTEP]
exact (P i).fac (coconeCompEval s i) j
[GOAL]
I : Type v₁
C : I → Type u₁
inst✝¹ : (i : I) → Category.{v₁, u₁} (C i)
J : Type v₁
inst✝ : SmallCategory J
F : J ⥤ ((i : I) → C i)
c : (i : I) → Cocone (F ⋙ Pi.eval C i)
P : (i : I) → IsColimit (c i)
s : Cocone F
m : (coconeOfCoconeCompEval c).pt ⟶ s.pt
w : ∀ (j : J), NatTrans.app (coconeOfCoconeCompEval c).ι j ≫ m = NatTrans.app s.ι j
⊢ m = (fun s i => IsColimit.desc (P i) (coconeCompEval s i)) s
[PROOFSTEP]
funext i
[GOAL]
case h
I : Type v₁
C : I → Type u₁
inst✝¹ : (i : I) → Category.{v₁, u₁} (C i)
J : Type v₁
inst✝ : SmallCategory J
F : J ⥤ ((i : I) → C i)
c : (i : I) → Cocone (F ⋙ Pi.eval C i)
P : (i : I) → IsColimit (c i)
s : Cocone F
m : (coconeOfCoconeCompEval c).pt ⟶ s.pt
w : ∀ (j : J), NatTrans.app (coconeOfCoconeCompEval c).ι j ≫ m = NatTrans.app s.ι j
i : I
⊢ m i = (fun s i => IsColimit.desc (P i) (coconeCompEval s i)) s i
[PROOFSTEP]
exact (P i).uniq (coconeCompEval s i) (m i) fun j => congr_fun (w j) i


[GOAL]
C : Type u
inst✝¹ : SmallCategory C
inst✝ : HasProducts C
X Y : C
r s : X ⟶ Y
⊢ r = s
[PROOFSTEP]
classical
by_contra r_ne_s
have z : (2 : Cardinal) ≤ #(X ⟶ Y) := by
  rw [Cardinal.two_le_iff]
  exact ⟨_, _, r_ne_s⟩
let md := Σ Z W : C, Z ⟶ W
let α := #md
apply not_le_of_lt (Cardinal.cantor α)
let yp : C := ∏ fun _ : md => Y
refine' _root_.trans _ _
· exact #(X ⟶ yp)
· apply le_trans (Cardinal.power_le_power_right z)
  rw [Cardinal.power_def]
  apply le_of_eq
  rw [Cardinal.eq]
  refine' ⟨⟨Pi.lift, fun f k => f ≫ Pi.π _ k, _, _⟩⟩
  · intro f
    ext k
    simp
  · intro f
    ext ⟨j⟩
    simp
· apply Cardinal.mk_le_of_injective _
  · intro f
    exact ⟨_, _, f⟩
  · rintro f g k
    cases k
    rfl
[GOAL]
C : Type u
inst✝¹ : SmallCategory C
inst✝ : HasProducts C
X Y : C
r s : X ⟶ Y
⊢ r = s
[PROOFSTEP]
by_contra r_ne_s
[GOAL]
C : Type u
inst✝¹ : SmallCategory C
inst✝ : HasProducts C
X Y : C
r s : X ⟶ Y
r_ne_s : ¬r = s
⊢ False
[PROOFSTEP]
have z : (2 : Cardinal) ≤ #(X ⟶ Y) := by
  rw [Cardinal.two_le_iff]
  exact ⟨_, _, r_ne_s⟩
[GOAL]
C : Type u
inst✝¹ : SmallCategory C
inst✝ : HasProducts C
X Y : C
r s : X ⟶ Y
r_ne_s : ¬r = s
⊢ 2 ≤ #(X ⟶ Y)
[PROOFSTEP]
rw [Cardinal.two_le_iff]
[GOAL]
C : Type u
inst✝¹ : SmallCategory C
inst✝ : HasProducts C
X Y : C
r s : X ⟶ Y
r_ne_s : ¬r = s
⊢ ∃ x y, x ≠ y
[PROOFSTEP]
exact ⟨_, _, r_ne_s⟩
[GOAL]
C : Type u
inst✝¹ : SmallCategory C
inst✝ : HasProducts C
X Y : C
r s : X ⟶ Y
r_ne_s : ¬r = s
z : 2 ≤ #(X ⟶ Y)
⊢ False
[PROOFSTEP]
let md := Σ Z W : C, Z ⟶ W
[GOAL]
C : Type u
inst✝¹ : SmallCategory C
inst✝ : HasProducts C
X Y : C
r s : X ⟶ Y
r_ne_s : ¬r = s
z : 2 ≤ #(X ⟶ Y)
md : Type u := (Z : C) × (W : C) × (Z ⟶ W)
⊢ False
[PROOFSTEP]
let α := #md
[GOAL]
C : Type u
inst✝¹ : SmallCategory C
inst✝ : HasProducts C
X Y : C
r s : X ⟶ Y
r_ne_s : ¬r = s
z : 2 ≤ #(X ⟶ Y)
md : Type u := (Z : C) × (W : C) × (Z ⟶ W)
α : Cardinal.{u} := #md
⊢ False
[PROOFSTEP]
apply not_le_of_lt (Cardinal.cantor α)
[GOAL]
C : Type u
inst✝¹ : SmallCategory C
inst✝ : HasProducts C
X Y : C
r s : X ⟶ Y
r_ne_s : ¬r = s
z : 2 ≤ #(X ⟶ Y)
md : Type u := (Z : C) × (W : C) × (Z ⟶ W)
α : Cardinal.{u} := #md
⊢ 2 ^ α ≤ α
[PROOFSTEP]
let yp : C := ∏ fun _ : md => Y
[GOAL]
C : Type u
inst✝¹ : SmallCategory C
inst✝ : HasProducts C
X Y : C
r s : X ⟶ Y
r_ne_s : ¬r = s
z : 2 ≤ #(X ⟶ Y)
md : Type u := (Z : C) × (W : C) × (Z ⟶ W)
α : Cardinal.{u} := #md
yp : C := ∏ fun x => Y
⊢ 2 ^ α ≤ α
[PROOFSTEP]
refine' _root_.trans _ _
[GOAL]
case refine'_1
C : Type u
inst✝¹ : SmallCategory C
inst✝ : HasProducts C
X Y : C
r s : X ⟶ Y
r_ne_s : ¬r = s
z : 2 ≤ #(X ⟶ Y)
md : Type u := (Z : C) × (W : C) × (Z ⟶ W)
α : Cardinal.{u} := #md
yp : C := ∏ fun x => Y
⊢ Cardinal.{u}
[PROOFSTEP]
exact #(X ⟶ yp)
[GOAL]
case refine'_2
C : Type u
inst✝¹ : SmallCategory C
inst✝ : HasProducts C
X Y : C
r s : X ⟶ Y
r_ne_s : ¬r = s
z : 2 ≤ #(X ⟶ Y)
md : Type u := (Z : C) × (W : C) × (Z ⟶ W)
α : Cardinal.{u} := #md
yp : C := ∏ fun x => Y
⊢ 2 ^ α ≤ #(X ⟶ yp)
[PROOFSTEP]
apply le_trans (Cardinal.power_le_power_right z)
[GOAL]
case refine'_2
C : Type u
inst✝¹ : SmallCategory C
inst✝ : HasProducts C
X Y : C
r s : X ⟶ Y
r_ne_s : ¬r = s
z : 2 ≤ #(X ⟶ Y)
md : Type u := (Z : C) × (W : C) × (Z ⟶ W)
α : Cardinal.{u} := #md
yp : C := ∏ fun x => Y
⊢ #(X ⟶ Y) ^ α ≤ #(X ⟶ yp)
[PROOFSTEP]
rw [Cardinal.power_def]
[GOAL]
case refine'_2
C : Type u
inst✝¹ : SmallCategory C
inst✝ : HasProducts C
X Y : C
r s : X ⟶ Y
r_ne_s : ¬r = s
z : 2 ≤ #(X ⟶ Y)
md : Type u := (Z : C) × (W : C) × (Z ⟶ W)
α : Cardinal.{u} := #md
yp : C := ∏ fun x => Y
⊢ #(md → (X ⟶ Y)) ≤ #(X ⟶ yp)
[PROOFSTEP]
apply le_of_eq
[GOAL]
case refine'_2.a
C : Type u
inst✝¹ : SmallCategory C
inst✝ : HasProducts C
X Y : C
r s : X ⟶ Y
r_ne_s : ¬r = s
z : 2 ≤ #(X ⟶ Y)
md : Type u := (Z : C) × (W : C) × (Z ⟶ W)
α : Cardinal.{u} := #md
yp : C := ∏ fun x => Y
⊢ #(md → (X ⟶ Y)) = #(X ⟶ yp)
[PROOFSTEP]
rw [Cardinal.eq]
[GOAL]
case refine'_2.a
C : Type u
inst✝¹ : SmallCategory C
inst✝ : HasProducts C
X Y : C
r s : X ⟶ Y
r_ne_s : ¬r = s
z : 2 ≤ #(X ⟶ Y)
md : Type u := (Z : C) × (W : C) × (Z ⟶ W)
α : Cardinal.{u} := #md
yp : C := ∏ fun x => Y
⊢ Nonempty ((md → (X ⟶ Y)) ≃ (X ⟶ yp))
[PROOFSTEP]
refine' ⟨⟨Pi.lift, fun f k => f ≫ Pi.π _ k, _, _⟩⟩
[GOAL]
case refine'_2.a.refine'_1
C : Type u
inst✝¹ : SmallCategory C
inst✝ : HasProducts C
X Y : C
r s : X ⟶ Y
r_ne_s : ¬r = s
z : 2 ≤ #(X ⟶ Y)
md : Type u := (Z : C) × (W : C) × (Z ⟶ W)
α : Cardinal.{u} := #md
yp : C := ∏ fun x => Y
⊢ Function.LeftInverse (fun f k => f ≫ Pi.π (fun x => Y) k) Pi.lift
[PROOFSTEP]
intro f
[GOAL]
case refine'_2.a.refine'_1
C : Type u
inst✝¹ : SmallCategory C
inst✝ : HasProducts C
X Y : C
r s : X ⟶ Y
r_ne_s : ¬r = s
z : 2 ≤ #(X ⟶ Y)
md : Type u := (Z : C) × (W : C) × (Z ⟶ W)
α : Cardinal.{u} := #md
yp : C := ∏ fun x => Y
f : md → (X ⟶ Y)
⊢ (fun f k => f ≫ Pi.π (fun x => Y) k) (Pi.lift f) = f
[PROOFSTEP]
ext k
[GOAL]
case refine'_2.a.refine'_1.h
C : Type u
inst✝¹ : SmallCategory C
inst✝ : HasProducts C
X Y : C
r s : X ⟶ Y
r_ne_s : ¬r = s
z : 2 ≤ #(X ⟶ Y)
md : Type u := (Z : C) × (W : C) × (Z ⟶ W)
α : Cardinal.{u} := #md
yp : C := ∏ fun x => Y
f : md → (X ⟶ Y)
k : md
⊢ (fun f k => f ≫ Pi.π (fun x => Y) k) (Pi.lift f) k = f k
[PROOFSTEP]
simp
[GOAL]
case refine'_2.a.refine'_2
C : Type u
inst✝¹ : SmallCategory C
inst✝ : HasProducts C
X Y : C
r s : X ⟶ Y
r_ne_s : ¬r = s
z : 2 ≤ #(X ⟶ Y)
md : Type u := (Z : C) × (W : C) × (Z ⟶ W)
α : Cardinal.{u} := #md
yp : C := ∏ fun x => Y
⊢ Function.RightInverse (fun f k => f ≫ Pi.π (fun x => Y) k) Pi.lift
[PROOFSTEP]
intro f
[GOAL]
case refine'_2.a.refine'_2
C : Type u
inst✝¹ : SmallCategory C
inst✝ : HasProducts C
X Y : C
r s : X ⟶ Y
r_ne_s : ¬r = s
z : 2 ≤ #(X ⟶ Y)
md : Type u := (Z : C) × (W : C) × (Z ⟶ W)
α : Cardinal.{u} := #md
yp : C := ∏ fun x => Y
f : X ⟶ yp
⊢ Pi.lift ((fun f k => f ≫ Pi.π (fun x => Y) k) f) = f
[PROOFSTEP]
ext ⟨j⟩
[GOAL]
case refine'_2.a.refine'_2.h.mk
C : Type u
inst✝¹ : SmallCategory C
inst✝ : HasProducts C
X Y : C
r s : X ⟶ Y
r_ne_s : ¬r = s
z : 2 ≤ #(X ⟶ Y)
md : Type u := (Z : C) × (W : C) × (Z ⟶ W)
α : Cardinal.{u} := #md
yp : C := ∏ fun x => Y
f : X ⟶ yp
j : C
snd✝ : (W : C) × (j ⟶ W)
⊢ Pi.lift ((fun f k => f ≫ Pi.π (fun x => Y) k) f) ≫ Pi.π (fun a => Y) { fst := j, snd := snd✝ } =
    f ≫ Pi.π (fun a => Y) { fst := j, snd := snd✝ }
[PROOFSTEP]
simp
[GOAL]
case refine'_3
C : Type u
inst✝¹ : SmallCategory C
inst✝ : HasProducts C
X Y : C
r s : X ⟶ Y
r_ne_s : ¬r = s
z : 2 ≤ #(X ⟶ Y)
md : Type u := (Z : C) × (W : C) × (Z ⟶ W)
α : Cardinal.{u} := #md
yp : C := ∏ fun x => Y
⊢ #(X ⟶ yp) ≤ α
[PROOFSTEP]
apply Cardinal.mk_le_of_injective _
[GOAL]
C : Type u
inst✝¹ : SmallCategory C
inst✝ : HasProducts C
X Y : C
r s : X ⟶ Y
r_ne_s : ¬r = s
z : 2 ≤ #(X ⟶ Y)
md : Type u := (Z : C) × (W : C) × (Z ⟶ W)
α : Cardinal.{u} := #md
yp : C := ∏ fun x => Y
⊢ (X ⟶ yp) → md
[PROOFSTEP]
intro f
[GOAL]
C : Type u
inst✝¹ : SmallCategory C
inst✝ : HasProducts C
X Y : C
r s : X ⟶ Y
r_ne_s : ¬r = s
z : 2 ≤ #(X ⟶ Y)
md : Type u := (Z : C) × (W : C) × (Z ⟶ W)
α : Cardinal.{u} := #md
yp : C := ∏ fun x => Y
f : X ⟶ yp
⊢ md
[PROOFSTEP]
exact ⟨_, _, f⟩
[GOAL]
C : Type u
inst✝¹ : SmallCategory C
inst✝ : HasProducts C
X Y : C
r s : X ⟶ Y
r_ne_s : ¬r = s
z : 2 ≤ #(X ⟶ Y)
md : Type u := (Z : C) × (W : C) × (Z ⟶ W)
α : Cardinal.{u} := #md
yp : C := ∏ fun x => Y
⊢ Function.Injective fun f => { fst := X, snd := { fst := yp, snd := f } }
[PROOFSTEP]
rintro f g k
[GOAL]
C : Type u
inst✝¹ : SmallCategory C
inst✝ : HasProducts C
X Y : C
r s : X ⟶ Y
r_ne_s : ¬r = s
z : 2 ≤ #(X ⟶ Y)
md : Type u := (Z : C) × (W : C) × (Z ⟶ W)
α : Cardinal.{u} := #md
yp : C := ∏ fun x => Y
f g : X ⟶ yp
k :
  (fun f => { fst := X, snd := { fst := yp, snd := f } }) f = (fun f => { fst := X, snd := { fst := yp, snd := f } }) g
⊢ f = g
[PROOFSTEP]
cases k
[GOAL]
case refl
C : Type u
inst✝¹ : SmallCategory C
inst✝ : HasProducts C
X Y : C
r s : X ⟶ Y
r_ne_s : ¬r = s
z : 2 ≤ #(X ⟶ Y)
md : Type u := (Z : C) × (W : C) × (Z ⟶ W)
α : Cardinal.{u} := #md
yp : C := ∏ fun x => Y
f : X ⟶ yp
⊢ f = f
[PROOFSTEP]
rfl