[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : op X ⟶ op Y
⊢ (yoneda.obj X).map f (𝟙 X) = NatTrans.app (yoneda.map f.unop) (op Y) (𝟙 Y)
[PROOFSTEP]
dsimp
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : op X ⟶ op Y
⊢ f.unop ≫ 𝟙 X = 𝟙 Y ≫ f.unop
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f g : X ⟶ Y
p : yoneda.map f = yoneda.map g
⊢ f = g
[PROOFSTEP]
convert congr_fun (congr_app p (op X)) (𝟙 X) using 1
[GOAL]
case h.e'_2.h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f g : X ⟶ Y
p : yoneda.map f = yoneda.map g
e_1✝ : (X ⟶ Y) = (yoneda.obj Y).obj (op X)
⊢ f = NatTrans.app (yoneda.map f) (op X) (𝟙 X)
[PROOFSTEP]
dsimp
[GOAL]
case h.e'_3.h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f g : X ⟶ Y
p : yoneda.map f = yoneda.map g
e_1✝ : (X ⟶ Y) = (yoneda.obj Y).obj (op X)
⊢ g = NatTrans.app (yoneda.map g) (op X) (𝟙 X)
[PROOFSTEP]
dsimp
[GOAL]
case h.e'_2.h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f g : X ⟶ Y
p : yoneda.map f = yoneda.map g
e_1✝ : (X ⟶ Y) = (yoneda.obj Y).obj (op X)
⊢ f = 𝟙 X ≫ f
[PROOFSTEP]
simp
[GOAL]
case h.e'_3.h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f g : X ⟶ Y
p : yoneda.map f = yoneda.map g
e_1✝ : (X ⟶ Y) = (yoneda.obj Y).obj (op X)
⊢ g = 𝟙 X ≫ g
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : Cᵒᵖ
f : coyoneda.obj X ⟶ coyoneda.obj Y
⊢ coyoneda.map ((fun {X} x f => (NatTrans.app f X.unop (𝟙 X.unop)).op) Y f) = f
[PROOFSTEP]
simp only [coyoneda]
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : Cᵒᵖ
f : coyoneda.obj X ⟶ coyoneda.obj Y
⊢ (NatTrans.mk fun Y_1 g => (NatTrans.app f X.unop (𝟙 X.unop)).op.unop ≫ g) = f
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X x✝² : Cᵒᵖ
x✝¹ x✝ : X ⟶ x✝²
p : coyoneda.map x✝¹ = coyoneda.map x✝
⊢ x✝¹ = x✝
[PROOFSTEP]
have t := congr_fun (congr_app p X.unop) (𝟙 _)
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X x✝² : Cᵒᵖ
x✝¹ x✝ : X ⟶ x✝²
p : coyoneda.map x✝¹ = coyoneda.map x✝
t : NatTrans.app (coyoneda.map x✝¹) X.unop (𝟙 X.unop) = NatTrans.app (coyoneda.map x✝) X.unop (𝟙 X.unop)
⊢ x✝¹ = x✝
[PROOFSTEP]
simpa using congr_arg Quiver.Hom.op t
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
F : Cᵒᵖ ⥤ Type v₁
inst✝ : Representable F
X : Cᵒᵖ
f : X.unop ⟶ reprX F
⊢ ((reprW F).app X).hom f = F.map f.op (reprx F)
[PROOFSTEP]
change F.reprF.app X f = (F.reprF.app (op F.reprX) ≫ F.map f.op) (𝟙 F.reprX)
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
F : Cᵒᵖ ⥤ Type v₁
inst✝ : Representable F
X : Cᵒᵖ
f : X.unop ⟶ reprX F
⊢ NatTrans.app (reprF F) X f = (NatTrans.app (reprF F) (op (reprX F)) ≫ F.map f.op) (𝟙 (reprX F))
[PROOFSTEP]
rw [← F.reprF.naturality]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
F : Cᵒᵖ ⥤ Type v₁
inst✝ : Representable F
X : Cᵒᵖ
f : X.unop ⟶ reprX F
⊢ NatTrans.app (reprF F) X f = ((yoneda.obj (reprX F)).map f.op ≫ NatTrans.app (reprF F) (op X.unop)) (𝟙 (reprX F))
[PROOFSTEP]
dsimp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
F : Cᵒᵖ ⥤ Type v₁
inst✝ : Representable F
X : Cᵒᵖ
f : X.unop ⟶ reprX F
⊢ NatTrans.app (reprF F) X f = NatTrans.app (reprF F) X (f ≫ 𝟙 (reprX F))
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
F : C ⥤ Type v₁
inst✝ : Corepresentable F
X : C
f : coreprX F ⟶ X
⊢ ((coreprW F).app X).hom f = F.map f (coreprx F)
[PROOFSTEP]
change F.coreprF.app X f = (F.coreprF.app F.coreprX ≫ F.map f) (𝟙 F.coreprX)
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
F : C ⥤ Type v₁
inst✝ : Corepresentable F
X : C
f : coreprX F ⟶ X
⊢ NatTrans.app (coreprF F) X f = (NatTrans.app (coreprF F) (coreprX F) ≫ F.map f) (𝟙 (coreprX F))
[PROOFSTEP]
rw [← F.coreprF.naturality]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
F : C ⥤ Type v₁
inst✝ : Corepresentable F
X : C
f : coreprX F ⟶ X
⊢ NatTrans.app (coreprF F) X f = ((coyoneda.obj (op (coreprX F))).map f ≫ NatTrans.app (coreprF F) X) (𝟙 (coreprX F))
[PROOFSTEP]
dsimp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
F : C ⥤ Type v₁
inst✝ : Corepresentable F
X : C
f : coreprX F ⟶ X
⊢ NatTrans.app (coreprF F) X f = NatTrans.app (coreprF F) X (𝟙 (coreprX F) ≫ f)
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
⊢ ∀ ⦃X Y : Cᵒᵖ × (Cᵒᵖ ⥤ Type v₁)⦄ (f : X ⟶ Y),
    (yonedaPairing C).map f ≫ (fun F x => { down := NatTrans.app x F.fst (𝟙 F.fst.unop) }) Y =
      (fun F x => { down := NatTrans.app x F.fst (𝟙 F.fst.unop) }) X ≫ (yonedaEvaluation C).map f
[PROOFSTEP]
intro X Y f
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : Cᵒᵖ × (Cᵒᵖ ⥤ Type v₁)
f : X ⟶ Y
⊢ (yonedaPairing C).map f ≫ (fun F x => { down := NatTrans.app x F.fst (𝟙 F.fst.unop) }) Y =
    (fun F x => { down := NatTrans.app x F.fst (𝟙 F.fst.unop) }) X ≫ (yonedaEvaluation C).map f
[PROOFSTEP]
simp only [yonedaEvaluation]
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : Cᵒᵖ × (Cᵒᵖ ⥤ Type v₁)
f : X ⟶ Y
⊢ ((yonedaPairing C).map f ≫ fun x => { down := NatTrans.app x Y.fst (𝟙 Y.fst.unop) }) =
    (fun x => { down := NatTrans.app x X.fst (𝟙 X.fst.unop) }) ≫
      (evaluationUncurried Cᵒᵖ (Type v₁) ⋙ uliftFunctor.{u₁, v₁}).map f
[PROOFSTEP]
ext
[GOAL]
case h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : Cᵒᵖ × (Cᵒᵖ ⥤ Type v₁)
f : X ⟶ Y
a✝ : (yonedaPairing C).obj X
⊢ ((yonedaPairing C).map f ≫ fun x => { down := NatTrans.app x Y.fst (𝟙 Y.fst.unop) }) a✝ =
    ((fun x => { down := NatTrans.app x X.fst (𝟙 X.fst.unop) }) ≫
        (evaluationUncurried Cᵒᵖ (Type v₁) ⋙ uliftFunctor.{u₁, v₁}).map f)
      a✝
[PROOFSTEP]
dsimp
[GOAL]
case h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : Cᵒᵖ × (Cᵒᵖ ⥤ Type v₁)
f : X ⟶ Y
a✝ : (yonedaPairing C).obj X
⊢ { down := NatTrans.app f.snd Y.fst (NatTrans.app a✝ Y.fst (𝟙 Y.fst.unop ≫ f.fst.unop)) } =
    { down := NatTrans.app f.snd Y.fst (X.snd.map f.fst (NatTrans.app a✝ X.fst (𝟙 X.fst.unop))) }
[PROOFSTEP]
erw [Category.id_comp, ← FunctorToTypes.naturality]
[GOAL]
case h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : Cᵒᵖ × (Cᵒᵖ ⥤ Type v₁)
f : X ⟶ Y
a✝ : (yonedaPairing C).obj X
⊢ { down := NatTrans.app f.snd Y.fst (NatTrans.app a✝ Y.fst f.fst.unop) } =
    { down := NatTrans.app f.snd Y.fst (NatTrans.app a✝ Y.fst ((yoneda.obj X.fst.unop).map f.fst (𝟙 X.fst.unop))) }
[PROOFSTEP]
simp only [Category.comp_id, yoneda_obj_map]
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : Cᵒᵖ × (Cᵒᵖ ⥤ Type v₁)
x : (yonedaEvaluation C).obj F
⊢ ∀ ⦃X Y : Cᵒᵖ⦄ (f : X ⟶ Y),
    ((Functor.prod yoneda.op (𝟭 (Cᵒᵖ ⥤ Type v₁))).obj F).fst.unop.map f ≫ (fun X a => F.snd.map a.op x.down) Y =
      (fun X a => F.snd.map a.op x.down) X ≫ ((Functor.prod yoneda.op (𝟭 (Cᵒᵖ ⥤ Type v₁))).obj F).snd.map f
[PROOFSTEP]
intro X Y f
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : Cᵒᵖ × (Cᵒᵖ ⥤ Type v₁)
x : (yonedaEvaluation C).obj F
X Y : Cᵒᵖ
f : X ⟶ Y
⊢ ((Functor.prod yoneda.op (𝟭 (Cᵒᵖ ⥤ Type v₁))).obj F).fst.unop.map f ≫ (fun X a => F.snd.map a.op x.down) Y =
    (fun X a => F.snd.map a.op x.down) X ≫ ((Functor.prod yoneda.op (𝟭 (Cᵒᵖ ⥤ Type v₁))).obj F).snd.map f
[PROOFSTEP]
ext
[GOAL]
case h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : Cᵒᵖ × (Cᵒᵖ ⥤ Type v₁)
x : (yonedaEvaluation C).obj F
X Y : Cᵒᵖ
f : X ⟶ Y
a✝ : ((Functor.prod yoneda.op (𝟭 (Cᵒᵖ ⥤ Type v₁))).obj F).fst.unop.obj X
⊢ (((Functor.prod yoneda.op (𝟭 (Cᵒᵖ ⥤ Type v₁))).obj F).fst.unop.map f ≫ (fun X a => F.snd.map a.op x.down) Y) a✝ =
    ((fun X a => F.snd.map a.op x.down) X ≫ ((Functor.prod yoneda.op (𝟭 (Cᵒᵖ ⥤ Type v₁))).obj F).snd.map f) a✝
[PROOFSTEP]
dsimp
[GOAL]
case h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : Cᵒᵖ × (Cᵒᵖ ⥤ Type v₁)
x : (yonedaEvaluation C).obj F
X Y : Cᵒᵖ
f : X ⟶ Y
a✝ : ((Functor.prod yoneda.op (𝟭 (Cᵒᵖ ⥤ Type v₁))).obj F).fst.unop.obj X
⊢ F.snd.map (a✝.op ≫ f) x.down = F.snd.map f (F.snd.map a✝.op x.down)
[PROOFSTEP]
rw [FunctorToTypes.map_comp_apply]
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
⊢ ∀ ⦃X Y : Cᵒᵖ × (Cᵒᵖ ⥤ Type v₁)⦄ (f : X ⟶ Y),
    (yonedaEvaluation C).map f ≫ (fun F x => NatTrans.mk fun X a => F.snd.map a.op x.down) Y =
      (fun F x => NatTrans.mk fun X a => F.snd.map a.op x.down) X ≫ (yonedaPairing C).map f
[PROOFSTEP]
intro X Y f
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : Cᵒᵖ × (Cᵒᵖ ⥤ Type v₁)
f : X ⟶ Y
⊢ (yonedaEvaluation C).map f ≫ (fun F x => NatTrans.mk fun X a => F.snd.map a.op x.down) Y =
    (fun F x => NatTrans.mk fun X a => F.snd.map a.op x.down) X ≫ (yonedaPairing C).map f
[PROOFSTEP]
simp only [yoneda]
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : Cᵒᵖ × (Cᵒᵖ ⥤ Type v₁)
f : X ⟶ Y
⊢ ((yonedaEvaluation C).map f ≫ fun x => NatTrans.mk fun X a => Y.snd.map a.op x.down) =
    (fun x => NatTrans.mk fun X_1 a => X.snd.map a.op x.down) ≫ (yonedaPairing C).map f
[PROOFSTEP]
ext
[GOAL]
case h.w.h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : Cᵒᵖ × (Cᵒᵖ ⥤ Type v₁)
f : X ⟶ Y
a✝¹ : (yonedaEvaluation C).obj X
Y✝ : Cᵒᵖ
a✝ : ((Functor.prod yoneda.op (𝟭 (Cᵒᵖ ⥤ Type v₁))).obj Y).fst.unop.obj Y✝
⊢ NatTrans.app (((yonedaEvaluation C).map f ≫ fun x => NatTrans.mk fun X a => Y.snd.map a.op x.down) a✝¹) Y✝ a✝ =
    NatTrans.app (((fun x => NatTrans.mk fun X_1 a => X.snd.map a.op x.down) ≫ (yonedaPairing C).map f) a✝¹) Y✝ a✝
[PROOFSTEP]
dsimp
[GOAL]
case h.w.h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : Cᵒᵖ × (Cᵒᵖ ⥤ Type v₁)
f : X ⟶ Y
a✝¹ : (yonedaEvaluation C).obj X
Y✝ : Cᵒᵖ
a✝ : ((Functor.prod yoneda.op (𝟭 (Cᵒᵖ ⥤ Type v₁))).obj Y).fst.unop.obj Y✝
⊢ Y.snd.map a✝.op (NatTrans.app f.snd Y.fst (X.snd.map f.fst a✝¹.down)) =
    NatTrans.app f.snd Y✝ (X.snd.map (f.fst ≫ a✝.op) a✝¹.down)
[PROOFSTEP]
rw [← FunctorToTypes.naturality X.snd Y.snd f.snd, FunctorToTypes.map_comp_apply]
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
⊢ ((NatTrans.mk fun F x => { down := NatTrans.app x F.fst (𝟙 F.fst.unop) }) ≫
      NatTrans.mk fun F x => NatTrans.mk fun X a => F.snd.map a.op x.down) =
    𝟙 (yonedaPairing C)
[PROOFSTEP]
ext
[GOAL]
case w.h.h.w.h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
x✝ : Cᵒᵖ × (Cᵒᵖ ⥤ Type v₁)
a✝¹ : (yonedaPairing C).obj x✝
Y✝ : Cᵒᵖ
a✝ : ((Functor.prod yoneda.op (𝟭 (Cᵒᵖ ⥤ Type v₁))).obj x✝).fst.unop.obj Y✝
⊢ NatTrans.app
      (NatTrans.app
        ((NatTrans.mk fun F x => { down := NatTrans.app x F.fst (𝟙 F.fst.unop) }) ≫
          NatTrans.mk fun F x => NatTrans.mk fun X a => F.snd.map a.op x.down)
        x✝ a✝¹)
      Y✝ a✝ =
    NatTrans.app (NatTrans.app (𝟙 (yonedaPairing C)) x✝ a✝¹) Y✝ a✝
[PROOFSTEP]
dsimp
[GOAL]
case w.h.h.w.h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
x✝ : Cᵒᵖ × (Cᵒᵖ ⥤ Type v₁)
a✝¹ : (yonedaPairing C).obj x✝
Y✝ : Cᵒᵖ
a✝ : ((Functor.prod yoneda.op (𝟭 (Cᵒᵖ ⥤ Type v₁))).obj x✝).fst.unop.obj Y✝
⊢ x✝.snd.map a✝.op (NatTrans.app a✝¹ x✝.fst (𝟙 x✝.fst.unop)) = NatTrans.app a✝¹ Y✝ a✝
[PROOFSTEP]
erw [← FunctorToTypes.naturality, obj_map_id]
[GOAL]
case w.h.h.w.h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
x✝ : Cᵒᵖ × (Cᵒᵖ ⥤ Type v₁)
a✝¹ : (yonedaPairing C).obj x✝
Y✝ : Cᵒᵖ
a✝ : ((Functor.prod yoneda.op (𝟭 (Cᵒᵖ ⥤ Type v₁))).obj x✝).fst.unop.obj Y✝
⊢ NatTrans.app a✝¹ Y✝ (NatTrans.app (yoneda.map a✝.op.unop) (op Y✝.unop) (𝟙 Y✝.unop)) = NatTrans.app a✝¹ Y✝ a✝
[PROOFSTEP]
simp only [yoneda_map_app, Quiver.Hom.unop_op]
[GOAL]
case w.h.h.w.h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
x✝ : Cᵒᵖ × (Cᵒᵖ ⥤ Type v₁)
a✝¹ : (yonedaPairing C).obj x✝
Y✝ : Cᵒᵖ
a✝ : ((Functor.prod yoneda.op (𝟭 (Cᵒᵖ ⥤ Type v₁))).obj x✝).fst.unop.obj Y✝
⊢ NatTrans.app a✝¹ Y✝ (𝟙 Y✝.unop ≫ a✝) = NatTrans.app a✝¹ Y✝ a✝
[PROOFSTEP]
erw [Category.id_comp]
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
⊢ ((NatTrans.mk fun F x => NatTrans.mk fun X a => F.snd.map a.op x.down) ≫
      NatTrans.mk fun F x => { down := NatTrans.app x F.fst (𝟙 F.fst.unop) }) =
    𝟙 (yonedaEvaluation C)
[PROOFSTEP]
ext
[GOAL]
case w.h.h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
x✝ : Cᵒᵖ × (Cᵒᵖ ⥤ Type v₁)
a✝ : (yonedaEvaluation C).obj x✝
⊢ NatTrans.app
      ((NatTrans.mk fun F x => NatTrans.mk fun X a => F.snd.map a.op x.down) ≫
        NatTrans.mk fun F x => { down := NatTrans.app x F.fst (𝟙 F.fst.unop) })
      x✝ a✝ =
    NatTrans.app (𝟙 (yonedaEvaluation C)) x✝ a✝
[PROOFSTEP]
dsimp
[GOAL]
case w.h.h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
x✝ : Cᵒᵖ × (Cᵒᵖ ⥤ Type v₁)
a✝ : (yonedaEvaluation C).obj x✝
⊢ { down := x✝.snd.map (𝟙 x✝.fst) a✝.down } = a✝
[PROOFSTEP]
rw [FunctorToTypes.map_id_apply, ULift.up_down]
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
F : Cᵒᵖ ⥤ Type v₁
f : yoneda.obj X ⟶ F
g : Y ⟶ X
⊢ F.map g.op (↑yonedaEquiv f) = ↑yonedaEquiv (yoneda.map g ≫ f)
[PROOFSTEP]
change (f.app (op X) ≫ F.map g.op) (𝟙 X) = f.app (op Y) (𝟙 Y ≫ g)
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
F : Cᵒᵖ ⥤ Type v₁
f : yoneda.obj X ⟶ F
g : Y ⟶ X
⊢ (NatTrans.app f (op X) ≫ F.map g.op) (𝟙 X) = NatTrans.app f (op Y) (𝟙 Y ≫ g)
[PROOFSTEP]
rw [← f.naturality]
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
F : Cᵒᵖ ⥤ Type v₁
f : yoneda.obj X ⟶ F
g : Y ⟶ X
⊢ ((yoneda.obj X).map g.op ≫ NatTrans.app f (op Y)) (𝟙 X) = NatTrans.app f (op Y) (𝟙 Y ≫ g)
[PROOFSTEP]
dsimp
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
F : Cᵒᵖ ⥤ Type v₁
f : yoneda.obj X ⟶ F
g : Y ⟶ X
⊢ NatTrans.app f (op Y) (g ≫ 𝟙 X) = NatTrans.app f (op Y) (𝟙 Y ≫ g)
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
⊢ ↑yonedaEquiv (yoneda.map f) = f
[PROOFSTEP]
rw [yonedaEquiv_apply]
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
⊢ NatTrans.app (yoneda.map f) (op X) (𝟙 X) = f
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : Cᵒᵖ
f : X ⟶ Y
F : Cᵒᵖ ⥤ Type v₁
t : F.obj X
⊢ ↑yonedaEquiv.symm (F.map f t) = yoneda.map f.unop ≫ ↑yonedaEquiv.symm t
[PROOFSTEP]
obtain ⟨u, rfl⟩ := yonedaEquiv.surjective t
[GOAL]
case intro
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : Cᵒᵖ
f : X ⟶ Y
F : Cᵒᵖ ⥤ Type v₁
u : yoneda.obj X.unop ⟶ F
⊢ ↑yonedaEquiv.symm (F.map f (↑yonedaEquiv u)) = yoneda.map f.unop ≫ ↑yonedaEquiv.symm (↑yonedaEquiv u)
[PROOFSTEP]
rw [yonedaEquiv_naturality', Equiv.symm_apply_apply, Equiv.symm_apply_apply]
[GOAL]
C✝ : Type u₁
inst✝¹ : Category.{v₁, u₁} C✝
C : Type u₁
inst✝ : SmallCategory C
⊢ yoneda.op ⋙ coyoneda ≅ evaluation Cᵒᵖ (Type u₁)
[PROOFSTEP]
refine
  eqToIso ?_ ≪≫
    curry.mapIso (yonedaLemma C ≪≫ isoWhiskerLeft (evaluationUncurried Cᵒᵖ (Type u₁)) uliftFunctorTrivial) ≪≫ eqToIso ?_
[GOAL]
case refine_1
C✝ : Type u₁
inst✝¹ : Category.{v₁, u₁} C✝
C : Type u₁
inst✝ : SmallCategory C
⊢ yoneda.op ⋙ coyoneda = curry.obj (yonedaPairing C)
[PROOFSTEP]
apply Functor.ext
[GOAL]
case refine_1.h_map
C✝ : Type u₁
inst✝¹ : Category.{v₁, u₁} C✝
C : Type u₁
inst✝ : SmallCategory C
⊢ autoParam
    (∀ (X Y : Cᵒᵖ) (f : X ⟶ Y),
      (yoneda.op ⋙ coyoneda).map f =
        eqToHom (_ : ?F.obj X = ?G.obj X) ≫
          (curry.obj (yonedaPairing C)).map f ≫
            eqToHom (_ : (curry.obj (yonedaPairing C)).obj Y = (yoneda.op ⋙ coyoneda).obj Y))
    _auto✝
[PROOFSTEP]
intro X Y f
[GOAL]
case refine_1.h_map
C✝ : Type u₁
inst✝¹ : Category.{v₁, u₁} C✝
C : Type u₁
inst✝ : SmallCategory C
X Y : Cᵒᵖ
f : X ⟶ Y
⊢ (yoneda.op ⋙ coyoneda).map f =
    eqToHom (_ : ?F.obj X = ?G.obj X) ≫
      (curry.obj (yonedaPairing C)).map f ≫
        eqToHom (_ : (curry.obj (yonedaPairing C)).obj Y = (yoneda.op ⋙ coyoneda).obj Y)
[PROOFSTEP]
ext
[GOAL]
case refine_1.h_map.w.h.h
C✝ : Type u₁
inst✝¹ : Category.{v₁, u₁} C✝
C : Type u₁
inst✝ : SmallCategory C
X Y : Cᵒᵖ
f : X ⟶ Y
x✝ : Cᵒᵖ ⥤ Type u₁
a✝ : ((yoneda.op ⋙ coyoneda).obj X).obj x✝
⊢ NatTrans.app ((yoneda.op ⋙ coyoneda).map f) x✝ a✝ =
    NatTrans.app
      (eqToHom (_ : ?F.obj X = ?G.obj X) ≫
        (curry.obj (yonedaPairing C)).map f ≫
          eqToHom (_ : (curry.obj (yonedaPairing C)).obj Y = (yoneda.op ⋙ coyoneda).obj Y))
      x✝ a✝
[PROOFSTEP]
simp
[GOAL]
case refine_1.h_obj
C✝ : Type u₁
inst✝¹ : Category.{v₁, u₁} C✝
C : Type u₁
inst✝ : SmallCategory C
⊢ ∀ (X : Cᵒᵖ), (yoneda.op ⋙ coyoneda).obj X = (curry.obj (yonedaPairing C)).obj X
[PROOFSTEP]
aesop_cat
[GOAL]
case refine_2
C✝ : Type u₁
inst✝¹ : Category.{v₁, u₁} C✝
C : Type u₁
inst✝ : SmallCategory C
⊢ curry.obj (evaluationUncurried Cᵒᵖ (Type u₁) ⋙ 𝟭 (Type u₁)) = evaluation Cᵒᵖ (Type u₁)
[PROOFSTEP]
apply Functor.ext
[GOAL]
case refine_2.h_map
C✝ : Type u₁
inst✝¹ : Category.{v₁, u₁} C✝
C : Type u₁
inst✝ : SmallCategory C
⊢ autoParam
    (∀ (X Y : Cᵒᵖ) (f : X ⟶ Y),
      (curry.obj (evaluationUncurried Cᵒᵖ (Type u₁) ⋙ 𝟭 (Type u₁))).map f =
        eqToHom (_ : ?F.obj X = ?G.obj X) ≫
          (evaluation Cᵒᵖ (Type u₁)).map f ≫
            eqToHom
              (_ :
                (evaluation Cᵒᵖ (Type u₁)).obj Y = (curry.obj (evaluationUncurried Cᵒᵖ (Type u₁) ⋙ 𝟭 (Type u₁))).obj Y))
    _auto✝
[PROOFSTEP]
intro X Y f
[GOAL]
case refine_2.h_map
C✝ : Type u₁
inst✝¹ : Category.{v₁, u₁} C✝
C : Type u₁
inst✝ : SmallCategory C
X Y : Cᵒᵖ
f : X ⟶ Y
⊢ (curry.obj (evaluationUncurried Cᵒᵖ (Type u₁) ⋙ 𝟭 (Type u₁))).map f =
    eqToHom (_ : ?F.obj X = ?G.obj X) ≫
      (evaluation Cᵒᵖ (Type u₁)).map f ≫
        eqToHom
          (_ : (evaluation Cᵒᵖ (Type u₁)).obj Y = (curry.obj (evaluationUncurried Cᵒᵖ (Type u₁) ⋙ 𝟭 (Type u₁))).obj Y)
[PROOFSTEP]
ext
[GOAL]
case refine_2.h_map.w.h.h
C✝ : Type u₁
inst✝¹ : Category.{v₁, u₁} C✝
C : Type u₁
inst✝ : SmallCategory C
X Y : Cᵒᵖ
f : X ⟶ Y
x✝ : Cᵒᵖ ⥤ Type u₁
a✝ : ((curry.obj (evaluationUncurried Cᵒᵖ (Type u₁) ⋙ 𝟭 (Type u₁))).obj X).obj x✝
⊢ NatTrans.app ((curry.obj (evaluationUncurried Cᵒᵖ (Type u₁) ⋙ 𝟭 (Type u₁))).map f) x✝ a✝ =
    NatTrans.app
      (eqToHom (_ : ?F.obj X = ?G.obj X) ≫
        (evaluation Cᵒᵖ (Type u₁)).map f ≫
          eqToHom
            (_ :
              (evaluation Cᵒᵖ (Type u₁)).obj Y = (curry.obj (evaluationUncurried Cᵒᵖ (Type u₁) ⋙ 𝟭 (Type u₁))).obj Y))
      x✝ a✝
[PROOFSTEP]
simp
[GOAL]
case refine_2.h_obj
C✝ : Type u₁
inst✝¹ : Category.{v₁, u₁} C✝
C : Type u₁
inst✝ : SmallCategory C
⊢ ∀ (X : Cᵒᵖ), (curry.obj (evaluationUncurried Cᵒᵖ (Type u₁) ⋙ 𝟭 (Type u₁))).obj X = (evaluation Cᵒᵖ (Type u₁)).obj X
[PROOFSTEP]
intro X
[GOAL]
case refine_2.h_obj
C✝ : Type u₁
inst✝¹ : Category.{v₁, u₁} C✝
C : Type u₁
inst✝ : SmallCategory C
X : Cᵒᵖ
⊢ (curry.obj (evaluationUncurried Cᵒᵖ (Type u₁) ⋙ 𝟭 (Type u₁))).obj X = (evaluation Cᵒᵖ (Type u₁)).obj X
[PROOFSTEP]
simp only [curry, yoneda, coyoneda, curryObj, yonedaPairing]
[GOAL]
case refine_2.h_obj
C✝ : Type u₁
inst✝¹ : Category.{v₁, u₁} C✝
C : Type u₁
inst✝ : SmallCategory C
X : Cᵒᵖ
⊢ Functor.mk
      { obj := fun Y => (evaluationUncurried Cᵒᵖ (Type u₁) ⋙ 𝟭 (Type u₁)).obj (X, Y),
        map := fun {X_1 Y} g => (evaluationUncurried Cᵒᵖ (Type u₁) ⋙ 𝟭 (Type u₁)).map (𝟙 X, g) } =
    (evaluation Cᵒᵖ (Type u₁)).obj X
[PROOFSTEP]
aesop_cat
[GOAL]
C✝ : Type u₁
inst✝¹ : Category.{v₁, u₁} C✝
C : Type u₁
inst✝ : SmallCategory C
⊢ yoneda ⋙ (whiskeringLeft Cᵒᵖ (Cᵒᵖ ⥤ Type u₁)ᵒᵖ (Type u₁)).obj yoneda.op ≅ 𝟭 (Cᵒᵖ ⥤ Type u₁)
[PROOFSTEP]
refine
  eqToIso ?_ ≪≫
    curry.mapIso
        (isoWhiskerLeft (Prod.swap _ _)
          (yonedaLemma C ≪≫ isoWhiskerLeft (evaluationUncurried Cᵒᵖ (Type u₁)) uliftFunctorTrivial : _)) ≪≫
      eqToIso ?_
[GOAL]
case refine_1
C✝ : Type u₁
inst✝¹ : Category.{v₁, u₁} C✝
C : Type u₁
inst✝ : SmallCategory C
⊢ yoneda ⋙ (whiskeringLeft Cᵒᵖ (Cᵒᵖ ⥤ Type u₁)ᵒᵖ (Type u₁)).obj yoneda.op =
    curry.obj (Prod.swap (Cᵒᵖ ⥤ Type u₁) Cᵒᵖ ⋙ yonedaPairing C)
[PROOFSTEP]
apply Functor.ext
[GOAL]
case refine_1.h_map
C✝ : Type u₁
inst✝¹ : Category.{v₁, u₁} C✝
C : Type u₁
inst✝ : SmallCategory C
⊢ autoParam
    (∀ (X Y : Cᵒᵖ ⥤ Type u₁) (f : X ⟶ Y),
      (yoneda ⋙ (whiskeringLeft Cᵒᵖ (Cᵒᵖ ⥤ Type u₁)ᵒᵖ (Type u₁)).obj yoneda.op).map f =
        eqToHom (_ : ?F.obj X = ?G.obj X) ≫
          (curry.obj (Prod.swap (Cᵒᵖ ⥤ Type u₁) Cᵒᵖ ⋙ yonedaPairing C)).map f ≫
            eqToHom
              (_ :
                (curry.obj (Prod.swap (Cᵒᵖ ⥤ Type u₁) Cᵒᵖ ⋙ yonedaPairing C)).obj Y =
                  (yoneda ⋙ (whiskeringLeft Cᵒᵖ (Cᵒᵖ ⥤ Type u₁)ᵒᵖ (Type u₁)).obj yoneda.op).obj Y))
    _auto✝
[PROOFSTEP]
intro X Y f
[GOAL]
case refine_1.h_map
C✝ : Type u₁
inst✝¹ : Category.{v₁, u₁} C✝
C : Type u₁
inst✝ : SmallCategory C
X Y : Cᵒᵖ ⥤ Type u₁
f : X ⟶ Y
⊢ (yoneda ⋙ (whiskeringLeft Cᵒᵖ (Cᵒᵖ ⥤ Type u₁)ᵒᵖ (Type u₁)).obj yoneda.op).map f =
    eqToHom (_ : ?F.obj X = ?G.obj X) ≫
      (curry.obj (Prod.swap (Cᵒᵖ ⥤ Type u₁) Cᵒᵖ ⋙ yonedaPairing C)).map f ≫
        eqToHom
          (_ :
            (curry.obj (Prod.swap (Cᵒᵖ ⥤ Type u₁) Cᵒᵖ ⋙ yonedaPairing C)).obj Y =
              (yoneda ⋙ (whiskeringLeft Cᵒᵖ (Cᵒᵖ ⥤ Type u₁)ᵒᵖ (Type u₁)).obj yoneda.op).obj Y)
[PROOFSTEP]
aesop_cat
[GOAL]
case refine_2
C✝ : Type u₁
inst✝¹ : Category.{v₁, u₁} C✝
C : Type u₁
inst✝ : SmallCategory C
⊢ curry.obj (Prod.swap (Cᵒᵖ ⥤ Type u₁) Cᵒᵖ ⋙ evaluationUncurried Cᵒᵖ (Type u₁) ⋙ 𝟭 (Type u₁)) = 𝟭 (Cᵒᵖ ⥤ Type u₁)
[PROOFSTEP]
apply Functor.ext
[GOAL]
case refine_2.h_map
C✝ : Type u₁
inst✝¹ : Category.{v₁, u₁} C✝
C : Type u₁
inst✝ : SmallCategory C
⊢ autoParam
    (∀ (X Y : Cᵒᵖ ⥤ Type u₁) (f : X ⟶ Y),
      (curry.obj (Prod.swap (Cᵒᵖ ⥤ Type u₁) Cᵒᵖ ⋙ evaluationUncurried Cᵒᵖ (Type u₁) ⋙ 𝟭 (Type u₁))).map f =
        eqToHom (_ : ?F.obj X = ?G.obj X) ≫
          (𝟭 (Cᵒᵖ ⥤ Type u₁)).map f ≫
            eqToHom
              (_ :
                (𝟭 (Cᵒᵖ ⥤ Type u₁)).obj Y =
                  (curry.obj (Prod.swap (Cᵒᵖ ⥤ Type u₁) Cᵒᵖ ⋙ evaluationUncurried Cᵒᵖ (Type u₁) ⋙ 𝟭 (Type u₁))).obj Y))
    _auto✝
[PROOFSTEP]
aesop_cat
