awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Subsheaf (goal)
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
f : G.toFunctor ⟶ F'
h : Presieve.IsSheaf J F'
U V : Cᵒᵖ
i : U ⟶ V
s : (sheafify J G).toFunctor.obj U
W : C
j : W ⟶ unop V
hj :
  Sieve.arrows
    (G.sieveOfSection
      (↑((ConcreteCategory.hom (FC := TypeCat.Fun) ((sheafify J G).toFunctor.map i) :
              (a : (fun (X : Type w) ↦ X) ((sheafify J G).toFunctor.obj U)) →
                (fun (X : Type w) ↦ X) ((sheafify J G).toFunctor.obj V))
            s) :
        F.obj V))
    j
⊢ Eq (α := F'.obj (op W))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op W)) : (a : (↑(G.obj (op W)) : Type w)) → F'.obj (op W))
        (G.familyOfElementsOfSection
          (↑(({
                    toFun := fun (x : (↑((sheafify J G).obj U) : Type w)) ↦
                      Subtype.mk (p := fun (x : F.obj V) ↦ x ∈ (sheafify J G).obj V)
                        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map i) : (a : F.obj U) → F.obj V) (↑x : F.obj U))
                        ⋯ :
                    TypeCat.Fun (↑((sheafify J G).obj U) : Type w) (↑((sheafify J G).obj V) : Type w) } :
                  (a : (↑((sheafify J G).obj U) : Type w)) → (↑((sheafify J G).obj V) : Type w))
                s) :
            F.obj V)
          j hj) :
      F'.obj (op W))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F'.map j.op) : (a : F'.obj V) → F'.obj (op W))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F'.map i) : (a : F'.obj U) → F'.obj V)
            (⋯.amalgamate (R := (G.sieveOfSection (↑s : F.obj U)).arrows)
              ((G.familyOfElementsOfSection (↑s : F.obj U)).map (R := (G.sieveOfSection (↑s : F.obj U)).arrows) f) ⋯) :
          F'.obj V) :
      F'.obj (op W))
have h₁ : Eq (α := F'.obj (op W))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op W)) : (a : (↑(G.obj (op W)) : Type w)) → F'.obj (op W))
      (G.familyOfElementsOfSection
        (↑(({
                  toFun := fun (x : (↑((sheafify J G).obj U) : Type w)) ↦
                    Subtype.mk (p := fun (x : F.obj V) ↦ x ∈ (sheafify J G).obj V)
                      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map i) : (a : F.obj U) → F.obj V) (↑x : F.obj U))
                      sorry :
                  TypeCat.Fun (↑((sheafify J G).obj U) : Type w) (↑((sheafify J G).obj V) : Type w) } :
                (a : (↑((sheafify J G).obj U) : Type w)) → (↑((sheafify J G).obj V) : Type w))
              s) :
          F.obj V)
        j hj) :
    F'.obj (op W))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (F'.map (i ≫ j.op)) : (a : F'.obj U) → F'.obj (op W))
      (sorry.amalgamate (R := (G.sieveOfSection (↑s : F.obj U)).arrows)
        ((G.familyOfElementsOfSection (↑s : F.obj U)).map (R := (G.sieveOfSection (↑s : F.obj U)).arrows) f) sorry) :
    F'.obj (op W))
Tactic: simp only [← comp_apply, ← Functor.map_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Subsheaf (goal)
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
f : G.toFunctor ⟶ F'
h : Presieve.IsSheaf J F'
U V : Cᵒᵖ
i : U ⟶ V
s : (sheafify J G).toFunctor.obj U
W : C
j : W ⟶ unop V
hj :
  Sieve.arrows
    (G.sieveOfSection
      (↑((ConcreteCategory.hom (FC := TypeCat.Fun) ((sheafify J G).toFunctor.map i) :
              (a : (fun (X : Type w) ↦ X) ((sheafify J G).toFunctor.obj U)) →
                (fun (X : Type w) ↦ X) ((sheafify J G).toFunctor.obj V))
            s) :
        F.obj V))
    j
⊢ Eq (α := F'.obj (op W))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op W)) : (a : (↑(G.obj (op W)) : Type w)) → F'.obj (op W))
        (G.familyOfElementsOfSection
          (↑(({
                    toFun := fun (x : (↑((sheafify J G).obj U) : Type w)) ↦
                      Subtype.mk (p := fun (x : F.obj V) ↦ x ∈ (sheafify J G).obj V)
                        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map i) : (a : F.obj U) → F.obj V) (↑x : F.obj U))
                        ⋯ :
                    TypeCat.Fun (↑((sheafify J G).obj U) : Type w) (↑((sheafify J G).obj V) : Type w) } :
                  (a : (↑((sheafify J G).obj U) : Type w)) → (↑((sheafify J G).obj V) : Type w))
                s) :
            F.obj V)
          j hj) :
      F'.obj (op W))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F'.map (i ≫ j.op)) : (a : F'.obj U) → F'.obj (op W))
        (⋯.amalgamate (R := (G.sieveOfSection (↑s : F.obj U)).arrows)
          ((G.familyOfElementsOfSection (↑s : F.obj U)).map (R := (G.sieveOfSection (↑s : F.obj U)).arrows) f) ⋯) :
      F'.obj (op W))
have h₁ : Eq (α := (fun (X : Type w) ↦ X) (F'.obj (op W)))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op W)) : (a : (↑(G.obj (op W)) : Type w)) → F'.obj (op W))
      (G.familyOfElementsOfSection
        (↑(({
                  toFun := fun (x : (↑((sheafify J G).obj U) : Type w)) ↦
                    Subtype.mk (p := fun (x : F.obj V) ↦ x ∈ (sheafify J G).obj V)
                      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map i) : (a : F.obj U) → F.obj V) (↑x : F.obj U))
                      sorry :
                  TypeCat.Fun (↑((sheafify J G).obj U) : Type w) (↑((sheafify J G).obj V) : Type w) } :
                (a : (↑((sheafify J G).obj U) : Type w)) → (↑((sheafify J G).obj V) : Type w))
              s) :
          F.obj V)
        j hj) :
    F'.obj (op W))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (F'.map (j ≫ i.unop).op) :
        (a : (fun (X : Type w) ↦ X) (F'.obj (op (unop U)))) → (fun (X : Type w) ↦ X) (F'.obj (op W)))
      (sorry.amalgamate (R := (G.sieveOfSection (↑s : F.obj U)).arrows)
        ((G.familyOfElementsOfSection (↑s : F.obj U)).map (R := (G.sieveOfSection (↑s : F.obj U)).arrows) f) sorry) :
    (fun (X : Type w) ↦ X) (F'.obj (op W)))
Tactic: change _ = F'.map (j ≫ i.unop).op _
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Subsheaf (goal)
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
f : G.toFunctor ⟶ F'
h : Presieve.IsSheaf J F'
U V : Cᵒᵖ
i : U ⟶ V
s : (sheafify J G).toFunctor.obj U
W : C
j : W ⟶ unop V
hj :
  Sieve.arrows
    (G.sieveOfSection
      (↑((ConcreteCategory.hom (FC := TypeCat.Fun) ((sheafify J G).toFunctor.map i) :
              (a : (fun (X : Type w) ↦ X) ((sheafify J G).toFunctor.obj U)) →
                (fun (X : Type w) ↦ X) ((sheafify J G).toFunctor.obj V))
            s) :
        F.obj V))
    j
⊢ Eq (α := (fun (X : Type w) ↦ X) (F'.obj (op W)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op W)) : (a : (↑(G.obj (op W)) : Type w)) → F'.obj (op W))
        (G.familyOfElementsOfSection
          (↑(({
                    toFun := fun (x : (↑((sheafify J G).obj U) : Type w)) ↦
                      Subtype.mk (p := fun (x : F.obj V) ↦ x ∈ (sheafify J G).obj V)
                        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map i) : (a : F.obj U) → F.obj V) (↑x : F.obj U))
                        ⋯ :
                    TypeCat.Fun (↑((sheafify J G).obj U) : Type w) (↑((sheafify J G).obj V) : Type w) } :
                  (a : (↑((sheafify J G).obj U) : Type w)) → (↑((sheafify J G).obj V) : Type w))
                s) :
            F.obj V)
          j hj) :
      F'.obj (op W))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F'.map (j ≫ i.unop).op) :
          (a : (fun (X : Type w) ↦ X) (F'.obj (op (unop U)))) → (fun (X : Type w) ↦ X) (F'.obj (op W)))
        (⋯.amalgamate (R := (G.sieveOfSection (↑s : F.obj U)).arrows)
          ((G.familyOfElementsOfSection (↑s : F.obj U)).map (R := (G.sieveOfSection (↑s : F.obj U)).arrows) f) ⋯) :
      (fun (X : Type w) ↦ X) (F'.obj (op W)))
have h₁ : (ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op W)) : (a : (↑(G.obj (op W)) : Type w)) → F'.obj (op W))
    (G.familyOfElementsOfSection
      (↑(({
                toFun := fun (x : (↑((sheafify J G).obj U) : Type w)) ↦
                  Subtype.mk (p := fun (x : F.obj V) ↦ x ∈ (sheafify J G).obj V)
                    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map i) : (a : F.obj U) → F.obj V) (↑x : F.obj U)) sorry :
                TypeCat.Fun (↑((sheafify J G).obj U) : Type w) (↑((sheafify J G).obj V) : Type w) } :
              (a : (↑((sheafify J G).obj U) : Type w)) → (↑((sheafify J G).obj V) : Type w))
            s) :
        F.obj V)
      j hj) =
  (G.familyOfElementsOfSection (↑s : F.obj U)).map (R := (G.sieveOfSection (↑s : F.obj U)).arrows) f (j ≫ i.unop) sorry
Tactic: refine Eq.trans ?_ (Presieve.IsSheafFor.valid_glue (h _ s.2)
      ((G.family_of_elements_compatible s.1).map f) (j ≫ i.unop) ?_).symm
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Subsheaf (goal)
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
f : G.toFunctor ⟶ F'
h : Presieve.IsSheaf J F'
U V : Cᵒᵖ
i : U ⟶ V
s : (sheafify J G).toFunctor.obj U
W : C
j : W ⟶ unop V
hj :
  Sieve.arrows
    (G.sieveOfSection
      (↑((ConcreteCategory.hom (FC := TypeCat.Fun) ((sheafify J G).toFunctor.map i) :
              (a : (fun (X : Type w) ↦ X) ((sheafify J G).toFunctor.obj U)) →
                (fun (X : Type w) ↦ X) ((sheafify J G).toFunctor.obj V))
            s) :
        F.obj V))
    j
h₁ :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op W)) : (a : (↑(G.obj (op W)) : Type w)) → F'.obj (op W))
      (G.familyOfElementsOfSection
        (↑(({
                  toFun := fun (x : (↑((sheafify J G).obj U) : Type w)) ↦
                    Subtype.mk (p := fun (x : F.obj V) ↦ x ∈ (sheafify J G).obj V)
                      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map i) : (a : F.obj U) → F.obj V) (↑x : F.obj U))
                      ⋯ :
                  TypeCat.Fun (↑((sheafify J G).obj U) : Type w) (↑((sheafify J G).obj V) : Type w) } :
                (a : (↑((sheafify J G).obj U) : Type w)) → (↑((sheafify J G).obj V) : Type w))
              s) :
          F.obj V)
        j hj) =
    (G.familyOfElementsOfSection (↑s : F.obj U)).map (R := (G.sieveOfSection (↑s : F.obj U)).arrows) f (j ≫ i.unop) ⋯
⊢ Eq (α := (fun (X : Type w) ↦ X) (F'.obj (op W)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op W)) : (a : (↑(G.obj (op W)) : Type w)) → F'.obj (op W))
        (G.familyOfElementsOfSection
          (↑(({
                    toFun := fun (x : (↑((sheafify J G).obj U) : Type w)) ↦
                      Subtype.mk (p := fun (x : F.obj V) ↦ x ∈ (sheafify J G).obj V)
                        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map i) : (a : F.obj U) → F.obj V) (↑x : F.obj U))
                        ⋯ :
                    TypeCat.Fun (↑((sheafify J G).obj U) : Type w) (↑((sheafify J G).obj V) : Type w) } :
                  (a : (↑((sheafify J G).obj U) : Type w)) → (↑((sheafify J G).obj V) : Type w))
                s) :
            F.obj V)
          j hj) :
      F'.obj (op W))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F'.map (j ≫ i.unop).op) :
          (a : (fun (X : Type w) ↦ X) (F'.obj (op (unop U)))) → (fun (X : Type w) ↦ X) (F'.obj (op W)))
        (⋯.amalgamate (R := (G.sieveOfSection (↑s : F.obj U)).arrows)
          ((G.familyOfElementsOfSection (↑s : F.obj U)).map (R := (G.sieveOfSection (↑s : F.obj U)).arrows) f) ⋯) :
      (fun (X : Type w) ↦ X) (F'.obj (op W)))
have h₂ : (G.sieveOfSection (↑s : F.obj U)).arrows (j ≫ i.unop)
Tactic: refine Eq.trans ?_ (Presieve.IsSheafFor.valid_glue (h _ s.2)
      ((G.family_of_elements_compatible s.1).map f) (j ≫ i.unop) ?_).symm
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Subsheaf (goal)
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
f : G.toFunctor ⟶ F'
h : Presieve.IsSheaf J F'
U V : Cᵒᵖ
i : U ⟶ V
s : (sheafify J G).toFunctor.obj U
W : C
j : W ⟶ unop V
hj :
  Sieve.arrows
    (G.sieveOfSection
      (↑((ConcreteCategory.hom (FC := TypeCat.Fun) ((sheafify J G).toFunctor.map i) :
              (a : (fun (X : Type w) ↦ X) ((sheafify J G).toFunctor.obj U)) →
                (fun (X : Type w) ↦ X) ((sheafify J G).toFunctor.obj V))
            s) :
        F.obj V))
    j
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op W)) : (a : (↑(G.obj (op W)) : Type w)) → F'.obj (op W))
      (G.familyOfElementsOfSection
        (↑(({
                  toFun := fun (x : (↑((sheafify J G).obj U) : Type w)) ↦
                    Subtype.mk (p := fun (x : F.obj V) ↦ x ∈ (sheafify J G).obj V)
                      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map i) : (a : F.obj U) → F.obj V) (↑x : F.obj U))
                      ⋯ :
                  TypeCat.Fun (↑((sheafify J G).obj U) : Type w) (↑((sheafify J G).obj V) : Type w) } :
                (a : (↑((sheafify J G).obj U) : Type w)) → (↑((sheafify J G).obj V) : Type w))
              s) :
          F.obj V)
        j hj) =
    (G.familyOfElementsOfSection (↑s : F.obj U)).map (R := (G.sieveOfSection (↑s : F.obj U)).arrows) f (j ≫ i.unop) ⋯
have h₁ : Eq (α := F'.obj (op W))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op W)) : (a : (↑(G.obj (op W)) : Type w)) → F'.obj (op W))
      (Subtype.mk (p := fun (x : F.obj (op W)) ↦ Membership.mem (γ := Set (F.obj (op W))) (G.obj (op W)) x)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map j.op) : (a : F.obj V) → F.obj (op W))
            (↑(({
                      toFun := fun (x : (↑((sheafify J G).obj U) : Type w)) ↦
                        Subtype.mk (p := fun (x : F.obj V) ↦ x ∈ (sheafify J G).obj V)
                          ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map i) : (a : F.obj U) → F.obj V)
                            (↑x : F.obj U))
                          sorry } :
                    (a : (↑((sheafify J G).obj U) : Type w)) → (↑((sheafify J G).obj V) : Type w))
                  s) :
              F.obj V))
          hj :
        { x : F.obj (op W) // Membership.mem (γ := Set (F.obj (op W))) (G.obj (op W)) x }) :
    F'.obj (op W))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op W)) : (a : (↑(G.obj (op W)) : Type w)) → F'.obj (op W))
      (Subtype.mk (p := fun (x : F.obj (op W)) ↦ Membership.mem (γ := Set (F.obj (op W))) (G.obj (op W)) x)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map j.op) : (a : F.obj V) → F.obj (op W))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map i) : (a : F.obj U) → F.obj V) (↑s : F.obj U) : F.obj V))
          sorry :
        { x : F.obj (op W) // Membership.mem (γ := Set (F.obj (op W))) (G.obj (op W)) x }) :
    F'.obj (op W))
Tactic: simp [Presieve.FamilyOfElements.map, Subfunctor.familyOfElementsOfSection]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Subsheaf (goal)
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
f : G.toFunctor ⟶ F'
h : Presieve.IsSheaf J F'
U V : Cᵒᵖ
i : U ⟶ V
s : (sheafify J G).toFunctor.obj U
W : C
j : W ⟶ unop V
hj :
  Sieve.arrows
    (G.sieveOfSection
      (↑((ConcreteCategory.hom (FC := TypeCat.Fun) ((sheafify J G).toFunctor.map i) :
              (a : (fun (X : Type w) ↦ X) ((sheafify J G).toFunctor.obj U)) →
                (fun (X : Type w) ↦ X) ((sheafify J G).toFunctor.obj V))
            s) :
        F.obj V))
    j
⊢ (G.sieveOfSection (↑s : F.obj U)).arrows (j ≫ i.unop)
have h₁ : Membership.mem (α := F.obj (op W)) (γ := Set (F.obj (op W))) (G.obj (op W))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (i ≫ j.op)) : (a : F.obj U) → F.obj (op W)) (↑s : F.obj U) :
    F.obj (op W))
Tactic: dsimp [Presieve.FamilyOfElements.map] at hj ⊢
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Subsheaf (goal)
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
f : G.toFunctor ⟶ F'
h : Presieve.IsSheaf J F'
U V : Cᵒᵖ
i : U ⟶ V
s : (sheafify J G).toFunctor.obj U
W : C
j : W ⟶ unop V
hj :
  Membership.mem (α := F.obj (op W)) (γ := Set (F.obj (op W))) (G.obj (op W))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map j.op) : (a : F.obj V) → F.obj (op W))
        (↑(({
                  toFun := fun (x : (↑((sheafify J G).obj U) : Type w)) ↦
                    Subtype.mk (p := fun (x : F.obj V) ↦ x ∈ (sheafify J G).obj V)
                      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map i) : (a : F.obj U) → F.obj V) (↑x : F.obj U))
                      ⋯ } :
                (a : (↑((sheafify J G).obj U) : Type w)) → (↑((sheafify J G).obj V) : Type w))
              s) :
          F.obj V) :
      F.obj (op W))
⊢ Membership.mem (α := F.obj (op W)) (γ := Set (F.obj (op W))) (G.obj (op W))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (i ≫ j.op)) : (a : F.obj U) → F.obj (op W)) (↑s : F.obj U) :
      F.obj (op W))
have h₁ : Membership.mem (α := F.obj (op W)) (γ := Set (F.obj (op W))) (G.obj (op W))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map i ≫ F.map j.op) : (a : F.obj U) → F.obj (op W)) (↑s : F.obj U) :
    F.obj (op W))
Tactic: rwa [Functor.map_comp, comp_apply]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Subsheaf (goal)
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
f : G.toFunctor ⟶ F'
h : Presieve.IsSheaf J F'
U V : Cᵒᵖ
i : U ⟶ V
s : (sheafify J G).toFunctor.obj U
W : C
j : W ⟶ unop V
hj :
  Membership.mem (α := F.obj (op W)) (γ := Set (F.obj (op W))) (G.obj (op W))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map j.op) : (a : F.obj V) → F.obj (op W))
        (↑(({
                  toFun := fun (x : (↑((sheafify J G).obj U) : Type w)) ↦
                    Subtype.mk (p := fun (x : F.obj V) ↦ x ∈ (sheafify J G).obj V)
                      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map i) : (a : F.obj U) → F.obj V) (↑x : F.obj U))
                      ⋯ } :
                (a : (↑((sheafify J G).obj U) : Type w)) → (↑((sheafify J G).obj V) : Type w))
              s) :
          F.obj V) :
      F.obj (op W))
h₁ :
  Membership.mem (α := F.obj (op W)) (γ := Set (F.obj (op W))) (G.obj (op W))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map i ≫ F.map j.op) : (a : F.obj U) → F.obj (op W)) (↑s : F.obj U) :
      F.obj (op W))
⊢ Membership.mem (α := F.obj (op W)) (γ := Set (F.obj (op W))) (G.obj (op W))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (i ≫ j.op)) : (a : F.obj U) → F.obj (op W)) (↑s : F.obj U) :
      F.obj (op W))
have h₂ : Membership.mem (α := F.obj (op W)) (γ := Set (F.obj (op W))) (G.obj (op W))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map j.op) : (a : F.obj V) → F.obj (op W))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map i) : (a : F.obj U) → F.obj V) (↑s : F.obj U) : F.obj V) :
    F.obj (op W))
Tactic: rwa [Functor.map_comp, comp_apply]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Subsheaf (goal)
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
f : G.toFunctor ⟶ F'
h : Presieve.IsSheaf J F'
⊢ homOfLe ⋯ ≫ G.sheafifyLift f h = f
have w : ∀ (U : Cᵒᵖ) (s : G.toFunctor.obj U),
  (ConcreteCategory.hom (FC := TypeCat.Fun) ((homOfLe sorry ≫ G.sheafifyLift f h).app U)).toFun s =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (f.app U)).toFun s
Tactic: ext U s
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Subsheaf (goal)
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
f : G.toFunctor ⟶ F'
h : Presieve.IsSheaf J F'
U : Cᵒᵖ
s : G.toFunctor.obj U
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) ((homOfLe ⋯ ≫ G.sheafifyLift f h).app U)).toFun s =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (f.app U)).toFun s
have w : ∀ ⦃Y : C⦄ ⦃f_1 : Y ⟶ unop U⦄,
  Sieve.arrows
      (G.sieveOfSection
        (↑((ConcreteCategory.hom (FC := TypeCat.Fun) ((homOfLe sorry).app U) :
                (a : (fun (X : Type w) ↦ X) (G.toFunctor.obj U)) →
                  (fun (X : Type w) ↦ X) ((sheafify J G).toFunctor.obj U))
              s) :
          F.obj U))
      f_1 →
    Eq (α := (fun (X : Type w) ↦ X) (F'.obj (op Y)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F'.map f_1.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) ((homOfLe sorry ≫ G.sheafifyLift f h).app U)).toFun s) :
        (fun (X : Type w) ↦ X) (F'.obj (op Y)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F'.map f_1.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) (f.app U)).toFun s) :
        (fun (X : Type w) ↦ X) (F'.obj (op Y)))
Tactic: apply (h _ ((Subfunctor.homOfLe (G.le_sheafify J)).app U s).prop).isSeparatedFor.ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Subsheaf (hypothesis)
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
f : G.toFunctor ⟶ F'
h : Presieve.IsSheaf J F'
U : Cᵒᵖ
s : G.toFunctor.obj U
V : C
i : V ⟶ unop U
hi :
  Sieve.arrows
    (G.sieveOfSection
      (↑((ConcreteCategory.hom (FC := TypeCat.Fun) ((homOfLe ⋯).app U) :
              (a : (fun (X : Type w) ↦ X) (G.toFunctor.obj U)) →
                (fun (X : Type w) ↦ X) ((sheafify J G).toFunctor.obj U))
            s) :
        F.obj U))
    i
⊢ Eq (α := (fun (X : Type w) ↦ X) (F'.obj (op V)))
    ((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)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) ((homOfLe ⋯ ≫ G.sheafifyLift f h).app U)).toFun s) :
      (fun (X : Type w) ↦ X) (F'.obj (op V)))
    ((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)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app U)).toFun s) :
      (fun (X : Type w) ↦ X) (F'.obj (op V)))
have this : ∀ ⦃X Y : Cᵒᵖ⦄ (f_1 : X ⟶ Y) (x : G.toFunctor.obj X),
  Eq (α := F'.obj Y)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app Y) : (a : G.toFunctor.obj Y) → F'.obj Y)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (G.toFunctor.map f_1) : (a : G.toFunctor.obj X) → G.toFunctor.obj Y)
            x :
          G.toFunctor.obj Y) :
      F'.obj Y)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F'.map f_1) : (a : F'.obj X) → F'.obj Y)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app X) : (a : G.toFunctor.obj X) → F'.obj X) x : F'.obj X) :
      F'.obj Y)
Tactic: have := elementwise_of% f.naturality
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Subsheaf (goal)
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₂
⊢ l₁ = l₂
have w : ∀ (U : Cᵒᵖ) (s : (sheafify J G).toFunctor.obj U),
  (ConcreteCategory.hom (FC := TypeCat.Fun) (l₁.app U)).toFun s =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (l₂.app U)).toFun s
Tactic: ext U s