awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Sites.Subcanonical
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
inst_1 : J.Subcanonical
X Y : C
F : Sheaf J (Type (max v v'))
f : (uliftYoneda.{v', v, u} J).obj X ⟶ F
g : Y ⟶ X
rw :
  Eq (α := (fun (X : Type (max v v')) ↦ X) (F.obj (P := Presheaf.IsSheaf J).obj (op Y)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (((uliftYoneda.{v', v, u} J).obj X).obj (P := Presheaf.IsSheaf J).map g.op ≫ f.hom.app (op Y)) :
          (a : (fun (X : Type (max v v')) ↦ X) (((uliftYoneda.{v', v, u} J).obj X).obj.obj (op X))) →
            (fun (X : Type (max v v')) ↦ X) (F.obj.obj (op Y)))
        { down := 𝟙 X } :
      (fun (X : Type (max v v')) ↦ X) (F.obj (P := Presheaf.IsSheaf J).obj (op Y)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.hom.app (op Y)) :
          (a : (fun (X : Type (max v v')) ↦ X) (((uliftYoneda.{v', v, u} J).obj X).obj.obj (op Y))) →
            (fun (X : Type (max v v')) ↦ X) (F.obj.obj (op Y)))
        { down := 𝟙 Y ≫ g } :
      (fun (X : Type (max v v')) ↦ X) (F.obj (P := Presheaf.IsSheaf J).obj (op Y)))
⊢ Eq (α := (fun (X : Type (max v v')) ↦ X) (F.obj (P := Presheaf.IsSheaf J).obj (op Y)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.hom.app (op X) ≫ F.obj (P := Presheaf.IsSheaf J).map g.op) :
          (a : (fun (X : Type (max v v')) ↦ X) (((uliftYoneda.{v', v, u} J).obj X).obj.obj (op X))) →
            (fun (X : Type (max v v')) ↦ X) (F.obj.obj (op Y)))
        { down := 𝟙 X } :
      (fun (X : Type (max v v')) ↦ X) (F.obj (P := Presheaf.IsSheaf J).obj (op Y)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.hom.app (op Y)) :
          (a : (fun (X : Type (max v v')) ↦ X) (((uliftYoneda.{v', v, u} J).obj X).obj.obj (op Y))) →
            (fun (X : Type (max v v')) ↦ X) (F.obj.obj (op Y)))
        { down := 𝟙 Y ≫ g } :
      (fun (X : Type (max v v')) ↦ X) (F.obj (P := Presheaf.IsSheaf J).obj (op Y)))

Tactic:
rw [← f.hom.naturality]

Premises used: CategoryTheory.NatTrans.naturality, CategoryTheory.InducedCategory.Hom.hom
-- Module: Mathlib.CategoryTheory.Sites.Subcanonical
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
inst_1 : J.Subcanonical
X Y : C
F : Sheaf J (Type (max v v'))
f : (uliftYoneda.{v', v, u} J).obj X ⟶ F
g : Y ⟶ X
⊢ Eq (α := (fun (X : Type (max v v')) ↦ X) (F.obj (P := Presheaf.IsSheaf J).obj (op Y)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (((uliftYoneda.{v', v, u} J).obj X).obj (P := Presheaf.IsSheaf J).map g.op ≫ f.hom.app (op Y)) :
          (a : (fun (X : Type (max v v')) ↦ X) (((uliftYoneda.{v', v, u} J).obj X).obj.obj (op X))) →
            (fun (X : Type (max v v')) ↦ X) (F.obj.obj (op Y)))
        { down := 𝟙 X } :
      (fun (X : Type (max v v')) ↦ X) (F.obj (P := Presheaf.IsSheaf J).obj (op Y)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.hom.app (op Y)) :
          (a : (fun (X : Type (max v v')) ↦ X) (((uliftYoneda.{v', v, u} J).obj X).obj.obj (op Y))) →
            (fun (X : Type (max v v')) ↦ X) (F.obj.obj (op Y)))
        { down := 𝟙 Y ≫ g } :
      (fun (X : Type (max v v')) ↦ X) (F.obj (P := Presheaf.IsSheaf J).obj (op Y)))

Tactic:
simp [uliftYoneda]

Premises used: CategoryTheory.GrothendieckTopology.uliftYoneda
-- Module: Mathlib.CategoryTheory.Sites.Subcanonical
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
inst_1 : J.Subcanonical
X Y : Cᵒᵖ
F : Sheaf J (Type (max v v'))
f : (uliftYoneda.{v', v, u} J).obj (unop X) ⟶ F
g : X ⟶ Y
⊢ Eq (α := (fun (X : Type (max v v')) ↦ X) (F.obj (P := Presheaf.IsSheaf J).obj Y))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.obj (P := Presheaf.IsSheaf J).map g) :
          (a : (fun (X : Type (max v v')) ↦ X) (F.obj.obj X)) → (fun (X : Type (max v v')) ↦ X) (F.obj.obj Y))
        ((J.uliftYonedaEquiv : (a : (uliftYoneda.{v', v, u} J).obj (unop X) ⟶ F) → F.obj.obj (op (unop X))) f) :
      (fun (X : Type (max v v')) ↦ X) (F.obj (P := Presheaf.IsSheaf J).obj Y))
    ((J.uliftYonedaEquiv : (a : (uliftYoneda.{v', v, u} J).obj (unop Y) ⟶ F) → F.obj.obj (op (unop Y)))
        ((uliftYoneda.{v', v, u} J).map g.unop ≫ f) :
      F.obj (P := Presheaf.IsSheaf J).obj (op (unop Y)))

Tactic:
J.uliftYonedaEquiv_naturality _ _

Premises used: CategoryTheory.GrothendieckTopology.uliftYonedaEquiv_naturality, Quiver.Hom.op, Quiver.Hom.unop
-- Module: Mathlib.CategoryTheory.Sites.Subcanonical
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
inst_1 : J.Subcanonical
X : C
F G : Sheaf J (Type (max v v'))
α : (uliftYoneda.{v', v, u} J).obj X ⟶ F
β : F ⟶ G
⊢ Eq (α := G.obj (P := Presheaf.IsSheaf J).obj (op X))
    ((J.uliftYonedaEquiv : (a : (uliftYoneda.{v', v, u} J).obj X ⟶ G) → G.obj.obj (op X)) (α ≫ β) :
      G.obj (P := Presheaf.IsSheaf J).obj (op X))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (β.hom.app (op X)) :
          (a : (fun (X : Type (max v v')) ↦ X) (F.obj.obj (op X))) → (fun (X : Type (max v v')) ↦ X) (G.obj.obj (op X)))
        ((J.uliftYonedaEquiv : (a : (uliftYoneda.{v', v, u} J).obj X ⟶ F) → F.obj.obj (op X)) α) :
      (fun (X : Type (max v v')) ↦ X) (G.obj (P := Presheaf.IsSheaf J).obj (op X)))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Sites.Subcanonical
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
inst_1 : J.Subcanonical
X Y : C
f : X ⟶ Y
rw :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (((uliftYoneda.{v', v, u} J).map f).hom.app (op X)) :
        (a : (fun (X : Type (max v v')) ↦ X) (((uliftYoneda.{v', v, u} J).obj X).obj.obj (op X))) →
          (fun (X : Type (max v v')) ↦ X) (((uliftYoneda.{v', v, u} J).obj Y).obj.obj (op X)))
      { down := 𝟙 X } =
    { down := f : ULift.{v', v} ((obj (sheafToPresheaf J (Type v)) (J.yoneda.obj Y)).obj (op X)) }
⊢ (J.uliftYonedaEquiv :
        (a : (uliftYoneda.{v', v, u} J).obj X ⟶ (uliftYoneda.{v', v, u} J).obj Y) →
          ((uliftYoneda.{v', v, u} J).obj Y).obj.obj (op X))
      ((uliftYoneda.{v', v, u} J).map f) =
    { down := f : ULift.{v', v} ((obj (sheafToPresheaf J (Type v)) (J.yoneda.obj Y)).obj (op X)) }

Tactic:
rw [uliftYonedaEquiv_apply]

Premises used: CategoryTheory.GrothendieckTopology.uliftYonedaEquiv_apply
-- Module: Mathlib.CategoryTheory.Sites.Subcanonical
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
inst_1 : J.Subcanonical
X Y : C
f : X ⟶ Y
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (((uliftYoneda.{v', v, u} J).map f).hom.app (op X)) :
        (a : (fun (X : Type (max v v')) ↦ X) (((uliftYoneda.{v', v, u} J).obj X).obj.obj (op X))) →
          (fun (X : Type (max v v')) ↦ X) (((uliftYoneda.{v', v, u} J).obj Y).obj.obj (op X)))
      { down := 𝟙 X } =
    { down := f : ULift.{v', v} ((obj (sheafToPresheaf J (Type v)) (J.yoneda.obj Y)).obj (op X)) }

Tactic:
simp [uliftYoneda]

Premises used: CategoryTheory.GrothendieckTopology.uliftYoneda
-- Module: Mathlib.CategoryTheory.Sites.Subcanonical
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
inst_1 : J.Subcanonical
X X' : C
f : X' ⟶ X
F : Sheaf J (Type (max v v'))
x : F.obj (P := Presheaf.IsSheaf J).obj (op X)
a :
  Eq (α := F.obj (P := Presheaf.IsSheaf J).obj (op X'))
    ((J.uliftYonedaEquiv : (a : (uliftYoneda.{v', v, u} J).obj X' ⟶ F) → F.obj.obj (op X'))
        ((uliftYoneda.{v', v, u} J).map f ≫
          (Equiv.symm J.uliftYonedaEquiv : (a : F.obj.obj (op X)) → (uliftYoneda.{v', v, u} J).obj X ⟶ F) x) :
      F.obj (P := Presheaf.IsSheaf J).obj (op X'))
    ((J.uliftYonedaEquiv : (a : (uliftYoneda.{v', v, u} J).obj X' ⟶ F) → F.obj.obj (op X'))
        ((Equiv.symm J.uliftYonedaEquiv : (a : F.obj.obj (op X')) → (uliftYoneda.{v', v, u} J).obj X' ⟶ F)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.obj (P := Presheaf.IsSheaf J).map f.op) :
              (a : (fun (X : Type (max v v')) ↦ X) (F.obj.obj (op X))) →
                (fun (X : Type (max v v')) ↦ X) (F.obj.obj (op X')))
            x)) :
      F.obj (P := Presheaf.IsSheaf J).obj (op X'))
⊢ Eq (α := (uliftYoneda.{v', v, u} J).obj X' ⟶ F)
    ((uliftYoneda.{v', v, u} J).map f ≫
      (Equiv.symm J.uliftYonedaEquiv : (a : F.obj.obj (op X)) → (uliftYoneda.{v', v, u} J).obj X ⟶ F) x)
    ((Equiv.symm J.uliftYonedaEquiv : (a : F.obj.obj (op X')) → (uliftYoneda.{v', v, u} J).obj X' ⟶ F)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.obj (P := Presheaf.IsSheaf J).map f.op) :
          (a : (fun (X : Type (max v v')) ↦ X) (F.obj.obj (op X))) →
            (fun (X : Type (max v v')) ↦ X) (F.obj.obj (op X')))
        x))

Tactic:
apply J.uliftYonedaEquiv.injective

Premises used: CategoryTheory.GrothendieckTopology.uliftYonedaEquiv, Equiv.injective
-- Module: Mathlib.CategoryTheory.Sites.Subcanonical
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
inst_1 : J.Subcanonical
X X' : C
f : X' ⟶ X
F : Sheaf J (Type (max v v'))
x : F.obj (P := Presheaf.IsSheaf J).obj (op X)
a :
  Eq (α := F.obj (P := Presheaf.IsSheaf J).obj (op X'))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (NatTrans.app
              (InducedCategory.Hom.hom
                ((Equiv.symm J.uliftYonedaEquiv : (a : F.obj.obj (op X)) → (uliftYoneda.{v', v, u} J).obj X ⟶ F) x))
              (op X')) :
          (a : ((uliftYoneda.{v', v, u} J).obj X).obj.obj (op X')) → F.obj.obj (op X'))
        ((J.uliftYonedaEquiv :
            (a : (uliftYoneda.{v', v, u} J).obj X' ⟶ (uliftYoneda.{v', v, u} J).obj X) →
              ((uliftYoneda.{v', v, u} J).obj X).obj.obj (op X'))
          ((uliftYoneda.{v', v, u} J).map f)) :
      F.obj (P := Presheaf.IsSheaf J).obj (op X'))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.obj (P := Presheaf.IsSheaf J).map f.op) :
          (a : F.obj.obj (op X)) → F.obj.obj (op X'))
        x :
      F.obj (P := Presheaf.IsSheaf J).obj (op X'))
⊢ Eq (α := F.obj (P := Presheaf.IsSheaf J).obj (op X'))
    ((J.uliftYonedaEquiv : (a : (uliftYoneda.{v', v, u} J).obj X' ⟶ F) → F.obj.obj (op X'))
        ((uliftYoneda.{v', v, u} J).map f ≫
          (Equiv.symm J.uliftYonedaEquiv : (a : F.obj.obj (op X)) → (uliftYoneda.{v', v, u} J).obj X ⟶ F) x) :
      F.obj (P := Presheaf.IsSheaf J).obj (op X'))
    ((J.uliftYonedaEquiv : (a : (uliftYoneda.{v', v, u} J).obj X' ⟶ F) → F.obj.obj (op X'))
        ((Equiv.symm J.uliftYonedaEquiv : (a : F.obj.obj (op X')) → (uliftYoneda.{v', v, u} J).obj X' ⟶ F)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.obj (P := Presheaf.IsSheaf J).map f.op) :
              (a : (fun (X : Type (max v v')) ↦ X) (F.obj.obj (op X))) →
                (fun (X : Type (max v v')) ↦ X) (F.obj.obj (op X')))
            x)) :
      F.obj (P := Presheaf.IsSheaf J).obj (op X'))

Tactic:
simp only [uliftYonedaEquiv_comp, Equiv.apply_symm_apply]

Premises used: Equiv.apply_symm_apply, CategoryTheory.GrothendieckTopology.uliftYonedaEquiv_comp
-- Module: Mathlib.CategoryTheory.Sites.Subcanonical
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
inst_1 : J.Subcanonical
X X' : C
f : X' ⟶ X
F : Sheaf J (Type (max v v'))
x : F.obj (P := Presheaf.IsSheaf J).obj (op X)
a :
  Eq (α := F.obj (P := Presheaf.IsSheaf J).obj (op X'))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (NatTrans.app
              (InducedCategory.Hom.hom
                ((Equiv.symm J.uliftYonedaEquiv : (a : F.obj.obj (op X)) → (uliftYoneda.{v', v, u} J).obj X ⟶ F) x))
              (op X')) :
          (a : ((uliftYoneda.{v', v, u} J).obj X).obj.obj (op X')) → F.obj.obj (op X'))
        { down := f } :
      F.obj (P := Presheaf.IsSheaf J).obj (op X'))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.obj (P := Presheaf.IsSheaf J).map f.op) :
          (a : F.obj.obj (op X)) → F.obj.obj (op X'))
        x :
      F.obj (P := Presheaf.IsSheaf J).obj (op X'))
⊢ Eq (α := F.obj (P := Presheaf.IsSheaf J).obj (op X'))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (NatTrans.app
              (InducedCategory.Hom.hom
                ((Equiv.symm J.uliftYonedaEquiv : (a : F.obj.obj (op X)) → (uliftYoneda.{v', v, u} J).obj X ⟶ F) x))
              (op X')) :
          (a : ((uliftYoneda.{v', v, u} J).obj X).obj.obj (op X')) → F.obj.obj (op X'))
        ((J.uliftYonedaEquiv :
            (a : (uliftYoneda.{v', v, u} J).obj X' ⟶ (uliftYoneda.{v', v, u} J).obj X) →
              ((uliftYoneda.{v', v, u} J).obj X).obj.obj (op X'))
          ((uliftYoneda.{v', v, u} J).map f)) :
      F.obj (P := Presheaf.IsSheaf J).obj (op X'))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.obj (P := Presheaf.IsSheaf J).map f.op) :
          (a : F.obj.obj (op X)) → F.obj.obj (op X'))
        x :
      F.obj (P := Presheaf.IsSheaf J).obj (op X'))

Tactic:
rw [uliftYonedaEquiv_uliftYoneda_map]

Premises used: CategoryTheory.GrothendieckTopology.uliftYonedaEquiv_uliftYoneda_map
-- Module: Mathlib.CategoryTheory.Sites.Subcanonical
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
inst_1 : J.Subcanonical
X X' : C
f : X' ⟶ X
F : Sheaf J (Type (max v v'))
x : F.obj (P := Presheaf.IsSheaf J).obj (op X)
⊢ Eq (α := F.obj (P := Presheaf.IsSheaf J).obj (op X'))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (NatTrans.app
              (InducedCategory.Hom.hom
                ((Equiv.symm J.uliftYonedaEquiv : (a : F.obj.obj (op X)) → (uliftYoneda.{v', v, u} J).obj X ⟶ F) x))
              (op X')) :
          (a : ((uliftYoneda.{v', v, u} J).obj X).obj.obj (op X')) → F.obj.obj (op X'))
        { down := f } :
      F.obj (P := Presheaf.IsSheaf J).obj (op X'))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.obj (P := Presheaf.IsSheaf J).map f.op) :
          (a : F.obj.obj (op X)) → F.obj.obj (op X'))
        x :
      F.obj (P := Presheaf.IsSheaf J).obj (op X'))

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Sites.Subcanonical
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
inst_1 : J.Subcanonical
X : C
F F' : Sheaf J (Type (max v v'))
f : F ⟶ F'
x : F.obj (P := Presheaf.IsSheaf J).obj (op X)
a :
  Eq (α := F'.obj (P := Presheaf.IsSheaf J).obj (op X))
    ((J.uliftYonedaEquiv : (a : (uliftYoneda.{v', v, u} J).obj X ⟶ F') → F'.obj.obj (op X))
        ((Equiv.symm J.uliftYonedaEquiv : (a : F.obj.obj (op X)) → (uliftYoneda.{v', v, u} J).obj X ⟶ F) x ≫ f) :
      F'.obj (P := Presheaf.IsSheaf J).obj (op X))
    ((J.uliftYonedaEquiv : (a : (uliftYoneda.{v', v, u} J).obj X ⟶ F') → F'.obj.obj (op X))
        ((Equiv.symm J.uliftYonedaEquiv : (a : F'.obj.obj (op X)) → (uliftYoneda.{v', v, u} J).obj X ⟶ F')
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.hom.app (op X)) :
              (a : (fun (X : Type (max v v')) ↦ X) (F.obj.obj (op X))) →
                (fun (X : Type (max v v')) ↦ X) (F'.obj.obj (op X)))
            x)) :
      F'.obj (P := Presheaf.IsSheaf J).obj (op X))
⊢ Eq (α := (uliftYoneda.{v', v, u} J).obj X ⟶ F')
    ((Equiv.symm J.uliftYonedaEquiv : (a : F.obj.obj (op X)) → (uliftYoneda.{v', v, u} J).obj X ⟶ F) x ≫ f :
      (uliftYoneda.{v', v, u} J).obj X ⟶ F')
    ((Equiv.symm J.uliftYonedaEquiv : (a : F'.obj.obj (op X)) → (uliftYoneda.{v', v, u} J).obj X ⟶ F')
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.hom.app (op X)) :
            (a : (fun (X : Type (max v v')) ↦ X) (F.obj.obj (op X))) →
              (fun (X : Type (max v v')) ↦ X) (F'.obj.obj (op X)))
          x) :
      (uliftYoneda.{v', v, u} J).obj X ⟶ F')

Tactic:
apply J.uliftYonedaEquiv.injective

Premises used: CategoryTheory.GrothendieckTopology.uliftYonedaEquiv, Equiv.injective
-- Module: Mathlib.CategoryTheory.Sites.Subcanonical
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
inst_1 : J.Subcanonical
X : C
F F' : Sheaf J (Type (max v v'))
f : F ⟶ F'
x : F.obj (P := Presheaf.IsSheaf J).obj (op X)
⊢ Eq (α := F'.obj (P := Presheaf.IsSheaf J).obj (op X))
    ((J.uliftYonedaEquiv : (a : (uliftYoneda.{v', v, u} J).obj X ⟶ F') → F'.obj.obj (op X))
        ((Equiv.symm J.uliftYonedaEquiv : (a : F.obj.obj (op X)) → (uliftYoneda.{v', v, u} J).obj X ⟶ F) x ≫ f) :
      F'.obj (P := Presheaf.IsSheaf J).obj (op X))
    ((J.uliftYonedaEquiv : (a : (uliftYoneda.{v', v, u} J).obj X ⟶ F') → F'.obj.obj (op X))
        ((Equiv.symm J.uliftYonedaEquiv : (a : F'.obj.obj (op X)) → (uliftYoneda.{v', v, u} J).obj X ⟶ F')
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.hom.app (op X)) :
              (a : (fun (X : Type (max v v')) ↦ X) (F.obj.obj (op X))) →
                (fun (X : Type (max v v')) ↦ X) (F'.obj.obj (op X)))
            x)) :
      F'.obj (P := Presheaf.IsSheaf J).obj (op X))

Tactic:
simp [uliftYonedaEquiv_comp]

Premises used: CategoryTheory.GrothendieckTopology.uliftYonedaEquiv_comp
-- Module: Mathlib.CategoryTheory.Sites.Subcanonical
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
inst_1 : J.Subcanonical
X Y : Cᵒᵖ
f : X ⟶ Y
F : Sheaf J (Type (max v v'))
t : F.obj (P := Presheaf.IsSheaf J).obj X
obtain :
  ∀ (u : (uliftYoneda.{v', v, u} J).obj (unop X) ⟶ F),
    Eq (α := (uliftYoneda.{v', v, u} J).obj (unop Y) ⟶ F)
      ((Equiv.symm J.uliftYonedaEquiv : (a : F.obj.obj (op (unop Y))) → (uliftYoneda.{v', v, u} J).obj (unop Y) ⟶ F)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.obj (P := Presheaf.IsSheaf J).map f) :
              (a : (fun (X : Type (max v v')) ↦ X) (F.obj.obj X)) → (fun (X : Type (max v v')) ↦ X) (F.obj.obj Y))
            ((J.uliftYonedaEquiv : (a : (uliftYoneda.{v', v, u} J).obj (unop X) ⟶ F) → F.obj.obj (op (unop X))) u)) :
        (uliftYoneda.{v', v, u} J).obj (unop Y) ⟶ F)
      ((uliftYoneda.{v', v, u} J).map f.unop ≫
          (Equiv.symm J.uliftYonedaEquiv : (a : F.obj.obj (op (unop X))) → (uliftYoneda.{v', v, u} J).obj (unop X) ⟶ F)
            ((J.uliftYonedaEquiv : (a : (uliftYoneda.{v', v, u} J).obj (unop X) ⟶ F) → F.obj.obj (op (unop X))) u) :
        (uliftYoneda.{v', v, u} J).obj (unop Y) ⟶ F)
⊢ Eq (α := (uliftYoneda.{v', v, u} J).obj (unop Y) ⟶ F)
    ((Equiv.symm J.uliftYonedaEquiv : (a : F.obj.obj (op (unop Y))) → (uliftYoneda.{v', v, u} J).obj (unop Y) ⟶ F)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.obj (P := Presheaf.IsSheaf J).map f) :
            (a : (fun (X : Type (max v v')) ↦ X) (F.obj.obj X)) → (fun (X : Type (max v v')) ↦ X) (F.obj.obj Y))
          t) :
      (uliftYoneda.{v', v, u} J).obj (unop Y) ⟶ F)
    ((uliftYoneda.{v', v, u} J).map f.unop ≫
        (Equiv.symm J.uliftYonedaEquiv : (a : F.obj.obj (op (unop X))) → (uliftYoneda.{v', v, u} J).obj (unop X) ⟶ F)
          t :
      (uliftYoneda.{v', v, u} J).obj (unop Y) ⟶ F)

Tactic:
obtain ⟨u, rfl⟩ := J.uliftYonedaEquiv.surjective t

Premises used: CategoryTheory.GrothendieckTopology.uliftYonedaEquiv, Equiv.surjective, rfl
-- Module: Mathlib.CategoryTheory.Sites.Subcanonical
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
inst_1 : J.Subcanonical
X Y : Cᵒᵖ
f : X ⟶ Y
F : Sheaf J (Type (max v v'))
u : (uliftYoneda.{v', v, u} J).obj (unop X) ⟶ F
rw :
  Eq (α := (uliftYoneda.{v', v, u} J).obj (unop Y) ⟶ F)
    ((Equiv.symm J.uliftYonedaEquiv : (a : F.obj.obj (op (unop Y))) → (uliftYoneda.{v', v, u} J).obj (unop Y) ⟶ F)
        ((J.uliftYonedaEquiv : (a : (uliftYoneda.{v', v, u} J).obj (unop Y) ⟶ F) → F.obj.obj (op (unop Y)))
          ((uliftYoneda.{v', v, u} J).map f.unop ≫ u)) :
      (uliftYoneda.{v', v, u} J).obj (unop Y) ⟶ F)
    ((uliftYoneda.{v', v, u} J).map f.unop ≫
        (Equiv.symm J.uliftYonedaEquiv : (a : F.obj.obj (op (unop X))) → (uliftYoneda.{v', v, u} J).obj (unop X) ⟶ F)
          ((J.uliftYonedaEquiv : (a : (uliftYoneda.{v', v, u} J).obj (unop X) ⟶ F) → F.obj.obj (op (unop X))) u) :
      (uliftYoneda.{v', v, u} J).obj (unop Y) ⟶ F)
rw₁ :
  (uliftYoneda.{v', v, u} J).map f.unop ≫ u =
    (uliftYoneda.{v', v, u} J).map f.unop ≫
      (Equiv.symm J.uliftYonedaEquiv : (a : F.obj.obj (op (unop X))) → (uliftYoneda.{v', v, u} J).obj (unop X) ⟶ F)
        ((J.uliftYonedaEquiv : (a : (uliftYoneda.{v', v, u} J).obj (unop X) ⟶ F) → F.obj.obj (op (unop X))) u)
rw₂ rw₃ : (uliftYoneda.{v', v, u} J).map f.unop ≫ u = (uliftYoneda.{v', v, u} J).map f.unop ≫ u
⊢ Eq (α := (uliftYoneda.{v', v, u} J).obj (unop Y) ⟶ F)
    ((Equiv.symm J.uliftYonedaEquiv : (a : F.obj.obj (op (unop Y))) → (uliftYoneda.{v', v, u} J).obj (unop Y) ⟶ F)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.obj (P := Presheaf.IsSheaf J).map f) :
            (a : (fun (X : Type (max v v')) ↦ X) (F.obj.obj X)) → (fun (X : Type (max v v')) ↦ X) (F.obj.obj Y))
          ((J.uliftYonedaEquiv : (a : (uliftYoneda.{v', v, u} J).obj (unop X) ⟶ F) → F.obj.obj (op (unop X))) u)) :
      (uliftYoneda.{v', v, u} J).obj (unop Y) ⟶ F)
    ((uliftYoneda.{v', v, u} J).map f.unop ≫
        (Equiv.symm J.uliftYonedaEquiv : (a : F.obj.obj (op (unop X))) → (uliftYoneda.{v', v, u} J).obj (unop X) ⟶ F)
          ((J.uliftYonedaEquiv : (a : (uliftYoneda.{v', v, u} J).obj (unop X) ⟶ F) → F.obj.obj (op (unop X))) u) :
      (uliftYoneda.{v', v, u} J).obj (unop Y) ⟶ F)

Tactic:
rw [uliftYonedaEquiv_naturality', Equiv.symm_apply_apply, Equiv.symm_apply_apply]

Premises used: Equiv.symm_apply_apply, CategoryTheory.GrothendieckTopology.uliftYonedaEquiv_naturality'
-- Module: Mathlib.CategoryTheory.Sites.Subcanonical
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
inst_1 : J.Subcanonical
P Q : Sheaf J (Type (max v v'))
f g : P ⟶ Q
h : ∀ (X : C) (p : (uliftYoneda.{v', v, u} J).obj X ⟶ P), p ≫ f = p ≫ g
h₁ :
  ∀ (X : Cᵒᵖ) (x : P.obj (P := Presheaf.IsSheaf J).obj X),
    (ConcreteCategory.hom (FC := TypeCat.Fun) (f.hom.app X)).toFun x =
      (ConcreteCategory.hom (FC := TypeCat.Fun) (g.hom.app X)).toFun x
⊢ f = g

Tactic:
ext X x
-- Module: Mathlib.CategoryTheory.Sites.Subcanonical
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
inst_1 : J.Subcanonical
P Q : Sheaf J (Type (max v v'))
f g : P ⟶ Q
h : ∀ (X : C) (p : (uliftYoneda.{v', v, u} J).obj X ⟶ P), p ≫ f = p ≫ g
X : Cᵒᵖ
x : P.obj (P := Presheaf.IsSheaf J).obj X
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (f.hom.app X)).toFun x =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (g.hom.app X)).toFun x

Tactic:
simpa only [uliftYonedaEquiv_comp, Equiv.apply_symm_apply]
    using congr_arg (J.uliftYonedaEquiv) (h _ (J.uliftYonedaEquiv.symm x))

Premises used: CategoryTheory.GrothendieckTopology.uliftYonedaEquiv, Equiv.apply_symm_apply, congr_arg, Equiv.symm, DFunLike.coe, CategoryTheory.GrothendieckTopology.uliftYonedaEquiv_comp
-- Module: Mathlib.CategoryTheory.Sites.Subcanonical
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
inst_1 : J.Subcanonical
X : Cᵒᵖ
F : Sheaf J (Type (max v v'))
s : ULift.{u, max v v'} (F.obj (P := Presheaf.IsSheaf J).obj X)
⊢ Eq (α := obj (obj coyoneda (op ((uliftYoneda.{v', v, u} J).obj (unop X)))) F)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (NatTrans.app (Iso.inv J.uliftYonedaOpCompCoyoneda) X) F) :
          (a :
              (sheafToPresheaf J (Type (max v v')) ⋙
                    (evaluation Cᵒᵖ (Type (max v v'))).obj X ⋙ uliftFunctor.{u, max v v'}).obj
                F) →
            (coyoneda.obj (op ((uliftYoneda.{v', v, u} J).obj (unop X)))).obj F)
        s :
      obj (obj coyoneda (op ((uliftYoneda.{v', v, u} J).obj (unop X)))) F)
    ((Equiv.symm J.uliftYonedaEquiv : (a : F.obj.obj X) → (uliftYoneda.{v', v, u} J).obj (unop X) ⟶ F) s.down :
      (uliftYoneda.{v', v, u} J).obj (unop X) ⟶ F)

Tactic:
rfl

Premises used: CategoryTheory.NatTrans.vcomp, CategoryTheory.Functor.comp, TypeCat.Fun.comp, rfl