[GOAL]
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type w
x y : Elements F
h₁ : x.fst = y.fst
h₂ : F.map (eqToHom h₁) x.snd = y.snd
⊢ x = y
[PROOFSTEP]
cases x
[GOAL]
case mk
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type w
y : Elements F
fst✝ : C
snd✝ : F.obj fst✝
h₁ : { fst := fst✝, snd := snd✝ }.fst = y.fst
h₂ : F.map (eqToHom h₁) { fst := fst✝, snd := snd✝ }.snd = y.snd
⊢ { fst := fst✝, snd := snd✝ } = y
[PROOFSTEP]
cases y
[GOAL]
case mk.mk
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type w
fst✝¹ : C
snd✝¹ : F.obj fst✝¹
fst✝ : C
snd✝ : F.obj fst✝
h₁ : { fst := fst✝¹, snd := snd✝¹ }.fst = { fst := fst✝, snd := snd✝ }.fst
h₂ : F.map (eqToHom h₁) { fst := fst✝¹, snd := snd✝¹ }.snd = { fst := fst✝, snd := snd✝ }.snd
⊢ { fst := fst✝¹, snd := snd✝¹ } = { fst := fst✝, snd := snd✝ }
[PROOFSTEP]
cases h₁
[GOAL]
case mk.mk.refl
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type w
fst✝ : C
snd✝¹ snd✝ : F.obj fst✝
h₂ :
  F.map (eqToHom (_ : { fst := fst✝, snd := snd✝¹ }.fst = { fst := fst✝, snd := snd✝¹ }.fst))
      { fst := fst✝, snd := snd✝¹ }.snd =
    { fst := fst✝, snd := snd✝ }.snd
⊢ { fst := fst✝, snd := snd✝¹ } = { fst := fst✝, snd := snd✝ }
[PROOFSTEP]
simp only [eqToHom_refl, FunctorToTypes.map_id_apply] at h₂ 
[GOAL]
case mk.mk.refl
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type w
fst✝ : C
snd✝¹ snd✝ : F.obj fst✝
h₂ : snd✝¹ = snd✝
⊢ { fst := fst✝, snd := snd✝¹ } = { fst := fst✝, snd := snd✝ }
[PROOFSTEP]
simp [h₂]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type w
p : Functor.Elements F
⊢ F.map (𝟙 p.fst) p.snd = p.snd
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type w
X Y Z : Functor.Elements F
f : X ⟶ Y
g : Y ⟶ Z
⊢ F.map (↑f ≫ ↑g) X.snd = Z.snd
[PROOFSTEP]
simp [f.2, g.2]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
G : Type u
inst✝ : Groupoid G
F : G ⥤ Type w
p q : Functor.Elements F
f : p ⟶ q
⊢ F.map (inv ↑f) q.snd = F.map (inv ↑f) (F.map (↑f) p.snd)
[PROOFSTEP]
rw [f.2]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
G : Type u
inst✝ : Groupoid G
F : G ⥤ Type w
p q : Functor.Elements F
f : p ⟶ q
⊢ (F.map ↑f ≫ F.map (inv ↑f)) p.snd = p.snd
[PROOFSTEP]
rw [← F.map_comp]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
G : Type u
inst✝ : Groupoid G
F : G ⥤ Type w
p q : Functor.Elements F
f : p ⟶ q
⊢ F.map (↑f ≫ inv ↑f) p.snd = p.snd
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
G : Type u
inst✝ : Groupoid G
F : G ⥤ Type w
X✝ Y✝ : Functor.Elements F
x✝ : X✝ ⟶ Y✝
⊢ (fun {p q} f => { val := inv ↑f, property := (_ : F.map (inv ↑f) q.snd = p.snd) }) x✝ ≫ x✝ = 𝟙 Y✝
[PROOFSTEP]
ext
[GOAL]
case w
C : Type u
inst✝¹ : Category.{v, u} C
G : Type u
inst✝ : Groupoid G
F : G ⥤ Type w
X✝ Y✝ : Functor.Elements F
x✝ : X✝ ⟶ Y✝
⊢ ↑((fun {p q} f => { val := inv ↑f, property := (_ : F.map (inv ↑f) q.snd = p.snd) }) x✝ ≫ x✝) = ↑(𝟙 Y✝)
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
G : Type u
inst✝ : Groupoid G
F : G ⥤ Type w
X✝ Y✝ : Functor.Elements F
x✝ : X✝ ⟶ Y✝
⊢ x✝ ≫ (fun {p q} f => { val := inv ↑f, property := (_ : F.map (inv ↑f) q.snd = p.snd) }) x✝ = 𝟙 X✝
[PROOFSTEP]
ext
[GOAL]
case w
C : Type u
inst✝¹ : Category.{v, u} C
G : Type u
inst✝ : Groupoid G
F : G ⥤ Type w
X✝ Y✝ : Functor.Elements F
x✝ : X✝ ⟶ Y✝
⊢ ↑(x✝ ≫ (fun {p q} f => { val := inv ↑f, property := (_ : F.map (inv ↑f) q.snd = p.snd) }) x✝) = ↑(𝟙 X✝)
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
F F₁ F₂ : C ⥤ Type w
α : F₁ ⟶ F₂
t₁ t₂ : Functor.Elements F₁
k : t₁ ⟶ t₂
⊢ F₂.map (↑k) ((fun t => { fst := t.fst, snd := NatTrans.app α t.fst t.snd }) t₁).snd =
    ((fun t => { fst := t.fst, snd := NatTrans.app α t.fst t.snd }) t₂).snd
[PROOFSTEP]
simpa [← k.2] using (FunctorToTypes.naturality _ _ α k.1 t₁.2).symm
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type w
X Y : Functor.Elements F
f : X ⟶ Y
⊢ ((fun X => StructuredArrow.mk fun x => X.snd) X).hom ≫ F.map ↑f = ((fun X => StructuredArrow.mk fun x => X.snd) Y).hom
[PROOFSTEP]
funext
[GOAL]
case h
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type w
X Y : Functor.Elements F
f : X ⟶ Y
x✝ : (Functor.fromPUnit PUnit).obj ((fun X => StructuredArrow.mk fun x => X.snd) X).left
⊢ (((fun X => StructuredArrow.mk fun x => X.snd) X).hom ≫ F.map ↑f) x✝ =
    Comma.hom ((fun X => StructuredArrow.mk fun x => X.snd) Y) x✝
[PROOFSTEP]
simp [f.2]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type w
X : Functor.Elements F
⊢ (𝟭 (Functor.Elements F)).obj X = (toStructuredArrow F ⋙ fromStructuredArrow F).obj X
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
F✝ : C ⥤ Type w
F : Cᵒᵖ ⥤ Type v
X✝ Y✝ : (Functor.Elements F)ᵒᵖ
f : X✝ ⟶ Y✝
⊢ (fun X => CostructuredArrow.mk ((yonedaSections X.unop.fst.unop F).inv { down := X.unop.snd })) X✝ ⟶
    (fun X => CostructuredArrow.mk ((yonedaSections X.unop.fst.unop F).inv { down := X.unop.snd })) Y✝
[PROOFSTEP]
fapply CostructuredArrow.homMk
[GOAL]
case g
C : Type u
inst✝ : Category.{v, u} C
F✝ : C ⥤ Type w
F : Cᵒᵖ ⥤ Type v
X✝ Y✝ : (Functor.Elements F)ᵒᵖ
f : X✝ ⟶ Y✝
⊢ ((fun X => CostructuredArrow.mk ((yonedaSections X.unop.fst.unop F).inv { down := X.unop.snd })) X✝).left ⟶
    ((fun X => CostructuredArrow.mk ((yonedaSections X.unop.fst.unop F).inv { down := X.unop.snd })) Y✝).left
[PROOFSTEP]
exact f.unop.val.unop
[GOAL]
case w
C : Type u
inst✝ : Category.{v, u} C
F✝ : C ⥤ Type w
F : Cᵒᵖ ⥤ Type v
X✝ Y✝ : (Functor.Elements F)ᵒᵖ
f : X✝ ⟶ Y✝
⊢ autoParam
    (yoneda.map (↑f.unop).unop ≫
        ((fun X => CostructuredArrow.mk ((yonedaSections X.unop.fst.unop F).inv { down := X.unop.snd })) Y✝).hom =
      ((fun X => CostructuredArrow.mk ((yonedaSections X.unop.fst.unop F).inv { down := X.unop.snd })) X✝).hom)
    _auto✝
[PROOFSTEP]
ext Z y
[GOAL]
case w.w.h.h
C : Type u
inst✝ : Category.{v, u} C
F✝ : C ⥤ Type w
F : Cᵒᵖ ⥤ Type v
X✝ Y✝ : (Functor.Elements F)ᵒᵖ
f : X✝ ⟶ Y✝
Z : Cᵒᵖ
y :
  (yoneda.obj
        ((fun X => CostructuredArrow.mk ((yonedaSections X.unop.fst.unop F).inv { down := X.unop.snd })) X✝).left).obj
    Z
⊢ NatTrans.app
      (yoneda.map (↑f.unop).unop ≫
        ((fun X => CostructuredArrow.mk ((yonedaSections X.unop.fst.unop F).inv { down := X.unop.snd })) Y✝).hom)
      Z y =
    NatTrans.app
      ((fun X => CostructuredArrow.mk ((yonedaSections X.unop.fst.unop F).inv { down := X.unop.snd })) X✝).hom Z y
[PROOFSTEP]
dsimp
[GOAL]
case w.w.h.h
C : Type u
inst✝ : Category.{v, u} C
F✝ : C ⥤ Type w
F : Cᵒᵖ ⥤ Type v
X✝ Y✝ : (Functor.Elements F)ᵒᵖ
f : X✝ ⟶ Y✝
Z : Cᵒᵖ
y :
  (yoneda.obj
        ((fun X => CostructuredArrow.mk ((yonedaSections X.unop.fst.unop F).inv { down := X.unop.snd })) X✝).left).obj
    Z
⊢ F.map (↑f.unop ≫ y.op) Y✝.unop.snd = F.map y.op X✝.unop.snd
[PROOFSTEP]
simp only [FunctorToTypes.map_comp_apply, ← f.unop.2]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
F✝ : C ⥤ Type w
F : Cᵒᵖ ⥤ Type v
X Y : (CostructuredArrow yoneda F)ᵒᵖ
f : X ⟶ Y
⊢ F.map f.unop.left.op ((fun X => { fst := op X.unop.left, snd := Equiv.toFun yonedaEquiv X.unop.hom }) X).snd =
    ((fun X => { fst := op X.unop.left, snd := Equiv.toFun yonedaEquiv X.unop.hom }) Y).snd
[PROOFSTEP]
convert (congr_fun ((unop X).hom.naturality f.unop.left.op) (𝟙 _)).symm
[GOAL]
case h.e'_3.h
C : Type u
inst✝ : Category.{v, u} C
F✝ : C ⥤ Type w
F : Cᵒᵖ ⥤ Type v
X Y : (CostructuredArrow yoneda F)ᵒᵖ
f : X ⟶ Y
e_1✝ :
  F.obj ((fun X => { fst := op X.unop.left, snd := Equiv.toFun yonedaEquiv X.unop.hom }) Y).fst =
    ((Functor.fromPUnit F).obj X.unop.right).obj (op Y.unop.left)
⊢ ((fun X => { fst := op X.unop.left, snd := Equiv.toFun yonedaEquiv X.unop.hom }) Y).snd =
    ((yoneda.obj X.unop.left).map f.unop.left.op ≫ NatTrans.app X.unop.hom (op Y.unop.left)) (𝟙 (op X.unop.left).unop)
[PROOFSTEP]
simp only [Equiv.toFun_as_coe, Quiver.Hom.unop_op, yonedaEquiv_apply, types_comp_apply, Category.comp_id,
  yoneda_obj_map]
[GOAL]
case h.e'_3.h
C : Type u
inst✝ : Category.{v, u} C
F✝ : C ⥤ Type w
F : Cᵒᵖ ⥤ Type v
X Y : (CostructuredArrow yoneda F)ᵒᵖ
f : X ⟶ Y
e_1✝ :
  F.obj ((fun X => { fst := op X.unop.left, snd := Equiv.toFun yonedaEquiv X.unop.hom }) Y).fst =
    ((Functor.fromPUnit F).obj X.unop.right).obj (op Y.unop.left)
⊢ NatTrans.app Y.unop.hom (op Y.unop.left) (𝟙 Y.unop.left) = NatTrans.app X.unop.hom (op Y.unop.left) f.unop.left
[PROOFSTEP]
have : yoneda.map f.unop.left ≫ (unop X).hom = (unop Y).hom := by convert f.unop.3
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
F✝ : C ⥤ Type w
F : Cᵒᵖ ⥤ Type v
X Y : (CostructuredArrow yoneda F)ᵒᵖ
f : X ⟶ Y
e_1✝ :
  F.obj ((fun X => { fst := op X.unop.left, snd := Equiv.toFun yonedaEquiv X.unop.hom }) Y).fst =
    ((Functor.fromPUnit F).obj X.unop.right).obj (op Y.unop.left)
⊢ yoneda.map f.unop.left ≫ X.unop.hom = Y.unop.hom
[PROOFSTEP]
convert f.unop.3
[GOAL]
case h.e'_3.h
C : Type u
inst✝ : Category.{v, u} C
F✝ : C ⥤ Type w
F : Cᵒᵖ ⥤ Type v
X Y : (CostructuredArrow yoneda F)ᵒᵖ
f : X ⟶ Y
e_1✝ :
  F.obj ((fun X => { fst := op X.unop.left, snd := Equiv.toFun yonedaEquiv X.unop.hom }) Y).fst =
    ((Functor.fromPUnit F).obj X.unop.right).obj (op Y.unop.left)
this : yoneda.map f.unop.left ≫ X.unop.hom = Y.unop.hom
⊢ NatTrans.app Y.unop.hom (op Y.unop.left) (𝟙 Y.unop.left) = NatTrans.app X.unop.hom (op Y.unop.left) f.unop.left
[PROOFSTEP]
erw [← this]
[GOAL]
case h.e'_3.h
C : Type u
inst✝ : Category.{v, u} C
F✝ : C ⥤ Type w
F : Cᵒᵖ ⥤ Type v
X Y : (CostructuredArrow yoneda F)ᵒᵖ
f : X ⟶ Y
e_1✝ :
  F.obj ((fun X => { fst := op X.unop.left, snd := Equiv.toFun yonedaEquiv X.unop.hom }) Y).fst =
    ((Functor.fromPUnit F).obj X.unop.right).obj (op Y.unop.left)
this : yoneda.map f.unop.left ≫ X.unop.hom = Y.unop.hom
⊢ NatTrans.app (yoneda.map f.unop.left ≫ X.unop.hom) (op Y.unop.left) (𝟙 Y.unop.left) =
    NatTrans.app X.unop.hom (op Y.unop.left) f.unop.left
[PROOFSTEP]
simp only [yoneda_map_app, FunctorToTypes.comp]
[GOAL]
case h.e'_3.h
C : Type u
inst✝ : Category.{v, u} C
F✝ : C ⥤ Type w
F : Cᵒᵖ ⥤ Type v
X Y : (CostructuredArrow yoneda F)ᵒᵖ
f : X ⟶ Y
e_1✝ :
  F.obj ((fun X => { fst := op X.unop.left, snd := Equiv.toFun yonedaEquiv X.unop.hom }) Y).fst =
    ((Functor.fromPUnit F).obj X.unop.right).obj (op Y.unop.left)
this : yoneda.map f.unop.left ≫ X.unop.hom = Y.unop.hom
⊢ NatTrans.app X.unop.hom (op Y.unop.left) (𝟙 Y.unop.left ≫ f.unop.left) =
    NatTrans.app X.unop.hom (op Y.unop.left) f.unop.left
[PROOFSTEP]
erw [Category.id_comp]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
F✝ : C ⥤ Type w
F : Cᵒᵖ ⥤ Type v
⊢ (toCostructuredArrow F).rightOp ⋙ fromCostructuredArrow F = 𝟭 (Functor.Elements F)
[PROOFSTEP]
refine' Functor.ext _ _
[GOAL]
case refine'_1
C : Type u
inst✝ : Category.{v, u} C
F✝ : C ⥤ Type w
F : Cᵒᵖ ⥤ Type v
⊢ ∀ (X : Functor.Elements F),
    ((toCostructuredArrow F).rightOp ⋙ fromCostructuredArrow F).obj X = (𝟭 (Functor.Elements F)).obj X
[PROOFSTEP]
intro X
[GOAL]
case refine'_1
C : Type u
inst✝ : Category.{v, u} C
F✝ : C ⥤ Type w
F : Cᵒᵖ ⥤ Type v
X : Functor.Elements F
⊢ ((toCostructuredArrow F).rightOp ⋙ fromCostructuredArrow F).obj X = (𝟭 (Functor.Elements F)).obj X
[PROOFSTEP]
exact Functor.Elements.ext _ _ rfl (by simp [yonedaEquiv])
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
F✝ : C ⥤ Type w
F : Cᵒᵖ ⥤ Type v
X : Functor.Elements F
⊢ F.map
      (eqToHom
        (_ :
          (((toCostructuredArrow F).rightOp ⋙ fromCostructuredArrow F).obj X).fst =
            (((toCostructuredArrow F).rightOp ⋙ fromCostructuredArrow F).obj X).fst))
      (((toCostructuredArrow F).rightOp ⋙ fromCostructuredArrow F).obj X).snd =
    ((𝟭 (Functor.Elements F)).obj X).snd
[PROOFSTEP]
simp [yonedaEquiv]
[GOAL]
case refine'_2
C : Type u
inst✝ : Category.{v, u} C
F✝ : C ⥤ Type w
F : Cᵒᵖ ⥤ Type v
⊢ ∀ (X Y : Functor.Elements F) (f : X ⟶ Y),
    ((toCostructuredArrow F).rightOp ⋙ fromCostructuredArrow F).map f =
      eqToHom (_ : ((toCostructuredArrow F).rightOp ⋙ fromCostructuredArrow F).obj X = (𝟭 (Functor.Elements F)).obj X) ≫
        (𝟭 (Functor.Elements F)).map f ≫
          eqToHom
            (_ : (𝟭 (Functor.Elements F)).obj Y = ((toCostructuredArrow F).rightOp ⋙ fromCostructuredArrow F).obj Y)
[PROOFSTEP]
intro X Y f
[GOAL]
case refine'_2
C : Type u
inst✝ : Category.{v, u} C
F✝ : C ⥤ Type w
F : Cᵒᵖ ⥤ Type v
X Y : Functor.Elements F
f : X ⟶ Y
⊢ ((toCostructuredArrow F).rightOp ⋙ fromCostructuredArrow F).map f =
    eqToHom (_ : ((toCostructuredArrow F).rightOp ⋙ fromCostructuredArrow F).obj X = (𝟭 (Functor.Elements F)).obj X) ≫
      (𝟭 (Functor.Elements F)).map f ≫
        eqToHom (_ : (𝟭 (Functor.Elements F)).obj Y = ((toCostructuredArrow F).rightOp ⋙ fromCostructuredArrow F).obj Y)
[PROOFSTEP]
have : ∀ {a b : F.Elements} (H : a = b), (eqToHom H).1 = eqToHom (show a.fst = b.fst by cases H; rfl) :=
  by
  rintro _ _ rfl
  simp
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
F✝ : C ⥤ Type w
F : Cᵒᵖ ⥤ Type v
X Y : Functor.Elements F
f : X ⟶ Y
a b : Functor.Elements F
H : a = b
⊢ a.fst = b.fst
[PROOFSTEP]
cases H
[GOAL]
case refl
C : Type u
inst✝ : Category.{v, u} C
F✝ : C ⥤ Type w
F : Cᵒᵖ ⥤ Type v
X Y : Functor.Elements F
f : X ⟶ Y
a : Functor.Elements F
⊢ a.fst = a.fst
[PROOFSTEP]
rfl
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
F✝ : C ⥤ Type w
F : Cᵒᵖ ⥤ Type v
X Y : Functor.Elements F
f : X ⟶ Y
⊢ ∀ {a b : Functor.Elements F} (H : a = b), ↑(eqToHom H) = eqToHom (_ : a.fst = b.fst)
[PROOFSTEP]
rintro _ _ rfl
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
F✝ : C ⥤ Type w
F : Cᵒᵖ ⥤ Type v
X Y : Functor.Elements F
f : X ⟶ Y
a✝ : Functor.Elements F
⊢ ↑(eqToHom (_ : a✝ = a✝)) = eqToHom (_ : a✝.fst = a✝.fst)
[PROOFSTEP]
simp
[GOAL]
case refine'_2
C : Type u
inst✝ : Category.{v, u} C
F✝ : C ⥤ Type w
F : Cᵒᵖ ⥤ Type v
X Y : Functor.Elements F
f : X ⟶ Y
this : ∀ {a b : Functor.Elements F} (H : a = b), ↑(eqToHom H) = eqToHom (_ : a.fst = b.fst)
⊢ ((toCostructuredArrow F).rightOp ⋙ fromCostructuredArrow F).map f =
    eqToHom (_ : ((toCostructuredArrow F).rightOp ⋙ fromCostructuredArrow F).obj X = (𝟭 (Functor.Elements F)).obj X) ≫
      (𝟭 (Functor.Elements F)).map f ≫
        eqToHom (_ : (𝟭 (Functor.Elements F)).obj Y = ((toCostructuredArrow F).rightOp ⋙ fromCostructuredArrow F).obj Y)
[PROOFSTEP]
ext
[GOAL]
case refine'_2.w
C : Type u
inst✝ : Category.{v, u} C
F✝ : C ⥤ Type w
F : Cᵒᵖ ⥤ Type v
X Y : Functor.Elements F
f : X ⟶ Y
this : ∀ {a b : Functor.Elements F} (H : a = b), ↑(eqToHom H) = eqToHom (_ : a.fst = b.fst)
⊢ ↑(((toCostructuredArrow F).rightOp ⋙ fromCostructuredArrow F).map f) =
    ↑(eqToHom (_ : ((toCostructuredArrow F).rightOp ⋙ fromCostructuredArrow F).obj X = (𝟭 (Functor.Elements F)).obj X) ≫
        (𝟭 (Functor.Elements F)).map f ≫
          eqToHom
            (_ : (𝟭 (Functor.Elements F)).obj Y = ((toCostructuredArrow F).rightOp ⋙ fromCostructuredArrow F).obj Y))
[PROOFSTEP]
simp [this]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
F✝ : C ⥤ Type w
F : Cᵒᵖ ⥤ Type v
⊢ (fromCostructuredArrow F).rightOp ⋙ toCostructuredArrow F = 𝟭 (CostructuredArrow yoneda F)
[PROOFSTEP]
refine' Functor.ext _ _
[GOAL]
case refine'_1
C : Type u
inst✝ : Category.{v, u} C
F✝ : C ⥤ Type w
F : Cᵒᵖ ⥤ Type v
⊢ ∀ (X : CostructuredArrow yoneda F),
    ((fromCostructuredArrow F).rightOp ⋙ toCostructuredArrow F).obj X = (𝟭 (CostructuredArrow yoneda F)).obj X
[PROOFSTEP]
intro X
[GOAL]
case refine'_1
C : Type u
inst✝ : Category.{v, u} C
F✝ : C ⥤ Type w
F : Cᵒᵖ ⥤ Type v
X : CostructuredArrow yoneda F
⊢ ((fromCostructuredArrow F).rightOp ⋙ toCostructuredArrow F).obj X = (𝟭 (CostructuredArrow yoneda F)).obj X
[PROOFSTEP]
cases' X with X_left X_right X_hom
[GOAL]
case refine'_1.mk
C : Type u
inst✝ : Category.{v, u} C
F✝ : C ⥤ Type w
F : Cᵒᵖ ⥤ Type v
X_left : C
X_right : Discrete PUnit
X_hom : yoneda.obj X_left ⟶ (Functor.fromPUnit F).obj X_right
⊢ ((fromCostructuredArrow F).rightOp ⋙ toCostructuredArrow F).obj { left := X_left, right := X_right, hom := X_hom } =
    (𝟭 (CostructuredArrow yoneda F)).obj { left := X_left, right := X_right, hom := X_hom }
[PROOFSTEP]
cases X_right
[GOAL]
case refine'_1.mk.mk
C : Type u
inst✝ : Category.{v, u} C
F✝ : C ⥤ Type w
F : Cᵒᵖ ⥤ Type v
X_left : C
as✝ : PUnit
X_hom : yoneda.obj X_left ⟶ (Functor.fromPUnit F).obj { as := as✝ }
⊢ ((fromCostructuredArrow F).rightOp ⋙ toCostructuredArrow F).obj
      { left := X_left, right := { as := as✝ }, hom := X_hom } =
    (𝟭 (CostructuredArrow yoneda F)).obj { left := X_left, right := { as := as✝ }, hom := X_hom }
[PROOFSTEP]
simp only [Functor.id_obj, Functor.rightOp_obj, toCostructuredArrow_obj, Functor.comp_obj, CostructuredArrow.mk]
[GOAL]
case refine'_1.mk.mk
C : Type u
inst✝ : Category.{v, u} C
F✝ : C ⥤ Type w
F : Cᵒᵖ ⥤ Type v
X_left : C
as✝ : PUnit
X_hom : yoneda.obj X_left ⟶ (Functor.fromPUnit F).obj { as := as✝ }
⊢ {
      left :=
        (op
                ((fromCostructuredArrow F).obj
                  (op { left := X_left, right := { as := as✝ }, hom := X_hom }))).unop.fst.unop,
      right := { as := PUnit.unit },
      hom :=
        (yonedaSections
              (op
                      ((fromCostructuredArrow F).obj
                        (op { left := X_left, right := { as := as✝ }, hom := X_hom }))).unop.fst.unop
              F).inv
          {
            down :=
              (op
                    ((fromCostructuredArrow F).obj
                      (op { left := X_left, right := { as := as✝ }, hom := X_hom }))).unop.snd } } =
    { left := X_left, right := { as := as✝ }, hom := X_hom }
[PROOFSTEP]
congr
[GOAL]
case refine'_1.mk.mk.e_hom
C : Type u
inst✝ : Category.{v, u} C
F✝ : C ⥤ Type w
F : Cᵒᵖ ⥤ Type v
X_left : C
as✝ : PUnit
X_hom : yoneda.obj X_left ⟶ (Functor.fromPUnit F).obj { as := as✝ }
⊢ (yonedaSections
          (op
                  ((fromCostructuredArrow F).obj
                    (op { left := X_left, right := { as := as✝ }, hom := X_hom }))).unop.fst.unop
          F).inv
      {
        down :=
          (op
                ((fromCostructuredArrow F).obj
                  (op { left := X_left, right := { as := as✝ }, hom := X_hom }))).unop.snd } =
    X_hom
[PROOFSTEP]
ext x f
[GOAL]
case refine'_1.mk.mk.e_hom.w.h.h
C : Type u
inst✝ : Category.{v, u} C
F✝ : C ⥤ Type w
F : Cᵒᵖ ⥤ Type v
X_left : C
as✝ : PUnit
X_hom : yoneda.obj X_left ⟶ (Functor.fromPUnit F).obj { as := as✝ }
x : Cᵒᵖ
f :
  (yoneda.obj
        (op
                ((fromCostructuredArrow F).obj
                  (op { left := X_left, right := { as := as✝ }, hom := X_hom }))).unop.fst.unop).obj
    x
⊢ NatTrans.app
      ((yonedaSections
            (op
                    ((fromCostructuredArrow F).obj
                      (op { left := X_left, right := { as := as✝ }, hom := X_hom }))).unop.fst.unop
            F).inv
        {
          down :=
            (op
                  ((fromCostructuredArrow F).obj
                    (op { left := X_left, right := { as := as✝ }, hom := X_hom }))).unop.snd })
      x f =
    NatTrans.app X_hom x f
[PROOFSTEP]
convert congr_fun (X_hom.naturality f.op).symm (𝟙 X_left)
[GOAL]
case h.e'_3.h
C : Type u
inst✝ : Category.{v, u} C
F✝ : C ⥤ Type w
F : Cᵒᵖ ⥤ Type v
X_left : C
as✝ : PUnit
X_hom : yoneda.obj X_left ⟶ (Functor.fromPUnit F).obj { as := as✝ }
x : Cᵒᵖ
f :
  (yoneda.obj
        (op
                ((fromCostructuredArrow F).obj
                  (op { left := X_left, right := { as := as✝ }, hom := X_hom }))).unop.fst.unop).obj
    x
e_1✝ : F.obj x = ((Functor.fromPUnit F).obj { as := as✝ }).obj (op x.unop)
⊢ NatTrans.app X_hom x f = ((yoneda.obj X_left).map f.op ≫ NatTrans.app X_hom (op x.unop)) (𝟙 X_left)
[PROOFSTEP]
simp
[GOAL]
case refine'_2
C : Type u
inst✝ : Category.{v, u} C
F✝ : C ⥤ Type w
F : Cᵒᵖ ⥤ Type v
⊢ ∀ (X Y : CostructuredArrow yoneda F) (f : X ⟶ Y),
    ((fromCostructuredArrow F).rightOp ⋙ toCostructuredArrow F).map f =
      eqToHom
          (_ :
            ((fromCostructuredArrow F).rightOp ⋙ toCostructuredArrow F).obj X =
              (𝟭 (CostructuredArrow yoneda F)).obj X) ≫
        (𝟭 (CostructuredArrow yoneda F)).map f ≫
          eqToHom
            (_ :
              (𝟭 (CostructuredArrow yoneda F)).obj Y =
                ((fromCostructuredArrow F).rightOp ⋙ toCostructuredArrow F).obj Y)
[PROOFSTEP]
intro X Y f
[GOAL]
case refine'_2
C : Type u
inst✝ : Category.{v, u} C
F✝ : C ⥤ Type w
F : Cᵒᵖ ⥤ Type v
X Y : CostructuredArrow yoneda F
f : X ⟶ Y
⊢ ((fromCostructuredArrow F).rightOp ⋙ toCostructuredArrow F).map f =
    eqToHom
        (_ :
          ((fromCostructuredArrow F).rightOp ⋙ toCostructuredArrow F).obj X = (𝟭 (CostructuredArrow yoneda F)).obj X) ≫
      (𝟭 (CostructuredArrow yoneda F)).map f ≫
        eqToHom
          (_ :
            (𝟭 (CostructuredArrow yoneda F)).obj Y = ((fromCostructuredArrow F).rightOp ⋙ toCostructuredArrow F).obj Y)
[PROOFSTEP]
ext
[GOAL]
case refine'_2.h
C : Type u
inst✝ : Category.{v, u} C
F✝ : C ⥤ Type w
F : Cᵒᵖ ⥤ Type v
X Y : CostructuredArrow yoneda F
f : X ⟶ Y
⊢ (((fromCostructuredArrow F).rightOp ⋙ toCostructuredArrow F).map f).left =
    (eqToHom
          (_ :
            ((fromCostructuredArrow F).rightOp ⋙ toCostructuredArrow F).obj X =
              (𝟭 (CostructuredArrow yoneda F)).obj X) ≫
        (𝟭 (CostructuredArrow yoneda F)).map f ≫
          eqToHom
            (_ :
              (𝟭 (CostructuredArrow yoneda F)).obj Y =
                ((fromCostructuredArrow F).rightOp ⋙ toCostructuredArrow F).obj Y)).left
[PROOFSTEP]
simp [CostructuredArrow.eqToHom_left]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type w
F₁ F₂ : Cᵒᵖ ⥤ Type v
α : F₁ ⟶ F₂
⊢ (map α).op ⋙ toCostructuredArrow F₂ = toCostructuredArrow F₁ ⋙ CostructuredArrow.map α
[PROOFSTEP]
fapply Functor.ext
[GOAL]
case h_obj
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type w
F₁ F₂ : Cᵒᵖ ⥤ Type v
α : F₁ ⟶ F₂
⊢ ∀ (X : (Functor.Elements F₁)ᵒᵖ),
    ((map α).op ⋙ toCostructuredArrow F₂).obj X = (toCostructuredArrow F₁ ⋙ CostructuredArrow.map α).obj X
[PROOFSTEP]
intro X
[GOAL]
case h_obj
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type w
F₁ F₂ : Cᵒᵖ ⥤ Type v
α : F₁ ⟶ F₂
X : (Functor.Elements F₁)ᵒᵖ
⊢ ((map α).op ⋙ toCostructuredArrow F₂).obj X = (toCostructuredArrow F₁ ⋙ CostructuredArrow.map α).obj X
[PROOFSTEP]
simp only [CostructuredArrow.map_mk, toCostructuredArrow_obj, Functor.op_obj, Functor.comp_obj]
[GOAL]
case h_obj
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type w
F₁ F₂ : Cᵒᵖ ⥤ Type v
α : F₁ ⟶ F₂
X : (Functor.Elements F₁)ᵒᵖ
⊢ CostructuredArrow.mk
      ((yonedaSections (op ((map α).obj X.unop)).unop.fst.unop F₂).inv { down := (op ((map α).obj X.unop)).unop.snd }) =
    CostructuredArrow.mk ((yonedaSections X.unop.fst.unop F₁).inv { down := X.unop.snd } ≫ α)
[PROOFSTEP]
congr
[GOAL]
case h_obj.e_f
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type w
F₁ F₂ : Cᵒᵖ ⥤ Type v
α : F₁ ⟶ F₂
X : (Functor.Elements F₁)ᵒᵖ
⊢ (yonedaSections (op ((map α).obj X.unop)).unop.fst.unop F₂).inv { down := (op ((map α).obj X.unop)).unop.snd } =
    (yonedaSections X.unop.fst.unop F₁).inv { down := X.unop.snd } ≫ α
[PROOFSTEP]
ext _ f
[GOAL]
case h_obj.e_f.w.h.h
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type w
F₁ F₂ : Cᵒᵖ ⥤ Type v
α : F₁ ⟶ F₂
X : (Functor.Elements F₁)ᵒᵖ
x✝ : Cᵒᵖ
f : (yoneda.obj (op ((map α).obj X.unop)).unop.fst.unop).obj x✝
⊢ NatTrans.app
      ((yonedaSections (op ((map α).obj X.unop)).unop.fst.unop F₂).inv { down := (op ((map α).obj X.unop)).unop.snd })
      x✝ f =
    NatTrans.app ((yonedaSections X.unop.fst.unop F₁).inv { down := X.unop.snd } ≫ α) x✝ f
[PROOFSTEP]
simpa using congr_fun (α.naturality f.op).symm (unop X).snd
[GOAL]
case h_map
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type w
F₁ F₂ : Cᵒᵖ ⥤ Type v
α : F₁ ⟶ F₂
⊢ autoParam
    (∀ (X Y : (Functor.Elements F₁)ᵒᵖ) (f : X ⟶ Y),
      ((map α).op ⋙ toCostructuredArrow F₂).map f =
        eqToHom
            (_ :
              ((map α).op ⋙ toCostructuredArrow F₂).obj X = (toCostructuredArrow F₁ ⋙ CostructuredArrow.map α).obj X) ≫
          (toCostructuredArrow F₁ ⋙ CostructuredArrow.map α).map f ≫
            eqToHom
              (_ :
                (toCostructuredArrow F₁ ⋙ CostructuredArrow.map α).obj Y = ((map α).op ⋙ toCostructuredArrow F₂).obj Y))
    _auto✝
[PROOFSTEP]
intro X Y f
[GOAL]
case h_map
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type w
F₁ F₂ : Cᵒᵖ ⥤ Type v
α : F₁ ⟶ F₂
X Y : (Functor.Elements F₁)ᵒᵖ
f : X ⟶ Y
⊢ ((map α).op ⋙ toCostructuredArrow F₂).map f =
    eqToHom
        (_ : ((map α).op ⋙ toCostructuredArrow F₂).obj X = (toCostructuredArrow F₁ ⋙ CostructuredArrow.map α).obj X) ≫
      (toCostructuredArrow F₁ ⋙ CostructuredArrow.map α).map f ≫
        eqToHom
          (_ : (toCostructuredArrow F₁ ⋙ CostructuredArrow.map α).obj Y = ((map α).op ⋙ toCostructuredArrow F₂).obj Y)
[PROOFSTEP]
ext
[GOAL]
case h_map.h
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type w
F₁ F₂ : Cᵒᵖ ⥤ Type v
α : F₁ ⟶ F₂
X Y : (Functor.Elements F₁)ᵒᵖ
f : X ⟶ Y
⊢ (((map α).op ⋙ toCostructuredArrow F₂).map f).left =
    (eqToHom
          (_ : ((map α).op ⋙ toCostructuredArrow F₂).obj X = (toCostructuredArrow F₁ ⋙ CostructuredArrow.map α).obj X) ≫
        (toCostructuredArrow F₁ ⋙ CostructuredArrow.map α).map f ≫
          eqToHom
            (_ :
              (toCostructuredArrow F₁ ⋙ CostructuredArrow.map α).obj Y =
                ((map α).op ⋙ toCostructuredArrow F₂).obj Y)).left
[PROOFSTEP]
simp [CostructuredArrow.eqToHom_left]
