awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
p : A.obj (op X)
p' : F.obj (op (CostructuredArrow.mk (Y := X) ((Equiv.symm yonedaEquiv : (a : A.obj (op X)) → yoneda.obj X ⟶ A) p)))
q : A.obj (op X)
q' : F.obj (op (CostructuredArrow.mk (Y := X) ((Equiv.symm yonedaEquiv : (a : A.obj (op X)) → yoneda.obj X ⟶ A) q)))
h :
  fst (F := F)
      (Sigma.mk (β := fun (s : A.obj (op X)) ↦
        F.obj (op (CostructuredArrow.mk (Y := X) ((Equiv.symm yonedaEquiv : (a : A.obj (op X)) → yoneda.obj X ⟶ A) s))))
        p p') =
    fst (F := F)
      (Sigma.mk (β := fun (s : A.obj (op X)) ↦
        F.obj (op (CostructuredArrow.mk (Y := X) ((Equiv.symm yonedaEquiv : (a : A.obj (op X)) → yoneda.obj X ⟶ A) s))))
        q q')
h' :
  Eq (α :=
    (fun (X : Type v) ↦ X)
      (F.obj
        (op
          (CostructuredArrow.mk
            (fst (F := F)
              (Sigma.mk (β := fun (s : A.obj (op X)) ↦
                F.obj
                  (op
                    (CostructuredArrow.mk (Y := X)
                      ((Equiv.symm yonedaEquiv : (a : A.obj (op X)) → yoneda.obj X ⟶ A) s))))
                p p'))))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (eqToHom ⋯)) :
          (a : (fun (X : Type v) ↦ X) (F.obj (op (CostructuredArrow.mk (fst ⟨q, q'⟩))))) →
            (fun (X : Type v) ↦ X) (F.obj (op (CostructuredArrow.mk (fst ⟨p, p'⟩)))))
        (snd
          (Sigma.mk (β := fun (s : A.obj (op X)) ↦
            F.obj
              (op (CostructuredArrow.mk (Y := X) ((Equiv.symm yonedaEquiv : (a : A.obj (op X)) → yoneda.obj X ⟶ A) s))))
            q q')) :
      (fun (X : Type v) ↦ X)
        (F.obj
          (op
            (CostructuredArrow.mk
              (fst (F := F)
                (Sigma.mk (β := fun (s : A.obj (op X)) ↦
                  F.obj
                    (op
                      (CostructuredArrow.mk (Y := X)
                        ((Equiv.symm yonedaEquiv : (a : A.obj (op X)) → yoneda.obj X ⟶ A) s))))
                  p p'))))))
    (snd
        (Sigma.mk (β := fun (s : A.obj (op X)) ↦
          F.obj
            (op (CostructuredArrow.mk (Y := X) ((Equiv.symm yonedaEquiv : (a : A.obj (op X)) → yoneda.obj X ⟶ A) s))))
          p p') :
      F.obj
        (op
          (CostructuredArrow.mk
            (fst (F := F)
              (Sigma.mk (β := fun (s : A.obj (op X)) ↦
                F.obj
                  (op
                    (CostructuredArrow.mk (Y := X)
                      ((Equiv.symm yonedaEquiv : (a : A.obj (op X)) → yoneda.obj X ⟶ A) s))))
                p p')))))
⊢ p = q

Tactic:
yonedaEquiv.symm.injective h

Premises used: Equiv.injective, Equiv.symm, CategoryTheory.yonedaEquiv
-- 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
p : A.obj (op X)
p' q' : F.obj (op (CostructuredArrow.mk (Y := X) ((Equiv.symm yonedaEquiv : (a : A.obj (op X)) → yoneda.obj X ⟶ A) p)))
h :
  fst (F := F)
      (Sigma.mk (β := fun (s : A.obj (op X)) ↦
        F.obj (op (CostructuredArrow.mk (Y := X) ((Equiv.symm yonedaEquiv : (a : A.obj (op X)) → yoneda.obj X ⟶ A) s))))
        p p') =
    fst (F := F)
      (Sigma.mk (β := fun (s : A.obj (op X)) ↦
        F.obj (op (CostructuredArrow.mk (Y := X) ((Equiv.symm yonedaEquiv : (a : A.obj (op X)) → yoneda.obj X ⟶ A) s))))
        p q')
h' :
  Eq (α :=
    (fun (X : Type v) ↦ X)
      (F.obj
        (op
          (CostructuredArrow.mk
            (fst (F := F)
              (Sigma.mk (β := fun (s : A.obj (op X)) ↦
                F.obj
                  (op
                    (CostructuredArrow.mk (Y := X)
                      ((Equiv.symm yonedaEquiv : (a : A.obj (op X)) → yoneda.obj X ⟶ A) s))))
                p p'))))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (eqToHom ⋯)) :
          (a : (fun (X : Type v) ↦ X) (F.obj (op (CostructuredArrow.mk (fst ⟨p, q'⟩))))) →
            (fun (X : Type v) ↦ X) (F.obj (op (CostructuredArrow.mk (fst ⟨p, p'⟩)))))
        (snd
          (Sigma.mk (β := fun (s : A.obj (op X)) ↦
            F.obj
              (op (CostructuredArrow.mk (Y := X) ((Equiv.symm yonedaEquiv : (a : A.obj (op X)) → yoneda.obj X ⟶ A) s))))
            p q')) :
      (fun (X : Type v) ↦ X)
        (F.obj
          (op
            (CostructuredArrow.mk
              (fst (F := F)
                (Sigma.mk (β := fun (s : A.obj (op X)) ↦
                  F.obj
                    (op
                      (CostructuredArrow.mk (Y := X)
                        ((Equiv.symm yonedaEquiv : (a : A.obj (op X)) → yoneda.obj X ⟶ A) s))))
                  p p'))))))
    (snd
        (Sigma.mk (β := fun (s : A.obj (op X)) ↦
          F.obj
            (op (CostructuredArrow.mk (Y := X) ((Equiv.symm yonedaEquiv : (a : A.obj (op X)) → yoneda.obj X ⟶ A) s))))
          p p') :
      F.obj
        (op
          (CostructuredArrow.mk
            (fst (F := F)
              (Sigma.mk (β := fun (s : A.obj (op X)) ↦
                F.obj
                  (op
                    (CostructuredArrow.mk (Y := X)
                      ((Equiv.symm yonedaEquiv : (a : A.obj (op X)) → yoneda.obj X ⟶ A) s))))
                p p')))))
⊢ Eq (α := YonedaCollection F X)
    (Sigma.mk (β := fun (s : A.obj (op X)) ↦
      F.obj (op (CostructuredArrow.mk (Y := X) ((Equiv.symm yonedaEquiv : (a : A.obj (op X)) → yoneda.obj X ⟶ A) s)))) p
      p')
    (Sigma.mk (β := fun (s : A.obj (op X)) ↦
      F.obj (op (CostructuredArrow.mk (Y := X) ((Equiv.symm yonedaEquiv : (a : A.obj (op X)) → yoneda.obj X ⟶ A) s)))) p
      q')

Tactic:
exact Sigma.ext rfl (by simpa [snd] using h'.symm)

Premises used: Sigma.ext, 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
X : C
G : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
η : F ⟶ G
p : YonedaCollection F X
⊢ (map₁ η p).fst = p.fst

Tactic:
simp [map₁]

Premises used: CategoryTheory.OverPresheafAux.YonedaCollection.map₁
-- 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
G : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
η : F ⟶ G
p : YonedaCollection F X
⊢ (map₁ η p).yonedaEquivFst = p.yonedaEquivFst

Tactic:
simp only [YonedaCollection.yonedaEquivFst_eq, map₁_fst]

Premises used: CategoryTheory.OverPresheafAux.YonedaCollection.yonedaEquivFst_eq, CategoryTheory.OverPresheafAux.YonedaCollection.map₁_fst
-- 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
G : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
η : F ⟶ G
p : YonedaCollection F X
rw rw₁ : op (CostructuredArrow.mk p.fst) = op (CostructuredArrow.mk p.fst)
⊢ op (CostructuredArrow.mk p.fst) = op (CostructuredArrow.mk (map₁ η p).fst)

Tactic:
rw [YonedaCollection.map₁_fst]

Premises used: CategoryTheory.OverPresheafAux.YonedaCollection.map₁_fst
-- 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
G : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
η : F ⟶ G
p : YonedaCollection F X
⊢ (map₁ η p).snd =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (G.map (eqToHom ⋯)) :
        (a : (fun (X : Type v) ↦ X) (G.obj (op (CostructuredArrow.mk p.fst)))) →
          (fun (X : Type v) ↦ X) (G.obj (op (CostructuredArrow.mk (map₁ η p).fst))))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (η.app (op (CostructuredArrow.mk p.fst))) :
            (a : (fun (X : Type v) ↦ X) (F.obj (op (CostructuredArrow.mk p.fst)))) →
              (fun (X : Type v) ↦ X) (G.obj (op (CostructuredArrow.mk p.fst))))
          p.snd :
        (fun (X : Type v) ↦ X) (G.obj (op (CostructuredArrow.mk p.fst))))

Tactic:
simp [map₁]

Premises used: CategoryTheory.OverPresheafAux.YonedaCollection.map₁
-- 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 Y : C
f : X ⟶ Y
p : YonedaCollection F Y
⊢ (map₂ F f p).fst = Functor.map yoneda f ≫ p.fst

Tactic:
simp [map₂]

Premises used: CategoryTheory.OverPresheafAux.YonedaCollection.map₂
-- 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 Y : C
f : X ⟶ Y
p : YonedaCollection F Y
⊢ (map₂ F f p).yonedaEquivFst =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (A.map f.op) :
        (a : (fun (X : Type v) ↦ X) (A.obj (op Y))) → (fun (X : Type v) ↦ X) (A.obj (op X)))
      p.yonedaEquivFst

Tactic:
simp only [YonedaCollection.yonedaEquivFst_eq, map₂_fst, yonedaEquiv_naturality]

Premises used: CategoryTheory.OverPresheafAux.YonedaCollection.yonedaEquivFst_eq, CategoryTheory.yonedaEquiv_naturality, CategoryTheory.OverPresheafAux.YonedaCollection.map₂_fst
-- 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 Y : C
f : X ⟶ Y
p : YonedaCollection F Y
rw rw₁ :
  op (CostructuredArrow.mk (Functor.map yoneda f ≫ p.fst)) = op (CostructuredArrow.mk (Functor.map yoneda f ≫ p.fst))
⊢ op (CostructuredArrow.mk (Functor.map yoneda f ≫ p.fst)) = op (CostructuredArrow.mk (map₂ F f p).fst)

Tactic:
rw [YonedaCollection.map₂_fst f]

Premises used: CategoryTheory.OverPresheafAux.YonedaCollection.map₂_fst
-- 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 Y : C
f : X ⟶ Y
p : YonedaCollection F Y
⊢ (map₂ F f p).snd =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map ((CostructuredArrow.mkPrecomp p.fst f).op ≫ eqToHom ⋯)) :
        (a : (fun (X : Type v) ↦ X) (F.obj (op (CostructuredArrow.mk p.fst)))) →
          (fun (X : Type v) ↦ X) (F.obj (op (CostructuredArrow.mk (map₂ F f p).fst))))
      p.snd

Tactic:
simp [map₂]

Premises used: CategoryTheory.OverPresheafAux.YonedaCollection.map₂
-- 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
G H : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
η : F ⟶ G
μ : G ⟶ H
h :
  ∀ (x : YonedaCollection F X) (x_1 : Cᵒᵖ) (x_2 : Functor.obj (Functor.obj yoneda X) x_1),
    (ConcreteCategory.hom (FC := TypeCat.Fun) ((map₁ (η ≫ μ) x).fst.app x_1)).toFun x_2 =
      (ConcreteCategory.hom (FC := TypeCat.Fun) (((map₁ μ ∘ map₁ η) x).fst.app x_1)).toFun x_2
h₁ :
  ∀ (x : YonedaCollection F X),
    (ConcreteCategory.hom (FC := TypeCat.Fun) (H.map (eqToHom ⋯)) :
          (a : (fun (X : Type v) ↦ X) (H.obj (op (CostructuredArrow.mk ((map₁ μ ∘ map₁ η) x).fst)))) →
            (fun (X : Type v) ↦ X) (H.obj (op (CostructuredArrow.mk (map₁ (η ≫ μ) x).fst))))
        ((map₁ μ ∘ map₁ η) x).snd =
      (map₁ (η ≫ μ) x).snd
⊢ Eq (α := YonedaCollection F X → YonedaCollection H X) (map₁ (η ≫ μ)) (map₁ μ ∘ map₁ η)

Tactic:
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
X : C
G H : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
η : F ⟶ G
μ : G ⟶ H
x : YonedaCollection F X
x_1 : Cᵒᵖ
x_2 : Functor.obj (Functor.obj yoneda X) x_1
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) ((map₁ (η ≫ μ) x).fst.app x_1)).toFun x_2 =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (((map₁ μ ∘ map₁ η) x).fst.app x_1)).toFun x_2

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
G H : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
η : F ⟶ G
μ : G ⟶ H
x : YonedaCollection F X
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (H.map (eqToHom ⋯)) :
        (a : (fun (X : Type v) ↦ X) (H.obj (op (CostructuredArrow.mk ((map₁ μ ∘ map₁ η) x).fst)))) →
          (fun (X : Type v) ↦ X) (H.obj (op (CostructuredArrow.mk (map₁ (η ≫ μ) x).fst))))
      ((map₁ μ ∘ map₁ η) x).snd =
    (map₁ (η ≫ μ) x).snd

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
h :
  ∀ (x : YonedaCollection F X) (x_1 : Cᵒᵖ) (x_2 : Functor.obj (Functor.obj yoneda X) x_1),
    (ConcreteCategory.hom (FC := TypeCat.Fun) ((map₂ F (𝟙 X) x).fst.app x_1)).toFun x_2 =
      (ConcreteCategory.hom (FC := TypeCat.Fun) ((id x).fst.app x_1)).toFun x_2
h₁ :
  ∀ (x : YonedaCollection F X),
    (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (eqToHom ⋯)) :
          (a : (fun (X : Type v) ↦ X) (F.obj (op (CostructuredArrow.mk (id x).fst)))) →
            (fun (X : Type v) ↦ X) (F.obj (op (CostructuredArrow.mk (map₂ F (𝟙 X) x).fst))))
        (id x).snd =
      (map₂ F (𝟙 X) x).snd
⊢ map₂ F (𝟙 X) = id

Tactic:
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
X : C
x : YonedaCollection F X
x_1 : Cᵒᵖ
x_2 : Functor.obj (Functor.obj yoneda X) x_1
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) ((map₂ F (𝟙 X) x).fst.app x_1)).toFun x_2 =
    (ConcreteCategory.hom (FC := TypeCat.Fun) ((id x).fst.app x_1)).toFun x_2

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
x : YonedaCollection F X
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (eqToHom ⋯)) :
        (a : (fun (X : Type v) ↦ X) (F.obj (op (CostructuredArrow.mk (id x).fst)))) →
          (fun (X : Type v) ↦ X) (F.obj (op (CostructuredArrow.mk (map₂ F (𝟙 X) x).fst))))
      (id x).snd =
    (map₂ F (𝟙 X) x).snd

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 Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
h :
  ∀ (x : YonedaCollection F Z) (x_1 : Cᵒᵖ) (x_2 : Functor.obj (Functor.obj yoneda X) x_1),
    (ConcreteCategory.hom (FC := TypeCat.Fun) ((map₂ F (f ≫ g) x).fst.app x_1)).toFun x_2 =
      (ConcreteCategory.hom (FC := TypeCat.Fun) (((map₂ F f ∘ map₂ F g) x).fst.app x_1)).toFun x_2
h₁ :
  ∀ (x : YonedaCollection F Z),
    (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (eqToHom ⋯)) :
          (a : (fun (X : Type v) ↦ X) (F.obj (op (CostructuredArrow.mk ((map₂ F f ∘ map₂ F g) x).fst)))) →
            (fun (X : Type v) ↦ X) (F.obj (op (CostructuredArrow.mk (map₂ F (f ≫ g) x).fst))))
        ((map₂ F f ∘ map₂ F g) x).snd =
      (map₂ F (f ≫ g) x).snd
⊢ map₂ F (f ≫ g) = map₂ F f ∘ map₂ F g

Tactic:
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
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
x : YonedaCollection F Z
x_1 : Cᵒᵖ
x_2 : Functor.obj (Functor.obj yoneda X) x_1
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) ((map₂ F (f ≫ g) x).fst.app x_1)).toFun x_2 =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (((map₂ F f ∘ map₂ F g) x).fst.app x_1)).toFun x_2

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 Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
x : YonedaCollection F Z
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (eqToHom ⋯)) :
        (a : (fun (X : Type v) ↦ X) (F.obj (op (CostructuredArrow.mk ((map₂ F f ∘ map₂ F g) x).fst)))) →
          (fun (X : Type v) ↦ X) (F.obj (op (CostructuredArrow.mk (map₂ F (f ≫ g) x).fst))))
      ((map₂ F f ∘ map₂ F g) x).snd =
    (map₂ F (f ≫ g) x).snd

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
G : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
η : F ⟶ G
Y : C
f : X ⟶ Y
p : YonedaCollection F Y
h :
  ∀ (x : Cᵒᵖ) (x_1 : Functor.obj (Functor.obj yoneda X) x),
    (ConcreteCategory.hom (FC := TypeCat.Fun) ((map₂ G f (map₁ η p)).fst.app x)).toFun x_1 =
      (ConcreteCategory.hom (FC := TypeCat.Fun) ((map₁ η (map₂ F f p)).fst.app x)).toFun x_1
h' :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (G.map (eqToHom ⋯)) :
        (a : (fun (X : Type v) ↦ X) (G.obj (op (CostructuredArrow.mk (map₁ η (map₂ F f p)).fst)))) →
          (fun (X : Type v) ↦ X) (G.obj (op (CostructuredArrow.mk (map₂ G f (map₁ η p)).fst))))
      (map₁ η (map₂ F f p)).snd =
    (map₂ G f (map₁ η p)).snd
⊢ map₂ G f (map₁ η p) = map₁ η (map₂ F f p)

Tactic:
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
X : C
G : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
η : F ⟶ G
Y : C
f : X ⟶ Y
p : YonedaCollection F Y
x : Cᵒᵖ
x_1 : Functor.obj (Functor.obj yoneda X) x
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) ((map₂ G f (map₁ η p)).fst.app x)).toFun x_1 =
    (ConcreteCategory.hom (FC := TypeCat.Fun) ((map₁ η (map₂ F f p)).fst.app x)).toFun x_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
X : C
G : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
η : F ⟶ G
Y : C
f : X ⟶ Y
p : YonedaCollection F Y
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (G.map (eqToHom ⋯)) :
        (a : (fun (X : Type v) ↦ X) (G.obj (op (CostructuredArrow.mk (map₁ η (map₂ F f p)).fst)))) →
          (fun (X : Type v) ↦ X) (G.obj (op (CostructuredArrow.mk (map₂ G f (map₁ η p)).fst))))
      (map₁ η (map₂ F f p)).snd =
    (map₂ G f (map₁ η p)).snd

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
X Y : Cᵒᵖ
f : X ⟶ Y
h :
  ∀ (x : (yonedaCollectionPresheaf A F).obj X),
    (ConcreteCategory.hom (FC := TypeCat.Fun) ((yonedaCollectionPresheaf A F).map f ≫ ↾YonedaCollection.map₁ η)).toFun
        x =
      (ConcreteCategory.hom (FC := TypeCat.Fun) (↾YonedaCollection.map₁ η ≫ (yonedaCollectionPresheaf A G).map f)).toFun
        x
⊢ (yonedaCollectionPresheaf A F).map f ≫ ↾YonedaCollection.map₁ η =
    ↾YonedaCollection.map₁ η ≫ (yonedaCollectionPresheaf A G).map f

Tactic:
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 G : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
η : F ⟶ G
X Y : Cᵒᵖ
f : X ⟶ Y
x : (yonedaCollectionPresheaf A F).obj X
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) ((yonedaCollectionPresheaf A F).map f ≫ ↾YonedaCollection.map₁ η)).toFun x =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (↾YonedaCollection.map₁ η ≫ (yonedaCollectionPresheaf A G).map f)).toFun x

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Comma.Presheaf.Basic
Goal:
C : Type u
inst : Category.{v, u} C
A F G : Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)
η : F ⟶ A
μ : G ⟶ A
ε : F ⟶ G
hε : ε ≫ μ = η
X : C
p : YonedaCollection (restrictedYonedaObj η) X
⊢ unitForward μ X (YonedaCollection.map₁ (restrictedYonedaObjMap₁ ε hε) p) =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (ε.app (op X)) :
        (a : (fun (X : Type v) ↦ X) (F.obj (op X))) → (fun (X : Type v) ↦ X) (G.obj (op X)))
      (unitForward η X p)

Tactic:
simp [unitForward]

Premises used: CategoryTheory.OverPresheafAux.unitForward
-- 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 Y : C
f : X ⟶ Y
p : YonedaCollection (restrictedYonedaObj η) Y
⊢ unitForward η X (YonedaCollection.map₂ (restrictedYonedaObj η) f p) =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f.op) :
        (a : (fun (X : Type v) ↦ X) (F.obj (op Y))) → (fun (X : Type v) ↦ X) (F.obj (op X)))
      (unitForward η Y p)

Tactic:
simp [unitForward]

Premises used: CategoryTheory.OverPresheafAux.unitForward
-- 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 η) (unop X)
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (η.app X) :
        (a : (fun (X : Type v) ↦ X) (F.obj X)) → (fun (X : Type v) ↦ X) (A.obj X))
      (unitForward η (unop X) p) =
    p.yonedaEquivFst

Tactic:
simpa [unitForward] using p.snd.app_val

Premises used: CategoryTheory.OverPresheafAux.unitForward, CategoryTheory.OverPresheafAux.OverArrows.app_val, CategoryTheory.OverPresheafAux.YonedaCollection.snd
-- 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
x : F.obj (op X)
⊢ (unitForward η X ∘ unitBackward η X) x = id x

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 F : Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)
η : F ⟶ A
X : C
⊢ unitBackward η X ∘ unitForward η X = id

Tactic:
funext fun p => YonedaCollection.ext ?_ (OverArrows.ext ?_)

Premises used: CategoryTheory.OverPresheafAux.OverArrows.ext, funext, CategoryTheory.OverPresheafAux.YonedaCollection.ext
-- 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
refine_1 : ∀ (p : YonedaCollection (restrictedYonedaObj η) X), ((unitBackward η X ∘ unitForward η X) p).fst = (id p).fst
refine_2 :
  ∀ (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
⊢ unitBackward η X ∘ unitForward η X = id

Tactic:
refine funext fun p => YonedaCollection.ext ?_ (OverArrows.ext ?_)

Premises used: funext, CategoryTheory.OverPresheafAux.YonedaCollection.ext
-- 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
⊢ ((unitBackward η X ∘ unitForward η X) p).fst = (id p).fst

Tactic:
simpa [unitForward, unitBackward] using congrArg yonedaEquiv.symm p.snd.app_val

Premises used: CategoryTheory.OverPresheafAux.unitForward, congrArg, CategoryTheory.OverPresheafAux.unitBackward, CategoryTheory.OverPresheafAux.OverArrows.app_val, Equiv.symm, CategoryTheory.yonedaEquiv, CategoryTheory.OverPresheafAux.YonedaCollection.snd, DFunLike.coe