awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Sheaves.LocalPredicate
Goal:
X : TopCat
T : (↑X : Type u_2) → Type u_1
P : LocalPredicate T
ι : Type u_2
U : ι → Opens (↑X : Type u_2)
sf :
  (i : ι) → ToType (FC := TypeCat.Fun) ((subpresheafToTypes (T := T) (P.toPrelocalPredicate (T := T))).obj (op (U i)))
sf_comp : (subpresheafToTypes (T := T) (P.toPrelocalPredicate (T := T))).IsCompatible (FC := TypeCat.Fun) U sf
sf' : (i : ι) → (X.presheafToTypes T).obj (op (U i)) :=
  fun (i : ι) ↦ (↑(sf i) : (x : ↥(unop (op (U i)))) → T (↑x : (↑X : Type u_2)))
sf'_comp : (X.presheafToTypes T).IsCompatible (FC := TypeCat.Fun) U sf'
gl :
  ToType (FC := TypeCat.Fun)
    ((X.sheafToTypes T).obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u_2))).obj
      (op (iSup U)))
gl_spec :
  IsGluing (FC := TypeCat.Fun)
    ((X.sheafToTypes T).obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u_2)))) U sf'
    gl
gl_uniq :
  ∀
    (y :
      ToType (FC := TypeCat.Fun)
        ((X.sheafToTypes T).obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u_2))).obj
          (op (iSup U)))),
    (fun
            (s :
              ToType (FC := TypeCat.Fun)
                ((X.sheafToTypes T).obj (P :=
                      CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u_2))).obj
                  (op (iSup U)))) ↦
          IsGluing (FC := TypeCat.Fun)
            ((X.sheafToTypes T).obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u_2))))
            U sf' s)
        y →
      y = gl
x : (↑X : Type u_2)
mem : x ∈ unop (op (iSup U))
refine_1 :
  ∀ (i : ι) (hi : x ∈ U i),
    ∃ (V : Opens (↑X : Type u_2)) (_ :
      (↑(Subtype.mk (p := fun (x : (↑X : Type u_2)) ↦ x ∈ unop (op (iSup U))) x mem) : (↑X : Type u_2)) ∈ V) (i :
      V ⟶ unop (op (iSup U))),
      P.toPrelocalPredicate (T := T).pred (T := T) (U := V) fun (x : ↥V) ↦ gl ((i : (a : ↥V) → ↥(unop (op (iSup U)))) x)
⊢ ∃ (V : Opens (↑X : Type u_2)) (_ :
    (↑(Subtype.mk (p := fun (x : (↑X : Type u_2)) ↦ x ∈ unop (op (iSup U))) x mem) : (↑X : Type u_2)) ∈ V) (i :
    V ⟶ unop (op (iSup U))),
    P.toPrelocalPredicate (T := T).pred (T := T) (U := V) fun (x : ↥V) ↦ gl ((i : (a : ↥V) → ↥(unop (op (iSup U)))) x)

Tactic:
choose i hi using Opens.mem_iSup.mp mem

Premises used: TopologicalSpace.Opens.mem_iSup, Iff.mp
-- Module: Mathlib.Topology.Sheaves.LocalPredicate
Goal:
X : TopCat
T : (↑X : Type u_2) → Type u_1
P : LocalPredicate T
ι : Type u_2
U : ι → Opens (↑X : Type u_2)
sf :
  (i : ι) → ToType (FC := TypeCat.Fun) ((subpresheafToTypes (T := T) (P.toPrelocalPredicate (T := T))).obj (op (U i)))
sf_comp : (subpresheafToTypes (T := T) (P.toPrelocalPredicate (T := T))).IsCompatible (FC := TypeCat.Fun) U sf
sf' : (i : ι) → (X.presheafToTypes T).obj (op (U i)) :=
  fun (i : ι) ↦ (↑(sf i) : (x : ↥(unop (op (U i)))) → T (↑x : (↑X : Type u_2)))
sf'_comp : (X.presheafToTypes T).IsCompatible (FC := TypeCat.Fun) U sf'
gl :
  ToType (FC := TypeCat.Fun)
    ((X.sheafToTypes T).obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u_2))).obj
      (op (iSup U)))
gl_spec :
  IsGluing (FC := TypeCat.Fun)
    ((X.sheafToTypes T).obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u_2)))) U sf'
    gl
gl_uniq :
  ∀
    (y :
      ToType (FC := TypeCat.Fun)
        ((X.sheafToTypes T).obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u_2))).obj
          (op (iSup U)))),
    (fun
            (s :
              ToType (FC := TypeCat.Fun)
                ((X.sheafToTypes T).obj (P :=
                      CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u_2))).obj
                  (op (iSup U)))) ↦
          IsGluing (FC := TypeCat.Fun)
            ((X.sheafToTypes T).obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u_2))))
            U sf' s)
        y →
      y = gl
x : (↑X : Type u_2)
mem : x ∈ unop (op (iSup U))
i : ι
hi : x ∈ U i
h :
  P.toPrelocalPredicate (T := T).pred (T := T) (U := U i) fun (x : ↥(U i)) ↦
    gl ((Opens.leSupr U i : (a : ↥(U i)) → ↥(unop (op (iSup U)))) x)
⊢ ∃ (V : Opens (↑X : Type u_2)) (_ :
    (↑(Subtype.mk (p := fun (x : (↑X : Type u_2)) ↦ x ∈ unop (op (iSup U))) x mem) : (↑X : Type u_2)) ∈ V) (i :
    V ⟶ unop (op (iSup U))),
    P.toPrelocalPredicate (T := T).pred (T := T) (U := V) fun (x : ↥V) ↦ gl ((i : (a : ↥V) → ↥(unop (op (iSup U)))) x)

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

Premises used: TopologicalSpace.Opens.leSupr
-- Module: Mathlib.Topology.Sheaves.LocalPredicate
Goal:
X : TopCat
T : (↑X : Type u_2) → Type u_1
P : LocalPredicate T
ι : Type u_2
U : ι → Opens (↑X : Type u_2)
sf :
  (i : ι) → ToType (FC := TypeCat.Fun) ((subpresheafToTypes (T := T) (P.toPrelocalPredicate (T := T))).obj (op (U i)))
sf_comp : (subpresheafToTypes (T := T) (P.toPrelocalPredicate (T := T))).IsCompatible (FC := TypeCat.Fun) U sf
sf' : (i : ι) → (X.presheafToTypes T).obj (op (U i)) :=
  fun (i : ι) ↦ (↑(sf i) : (x : ↥(unop (op (U i)))) → T (↑x : (↑X : Type u_2)))
sf'_comp : (X.presheafToTypes T).IsCompatible (FC := TypeCat.Fun) U sf'
gl :
  ToType (FC := TypeCat.Fun)
    ((X.sheafToTypes T).obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u_2))).obj
      (op (iSup U)))
gl_spec :
  IsGluing (FC := TypeCat.Fun)
    ((X.sheafToTypes T).obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u_2)))) U sf'
    gl
gl_uniq :
  ∀
    (y :
      ToType (FC := TypeCat.Fun)
        ((X.sheafToTypes T).obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u_2))).obj
          (op (iSup U)))),
    (fun
            (s :
              ToType (FC := TypeCat.Fun)
                ((X.sheafToTypes T).obj (P :=
                      CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u_2))).obj
                  (op (iSup U)))) ↦
          IsGluing (FC := TypeCat.Fun)
            ((X.sheafToTypes T).obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u_2))))
            U sf' s)
        y →
      y = gl
x : (↑X : Type u_2)
mem : x ∈ unop (op (iSup U))
i : ι
hi : x ∈ U i
⊢ P.toPrelocalPredicate (T := T).pred (T := T) (↑(sf i) : (x : ↥(unop (op (U i)))) → T (↑x : (↑X : Type u_2)))

Tactic:
(sf i).property

Premises used: Subtype.property
-- Module: Mathlib.Topology.Sheaves.LocalPredicate
Goal:
X : TopCat
T : (↑X : Type u_2) → Type u_1
P : LocalPredicate T
ι : Type u_2
U : ι → Opens (↑X : Type u_2)
sf :
  (i : ι) → ToType (FC := TypeCat.Fun) ((subpresheafToTypes (T := T) (P.toPrelocalPredicate (T := T))).obj (op (U i)))
sf_comp : (subpresheafToTypes (T := T) (P.toPrelocalPredicate (T := T))).IsCompatible (FC := TypeCat.Fun) U sf
sf' : (i : ι) → (X.presheafToTypes T).obj (op (U i)) :=
  fun (i : ι) ↦ (↑(sf i) : (x : ↥(unop (op (U i)))) → T (↑x : (↑X : Type u_2)))
sf'_comp : (X.presheafToTypes T).IsCompatible (FC := TypeCat.Fun) U sf'
gl :
  ToType (FC := TypeCat.Fun)
    ((X.sheafToTypes T).obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u_2))).obj
      (op (iSup U)))
gl_spec :
  IsGluing (FC := TypeCat.Fun)
    ((X.sheafToTypes T).obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u_2)))) U sf'
    gl
gl_uniq :
  ∀
    (y :
      ToType (FC := TypeCat.Fun)
        ((X.sheafToTypes T).obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u_2))).obj
          (op (iSup U)))),
    (fun
            (s :
              ToType (FC := TypeCat.Fun)
                ((X.sheafToTypes T).obj (P :=
                      CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u_2))).obj
                  (op (iSup U)))) ↦
          IsGluing (FC := TypeCat.Fun)
            ((X.sheafToTypes T).obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u_2))))
            U sf' s)
        y →
      y = gl
x : (↑X : Type u_2)
mem : x ∈ unop (op (iSup U))
i : ι
hi : x ∈ U i
h :
  (fun (x : ↥(U i)) ↦ gl ((Opens.leSupr U i : (a : ↥(U i)) → ↥(unop (op (iSup U)))) x)) =
    (↑(sf i) : (x : ↥(unop (op (U i)))) → T (↑x : (↑X : Type u_2)))
⊢ P.toPrelocalPredicate (T := T).pred (T := T) (U := U i) fun (x : ↥(U i)) ↦
    gl ((Opens.leSupr U i : (a : ↥(U i)) → ↥(unop (op (iSup U)))) x)

Tactic:
convert! (sf i).property using 1

Premises used: Subtype.property
-- Module: Mathlib.Topology.Sheaves.LocalPredicate
Goal:
X : TopCat
T : (↑X : Type u_2) → Type u_1
P : LocalPredicate T
ι : Type u_2
U : ι → Opens (↑X : Type u_2)
sf :
  (i : ι) → ToType (FC := TypeCat.Fun) ((subpresheafToTypes (T := T) (P.toPrelocalPredicate (T := T))).obj (op (U i)))
sf_comp : (subpresheafToTypes (T := T) (P.toPrelocalPredicate (T := T))).IsCompatible (FC := TypeCat.Fun) U sf
sf' : (i : ι) → (X.presheafToTypes T).obj (op (U i)) :=
  fun (i : ι) ↦ (↑(sf i) : (x : ↥(unop (op (U i)))) → T (↑x : (↑X : Type u_2)))
sf'_comp : (X.presheafToTypes T).IsCompatible (FC := TypeCat.Fun) U sf'
gl :
  ToType (FC := TypeCat.Fun)
    ((X.sheafToTypes T).obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u_2))).obj
      (op (iSup U)))
gl_spec :
  IsGluing (FC := TypeCat.Fun)
    ((X.sheafToTypes T).obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u_2)))) U sf'
    gl
gl_uniq :
  ∀
    (y :
      ToType (FC := TypeCat.Fun)
        ((X.sheafToTypes T).obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u_2))).obj
          (op (iSup U)))),
    (fun
            (s :
              ToType (FC := TypeCat.Fun)
                ((X.sheafToTypes T).obj (P :=
                      CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u_2))).obj
                  (op (iSup U)))) ↦
          IsGluing (FC := TypeCat.Fun)
            ((X.sheafToTypes T).obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u_2))))
            U sf' s)
        y →
      y = gl
x : (↑X : Type u_2)
mem : x ∈ unop (op (iSup U))
i : ι
hi : x ∈ U i
⊢ (fun (x : ↥(U i)) ↦ gl ((Opens.leSupr U i : (a : ↥(U i)) → ↥(unop (op (iSup U)))) x)) =
    (↑(sf i) : (x : ↥(unop (op (U i)))) → T (↑x : (↑X : Type u_2)))

Tactic:
gl_spec i

Premises used: Set.Mem
-- Module: Mathlib.Topology.Sheaves.LocalPredicate
Goal:
X : TopCat
T : (↑X : Type u_2) → Type u_1
P : LocalPredicate T
ι : Type u_2
U : ι → Opens (↑X : Type u_2)
sf :
  (i : ι) → ToType (FC := TypeCat.Fun) ((subpresheafToTypes (T := T) (P.toPrelocalPredicate (T := T))).obj (op (U i)))
sf_comp : (subpresheafToTypes (T := T) (P.toPrelocalPredicate (T := T))).IsCompatible (FC := TypeCat.Fun) U sf
sf' : (i : ι) → (X.presheafToTypes T).obj (op (U i)) :=
  fun (i : ι) ↦ (↑(sf i) : (x : ↥(unop (op (U i)))) → T (↑x : (↑X : Type u_2)))
sf'_comp : (X.presheafToTypes T).IsCompatible (FC := TypeCat.Fun) U sf'
gl :
  ToType (FC := TypeCat.Fun)
    ((X.sheafToTypes T).obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u_2))).obj
      (op (iSup U)))
gl_spec :
  IsGluing (FC := TypeCat.Fun)
    ((X.sheafToTypes T).obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u_2)))) U sf'
    gl
gl_uniq :
  ∀
    (y :
      ToType (FC := TypeCat.Fun)
        ((X.sheafToTypes T).obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u_2))).obj
          (op (iSup U)))),
    (fun
            (s :
              ToType (FC := TypeCat.Fun)
                ((X.sheafToTypes T).obj (P :=
                      CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u_2))).obj
                  (op (iSup U)))) ↦
          IsGluing (FC := TypeCat.Fun)
            ((X.sheafToTypes T).obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u_2))))
            U sf' s)
        y →
      y = gl
x : (↑X : Type u_2)
mem : x ∈ unop (op (iSup U))
i : ι
hi : x ∈ U i
⊢ (fun (x : ↥(U i)) ↦ gl ((Opens.leSupr U i : (a : ↥(U i)) → ↥(unop (op (iSup U)))) x)) =
    (↑(sf i) : (x : ↥(unop (op (U i)))) → T (↑x : (↑X : Type u_2)))

Tactic:
exact gl_spec i
-- Module: Mathlib.Topology.Sheaves.LocalPredicate
Goal:
X : TopCat
T : (↑X : Type u_2) → Type u_1
P : LocalPredicate T
ι : Type u_2
U : ι → Opens (↑X : Type u_2)
sf :
  (i : ι) → ToType (FC := TypeCat.Fun) ((subpresheafToTypes (T := T) (P.toPrelocalPredicate (T := T))).obj (op (U i)))
sf_comp : (subpresheafToTypes (T := T) (P.toPrelocalPredicate (T := T))).IsCompatible (FC := TypeCat.Fun) U sf
sf' : (i : ι) → (X.presheafToTypes T).obj (op (U i)) :=
  fun (i : ι) ↦ (↑(sf i) : (x : ↥(unop (op (U i)))) → T (↑x : (↑X : Type u_2)))
sf'_comp : (X.presheafToTypes T).IsCompatible (FC := TypeCat.Fun) U sf'
gl :
  ToType (FC := TypeCat.Fun)
    ((X.sheafToTypes T).obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u_2))).obj
      (op (iSup U)))
gl_spec :
  IsGluing (FC := TypeCat.Fun)
    ((X.sheafToTypes T).obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u_2)))) U sf'
    gl
gl_uniq :
  ∀
    (y :
      ToType (FC := TypeCat.Fun)
        ((X.sheafToTypes T).obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u_2))).obj
          (op (iSup U)))),
    (fun
            (s :
              ToType (FC := TypeCat.Fun)
                ((X.sheafToTypes T).obj (P :=
                      CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u_2))).obj
                  (op (iSup U)))) ↦
          IsGluing (FC := TypeCat.Fun)
            ((X.sheafToTypes T).obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u_2))))
            U sf' s)
        y →
      y = gl
⊢ (fun
        (s :
          ToType (FC := TypeCat.Fun)
            ((subpresheafToTypes (T := T) (P.toPrelocalPredicate (T := T))).obj (op (iSup U)))) ↦
      (subpresheafToTypes (T := T) (P.toPrelocalPredicate (T := T))).IsGluing (FC := TypeCat.Fun) U sf s)
    (Subtype.mk (p := fun (f : (x : ↥(unop (op (iSup U)))) → T (↑x : (↑X : Type u_2))) ↦
      P.toPrelocalPredicate (T := T).pred (T := T) f) gl ⋯)

Tactic:
fun i ↦ Subtype.ext (gl_spec i)

Premises used: TopCat.Presheaf.IsGluing, Subtype.ext
-- Module: Mathlib.Topology.Sheaves.LocalPredicate
Goal:
X : TopCat
T : (↑X : Type u_2) → Type u_1
P : LocalPredicate T
ι : Type u_2
U : ι → Opens (↑X : Type u_2)
sf :
  (i : ι) → ToType (FC := TypeCat.Fun) ((subpresheafToTypes (T := T) (P.toPrelocalPredicate (T := T))).obj (op (U i)))
sf_comp : (subpresheafToTypes (T := T) (P.toPrelocalPredicate (T := T))).IsCompatible (FC := TypeCat.Fun) U sf
sf' : (i : ι) → (X.presheafToTypes T).obj (op (U i)) :=
  fun (i : ι) ↦ (↑(sf i) : (x : ↥(unop (op (U i)))) → T (↑x : (↑X : Type u_2)))
sf'_comp : (X.presheafToTypes T).IsCompatible (FC := TypeCat.Fun) U sf'
gl :
  ToType (FC := TypeCat.Fun)
    ((X.sheafToTypes T).obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u_2))).obj
      (op (iSup U)))
gl_spec :
  IsGluing (FC := TypeCat.Fun)
    ((X.sheafToTypes T).obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u_2)))) U sf'
    gl
gl_uniq :
  ∀
    (y :
      ToType (FC := TypeCat.Fun)
        ((X.sheafToTypes T).obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u_2))).obj
          (op (iSup U)))),
    (fun
            (s :
              ToType (FC := TypeCat.Fun)
                ((X.sheafToTypes T).obj (P :=
                      CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u_2))).obj
                  (op (iSup U)))) ↦
          IsGluing (FC := TypeCat.Fun)
            ((X.sheafToTypes T).obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u_2))))
            U sf' s)
        y →
      y = gl
⊢ (fun
        (s :
          ToType (FC := TypeCat.Fun)
            ((subpresheafToTypes (T := T) (P.toPrelocalPredicate (T := T))).obj (op (iSup U)))) ↦
      (subpresheafToTypes (T := T) (P.toPrelocalPredicate (T := T))).IsGluing (FC := TypeCat.Fun) U sf s)
    (Subtype.mk (p := fun (f : (x : ↥(unop (op (iSup U)))) → T (↑x : (↑X : Type u_2))) ↦
      P.toPrelocalPredicate (T := T).pred (T := T) f) gl ⋯)

Tactic:
exact fun i ↦ Subtype.ext (gl_spec i)

Premises used: Subtype.ext
-- Module: Mathlib.Topology.Sheaves.LocalPredicate
Goal:
X : TopCat
T : (↑X : Type u_2) → Type u_1
P : LocalPredicate T
ι : Type u_2
U : ι → Opens (↑X : Type u_2)
sf :
  (i : ι) → ToType (FC := TypeCat.Fun) ((subpresheafToTypes (T := T) (P.toPrelocalPredicate (T := T))).obj (op (U i)))
sf_comp : (subpresheafToTypes (T := T) (P.toPrelocalPredicate (T := T))).IsCompatible (FC := TypeCat.Fun) U sf
sf' : (i : ι) → (X.presheafToTypes T).obj (op (U i)) :=
  fun (i : ι) ↦ (↑(sf i) : (x : ↥(unop (op (U i)))) → T (↑x : (↑X : Type u_2)))
sf'_comp : (X.presheafToTypes T).IsCompatible (FC := TypeCat.Fun) U sf'
gl :
  ToType (FC := TypeCat.Fun)
    ((X.sheafToTypes T).obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u_2))).obj
      (op (iSup U)))
gl_spec :
  IsGluing (FC := TypeCat.Fun)
    ((X.sheafToTypes T).obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u_2)))) U sf'
    gl
gl_uniq :
  ∀
    (y :
      ToType (FC := TypeCat.Fun)
        ((X.sheafToTypes T).obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u_2))).obj
          (op (iSup U)))),
    (fun
            (s :
              ToType (FC := TypeCat.Fun)
                ((X.sheafToTypes T).obj (P :=
                      CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u_2))).obj
                  (op (iSup U)))) ↦
          IsGluing (FC := TypeCat.Fun)
            ((X.sheafToTypes T).obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u_2))))
            U sf' s)
        y →
      y = gl
gl' : ToType (FC := TypeCat.Fun) ((subpresheafToTypes (T := T) (P.toPrelocalPredicate (T := T))).obj (op (iSup U)))
hgl' : (subpresheafToTypes (T := T) (P.toPrelocalPredicate (T := T))).IsGluing (FC := TypeCat.Fun) U sf gl'
⊢ gl' =
    Subtype.mk (p := fun (f : (x : ↥(unop (op (iSup U)))) → T (↑x : (↑X : Type u_2))) ↦
      P.toPrelocalPredicate (T := T).pred (T := T) f) gl ⋯

Tactic:
Subtype.ext ?_

Premises used: Subtype.ext
-- Module: Mathlib.Topology.Sheaves.LocalPredicate
Goal:
X : TopCat
T : (↑X : Type u_2) → Type u_1
P : LocalPredicate T
ι : Type u_2
U : ι → Opens (↑X : Type u_2)
sf :
  (i : ι) → ToType (FC := TypeCat.Fun) ((subpresheafToTypes (T := T) (P.toPrelocalPredicate (T := T))).obj (op (U i)))
sf_comp : (subpresheafToTypes (T := T) (P.toPrelocalPredicate (T := T))).IsCompatible (FC := TypeCat.Fun) U sf
sf' : (i : ι) → (X.presheafToTypes T).obj (op (U i)) :=
  fun (i : ι) ↦ (↑(sf i) : (x : ↥(unop (op (U i)))) → T (↑x : (↑X : Type u_2)))
sf'_comp : (X.presheafToTypes T).IsCompatible (FC := TypeCat.Fun) U sf'
gl :
  ToType (FC := TypeCat.Fun)
    ((X.sheafToTypes T).obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u_2))).obj
      (op (iSup U)))
gl_spec :
  IsGluing (FC := TypeCat.Fun)
    ((X.sheafToTypes T).obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u_2)))) U sf'
    gl
gl_uniq :
  ∀
    (y :
      ToType (FC := TypeCat.Fun)
        ((X.sheafToTypes T).obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u_2))).obj
          (op (iSup U)))),
    (fun
            (s :
              ToType (FC := TypeCat.Fun)
                ((X.sheafToTypes T).obj (P :=
                      CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u_2))).obj
                  (op (iSup U)))) ↦
          IsGluing (FC := TypeCat.Fun)
            ((X.sheafToTypes T).obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u_2))))
            U sf' s)
        y →
      y = gl
gl' : ToType (FC := TypeCat.Fun) ((subpresheafToTypes (T := T) (P.toPrelocalPredicate (T := T))).obj (op (iSup U)))
hgl' : (subpresheafToTypes (T := T) (P.toPrelocalPredicate (T := T))).IsGluing (FC := TypeCat.Fun) U sf gl'
refine_3 :
  (↑gl' : (x : ↥(unop (op (iSup U)))) → T (↑x : (↑X : Type u_2))) =
    (↑(Subtype.mk (p := fun (f : (x : ↥(unop (op (iSup U)))) → T (↑x : (↑X : Type u_2))) ↦
          P.toPrelocalPredicate (T := T).pred (T := T) f) gl ⋯) :
      (x : ↥(unop (op (iSup U)))) → T (↑x : (↑X : Type u_2)))
⊢ gl' =
    Subtype.mk (p := fun (f : (x : ↥(unop (op (iSup U)))) → T (↑x : (↑X : Type u_2))) ↦
      P.toPrelocalPredicate (T := T).pred (T := T) f) gl ⋯

Tactic:
refine Subtype.ext ?_

Premises used: Subtype.ext
-- Module: Mathlib.Topology.Sheaves.LocalPredicate
Goal:
X : TopCat
T : (↑X : Type u_2) → Type u_1
P : LocalPredicate T
ι : Type u_2
U : ι → Opens (↑X : Type u_2)
sf :
  (i : ι) → ToType (FC := TypeCat.Fun) ((subpresheafToTypes (T := T) (P.toPrelocalPredicate (T := T))).obj (op (U i)))
sf_comp : (subpresheafToTypes (T := T) (P.toPrelocalPredicate (T := T))).IsCompatible (FC := TypeCat.Fun) U sf
sf' : (i : ι) → (X.presheafToTypes T).obj (op (U i)) :=
  fun (i : ι) ↦ (↑(sf i) : (x : ↥(unop (op (U i)))) → T (↑x : (↑X : Type u_2)))
sf'_comp : (X.presheafToTypes T).IsCompatible (FC := TypeCat.Fun) U sf'
gl :
  ToType (FC := TypeCat.Fun)
    ((X.sheafToTypes T).obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u_2))).obj
      (op (iSup U)))
gl_spec :
  IsGluing (FC := TypeCat.Fun)
    ((X.sheafToTypes T).obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u_2)))) U sf'
    gl
gl_uniq :
  ∀
    (y :
      ToType (FC := TypeCat.Fun)
        ((X.sheafToTypes T).obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u_2))).obj
          (op (iSup U)))),
    (fun
            (s :
              ToType (FC := TypeCat.Fun)
                ((X.sheafToTypes T).obj (P :=
                      CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u_2))).obj
                  (op (iSup U)))) ↦
          IsGluing (FC := TypeCat.Fun)
            ((X.sheafToTypes T).obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u_2))))
            U sf' s)
        y →
      y = gl
gl' : ToType (FC := TypeCat.Fun) ((subpresheafToTypes (T := T) (P.toPrelocalPredicate (T := T))).obj (op (iSup U)))
hgl' : (subpresheafToTypes (T := T) (P.toPrelocalPredicate (T := T))).IsGluing (FC := TypeCat.Fun) U sf gl'
⊢ (↑gl' : (x : ↥(unop (op (iSup U)))) → T (↑x : (↑X : Type u_2))) =
    (↑(Subtype.mk (p := fun (f : (x : ↥(unop (op (iSup U)))) → T (↑x : (↑X : Type u_2))) ↦
          P.toPrelocalPredicate (T := T).pred (T := T) f) gl ⋯) :
      (x : ↥(unop (op (iSup U)))) → T (↑x : (↑X : Type u_2)))

Tactic:
gl_uniq gl'.1 fun i ↦ congr_arg Subtype.val (hgl' i)

Premises used: congr_arg, Subtype.val