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 F' : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
G : Subfunctor F
h : Presieve.IsSheaf J F'
l₁ l₂ : (sheafify J G).toFunctor ⟶ F'
e : homOfLe ⋯ ≫ l₁ = homOfLe ⋯ ≫ l₂
U : Cᵒᵖ
s : (sheafify J G).toFunctor.obj U
V : C
i : V ⟶ unop U
hi : (G.sieveOfSection (↑s : F.obj U)).arrows i
w :
  Eq (α := F'.obj (op V))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (l₁.app (op V)) :
          (a : (↑((sheafify J G).obj (op V)) : Type w)) → F'.obj (op V))
        (({
                toFun := fun (x : (↑((sheafify J G).obj U) : Type w)) ↦
                  Subtype.mk (p := fun (x : F.obj (op V)) ↦
                    Membership.mem (γ := Set (F.obj (op V))) ((sheafify J G).obj (op V)) x)
                    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map i.op) : (a : F.obj U) → F.obj (op V))
                      (↑x : F.obj U))
                    ⋯ } :
              (a : (↑((sheafify J G).obj U) : Type w)) → (↑((sheafify J G).obj (op V)) : Type w))
            s :
          (↑((sheafify J G).obj (op V)) : Type w)) :
      F'.obj (op V))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (l₂.app (op V)) :
          (a : (↑((sheafify J G).obj (op V)) : Type w)) → F'.obj (op V))
        (({
                toFun := fun (x : (↑((sheafify J G).obj U) : Type w)) ↦
                  Subtype.mk (p := fun (x : F.obj (op V)) ↦
                    Membership.mem (γ := Set (F.obj (op V))) ((sheafify J G).obj (op V)) x)
                    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map i.op) : (a : F.obj U) → F.obj (op V))
                      (↑x : F.obj U))
                    ⋯ } :
              (a : (↑((sheafify J G).obj U) : Type w)) → (↑((sheafify J G).obj (op V)) : Type w))
            s :
          (↑((sheafify J G).obj (op V)) : Type w)) :
      F'.obj (op V))
⊢ Eq (α := F'.obj (op V))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F'.map i.op) : (a : F'.obj U) → F'.obj (op V))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (l₁.app U) : (a : (↑((sheafify J G).obj U) : Type w)) → F'.obj U) s :
          F'.obj U) :
      F'.obj (op V))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F'.map i.op) : (a : F'.obj U) → F'.obj (op V))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (l₂.app U) : (a : (↑((sheafify J G).obj U) : Type w)) → F'.obj U) s :
          F'.obj U) :
      F'.obj (op V))

Tactic:
rw [← dsimp% l₁.naturality_apply, ← dsimp% l₂.naturality_apply]

Premises used: CategoryTheory.NatTrans.naturality_apply
-- Module: Mathlib.CategoryTheory.Sites.Subsheaf
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
F F' : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
G : Subfunctor F
h : Presieve.IsSheaf J F'
l₁ l₂ : (sheafify J G).toFunctor ⟶ F'
e : homOfLe ⋯ ≫ l₁ = homOfLe ⋯ ≫ l₂
U : Cᵒᵖ
s : (sheafify J G).toFunctor.obj U
V : C
i : V ⟶ unop U
hi : (G.sieveOfSection (↑s : F.obj U)).arrows i
⊢ Eq (α := F'.obj (op V))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (l₁.app (op V)) :
          (a : (↑((sheafify J G).obj (op V)) : Type w)) → F'.obj (op V))
        (({
                toFun := fun (x : (↑((sheafify J G).obj U) : Type w)) ↦
                  Subtype.mk (p := fun (x : F.obj (op V)) ↦
                    Membership.mem (γ := Set (F.obj (op V))) ((sheafify J G).obj (op V)) x)
                    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map i.op) : (a : F.obj U) → F.obj (op V))
                      (↑x : F.obj U))
                    ⋯ } :
              (a : (↑((sheafify J G).obj U) : Type w)) → (↑((sheafify J G).obj (op V)) : Type w))
            s :
          (↑((sheafify J G).obj (op V)) : Type w)) :
      F'.obj (op V))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (l₂.app (op V)) :
          (a : (↑((sheafify J G).obj (op V)) : Type w)) → F'.obj (op V))
        (({
                toFun := fun (x : (↑((sheafify J G).obj U) : Type w)) ↦
                  Subtype.mk (p := fun (x : F.obj (op V)) ↦
                    Membership.mem (γ := Set (F.obj (op V))) ((sheafify J G).obj (op V)) x)
                    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map i.op) : (a : F.obj U) → F.obj (op V))
                      (↑x : F.obj U))
                    ⋯ } :
              (a : (↑((sheafify J G).obj U) : Type w)) → (↑((sheafify J G).obj (op V)) : Type w))
            s :
          (↑((sheafify J G).obj (op V)) : Type w)) :
      F'.obj (op V))

Tactic:
ConcreteCategory.congr_hom (congr_app e <| op V) ⟨_, hi⟩

Premises used: Opposite.op, CategoryTheory.ConcreteCategory.congr_hom, CategoryTheory.congr_app
-- Module: Mathlib.CategoryTheory.Sites.Subsheaf
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
F F' : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
G : Subfunctor F
h : Presieve.IsSheaf J F'
l₁ l₂ : (sheafify J G).toFunctor ⟶ F'
e : homOfLe ⋯ ≫ l₁ = homOfLe ⋯ ≫ l₂
U : Cᵒᵖ
s : (sheafify J G).toFunctor.obj U
V : C
i : V ⟶ unop U
hi : (G.sieveOfSection (↑s : F.obj U)).arrows i
⊢ Eq (α := F'.obj (op V))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (l₁.app (op V)) :
          (a : (↑((sheafify J G).obj (op V)) : Type w)) → F'.obj (op V))
        (({
                toFun := fun (x : (↑((sheafify J G).obj U) : Type w)) ↦
                  Subtype.mk (p := fun (x : F.obj (op V)) ↦
                    Membership.mem (γ := Set (F.obj (op V))) ((sheafify J G).obj (op V)) x)
                    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map i.op) : (a : F.obj U) → F.obj (op V))
                      (↑x : F.obj U))
                    ⋯ } :
              (a : (↑((sheafify J G).obj U) : Type w)) → (↑((sheafify J G).obj (op V)) : Type w))
            s :
          (↑((sheafify J G).obj (op V)) : Type w)) :
      F'.obj (op V))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (l₂.app (op V)) :
          (a : (↑((sheafify J G).obj (op V)) : Type w)) → F'.obj (op V))
        (({
                toFun := fun (x : (↑((sheafify J G).obj U) : Type w)) ↦
                  Subtype.mk (p := fun (x : F.obj (op V)) ↦
                    Membership.mem (γ := Set (F.obj (op V))) ((sheafify J G).obj (op V)) x)
                    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map i.op) : (a : F.obj U) → F.obj (op V))
                      (↑x : F.obj U))
                    ⋯ } :
              (a : (↑((sheafify J G).obj U) : Type w)) → (↑((sheafify J G).obj (op V)) : Type w))
            s :
          (↑((sheafify J G).obj (op V)) : Type w)) :
      F'.obj (op V))

Tactic:
exact ConcreteCategory.congr_hom (congr_app e <| op V) ⟨_, hi⟩

Premises used: Opposite.op, CategoryTheory.ConcreteCategory.congr_hom, CategoryTheory.congr_app
-- Module: Mathlib.CategoryTheory.Sites.Subsheaf
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
G G' : Subfunctor F
h : G ≤ G'
hF : Presieve.IsSheaf J F
hG' : Presieve.IsSheaf.{w, v, u} J G'.toFunctor
U : Cᵒᵖ
x : F.obj U
hx : x ∈ (sheafify J G).obj U
⊢ (↑((ConcreteCategory.hom (FC := TypeCat.Fun) ((G.sheafifyLift (homOfLe h) hG').app U) :
            (a : (fun (X : Type w) ↦ X) ((sheafify J G).toFunctor.obj U)) → (fun (X : Type w) ↦ X) (G'.toFunctor.obj U))
          (Subtype.mk (p := fun (x : F.obj U) ↦ x ∈ (sheafify J G).obj U) x hx)) :
      F.obj U) ∈
    G'.obj U

Tactic:
((G.sheafifyLift (Subfunctor.homOfLe h) hG').app U ⟨x, hx⟩).2

Premises used: CategoryTheory.ConcreteCategory.hom, CategoryTheory.Subfunctor.homOfLe, Subtype.mk, CategoryTheory.Subfunctor.sheafifyLift, DFunLike.coe, CategoryTheory.NatTrans.app, Subtype.property
-- Module: Mathlib.CategoryTheory.Sites.Subsheaf
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
G G' : Subfunctor F
h : G ≤ G'
hF : Presieve.IsSheaf J F
hG' : Presieve.IsSheaf.{w, v, u} J G'.toFunctor
U : Cᵒᵖ
x : F.obj U
hx : x ∈ (sheafify J G).obj U
h₁ :
  x =
    (↑((ConcreteCategory.hom (FC := TypeCat.Fun) ((G.sheafifyLift (homOfLe h) hG').app U) :
            (a : (fun (X : Type w) ↦ X) ((sheafify J G).toFunctor.obj U)) → (fun (X : Type w) ↦ X) (G'.toFunctor.obj U))
          (Subtype.mk (p := fun (x : F.obj U) ↦ x ∈ (sheafify J G).obj U) x hx)) :
      F.obj U)
⊢ x ∈ G'.obj U

Tactic:
convert! ((G.sheafifyLift (Subfunctor.homOfLe h) hG').app U ⟨x, hx⟩).2

Premises used: CategoryTheory.ConcreteCategory.hom, CategoryTheory.Subfunctor.homOfLe, Subtype.mk, CategoryTheory.Subfunctor.sheafifyLift, DFunLike.coe, CategoryTheory.NatTrans.app, Subtype.property
-- Module: Mathlib.CategoryTheory.Sites.Subsheaf
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
G G' : Subfunctor F
h : G ≤ G'
hF : Presieve.IsSheaf J F
hG' : Presieve.IsSheaf.{w, v, u} J G'.toFunctor
U : Cᵒᵖ
x : F.obj U
hx : x ∈ (sheafify J G).obj U
h₁ :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ unop U⦄,
    (G.sieveOfSection x).arrows f →
      Eq (α := (fun (X : Type w) ↦ X) (F.obj (op Y)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f.op) :
              (a : (fun (X : Type w) ↦ X) (F.obj (op (unop U)))) → (fun (X : Type w) ↦ X) (F.obj (op Y)))
            x :
          (fun (X : Type w) ↦ X) (F.obj (op Y)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f.op) :
              (a : (fun (X : Type w) ↦ X) (F.obj (op (unop U)))) → (fun (X : Type w) ↦ X) (F.obj (op Y)))
            (↑((ConcreteCategory.hom (FC := TypeCat.Fun) ((G.sheafifyLift (homOfLe h) hG').app U) :
                    (a : (fun (X : Type w) ↦ X) ((sheafify J G).toFunctor.obj U)) →
                      (fun (X : Type w) ↦ X) (G'.toFunctor.obj U))
                  (Subtype.mk (p := fun (x : F.obj U) ↦ x ∈ (sheafify J G).obj U) x hx)) :
              F.obj U) :
          (fun (X : Type w) ↦ X) (F.obj (op Y)))
⊢ x =
    (↑((ConcreteCategory.hom (FC := TypeCat.Fun) ((G.sheafifyLift (homOfLe h) hG').app U) :
            (a : (fun (X : Type w) ↦ X) ((sheafify J G).toFunctor.obj U)) → (fun (X : Type w) ↦ X) (G'.toFunctor.obj U))
          (Subtype.mk (p := fun (x : F.obj U) ↦ x ∈ (sheafify J G).obj U) x hx)) :
      F.obj U)

Tactic:
apply (hF _ hx).isSeparatedFor.ext

Premises used: CategoryTheory.Presieve.IsSeparatedFor.ext, CategoryTheory.Presieve.IsSheafFor.isSeparatedFor
-- Module: Mathlib.CategoryTheory.Sites.Subsheaf
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
F : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
G G' : Subfunctor F
h : G ≤ G'
hF : Presieve.IsSheaf J F
hG' : Presieve.IsSheaf.{w, v, u} J G'.toFunctor
U : Cᵒᵖ
x : F.obj U
hx : x ∈ (sheafify J G).obj U
V : C
i : V ⟶ unop U
hi : (G.sieveOfSection x).arrows i
⊢ Eq.{w + 1} (α := F.obj (op V))
    ((fun (f : G.toFunctor ⟶ G'.toFunctor) ↦
        ((↑((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op V)) :
                  (a : (fun (X : Type w) ↦ X) (G.toFunctor.obj (op V))) →
                    (fun (X : Type w) ↦ X) (G'.toFunctor.obj (op V)))
                (Subtype.mk (p := fun (x : F.obj (op V)) ↦ Membership.mem (γ := Set (F.obj (op V))) (G.obj (op V)) x)
                  ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map i.op) :
                      (a : (fun (X : Type w) ↦ X) (F.obj (op (unop U)))) → (fun (X : Type w) ↦ X) (F.obj (op V)))
                    x)
                  hi)) :
            F.obj (op V)) :
          F.obj (op V)))
      (homOfLe ⋯ ≫ G.sheafifyLift (homOfLe h) hG'))
    ((fun (f : G.toFunctor ⟶ G'.toFunctor) ↦
        ((↑((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op V)) :
                  (a : (fun (X : Type w) ↦ X) (G.toFunctor.obj (op V))) →
                    (fun (X : Type w) ↦ X) (G'.toFunctor.obj (op V)))
                (Subtype.mk (p := fun (x : F.obj (op V)) ↦ Membership.mem (γ := Set (F.obj (op V))) (G.obj (op V)) x)
                  ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map i.op) :
                      (a : (fun (X : Type w) ↦ X) (F.obj (op (unop U)))) → (fun (X : Type w) ↦ X) (F.obj (op V)))
                    x)
                  hi)) :
            F.obj (op V)) :
          F.obj (op V)))
      (homOfLe h))

Tactic:
have :=
    congr_arg (fun f : G.toFunctor ⟶ G'.toFunctor => (NatTrans.app f (op V) ⟨_, hi⟩).1)
      (G.to_sheafifyLift (Subfunctor.homOfLe h) hG')
-- 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 w)
f : F ⟶ F'
rw : Presieve.IsSheaf.{w, v, u} J (Subfunctor.sheafify J (Subfunctor.range f.hom)).toFunctor
⊢ Presheaf.IsSheaf J (Subfunctor.sheafify J (Subfunctor.range f.hom)).toFunctor

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 w)
f : F ⟶ F'
hF : Presieve.IsSheaf.{w, v, u} J (F'.obj (P := Presheaf.IsSheaf J))
⊢ Presieve.IsSheaf.{w, v, u} J (Subfunctor.sheafify J (Subfunctor.range f.hom)).toFunctor

Tactic:
apply Subfunctor.sheafify_isSheaf

Premises used: CategoryTheory.Subfunctor.sheafify_isSheaf
-- 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 w)
f : F ⟶ F'
hF : Presheaf.IsSheaf J (F'.obj (P := Presheaf.IsSheaf J))
⊢ Presieve.IsSheaf.{w, v, u} 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 w)
f : F ⟶ F'
⊢ 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 w)
f : F ⟶ F'
⊢ 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 F' : Sheaf J (Type w)
f : F ⟶ F'
h : (toImage f ≫ imageι f).hom = f.hom
⊢ toImage f ≫ imageι f = f

Tactic:
ext1
-- Module: Mathlib.CategoryTheory.Sites.Subsheaf
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
F F' : Sheaf J (Type w)
f : F ⟶ F'
⊢ (toImage f ≫ imageι f).hom = f.hom

Tactic:
simp [Subfunctor.toRangeSheafify]

Premises used: CategoryTheory.Subfunctor.toRangeSheafify
-- 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 w)
f : F ⟶ F'
dsimp : Mono (Subfunctor.sheafify J (Subfunctor.range f.hom)).ι
⊢ Mono (X := Functor.obj (sheafToPresheaf J (Type w)) (Sheaf.image f))
    (Functor.map (sheafToPresheaf J (Type w)) (Sheaf.imageι f))

Tactic:
dsimp
-- 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 w)
f : F ⟶ F'
⊢ Mono (Subfunctor.sheafify J (Subfunctor.range f.hom)).ι

Tactic:
infer_instance
-- 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 w)
f : F ⟶ F'
⊢ Epi (Sheaf.toImage f)

Tactic:
⟨@fun G' g₁ g₂ e => ?_⟩

Premises used: CategoryTheory.Epi.mk
-- 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 w)
f : F ⟶ F'
refine :
  ∀ (G' : Sheaf J (Type w)) (g₁ g₂ : Sheaf.image f ⟶ G') (e : Sheaf.toImage f ≫ g₁ = Sheaf.toImage f ≫ g₂), g₁ = g₂
⊢ Epi (Sheaf.toImage f)

Tactic:
refine ⟨@fun G' g₁ g₂ 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'_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₂
h :
  ∀ (U : Cᵒᵖ) (s : F'.obj (P := Presheaf.IsSheaf J).obj U)
    (hx : s ∈ (Subfunctor.sheafify J (Subfunctor.range f.hom)).obj U),
    (ConcreteCategory.hom (FC := TypeCat.Fun) (g₁.hom.app U)).toFun
        (Subtype.mk (p := fun (x : F'.obj (P := Presheaf.IsSheaf J).obj U) ↦
          x ∈ (Subfunctor.sheafify J (Subfunctor.range f.hom)).obj U) s hx) =
      (ConcreteCategory.hom (FC := TypeCat.Fun) (g₂.hom.app U)).toFun
        (Subtype.mk (p := fun (x : F'.obj (P := Presheaf.IsSheaf J).obj U) ↦
          x ∈ (Subfunctor.sheafify J (Subfunctor.range f.hom)).obj U) s hx)
⊢ g₁ = g₂

Tactic:
ext U ⟨s, hx⟩
-- 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
h :
  ∀ ⦃Y : C⦄ ⦃f_1 : Y ⟶ unop U⦄,
    ((Subfunctor.range f.hom).sieveOfSection s).arrows f_1 →
      Eq (α := (fun (X : Type w) ↦ X) (G'.obj (P := Presheaf.IsSheaf J).obj (op Y)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (G'.obj (P := Presheaf.IsSheaf J).map f_1.op) :
              (a : (fun (X : Type w) ↦ X) (G'.obj.obj (op (unop U)))) → (fun (X : Type w) ↦ X) (G'.obj.obj (op Y)))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (g₁.hom.app U)).toFun
              (Subtype.mk (p := fun (x : F'.obj (P := Presheaf.IsSheaf J).obj U) ↦
                x ∈ (Subfunctor.sheafify J (Subfunctor.range f.hom)).obj U) s hx)) :
          (fun (X : Type w) ↦ X) (G'.obj (P := Presheaf.IsSheaf J).obj (op Y)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (G'.obj (P := Presheaf.IsSheaf J).map f_1.op) :
              (a : (fun (X : Type w) ↦ X) (G'.obj.obj (op (unop U)))) → (fun (X : Type w) ↦ X) (G'.obj.obj (op Y)))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (g₂.hom.app U)).toFun
              (Subtype.mk (p := fun (x : F'.obj (P := Presheaf.IsSheaf J).obj U) ↦
                x ∈ (Subfunctor.sheafify J (Subfunctor.range f.hom)).obj U) s hx)) :
          (fun (X : Type w) ↦ X) (G'.obj (P := Presheaf.IsSheaf J).obj (op Y)))
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (g₁.hom.app U)).toFun
      (Subtype.mk (p := fun (x : F'.obj (P := Presheaf.IsSheaf J).obj U) ↦
        x ∈ (Subfunctor.sheafify J (Subfunctor.range f.hom)).obj U) s hx) =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (g₂.hom.app U)).toFun
      (Subtype.mk (p := fun (x : F'.obj (P := Presheaf.IsSheaf J).obj U) ↦
        x ∈ (Subfunctor.sheafify J (Subfunctor.range f.hom)).obj U) s hx)

Tactic:
apply ((isSheaf_iff_isSheaf_of_type J _).mp G'.2 _ hx).isSeparatedFor.ext

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.property, CategoryTheory.Presieve.IsSeparatedFor.ext, CategoryTheory.Presieve.IsSheafFor.isSeparatedFor, CategoryTheory.isSheaf_iff_isSheaf_of_type, Iff.mp
-- 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)))
⊢ 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)))

Tactic:
have E : (Sheaf.toImage f).hom.app (op V) y = (Sheaf.image f).obj.map i.op ⟨s, hx⟩ :=
    Subtype.ext e'