[GOAL]
C : Type v
inst✝ : SmallCategory C
X : Cᵒᵖ
⊢ (X_1 : C) → (coyoneda.obj X).obj X_1 ⟶ ((Functor.const C).obj PUnit).obj X_1
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type v
inst✝ : SmallCategory C
X : Cᵒᵖ
s : Cocone (coyoneda.obj X)
Y : C
⊢ NatTrans.app (colimitCocone X).ι Y ≫ (fun s x => NatTrans.app s.ι X.unop (𝟙 X.unop)) s = NatTrans.app s.ι Y
[PROOFSTEP]
funext f
[GOAL]
case h
C : Type v
inst✝ : SmallCategory C
X : Cᵒᵖ
s : Cocone (coyoneda.obj X)
Y : C
f : (coyoneda.obj X).obj Y
⊢ (NatTrans.app (colimitCocone X).ι Y ≫ (fun s x => NatTrans.app s.ι X.unop (𝟙 X.unop)) s) f = NatTrans.app s.ι Y f
[PROOFSTEP]
convert congr_fun (s.w f).symm (𝟙 (unop X))
[GOAL]
case h.e'_3.h
C : Type v
inst✝ : SmallCategory C
X : Cᵒᵖ
s : Cocone (coyoneda.obj X)
Y : C
f : (coyoneda.obj X).obj Y
e_1✝ : s.pt = ((Functor.const C).obj s.pt).obj X.unop
⊢ NatTrans.app s.ι Y f = ((coyoneda.obj X).map f ≫ NatTrans.app s.ι Y) (𝟙 X.unop)
[PROOFSTEP]
simp only [coyoneda_obj_obj, Functor.const_obj_obj, types_comp_apply, coyoneda_obj_map, Category.id_comp]
[GOAL]
C : Type v
inst✝ : SmallCategory C
X : Cᵒᵖ
s : Cocone (coyoneda.obj X)
m : (colimitCocone X).pt ⟶ s.pt
w : ∀ (j : C), NatTrans.app (colimitCocone X).ι j ≫ m = NatTrans.app s.ι j
⊢ m = (fun s x => NatTrans.app s.ι X.unop (𝟙 X.unop)) s
[PROOFSTEP]
apply funext
[GOAL]
case h
C : Type v
inst✝ : SmallCategory C
X : Cᵒᵖ
s : Cocone (coyoneda.obj X)
m : (colimitCocone X).pt ⟶ s.pt
w : ∀ (j : C), NatTrans.app (colimitCocone X).ι j ≫ m = NatTrans.app s.ι j
⊢ ∀ (x : (colimitCocone X).pt), m x = (fun s x => NatTrans.app s.ι X.unop (𝟙 X.unop)) s x
[PROOFSTEP]
rintro ⟨⟩
[GOAL]
case h.unit
C : Type v
inst✝ : SmallCategory C
X : Cᵒᵖ
s : Cocone (coyoneda.obj X)
m : (colimitCocone X).pt ⟶ s.pt
w : ∀ (j : C), NatTrans.app (colimitCocone X).ι j ≫ m = NatTrans.app s.ι j
⊢ m PUnit.unit = (fun s x => NatTrans.app s.ι X.unop (𝟙 X.unop)) s PUnit.unit
[PROOFSTEP]
dsimp
[GOAL]
case h.unit
C : Type v
inst✝ : SmallCategory C
X : Cᵒᵖ
s : Cocone (coyoneda.obj X)
m : (colimitCocone X).pt ⟶ s.pt
w : ∀ (j : C), NatTrans.app (colimitCocone X).ι j ≫ m = NatTrans.app s.ι j
⊢ m PUnit.unit = NatTrans.app s.ι X.unop (𝟙 X.unop)
[PROOFSTEP]
rw [← w]
[GOAL]
case h.unit
C : Type v
inst✝ : SmallCategory C
X : Cᵒᵖ
s : Cocone (coyoneda.obj X)
m : (colimitCocone X).pt ⟶ s.pt
w : ∀ (j : C), NatTrans.app (colimitCocone X).ι j ≫ m = NatTrans.app s.ι j
⊢ m PUnit.unit = (NatTrans.app (colimitCocone X).ι X.unop ≫ m) (𝟙 X.unop)
[PROOFSTEP]
simp
[GOAL]
C : Type v
inst✝ : SmallCategory C
X : Cᵒᵖ
⊢ colimit (coyoneda.obj X) ≅ PUnit
[PROOFSTEP]
apply
  colimit.isoColimitCocone
    { cocone := _
      isColimit := colimitCoconeIsColimit X }
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : C
J : Type v
𝒥 : Category.{v, v} J
K : J ⥤ Cᵒᵖ
c : Cone K
t : IsLimit c
s : Cone (K ⋙ yoneda.obj X)
m : s.pt ⟶ ((yoneda.obj X).mapCone c).pt
w : ∀ (j : J), m ≫ NatTrans.app ((yoneda.obj X).mapCone c).π j = NatTrans.app s.π j
x : s.pt
⊢ m x = (fun s x => (IsLimit.lift t { pt := op X, π := NatTrans.mk fun j => (NatTrans.app s.π j x).op }).unop) s x
[PROOFSTEP]
refine' Quiver.Hom.op_inj (t.uniq ⟨op X, _, _⟩ _ fun j => _)
[GOAL]
case refine'_1
C : Type u
inst✝ : Category.{v, u} C
⊢ ∀ (X : C) {J : Type v} (𝒥 : Category.{v, v} J) {K : J ⥤ Cᵒᵖ} {c : Cone K},
    IsLimit c →
      ∀ (s : Cone (K ⋙ yoneda.obj X)) (x : s.pt) (j₁ j₂ : J) (α : j₁ ⟶ j₂),
        ((Functor.const J).obj (op X)).map α ≫ (fun j => (NatTrans.app s.π j x).op) j₂ =
          (fun j => (NatTrans.app s.π j x).op) j₁ ≫ K.map α
[PROOFSTEP]
intro X _ _ _ _ _ s _ _ _ α
[GOAL]
case refine'_1
C : Type u
inst✝ : Category.{v, u} C
X : C
J✝ : Type v
𝒥✝ : Category.{v, v} J✝
K✝ : J✝ ⥤ Cᵒᵖ
c✝ : Cone K✝
t✝ : IsLimit c✝
s : Cone (K✝ ⋙ yoneda.obj X)
x✝ : s.pt
j₁✝ j₂✝ : J✝
α : j₁✝ ⟶ j₂✝
⊢ ((Functor.const J✝).obj (op X)).map α ≫ (fun j => (NatTrans.app s.π j x✝).op) j₂✝ =
    (fun j => (NatTrans.app s.π j x✝).op) j₁✝ ≫ K✝.map α
[PROOFSTEP]
dsimp
[GOAL]
case refine'_1
C : Type u
inst✝ : Category.{v, u} C
X : C
J✝ : Type v
𝒥✝ : Category.{v, v} J✝
K✝ : J✝ ⥤ Cᵒᵖ
c✝ : Cone K✝
t✝ : IsLimit c✝
s : Cone (K✝ ⋙ yoneda.obj X)
x✝ : s.pt
j₁✝ j₂✝ : J✝
α : j₁✝ ⟶ j₂✝
⊢ 𝟙 (op X) ≫ (NatTrans.app s.π j₂✝ x✝).op = (NatTrans.app s.π j₁✝ x✝).op ≫ K✝.map α
[PROOFSTEP]
simp [← s.w α]
  -- See library note [dsimp, simp]
[GOAL]
case refine'_2
C : Type u
inst✝ : Category.{v, u} C
X : C
J : Type v
𝒥 : Category.{v, v} J
K : J ⥤ Cᵒᵖ
c : Cone K
t : IsLimit c
s : Cone (K ⋙ yoneda.obj X)
m : s.pt ⟶ ((yoneda.obj X).mapCone c).pt
w : ∀ (j : J), m ≫ NatTrans.app ((yoneda.obj X).mapCone c).π j = NatTrans.app s.π j
x : s.pt
j : J
⊢ (m x).op ≫ NatTrans.app c.π j = NatTrans.app { pt := op X, π := NatTrans.mk fun j => (NatTrans.app s.π j x).op }.π j
[PROOFSTEP]
exact Quiver.Hom.unop_inj (congrFun (w j) x)
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : Cᵒᵖ
J : Type v
𝒥 : Category.{v, v} J
K : J ⥤ C
c : Cone K
t : IsLimit c
s : Cone (K ⋙ coyoneda.obj X)
x : s.pt
j₁ j₂ : J
α : j₁ ⟶ j₂
⊢ ((Functor.const J).obj X.unop).map α ≫ (fun j => NatTrans.app s.π j x) j₂ =
    (fun j => NatTrans.app s.π j x) j₁ ≫ K.map α
[PROOFSTEP]
dsimp
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : Cᵒᵖ
J : Type v
𝒥 : Category.{v, v} J
K : J ⥤ C
c : Cone K
t : IsLimit c
s : Cone (K ⋙ coyoneda.obj X)
x : s.pt
j₁ j₂ : J
α : j₁ ⟶ j₂
⊢ 𝟙 X.unop ≫ NatTrans.app s.π j₂ x = NatTrans.app s.π j₁ x ≫ K.map α
[PROOFSTEP]
simp [← s.w α]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : Cᵒᵖ
J : Type v
𝒥 : Category.{v, v} J
K : J ⥤ C
c : Cone K
t : IsLimit c
s : Cone (K ⋙ coyoneda.obj X)
m : s.pt ⟶ ((coyoneda.obj X).mapCone c).pt
w : ∀ (j : J), m ≫ NatTrans.app ((coyoneda.obj X).mapCone c).π j = NatTrans.app s.π j
x : s.pt
⊢ m x = (fun s x => IsLimit.lift t { pt := X.unop, π := NatTrans.mk fun j => NatTrans.app s.π j x }) s x
[PROOFSTEP]
refine' t.uniq ⟨unop X, _⟩ _ fun j => _
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : Cᵒᵖ
J : Type v
𝒥 : Category.{v, v} J
K : J ⥤ C
c : Cone K
t : IsLimit c
s : Cone (K ⋙ coyoneda.obj X)
m : s.pt ⟶ ((coyoneda.obj X).mapCone c).pt
w : ∀ (j : J), m ≫ NatTrans.app ((coyoneda.obj X).mapCone c).π j = NatTrans.app s.π j
x : s.pt
j : J
⊢ m x ≫ NatTrans.app c.π j = NatTrans.app { pt := X.unop, π := NatTrans.mk fun j => NatTrans.app s.π j x }.π j
[PROOFSTEP]
exact congrFun (w j) x
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
J : Type w
inst✝ : SmallCategory J
K : J ⥤ Cᵒᵖ
c : Cone K
t : (X : C) → IsLimit ((yoneda.obj X).mapCone c)
s' : (s : Cone K) → Cone (K ⋙ yoneda.obj s.pt.unop) :=
  fun s => { pt := PUnit, π := NatTrans.mk fun j x => (NatTrans.app s.π j).unop }
s : Cone K
m : s.pt ⟶ c.pt
w : ∀ (j : J), m ≫ NatTrans.app c.π j = NatTrans.app s.π j
⊢ m = (fun s => (IsLimit.lift (t s.pt.unop) (s' s) PUnit.unit).op) s
[PROOFSTEP]
apply Quiver.Hom.unop_inj
[GOAL]
case a
C : Type u
inst✝¹ : Category.{v, u} C
J : Type w
inst✝ : SmallCategory J
K : J ⥤ Cᵒᵖ
c : Cone K
t : (X : C) → IsLimit ((yoneda.obj X).mapCone c)
s' : (s : Cone K) → Cone (K ⋙ yoneda.obj s.pt.unop) :=
  fun s => { pt := PUnit, π := NatTrans.mk fun j x => (NatTrans.app s.π j).unop }
s : Cone K
m : s.pt ⟶ c.pt
w : ∀ (j : J), m ≫ NatTrans.app c.π j = NatTrans.app s.π j
⊢ m.unop = ((fun s => (IsLimit.lift (t s.pt.unop) (s' s) PUnit.unit).op) s).unop
[PROOFSTEP]
suffices (fun _ : PUnit => m.unop) = (t s.pt.unop).lift (s' s) by apply congr_fun this PUnit.unit
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
J : Type w
inst✝ : SmallCategory J
K : J ⥤ Cᵒᵖ
c : Cone K
t : (X : C) → IsLimit ((yoneda.obj X).mapCone c)
s' : (s : Cone K) → Cone (K ⋙ yoneda.obj s.pt.unop) :=
  fun s => { pt := PUnit, π := NatTrans.mk fun j x => (NatTrans.app s.π j).unop }
s : Cone K
m : s.pt ⟶ c.pt
w : ∀ (j : J), m ≫ NatTrans.app c.π j = NatTrans.app s.π j
this : (fun x => m.unop) = IsLimit.lift (t s.pt.unop) (s' s)
⊢ m.unop = ((fun s => (IsLimit.lift (t s.pt.unop) (s' s) PUnit.unit).op) s).unop
[PROOFSTEP]
apply congr_fun this PUnit.unit
[GOAL]
case a
C : Type u
inst✝¹ : Category.{v, u} C
J : Type w
inst✝ : SmallCategory J
K : J ⥤ Cᵒᵖ
c : Cone K
t : (X : C) → IsLimit ((yoneda.obj X).mapCone c)
s' : (s : Cone K) → Cone (K ⋙ yoneda.obj s.pt.unop) :=
  fun s => { pt := PUnit, π := NatTrans.mk fun j x => (NatTrans.app s.π j).unop }
s : Cone K
m : s.pt ⟶ c.pt
w : ∀ (j : J), m ≫ NatTrans.app c.π j = NatTrans.app s.π j
⊢ (fun x => m.unop) = IsLimit.lift (t s.pt.unop) (s' s)
[PROOFSTEP]
apply (t _).uniq (s' s) _ fun j => _
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
J : Type w
inst✝ : SmallCategory J
K : J ⥤ Cᵒᵖ
c : Cone K
t : (X : C) → IsLimit ((yoneda.obj X).mapCone c)
s' : (s : Cone K) → Cone (K ⋙ yoneda.obj s.pt.unop) :=
  fun s => { pt := PUnit, π := NatTrans.mk fun j x => (NatTrans.app s.π j).unop }
s : Cone K
m : s.pt ⟶ c.pt
w : ∀ (j : J), m ≫ NatTrans.app c.π j = NatTrans.app s.π j
⊢ ∀ (j : J), (fun x => m.unop) ≫ NatTrans.app ((yoneda.obj s.pt.unop).mapCone c).π j = NatTrans.app (s' s).π j
[PROOFSTEP]
intro j
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
J : Type w
inst✝ : SmallCategory J
K : J ⥤ Cᵒᵖ
c : Cone K
t : (X : C) → IsLimit ((yoneda.obj X).mapCone c)
s' : (s : Cone K) → Cone (K ⋙ yoneda.obj s.pt.unop) :=
  fun s => { pt := PUnit, π := NatTrans.mk fun j x => (NatTrans.app s.π j).unop }
s : Cone K
m : s.pt ⟶ c.pt
w : ∀ (j : J), m ≫ NatTrans.app c.π j = NatTrans.app s.π j
j : J
⊢ (fun x => m.unop) ≫ NatTrans.app ((yoneda.obj s.pt.unop).mapCone c).π j = NatTrans.app (s' s).π j
[PROOFSTEP]
funext
[GOAL]
case h
C : Type u
inst✝¹ : Category.{v, u} C
J : Type w
inst✝ : SmallCategory J
K : J ⥤ Cᵒᵖ
c : Cone K
t : (X : C) → IsLimit ((yoneda.obj X).mapCone c)
s' : (s : Cone K) → Cone (K ⋙ yoneda.obj s.pt.unop) :=
  fun s => { pt := PUnit, π := NatTrans.mk fun j x => (NatTrans.app s.π j).unop }
s : Cone K
m : s.pt ⟶ c.pt
w : ∀ (j : J), m ≫ NatTrans.app c.π j = NatTrans.app s.π j
j : J
x✝ : (s' s).pt
⊢ ((fun x => m.unop) ≫ NatTrans.app ((yoneda.obj s.pt.unop).mapCone c).π j) x✝ = NatTrans.app (s' s).π j x✝
[PROOFSTEP]
exact Quiver.Hom.op_inj (w j)
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
J : Type w
inst✝ : SmallCategory J
K : J ⥤ C
c : Cone K
t : (X : Cᵒᵖ) → IsLimit ((coyoneda.obj X).mapCone c)
s' : (s : Cone K) → Cone (K ⋙ coyoneda.obj (op s.pt)) :=
  fun s => { pt := PUnit, π := NatTrans.mk fun j x => NatTrans.app s.π j }
s : Cone K
m : s.pt ⟶ c.pt
w : ∀ (j : J), m ≫ NatTrans.app c.π j = NatTrans.app s.π j
⊢ m = (fun s => IsLimit.lift (t (op s.pt)) (s' s) PUnit.unit) s
[PROOFSTEP]
suffices (fun _ : PUnit => m) = (t _).lift (s' s) by apply congr_fun this PUnit.unit
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
J : Type w
inst✝ : SmallCategory J
K : J ⥤ C
c : Cone K
t : (X : Cᵒᵖ) → IsLimit ((coyoneda.obj X).mapCone c)
s' : (s : Cone K) → Cone (K ⋙ coyoneda.obj (op s.pt)) :=
  fun s => { pt := PUnit, π := NatTrans.mk fun j x => NatTrans.app s.π j }
s : Cone K
m : s.pt ⟶ c.pt
w : ∀ (j : J), m ≫ NatTrans.app c.π j = NatTrans.app s.π j
this : (fun x => m) = IsLimit.lift (t (op s.pt)) (s' s)
⊢ m = (fun s => IsLimit.lift (t (op s.pt)) (s' s) PUnit.unit) s
[PROOFSTEP]
apply congr_fun this PUnit.unit
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
J : Type w
inst✝ : SmallCategory J
K : J ⥤ C
c : Cone K
t : (X : Cᵒᵖ) → IsLimit ((coyoneda.obj X).mapCone c)
s' : (s : Cone K) → Cone (K ⋙ coyoneda.obj (op s.pt)) :=
  fun s => { pt := PUnit, π := NatTrans.mk fun j x => NatTrans.app s.π j }
s : Cone K
m : s.pt ⟶ c.pt
w : ∀ (j : J), m ≫ NatTrans.app c.π j = NatTrans.app s.π j
⊢ (fun x => m) = IsLimit.lift (t (op s.pt)) (s' s)
[PROOFSTEP]
apply (t _).uniq (s' s) _ fun j => _
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
J : Type w
inst✝ : SmallCategory J
K : J ⥤ C
c : Cone K
t : (X : Cᵒᵖ) → IsLimit ((coyoneda.obj X).mapCone c)
s' : (s : Cone K) → Cone (K ⋙ coyoneda.obj (op s.pt)) :=
  fun s => { pt := PUnit, π := NatTrans.mk fun j x => NatTrans.app s.π j }
s : Cone K
m : s.pt ⟶ c.pt
w : ∀ (j : J), m ≫ NatTrans.app c.π j = NatTrans.app s.π j
⊢ ∀ (j : J), (fun x => m) ≫ NatTrans.app ((coyoneda.obj (op s.pt)).mapCone c).π j = NatTrans.app (s' s).π j
[PROOFSTEP]
intro j
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
J : Type w
inst✝ : SmallCategory J
K : J ⥤ C
c : Cone K
t : (X : Cᵒᵖ) → IsLimit ((coyoneda.obj X).mapCone c)
s' : (s : Cone K) → Cone (K ⋙ coyoneda.obj (op s.pt)) :=
  fun s => { pt := PUnit, π := NatTrans.mk fun j x => NatTrans.app s.π j }
s : Cone K
m : s.pt ⟶ c.pt
w : ∀ (j : J), m ≫ NatTrans.app c.π j = NatTrans.app s.π j
j : J
⊢ (fun x => m) ≫ NatTrans.app ((coyoneda.obj (op s.pt)).mapCone c).π j = NatTrans.app (s' s).π j
[PROOFSTEP]
funext
[GOAL]
case h
C : Type u
inst✝¹ : Category.{v, u} C
J : Type w
inst✝ : SmallCategory J
K : J ⥤ C
c : Cone K
t : (X : Cᵒᵖ) → IsLimit ((coyoneda.obj X).mapCone c)
s' : (s : Cone K) → Cone (K ⋙ coyoneda.obj (op s.pt)) :=
  fun s => { pt := PUnit, π := NatTrans.mk fun j x => NatTrans.app s.π j }
s : Cone K
m : s.pt ⟶ c.pt
w : ∀ (j : J), m ≫ NatTrans.app c.π j = NatTrans.app s.π j
j : J
x✝ : (s' s).pt
⊢ ((fun x => m) ≫ NatTrans.app ((coyoneda.obj (op s.pt)).mapCone c).π j) x✝ = NatTrans.app (s' s).π j x✝
[PROOFSTEP]
exact w j
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u
inst✝ : SmallCategory D
⊢ PreservesLimits yoneda
[PROOFSTEP]
apply preservesLimitsOfEvaluation
[GOAL]
case x
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u
inst✝ : SmallCategory D
⊢ (k : Dᵒᵖ) → PreservesLimitsOfSize.{u, u, u, u, u, u + 1} (yoneda ⋙ (evaluation Dᵒᵖ (Type u)).obj k)
[PROOFSTEP]
intro K
[GOAL]
case x
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u
inst✝ : SmallCategory D
K : Dᵒᵖ
⊢ PreservesLimitsOfSize.{u, u, u, u, u, u + 1} (yoneda ⋙ (evaluation Dᵒᵖ (Type u)).obj K)
[PROOFSTEP]
change PreservesLimits (coyoneda.obj K)
[GOAL]
case x
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u
inst✝ : SmallCategory D
K : Dᵒᵖ
⊢ PreservesLimits (coyoneda.obj K)
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u
inst✝ : SmallCategory D
⊢ PreservesLimits coyoneda
[PROOFSTEP]
apply preservesLimitsOfEvaluation
[GOAL]
case x
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u
inst✝ : SmallCategory D
⊢ (k : D) → PreservesLimitsOfSize.{u, u, u, u, u, u + 1} (coyoneda ⋙ (evaluation D (Type u)).obj k)
[PROOFSTEP]
intro K
[GOAL]
case x
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u
inst✝ : SmallCategory D
K : D
⊢ PreservesLimitsOfSize.{u, u, u, u, u, u + 1} (coyoneda ⋙ (evaluation D (Type u)).obj K)
[PROOFSTEP]
change PreservesLimits (yoneda.obj K)
[GOAL]
case x
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u
inst✝ : SmallCategory D
K : D
⊢ PreservesLimits (yoneda.obj K)
[PROOFSTEP]
infer_instance
