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 : X ⟶ Y
F : Sheaf J (Type v)
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)
have 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)
Tactic: rw [yonedaEquiv_naturality', Equiv.symm_apply_apply, Equiv.symm_apply_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 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)
⊢ 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)
have 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)
Tactic: rw [yonedaEquiv_naturality', Equiv.symm_apply_apply, Equiv.symm_apply_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 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)
⊢ 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)
have rw₂ : J.yoneda.map f.unop ≫ u = J.yoneda.map f.unop ≫ u
Tactic: rw [yonedaEquiv_naturality', Equiv.symm_apply_apply, Equiv.symm_apply_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
P Q : Sheaf J (Type v)
f g : P ⟶ Q
h : ∀ (X : C) (p : J.yoneda.obj X ⟶ P), p ≫ f = p ≫ g
⊢ f = g
have 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
Tactic: ext X x
-- 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 (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) (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))
have 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)))
Tactic: change (f.hom.app (op X) ≫ F.obj.map g.op) ⟨𝟙 X⟩ = f.hom.app (op Y) ⟨𝟙 Y ≫ g⟩
-- 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 (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) (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)))
have 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)))
Tactic: rw [← f.hom.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.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)) }
have 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)) }
Tactic: rw [uliftYonedaEquiv_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 (max v v'))
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))
have 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'))
Tactic: apply J.uliftYonedaEquiv.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 (max v v'))
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'))
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.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: simp only [uliftYonedaEquiv_comp, Equiv.apply_symm_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 (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'))
        ((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'))
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.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: rw [uliftYonedaEquiv_uliftYoneda_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 : C
F F' : Sheaf J (Type (max v v'))
f : F ⟶ F'
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')
have 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))
Tactic: apply J.uliftYonedaEquiv.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 (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) (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)))
    ((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 := g } :
      (fun (X : Type (max v v')) ↦ X) (F.obj (P := Presheaf.IsSheaf J).obj (op Y)))
have rw : Eq (α := (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))
  ((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 := g } :
    (fun (X : Type (max v v')) ↦ X) (F.obj (P := Presheaf.IsSheaf J).obj (op Y)))
Tactic: rw [uliftYonedaEquiv_naturality, uliftYonedaEquiv_comp, uliftYonedaEquiv_uliftYoneda_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 (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)))
    ((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))
    ((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 := 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)))
    ((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 := g } :
      (fun (X : Type (max v v')) ↦ X) (F.obj (P := Presheaf.IsSheaf J).obj (op Y)))
have rw₁ : 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 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)))
      ((J.uliftYonedaEquiv :
          (a : (uliftYoneda.{v', v, u} J).obj Y ⟶ (uliftYoneda.{v', v, u} J).obj X) →
            ((uliftYoneda.{v', v, u} J).obj X).obj.obj (op Y))
        ((uliftYoneda.{v', v, u} J).map g)) :
    (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 := g } :
    (fun (X : Type (max v v')) ↦ X) (F.obj (P := Presheaf.IsSheaf J).obj (op Y)))
Tactic: rw [uliftYonedaEquiv_naturality, uliftYonedaEquiv_comp, uliftYonedaEquiv_uliftYoneda_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 (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))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.hom.app Y) :
          (a : (fun (X : Type (max v v')) ↦ X) (((uliftYoneda.{v', v, u} J).obj (unop X)).obj.obj Y)) →
            (fun (X : Type (max v v')) ↦ X) (F.obj.obj Y))
        { down := g.unop } :
      (fun (X : Type (max v v')) ↦ X) (F.obj (P := Presheaf.IsSheaf J).obj Y))
have rw : Eq (α := (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)))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.hom.app Y) :
        (a : (fun (X : Type (max v v')) ↦ X) (((uliftYoneda.{v', v, u} J).obj (unop X)).obj.obj Y)) →
          (fun (X : Type (max v v')) ↦ X) (F.obj.obj Y))
      { down := g.unop } :
    (fun (X : Type (max v v')) ↦ X) (F.obj (P := Presheaf.IsSheaf J).obj Y))
Tactic: rw [uliftYonedaEquiv_naturality', uliftYonedaEquiv_comp, uliftYonedaEquiv_uliftYoneda_map]