case refine'_1
C : Type u
inst✝ : Category 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

case refine'_2
C : Type u
inst✝ : Category 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 (_ : ?m.78758.obj X = ?m.78759.obj X) ≫
        (𝟭 (Functor.Elements F)).map f ≫
          eqToHom
            (_ : (𝟭 (Functor.Elements F)).obj Y = ((toCostructuredArrow F).rightOp ⋙ fromCostructuredArrow F).obj Y)
C : Type u
inst✝ : Category C
F✝ : C ⥤ Type w
F : Cᵒᵖ ⥤ Type v
⊢ (toCostructuredArrow F).rightOp ⋙ fromCostructuredArrow F = 𝟭 (Functor.Elements F)
refine' Functor.ext _ _
case refine'_1
C : Type u
inst✝ : Category 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
case refine'_1
C : Type u
inst✝ : Category 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
intro X
no goals
case refine'_1
C : Type u
inst✝ : Category 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
exact Functor.Elements.ext _ _ rfl (by simp [yonedaEquiv])
no goals
C : Type u
inst✝ : Category 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
simp [yonedaEquiv]
case refine'_2
C : Type u
inst✝ : Category 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)
case refine'_2
C : Type u
inst✝ : Category 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)
intro X Y f
case refine'_2
C : Type u
inst✝ : Category 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)
case refine'_2
C : Type u
inst✝ : Category 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)
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
case refine'_2.w
C : Type u
inst✝ : Category 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))
case refine'_2
C : Type u
inst✝ : Category 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)
ext
no goals
case refine'_2.w
C : Type u
inst✝ : Category 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))
simp [this]
case refl
C : Type u
inst✝ : Category 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
C : Type u
inst✝ : Category 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
cases H
no goals
case refl
C : Type u
inst✝ : Category 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
rfl
C : Type u
inst✝ : Category 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)
C : Type u
inst✝ : Category 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)
rintro _ _ rfl
no goals
C : Type u
inst✝ : Category 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)
simp