[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
