awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Elements
Goal:
C : Type u
inst : Category.{v, u} C
F_1 : Functor.{v, w, u, w + 1} C (Type w)
F : Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)
X : F.Elementsᵒᵖ
simp :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (𝟙 (F.obj (unop X).1)) : (a : F.obj (unop X).1) → F.obj (unop X).fst)
      ((unop X).snd (β := fun (c : Cᵒᵖ) ↦ F.obj c)) =
    (unop X).snd (β := fun (c : Cᵒᵖ) ↦ F.obj c)
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun)
          (F.map
            (Iso.hom
              (Iso.refl
                (((fromCostructuredArrow F).obj (op ((toCostructuredArrow F).obj X))).fst (β := fun (c : Cᵒᵖ) ↦
                  F.obj c))))) :
        (a : (fun (X : Type v) ↦ X) (F.obj ((fromCostructuredArrow F).obj (op ((toCostructuredArrow F).obj X))).fst)) →
          (fun (X : Type v) ↦ X) (F.obj (unop X).fst))
      (((fromCostructuredArrow F).obj (op ((toCostructuredArrow F).obj X))).snd (β := fun (c : Cᵒᵖ) ↦ F.obj c)) =
    (unop X).snd (β := fun (c : Cᵒᵖ) ↦ F.obj c)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Elements
Goal:
C : Type u
inst : Category.{v, u} C
F_1 : Functor.{v, w, u, w + 1} C (Type w)
F : Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)
X : F.Elementsᵒᵖ
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (𝟙 (F.obj (unop X).1)) : (a : F.obj (unop X).1) → F.obj (unop X).fst)
      ((unop X).snd (β := fun (c : Cᵒᵖ) ↦ F.obj c)) =
    (unop X).snd (β := fun (c : Cᵒᵖ) ↦ F.obj c)

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Elements
Goal:
C : Type u
inst : Category.{v, u} C
F_1 : Functor.{v, w, u, w + 1} C (Type w)
F : Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)
x y : F.Elements
f : y ⟶ x
w :
  Eq (α :=
    (unop ((toCostructuredArrow F ⋙ (fromCostructuredArrow F).rightOp).obj (op y))).fst (β := fun (c : Cᵒᵖ) ↦ F.obj c) ⟶
      (unop (Functor.obj (𝟭 F.Elementsᵒᵖ) (op x))).fst (β := fun (c : Cᵒᵖ) ↦ F.obj c))
    (↑(Quiver.Hom.unop
          (CategoryStruct.comp (Y := Functor.obj (𝟭 F.Elementsᵒᵖ) (op y)) (Functor.map (𝟭 F.Elementsᵒᵖ) (op f))
            (Iso.hom
              ((fun (X : F.Elementsᵒᵖ) ↦
                  (isoMk ((fromCostructuredArrow F).obj (op ((toCostructuredArrow F).obj X))) (unop X)
                      (Iso.refl
                        (((fromCostructuredArrow F).obj (op ((toCostructuredArrow F).obj X))).fst (β := fun (c : Cᵒᵖ) ↦
                          F.obj c)))
                      ⋯).op)
                (op y))))) :
      (unop ((toCostructuredArrow F ⋙ (fromCostructuredArrow F).rightOp).obj (op y))).fst ⟶
        (unop ((𝟭 F.Elementsᵒᵖ).obj (op x))).fst)
    (↑(Quiver.Hom.unop
          (Iso.hom
              ((fun (X : F.Elementsᵒᵖ) ↦
                  (isoMk ((fromCostructuredArrow F).obj (op ((toCostructuredArrow F).obj X))) (unop X)
                      (Iso.refl
                        (((fromCostructuredArrow F).obj (op ((toCostructuredArrow F).obj X))).fst (β := fun (c : Cᵒᵖ) ↦
                          F.obj c)))
                      ⋯).op)
                (op x)) ≫
            (toCostructuredArrow F ⋙ (fromCostructuredArrow F).rightOp).map (op f))) :
      (unop ((toCostructuredArrow F ⋙ (fromCostructuredArrow F).rightOp).obj (op y))).fst ⟶
        (unop ((𝟭 F.Elementsᵒᵖ).obj (op x))).fst)
⊢ Eq (α :=
    unop ((toCostructuredArrow F ⋙ (fromCostructuredArrow F).rightOp).obj (op y)) ⟶
      unop (Functor.obj (𝟭 F.Elementsᵒᵖ) (op x)))
    (Quiver.Hom.unop
      (CategoryStruct.comp (Y := Functor.obj (𝟭 F.Elementsᵒᵖ) (op y)) (Functor.map (𝟭 F.Elementsᵒᵖ) (op f))
        (Iso.hom
          ((fun (X : F.Elementsᵒᵖ) ↦
              (isoMk ((fromCostructuredArrow F).obj (op ((toCostructuredArrow F).obj X))) (unop X)
                  (Iso.refl
                    (((fromCostructuredArrow F).obj (op ((toCostructuredArrow F).obj X))).fst (β := fun (c : Cᵒᵖ) ↦
                      F.obj c)))
                  ⋯).op)
            (op y)))))
    (Quiver.Hom.unop
      (Iso.hom
          ((fun (X : F.Elementsᵒᵖ) ↦
              (isoMk ((fromCostructuredArrow F).obj (op ((toCostructuredArrow F).obj X))) (unop X)
                  (Iso.refl
                    (((fromCostructuredArrow F).obj (op ((toCostructuredArrow F).obj X))).fst (β := fun (c : Cᵒᵖ) ↦
                      F.obj c)))
                  ⋯).op)
            (op x)) ≫
        (toCostructuredArrow F ⋙ (fromCostructuredArrow F).rightOp).map (op f)))

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Elements
Goal:
C : Type u
inst : Category.{v, u} C
F_1 : Functor.{v, w, u, w + 1} C (Type w)
F : Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)
x y : F.Elements
f : y ⟶ x
⊢ Eq (α :=
    (unop ((toCostructuredArrow F ⋙ (fromCostructuredArrow F).rightOp).obj (op y))).fst (β := fun (c : Cᵒᵖ) ↦ F.obj c) ⟶
      (unop (Functor.obj (𝟭 F.Elementsᵒᵖ) (op x))).fst (β := fun (c : Cᵒᵖ) ↦ F.obj c))
    (↑(Quiver.Hom.unop
          (CategoryStruct.comp (Y := Functor.obj (𝟭 F.Elementsᵒᵖ) (op y)) (Functor.map (𝟭 F.Elementsᵒᵖ) (op f))
            (Iso.hom
              ((fun (X : F.Elementsᵒᵖ) ↦
                  (isoMk ((fromCostructuredArrow F).obj (op ((toCostructuredArrow F).obj X))) (unop X)
                      (Iso.refl
                        (((fromCostructuredArrow F).obj (op ((toCostructuredArrow F).obj X))).fst (β := fun (c : Cᵒᵖ) ↦
                          F.obj c)))
                      ⋯).op)
                (op y))))) :
      (unop ((toCostructuredArrow F ⋙ (fromCostructuredArrow F).rightOp).obj (op y))).fst ⟶
        (unop ((𝟭 F.Elementsᵒᵖ).obj (op x))).fst)
    (↑(Quiver.Hom.unop
          (Iso.hom
              ((fun (X : F.Elementsᵒᵖ) ↦
                  (isoMk ((fromCostructuredArrow F).obj (op ((toCostructuredArrow F).obj X))) (unop X)
                      (Iso.refl
                        (((fromCostructuredArrow F).obj (op ((toCostructuredArrow F).obj X))).fst (β := fun (c : Cᵒᵖ) ↦
                          F.obj c)))
                      ⋯).op)
                (op x)) ≫
            (toCostructuredArrow F ⋙ (fromCostructuredArrow F).rightOp).map (op f))) :
      (unop ((toCostructuredArrow F ⋙ (fromCostructuredArrow F).rightOp).obj (op y))).fst ⟶
        (unop ((𝟭 F.Elementsᵒᵖ).obj (op x))).fst)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Elements
Goal:
C : Type u
inst : Category.{v, u} C
F_1 : Functor.{v, w, u, w + 1} C (Type w)
F : Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)
x y : F.Elements
f : y ⟶ x
⊢ Eq (α := Functor.obj (𝟭 F.Elementsᵒᵖ) (op x) ⟶ (toCostructuredArrow F ⋙ (fromCostructuredArrow F).rightOp).obj (op y))
    (CategoryStruct.comp (Y := Functor.obj (𝟭 F.Elementsᵒᵖ) (op y)) (Functor.map (𝟭 F.Elementsᵒᵖ) (op f))
      (Iso.hom
        ((fun (X : F.Elementsᵒᵖ) ↦
            (isoMk ((fromCostructuredArrow F).obj (op ((toCostructuredArrow F).obj X))) (unop X)
                (Iso.refl
                  (((fromCostructuredArrow F).obj (op ((toCostructuredArrow F).obj X))).fst (β := fun (c : Cᵒᵖ) ↦
                    F.obj c)))
                ⋯).op)
          (op y))))
    (Iso.hom
        ((fun (X : F.Elementsᵒᵖ) ↦
            (isoMk ((fromCostructuredArrow F).obj (op ((toCostructuredArrow F).obj X))) (unop X)
                (Iso.refl
                  (((fromCostructuredArrow F).obj (op ((toCostructuredArrow F).obj X))).fst (β := fun (c : Cᵒᵖ) ↦
                    F.obj c)))
                ⋯).op)
          (op x)) ≫
      (toCostructuredArrow F ⋙ (fromCostructuredArrow F).rightOp).map (op f))

Tactic:
exact Quiver.Hom.unop_inj (by ext; simp)

Premises used: Quiver.Hom.unop_inj
-- Module: Mathlib.CategoryTheory.Elements
Goal:
C : Type u
inst : Category.{v, u} C
F_1 : Functor.{v, w, u, w + 1} C (Type w)
F : Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)
X : CostructuredArrow yoneda F
dsimp :
  Functor.map yoneda (𝟙 X.left) ≫ X.hom =
    (Equiv.symm yonedaEquiv : (a : F.obj (op X.left)) → yoneda.obj X.left ⟶ F)
      ((yonedaEquiv : (a : yoneda.obj X.left ⟶ F) → F.obj (op X.left)) X.hom)
⊢ Functor.map yoneda (Iso.hom (Iso.refl (((fromCostructuredArrow F).rightOp ⋙ toCostructuredArrow F).obj X).left)) ≫
      (Functor.obj (𝟭 (CostructuredArrow yoneda F)) X).hom =
    (((fromCostructuredArrow F).rightOp ⋙ toCostructuredArrow F).obj X).hom

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Elements
Goal:
C : Type u
inst : Category.{v, u} C
F_1 : Functor.{v, w, u, w + 1} C (Type w)
F : Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)
X : CostructuredArrow yoneda F
⊢ Functor.map yoneda (𝟙 X.left) ≫ X.hom =
    (Equiv.symm yonedaEquiv : (a : F.obj (op X.left)) → yoneda.obj X.left ⟶ F)
      ((yonedaEquiv : (a : yoneda.obj X.left ⟶ F) → F.obj (op X.left)) X.hom)

Tactic:
simpa only [Functor.map_id, Category.id_comp] using
      (yonedaEquiv.symm_apply_apply X.hom).symm

Premises used: Equiv.symm_apply_apply, CategoryTheory.CostructuredArrow.hom, CategoryTheory.Functor.map_id, Eq.symm, CategoryTheory.yonedaEquiv, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Elements
Goal:
C : Type u
inst : Category.{v, u} C
F₁ F₂ : Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)
α : F₁ ⟶ F₂
h_obj :
  ∀ (X : F₁.Elementsᵒᵖ),
    ((map α).op ⋙ toCostructuredArrow F₂).obj X = (toCostructuredArrow F₁ ⋙ CostructuredArrow.map α).obj X
h_map :
  autoParam
    (∀ (X Y : F₁.Elementsᵒᵖ) (f : X ⟶ Y),
      ((map α).op ⋙ toCostructuredArrow F₂).map f =
        eqToHom ⋯ ≫ (toCostructuredArrow F₁ ⋙ CostructuredArrow.map α).map f ≫ eqToHom ⋯)
    Functor.ext._auto_1
⊢ (map α).op ⋙ toCostructuredArrow F₂ = toCostructuredArrow F₁ ⋙ CostructuredArrow.map α

Tactic:
fapply Functor.ext

Premises used: CategoryTheory.Functor.ext
-- Module: Mathlib.CategoryTheory.Elements
Goal:
C : Type u
inst : Category.{v, u} C
F₁ F₂ : Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)
α : F₁ ⟶ F₂
X : F₁.Elementsᵒᵖ
h_obj :
  Eq (α := CostructuredArrow yoneda F₂)
    (CostructuredArrow.mk (Y := unop ((map α).obj (unop X)).1)
        ((Equiv.symm yonedaEquiv :
            (a : F₂.obj (op (unop ((map α).obj (unop X)).1))) → yoneda.obj (unop ((map α).obj (unop X)).1) ⟶ F₂)
          (((map α).obj (unop X)).snd (β := fun (c : Cᵒᵖ) ↦ F₂.obj c))) :
      CostructuredArrow yoneda F₂)
    (CostructuredArrow.mk (Y := unop (unop X).1)
        ((Equiv.symm yonedaEquiv : (a : F₁.obj (op (unop (unop X).1))) → yoneda.obj (unop (unop X).1) ⟶ F₁)
            ((unop X).snd (β := fun (c : Cᵒᵖ) ↦ F₁.obj c)) ≫
          α) :
      CostructuredArrow yoneda F₂)
⊢ ((map α).op ⋙ toCostructuredArrow F₂).obj X = (toCostructuredArrow F₁ ⋙ CostructuredArrow.map α).obj X

Tactic:
simp only [CostructuredArrow.map_mk, toCostructuredArrow_obj, Functor.op_obj,
      Functor.comp_obj]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.CategoryOfElements.toCostructuredArrow_obj, CategoryTheory.CostructuredArrow.map_mk, CategoryTheory.Functor.op_obj
-- Module: Mathlib.CategoryTheory.Elements
Goal:
C : Type u
inst : Category.{v, u} C
F₁ F₂ : Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)
α : F₁ ⟶ F₂
X : F₁.Elementsᵒᵖ
h_obj :
  Eq (α := Functor.obj yoneda (unop ((map α).obj (unop X)).1) ⟶ F₂)
    ((Equiv.symm yonedaEquiv :
          (a : F₂.obj (op (unop ((map α).obj (unop X)).1))) → yoneda.obj (unop ((map α).obj (unop X)).1) ⟶ F₂)
        (((map α).obj (unop X)).snd (β := fun (c : Cᵒᵖ) ↦ F₂.obj c)) :
      Functor.obj yoneda (unop ((map α).obj (unop X)).1) ⟶ F₂)
    ((Equiv.symm yonedaEquiv : (a : F₁.obj (op (unop (unop X).1))) → yoneda.obj (unop (unop X).1) ⟶ F₁)
          ((unop X).snd (β := fun (c : Cᵒᵖ) ↦ F₁.obj c)) ≫
        α :
      Functor.obj yoneda (unop (unop X).1) ⟶ F₂)
⊢ Eq (α := CostructuredArrow yoneda F₂)
    (CostructuredArrow.mk (Y := unop ((map α).obj (unop X)).1)
        ((Equiv.symm yonedaEquiv :
            (a : F₂.obj (op (unop ((map α).obj (unop X)).1))) → yoneda.obj (unop ((map α).obj (unop X)).1) ⟶ F₂)
          (((map α).obj (unop X)).snd (β := fun (c : Cᵒᵖ) ↦ F₂.obj c))) :
      CostructuredArrow yoneda F₂)
    (CostructuredArrow.mk (Y := unop (unop X).1)
        ((Equiv.symm yonedaEquiv : (a : F₁.obj (op (unop (unop X).1))) → yoneda.obj (unop (unop X).1) ⟶ F₁)
            ((unop X).snd (β := fun (c : Cᵒᵖ) ↦ F₁.obj c)) ≫
          α) :
      CostructuredArrow yoneda F₂)

Tactic:
congr
-- Module: Mathlib.CategoryTheory.Elements
Goal:
C : Type u
inst : Category.{v, u} C
F₁ F₂ : Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)
α : F₁ ⟶ F₂
X : F₁.Elementsᵒᵖ
h_obj :
  ∀ (x : Cᵒᵖ) (f : Functor.obj (Functor.obj yoneda (unop ((map α).obj (unop X)).1)) x),
    Eq (α := F₂.obj x)
      (TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (NatTrans.app
            ((Equiv.symm yonedaEquiv :
                (a : F₂.obj (op (unop ((map α).obj (unop X)).1))) → yoneda.obj (unop ((map α).obj (unop X)).1) ⟶ F₂)
              (((map α).obj (unop X)).snd (β := fun (c : Cᵒᵖ) ↦ F₂.obj c)))
            x))
        f)
      (TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (NatTrans.app
            ((Equiv.symm yonedaEquiv : (a : F₁.obj (op (unop (unop X).1))) → yoneda.obj (unop (unop X).1) ⟶ F₁)
                ((unop X).snd (β := fun (c : Cᵒᵖ) ↦ F₁.obj c)) ≫
              α)
            x))
        f)
⊢ Eq (α := Functor.obj yoneda (unop ((map α).obj (unop X)).1) ⟶ F₂)
    ((Equiv.symm yonedaEquiv :
          (a : F₂.obj (op (unop ((map α).obj (unop X)).1))) → yoneda.obj (unop ((map α).obj (unop X)).1) ⟶ F₂)
        (((map α).obj (unop X)).snd (β := fun (c : Cᵒᵖ) ↦ F₂.obj c)) :
      Functor.obj yoneda (unop ((map α).obj (unop X)).1) ⟶ F₂)
    ((Equiv.symm yonedaEquiv : (a : F₁.obj (op (unop (unop X).1))) → yoneda.obj (unop (unop X).1) ⟶ F₁)
          ((unop X).snd (β := fun (c : Cᵒᵖ) ↦ F₁.obj c)) ≫
        α :
      Functor.obj yoneda (unop (unop X).1) ⟶ F₂)

Tactic:
ext _ f
-- Module: Mathlib.CategoryTheory.Elements
Goal:
C : Type u
inst : Category.{v, u} C
F₁ F₂ : Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)
α : F₁ ⟶ F₂
X : F₁.Elementsᵒᵖ
x : Cᵒᵖ
f : Functor.obj (Functor.obj yoneda (unop ((map α).obj (unop X)).1)) x
⊢ Eq (α := F₂.obj x)
    (TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (NatTrans.app
          ((Equiv.symm yonedaEquiv :
              (a : F₂.obj (op (unop ((map α).obj (unop X)).1))) → yoneda.obj (unop ((map α).obj (unop X)).1) ⟶ F₂)
            (((map α).obj (unop X)).snd (β := fun (c : Cᵒᵖ) ↦ F₂.obj c)))
          x))
      f)
    (TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (NatTrans.app
          ((Equiv.symm yonedaEquiv : (a : F₁.obj (op (unop (unop X).1))) → yoneda.obj (unop (unop X).1) ⟶ F₁)
              ((unop X).snd (β := fun (c : Cᵒᵖ) ↦ F₁.obj c)) ≫
            α)
          x))
      f)

Tactic:
(α.naturality_apply f.op (unop X).snd).symm

Premises used: CategoryTheory.NatTrans.naturality_apply, Quiver.Hom.op, Eq.symm
-- Module: Mathlib.CategoryTheory.Elements
Goal:
C : Type u
inst : Category.{v, u} C
F₁ F₂ : Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)
α : F₁ ⟶ F₂
X : F₁.Elementsᵒᵖ
x : Cᵒᵖ
f : Functor.obj (Functor.obj yoneda (unop ((map α).obj (unop X)).1)) x
⊢ Eq (α := F₂.obj x)
    (TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (NatTrans.app
          ((Equiv.symm yonedaEquiv :
              (a : F₂.obj (op (unop ((map α).obj (unop X)).1))) → yoneda.obj (unop ((map α).obj (unop X)).1) ⟶ F₂)
            (((map α).obj (unop X)).snd (β := fun (c : Cᵒᵖ) ↦ F₂.obj c)))
          x))
      f)
    (TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (NatTrans.app
          ((Equiv.symm yonedaEquiv : (a : F₁.obj (op (unop (unop X).1))) → yoneda.obj (unop (unop X).1) ⟶ F₁)
              ((unop X).snd (β := fun (c : Cᵒᵖ) ↦ F₁.obj c)) ≫
            α)
          x))
      f)

Tactic:
exact (α.naturality_apply f.op (unop X).snd).symm

Premises used: CategoryTheory.NatTrans.naturality_apply, Quiver.Hom.op, Eq.symm
-- Module: Mathlib.CategoryTheory.Elements
Goal:
C : Type u
inst : Category.{v, u} C
F₁ F₂ : Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)
α : F₁ ⟶ F₂
⊢ autoParam
    (∀ (X Y : F₁.Elementsᵒᵖ) (f : X ⟶ Y),
      ((map α).op ⋙ toCostructuredArrow F₂).map f =
        eqToHom ⋯ ≫ (toCostructuredArrow F₁ ⋙ CostructuredArrow.map α).map f ≫ eqToHom ⋯)
    Functor.ext._auto_1

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Elements
Goal:
C : Type u
inst : Category.{v, u} C
F_1 : Functor.{v, w, u, w + 1} C (Type w)
F : Cᵒᵖ ⥤ Type (max w v)
X Y : F.Elementsᵒᵖ
f : X ⟶ Y
dsimp :
  Eq (α := Functor.obj uliftYoneda.{w, v, u} (unop (unop X).1) ⟶ F)
    (Functor.map uliftYoneda.{w, v, u} (↑(unop f) : (unop Y).fst ⟶ (unop X).fst).unop ≫
      (Equiv.symm uliftYonedaEquiv : (a : F.obj (unop Y).1) → uliftYoneda.{w, v, u}.obj (unop (unop Y).1) ⟶ F)
        ((unop Y).snd (β := fun (c : Cᵒᵖ) ↦ F.obj c)))
    ((Equiv.symm uliftYonedaEquiv : (a : F.obj (unop X).1) → uliftYoneda.{w, v, u}.obj (unop (unop X).1) ⟶ F)
      ((unop X).snd (β := fun (c : Cᵒᵖ) ↦ F.obj c)))
⊢ Eq (α :=
    Functor.obj uliftYoneda.{w, v, u}
        (CostructuredArrow.left (S := (uliftYoneda.{w, v, u} : C ⥤ Cᵒᵖ ⥤ Type (max w v)))
          (CostructuredArrow.mk (Y := unop (unop X).1)
              ((Equiv.symm uliftYonedaEquiv :
                  (a : F.obj (op (unop (unop X).1))) → uliftYoneda.{w, v, u}.obj (unop (unop X).1) ⟶ F)
                ((unop X).snd (β := fun (c : Cᵒᵖ) ↦ F.obj c))) :
            CostructuredArrow uliftYoneda.{w, v, u} F)) ⟶
      F)
    (Functor.map uliftYoneda.{w, v, u} (↑(unop f) : (unop Y).fst ⟶ (unop X).fst).unop ≫
      CostructuredArrow.hom
        (CostructuredArrow.mk (Y := unop (unop Y).1)
          ((Equiv.symm uliftYonedaEquiv :
              (a : F.obj (op (unop (unop Y).1))) → uliftYoneda.{w, v, u}.obj (unop (unop Y).1) ⟶ F)
            ((unop Y).snd (β := fun (c : Cᵒᵖ) ↦ F.obj c)))))
    (CostructuredArrow.hom
      (CostructuredArrow.mk (Y := unop (unop X).1)
        ((Equiv.symm uliftYonedaEquiv :
            (a : F.obj (op (unop (unop X).1))) → uliftYoneda.{w, v, u}.obj (unop (unop X).1) ⟶ F)
          ((unop X).snd (β := fun (c : Cᵒᵖ) ↦ F.obj c)))))

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Elements
Goal:
C : Type u
inst : Category.{v, u} C
F_1 : Functor.{v, w, u, w + 1} C (Type w)
F : Cᵒᵖ ⥤ Type (max w v)
X Y : F.Elementsᵒᵖ
f : X ⟶ Y
rw :
  Eq (α := Functor.obj uliftYoneda.{w, v, u} (unop (unop X).1) ⟶ F)
    ((Equiv.symm uliftYonedaEquiv :
          (a : F.obj (op (unop (unop X).fst))) → uliftYoneda.{w, v, u}.obj (unop (unop X).fst) ⟶ F)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (↑(unop f) : (unop Y).fst ⟶ (unop X).fst)) :
            (a : (fun (X : Type (max v w)) ↦ X) (F.obj (unop Y).fst)) →
              (fun (X : Type (max v w)) ↦ X) (F.obj (unop X).fst))
          ((unop Y).snd (β := fun (c : Cᵒᵖ) ↦ F.obj c))) :
      Functor.obj uliftYoneda.{w, v, u} (unop ((unop X).fst (β := fun (c : Cᵒᵖ) ↦ F.obj c))) ⟶ F)
    ((Equiv.symm uliftYonedaEquiv : (a : F.obj (unop X).1) → uliftYoneda.{w, v, u}.obj (unop (unop X).1) ⟶ F)
        ((unop X).snd (β := fun (c : Cᵒᵖ) ↦ F.obj c)) :
      Functor.obj uliftYoneda.{w, v, u} (unop (unop X).1) ⟶ F)
rw₁ rw₂ :
  Eq (α := Functor.obj uliftYoneda.{w, v, u} (unop (unop X).1) ⟶ F)
    ((Equiv.symm uliftYonedaEquiv :
          (a : F.obj (op (unop (unop X).fst))) → uliftYoneda.{w, v, u}.obj (unop (unop X).fst) ⟶ F)
        ((unop X).snd (β := fun (c : Cᵒᵖ) ↦ F.obj c)) :
      Functor.obj uliftYoneda.{w, v, u} (unop ((unop X).fst (β := fun (c : Cᵒᵖ) ↦ F.obj c))) ⟶ F)
    ((Equiv.symm uliftYonedaEquiv : (a : F.obj (unop X).1) → uliftYoneda.{w, v, u}.obj (unop (unop X).1) ⟶ F)
        ((unop X).snd (β := fun (c : Cᵒᵖ) ↦ F.obj c)) :
      Functor.obj uliftYoneda.{w, v, u} (unop (unop X).1) ⟶ F)
⊢ Eq (α := Functor.obj uliftYoneda.{w, v, u} (unop (unop X).1) ⟶ F)
    (Functor.map uliftYoneda.{w, v, u} (↑(unop f) : (unop Y).fst ⟶ (unop X).fst).unop ≫
      (Equiv.symm uliftYonedaEquiv : (a : F.obj (unop Y).1) → uliftYoneda.{w, v, u}.obj (unop (unop Y).1) ⟶ F)
        ((unop Y).snd (β := fun (c : Cᵒᵖ) ↦ F.obj c)))
    ((Equiv.symm uliftYonedaEquiv : (a : F.obj (unop X).1) → uliftYoneda.{w, v, u}.obj (unop (unop X).1) ⟶ F)
      ((unop X).snd (β := fun (c : Cᵒᵖ) ↦ F.obj c)))

Tactic:
rw [← uliftYonedaEquiv_symm_map, map_snd]

Premises used: CategoryTheory.CategoryOfElements.map_snd, CategoryTheory.uliftYonedaEquiv_symm_map
-- Module: Mathlib.CategoryTheory.Elements
Goal:
C : Type u
inst : Category.{v, u} C
F_1 : Functor.{v, w, u, w + 1} C (Type w)
F : Cᵒᵖ ⥤ Type (max w v)
X Y : CostructuredArrow uliftYoneda.{w, v, u} F
f : X ⟶ Y
dsimp :
  Eq (α := F.obj (op X.left))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f.left.op) : (a : F.obj (op Y.left)) → F.obj (op X.left))
        ((uliftYonedaEquiv : (a : uliftYoneda.{w, v, u}.obj Y.left ⟶ F) → F.obj (op Y.left)) Y.hom) :
      F.obj (op X.left))
    ((uliftYonedaEquiv : (a : uliftYoneda.{w, v, u}.obj X.left ⟶ F) → F.obj (op X.left)) X.hom : F.obj (op X.left))
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f.left.op) :
        (a :
            (fun (X : Type (max v w)) ↦ X)
              (F.obj
                (F.elementsMk (op Y.left)
                    ((uliftYonedaEquiv : (a : uliftYoneda.{w, v, u}.obj Y.left ⟶ F) → F.obj (op Y.left)) Y.hom)).fst)) →
          (fun (X : Type (max v w)) ↦ X)
            (F.obj
              (F.elementsMk (op X.left)
                  ((uliftYonedaEquiv : (a : uliftYoneda.{w, v, u}.obj X.left ⟶ F) → F.obj (op X.left)) X.hom)).fst))
      ((F.elementsMk (op Y.left)
            ((uliftYonedaEquiv : (a : uliftYoneda.{w, v, u}.obj Y.left ⟶ F) → F.obj (op Y.left)) Y.hom)).snd
        (β := fun (c : Cᵒᵖ) ↦ F.obj c)) =
    (F.elementsMk (op X.left)
          ((uliftYonedaEquiv : (a : uliftYoneda.{w, v, u}.obj X.left ⟶ F) → F.obj (op X.left)) X.hom)).snd
      (β := fun (c : Cᵒᵖ) ↦ F.obj c)

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Elements
Goal:
C : Type u
inst : Category.{v, u} C
F_1 : Functor.{v, w, u, w + 1} C (Type w)
F : Cᵒᵖ ⥤ Type (max w v)
X Y : CostructuredArrow uliftYoneda.{w, v, u} F
f : X ⟶ Y
rw :
  Eq (α := F.obj (op X.left))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f.left.op) : (a : F.obj (op Y.left)) → F.obj (op X.left))
        ((uliftYonedaEquiv : (a : uliftYoneda.{w, v, u}.obj Y.left ⟶ F) → F.obj (op Y.left)) Y.hom) :
      F.obj (op X.left))
    ((uliftYonedaEquiv : (a : uliftYoneda.{w, v, u}.obj X.left ⟶ F) → F.obj (op X.left))
        (Functor.map uliftYoneda.{w, v, u} f.left ≫ Y.hom) :
      F.obj (op X.left))
rw₁ :
  Eq (α := F.obj (op X.left))
    ((uliftYonedaEquiv : (a : uliftYoneda.{w, v, u}.obj (unop (op X.left)) ⟶ F) → F.obj (op (unop (op X.left))))
        (Functor.map uliftYoneda.{w, v, u} f.left.op.unop ≫ Y.hom) :
      F.obj (op (unop (op X.left))))
    ((uliftYonedaEquiv : (a : uliftYoneda.{w, v, u}.obj X.left ⟶ F) → F.obj (op X.left))
        (Functor.map uliftYoneda.{w, v, u} f.left ≫ Y.hom) :
      F.obj (op X.left))
rw₂ rw₃ :
  Eq (α := F.obj (op X.left))
    ((uliftYonedaEquiv : (a : uliftYoneda.{w, v, u}.obj (unop (op X.left)) ⟶ F) → F.obj (op (unop (op X.left))))
        (Functor.map uliftYoneda.{w, v, u} f.left ≫ Y.hom) :
      F.obj (op (unop (op X.left))))
    ((uliftYonedaEquiv : (a : uliftYoneda.{w, v, u}.obj X.left ⟶ F) → F.obj (op X.left))
        (Functor.map uliftYoneda.{w, v, u} f.left ≫ Y.hom) :
      F.obj (op X.left))
⊢ Eq (α := F.obj (op X.left))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f.left.op) : (a : F.obj (op Y.left)) → F.obj (op X.left))
        ((uliftYonedaEquiv : (a : uliftYoneda.{w, v, u}.obj Y.left ⟶ F) → F.obj (op Y.left)) Y.hom) :
      F.obj (op X.left))
    ((uliftYonedaEquiv : (a : uliftYoneda.{w, v, u}.obj X.left ⟶ F) → F.obj (op X.left)) X.hom : F.obj (op X.left))

Tactic:
rw [← CostructuredArrow.w f, uliftYonedaEquiv_naturality, Quiver.Hom.unop_op]

Premises used: Quiver.Hom.unop_op, CategoryTheory.uliftYonedaEquiv_naturality, CategoryTheory.CostructuredArrow.w
-- Module: Mathlib.CategoryTheory.Elements
Goal:
C : Type u
inst : Category.{v, u} C
F_1 : Functor.{v, w, u, w + 1} C (Type w)
F : Cᵒᵖ ⥤ Type (max w v)
x : F.Elementsᵒᵖ
dsimp :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (𝟙 (unop x).1)) : (a : F.obj (unop x).1) → F.obj (unop x).fst)
      ((uliftYonedaEquiv : (a : uliftYoneda.{w, v, u}.obj (unop (unop x).1) ⟶ F) → F.obj (unop x).1)
        ((Equiv.symm uliftYonedaEquiv : (a : F.obj (unop x).1) → uliftYoneda.{w, v, u}.obj (unop (unop x).1) ⟶ F)
          ((unop x).snd (β := fun (c : Cᵒᵖ) ↦ F.obj c)))) =
    (unop x).snd (β := fun (c : Cᵒᵖ) ↦ F.obj c)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
dsimp