awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Subcanonical (goal)
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
⊢ 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)))
    ((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))
have simp : Eq (α := obj CategoryTheory.yoneda Y ⟶ F.obj (P := Presheaf.IsSheaf J))
  (map CategoryTheory.yoneda g ≫
    (FullyFaithful.homEquiv (fullyFaithfulSheafToPresheaf J (Type v)) :
        (a : J.yoneda.obj X ⟶ F) → CategoryTheory.yoneda.obj X ⟶ F.obj)
      f)
  ((FullyFaithful.homEquiv (fullyFaithfulSheafToPresheaf J (Type v)) :
      (a : J.yoneda.obj Y ⟶ F) → CategoryTheory.yoneda.obj Y ⟶ F.obj)
    (J.yoneda.map g ≫ f))
Tactic: simp [yonedaEquiv, CategoryTheory.yonedaEquiv_naturality]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Subcanonical (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
inst_1 : J.Subcanonical
X Y : C
f : X ⟶ Y
⊢ (J.yonedaEquiv : (a : J.yoneda.obj X ⟶ J.yoneda.obj Y) → (J.yoneda.obj Y).obj.obj (op X)) (J.yoneda.map f) = f
have 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
Tactic: rw [yonedaEquiv_apply]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Subcanonical (goal)
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 (α := 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))
have 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'))
Tactic: apply J.yonedaEquiv.injective
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Subcanonical (goal)
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.{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'))
have 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'))
Tactic: rw [yonedaEquiv_comp, yonedaEquiv_yoneda_map]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Subcanonical (goal)
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 (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'))
have 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'))
Tactic: simp
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Subcanonical (goal)
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 (α := 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')
have 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))
Tactic: apply J.yonedaEquiv.injective
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Subcanonical (goal)
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
⊢ 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)))
have 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)))
Tactic: rw [yonedaEquiv_naturality, yonedaEquiv_comp, yonedaEquiv_yoneda_map]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Subcanonical (goal)
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)))
⊢ 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)))
have 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)))
Tactic: rw [yonedaEquiv_naturality, yonedaEquiv_comp, yonedaEquiv_yoneda_map]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Subcanonical (goal)
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)))
⊢ 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)))
have 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)))
Tactic: rw [yonedaEquiv_naturality, yonedaEquiv_comp, yonedaEquiv_yoneda_map]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Subcanonical (goal)
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))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.hom.app Y) :
          (a : (fun (X : Type v) ↦ X) ((J.yoneda.obj (unop X)).obj.obj Y)) → (fun (X : Type v) ↦ X) (F.obj.obj Y))
        g.unop :
      (fun (X : Type v) ↦ X) (F.obj (P := Presheaf.IsSheaf J).obj Y))
have rw : Eq.{v + 1} (α := (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)))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.hom.app Y) :
        (a : (fun (X : Type v) ↦ X) ((J.yoneda.obj (unop X)).obj.obj Y)) → (fun (X : Type v) ↦ X) (F.obj.obj Y))
      g.unop :
    (fun (X : Type v) ↦ X) (F.obj (P := Presheaf.IsSheaf J).obj Y))
Tactic: rw [yonedaEquiv_naturality', yonedaEquiv_comp, yonedaEquiv_yoneda_map]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Subcanonical (goal)
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
rw :
  Eq.{v + 1} (α := (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)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.hom.app Y) :
          (a : (fun (X : Type v) ↦ X) ((J.yoneda.obj (unop X)).obj.obj Y)) → (fun (X : Type v) ↦ X) (F.obj.obj Y))
        g.unop :
      (fun (X : Type v) ↦ X) (F.obj (P := Presheaf.IsSheaf J).obj 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))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.hom.app Y) :
          (a : (fun (X : Type v) ↦ X) ((J.yoneda.obj (unop X)).obj.obj Y)) → (fun (X : Type v) ↦ X) (F.obj.obj Y))
        g.unop :
      (fun (X : Type v) ↦ X) (F.obj (P := Presheaf.IsSheaf J).obj Y))
have rw₁ : Eq (α := (fun (X : Type v) ↦ X) (F.obj (P := Presheaf.IsSheaf J).obj Y))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.hom.app (op (unop Y))) :
        (a : (fun (X : Type v) ↦ X) ((J.yoneda.obj (unop X)).obj.obj (op (unop Y)))) →
          (fun (X : Type v) ↦ X) (F.obj.obj (op (unop Y))))
      ((J.yonedaEquiv :
            (a : J.yoneda.obj (unop Y) ⟶ J.yoneda.obj (unop X)) → (J.yoneda.obj (unop X)).obj.obj (op (unop Y)))
          (J.yoneda.map g.unop) :
        (J.yoneda.obj (unop X)).obj (P := Presheaf.IsSheaf J).obj (op (unop Y))) :
    (fun (X : Type v) ↦ X) (F.obj (P := Presheaf.IsSheaf J).obj (op (unop Y))))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.hom.app Y) :
        (a : (fun (X : Type v) ↦ X) ((J.yoneda.obj (unop X)).obj.obj Y)) → (fun (X : Type v) ↦ X) (F.obj.obj Y))
      g.unop :
    (fun (X : Type v) ↦ X) (F.obj (P := Presheaf.IsSheaf J).obj Y))
Tactic: rw [yonedaEquiv_naturality', yonedaEquiv_comp, yonedaEquiv_yoneda_map]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Subcanonical (goal)
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
rw :
  Eq.{v + 1} (α := (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)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.hom.app Y) :
          (a : (fun (X : Type v) ↦ X) ((J.yoneda.obj (unop X)).obj.obj Y)) → (fun (X : Type v) ↦ X) (F.obj.obj Y))
        g.unop :
      (fun (X : Type v) ↦ X) (F.obj (P := Presheaf.IsSheaf J).obj Y))
rw₁ :
  Eq (α := (fun (X : Type v) ↦ X) (F.obj (P := Presheaf.IsSheaf J).obj Y))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.hom.app (op (unop Y))) :
          (a : (fun (X : Type v) ↦ X) ((J.yoneda.obj (unop X)).obj.obj (op (unop Y)))) →
            (fun (X : Type v) ↦ X) (F.obj.obj (op (unop Y))))
        ((J.yonedaEquiv :
              (a : J.yoneda.obj (unop Y) ⟶ J.yoneda.obj (unop X)) → (J.yoneda.obj (unop X)).obj.obj (op (unop Y)))
            (J.yoneda.map g.unop) :
          (J.yoneda.obj (unop X)).obj (P := Presheaf.IsSheaf J).obj (op (unop Y))) :
      (fun (X : Type v) ↦ X) (F.obj (P := Presheaf.IsSheaf J).obj (op (unop Y))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.hom.app Y) :
          (a : (fun (X : Type v) ↦ X) ((J.yoneda.obj (unop X)).obj.obj Y)) → (fun (X : Type v) ↦ X) (F.obj.obj Y))
        g.unop :
      (fun (X : Type v) ↦ X) (F.obj (P := Presheaf.IsSheaf J).obj 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))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.hom.app Y) :
          (a : (fun (X : Type v) ↦ X) ((J.yoneda.obj (unop X)).obj.obj Y)) → (fun (X : Type v) ↦ X) (F.obj.obj Y))
        g.unop :
      (fun (X : Type v) ↦ X) (F.obj (P := Presheaf.IsSheaf J).obj Y))
have rw₂ : Eq (α := (fun (X : Type v) ↦ X) (F.obj (P := Presheaf.IsSheaf J).obj Y))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.hom.app (op (unop Y))) :
        (a : (fun (X : Type v) ↦ X) ((J.yoneda.obj (unop X)).obj.obj (op (unop Y)))) →
          (fun (X : Type v) ↦ X) (F.obj.obj (op (unop Y))))
      g.unop :
    (fun (X : Type v) ↦ X) (F.obj (P := Presheaf.IsSheaf J).obj (op (unop Y))))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.hom.app Y) :
        (a : (fun (X : Type v) ↦ X) ((J.yoneda.obj (unop X)).obj.obj Y)) → (fun (X : Type v) ↦ X) (F.obj.obj Y))
      g.unop :
    (fun (X : Type v) ↦ X) (F.obj (P := Presheaf.IsSheaf J).obj Y))
Tactic: rw [yonedaEquiv_naturality', yonedaEquiv_comp, yonedaEquiv_yoneda_map]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Subcanonical (goal)
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
⊢ 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)
have 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)
Tactic: obtain ⟨u, rfl⟩ := J.yonedaEquiv.surjective t
Cleared hypotheses: t