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 v)
f : J.yoneda.obj (unop X) ⟶ F
g : X ⟶ Y
⊢ Eq (α := (fun (X : Type 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 v) ↦ X) (F.obj.obj X)) → (fun (X : Type v) ↦ X) (F.obj.obj Y))
        ((J.yonedaEquiv : (a : J.yoneda.obj (unop X) ⟶ F) → F.obj.obj (op (unop X))) f :
          F.obj (P := Presheaf.IsSheaf J).obj (op (unop X))) :
      (fun (X : Type v) ↦ X) (F.obj (P := Presheaf.IsSheaf J).obj Y))
    ((J.yonedaEquiv : (a : J.yoneda.obj (unop Y) ⟶ F) → F.obj.obj (op (unop Y))) (J.yoneda.map g.unop ≫ f) :
      F.obj (P := Presheaf.IsSheaf J).obj (op (unop Y)))

Tactic:
J.yonedaEquiv_naturality _ _

Premises used: Quiver.Hom.op, Quiver.Hom.unop, CategoryTheory.GrothendieckTopology.yonedaEquiv_naturality
-- 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 v)
α : J.yoneda.obj X ⟶ F
β : F ⟶ G
⊢ Eq.{v + 1} (α := G.obj (P := Presheaf.IsSheaf J).obj (op X))
    ((J.yonedaEquiv : (a : J.yoneda.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 v) ↦ X) (F.obj.obj (op X))) → (fun (X : Type v) ↦ X) (G.obj.obj (op X)))
        ((J.yonedaEquiv : (a : J.yoneda.obj X ⟶ F) → F.obj.obj (op X)) α : F.obj (P := Presheaf.IsSheaf J).obj (op X)) :
      (fun (X : Type 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) ((J.yoneda.map f).hom.app (op X)) :
        (a : (fun (X : Type v) ↦ X) ((J.yoneda.obj X).obj.obj (op X))) →
          (fun (X : Type v) ↦ X) ((J.yoneda.obj Y).obj.obj (op X)))
      (𝟙 X) =
    f
⊢ (J.yonedaEquiv : (a : J.yoneda.obj X ⟶ J.yoneda.obj Y) → (J.yoneda.obj Y).obj.obj (op X)) (J.yoneda.map f) = f

Tactic:
rw [yonedaEquiv_apply]

Premises used: CategoryTheory.GrothendieckTopology.yonedaEquiv_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) ((J.yoneda.map f).hom.app (op X)) :
        (a : (fun (X : Type v) ↦ X) ((J.yoneda.obj X).obj.obj (op X))) →
          (fun (X : Type v) ↦ X) ((J.yoneda.obj Y).obj.obj (op X)))
      (𝟙 X) =
    f

Tactic:
simp
-- 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 v)
x : F.obj (P := Presheaf.IsSheaf J).obj (op X)
a :
  Eq.{v + 1} (α := F.obj (P := Presheaf.IsSheaf J).obj (op X'))
    ((J.yonedaEquiv : (a : J.yoneda.obj X' ⟶ F) → F.obj.obj (op X'))
        (J.yoneda.map f ≫ (Equiv.symm J.yonedaEquiv : (a : F.obj.obj (op X)) → J.yoneda.obj X ⟶ F) x) :
      F.obj (P := Presheaf.IsSheaf J).obj (op X'))
    ((J.yonedaEquiv : (a : J.yoneda.obj X' ⟶ F) → F.obj.obj (op X'))
        ((Equiv.symm J.yonedaEquiv : (a : F.obj.obj (op X')) → J.yoneda.obj X' ⟶ F)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.obj (P := Presheaf.IsSheaf J).map f.op) :
              (a : (fun (X : Type v) ↦ X) (F.obj.obj (op X))) → (fun (X : Type v) ↦ X) (F.obj.obj (op X')))
            x)) :
      F.obj (P := Presheaf.IsSheaf J).obj (op X'))
⊢ Eq (α := J.yoneda.obj X' ⟶ F)
    (J.yoneda.map f ≫ (Equiv.symm J.yonedaEquiv : (a : F.obj.obj (op X)) → J.yoneda.obj X ⟶ F) x)
    ((Equiv.symm J.yonedaEquiv : (a : F.obj.obj (op X')) → J.yoneda.obj X' ⟶ F)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.obj (P := Presheaf.IsSheaf J).map f.op) :
          (a : (fun (X : Type v) ↦ X) (F.obj.obj (op X))) → (fun (X : Type v) ↦ X) (F.obj.obj (op X')))
        x))

Tactic:
apply J.yonedaEquiv.injective

Premises used: CategoryTheory.GrothendieckTopology.yonedaEquiv, 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 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.yonedaEquiv : (a : F.obj.obj (op X)) → J.yoneda.obj X ⟶ F) x))
              (op X')) :
          (a : (fun (X : Type v) ↦ X) ((J.yoneda.obj X).obj.obj (op X'))) → (fun (X : Type v) ↦ X) (F.obj.obj (op X')))
        f :
      (fun (X : Type v) ↦ X) (F.obj (P := Presheaf.IsSheaf J).obj (op X')))
    ((J.yonedaEquiv : (a : J.yoneda.obj X' ⟶ F) → F.obj.obj (op X'))
        ((Equiv.symm J.yonedaEquiv : (a : F.obj.obj (op X')) → J.yoneda.obj X' ⟶ F)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.obj (P := Presheaf.IsSheaf J).map f.op) :
              (a : (fun (X : Type v) ↦ X) (F.obj.obj (op X))) → (fun (X : Type v) ↦ X) (F.obj.obj (op X')))
            x)) :
      F.obj (P := Presheaf.IsSheaf J).obj (op X'))
⊢ Eq.{v + 1} (α := F.obj (P := Presheaf.IsSheaf J).obj (op X'))
    ((J.yonedaEquiv : (a : J.yoneda.obj X' ⟶ F) → F.obj.obj (op X'))
        (J.yoneda.map f ≫ (Equiv.symm J.yonedaEquiv : (a : F.obj.obj (op X)) → J.yoneda.obj X ⟶ F) x) :
      F.obj (P := Presheaf.IsSheaf J).obj (op X'))
    ((J.yonedaEquiv : (a : J.yoneda.obj X' ⟶ F) → F.obj.obj (op X'))
        ((Equiv.symm J.yonedaEquiv : (a : F.obj.obj (op X')) → J.yoneda.obj X' ⟶ F)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.obj (P := Presheaf.IsSheaf J).map f.op) :
              (a : (fun (X : Type v) ↦ X) (F.obj.obj (op X))) → (fun (X : Type v) ↦ X) (F.obj.obj (op X')))
            x)) :
      F.obj (P := Presheaf.IsSheaf J).obj (op X'))

Tactic:
rw [yonedaEquiv_comp, yonedaEquiv_yoneda_map]

Premises used: CategoryTheory.GrothendieckTopology.yonedaEquiv_comp, CategoryTheory.GrothendieckTopology.yonedaEquiv_yoneda_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 v)
x : F.obj (P := Presheaf.IsSheaf J).obj (op X)
a :
  Eq (α := F.obj (P := Presheaf.IsSheaf J).obj (op X'))
    ((@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
            (NatTrans.app
              (InducedCategory.Hom.hom ((Equiv.symm J.yonedaEquiv : (a : F.obj.obj (op X)) → J.yoneda.obj X ⟶ F) x))
              (op X')) :
          (a : X' ⟶ X) → F.obj.obj (op X'))
        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.yonedaEquiv : (a : F.obj.obj (op X)) → J.yoneda.obj X ⟶ F) x))
              (op X')) :
          (a : (fun (X : Type v) ↦ X) ((J.yoneda.obj X).obj.obj (op X'))) → (fun (X : Type v) ↦ X) (F.obj.obj (op X')))
        f :
      (fun (X : Type v) ↦ X) (F.obj (P := Presheaf.IsSheaf J).obj (op X')))
    ((J.yonedaEquiv : (a : J.yoneda.obj X' ⟶ F) → F.obj.obj (op X'))
        ((Equiv.symm J.yonedaEquiv : (a : F.obj.obj (op X')) → J.yoneda.obj X' ⟶ F)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.obj (P := Presheaf.IsSheaf J).map f.op) :
              (a : (fun (X : Type v) ↦ X) (F.obj.obj (op X))) → (fun (X : Type v) ↦ X) (F.obj.obj (op X')))
            x)) :
      F.obj (P := Presheaf.IsSheaf J).obj (op X'))

Tactic:
simp
-- 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 v)
x : F.obj (P := Presheaf.IsSheaf J).obj (op X)
⊢ Eq (α := F.obj (P := Presheaf.IsSheaf J).obj (op X'))
    ((@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
            (NatTrans.app
              (InducedCategory.Hom.hom ((Equiv.symm J.yonedaEquiv : (a : F.obj.obj (op X)) → J.yoneda.obj X ⟶ F) x))
              (op X')) :
          (a : X' ⟶ X) → F.obj.obj (op X'))
        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 v)
f : F ⟶ F'
x : F.obj (P := Presheaf.IsSheaf J).obj (op X)
a :
  Eq.{v + 1} (α := F'.obj (P := Presheaf.IsSheaf J).obj (op X))
    ((J.yonedaEquiv : (a : J.yoneda.obj X ⟶ F') → F'.obj.obj (op X))
        ((Equiv.symm J.yonedaEquiv : (a : F.obj.obj (op X)) → J.yoneda.obj X ⟶ F) x ≫ f) :
      F'.obj (P := Presheaf.IsSheaf J).obj (op X))
    ((J.yonedaEquiv : (a : J.yoneda.obj X ⟶ F') → F'.obj.obj (op X))
        ((Equiv.symm J.yonedaEquiv : (a : F'.obj.obj (op X)) → J.yoneda.obj X ⟶ F')
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.hom.app (op X)) :
              (a : (fun (X : Type v) ↦ X) (F.obj.obj (op X))) → (fun (X : Type v) ↦ X) (F'.obj.obj (op X)))
            x)) :
      F'.obj (P := Presheaf.IsSheaf J).obj (op X))
⊢ Eq (α := J.yoneda.obj X ⟶ F')
    ((Equiv.symm J.yonedaEquiv : (a : F.obj.obj (op X)) → J.yoneda.obj X ⟶ F) x ≫ f : J.yoneda.obj X ⟶ F')
    ((Equiv.symm J.yonedaEquiv : (a : F'.obj.obj (op X)) → J.yoneda.obj X ⟶ F')
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.hom.app (op X)) :
            (a : (fun (X : Type v) ↦ X) (F.obj.obj (op X))) → (fun (X : Type v) ↦ X) (F'.obj.obj (op X)))
          x) :
      J.yoneda.obj X ⟶ F')

Tactic:
apply J.yonedaEquiv.injective

Premises used: CategoryTheory.GrothendieckTopology.yonedaEquiv, 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 v)
f : F ⟶ F'
x : F.obj (P := Presheaf.IsSheaf J).obj (op X)
⊢ Eq.{v + 1} (α := F'.obj (P := Presheaf.IsSheaf J).obj (op X))
    ((J.yonedaEquiv : (a : J.yoneda.obj X ⟶ F') → F'.obj.obj (op X))
        ((Equiv.symm J.yonedaEquiv : (a : F.obj.obj (op X)) → J.yoneda.obj X ⟶ F) x ≫ f) :
      F'.obj (P := Presheaf.IsSheaf J).obj (op X))
    ((J.yonedaEquiv : (a : J.yoneda.obj X ⟶ F') → F'.obj.obj (op X))
        ((Equiv.symm J.yonedaEquiv : (a : F'.obj.obj (op X)) → J.yoneda.obj X ⟶ F')
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.hom.app (op X)) :
              (a : (fun (X : Type v) ↦ X) (F.obj.obj (op X))) → (fun (X : Type v) ↦ X) (F'.obj.obj (op X)))
            x)) :
      F'.obj (P := Presheaf.IsSheaf J).obj (op X))

Tactic:
simp [yonedaEquiv_comp]

Premises used: CategoryTheory.GrothendieckTopology.yonedaEquiv_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 : Sheaf J (Type v)
f : J.yoneda.obj X ⟶ F
g : Y ⟶ X
rw :
  Eq.{v + 1} (α := (fun (X : Type v) ↦ X) (F.obj (P := Presheaf.IsSheaf J).obj (op Y)))
    ((J.yonedaEquiv : (a : J.yoneda.obj Y ⟶ F) → F.obj.obj (op Y)) (J.yoneda.map g ≫ f) :
      F.obj (P := Presheaf.IsSheaf J).obj (op Y))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.hom.app (op Y)) :
          (a : (fun (X : Type v) ↦ X) ((J.yoneda.obj X).obj.obj (op Y))) → (fun (X : Type v) ↦ X) (F.obj.obj (op Y)))
        g :
      (fun (X : Type v) ↦ X) (F.obj (P := Presheaf.IsSheaf J).obj (op Y)))
rw₁ :
  Eq (α := (fun (X : Type 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 v) ↦ X) ((J.yoneda.obj X).obj.obj (op Y))) → (fun (X : Type v) ↦ X) (F.obj.obj (op Y)))
        ((J.yonedaEquiv : (a : J.yoneda.obj Y ⟶ J.yoneda.obj X) → (J.yoneda.obj X).obj.obj (op Y)) (J.yoneda.map g) :
          (J.yoneda.obj X).obj (P := Presheaf.IsSheaf J).obj (op Y)) :
      (fun (X : Type 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 v) ↦ X) ((J.yoneda.obj X).obj.obj (op Y))) → (fun (X : Type v) ↦ X) (F.obj.obj (op Y)))
        g :
      (fun (X : Type v) ↦ X) (F.obj (P := Presheaf.IsSheaf J).obj (op Y)))
rw₂ rw₃ :
  Eq (α := (fun (X : Type 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 v) ↦ X) ((J.yoneda.obj X).obj.obj (op Y))) → (fun (X : Type v) ↦ X) (F.obj.obj (op Y)))
        g :
      (fun (X : Type 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 v) ↦ X) ((J.yoneda.obj X).obj.obj (op Y))) → (fun (X : Type v) ↦ X) (F.obj.obj (op Y)))
        g :
      (fun (X : Type v) ↦ X) (F.obj (P := Presheaf.IsSheaf J).obj (op Y)))
⊢ Eq (α := (fun (X : Type v) ↦ X) (F.obj (P := Presheaf.IsSheaf J).obj (op Y)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.obj (P := Presheaf.IsSheaf J).map g.op) :
          (a : (fun (X : Type v) ↦ X) (F.obj.obj (op X))) → (fun (X : Type v) ↦ X) (F.obj.obj (op Y)))
        ((J.yonedaEquiv : (a : J.yoneda.obj X ⟶ F) → F.obj.obj (op X)) f : F.obj (P := Presheaf.IsSheaf J).obj (op X)) :
      (fun (X : Type 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 v) ↦ X) ((J.yoneda.obj X).obj.obj (op Y))) → (fun (X : Type v) ↦ X) (F.obj.obj (op Y)))
        g :
      (fun (X : Type v) ↦ X) (F.obj (P := Presheaf.IsSheaf J).obj (op Y)))

Tactic:
rw [yonedaEquiv_naturality, yonedaEquiv_comp, yonedaEquiv_yoneda_map]

Premises used: CategoryTheory.GrothendieckTopology.yonedaEquiv_comp, CategoryTheory.GrothendieckTopology.yonedaEquiv_naturality, CategoryTheory.GrothendieckTopology.yonedaEquiv_yoneda_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 Y : Cᵒᵖ
f : X ⟶ Y
F : Sheaf J (Type v)
t : F.obj (P := Presheaf.IsSheaf J).obj X
obtain :
  ∀ (u : J.yoneda.obj (unop X) ⟶ F),
    Eq (α := J.yoneda.obj (unop Y) ⟶ F)
      ((Equiv.symm J.yonedaEquiv : (a : F.obj.obj (op (unop Y))) → J.yoneda.obj (unop Y) ⟶ F)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.obj (P := Presheaf.IsSheaf J).map f) :
              (a : (fun (X : Type v) ↦ X) (F.obj.obj X)) → (fun (X : Type v) ↦ X) (F.obj.obj Y))
            ((J.yonedaEquiv : (a : J.yoneda.obj (unop X) ⟶ F) → F.obj.obj (op (unop X))) u :
              F.obj (P := Presheaf.IsSheaf J).obj (op (unop X)))) :
        J.yoneda.obj (unop Y) ⟶ F)
      (J.yoneda.map f.unop ≫
          (Equiv.symm J.yonedaEquiv : (a : F.obj.obj (op (unop X))) → J.yoneda.obj (unop X) ⟶ F)
            ((J.yonedaEquiv : (a : J.yoneda.obj (unop X) ⟶ F) → F.obj.obj (op (unop X))) u) :
        J.yoneda.obj (unop Y) ⟶ F)
⊢ Eq (α := J.yoneda.obj (unop Y) ⟶ F)
    ((Equiv.symm J.yonedaEquiv : (a : F.obj.obj (op (unop Y))) → J.yoneda.obj (unop Y) ⟶ F)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.obj (P := Presheaf.IsSheaf J).map f) :
            (a : (fun (X : Type v) ↦ X) (F.obj.obj X)) → (fun (X : Type v) ↦ X) (F.obj.obj Y))
          t) :
      J.yoneda.obj (unop Y) ⟶ F)
    (J.yoneda.map f.unop ≫ (Equiv.symm J.yonedaEquiv : (a : F.obj.obj (op (unop X))) → J.yoneda.obj (unop X) ⟶ F) t :
      J.yoneda.obj (unop Y) ⟶ F)

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

Premises used: CategoryTheory.GrothendieckTopology.yonedaEquiv, 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 v)
u : J.yoneda.obj (unop X) ⟶ F
rw :
  Eq (α := J.yoneda.obj (unop Y) ⟶ F)
    ((Equiv.symm J.yonedaEquiv : (a : F.obj.obj (op (unop Y))) → J.yoneda.obj (unop Y) ⟶ F)
        ((J.yonedaEquiv : (a : J.yoneda.obj (unop Y) ⟶ F) → F.obj.obj (op (unop Y))) (J.yoneda.map f.unop ≫ u)) :
      J.yoneda.obj (unop Y) ⟶ F)
    (J.yoneda.map f.unop ≫
        (Equiv.symm J.yonedaEquiv : (a : F.obj.obj (op (unop X))) → J.yoneda.obj (unop X) ⟶ F)
          ((J.yonedaEquiv : (a : J.yoneda.obj (unop X) ⟶ F) → F.obj.obj (op (unop X))) u) :
      J.yoneda.obj (unop Y) ⟶ F)
rw₁ :
  J.yoneda.map f.unop ≫ u =
    J.yoneda.map f.unop ≫
      (Equiv.symm J.yonedaEquiv : (a : F.obj.obj (op (unop X))) → J.yoneda.obj (unop X) ⟶ F)
        ((J.yonedaEquiv : (a : J.yoneda.obj (unop X) ⟶ F) → F.obj.obj (op (unop X))) u)
rw₂ rw₃ : J.yoneda.map f.unop ≫ u = J.yoneda.map f.unop ≫ u
⊢ Eq (α := J.yoneda.obj (unop Y) ⟶ F)
    ((Equiv.symm J.yonedaEquiv : (a : F.obj.obj (op (unop Y))) → J.yoneda.obj (unop Y) ⟶ F)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.obj (P := Presheaf.IsSheaf J).map f) :
            (a : (fun (X : Type v) ↦ X) (F.obj.obj X)) → (fun (X : Type v) ↦ X) (F.obj.obj Y))
          ((J.yonedaEquiv : (a : J.yoneda.obj (unop X) ⟶ F) → F.obj.obj (op (unop X))) u :
            F.obj (P := Presheaf.IsSheaf J).obj (op (unop X)))) :
      J.yoneda.obj (unop Y) ⟶ F)
    (J.yoneda.map f.unop ≫
        (Equiv.symm J.yonedaEquiv : (a : F.obj.obj (op (unop X))) → J.yoneda.obj (unop X) ⟶ F)
          ((J.yonedaEquiv : (a : J.yoneda.obj (unop X) ⟶ F) → F.obj.obj (op (unop X))) u) :
      J.yoneda.obj (unop Y) ⟶ F)

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

Premises used: Equiv.symm_apply_apply, CategoryTheory.GrothendieckTopology.yonedaEquiv_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 v)
f g : P ⟶ Q
h : ∀ (X : C) (p : J.yoneda.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 v)
f g : P ⟶ Q
h : ∀ (X : C) (p : J.yoneda.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 [yonedaEquiv_comp, Equiv.apply_symm_apply]
    using congr_arg (J.yonedaEquiv) (h _ (J.yonedaEquiv.symm x))

Premises used: Equiv.apply_symm_apply, CategoryTheory.GrothendieckTopology.yonedaEquiv, CategoryTheory.GrothendieckTopology.yonedaEquiv_comp, congr_arg, Equiv.symm, DFunLike.coe
-- 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'))
f : (uliftYoneda.{v', v, u} J).obj X ⟶ F
⊢ 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)) f :
      F.obj (P := Presheaf.IsSheaf J).obj (op X))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (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) (F.obj.obj (op X)))
        { down := 𝟙 X } :
      (fun (X : Type (max v v')) ↦ X) (F.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 : C
F : Sheaf J (Type (max v v'))
x : F.obj (P := Presheaf.IsSheaf J).obj (op X)
Y : Cᵒᵖ
f : unop Y ⟶ X
⊢ Eq (α := F.obj (P := Presheaf.IsSheaf J).obj Y)
    (((@ConcreteCategory.hom _ types 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))
                Y) :
            TypeCat.Fun (ULift.{v', v} (unop Y ⟶ X)) (F.obj (P := Presheaf.IsSheaf J).obj Y)) :
          (a : ULift.{v', v} (unop Y ⟶ X)) → F.obj.obj Y)
        { down := f } :
      F.obj (P := Presheaf.IsSheaf J).obj Y)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.obj (P := Presheaf.IsSheaf J).map f.op) :
          (a : F.obj.obj (op X)) → F.obj.obj Y)
        x :
      F.obj (P := Presheaf.IsSheaf J).obj Y)

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 : Sheaf J (Type (max v v'))
f : (uliftYoneda.{v', v, u} J).obj X ⟶ F
g : Y ⟶ X
change :
  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)))
⊢ Eq (α := (fun (X : Type (max v v')) ↦ X) (F.obj (P := Presheaf.IsSheaf J).obj (op Y)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.obj (P := Presheaf.IsSheaf J).map g.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 Y)))
        ((J.uliftYonedaEquiv : (a : (uliftYoneda.{v', v, u} J).obj X ⟶ F) → F.obj.obj (op X)) f) :
      (fun (X : Type (max v v')) ↦ X) (F.obj (P := Presheaf.IsSheaf J).obj (op Y)))
    ((J.uliftYonedaEquiv : (a : (uliftYoneda.{v', v, u} J).obj Y ⟶ F) → F.obj.obj (op Y))
        ((uliftYoneda.{v', v, u} J).map g ≫ f) :
      F.obj (P := Presheaf.IsSheaf J).obj (op Y))

Tactic:
change (f.hom.app (op X) ≫ F.obj.map g.op) ⟨𝟙 X⟩ = f.hom.app (op Y) ⟨𝟙 Y ≫ g⟩

Premises used: CategoryTheory.ConcreteCategory.hom, Quiver.Hom.op, CategoryTheory.CategoryStruct.id, CategoryTheory.ObjectProperty.FullSubcategory.obj, CategoryTheory.Functor.map, Opposite.op, CategoryTheory.CategoryStruct.comp, CategoryTheory.InducedCategory.Hom.hom, ULift.up, DFunLike.coe, CategoryTheory.NatTrans.app