awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Sites.Subsheaf
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
F_1 F'_1 F'' : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
G G'_1 : Subfunctor F_1
F F' : Sheaf J (Type w)
f : F ⟶ F'
G' : Sheaf J (Type w)
g₁ g₂ : Sheaf.image f ⟶ G'
e : Sheaf.toImage f ≫ g₁ = Sheaf.toImage f ≫ g₂
U : Cᵒᵖ
s : F'.obj (P := Presheaf.IsSheaf J).obj U
hx : s ∈ (Subfunctor.sheafify J (Subfunctor.range f.hom)).obj U
V : C
i : V ⟶ unop U
y : F.obj (P := Presheaf.IsSheaf J).obj (op V)
e' :
  Eq (α := F'.obj (P := Presheaf.IsSheaf J).obj (op V))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.hom.app (op V)) :
          (a : (fun (X : Type w) ↦ X) (F.obj.obj (op V))) → (fun (X : Type w) ↦ X) (F'.obj.obj (op V)))
        y :
      (fun (X : Type w) ↦ X) (F'.obj (P := Presheaf.IsSheaf J).obj (op V)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F'.obj (P := Presheaf.IsSheaf J).map i.op) :
          (a : (fun (X : Type w) ↦ X) (F'.obj.obj (op (unop U)))) → (fun (X : Type w) ↦ X) (F'.obj.obj (op V)))
        s :
      (fun (X : Type w) ↦ X) (F'.obj (P := Presheaf.IsSheaf J).obj (op V)))
E :
  Eq (α := (fun (X : Type w) ↦ X) ((Sheaf.image f).obj (P := Presheaf.IsSheaf J).obj (op V)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((Sheaf.toImage f).hom.app (op V)) :
          (a : (fun (X : Type w) ↦ X) (F.obj.obj (op V))) → (fun (X : Type w) ↦ X) ((Sheaf.image f).obj.obj (op V)))
        y :
      (fun (X : Type w) ↦ X) ((Sheaf.image f).obj (P := Presheaf.IsSheaf J).obj (op V)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((Sheaf.image f).obj (P := Presheaf.IsSheaf J).map i.op) :
          (a : (fun (X : Type w) ↦ X) ((Sheaf.image f).obj.obj (op (unop U)))) →
            (fun (X : Type w) ↦ X) ((Sheaf.image f).obj.obj (op V)))
        (Subtype.mk (p := fun (x : F'.obj (P := Presheaf.IsSheaf J).obj (op (unop U))) ↦
          Membership.mem (γ := Set (F'.obj (P := Presheaf.IsSheaf J).obj (op (unop U))))
            ((Subfunctor.sheafify J (Subfunctor.range f.hom)).obj (op (unop U))) x)
          s hx) :
      (fun (X : Type w) ↦ X) ((Sheaf.image f).obj (P := Presheaf.IsSheaf J).obj (op V)))
⊢ Eq.{w + 1} (α := (fun (X : Type w) ↦ X) (G'.obj (P := Presheaf.IsSheaf J).obj (op V)))
    ((fun (f : F ⟶ G') ↦
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.hom.app (op V)) :
              (a : (fun (X : Type w) ↦ X) (F.obj.obj (op V))) → (fun (X : Type w) ↦ X) (G'.obj.obj (op V)))
            y :
          (fun (X : Type w) ↦ X) (G'.obj (P := Presheaf.IsSheaf J).obj (op V))))
      (Sheaf.toImage f ≫ g₁))
    ((fun (f : F ⟶ G') ↦
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.hom.app (op V)) :
              (a : (fun (X : Type w) ↦ X) (F.obj.obj (op V))) → (fun (X : Type w) ↦ X) (G'.obj.obj (op V)))
            y :
          (fun (X : Type w) ↦ X) (G'.obj (P := Presheaf.IsSheaf J).obj (op V))))
      (Sheaf.toImage f ≫ g₂))

Tactic:
have := congr_arg (fun f : F ⟶ G' => f.hom.app _ y) e
-- Module: Mathlib.CategoryTheory.Sites.Subsheaf
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
F_1 F'_1 F'' : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
G G' : Subfunctor F_1
F F' : Sheaf J (Type (max v u))
f : F ⟶ F'
I : Limits.MonoFactorisation f
⊢ Mono I.m.hom

Tactic:
haveI M := (Sheaf.Hom.mono_iff_presheaf_mono J (Type (max v u)) _).mp I.m_mono
-- Module: Mathlib.CategoryTheory.Sites.Subsheaf
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
F_1 F'_1 F'' : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
G G' : Subfunctor F_1
F F' : Sheaf J (Type (max v u))
f : F ⟶ F'
I : Limits.MonoFactorisation f
M : Mono I.m.hom
refine : Subfunctor.sheafify J (Subfunctor.range f.hom) ≤ Subfunctor.range I.m.hom
⊢ (imageMonoFactorization f).I ⟶ I.I

Tactic:
refine ⟨Subfunctor.homOfLe ?_ ≫ inv (Subfunctor.toRange I.m.1)⟩
-- Module: Mathlib.CategoryTheory.Sites.Subsheaf
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
F_1 F'_1 F'' : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
G G' : Subfunctor F_1
F F' : Sheaf J (Type (max v u))
f : F ⟶ F'
I : Limits.MonoFactorisation f
M : Mono I.m.hom
h : Subfunctor.range f.hom ≤ Subfunctor.range I.m.hom
hF : Presieve.IsSheaf J (F'.obj (P := Presheaf.IsSheaf J))
hG' : Presieve.IsSheaf J (Subfunctor.range I.m.hom).toFunctor
⊢ Subfunctor.sheafify J (Subfunctor.range f.hom) ≤ Subfunctor.range I.m.hom

Tactic:
apply Subfunctor.sheafify_le

Premises used: CategoryTheory.Subfunctor.sheafify_le
-- Module: Mathlib.CategoryTheory.Sites.Subsheaf
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
F_1 F'_1 F'' : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
G G' : Subfunctor F_1
F F' : Sheaf J (Type (max v u))
f : F ⟶ F'
I : Limits.MonoFactorisation f
M : Mono I.m.hom
rw : Subfunctor.range (I.e ≫ I.m).hom
| Subfunctor.range f.hom

Tactic:
rw [← I.fac]

Premises used: CategoryTheory.Limits.MonoFactorisation.fac
-- Module: Mathlib.CategoryTheory.Sites.Subsheaf
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
F_1 F'_1 F'' : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
G G' : Subfunctor F_1
F F' : Sheaf J (Type (max v u))
f : F ⟶ F'
I : Limits.MonoFactorisation f
M : Mono I.m.hom
h : Subfunctor.range (I.e ≫ I.m).hom ≤ Subfunctor.range I.m.hom
⊢ Subfunctor.range f.hom ≤ Subfunctor.range I.m.hom

Tactic:
conv_lhs => rw [← I.fac]

Premises used: CategoryTheory.Limits.MonoFactorisation.fac
-- Module: Mathlib.CategoryTheory.Sites.Subsheaf
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
F_1 F'_1 F'' : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
G G' : Subfunctor F_1
F F' : Sheaf J (Type (max v u))
f : F ⟶ F'
I : Limits.MonoFactorisation f
M : Mono I.m.hom
hF : Presheaf.IsSheaf J (F'.obj (P := Presheaf.IsSheaf J))
⊢ Presieve.IsSheaf J (F'.obj (P := Presheaf.IsSheaf J))

Tactic:
rw [← isSheaf_iff_isSheaf_of_type]

Premises used: CategoryTheory.isSheaf_iff_isSheaf_of_type
-- Module: Mathlib.CategoryTheory.Sites.Subsheaf
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
F_1 F'_1 F'' : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
G G' : Subfunctor F_1
F F' : Sheaf J (Type (max v u))
f : F ⟶ F'
I : Limits.MonoFactorisation f
M : Mono I.m.hom
⊢ Presheaf.IsSheaf J (F'.obj (P := Presheaf.IsSheaf J))

Tactic:
F'.2

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.property
-- Module: Mathlib.CategoryTheory.Sites.Subsheaf
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
F_1 F'_1 F'' : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
G G' : Subfunctor F_1
F F' : Sheaf J (Type (max v u))
f : F ⟶ F'
I : Limits.MonoFactorisation f
M : Mono I.m.hom
⊢ Presheaf.IsSheaf J (F'.obj (P := Presheaf.IsSheaf J))

Tactic:
exact F'.2

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.property
-- Module: Mathlib.CategoryTheory.Sites.Subsheaf
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
F_1 F'_1 F'' : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
G G' : Subfunctor F_1
F F' : Sheaf J (Type (max v u))
f : F ⟶ F'
I : Limits.MonoFactorisation f
M : Mono I.m.hom
hG' : Presieve.IsSheaf J (I.I.obj (P := Presheaf.IsSheaf J))
⊢ Presieve.IsSheaf J (Subfunctor.range I.m.hom).toFunctor

Tactic:
apply Presieve.isSheaf_iso J (asIso <| Subfunctor.toRange I.m.1)

Premises used: CategoryTheory.Presieve.isSheaf_iso, CategoryTheory.Subfunctor.toRange, CategoryTheory.InducedCategory.Hom.hom, CategoryTheory.Limits.MonoFactorisation.m, CategoryTheory.asIso
-- Module: Mathlib.CategoryTheory.Sites.Subsheaf
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
F_1 F'_1 F'' : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
G G' : Subfunctor F_1
F F' : Sheaf J (Type (max v u))
f : F ⟶ F'
I : Limits.MonoFactorisation f
M : Mono I.m.hom
hG' : Presheaf.IsSheaf J (I.I.obj (P := Presheaf.IsSheaf J))
⊢ Presieve.IsSheaf J (I.I.obj (P := Presheaf.IsSheaf J))

Tactic:
rw [← isSheaf_iff_isSheaf_of_type]

Premises used: CategoryTheory.isSheaf_iff_isSheaf_of_type
-- Module: Mathlib.CategoryTheory.Sites.Subsheaf
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
F_1 F'_1 F'' : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
G G' : Subfunctor F_1
F F' : Sheaf J (Type (max v u))
f : F ⟶ F'
I : Limits.MonoFactorisation f
M : Mono I.m.hom
⊢ Presheaf.IsSheaf J (I.I.obj (P := Presheaf.IsSheaf J))

Tactic:
I.I.2

Premises used: CategoryTheory.Limits.MonoFactorisation.I, CategoryTheory.ObjectProperty.FullSubcategory.property
-- Module: Mathlib.CategoryTheory.Sites.Subsheaf
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
F_1 F'_1 F'' : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
G G' : Subfunctor F_1
F F' : Sheaf J (Type (max v u))
f : F ⟶ F'
I : Limits.MonoFactorisation f
M : Mono I.m.hom
⊢ Presheaf.IsSheaf J (I.I.obj (P := Presheaf.IsSheaf J))

Tactic:
exact I.I.2

Premises used: CategoryTheory.Limits.MonoFactorisation.I, CategoryTheory.ObjectProperty.FullSubcategory.property
-- Module: Mathlib.CategoryTheory.Sites.Subsheaf
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
F_1 F'_1 F'' : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
G G' : Subfunctor F_1
F F' : Sheaf J (Type (max v u))
f : F ⟶ F'
I : Limits.MonoFactorisation f
h :
  InducedCategory.Hom.hom
      ({ hom := Subfunctor.homOfLe ⋯ ≫ inv (Subfunctor.toRange I.m.hom) :
          InducedCategory.Hom (D := Cᵒᵖ ⥤ Type (max v u)) (F :=
            ObjectProperty.FullSubcategory.obj (P := Presheaf.IsSheaf J)) (imageMonoFactorization f).I I.I } ≫
        I.m) =
    (imageMonoFactorization f).m.hom
⊢ { hom := Subfunctor.homOfLe ⋯ ≫ inv (Subfunctor.toRange I.m.hom) :
        InducedCategory.Hom (D := Cᵒᵖ ⥤ Type (max v u)) (F :=
          ObjectProperty.FullSubcategory.obj (P := Presheaf.IsSheaf J)) (imageMonoFactorization f).I I.I } ≫
      I.m =
    (imageMonoFactorization f).m

Tactic:
ext1
-- Module: Mathlib.CategoryTheory.Sites.Subsheaf
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
F_1 F'_1 F'' : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
G G' : Subfunctor F_1
F F' : Sheaf J (Type (max v u))
f : F ⟶ F'
I : Limits.MonoFactorisation f
⊢ Subfunctor.sheafify J (Subfunctor.range f.hom) ≤ Subfunctor.range I.m.hom

Tactic:
generalize_proofs h
-- Module: Mathlib.CategoryTheory.Sites.Subsheaf
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
F_1 F'_1 F'' : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
G G' : Subfunctor F_1
F F' : Sheaf J (Type (max v u))
f : F ⟶ F'
I : Limits.MonoFactorisation f
h : Subfunctor.sheafify J (Subfunctor.range f.hom) ≤ Subfunctor.range I.m.hom
⊢ IsIso (Subfunctor.toRange I.m.hom)

Tactic:
generalize_proofs h
-- Module: Mathlib.CategoryTheory.Sites.Subsheaf
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
F_1 F'_1 F'' : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
G G' : Subfunctor F_1
F F' : Sheaf J (Type (max v u))
f : F ⟶ F'
I : Limits.MonoFactorisation f
h : Subfunctor.sheafify J (Subfunctor.range f.hom) ≤ Subfunctor.range I.m.hom
pf : IsIso (Subfunctor.toRange I.m.hom)
h₁ :
  Subfunctor.homOfLe h ≫ inv (Subfunctor.toRange I.m.hom) ≫ I.m.hom =
    Subfunctor.homOfLe h ≫ (Subfunctor.range I.m.hom).ι
⊢ (Subfunctor.homOfLe h ≫ inv (Subfunctor.toRange I.m.hom)) ≫ I.m.hom =
    (Subfunctor.sheafify J (Subfunctor.range f.hom)).ι

Tactic:
rw [← Subfunctor.homOfLe_ι h, Category.assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Subfunctor.homOfLe_ι
-- Module: Mathlib.CategoryTheory.Sites.Subsheaf
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
F_1 F'_1 F'' : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
G G' : Subfunctor F_1
F F' : Sheaf J (Type (max v u))
f : F ⟶ F'
I : Limits.MonoFactorisation f
h : Subfunctor.sheafify J (Subfunctor.range f.hom) ≤ Subfunctor.range I.m.hom
pf : IsIso (Subfunctor.toRange I.m.hom)
h₁ : inv (Subfunctor.toRange I.m.hom) ≫ I.m.hom = (Subfunctor.range I.m.hom).ι
⊢ Subfunctor.homOfLe h ≫ inv (Subfunctor.toRange I.m.hom) ≫ I.m.hom =
    Subfunctor.homOfLe h ≫ (Subfunctor.range I.m.hom).ι

Tactic:
congr 1
-- Module: Mathlib.CategoryTheory.Sites.Subsheaf
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
F_1 F'_1 F'' : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
G G' : Subfunctor F_1
F F' : Sheaf J (Type (max v u))
f : F ⟶ F'
I : Limits.MonoFactorisation f
h : Subfunctor.sheafify J (Subfunctor.range f.hom) ≤ Subfunctor.range I.m.hom
pf : IsIso (Subfunctor.toRange I.m.hom)
h₁ : I.m.hom = Subfunctor.toRange I.m.hom ≫ (Subfunctor.range I.m.hom).ι
h₂ h₃ : I.m.hom = I.m.hom
⊢ inv (Subfunctor.toRange I.m.hom) ≫ I.m.hom = (Subfunctor.range I.m.hom).ι

Tactic:
rw [IsIso.inv_comp_eq, Subfunctor.toRange_ι]

Premises used: CategoryTheory.IsIso.inv_comp_eq, CategoryTheory.Subfunctor.toRange_ι
-- Module: Mathlib.CategoryTheory.Sites.Subsheaf
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
F F' F'' : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
G G' : Subfunctor F
⊢ Limits.HasImages (Sheaf J (Type (max v u)))

Tactic:
⟨fun f => ⟨⟨imageFactorization f⟩⟩⟩

Premises used: CategoryTheory.Limits.HasImage.mk', CategoryTheory.Limits.HasImages.mk, Nonempty.intro, CategoryTheory.imageFactorization
-- Module: Mathlib.CategoryTheory.Sites.Types
Goal:
α : Type u
⊢ discreteSieve α ∈ (typesGrothendieckTopology : (a : Type u) → Set (Sieve a)) α

Tactic:
fun x => ⟨x, fun _ => rfl⟩

Premises used: Set.Mem, setOf, Exists.intro, rfl
-- Module: Mathlib.CategoryTheory.Sites.Types
Goal:
α : Type u
⊢ Sieve.generate (discretePresieve α) ∈ (typesGrothendieckTopology : (a : Type u) → Set (Sieve a)) α

Tactic:
fun x => ⟨PUnit, 𝟙 _, ↾fun _ => x,
    ⟨PUnit.unit, fun _ => Subsingleton.elim _ _⟩, rfl⟩

Premises used: Set.Mem, setOf, CategoryTheory.CategoryStruct.id, TypeCat.ofHom, PUnit, And.intro, Exists.intro, PUnit.unit, Subsingleton.elim, rfl
-- Module: Mathlib.CategoryTheory.Sites.Types
Goal:
α β : Type u
x_1 : Sieve β
hs : x_1 ∈ (typesGrothendieckTopology : (a : Type u) → Set (Sieve a)) β
x : FamilyOfElements (Functor.obj yoneda α) x_1.arrows
hx : x.Compatible (R := x_1.arrows)
γ : Type u
f : γ ⟶ β
h : x_1.arrows f
z : Opposite.unop (Opposite.op γ)
⊢ Eq (α := α)
    ((@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
            ((ConcreteCategory.hom (FC := TypeCat.Fun)
                  (Functor.map (Functor.obj yoneda α) (Quiver.Hom.op (𝟙 PUnit.{u + 1}))) :
                (a : (fun (X : Type u) ↦ X) ((yoneda.obj α).obj (Opposite.op PUnit.{u + 1}))) →
                  (fun (X : Type u) ↦ X) ((yoneda.obj α).obj (Opposite.op PUnit.{u + 1})))
              (x
                (↾fun (x : PUnit.{u + 1}) ↦
                  (ConcreteCategory.hom (FC := TypeCat.Fun) f :
                      (a : (fun (X : Type u) ↦ X) γ) → (fun (X : Type u) ↦ X) β)
                    z)
                ⋯)) :
          (a : Opposite.unop (Opposite.op PUnit.{u + 1})) → α)
        PUnit.unit :
      α)
    ((@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
            ((ConcreteCategory.hom (FC := TypeCat.Fun)
                  (Functor.map (Functor.obj yoneda α) (Quiver.Hom.op (↾fun (x : PUnit.{u + 1}) ↦ z))) :
                (a : (fun (X : Type u) ↦ X) ((yoneda.obj α).obj (Opposite.op (Opposite.unop (Opposite.op γ))))) →
                  (fun (X : Type u) ↦ X) ((yoneda.obj α).obj (Opposite.op PUnit.{u + 1})))
              (x f h)) :
          (a : Opposite.unop (Opposite.op PUnit.{u + 1})) → α)
        PUnit.unit :
      α)

Tactic:
ConcreteCategory.congr_hom (hx (𝟙 _) (↾fun _ => z) (hs <| f z) h rfl) PUnit.unit

Premises used: CategoryTheory.ConcreteCategory.hom, CategoryTheory.CategoryStruct.id, TypeCat.ofHom, CategoryTheory.ConcreteCategory.congr_hom, DFunLike.coe, rfl
-- Module: Mathlib.CategoryTheory.Sites.Types
Goal:
α β : Type u
x_1 : Sieve β
hs : x_1 ∈ (typesGrothendieckTopology : (a : Type u) → Set (Sieve a)) β
x : FamilyOfElements (Functor.obj yoneda α) x_1.arrows
hx : x.Compatible (R := x_1.arrows)
γ : Type u
f : γ ⟶ β
h : x_1.arrows f
z : Opposite.unop (Opposite.op γ)
⊢ Eq (α := α)
    ((@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (Functor.map (Functor.obj yoneda α) f.op) :
                (a : (fun (X : Type u) ↦ X) ((yoneda.obj α).obj (Opposite.op β))) →
                  (fun (X : Type u) ↦ X) ((yoneda.obj α).obj (Opposite.op γ)))
              (↾fun (y : Opposite.unop (Opposite.op β)) ↦
                (TypeCat.Hom.hom (x (↾fun (x : PUnit.{u + 1}) ↦ y) ⋯) :
                    (a : Opposite.unop (Opposite.op PUnit.{u + 1})) → α)
                  PUnit.unit)) :
          (a : Opposite.unop (Opposite.op γ)) → α)
        z :
      α)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (x f h) : (a : Opposite.unop (Opposite.op γ)) → α) z : α)

Tactic:
convert!
        ConcreteCategory.congr_hom (hx (𝟙 _) (↾fun _ => z) (hs <| f z) h rfl) PUnit.unit using 1

Premises used: CategoryTheory.ConcreteCategory.hom, CategoryTheory.CategoryStruct.id, TypeCat.ofHom, CategoryTheory.ConcreteCategory.congr_hom, DFunLike.coe, rfl
-- Module: Mathlib.CategoryTheory.Sites.Types
Goal:
α β : Type u
x_1 : Sieve β
hs : x_1 ∈ (typesGrothendieckTopology : (a : Type u) → Set (Sieve a)) β
x : FamilyOfElements (Functor.obj yoneda α) x_1.arrows
hx : x.Compatible (R := x_1.arrows)
f : Functor.obj (Functor.obj yoneda α) (Opposite.op β)
hf : (fun (t : Functor.obj (Functor.obj yoneda α) (Opposite.op β)) ↦ x.IsAmalgamation (R := x_1.arrows) t) f
y : Opposite.unop (Opposite.op β)
⊢ Eq (α := α)
    ((@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
            ((ConcreteCategory.hom (FC := TypeCat.Fun)
                  (Functor.map (Functor.obj yoneda α) (Quiver.Hom.op (↾fun (x : PUnit.{u + 1}) ↦ y))) :
                (a : (fun (X : Type u) ↦ X) ((yoneda.obj α).obj (Opposite.op β))) →
                  (fun (X : Type u) ↦ X) ((yoneda.obj α).obj (Opposite.op PUnit.{u + 1})))
              f) :
          (a : Opposite.unop (Opposite.op PUnit.{u + 1})) → α)
        PUnit.unit :
      α)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (x (↾fun (x : PUnit.{u + 1}) ↦ y) ⋯) :
          (a : Opposite.unop (Opposite.op PUnit.{u + 1})) → α)
        PUnit.unit :
      α)

Tactic:
ConcreteCategory.congr_hom (hf _ (hs y)) PUnit.unit

Premises used: CategoryTheory.ConcreteCategory.congr_hom
-- Module: Mathlib.CategoryTheory.Sites.Types
Goal:
α β : Type u
x_1 : Sieve β
hs : x_1 ∈ (typesGrothendieckTopology : (a : Type u) → Set (Sieve a)) β
x : FamilyOfElements (Functor.obj yoneda α) x_1.arrows
hx : x.Compatible (R := x_1.arrows)
f : Functor.obj (Functor.obj yoneda α) (Opposite.op β)
hf : (fun (t : Functor.obj (Functor.obj yoneda α) (Opposite.op β)) ↦ x.IsAmalgamation (R := x_1.arrows) t) f
y : Opposite.unop (Opposite.op β)
⊢ Eq (α := α) ((ConcreteCategory.hom (FC := TypeCat.Fun) f : (a : Opposite.unop (Opposite.op β)) → α) y : α)
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (↾fun (y : Opposite.unop (Opposite.op β)) ↦
              (TypeCat.Hom.hom (x (↾fun (x : PUnit.{u + 1}) ↦ y) ⋯) :
                  (a : Opposite.unop (Opposite.op PUnit.{u + 1})) → α)
                PUnit.unit) :
          (a : Opposite.unop (Opposite.op β)) → α)
        y :
      α)

Tactic:
convert! ConcreteCategory.congr_hom (hf _ (hs y)) PUnit.unit

Premises used: CategoryTheory.ConcreteCategory.congr_hom
-- Module: Mathlib.CategoryTheory.Sites.Types
Goal:
α : Type u
rw : Presieve.IsSheaf typesGrothendieckTopology (Functor.obj yoneda α)
⊢ IsSheaf typesGrothendieckTopology (Functor.obj yoneda α)

Tactic:
rw [isSheaf_iff_isSheaf_of_type]

Premises used: CategoryTheory.isSheaf_iff_isSheaf_of_type
-- Module: Mathlib.CategoryTheory.Sites.Types
Goal:
α : Type u
⊢ Presieve.IsSheaf typesGrothendieckTopology (Functor.obj yoneda α)

Tactic:
Presieve.isSheaf_yoneda'

Premises used: CategoryTheory.Presieve.isSheaf_yoneda'
-- Module: Mathlib.CategoryTheory.Sites.Types
Goal:
α : Type u
⊢ Presieve.IsSheaf typesGrothendieckTopology (Functor.obj yoneda α)

Tactic:
exact Presieve.isSheaf_yoneda'

Premises used: CategoryTheory.Presieve.isSheaf_yoneda'
-- Module: Mathlib.CategoryTheory.Sites.Types
Goal:
⊢ yoneda' ⋙ sheafToPresheaf typesGrothendieckTopology (Type u) = yoneda

Tactic:
rfl

Premises used: CategoryTheory.Functor.comp, CategoryTheory.yoneda, rfl
-- Module: Mathlib.CategoryTheory.Sites.Types
Goal:
S : Type uᵒᵖ ⥤ Type u
hs : IsSheaf typesGrothendieckTopology S
α : Type u
f : α → S.obj (op PUnit.{u + 1})
β γ δ : Type u
g₁ : δ ⟶ β
g₂ : δ ⟶ γ
f₁ : β ⟶ α
f₂ : γ ⟶ α
hf₁ : discretePresieve α f₁
hf₂ : discretePresieve α f₂
h : g₁ ≫ f₁ = g₂ ≫ f₂
ε : Type u
g : ε ⟶ δ
h_1 : discretePresieve δ g
x : ε
h_2 : ∀ (y : ε), y = x
⊢ Eq (α := (fun (X : Type u) ↦ X) α)
    ((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) α)
    ((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) α)

Tactic:
have : f₁ (Classical.choose hf₁) = f₂ (Classical.choose hf₂) :=
        Classical.choose_spec hf₁ (g₁ <| g x) ▸
          Classical.choose_spec hf₂ (g₂ <| g x) ▸ ConcreteCategory.congr_hom h _
-- Module: Mathlib.CategoryTheory.Sites.Types
Goal:
S : Type uᵒᵖ ⥤ Type u
hs : IsSheaf typesGrothendieckTopology S
α : Type u
f : α → S.obj (op PUnit.{u + 1})
β γ δ : Type u
g₁ : δ ⟶ β
g₂ : δ ⟶ γ
f₁ : β ⟶ α
f₂ : γ ⟶ α
hf₁ : discretePresieve α f₁
hf₂ : discretePresieve α f₂
h : g₁ ≫ f₁ = g₂ ≫ f₂
ε : Type u
g : ε ⟶ δ
h_1 : discretePresieve δ g
x : ε
h_2 : ∀ (y : ε), y = x
this :
  Eq (α := (fun (X : Type u) ↦ X) α)
    ((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) α)
    ((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) α)
⊢ Eq (α := S.obj (op ε))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (S.map (Quiver.Hom.op (g ≫ g₁ ≫ ↾fun (x : β) ↦ PUnit.unit))) :
          (a : S.obj (op PUnit.{u + 1})) → S.obj (op ε))
        (f
          ((ConcreteCategory.hom (FC := TypeCat.Fun) f₂ : (a : γ) → α)
            (Classical.choose (p := fun (x : γ) ↦ ∀ (y : γ), y = x) hf₂))) :
      S.obj (op ε))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (S.map (Quiver.Hom.op (g ≫ g₂ ≫ ↾fun (x : γ) ↦ PUnit.unit))) :
          (a : S.obj (op PUnit.{u + 1})) → S.obj (op ε))
        (f
          ((ConcreteCategory.hom (FC := TypeCat.Fun) f₂ : (a : γ) → α)
            (Classical.choose (p := fun (x : γ) ↦ ∀ (y : γ), y = x) hf₂))) :
      S.obj (op ε))

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Sites.Types
Goal:
S : Type uᵒᵖ ⥤ Type u
hs : IsSheaf typesGrothendieckTopology S
α : Type u
f : α → S.obj (op PUnit.{u + 1})
h :
  ∀ (x : (fun (X : Type u) ↦ 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
⊢ (⇑(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}))) =
    f

Tactic:
funext x