awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Comma.Presheaf.Basic
Goal:
C : Type u
inst : Category.{v, u} C
A F : Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)
η : F ⟶ A
X : C
p : YonedaCollection (restrictedYonedaObj η) X
⊢ OverArrows.val (A := A) (η := η) (s :=
      (unop (op (CostructuredArrow.mk ((unitBackward η X ∘ unitForward η X) p).fst))).hom)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) ((restrictedYonedaObj η).map (eqToHom ⋯)) :
          (a : (fun (X : Type v) ↦ X) ((restrictedYonedaObj η).obj (op (CostructuredArrow.mk (id p).fst)))) →
            (fun (X : Type v) ↦ X)
              ((restrictedYonedaObj η).obj (op (CostructuredArrow.mk ((unitBackward η X ∘ unitForward η X) p).fst))))
        (id p).snd) =
    OverArrows.val ((unitBackward η X ∘ unitForward η X) p).snd

Tactic:
simp [unitForward, unitBackward]

Premises used: CategoryTheory.OverPresheafAux.unitForward, CategoryTheory.OverPresheafAux.unitBackward
-- Module: Mathlib.CategoryTheory.Comma.Presheaf.Basic
Goal:
C : Type u
inst : Category.{v, u} C
A : Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
X : C
s : Functor.obj yoneda X ⟶ A
p : OverArrows (yonedaCollectionPresheafToA F) s
⊢ YonedaCollection.fst p.val = s

Tactic:
simpa [YonedaCollection.yonedaEquivFst_eq] using p.app_val

Premises used: CategoryTheory.OverPresheafAux.YonedaCollection.yonedaEquivFst_eq, CategoryTheory.OverPresheafAux.OverArrows.app_val
-- Module: Mathlib.CategoryTheory.Comma.Presheaf.Basic
Goal:
C : Type u
inst : Category.{v, u} C
A : Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)
F_1 : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
X : C
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
s : CostructuredArrow yoneda A
x : F.obj (op s)
⊢ Eq (α := (fun (X : Type v) ↦ X) (A.obj (op s.left)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((yonedaCollectionPresheafToA F).app (op s.left)) :
          (a : (fun (X : Type v) ↦ X) ((yonedaCollectionPresheaf A F).obj (op s.left))) →
            (fun (X : Type v) ↦ X) (A.obj (op s.left)))
        (YonedaCollection.mk s.hom x) :
      (fun (X : Type v) ↦ X) (A.obj (op s.left)))
    ((yonedaEquiv : (a : yoneda.obj s.left ⟶ A) → A.obj (op s.left)) s.hom : A.obj (op s.left))

Tactic:
simp [YonedaCollection.yonedaEquivFst_eq]

Premises used: CategoryTheory.OverPresheafAux.YonedaCollection.yonedaEquivFst_eq
-- Module: Mathlib.CategoryTheory.Comma.Presheaf.Basic
Goal:
C : Type u
inst : Category.{v, u} C
A : Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
s : CostructuredArrow yoneda A
x : F.obj (op s)
⊢ YonedaCollection.fst (counitForward F s x).val = s.hom

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Comma.Presheaf.Basic
Goal:
C : Type u
inst : Category.{v, u} C
A : Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
X : C
s : CostructuredArrow yoneda A
x : F.obj (op s)
⊢ op s = op (CostructuredArrow.mk (YonedaCollection.fst (counitForward F s x).val))

Tactic:
simp [← CostructuredArrow.eq_mk]

Premises used: CategoryTheory.CostructuredArrow.eq_mk
-- Module: Mathlib.CategoryTheory.Comma.Presheaf.Basic
Goal:
C : Type u
inst : Category.{v, u} C
A : Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
s : CostructuredArrow yoneda A
x : F.obj (op s)
⊢ YonedaCollection.snd (counitForward F s x).val =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (eqToHom ⋯)) :
        (a : (fun (X : Type v) ↦ X) (F.obj (op s))) →
          (fun (X : Type v) ↦ X) (F.obj (op (CostructuredArrow.mk (YonedaCollection.fst (counitForward F s x).val)))))
      x

Tactic:
YonedaCollection.mk_snd _ _

Premises used: CategoryTheory.OverPresheafAux.OverArrows.val, CategoryTheory.CostructuredArrow, CategoryTheory.OverPresheafAux.YonedaCollection.mk_snd, CategoryTheory.OverPresheafAux.YonedaCollection.mk, CategoryTheory.CostructuredArrow.mk
-- Module: Mathlib.CategoryTheory.Comma.Presheaf.Basic
Goal:
C : Type u
inst : Category.{v, u} C
A : Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)
F G : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
η : F ⟶ G
s : (CostructuredArrow yoneda A)ᵒᵖ
x : F.obj s
⊢ YonedaCollection.fst
      (OverArrows.val
        (counitForward G (unop s)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (η.app s) :
              (a : (fun (X : Type v) ↦ X) (F.obj s)) → (fun (X : Type v) ↦ X) (G.obj s))
            x))) =
    YonedaCollection.fst ((counitForward F (unop s) x).map₁ (yonedaCollectionPresheafMap₁ η) ⋯).val

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Comma.Presheaf.Basic
Goal:
C : Type u
inst : Category.{v, u} C
A : Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)
F G : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
η : F ⟶ G
s : (CostructuredArrow yoneda A)ᵒᵖ
x : F.obj s
⊢ Eq (α :=
    (fun (X : Type v) ↦ X)
      (G.obj
        (op
          (CostructuredArrow.mk (Y := unop (op (unop s).left))
            (YonedaCollection.fst
              (OverArrows.val
                (counitForward G (unop s)
                  ((ConcreteCategory.hom (FC := TypeCat.Fun) (η.app s) :
                      (a : (fun (X : Type v) ↦ X) (F.obj s)) → (fun (X : Type v) ↦ X) (G.obj s))
                    x))))))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (G.map (eqToHom ⋯)) :
          (a :
              (fun (X : Type v) ↦ X)
                (G.obj
                  (op
                    (CostructuredArrow.mk
                      (YonedaCollection.fst
                        ((counitForward F (unop s) x).map₁ (yonedaCollectionPresheafMap₁ η) ⋯).val))))) →
            (fun (X : Type v) ↦ X)
              (G.obj
                (op
                  (CostructuredArrow.mk
                    (YonedaCollection.fst
                      (counitForward G (unop s)
                          ((ConcreteCategory.hom (η.app s) :
                              (a : (fun (X : Type v) ↦ X) (F.obj s)) → (fun (X : Type v) ↦ X) (G.obj s))
                            x)).val)))))
        (YonedaCollection.snd ((counitForward F (unop s) x).map₁ (yonedaCollectionPresheafMap₁ η) ⋯).val) :
      (fun (X : Type v) ↦ X)
        (G.obj
          (op
            (CostructuredArrow.mk (Y := unop (op (unop s).left))
              (YonedaCollection.fst
                (OverArrows.val
                  (counitForward G (unop s)
                    ((ConcreteCategory.hom (FC := TypeCat.Fun) (η.app s) :
                        (a : (fun (X : Type v) ↦ X) (F.obj s)) → (fun (X : Type v) ↦ X) (G.obj s))
                      x))))))))
    (YonedaCollection.snd
        (OverArrows.val
          (counitForward G (unop s)
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (η.app s) :
                (a : (fun (X : Type v) ↦ X) (F.obj s)) → (fun (X : Type v) ↦ X) (G.obj s))
              x))) :
      G.obj
        (op
          (CostructuredArrow.mk (Y := unop (op (unop s).left))
            (YonedaCollection.fst
              (OverArrows.val
                (counitForward G (unop s)
                  ((ConcreteCategory.hom (FC := TypeCat.Fun) (η.app s) :
                      (a : (fun (X : Type v) ↦ X) (F.obj s)) → (fun (X : Type v) ↦ X) (G.obj s))
                    x)))))))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Comma.Presheaf.Basic
Goal:
C : Type u
inst : Category.{v, u} C
A : Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
X : C
s t : (CostructuredArrow yoneda A)ᵒᵖ
f : t ⟶ s
x : F.obj t
⊢ Functor.map yoneda f.unop.left ≫ (unop t).hom = (unop s).hom

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Comma.Presheaf.Basic
Goal:
C : Type u
inst : Category.{v, u} C
A : Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
s t : (CostructuredArrow yoneda A)ᵒᵖ
f : t ⟶ s
x : F.obj t
⊢ YonedaCollection.fst
      (OverArrows.val
        (counitForward F (unop s)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
              (a : (fun (X : Type v) ↦ X) (F.obj t)) → (fun (X : Type v) ↦ X) (F.obj s))
            x))) =
    YonedaCollection.fst ((counitForward F (unop t) x).map₂ f.unop.left ⋯).val

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Comma.Presheaf.Basic
Goal:
C : Type u
inst : Category.{v, u} C
A : Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
s t : (CostructuredArrow yoneda A)ᵒᵖ
f : t ⟶ s
x : F.obj t
refine :
  Eq (α :=
    (fun (X : Type v) ↦ X)
      (F.obj
        (op
          (CostructuredArrow.mk (Y := unop (op (unop s).left))
            (YonedaCollection.fst
              (OverArrows.val
                (counitForward F (unop s)
                  ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
                      (a : (fun (X : Type v) ↦ X) (F.obj t)) → (fun (X : Type v) ↦ X) (F.obj s))
                    x))))))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (eqToHom ⋯)) :
          (a :
              (fun (X : Type v) ↦ X)
                (F.obj
                  (op
                    (CostructuredArrow.mk
                      (YonedaCollection.fst ((counitForward F (unop t) x).map₂ f.unop.left ⋯).val))))) →
            (fun (X : Type v) ↦ X)
              (F.obj
                (op
                  (CostructuredArrow.mk
                    (YonedaCollection.fst
                      (counitForward F (unop s)
                          ((ConcreteCategory.hom (F.map f) :
                              (a : (fun (X : Type v) ↦ X) (F.obj t)) → (fun (X : Type v) ↦ X) (F.obj s))
                            x)).val)))))
        (YonedaCollection.snd ((counitForward F (unop t) x).map₂ f.unop.left ⋯).val) :
      (fun (X : Type v) ↦ X)
        (F.obj
          (op
            (CostructuredArrow.mk (Y := unop (op (unop s).left))
              (YonedaCollection.fst
                (OverArrows.val
                  (counitForward F (unop s)
                    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
                        (a : (fun (X : Type v) ↦ X) (F.obj t)) → (fun (X : Type v) ↦ X) (F.obj s))
                      x))))))))
    (YonedaCollection.snd
        (OverArrows.val
          (counitForward F (unop s)
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
                (a : (fun (X : Type v) ↦ X) (F.obj t)) → (fun (X : Type v) ↦ X) (F.obj s))
              x))) :
      F.obj
        (op
          (CostructuredArrow.mk (Y := unop (op (unop s).left))
            (YonedaCollection.fst
              (OverArrows.val
                (counitForward F (unop s)
                  ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
                      (a : (fun (X : Type v) ↦ X) (F.obj t)) → (fun (X : Type v) ↦ X) (F.obj s))
                    x)))))))
⊢ counitForward F (unop s)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
          (a : (fun (X : Type v) ↦ X) (F.obj t)) → (fun (X : Type v) ↦ X) (F.obj s))
        x) =
    (counitForward F (unop t) x).map₂ f.unop.left ⋯

Tactic:
refine OverArrows.ext <| YonedaCollection.ext (by simp) ?_

Premises used: CategoryTheory.OverPresheafAux.OverArrows.ext, CategoryTheory.OverPresheafAux.YonedaCollection.ext
-- Module: Mathlib.CategoryTheory.Comma.Presheaf.Basic
Goal:
C : Type u
inst : Category.{v, u} C
A : Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
s t : (CostructuredArrow yoneda A)ᵒᵖ
f : t ⟶ s
x : F.obj t
⊢ s = op (CostructuredArrow.mk (Functor.map yoneda f.unop.left ≫ (unop t).hom))

Tactic:
simp [← CostructuredArrow.eq_mk]

Premises used: CategoryTheory.CostructuredArrow.eq_mk
-- Module: Mathlib.CategoryTheory.Comma.Presheaf.Basic
Goal:
C : Type u
inst : Category.{v, u} C
A : Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
s t : (CostructuredArrow yoneda A)ᵒᵖ
f : t ⟶ s
x : F.obj t
a : (CostructuredArrow.mkPrecomp (unop t).hom f.unop.left).op.unop = Quiver.Hom.unop (f ≫ eqToHom ⋯)
⊢ (CostructuredArrow.mkPrecomp (unop t).hom f.unop.left).op = f ≫ eqToHom ⋯

Tactic:
apply Quiver.Hom.unop_inj

Premises used: Quiver.Hom.unop_inj
-- Module: Mathlib.CategoryTheory.Comma.Presheaf.Basic
Goal:
C : Type u
inst : Category.{v, u} C
A : Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
s t : (CostructuredArrow yoneda A)ᵒᵖ
f : t ⟶ s
x : F.obj t
⊢ (CostructuredArrow.mkPrecomp (unop t).hom f.unop.left).op.unop = Quiver.Hom.unop (f ≫ eqToHom ⋯)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Comma.Presheaf.Basic
Goal:
C : Type u
inst : Category.{v, u} C
A : Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
s t : (CostructuredArrow yoneda A)ᵒᵖ
f : t ⟶ s
x : F.obj t
⊢ (CostructuredArrow.mkPrecomp (unop t).hom f.unop.left).op = f ≫ eqToHom ⋯

Tactic:
have : (CostructuredArrow.mkPrecomp t.unop.hom f.unop.left).op =
      f ≫ eqToHom (by simp [← CostructuredArrow.eq_mk]) := by
    apply Quiver.Hom.unop_inj
    simp
-- Module: Mathlib.CategoryTheory.Comma.Presheaf.Basic
Goal:
C : Type u
inst : Category.{v, u} C
A : Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
s t : (CostructuredArrow yoneda A)ᵒᵖ
f : t ⟶ s
x : F.obj t
this : (CostructuredArrow.mkPrecomp (unop t).hom f.unop.left).op = f ≫ eqToHom ⋯
simp : t = op (CostructuredArrow.mk (unop t).hom)
⊢ t = op (CostructuredArrow.mk (YonedaCollection.fst (counitForward F (unop t) x).val))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Comma.Presheaf.Basic
Goal:
C : Type u
inst : Category.{v, u} C
A : Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
s t : (CostructuredArrow yoneda A)ᵒᵖ
f : t ⟶ s
x : F.obj t
this : (CostructuredArrow.mkPrecomp (unop t).hom f.unop.left).op = f ≫ eqToHom ⋯
⊢ t = op (CostructuredArrow.mk (unop t).hom)

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Comma.Presheaf.Basic
Goal:
C : Type u
inst : Category.{v, u} C
A : Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
s t : (CostructuredArrow yoneda A)ᵒᵖ
f : t ⟶ s
x : F.obj t
this : (CostructuredArrow.mkPrecomp (unop t).hom f.unop.left).op = f ≫ eqToHom ⋯
⊢ YonedaCollection.fst (counitForward F (unop t) x).val = Comma.hom t.1

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Comma.Presheaf.Basic
Goal:
C : Type u
inst : Category.{v, u} C
A : Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
s t : (CostructuredArrow yoneda A)ᵒᵖ
f : t ⟶ s
x : F.obj t
this : (CostructuredArrow.mkPrecomp (unop t).hom f.unop.left).op = f ≫ eqToHom ⋯
⊢ Eq (α :=
    (fun (X : Type v) ↦ X)
      (F.obj
        (op
          (CostructuredArrow.mk
            (Functor.map yoneda f.unop.left ≫ YonedaCollection.fst (counitForward F (unop t) x).val)))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (F.map
              (CostructuredArrow.mkPrecomp (YonedaCollection.fst (counitForward F (unop t) x).val) f.unop.left).op) :
          (a :
              (fun (X : Type v) ↦ X)
                (F.obj (op (CostructuredArrow.mk (YonedaCollection.fst (counitForward F (unop t) x).val))))) →
            (fun (X : Type v) ↦ X)
              (F.obj
                (op
                  (CostructuredArrow.mk
                    (yoneda.map f.unop.left ≫ YonedaCollection.fst (counitForward F (unop t) x).val)))))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (eqToHom ⋯)) :
              (a : (fun (X : Type v) ↦ X) (F.obj t)) →
                (fun (X : Type v) ↦ X)
                  (F.obj (op (CostructuredArrow.mk (YonedaCollection.fst (counitForward F (unop t) x).val)))))
            x :
          (fun (X : Type v) ↦ X)
            (F.obj (op (CostructuredArrow.mk (YonedaCollection.fst (counitForward F (unop t) x).val))))) :
      (fun (X : Type v) ↦ X)
        (F.obj
          (op
            (CostructuredArrow.mk
              (Functor.map yoneda f.unop.left ≫ YonedaCollection.fst (counitForward F (unop t) x).val)))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (eqToHom ⋯)) :
          (a : (fun (X : Type v) ↦ X) (F.obj (op (CostructuredArrow.mk (yoneda.map f.unop.left ≫ t.1.hom))))) →
            (fun (X : Type v) ↦ X)
              (F.obj
                (op
                  (CostructuredArrow.mk
                    (yoneda.map f.unop.left ≫ YonedaCollection.fst (counitForward F (unop t) x).val)))))
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
                (F.map (Quiver.Hom.op (CostructuredArrow.mkPrecomp (Comma.hom t.1) f.unop.left))) :
              (a : (fun (X : Type v) ↦ X) (F.obj (op (CostructuredArrow.mk t.1.hom)))) →
                (fun (X : Type v) ↦ X) (F.obj (op (CostructuredArrow.mk (yoneda.map f.unop.left ≫ t.1.hom)))))
            x :
          (fun (X : Type v) ↦ X) (F.obj (op (CostructuredArrow.mk (Functor.map yoneda f.unop.left ≫ Comma.hom t.1))))) :
      (fun (X : Type v) ↦ X)
        (F.obj
          (op
            (CostructuredArrow.mk
              (Functor.map yoneda f.unop.left ≫ YonedaCollection.fst (counitForward F (unop t) x).val)))))

Tactic:
have : F.map (CostructuredArrow.mkPrecomp
      (YonedaCollection.fst (counitForward F (unop t) x).val) f.unop.left).op
      (F.map (eqToHom (by simp; rfl)) x) = _ :=
    map_mkPrecomp_eqToHom (h := by simp)
-- Module: Mathlib.CategoryTheory.Comma.Presheaf.Basic
Goal:
C : Type u
inst : Category.{v, u} C
A : Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)
F_1 : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
X : C
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
s : CostructuredArrow yoneda A
p : OverArrows (yonedaCollectionPresheafToA F) s.hom
⊢ op (CostructuredArrow.mk (YonedaCollection.fst p.val)) = op s

Tactic:
simp [← CostructuredArrow.eq_mk]

Premises used: CategoryTheory.CostructuredArrow.eq_mk
-- Module: Mathlib.CategoryTheory.Comma.Presheaf.Basic
Goal:
C : Type u
inst : Category.{v, u} C
A : Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
s : CostructuredArrow yoneda A
p : OverArrows (yonedaCollectionPresheafToA F) s.hom
⊢ YonedaCollection.fst ((counitForward F s ∘ counitBackward F s) p).val = YonedaCollection.fst (id p).val

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Comma.Presheaf.Basic
Goal:
C : Type u
inst : Category.{v, u} C
A : Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
s : CostructuredArrow yoneda A
p : OverArrows (yonedaCollectionPresheafToA F) s.hom
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (eqToHom ⋯)) :
        (a : (fun (X : Type v) ↦ X) (F.obj (op (CostructuredArrow.mk (YonedaCollection.fst (id p).val))))) →
          (fun (X : Type v) ↦ X)
            (F.obj (op (CostructuredArrow.mk (YonedaCollection.fst ((counitForward F s ∘ counitBackward F s) p).val)))))
      (YonedaCollection.snd (id p).val) =
    YonedaCollection.snd ((counitForward F s ∘ counitBackward F s) p).val

Tactic:
simp [counitBackward]

Premises used: CategoryTheory.OverPresheafAux.counitBackward
-- Module: Mathlib.CategoryTheory.Comma.Presheaf.Basic
Goal:
C : Type u
inst : Category.{v, u} C
A : Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
s : CostructuredArrow yoneda A
x : F.obj (op s)
⊢ (counitBackward F s ∘ counitForward F s) x = id x

Tactic:
simp [counitBackward]

Premises used: CategoryTheory.OverPresheafAux.counitBackward
-- Module: Mathlib.CategoryTheory.Comma.Presheaf.Basic
Goal:
C : Type u
inst : Category.{v, u} C
A : Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)
T : Over A
X : CostructuredArrow yoneda A
f : Functor.obj (toOver yoneda A) X ⟶ T
⊢ (overEquivPresheafCostructuredArrow A).inverse.map
      ((ConcreteCategory.hom (FC := TypeCat.Fun) ((toOverCompYoneda A T).hom.app (op X)) :
          (a : (toOver yoneda A).obj X ⟶ T) → yoneda.obj X ⟶ (overEquivPresheafCostructuredArrow A).functor.obj T)
        f) =
    (toOverCompOverEquivPresheafCostructuredArrow A).isoCompInverse.inv.app X ≫
      f ≫ (overEquivPresheafCostructuredArrow A).unit.app T

Tactic:
simp [CostructuredArrow.toOverCompYoneda]

Premises used: CategoryTheory.CostructuredArrow.toOverCompYoneda
-- Module: Mathlib.CategoryTheory.Comma.Presheaf.Basic
Goal:
C : Type u
inst : Category.{v, u} C
A : Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)
T : Over A
X : CostructuredArrow yoneda A
f : Functor.obj yoneda X ⟶ (overEquivPresheafCostructuredArrow A).functor.obj T
⊢ (overEquivPresheafCostructuredArrow A).functor.map
      ((ConcreteCategory.hom (FC := TypeCat.Fun) ((toOverCompYoneda A T).inv.app (op X)) :
          (a : yoneda.obj X ⟶ (overEquivPresheafCostructuredArrow A).functor.obj T) → (toOver yoneda A).obj X ⟶ T)
        f) =
    (toOverCompOverEquivPresheafCostructuredArrow A).hom.app X ≫ f

Tactic:
simp [CostructuredArrow.toOverCompYoneda]

Premises used: CategoryTheory.CostructuredArrow.toOverCompYoneda
-- Module: Mathlib.CategoryTheory.Comma.Presheaf.Basic
Goal:
C : Type u
inst : Category.{v, u} C
A : Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)
T : Over A
X : CostructuredArrow yoneda A
f : Functor.obj (toOver yoneda A) X ⟶ T
⊢ (overEquivPresheafCostructuredArrow A).inverse.map
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app ((toOverCompCoyoneda A).hom.app (op X)) T) :
          (a : (toOver yoneda A).obj X ⟶ T) → yoneda.obj X ⟶ (overEquivPresheafCostructuredArrow A).functor.obj T)
        f) =
    (toOverCompOverEquivPresheafCostructuredArrow A).isoCompInverse.inv.app X ≫
      f ≫ (overEquivPresheafCostructuredArrow A).unit.app T

Tactic:
simp [CostructuredArrow.toOverCompCoyoneda]

Premises used: CategoryTheory.CostructuredArrow.toOverCompCoyoneda
-- Module: Mathlib.CategoryTheory.Comma.Presheaf.Basic
Goal:
C : Type u
inst : Category.{v, u} C
A : Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)
T : Over A
X : CostructuredArrow yoneda A
f : Functor.obj yoneda X ⟶ (overEquivPresheafCostructuredArrow A).functor.obj T
⊢ (overEquivPresheafCostructuredArrow A).functor.map
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app ((toOverCompCoyoneda A).inv.app (op X)) T) :
          (a : yoneda.obj X ⟶ (overEquivPresheafCostructuredArrow A).functor.obj T) → (toOver yoneda A).obj X ⟶ T)
        f) =
    (toOverCompOverEquivPresheafCostructuredArrow A).hom.app X ≫ f

Tactic:
simp [CostructuredArrow.toOverCompCoyoneda]

Premises used: CategoryTheory.CostructuredArrow.toOverCompCoyoneda
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
S : D
T : Functor.{v₁, v₂, u₁, u₂} C D
X Y : StructuredArrow S T
f : X ⟶ Y
⊢ X.hom ≫ T.map (Hom.right f) = Y.hom

Tactic:
simpa using (CommaMorphism.w f).symm

Premises used: CategoryTheory.CommaMorphism.w, Eq.symm
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
S : D
T : Functor.{v₁, v₂, u₁, u₂} C D
X Y : StructuredArrow S T
f : X ⟶ Y
⊢ X.hom ≫ T.map (right f) = Y.hom

Tactic:
StructuredArrow.w f

Premises used: CategoryTheory.StructuredArrow.w
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
S : D
T : Functor.{v₁, v₂, u₁, u₂} C D
X Y : StructuredArrow S T
f g : X ⟶ Y
h : Hom.right f = Hom.right g
⊢ f = g

Tactic:
CommaMorphism.ext (Subsingleton.elim _ _) h

Premises used: CategoryTheory.StructuredArrow.Hom, CategoryTheory.CommaMorphism.ext, Subsingleton.elim
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
S : D
T : Functor.{v₁, v₂, u₁, u₂} C D
X Y : StructuredArrow S T
f g : X ⟶ Y
h : f = g
rw rw₁ : Hom.right g = Hom.right g
⊢ Hom.right f = Hom.right g

Tactic:
rw [h]
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
S : D
Y : C
T : Functor.{v₁, v₂, u₁, u₂} C D
f : S ⟶ T.obj Y
⊢ (mk f).left = { as := PUnit.unit }

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
S : D
Y : C
T : Functor.{v₁, v₂, u₁, u₂} C D
f : S ⟶ T.obj Y
⊢ (mk f).right = Y

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
S : D
Y : C
T : Functor.{v₁, v₂, u₁, u₂} C D
f : S ⟶ T.obj Y
⊢ (mk f).hom = f

Tactic:
rfl

Premises used: rfl