awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Sites.Types
Goal:
S₁ S₂ : Sheaf typesGrothendieckTopology (Type u)
f : S₁ ⟶ S₂
α : Type u
s : S₁.obj (P := Presheaf.IsSheaf typesGrothendieckTopology).obj (op α)
x : α
⊢ Eq (α := (fun (X : Type u) ↦ X) (S₂.obj (P := Presheaf.IsSheaf typesGrothendieckTopology).obj (op PUnit.{u + 1})))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (eval (S₂.obj (P := Presheaf.IsSheaf typesGrothendieckTopology)) α
              ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.hom.app (op α)) :
                  (a : (fun (X : Type u) ↦ X) (S₁.obj.obj (op α))) → (fun (X : Type u) ↦ X) (S₂.obj.obj (op α)))
                s)) :
          (a : (fun (X : Type u) ↦ X) α) → (fun (X : Type u) ↦ X) (S₂.obj.obj (op PUnit.{u + 1})))
        x :
      (fun (X : Type u) ↦ X) (S₂.obj (P := Presheaf.IsSheaf typesGrothendieckTopology).obj (op PUnit.{u + 1})))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.hom.app (op PUnit.{u + 1})) :
          (a : (fun (X : Type u) ↦ X) (S₁.obj.obj (op PUnit.{u + 1}))) →
            (fun (X : Type u) ↦ X) (S₂.obj.obj (op PUnit.{u + 1})))
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
                (eval (S₁.obj (P := Presheaf.IsSheaf typesGrothendieckTopology)) α s) :
              (a : (fun (X : Type u) ↦ X) α) → (fun (X : Type u) ↦ X) (S₁.obj.obj (op PUnit.{u + 1})))
            x :
          (fun (X : Type u) ↦ X) (S₁.obj (P := Presheaf.IsSheaf typesGrothendieckTopology).obj (op PUnit.{u + 1}))) :
      (fun (X : Type u) ↦ X) (S₂.obj (P := Presheaf.IsSheaf typesGrothendieckTopology).obj (op PUnit.{u + 1})))

Tactic:
(ConcreteCategory.congr_hom (f.hom.naturality (↾fun _ => x).op) s).symm

Premises used: Quiver.Hom.op, TypeCat.ofHom, CategoryTheory.NatTrans.naturality, CategoryTheory.ConcreteCategory.congr_hom, CategoryTheory.InducedCategory.Hom.hom, Eq.symm
-- Module: Mathlib.CategoryTheory.Sites.Types
Goal:
S₁ S₂ : Sheaf typesGrothendieckTopology (Type u)
f : S₁ ⟶ S₂
h :
  ∀ (α : Type u)
    (s :
      (Functor.obj (𝟭 (Sheaf typesGrothendieckTopology (Type u))) S₁).obj (P :=
            Presheaf.IsSheaf typesGrothendieckTopology).obj
        (op α)),
    TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (NatTrans.app
            (InducedCategory.Hom.hom
              (Functor.map (𝟭 (Sheaf typesGrothendieckTopology (Type u))) f ≫
                Iso.hom ((fun (S : Sheaf typesGrothendieckTopology (Type u)) ↦ equivYoneda' S) S₂)))
            (op α)))
        s =
      TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (NatTrans.app
            (InducedCategory.Hom.hom
              (Iso.hom ((fun (S : Sheaf typesGrothendieckTopology (Type u)) ↦ equivYoneda' S) S₁) ≫
                ((sheafToPresheaf typesGrothendieckTopology (Type u) ⋙
                        Functor.obj (evaluation Type uᵒᵖ (Type u)) (op PUnit.{u + 1})) ⋙
                      yoneda').map
                  f))
            (op α)))
        s
⊢ Eq (α :=
    Functor.obj (𝟭 (Sheaf typesGrothendieckTopology (Type u))) S₁ ⟶
      ((sheafToPresheaf typesGrothendieckTopology (Type u) ⋙
              Functor.obj (evaluation Type uᵒᵖ (Type u)) (op PUnit.{u + 1})) ⋙
            yoneda').obj
        S₂)
    (Functor.map (𝟭 (Sheaf typesGrothendieckTopology (Type u))) f ≫
      Iso.hom ((fun (S : Sheaf typesGrothendieckTopology (Type u)) ↦ equivYoneda' S) S₂))
    (Iso.hom ((fun (S : Sheaf typesGrothendieckTopology (Type u)) ↦ equivYoneda' S) S₁) ≫
      ((sheafToPresheaf typesGrothendieckTopology (Type u) ⋙
              Functor.obj (evaluation Type uᵒᵖ (Type u)) (op PUnit.{u + 1})) ⋙
            yoneda').map
        f)

Tactic:
ext ⟨α⟩ s
-- Module: Mathlib.CategoryTheory.Sites.Types
Goal:
S₁ S₂ : Sheaf typesGrothendieckTopology (Type u)
f : S₁ ⟶ S₂
α : Type u
s :
  (Functor.obj (𝟭 (Sheaf typesGrothendieckTopology (Type u))) S₁).obj (P :=
        Presheaf.IsSheaf typesGrothendieckTopology).obj
    (op α)
h :
  Eq (α := α ⟶ S₂.obj (P := Presheaf.IsSheaf typesGrothendieckTopology).obj (op PUnit.{u + 1}))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            ((equivYoneda (S₂.obj (P := Presheaf.IsSheaf typesGrothendieckTopology)) ⋯).hom.app (op α)) :
          (a : S₂.obj.obj (op α)) → α ⟶ S₂.obj.obj (op PUnit.{u + 1}))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.hom.app (op α)) : (a : S₁.obj.obj (op α)) → S₂.obj.obj (op α)) s :
          S₂.obj (P := Presheaf.IsSheaf typesGrothendieckTopology).obj (op α)) :
      α ⟶ S₂.obj (P := Presheaf.IsSheaf typesGrothendieckTopology).obj (op PUnit.{u + 1}))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
              ((equivYoneda (S₁.obj (P := Presheaf.IsSheaf typesGrothendieckTopology)) ⋯).hom.app (op α)) :
            (a : S₁.obj.obj (op α)) → α ⟶ S₁.obj.obj (op PUnit.{u + 1}))
          s ≫
        f.hom.app (op PUnit.{u + 1}) :
      α ⟶ S₂.obj (P := Presheaf.IsSheaf typesGrothendieckTopology).obj (op PUnit.{u + 1}))
⊢ TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (NatTrans.app
          (InducedCategory.Hom.hom
            (Functor.map (𝟭 (Sheaf typesGrothendieckTopology (Type u))) f ≫
              Iso.hom ((fun (S : Sheaf typesGrothendieckTopology (Type u)) ↦ equivYoneda' S) S₂)))
          (op α)))
      s =
    TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (NatTrans.app
          (InducedCategory.Hom.hom
            (Iso.hom ((fun (S : Sheaf typesGrothendieckTopology (Type u)) ↦ equivYoneda' S) S₁) ≫
              ((sheafToPresheaf typesGrothendieckTopology (Type u) ⋙
                      Functor.obj (evaluation Type uᵒᵖ (Type u)) (op PUnit.{u + 1})) ⋙
                    yoneda').map
                f))
          (op α)))
      s

Tactic:
dsimp at s ⊢
-- Module: Mathlib.CategoryTheory.Sites.Types
Goal:
S₁ S₂ : Sheaf typesGrothendieckTopology (Type u)
f : S₁ ⟶ S₂
α : Type u
s : S₁.obj (P := Presheaf.IsSheaf typesGrothendieckTopology).obj (op α)
h :
  ∀ (x : α),
    Eq (α := S₂.obj (P := Presheaf.IsSheaf typesGrothendieckTopology).obj (op PUnit.{u + 1}))
      (TypeCat.Fun.toFun
        (@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
          ((ConcreteCategory.hom (FC := TypeCat.Fun)
                ((equivYoneda (S₂.obj (P := Presheaf.IsSheaf typesGrothendieckTopology)) ⋯).hom.app (op α)) :
              (a : S₂.obj.obj (op α)) → α ⟶ S₂.obj.obj (op PUnit.{u + 1}))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.hom.app (op α)) : (a : S₁.obj.obj (op α)) → S₂.obj.obj (op α))
                s :
              S₂.obj (P := Presheaf.IsSheaf typesGrothendieckTopology).obj (op α))))
        x)
      (TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          ((ConcreteCategory.hom (FC := TypeCat.Fun)
                  ((equivYoneda (S₁.obj (P := Presheaf.IsSheaf typesGrothendieckTopology)) ⋯).hom.app (op α)) :
                (a : S₁.obj.obj (op α)) → α ⟶ S₁.obj.obj (op PUnit.{u + 1}))
              s ≫
            f.hom.app (op PUnit.{u + 1})))
        x)
⊢ Eq (α := α ⟶ S₂.obj (P := Presheaf.IsSheaf typesGrothendieckTopology).obj (op PUnit.{u + 1}))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            ((equivYoneda (S₂.obj (P := Presheaf.IsSheaf typesGrothendieckTopology)) ⋯).hom.app (op α)) :
          (a : S₂.obj.obj (op α)) → α ⟶ S₂.obj.obj (op PUnit.{u + 1}))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.hom.app (op α)) : (a : S₁.obj.obj (op α)) → S₂.obj.obj (op α)) s :
          S₂.obj (P := Presheaf.IsSheaf typesGrothendieckTopology).obj (op α)) :
      α ⟶ S₂.obj (P := Presheaf.IsSheaf typesGrothendieckTopology).obj (op PUnit.{u + 1}))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
              ((equivYoneda (S₁.obj (P := Presheaf.IsSheaf typesGrothendieckTopology)) ⋯).hom.app (op α)) :
            (a : S₁.obj.obj (op α)) → α ⟶ S₁.obj.obj (op PUnit.{u + 1}))
          s ≫
        f.hom.app (op PUnit.{u + 1}) :
      α ⟶ S₂.obj (P := Presheaf.IsSheaf typesGrothendieckTopology).obj (op PUnit.{u + 1}))

Tactic:
ext x
-- Module: Mathlib.CategoryTheory.Sites.Types
Goal:
S₁ S₂ : Sheaf typesGrothendieckTopology (Type u)
f : S₁ ⟶ S₂
α : Type u
s : S₁.obj (P := Presheaf.IsSheaf typesGrothendieckTopology).obj (op α)
x : α
⊢ Eq (α := S₂.obj (P := Presheaf.IsSheaf typesGrothendieckTopology).obj (op PUnit.{u + 1}))
    (TypeCat.Fun.toFun
      (@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
              ((equivYoneda (S₂.obj (P := Presheaf.IsSheaf typesGrothendieckTopology)) ⋯).hom.app (op α)) :
            (a : S₂.obj.obj (op α)) → α ⟶ S₂.obj.obj (op PUnit.{u + 1}))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.hom.app (op α)) : (a : S₁.obj.obj (op α)) → S₂.obj.obj (op α))
              s :
            S₂.obj (P := Presheaf.IsSheaf typesGrothendieckTopology).obj (op α))))
      x)
    (TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
                ((equivYoneda (S₁.obj (P := Presheaf.IsSheaf typesGrothendieckTopology)) ⋯).hom.app (op α)) :
              (a : S₁.obj.obj (op α)) → α ⟶ S₁.obj.obj (op PUnit.{u + 1}))
            s ≫
          f.hom.app (op PUnit.{u + 1})))
      x)

Tactic:
eval_app S₁ S₂ f α s x

Premises used: CategoryTheory.eval_app
-- Module: Mathlib.CategoryTheory.Sites.Types
Goal:
S₁ S₂ : Sheaf typesGrothendieckTopology (Type u)
f : S₁ ⟶ S₂
α : Type u
s : S₁.obj (P := Presheaf.IsSheaf typesGrothendieckTopology).obj (op α)
x : α
⊢ Eq (α := S₂.obj (P := Presheaf.IsSheaf typesGrothendieckTopology).obj (op PUnit.{u + 1}))
    (TypeCat.Fun.toFun
      (@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
              ((equivYoneda (S₂.obj (P := Presheaf.IsSheaf typesGrothendieckTopology)) ⋯).hom.app (op α)) :
            (a : S₂.obj.obj (op α)) → α ⟶ S₂.obj.obj (op PUnit.{u + 1}))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.hom.app (op α)) : (a : S₁.obj.obj (op α)) → S₂.obj.obj (op α))
              s :
            S₂.obj (P := Presheaf.IsSheaf typesGrothendieckTopology).obj (op α))))
      x)
    (TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
                ((equivYoneda (S₁.obj (P := Presheaf.IsSheaf typesGrothendieckTopology)) ⋯).hom.app (op α)) :
              (a : S₁.obj.obj (op α)) → α ⟶ S₁.obj.obj (op PUnit.{u + 1}))
            s ≫
          f.hom.app (op PUnit.{u + 1})))
      x)

Tactic:
exact eval_app S₁ S₂ f α s x

Premises used: CategoryTheory.eval_app
-- Module: Mathlib.CategoryTheory.Sites.Types
Goal:
X : Type u
h :
  InducedCategory.Hom.hom
      (CategoryStruct.comp (Y :=
        yoneda'.obj
          (Functor.obj
            (sheafToPresheaf typesGrothendieckTopology (Type u) ⋙
              Functor.obj (evaluation Type uᵒᵖ (Type u)) (op PUnit.{u + 1}))
            (yoneda'.obj X)))
        (yoneda'.map
          (NatTrans.app
            (Iso.hom
              (NatIso.ofComponents
                (fun (_α : Type u) ↦
                  { hom := ↾fun (x : _α) ↦ ↾fun (x_1 : PUnit.{u + 1}) ↦ x,
                    inv := ↾fun (f : PUnit.{u + 1} ⟶ _α) ↦ (TypeCat.Hom.hom f : (a : PUnit.{u + 1}) → _α) PUnit.unit,
                    hom_inv_id := ⋯, inv_hom_id := ⋯ })
                ⋯))
            X))
        (NatTrans.app
          (Iso.hom
            (Iso.symm (NatIso.ofComponents (fun (S : Sheaf typesGrothendieckTopology (Type u)) ↦ equivYoneda' S) ⋯)))
          (yoneda'.obj X))) =
    InducedCategory.Hom.hom (𝟙 (yoneda'.obj X))
⊢ Eq (α := yoneda'.obj X ⟶ yoneda'.obj X)
    (CategoryStruct.comp (Y :=
        yoneda'.obj
          (Functor.obj
            (sheafToPresheaf typesGrothendieckTopology (Type u) ⋙
              Functor.obj (evaluation Type uᵒᵖ (Type u)) (op PUnit.{u + 1}))
            (yoneda'.obj X)))
        (yoneda'.map
          (NatTrans.app
            (Iso.hom
              (NatIso.ofComponents
                (fun (_α : Type u) ↦
                  { hom := ↾fun (x : _α) ↦ ↾fun (x_1 : PUnit.{u + 1}) ↦ x,
                    inv := ↾fun (f : PUnit.{u + 1} ⟶ _α) ↦ (TypeCat.Hom.hom f : (a : PUnit.{u + 1}) → _α) PUnit.unit,
                    hom_inv_id := ⋯, inv_hom_id := ⋯ })
                ⋯))
            X))
        (NatTrans.app
          (Iso.hom
            (Iso.symm (NatIso.ofComponents (fun (S : Sheaf typesGrothendieckTopology (Type u)) ↦ equivYoneda' S) ⋯)))
          (yoneda'.obj X)) :
      yoneda'.obj X ⟶ yoneda'.obj X)
    (𝟙 (yoneda'.obj X) : yoneda'.obj X ⟶ yoneda'.obj X)

Tactic:
ext1
-- Module: Mathlib.CategoryTheory.Sites.Types
Goal:
X : Type u
h :
  Eq (α := (yoneda'.obj X).obj (P := Presheaf.IsSheaf typesGrothendieckTopology).obj (op X))
    ((yonedaEquiv : (a : yoneda.obj X ⟶ (yoneda'.obj X).obj) → (yoneda'.obj X).obj.obj (op X))
        (InducedCategory.Hom.hom
          (CategoryStruct.comp (Y :=
            yoneda'.obj
              (Functor.obj
                (sheafToPresheaf typesGrothendieckTopology (Type u) ⋙
                  Functor.obj (evaluation Type uᵒᵖ (Type u)) (op PUnit.{u + 1}))
                (yoneda'.obj X)))
            (yoneda'.map
              (NatTrans.app
                (Iso.hom
                  (NatIso.ofComponents
                    (fun (_α : Type u) ↦
                      { hom := ↾fun (x : _α) ↦ ↾fun (x_1 : PUnit.{u + 1}) ↦ x,
                        inv :=
                          ↾fun (f : PUnit.{u + 1} ⟶ _α) ↦ (TypeCat.Hom.hom f : (a : PUnit.{u + 1}) → _α) PUnit.unit,
                        hom_inv_id := ⋯, inv_hom_id := ⋯ })
                    ⋯))
                X))
            (NatTrans.app
              (Iso.hom
                (Iso.symm
                  (NatIso.ofComponents (fun (S : Sheaf typesGrothendieckTopology (Type u)) ↦ equivYoneda' S) ⋯)))
              (yoneda'.obj X)))) :
      (yoneda'.obj X).obj (P := Presheaf.IsSheaf typesGrothendieckTopology).obj (op X))
    ((yonedaEquiv : (a : yoneda.obj X ⟶ (yoneda'.obj X).obj) → (yoneda'.obj X).obj.obj (op X))
        (InducedCategory.Hom.hom (𝟙 (yoneda'.obj X))) :
      (yoneda'.obj X).obj (P := Presheaf.IsSheaf typesGrothendieckTopology).obj (op X))
⊢ InducedCategory.Hom.hom
      (CategoryStruct.comp (Y :=
        yoneda'.obj
          (Functor.obj
            (sheafToPresheaf typesGrothendieckTopology (Type u) ⋙
              Functor.obj (evaluation Type uᵒᵖ (Type u)) (op PUnit.{u + 1}))
            (yoneda'.obj X)))
        (yoneda'.map
          (NatTrans.app
            (Iso.hom
              (NatIso.ofComponents
                (fun (_α : Type u) ↦
                  { hom := ↾fun (x : _α) ↦ ↾fun (x_1 : PUnit.{u + 1}) ↦ x,
                    inv := ↾fun (f : PUnit.{u + 1} ⟶ _α) ↦ (TypeCat.Hom.hom f : (a : PUnit.{u + 1}) → _α) PUnit.unit,
                    hom_inv_id := ⋯, inv_hom_id := ⋯ })
                ⋯))
            X))
        (NatTrans.app
          (Iso.hom
            (Iso.symm (NatIso.ofComponents (fun (S : Sheaf typesGrothendieckTopology (Type u)) ↦ equivYoneda' S) ⋯)))
          (yoneda'.obj X))) =
    InducedCategory.Hom.hom (𝟙 (yoneda'.obj X))

Tactic:
apply yonedaEquiv.injective

Premises used: Equiv.injective, CategoryTheory.yonedaEquiv
-- Module: Mathlib.CategoryTheory.Sites.Types
Goal:
X : Type u
h :
  Eq (α := X ⟶ X)
    (typesGlue (Functor.obj yoneda X) ⋯ X
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (𝟙 X ≫ ↾fun (x : X) ↦ ↾fun (x_1 : PUnit.{u + 1}) ↦ x)) :
          (a : X) → PUnit.{u + 1} ⟶ X) :
      Functor.obj (Functor.obj yoneda X) (op X))
    (𝟙 X : X ⟶ X)
⊢ Eq (α := (yoneda'.obj X).obj (P := Presheaf.IsSheaf typesGrothendieckTopology).obj (op X))
    ((yonedaEquiv : (a : yoneda.obj X ⟶ (yoneda'.obj X).obj) → (yoneda'.obj X).obj.obj (op X))
        (InducedCategory.Hom.hom
          (CategoryStruct.comp (Y :=
            yoneda'.obj
              (Functor.obj
                (sheafToPresheaf typesGrothendieckTopology (Type u) ⋙
                  Functor.obj (evaluation Type uᵒᵖ (Type u)) (op PUnit.{u + 1}))
                (yoneda'.obj X)))
            (yoneda'.map
              (NatTrans.app
                (Iso.hom
                  (NatIso.ofComponents
                    (fun (_α : Type u) ↦
                      { hom := ↾fun (x : _α) ↦ ↾fun (x_1 : PUnit.{u + 1}) ↦ x,
                        inv :=
                          ↾fun (f : PUnit.{u + 1} ⟶ _α) ↦ (TypeCat.Hom.hom f : (a : PUnit.{u + 1}) → _α) PUnit.unit,
                        hom_inv_id := ⋯, inv_hom_id := ⋯ })
                    ⋯))
                X))
            (NatTrans.app
              (Iso.hom
                (Iso.symm
                  (NatIso.ofComponents (fun (S : Sheaf typesGrothendieckTopology (Type u)) ↦ equivYoneda' S) ⋯)))
              (yoneda'.obj X)))) :
      (yoneda'.obj X).obj (P := Presheaf.IsSheaf typesGrothendieckTopology).obj (op X))
    ((yonedaEquiv : (a : yoneda.obj X ⟶ (yoneda'.obj X).obj) → (yoneda'.obj X).obj.obj (op X))
        (InducedCategory.Hom.hom (𝟙 (yoneda'.obj X))) :
      (yoneda'.obj X).obj (P := Presheaf.IsSheaf typesGrothendieckTopology).obj (op X))

Tactic:
dsimp [yoneda', yonedaEquiv, equivYoneda, evalEquiv]

Premises used: CategoryTheory.evalEquiv, CategoryTheory.yoneda', CategoryTheory.yonedaEquiv, CategoryTheory.equivYoneda
-- Module: Mathlib.CategoryTheory.Sites.Types
Goal:
X : Type u
⊢ Eq (α := X ⟶ X)
    (typesGlue (Functor.obj yoneda X) ⋯ X
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (𝟙 X ≫ ↾fun (x : X) ↦ ↾fun (x_1 : PUnit.{u + 1}) ↦ x)) :
          (a : X) → PUnit.{u + 1} ⟶ X) :
      Functor.obj (Functor.obj yoneda X) (op X))
    (𝟙 X : X ⟶ X)

Tactic:
simpa using typesGlue_eval (S := yoneda.obj X) (𝟙 X)

Premises used: CategoryTheory.typesGlue_eval, CategoryTheory.CategoryStruct.id
-- Module: Mathlib.CategoryTheory.Sites.Types
Goal:
⊢ typesGrothendieckTopology.Subcanonical

Tactic:
GrothendieckTopology.Subcanonical.of_isSheaf_yoneda_obj _ fun _ => Presieve.isSheaf_yoneda'

Premises used: CategoryTheory.GrothendieckTopology.Subcanonical.of_isSheaf_yoneda_obj, CategoryTheory.Presieve.isSheaf_yoneda'
-- Module: Mathlib.CategoryTheory.Sites.Types
Goal:
⊢ typesGrothendieckTopology = Sheaf.canonicalTopology (Type u)

Tactic:
le_antisymm typesGrothendieckTopology.le_canonical (sInf_le ?_)

Premises used: CategoryTheory.typesGrothendieckTopology, le_antisymm, sInf_le, CategoryTheory.GrothendieckTopology.le_canonical
-- Module: Mathlib.CategoryTheory.Sites.Types
Goal:
refine :
  Membership.mem (γ := Set (GrothendieckTopology (Type u)))
    (Sheaf.finestTopologySingle '' Set.range (Functor.obj yoneda)) typesGrothendieckTopology
⊢ typesGrothendieckTopology = Sheaf.canonicalTopology (Type u)

Tactic:
refine le_antisymm typesGrothendieckTopology.le_canonical (sInf_le ?_)

Premises used: CategoryTheory.typesGrothendieckTopology, le_antisymm, sInf_le, CategoryTheory.GrothendieckTopology.le_canonical
-- Module: Mathlib.CategoryTheory.Sites.Types
Goal:
⊢ Membership.mem (γ := Set (GrothendieckTopology (Type u)))
    (Sheaf.finestTopologySingle '' Set.range (Functor.obj yoneda)) typesGrothendieckTopology

Tactic:
⟨yoneda.obj (ULift Bool), ⟨_, rfl⟩, GrothendieckTopology.ext ?_⟩

Premises used: Set.Mem, setOf, ULift, CategoryTheory.yoneda, CategoryTheory.GrothendieckTopology.ext, And.intro, Exists.intro, Bool, Set.image, CategoryTheory.Functor.obj, rfl
-- Module: Mathlib.CategoryTheory.Sites.Types
Goal:
refine :
  (⇑(Sheaf.finestTopologySingle (Functor.obj yoneda (ULift.{u, 0} Bool))) : (a : Type u) → Set (Sieve a)) =
    (⇑typesGrothendieckTopology : (a : Type u) → Set (Sieve a))
⊢ Membership.mem (γ := Set (GrothendieckTopology (Type u)))
    (Sheaf.finestTopologySingle '' Set.range (Functor.obj yoneda)) typesGrothendieckTopology

Tactic:
refine ⟨yoneda.obj (ULift Bool), ⟨_, rfl⟩, GrothendieckTopology.ext ?_⟩
-- Module: Mathlib.CategoryTheory.Sites.Types
Goal:
h :
  ∀ (α : Type u),
    (Sheaf.finestTopologySingle (Functor.obj yoneda (ULift.{u, 0} Bool)) : (a : Type u) → Set (Sieve a)) α =
      (typesGrothendieckTopology : (a : Type u) → Set (Sieve a)) α
⊢ (⇑(Sheaf.finestTopologySingle (Functor.obj yoneda (ULift.{u, 0} Bool))) : (a : Type u) → Set (Sieve a)) =
    (⇑typesGrothendieckTopology : (a : Type u) → Set (Sieve a))

Tactic:
funext α
-- Module: Mathlib.CategoryTheory.Sites.Types
Goal:
α : Type u
h :
  ∀ (S : Sieve α),
    S ∈ (Sheaf.finestTopologySingle (Functor.obj yoneda (ULift.{u, 0} Bool)) : (a : Type u) → Set (Sieve a)) α ↔
      S ∈ (typesGrothendieckTopology : (a : Type u) → Set (Sieve a)) α
⊢ (Sheaf.finestTopologySingle (Functor.obj yoneda (ULift.{u, 0} Bool)) : (a : Type u) → Set (Sieve a)) α =
    (typesGrothendieckTopology : (a : Type u) → Set (Sieve a)) α

Tactic:
ext S
-- Module: Mathlib.CategoryTheory.Sites.Types
Goal:
α : Type u
S : Sieve α
⊢ S ∈ (Sheaf.finestTopologySingle (Functor.obj yoneda (ULift.{u, 0} Bool)) : (a : Type u) → Set (Sieve a)) α ↔
    S ∈ (typesGrothendieckTopology : (a : Type u) → Set (Sieve a)) α

Tactic:
⟨fun hs x => ?_, fun hs β f => Presieve.isSheaf_yoneda' _ fun y => hs (f y)⟩

Premises used: CategoryTheory.ConcreteCategory.hom, Iff.intro, CategoryTheory.Presieve.isSheaf_yoneda', CategoryTheory.Sieve.pullback, DFunLike.coe
-- Module: Mathlib.CategoryTheory.Sites.Types
Goal:
α : Type u
S : Sieve α
h :
  ∀ (hs : S ∈ (Sheaf.finestTopologySingle (Functor.obj yoneda (ULift.{u, 0} Bool)) : (a : Type u) → Set (Sieve a)) α)
    (x : α), S.arrows (Y := PUnit.{u + 1}) (↾fun (x_1 : PUnit.{u + 1}) ↦ x)
⊢ S ∈ (Sheaf.finestTopologySingle (Functor.obj yoneda (ULift.{u, 0} Bool)) : (a : Type u) → Set (Sieve a)) α ↔
    S ∈ (typesGrothendieckTopology : (a : Type u) → Set (Sieve a)) α

Tactic:
refine ⟨fun hs x => ?_, fun hs β f => Presieve.isSheaf_yoneda' _ fun y => hs (f y)⟩
-- Module: Mathlib.CategoryTheory.Sites.Types
Goal:
α : Type u
S : Sieve α
hs : S ∈ (Sheaf.finestTopologySingle (Functor.obj yoneda (ULift.{u, 0} Bool)) : (a : Type u) → Set (Sieve a)) α
x : α
h : ∀ (hsx : ¬S.arrows (Y := PUnit.{u + 1}) (↾fun (x_1 : PUnit.{u + 1}) ↦ x)), False
⊢ S.arrows (Y := PUnit.{u + 1}) (↾fun (x_1 : PUnit.{u + 1}) ↦ x)

Tactic:
by_contra hsx
-- Module: Mathlib.CategoryTheory.Sites.Types
Goal:
α : Type u
S : Sieve α
hs : S ∈ (Sheaf.finestTopologySingle (Functor.obj yoneda (ULift.{u, 0} Bool)) : (a : Type u) → Set (Sieve a)) α
x : α
hsx : ¬S.arrows (Y := PUnit.{u + 1}) (↾fun (x_1 : PUnit.{u + 1}) ↦ x)
β : Type u
f : β ⟶ PUnit.{u + 1}
hf : Sieve.arrows (Sieve.pullback (↾fun (x_1 : PUnit.{u + 1}) ↦ x) S) f
dsimp :
  Eq (α := β ⟶ ULift.{u, 0} Bool) (f ≫ ↾fun (x : PUnit.{u + 1}) ↦ { down := true })
    (f ≫ ↾fun (x : PUnit.{u + 1}) ↦ { down := false })
⊢ Eq (α := (fun (X : Type u) ↦ X) (Functor.obj (Functor.obj yoneda (ULift.{u, 0} Bool)) (op β)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Functor.map (Functor.obj yoneda (ULift.{u, 0} Bool)) f.op) :
          (a : (fun (X : Type u) ↦ X) ((yoneda.obj (ULift.{u, 0} Bool)).obj (op PUnit.{u + 1}))) →
            (fun (X : Type u) ↦ X) ((yoneda.obj (ULift.{u, 0} Bool)).obj (op β)))
        (↾fun (x : unop (op PUnit.{u + 1})) ↦ { down := true }) :
      (fun (X : Type u) ↦ X) (Functor.obj (Functor.obj yoneda (ULift.{u, 0} Bool)) (op β)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Functor.map (Functor.obj yoneda (ULift.{u, 0} Bool)) f.op) :
          (a : (fun (X : Type u) ↦ X) ((yoneda.obj (ULift.{u, 0} Bool)).obj (op PUnit.{u + 1}))) →
            (fun (X : Type u) ↦ X) ((yoneda.obj (ULift.{u, 0} Bool)).obj (op β)))
        (↾fun (x : unop (op PUnit.{u + 1})) ↦ { down := false }) :
      (fun (X : Type u) ↦ X) (Functor.obj (Functor.obj yoneda (ULift.{u, 0} Bool)) (op β)))

Tactic:
dsimp