awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Sites.Types
Goal:
S : Type uᵒᵖ ⥤ Type u
hs : IsSheaf typesGrothendieckTopology S
α : Type u
f : α → S.obj (op PUnit.{u + 1})
x : (fun (X : Type u) ↦ X) α
h :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (S.map (Quiver.Hom.op (↾fun (x : PUnit.{u + 1}) ↦ PUnit.unit))) :
        (a : (fun (X : Type u) ↦ X) (S.obj (op PUnit.{u + 1}))) → (fun (X : Type u) ↦ X) (S.obj (op PUnit.{u + 1})))
      (f
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (↾fun (x_1 : PUnit.{u + 1}) ↦ x) :
            (a : (fun (X : Type u) ↦ X) PUnit.{u + 1}) → (fun (X : Type u) ↦ X) α)
          (Classical.choose (p := fun (x : PUnit.{u + 1}) ↦ ∀ (y : PUnit.{u + 1}), y = x) ⋯))) =
    f x
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (eval S α (typesGlue S hs α f)) :
        (a : (fun (X : Type u) ↦ X) α) → (fun (X : Type u) ↦ X) (S.obj (op PUnit.{u + 1})))
      x =
    f x

Tactic:
apply (IsSheafFor.valid_glue _ _ _ <| ⟨PUnit.unit, fun _ => Subsingleton.elim _ _⟩).trans

Premises used: CategoryTheory.Presieve.IsSheafFor.valid_glue, Eq.trans
-- Module: Mathlib.CategoryTheory.Sites.Types
Goal:
S : Type uᵒᵖ ⥤ Type u
hs : IsSheaf typesGrothendieckTopology S
α : Type u
f : α → S.obj (op PUnit.{u + 1})
x : (fun (X : Type u) ↦ X) α
⊢ Eq (α := S.obj (op PUnit.{u + 1}))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (S.map (𝟙 (op PUnit.{u + 1}))) :
          (a : S.obj (op PUnit.{u + 1})) → S.obj (op PUnit.{u + 1}))
        (f
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (↾fun (x_1 : PUnit.{u + 1}) ↦ x) :
              (a : (fun (X : Type u) ↦ X) PUnit.{u + 1}) → (fun (X : Type u) ↦ X) α)
            (Classical.choose (p := fun (x : PUnit.{u + 1}) ↦ ∀ (y : PUnit.{u + 1}), y = x) ⋯))) :
      S.obj (op PUnit.{u + 1}))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (𝟙 (S.obj (op PUnit.{u + 1}))) :
          (a : S.obj (op PUnit.{u + 1})) → S.obj (op PUnit.{u + 1}))
        (f
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (↾fun (x_1 : PUnit.{u + 1}) ↦ x) :
              (a : (fun (X : Type u) ↦ X) PUnit.{u + 1}) → (fun (X : Type u) ↦ X) α)
            (Classical.choose (p := fun (x : PUnit.{u + 1}) ↦ ∀ (y : PUnit.{u + 1}), y = x) ⋯))) :
      S.obj (op PUnit.{u + 1}))

Tactic:
ConcreteCategory.congr_hom (S.map_id _) _

Premises used: CategoryTheory.Functor.map_id, CategoryTheory.ConcreteCategory.congr_hom
-- Module: Mathlib.CategoryTheory.Sites.Types
Goal:
S : Type uᵒᵖ ⥤ Type u
hs : IsSheaf typesGrothendieckTopology S
α : Type u
f : α → S.obj (op PUnit.{u + 1})
x : (fun (X : Type u) ↦ X) α
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (S.map (Quiver.Hom.op (↾fun (x : PUnit.{u + 1}) ↦ PUnit.unit))) :
        (a : (fun (X : Type u) ↦ X) (S.obj (op PUnit.{u + 1}))) → (fun (X : Type u) ↦ X) (S.obj (op PUnit.{u + 1})))
      (f
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (↾fun (x_1 : PUnit.{u + 1}) ↦ x) :
            (a : (fun (X : Type u) ↦ X) PUnit.{u + 1}) → (fun (X : Type u) ↦ X) α)
          (Classical.choose (p := fun (x : PUnit.{u + 1}) ↦ ∀ (y : PUnit.{u + 1}), y = x) ⋯))) =
    f x

Tactic:
convert! ConcreteCategory.congr_hom (S.map_id _) _

Premises used: CategoryTheory.Functor.map_id, CategoryTheory.ConcreteCategory.congr_hom
-- Module: Mathlib.CategoryTheory.Sites.Types
Goal:
S : Type uᵒᵖ ⥤ Type u
hs : IsSheaf typesGrothendieckTopology S
α : Type u
s : S.obj (op α)
apply :
  ∀ ⦃Y : Type u⦄ ⦃f : Y ⟶ α⦄,
    discretePresieve α f →
      Eq (α := (fun (X : Type u) ↦ X) (S.obj (op Y)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (S.map f.op) :
              (a : (fun (X : Type u) ↦ X) (S.obj (op α))) → (fun (X : Type u) ↦ X) (S.obj (op Y)))
            (typesGlue S hs α
              (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (eval S α s)) :
                (a : (fun (X : Type u) ↦ X) α) → (fun (X : Type u) ↦ X) (S.obj (op PUnit.{u + 1})))) :
          (fun (X : Type u) ↦ X) (S.obj (op Y)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (S.map f.op) :
              (a : (fun (X : Type u) ↦ X) (S.obj (op α))) → (fun (X : Type u) ↦ X) (S.obj (op Y)))
            s :
          (fun (X : Type u) ↦ X) (S.obj (op Y)))
⊢ typesGlue S hs α
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (eval S α s)) :
        (a : (fun (X : Type u) ↦ X) α) → (fun (X : Type u) ↦ X) (S.obj (op PUnit.{u + 1}))) =
    s

Tactic:
apply (hs.isSheafFor _ (generate_discretePresieve_mem α)).isSeparatedFor.ext

Premises used: CategoryTheory.Presieve.IsSeparatedFor.ext, CategoryTheory.generate_discretePresieve_mem, CategoryTheory.Presieve.IsSheafFor.isSeparatedFor, CategoryTheory.Presieve.IsSheaf.isSheafFor
-- Module: Mathlib.CategoryTheory.Sites.Types
Goal:
S : Type uᵒᵖ ⥤ Type u
hs : IsSheaf typesGrothendieckTopology S
α : Type u
s : S.obj (op α)
β : Type u
f : β ⟶ α
hf : discretePresieve α f
apply :
  Eq (α := (fun (X : Type u) ↦ X) (S.obj (op β)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (S.map (Quiver.Hom.op (↾fun (x : β) ↦ PUnit.unit))) :
          (a : (fun (X : Type u) ↦ X) (S.obj (op PUnit.{u + 1}))) → (fun (X : Type u) ↦ X) (S.obj (op β)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (eval S α s) :
              (a : (fun (X : Type u) ↦ X) α) → (fun (X : Type u) ↦ X) (S.obj (op PUnit.{u + 1})))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u) ↦ X) β) → (fun (X : Type u) ↦ X) α)
                (Classical.choose (p := fun (x : β) ↦ ∀ (y : β), y = x) hf) :
              (fun (X : Type u) ↦ X) α) :
          (fun (X : Type u) ↦ X) (S.obj (op PUnit.{u + 1}))) :
      (fun (X : Type u) ↦ X) (S.obj (op β)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (S.map f.op) :
          (a : (fun (X : Type u) ↦ X) (S.obj (op α))) → (fun (X : Type u) ↦ X) (S.obj (op β)))
        s :
      (fun (X : Type u) ↦ X) (S.obj (op β)))
⊢ Eq (α := (fun (X : Type u) ↦ X) (S.obj (op β)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (S.map f.op) :
          (a : (fun (X : Type u) ↦ X) (S.obj (op α))) → (fun (X : Type u) ↦ X) (S.obj (op β)))
        (typesGlue S hs α
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (eval S α s)) :
            (a : (fun (X : Type u) ↦ X) α) → (fun (X : Type u) ↦ X) (S.obj (op PUnit.{u + 1})))) :
      (fun (X : Type u) ↦ X) (S.obj (op β)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (S.map f.op) :
          (a : (fun (X : Type u) ↦ X) (S.obj (op α))) → (fun (X : Type u) ↦ X) (S.obj (op β)))
        s :
      (fun (X : Type u) ↦ X) (S.obj (op β)))

Tactic:
apply (IsSheafFor.valid_glue _ _ _ hf).trans

Premises used: CategoryTheory.Presieve.IsSheafFor.valid_glue, Eq.trans
-- Module: Mathlib.CategoryTheory.Sites.Types
Goal:
S : Type uᵒᵖ ⥤ Type u
hs : IsSheaf typesGrothendieckTopology S
α : Type u
s : S.obj (op α)
β : Type u
f : β ⟶ α
hf : discretePresieve α f
simp :
  Eq (α := S.obj (op β))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (S.map
              (Quiver.Hom.op
                (CategoryStruct.comp (Y := PUnit.{u + 1}) (↾fun (x : β) ↦ PUnit.unit)
                  (↾fun (x : PUnit.{u + 1}) ↦
                    (ConcreteCategory.hom (FC := TypeCat.Fun) f : (a : β) → α)
                      (Classical.choose (p := fun (x : β) ↦ ∀ (y : β), y = x) hf))))) :
          (a : S.obj (op α)) → S.obj (op β))
        s :
      S.obj (op β))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (S.map f.op) : (a : S.obj (op α)) → S.obj (op β)) s : S.obj (op β))
⊢ Eq (α := (fun (X : Type u) ↦ X) (S.obj (op β)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (S.map (Quiver.Hom.op (↾fun (x : β) ↦ PUnit.unit))) :
          (a : (fun (X : Type u) ↦ X) (S.obj (op PUnit.{u + 1}))) → (fun (X : Type u) ↦ X) (S.obj (op β)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (eval S α s) :
              (a : (fun (X : Type u) ↦ X) α) → (fun (X : Type u) ↦ X) (S.obj (op PUnit.{u + 1})))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u) ↦ X) β) → (fun (X : Type u) ↦ X) α)
                (Classical.choose (p := fun (x : β) ↦ ∀ (y : β), y = x) hf) :
              (fun (X : Type u) ↦ X) α) :
          (fun (X : Type u) ↦ X) (S.obj (op PUnit.{u + 1}))) :
      (fun (X : Type u) ↦ X) (S.obj (op β)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (S.map f.op) :
          (a : (fun (X : Type u) ↦ X) (S.obj (op α))) → (fun (X : Type u) ↦ X) (S.obj (op β)))
        s :
      (fun (X : Type u) ↦ X) (S.obj (op β)))

Tactic:
simp only [eval, ConcreteCategory.hom_ofHom, TypeCat.Fun.coe_mk, ← comp_apply,
    ← Functor.map_comp, ← op_comp]

Premises used: CategoryTheory.op_comp, TypeCat.Fun.coe_mk, CategoryTheory.comp_apply, CategoryTheory.Functor.map_comp, CategoryTheory.eval, CategoryTheory.ConcreteCategory.hom_ofHom
-- Module: Mathlib.CategoryTheory.Sites.Types
Goal:
S : Type uᵒᵖ ⥤ Type u
hs : IsSheaf typesGrothendieckTopology S
α : Type u
s : S.obj (op α)
β : Type u
f : β ⟶ α
hf : discretePresieve α f
e_a :
  CategoryStruct.comp (Y := PUnit.{u + 1}) (↾fun (x : β) ↦ PUnit.unit)
      (↾fun (x : PUnit.{u + 1}) ↦
        (ConcreteCategory.hom (FC := TypeCat.Fun) f : (a : β) → α)
          (Classical.choose (p := fun (x : β) ↦ ∀ (y : β), y = x) hf)) =
    f
⊢ Eq (α := S.obj (op β))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (S.map
              (Quiver.Hom.op
                (CategoryStruct.comp (Y := PUnit.{u + 1}) (↾fun (x : β) ↦ PUnit.unit)
                  (↾fun (x : PUnit.{u + 1}) ↦
                    (ConcreteCategory.hom (FC := TypeCat.Fun) f : (a : β) → α)
                      (Classical.choose (p := fun (x : β) ↦ ∀ (y : β), y = x) hf))))) :
          (a : S.obj (op α)) → S.obj (op β))
        s :
      S.obj (op β))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (S.map f.op) : (a : S.obj (op α)) → S.obj (op β)) s : S.obj (op β))

Tactic:
congr
-- Module: Mathlib.CategoryTheory.Sites.Types
Goal:
S : Type uᵒᵖ ⥤ Type u
hs : IsSheaf typesGrothendieckTopology S
α : Type u
s : S.obj (op α)
β : Type u
f : β ⟶ α
hf : discretePresieve α f
e_a :
  ∀ (x : β),
    TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (CategoryStruct.comp (Y := PUnit.{u + 1}) (↾fun (x : β) ↦ PUnit.unit)
            (↾fun (x : PUnit.{u + 1}) ↦
              (ConcreteCategory.hom (FC := TypeCat.Fun) f : (a : β) → α)
                (Classical.choose (p := fun (x : β) ↦ ∀ (y : β), y = x) hf))))
        x =
      (ConcreteCategory.hom (FC := TypeCat.Fun) f).toFun x
⊢ CategoryStruct.comp (Y := PUnit.{u + 1}) (↾fun (x : β) ↦ PUnit.unit)
      (↾fun (x : PUnit.{u + 1}) ↦
        (ConcreteCategory.hom (FC := TypeCat.Fun) f : (a : β) → α)
          (Classical.choose (p := fun (x : β) ↦ ∀ (y : β), y = x) hf)) =
    f

Tactic:
ext x
-- Module: Mathlib.CategoryTheory.Sites.Types
Goal:
S : Type uᵒᵖ ⥤ Type u
hs : IsSheaf typesGrothendieckTopology S
α : Type u
s : S.obj (op α)
β : Type u
f : β ⟶ α
hf : discretePresieve α f
x : β
⊢ TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (CategoryStruct.comp (Y := PUnit.{u + 1}) (↾fun (x : β) ↦ PUnit.unit)
          (↾fun (x : PUnit.{u + 1}) ↦
            (ConcreteCategory.hom (FC := TypeCat.Fun) f : (a : β) → α)
              (Classical.choose (p := fun (x : β) ↦ ∀ (y : β), y = x) hf))))
      x =
    (ConcreteCategory.hom (FC := TypeCat.Fun) f).toFun x

Tactic:
congr_arg f (Classical.choose_spec hf x).symm

Premises used: CategoryTheory.ConcreteCategory.hom, congr_arg, Classical.choose_spec, Eq.symm, DFunLike.coe
-- Module: Mathlib.CategoryTheory.Sites.Types
Goal:
S : Type uᵒᵖ ⥤ Type u
hs : IsSheaf typesGrothendieckTopology S
α : Type u
s : S.obj (op α)
β : Type u
f : β ⟶ α
hf : discretePresieve α f
x : β
⊢ TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (CategoryStruct.comp (Y := PUnit.{u + 1}) (↾fun (x : β) ↦ PUnit.unit)
          (↾fun (x : PUnit.{u + 1}) ↦
            (ConcreteCategory.hom (FC := TypeCat.Fun) f : (a : β) → α)
              (Classical.choose (p := fun (x : β) ↦ ∀ (y : β), y = x) hf))))
      x =
    (ConcreteCategory.hom (FC := TypeCat.Fun) f).toFun x

Tactic:
exact congr_arg f (Classical.choose_spec hf x).symm

Premises used: CategoryTheory.ConcreteCategory.hom, congr_arg, Classical.choose_spec, Eq.symm, DFunLike.coe
-- Module: Mathlib.CategoryTheory.Sites.Types
Goal:
S : Type uᵒᵖ ⥤ Type u
hs : Presheaf.IsSheaf typesGrothendieckTopology S
α : Type u
x : α ⟶ S.obj (op PUnit.{u + 1})
h :
  ∀ (x_1 : α),
    (ConcreteCategory.hom (FC := TypeCat.Fun)
            (eval S α
              ((fun (f : α ⟶ S.obj (op PUnit.{u + 1})) ↦
                  typesGlue S ⋯ α
                    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f) :
                      (a : (fun (X : Type u) ↦ X) α) → (fun (X : Type u) ↦ X) (S.obj (op PUnit.{u + 1}))))
                x))).toFun
        x_1 =
      (ConcreteCategory.hom (FC := TypeCat.Fun) x).toFun x_1
⊢ eval S α
      ((fun (f : α ⟶ S.obj (op PUnit.{u + 1})) ↦
          typesGlue S ⋯ α
            (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f) :
              (a : (fun (X : Type u) ↦ X) α) → (fun (X : Type u) ↦ X) (S.obj (op PUnit.{u + 1}))))
        x) =
    x

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Sites.Types
Goal:
S : Type uᵒᵖ ⥤ Type u
hs : Presheaf.IsSheaf typesGrothendieckTopology S
α : Type u
x : α ⟶ S.obj (op PUnit.{u + 1})
x_1 : α
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun)
          (eval S α
            ((fun (f : α ⟶ S.obj (op PUnit.{u + 1})) ↦
                typesGlue S ⋯ α
                  (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f) :
                    (a : (fun (X : Type u) ↦ X) α) → (fun (X : Type u) ↦ X) (S.obj (op PUnit.{u + 1}))))
              x))).toFun
      x_1 =
    (ConcreteCategory.hom (FC := TypeCat.Fun) x).toFun x_1

Tactic:
simp [eval_typesGlue]

Premises used: CategoryTheory.eval_typesGlue
-- Module: Mathlib.CategoryTheory.Sites.Types
Goal:
S : Type uᵒᵖ ⥤ Type u
α β : Type u
f : β ⟶ α
s : (fun (X : Type u) ↦ X) (S.obj (op α))
x : (fun (X : Type u) ↦ X) β
simp_rw :
  Eq (α := S.obj (op PUnit.{u + 1}))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (↾fun (x : β) ↦
              (ConcreteCategory.hom (FC := TypeCat.Fun) (S.map (Quiver.Hom.op ((↾fun (x_1 : PUnit.{u + 1}) ↦ x) ≫ f))) :
                  (a : S.obj (op α)) → S.obj (op PUnit.{u + 1}))
                s) :
          (a : β) → S.obj (op PUnit.{u + 1}))
        x :
      S.obj (op PUnit.{u + 1}))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (f ≫
              ↾fun (x : α) ↦
                (ConcreteCategory.hom (FC := TypeCat.Fun) (S.map (Quiver.Hom.op (↾fun (x_1 : PUnit.{u + 1}) ↦ x))) :
                    (a : S.obj (op α)) → S.obj (op PUnit.{u + 1}))
                  s) :
          (a : β) → S.obj (op PUnit.{u + 1}))
        x :
      S.obj (op PUnit.{u + 1}))
⊢ Eq (α := (fun (X : Type u) ↦ X) (S.obj (op PUnit.{u + 1})))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (eval S β
              ((ConcreteCategory.hom (FC := TypeCat.Fun) (S.map f.op) :
                  (a : (fun (X : Type u) ↦ X) (S.obj (op α))) → (fun (X : Type u) ↦ X) (S.obj (op β)))
                s)) :
          (a : (fun (X : Type u) ↦ X) β) → (fun (X : Type u) ↦ X) (S.obj (op PUnit.{u + 1})))
        x :
      (fun (X : Type u) ↦ X) (S.obj (op PUnit.{u + 1})))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (eval S α s) :
          (a : (fun (X : Type u) ↦ X) α) → (fun (X : Type u) ↦ X) (S.obj (op PUnit.{u + 1})))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u) ↦ X) β) → (fun (X : Type u) ↦ X) α) x :
          (fun (X : Type u) ↦ X) α) :
      (fun (X : Type u) ↦ X) (S.obj (op PUnit.{u + 1})))

Tactic:
simp_rw [eval, ← comp_apply, ← Functor.map_comp, ← op_comp]

Premises used: CategoryTheory.op_comp, CategoryTheory.comp_apply, CategoryTheory.Functor.map_comp, CategoryTheory.eval
-- Module: Mathlib.CategoryTheory.Sites.Types
Goal:
S : Type uᵒᵖ ⥤ Type u
α β : Type u
f : β ⟶ α
s : (fun (X : Type u) ↦ X) (S.obj (op α))
x : (fun (X : Type u) ↦ X) β
⊢ Eq (α := S.obj (op PUnit.{u + 1}))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (↾fun (x : β) ↦
              (ConcreteCategory.hom (FC := TypeCat.Fun) (S.map (Quiver.Hom.op ((↾fun (x_1 : PUnit.{u + 1}) ↦ x) ≫ f))) :
                  (a : S.obj (op α)) → S.obj (op PUnit.{u + 1}))
                s) :
          (a : β) → S.obj (op PUnit.{u + 1}))
        x :
      S.obj (op PUnit.{u + 1}))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (f ≫
              ↾fun (x : α) ↦
                (ConcreteCategory.hom (FC := TypeCat.Fun) (S.map (Quiver.Hom.op (↾fun (x_1 : PUnit.{u + 1}) ↦ x))) :
                    (a : S.obj (op α)) → S.obj (op PUnit.{u + 1}))
                  s) :
          (a : β) → S.obj (op PUnit.{u + 1}))
        x :
      S.obj (op PUnit.{u + 1}))

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Sites.Types
Goal:
S : Type uᵒᵖ ⥤ Type u
hs : Presheaf.IsSheaf typesGrothendieckTopology S
α β : Type uᵒᵖ
f : α ⟶ β
dsimp :
  S.map f ≫ Iso.hom (Equiv.toIso (evalEquiv S hs (unop β))) =
    Iso.hom (Equiv.toIso (evalEquiv S hs (unop α))) ≫ ↾fun (g : unop α ⟶ S.obj (op PUnit.{u + 1})) ↦ f.unop ≫ g
⊢ Eq (α := S.obj α ⟶ Functor.obj (Functor.obj yoneda (S.obj (op PUnit.{u + 1}))) β)
    (S.map f ≫
      Iso.hom
        ((fun (α : Type uᵒᵖ) ↦
            (Equiv.toIso (evalEquiv S hs (unop α)) : S.obj (op (unop α)) ≅ unop α ⟶ S.obj (op PUnit.{u + 1})))
          β))
    (Iso.hom
        ((fun (α : Type uᵒᵖ) ↦
            (Equiv.toIso (evalEquiv S hs (unop α)) : S.obj (op (unop α)) ≅ unop α ⟶ S.obj (op PUnit.{u + 1})))
          α) ≫
      Functor.map (Functor.obj yoneda (S.obj (op PUnit.{u + 1}))) f)

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Sites.Types
Goal:
S : Type uᵒᵖ ⥤ Type u
hs : Presheaf.IsSheaf typesGrothendieckTopology S
α β : Type uᵒᵖ
f : α ⟶ β
h :
  ∀ (x : S.obj α) (x_1 : unop β),
    (ConcreteCategory.hom (FC := TypeCat.Fun)
            ((ConcreteCategory.hom (FC := TypeCat.Fun)
                  (S.map f ≫ Iso.hom (Equiv.toIso (evalEquiv S hs (unop β))))).toFun
              x)).toFun
        x_1 =
      TypeCat.Fun.toFun
        (@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
          (TypeCat.Fun.toFun
            (ConcreteCategory.hom (FC := TypeCat.Fun)
              (Iso.hom (Equiv.toIso (evalEquiv S hs (unop α))) ≫
                ↾fun (g : unop α ⟶ S.obj (op PUnit.{u + 1})) ↦ f.unop ≫ g))
            x))
        x_1
⊢ S.map f ≫ Iso.hom (Equiv.toIso (evalEquiv S hs (unop β))) =
    Iso.hom (Equiv.toIso (evalEquiv S hs (unop α))) ≫ ↾fun (g : unop α ⟶ S.obj (op PUnit.{u + 1})) ↦ f.unop ≫ g

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Sites.Types
Goal:
S : Type uᵒᵖ ⥤ Type u
hs : Presheaf.IsSheaf typesGrothendieckTopology S
α β : Type uᵒᵖ
f : α ⟶ β
x : S.obj α
x_1 : unop β
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (S.map f ≫ Iso.hom (Equiv.toIso (evalEquiv S hs (unop β))))).toFun
            x)).toFun
      x_1 =
    TypeCat.Fun.toFun
      (@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
        (TypeCat.Fun.toFun
          (ConcreteCategory.hom (FC := TypeCat.Fun)
            (Iso.hom (Equiv.toIso (evalEquiv S hs (unop α))) ≫
              ↾fun (g : unop α ⟶ S.obj (op PUnit.{u + 1})) ↦ f.unop ≫ g))
          x))
      x_1

Tactic:
eval_map S (unop α) (unop β) f.unop _ _

Premises used: CategoryTheory.eval_map, Quiver.Hom.op, Quiver.Hom.unop, Opposite.unop
-- Module: Mathlib.CategoryTheory.Sites.Types
Goal:
S : Type uᵒᵖ ⥤ Type u
hs : Presheaf.IsSheaf typesGrothendieckTopology S
α β : Type uᵒᵖ
f : α ⟶ β
x : S.obj α
x_1 : unop β
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (S.map f ≫ Iso.hom (Equiv.toIso (evalEquiv S hs (unop β))))).toFun
            x)).toFun
      x_1 =
    TypeCat.Fun.toFun
      (@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
        (TypeCat.Fun.toFun
          (ConcreteCategory.hom (FC := TypeCat.Fun)
            (Iso.hom (Equiv.toIso (evalEquiv S hs (unop α))) ≫
              ↾fun (g : unop α ⟶ S.obj (op PUnit.{u + 1})) ↦ f.unop ≫ g))
          x))
      x_1

Tactic:
exact eval_map S (unop α) (unop β) f.unop _ _

Premises used: CategoryTheory.eval_map, Quiver.Hom.unop, Opposite.unop
-- Module: Mathlib.CategoryTheory.Sites.Types
Goal:
S : Sheaf typesGrothendieckTopology (Type u)
h :
  InducedCategory.Hom.hom
      (CategoryStruct.comp (Y :=
        yoneda'.obj (S.obj (P := Presheaf.IsSheaf typesGrothendieckTopology).obj (op PUnit.{u + 1})))
        { hom := (equivYoneda (S.obj (P := Presheaf.IsSheaf typesGrothendieckTopology)) ⋯).hom }
        { hom := (equivYoneda (S.obj (P := Presheaf.IsSheaf typesGrothendieckTopology)) ⋯).inv }) =
    InducedCategory.Hom.hom (𝟙 S)
⊢ CategoryStruct.comp (Y :=
      yoneda'.obj (S.obj (P := Presheaf.IsSheaf typesGrothendieckTopology).obj (op PUnit.{u + 1})))
      { hom := (equivYoneda (S.obj (P := Presheaf.IsSheaf typesGrothendieckTopology)) ⋯).hom }
      { hom := (equivYoneda (S.obj (P := Presheaf.IsSheaf typesGrothendieckTopology)) ⋯).inv } =
    𝟙 S

Tactic:
ext1
-- Module: Mathlib.CategoryTheory.Sites.Types
Goal:
S : Sheaf typesGrothendieckTopology (Type u)
⊢ InducedCategory.Hom.hom
      (CategoryStruct.comp (Y :=
        yoneda'.obj (S.obj (P := Presheaf.IsSheaf typesGrothendieckTopology).obj (op PUnit.{u + 1})))
        { hom := (equivYoneda (S.obj (P := Presheaf.IsSheaf typesGrothendieckTopology)) ⋯).hom }
        { hom := (equivYoneda (S.obj (P := Presheaf.IsSheaf typesGrothendieckTopology)) ⋯).inv }) =
    InducedCategory.Hom.hom (𝟙 S)

Tactic:
apply (equivYoneda S.1 S.2).hom_inv_id

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.property, CategoryTheory.Iso.hom_inv_id, CategoryTheory.ObjectProperty.FullSubcategory.obj, CategoryTheory.equivYoneda
-- Module: Mathlib.CategoryTheory.Sites.Types
Goal:
S : Sheaf typesGrothendieckTopology (Type u)
h :
  InducedCategory.Hom.hom
      (CategoryStruct.comp (Y := S)
        { hom := (equivYoneda (S.obj (P := Presheaf.IsSheaf typesGrothendieckTopology)) ⋯).inv }
        { hom := (equivYoneda (S.obj (P := Presheaf.IsSheaf typesGrothendieckTopology)) ⋯).hom }) =
    InducedCategory.Hom.hom
      (𝟙 (yoneda'.obj (S.obj (P := Presheaf.IsSheaf typesGrothendieckTopology).obj (op PUnit.{u + 1}))))
⊢ CategoryStruct.comp (Y := S) { hom := (equivYoneda (S.obj (P := Presheaf.IsSheaf typesGrothendieckTopology)) ⋯).inv }
      { hom := (equivYoneda (S.obj (P := Presheaf.IsSheaf typesGrothendieckTopology)) ⋯).hom } =
    𝟙 (yoneda'.obj (S.obj (P := Presheaf.IsSheaf typesGrothendieckTopology).obj (op PUnit.{u + 1})))

Tactic:
ext1
-- Module: Mathlib.CategoryTheory.Sites.Types
Goal:
S : Sheaf typesGrothendieckTopology (Type u)
⊢ InducedCategory.Hom.hom
      (CategoryStruct.comp (Y := S)
        { hom := (equivYoneda (S.obj (P := Presheaf.IsSheaf typesGrothendieckTopology)) ⋯).inv }
        { hom := (equivYoneda (S.obj (P := Presheaf.IsSheaf typesGrothendieckTopology)) ⋯).hom }) =
    InducedCategory.Hom.hom
      (𝟙 (yoneda'.obj (S.obj (P := Presheaf.IsSheaf typesGrothendieckTopology).obj (op PUnit.{u + 1}))))

Tactic:
apply (equivYoneda S.1 S.2).inv_hom_id

Premises used: CategoryTheory.Iso.inv_hom_id, CategoryTheory.ObjectProperty.FullSubcategory.property, CategoryTheory.ObjectProperty.FullSubcategory.obj, CategoryTheory.equivYoneda