-- Mathlib/Topology/Sheaves/LocalPredicate.lean
theorem isSheaf (P : LocalPredicate T) : (subpresheafToTypes P.toPrelocalPredicate).IsSheaf :=
  Presheaf.isSheaf_of_isSheafUniqueGluing_types.{v} _ fun ι U sf sf_comp => by
    -- We show the sheaf condition in terms of unique gluing.
    -- First we obtain a family of sections for the underlying sheaf of functions,
    -- by forgetting that the predicate holds
    let sf' : ∀ i : ι, (presheafToTypes X T).obj (op (U i)) := fun i => (sf i).val
    -- Since our original family is compatible, this one is as well
    have sf'_comp : (presheafToTypes X T).IsCompatible U sf' := fun i j =>
      congr_arg Subtype.val (sf_comp i j)
    -- So, we can obtain a unique gluing
    obtain ⟨gl, gl_spec, gl_uniq⟩ := (sheafToTypes X T).existsUnique_gluing U sf'
      -- `by exact` to help Lean infer the `ConcreteCategory` instance
      (by exact sf'_comp)
    refine ⟨⟨gl, ?_⟩, ?_, ?_⟩
    · -- Our first goal is to show that this chosen gluing satisfies the
      -- predicate. Of course, we use locality of the predicate.
      apply P.locality
      rintro ⟨x, mem⟩
      -- Once we're at a particular point `x`, we can select some open set `x ∈ U i`.
      choose i hi using Opens.mem_iSup.mp mem
      -- We claim that the predicate holds in `U i`
      use U i, hi, Opens.leSupr U i
      -- This follows, since our original family `sf` satisfies the predicate
      convert (sf i).property using 1
      exact gl_spec i

    -- It remains to show that the chosen lift is really a gluing for the subsheaf and
    -- that it is unique. Both of which follow immediately from the corresponding facts
    -- in the sheaf of functions without the local predicate.
    · exact fun i => Subtype.ext (gl_spec i)
    · intro gl' hgl'
      refine Subtype.ext ?_
      exact gl_uniq gl'.1 fun i => congr_arg Subtype.val (hgl' i)

Proof state:
case intro.intro.refine_1
X : TopCat
T : ↑X → Type v
P : LocalPredicate T
ι : Type v
U : ι → Opens ↑X
sf : (i : ι) → ToType ((subpresheafToTypes P.toPrelocalPredicate).obj (op (U i)))
sf_comp : (subpresheafToTypes P.toPrelocalPredicate).IsCompatible U sf
sf' : (i : ι) → (X.presheafToTypes T).obj (op (U i)) := fun i => ↑(sf i)
sf'_comp : (X.presheafToTypes T).IsCompatible U sf'
gl : ToType ((X.sheafToTypes T).val.obj (op (iSup U)))
gl_spec : IsGluing (X.sheafToTypes T).val U sf' gl
gl_uniq :
  ∀ (y : ToType ((X.sheafToTypes T).val.obj (op (iSup U)))),
    (fun s => IsGluing (X.sheafToTypes T).val U sf' s) y → y = gl
⊢ P.pred gl

Tactic:
apply P.locality

Result:
case intro.intro.refine_1.x
X : TopCat
T : ↑X → Type v
P : LocalPredicate T
ι : Type v
U : ι → Opens ↑X
sf : (i : ι) → ToType ((subpresheafToTypes P.toPrelocalPredicate).obj (op (U i)))
sf_comp : (subpresheafToTypes P.toPrelocalPredicate).IsCompatible U sf
sf' : (i : ι) → (X.presheafToTypes T).obj (op (U i)) := fun i => ↑(sf i)
sf'_comp : (X.presheafToTypes T).IsCompatible U sf'
gl : ToType ((X.sheafToTypes T).val.obj (op (iSup U)))
gl_spec : IsGluing (X.sheafToTypes T).val U sf' gl
gl_uniq :
  ∀ (y : ToType ((X.sheafToTypes T).val.obj (op (iSup U)))),
    (fun s => IsGluing (X.sheafToTypes T).val U sf' s) y → y = gl
⊢ ∀ (x : ↥(unop (op (iSup U)))), ∃ V, ∃ (_ : ↑x ∈ V), ∃ i, P.pred fun x => gl (i x)

Proof state:
case intro.intro.refine_3
X : TopCat
T : ↑X → Type v
P : LocalPredicate T
ι : Type v
U : ι → Opens ↑X
sf : (i : ι) → ToType ((subpresheafToTypes P.toPrelocalPredicate).obj (op (U i)))
sf_comp : (subpresheafToTypes P.toPrelocalPredicate).IsCompatible U sf
sf' : (i : ι) → (X.presheafToTypes T).obj (op (U i)) := fun i => ↑(sf i)
sf'_comp : (X.presheafToTypes T).IsCompatible U sf'
gl : ToType ((X.sheafToTypes T).val.obj (op (iSup U)))
gl_spec : IsGluing (X.sheafToTypes T).val U sf' gl
gl_uniq :
  ∀ (y : ToType ((X.sheafToTypes T).val.obj (op (iSup U)))),
    (fun s => IsGluing (X.sheafToTypes T).val U sf' s) y → y = gl
⊢ ∀ (y : ToType ((subpresheafToTypes P.toPrelocalPredicate).obj (op (iSup U)))),
    (fun s => (subpresheafToTypes P.toPrelocalPredicate).IsGluing U sf s) y → y = ⟨gl, ⋯⟩

Tactic:
intro gl' hgl'

Result:
case intro.intro.refine_3
X : TopCat
T : ↑X → Type v
P : LocalPredicate T
ι : Type v
U : ι → Opens ↑X
sf : (i : ι) → ToType ((subpresheafToTypes P.toPrelocalPredicate).obj (op (U i)))
sf_comp : (subpresheafToTypes P.toPrelocalPredicate).IsCompatible U sf
sf' : (i : ι) → (X.presheafToTypes T).obj (op (U i)) := fun i => ↑(sf i)
sf'_comp : (X.presheafToTypes T).IsCompatible U sf'
gl : ToType ((X.sheafToTypes T).val.obj (op (iSup U)))
gl_spec : IsGluing (X.sheafToTypes T).val U sf' gl
gl_uniq :
  ∀ (y : ToType ((X.sheafToTypes T).val.obj (op (iSup U)))),
    (fun s => IsGluing (X.sheafToTypes T).val U sf' s) y → y = gl
gl' : ToType ((subpresheafToTypes P.toPrelocalPredicate).obj (op (iSup U)))
hgl' : (subpresheafToTypes P.toPrelocalPredicate).IsGluing U sf gl'
⊢ gl' = ⟨gl, ⋯⟩

Proof state:
case intro.intro.refine_3
X : TopCat
T : ↑X → Type v
P : LocalPredicate T
ι : Type v
U : ι → Opens ↑X
sf : (i : ι) → ToType ((subpresheafToTypes P.toPrelocalPredicate).obj (op (U i)))
sf_comp : (subpresheafToTypes P.toPrelocalPredicate).IsCompatible U sf
sf' : (i : ι) → (X.presheafToTypes T).obj (op (U i)) := fun i => ↑(sf i)
sf'_comp : (X.presheafToTypes T).IsCompatible U sf'
gl : ToType ((X.sheafToTypes T).val.obj (op (iSup U)))
gl_spec : IsGluing (X.sheafToTypes T).val U sf' gl
gl_uniq :
  ∀ (y : ToType ((X.sheafToTypes T).val.obj (op (iSup U)))),
    (fun s => IsGluing (X.sheafToTypes T).val U sf' s) y → y = gl
gl' : ToType ((subpresheafToTypes P.toPrelocalPredicate).obj (op (iSup U)))
hgl' : (subpresheafToTypes P.toPrelocalPredicate).IsGluing U sf gl'
⊢ ↑gl' = ↑⟨gl, ⋯⟩

Tactic:
exact gl_uniq gl'.1 fun i => congr_arg Subtype.val (hgl' i)

Result:
no goals

Proof state:
case intro.intro.refine_1.x.mk
X : TopCat
T : ↑X → Type v
P : LocalPredicate T
ι : Type v
U : ι → Opens ↑X
sf : (i : ι) → ToType ((subpresheafToTypes P.toPrelocalPredicate).obj (op (U i)))
sf_comp : (subpresheafToTypes P.toPrelocalPredicate).IsCompatible U sf
sf' : (i : ι) → (X.presheafToTypes T).obj (op (U i)) := fun i => ↑(sf i)
sf'_comp : (X.presheafToTypes T).IsCompatible U sf'
gl : ToType ((X.sheafToTypes T).val.obj (op (iSup U)))
gl_spec : IsGluing (X.sheafToTypes T).val U sf' gl
gl_uniq :
  ∀ (y : ToType ((X.sheafToTypes T).val.obj (op (iSup U)))),
    (fun s => IsGluing (X.sheafToTypes T).val U sf' s) y → y = gl
x : ↑X
mem : x ∈ unop (op (iSup U))
i : ι
hi : x ∈ U i
⊢ ∃ V, ∃ (_ : ↑⟨x, mem⟩ ∈ V), ∃ i, P.pred fun x => gl (i x)

Tactic:
use U i, hi, Opens.leSupr U i

Result:
case h
X : TopCat
T : ↑X → Type v
P : LocalPredicate T
ι : Type v
U : ι → Opens ↑X
sf : (i : ι) → ToType ((subpresheafToTypes P.toPrelocalPredicate).obj (op (U i)))
sf_comp : (subpresheafToTypes P.toPrelocalPredicate).IsCompatible U sf
sf' : (i : ι) → (X.presheafToTypes T).obj (op (U i)) := fun i => ↑(sf i)
sf'_comp : (X.presheafToTypes T).IsCompatible U sf'
gl : ToType ((X.sheafToTypes T).val.obj (op (iSup U)))
gl_spec : IsGluing (X.sheafToTypes T).val U sf' gl
gl_uniq :
  ∀ (y : ToType ((X.sheafToTypes T).val.obj (op (iSup U)))),
    (fun s => IsGluing (X.sheafToTypes T).val U sf' s) y → y = gl
x : ↑X
mem : x ∈ unop (op (iSup U))
i : ι
hi : x ∈ U i
⊢ P.pred fun x => gl ((Opens.leSupr U i) x)