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
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:
exact gl_uniq gl'.1 fun i ↦ congr_arg Subtype.val (hgl' i)

Premises used: congr_arg, Subtype.val
-- Module: Mathlib.Topology.Sheaves.LocalPredicate
Goal:
X : TopCat
T : (↑X : Type u_1) → Type u_1
P : LocalPredicate T
x : (↑X : Type u_1)
U : (OpenNhds x)ᵒᵖ
fU :
  { f : (x_1 : ↥(unop ((OpenNhds.inclusion x).op.obj U))) → T (↑x_1 : (↑X : Type u_1)) //
    P.toPrelocalPredicate (T := T).pred (T := T) f }
⊢ Eq (α := T x)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (stalkToFiber (T := T) P x) :
          (a : (subpresheafToTypes P.toPrelocalPredicate).stalk x) → T x)
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
              (colimit.ι ((OpenNhds.inclusion x).op ⋙ subpresheafToTypes (T := T) (P.toPrelocalPredicate (T := T))) U) :
            (a : { f : (x_1 : ↥((OpenNhds.inclusion x).obj (unop U))) → T (↑x_1 : (↑X : Type u_1)) // P.pred f }) →
              colimit ((OpenNhds.inclusion x).op ⋙ subpresheafToTypes P.toPrelocalPredicate))
          fU) :
      T x)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((P.cocone (T := T) x).ι.app U) :
          (a : { f : (x_1 : ↥((OpenNhds.inclusion x).obj (unop U))) → T (↑x_1 : (↑X : Type u_1)) // P.pred f }) →
            (P.cocone x).pt)
        fU :
      (P.cocone (T := T) x).pt)

Tactic:
colimit.ι_desc_apply _ _ _

Premises used: CategoryTheory.Limits.colimit.ι_desc_apply
-- Module: Mathlib.Topology.Sheaves.LocalPredicate
Goal:
X : TopCat
T : (↑X : Type u_1) → Type u_1
P : LocalPredicate T
U : Opens (↑X : Type u_1)
x : (↑X : Type u_1)
hx : x ∈ U
f : (fun (X : Type u_1) ↦ X) ((subsheafToTypes (T := T) P).presheaf.obj (op U))
dsimp :
  ((@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
            (colimit.desc ((OpenNhds.inclusion x).op ⋙ subpresheafToTypes (T := T) (P.toPrelocalPredicate (T := T)))
              (P.cocone (T := T) x)) :
          TypeCat.Fun ((subpresheafToTypes (T := T) (P.toPrelocalPredicate (T := T))).stalk x) (T x)) :
        (a : (subpresheafToTypes P.toPrelocalPredicate).stalk x) → T x)
      (((@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
              (colimit.ι ((OpenNhds.inclusion x).op ⋙ subpresheafToTypes (T := T) (P.toPrelocalPredicate (T := T)))
                (op (Subtype.mk (p := fun (U : Opens (↑X : Type u_1)) ↦ x ∈ U) U hx))) :
            TypeCat.Fun { f : (x : ↥U) → T (↑x : (↑X : Type u_1)) // P.toPrelocalPredicate (T := T).pred (T := T) f }
              ((subpresheafToTypes (T := T) (P.toPrelocalPredicate (T := T))).stalk x)) :
          (a : { f : (x : ↥U) → T (↑x : (↑X : Type u_1)) // P.pred f }) →
            (subpresheafToTypes P.toPrelocalPredicate).stalk x)
        f) =
    (↑f : (x : ↥U) → T (↑x : (↑X : Type u_1))) (Subtype.mk (p := fun (x : (↑X : Type u_1)) ↦ x ∈ U) x hx)
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (stalkToFiber (T := T) P x) :
        (a : (fun (X : Type u_1) ↦ X) ((subsheafToTypes P).presheaf.stalk x)) → (fun (X : Type u_1) ↦ X) (T x))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) ((subsheafToTypes (T := T) P).presheaf.germ U x hx) :
          (a : (fun (X : Type u_1) ↦ X) ((subsheafToTypes P).presheaf.obj (op U))) →
            (fun (X : Type u_1) ↦ X) ((subsheafToTypes P).presheaf.stalk x))
        f) =
    (↑f : (x : ↥(unop (op U))) → T (↑x : (↑X : Type u_1)))
      (Subtype.mk (p := fun (x : (↑X : Type u_1)) ↦ x ∈ unop (op U)) x hx)

Tactic:
dsimp [stalkToFiber, Presheaf.germ]

Premises used: TopCat.stalkToFiber, TopCat.Presheaf.germ
-- Module: Mathlib.Topology.Sheaves.LocalPredicate
Goal:
X : TopCat
T : (↑X : Type u_1) → Type u_1
P : LocalPredicate T
U : Opens (↑X : Type u_1)
x : (↑X : Type u_1)
hx : x ∈ U
f : (fun (X : Type u_1) ↦ X) ((subsheafToTypes (T := T) P).presheaf.obj (op U))
⊢ ((@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
            (colimit.desc ((OpenNhds.inclusion x).op ⋙ subpresheafToTypes (T := T) (P.toPrelocalPredicate (T := T)))
              (P.cocone (T := T) x)) :
          TypeCat.Fun ((subpresheafToTypes (T := T) (P.toPrelocalPredicate (T := T))).stalk x) (T x)) :
        (a : (subpresheafToTypes P.toPrelocalPredicate).stalk x) → T x)
      (((@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
              (colimit.ι ((OpenNhds.inclusion x).op ⋙ subpresheafToTypes (T := T) (P.toPrelocalPredicate (T := T)))
                (op (Subtype.mk (p := fun (U : Opens (↑X : Type u_1)) ↦ x ∈ U) U hx))) :
            TypeCat.Fun { f : (x : ↥U) → T (↑x : (↑X : Type u_1)) // P.toPrelocalPredicate (T := T).pred (T := T) f }
              ((subpresheafToTypes (T := T) (P.toPrelocalPredicate (T := T))).stalk x)) :
          (a : { f : (x : ↥U) → T (↑x : (↑X : Type u_1)) // P.pred f }) →
            (subpresheafToTypes P.toPrelocalPredicate).stalk x)
        f) =
    (↑f : (x : ↥U) → T (↑x : (↑X : Type u_1))) (Subtype.mk (p := fun (x : (↑X : Type u_1)) ↦ x ∈ U) x hx)

Tactic:
colimit.ι_desc_apply _ _ _

Premises used: Set.Mem, CategoryTheory.Limits.colimit.ι_desc_apply
-- Module: Mathlib.Topology.Sheaves.LocalPredicate
Goal:
X : TopCat
T : (↑X : Type u_1) → Type u_1
P : LocalPredicate T
U : Opens (↑X : Type u_1)
x : (↑X : Type u_1)
hx : x ∈ U
f : (fun (X : Type u_1) ↦ X) ((subsheafToTypes (T := T) P).presheaf.obj (op U))
⊢ ((@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
            (colimit.desc ((OpenNhds.inclusion x).op ⋙ subpresheafToTypes (T := T) (P.toPrelocalPredicate (T := T)))
              (P.cocone (T := T) x)) :
          TypeCat.Fun ((subpresheafToTypes (T := T) (P.toPrelocalPredicate (T := T))).stalk x) (T x)) :
        (a : (subpresheafToTypes P.toPrelocalPredicate).stalk x) → T x)
      (((@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
              (colimit.ι ((OpenNhds.inclusion x).op ⋙ subpresheafToTypes (T := T) (P.toPrelocalPredicate (T := T)))
                (op (Subtype.mk (p := fun (U : Opens (↑X : Type u_1)) ↦ x ∈ U) U hx))) :
            TypeCat.Fun { f : (x : ↥U) → T (↑x : (↑X : Type u_1)) // P.toPrelocalPredicate (T := T).pred (T := T) f }
              ((subpresheafToTypes (T := T) (P.toPrelocalPredicate (T := T))).stalk x)) :
          (a : { f : (x : ↥U) → T (↑x : (↑X : Type u_1)) // P.pred f }) →
            (subpresheafToTypes P.toPrelocalPredicate).stalk x)
        f) =
    (↑f : (x : ↥U) → T (↑x : (↑X : Type u_1))) (Subtype.mk (p := fun (x : (↑X : Type u_1)) ↦ x ∈ U) x hx)

Tactic:
exact colimit.ι_desc_apply _ _ _

Premises used: CategoryTheory.Limits.colimit.ι_desc_apply
-- Module: Mathlib.Topology.Sheaves.LocalPredicate
Goal:
X : TopCat
T : (↑X : Type u_1) → Type u_1
P : LocalPredicate T
x : (↑X : Type u_1)
w :
  ∀ (t : T x),
    ∃ (U : OpenNhds x) (f : (y : ↥(↑U : Opens (↑X : Type u_1))) → T (↑y : (↑X : Type u_1))) (_ :
      P.toPrelocalPredicate (T := T).pred (T := T) f),
      f (Subtype.mk (p := fun (x_2 : (↑X : Type u_1)) ↦ x_2 ∈ (↑U : Opens (↑X : Type u_1))) x ⋯) = t
t : (fun (X : Type u_1) ↦ X) (T x)
rcases :
  ∀ (U : OpenNhds x) (f : (y : ↥(↑U : Opens (↑X : Type u_1))) → T (↑y : (↑X : Type u_1)))
    (h : P.toPrelocalPredicate (T := T).pred (T := T) f),
    ∃ (a : (fun (X : Type u_1) ↦ X) ((subsheafToTypes (T := T) P).presheaf.stalk x)),
      Eq (α := (fun (X : Type u_1) ↦ X) (T x))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (stalkToFiber (T := T) P x) :
              (a : (fun (X : Type u_1) ↦ X) ((subsheafToTypes P).presheaf.stalk x)) → (fun (X : Type u_1) ↦ X) (T x))
            a :
          (fun (X : Type u_1) ↦ X) (T x))
        (f (Subtype.mk (p := fun (x_1 : (↑X : Type u_1)) ↦ x_1 ∈ (↑U : Opens (↑X : Type u_1))) x ⋯) :
          T
            (↑(Subtype.mk (p := fun (x_1 : (↑X : Type u_1)) ↦ x_1 ∈ (↑U : Opens (↑X : Type u_1))) x ⋯) :
              (↑X : Type u_1)))
⊢ ∃ (a : (fun (X : Type u_1) ↦ X) ((subsheafToTypes (T := T) P).presheaf.stalk x)),
    (ConcreteCategory.hom (FC := TypeCat.Fun) (stalkToFiber (T := T) P x) :
          (a : (fun (X : Type u_1) ↦ X) ((subsheafToTypes P).presheaf.stalk x)) → (fun (X : Type u_1) ↦ X) (T x))
        a =
      t

Tactic:
rcases w t with ⟨U, f, h, rfl⟩

Premises used: rfl
-- Module: Mathlib.Topology.Sheaves.LocalPredicate
Goal:
X : TopCat
T : (↑X : Type u_1) → Type u_1
P : LocalPredicate T
x : (↑X : Type u_1)
w :
  ∀ (t : T x),
    ∃ (U : OpenNhds x) (f : (y : ↥(↑U : Opens (↑X : Type u_1))) → T (↑y : (↑X : Type u_1))) (_ :
      P.toPrelocalPredicate (T := T).pred (T := T) f),
      f (Subtype.mk (p := fun (x_2 : (↑X : Type u_1)) ↦ x_2 ∈ (↑U : Opens (↑X : Type u_1))) x ⋯) = t
U : OpenNhds x
f : (y : ↥(↑U : Opens (↑X : Type u_1))) → T (↑y : (↑X : Type u_1))
h : P.toPrelocalPredicate (T := T).pred (T := T) f
w₁ : (fun (X : Type u_1) ↦ X) ((subsheafToTypes (T := T) P).presheaf.stalk x)
h₁ :
  Eq (α := (fun (X : Type u_1) ↦ X) (T x))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (stalkToFiber (T := T) P x) :
          (a : (fun (X : Type u_1) ↦ X) ((subsheafToTypes P).presheaf.stalk x)) → (fun (X : Type u_1) ↦ X) (T x))
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
              ((subsheafToTypes (T := T) P).presheaf.germ (↑U : Opens (↑X : Type u_1)) x ⋯) :
            (a : (fun (X : Type u_1) ↦ X) ((subsheafToTypes P).presheaf.obj (op (↑U : Opens (↑X : Type u_1))))) →
              (fun (X : Type u_1) ↦ X) ((subsheafToTypes P).presheaf.stalk x))
          (Subtype.mk (p := fun (f : (x_1 : ↥(unop (op (↑U : Opens (↑X : Type u_1))))) → T (↑x_1 : (↑X : Type u_1))) ↦
            P.toPrelocalPredicate (T := T).pred (T := T) f) f h)) :
      (fun (X : Type u_1) ↦ X) (T x))
    (f (Subtype.mk (p := fun (x_1 : (↑X : Type u_1)) ↦ x_1 ∈ (↑U : Opens (↑X : Type u_1))) x ⋯) :
      T (↑(Subtype.mk (p := fun (x_1 : (↑X : Type u_1)) ↦ x_1 ∈ (↑U : Opens (↑X : Type u_1))) x ⋯) : (↑X : Type u_1)))
⊢ ∃ (a : (fun (X : Type u_1) ↦ X) ((subsheafToTypes (T := T) P).presheaf.stalk x)),
    Eq (α := (fun (X : Type u_1) ↦ X) (T x))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (stalkToFiber (T := T) P x) :
            (a : (fun (X : Type u_1) ↦ X) ((subsheafToTypes P).presheaf.stalk x)) → (fun (X : Type u_1) ↦ X) (T x))
          a :
        (fun (X : Type u_1) ↦ X) (T x))
      (f (Subtype.mk (p := fun (x_1 : (↑X : Type u_1)) ↦ x_1 ∈ (↑U : Opens (↑X : Type u_1))) x ⋯) :
        T (↑(Subtype.mk (p := fun (x_1 : (↑X : Type u_1)) ↦ x_1 ∈ (↑U : Opens (↑X : Type u_1))) x ⋯) : (↑X : Type u_1)))

Tactic:
fconstructor
-- Module: Mathlib.Topology.Sheaves.LocalPredicate
Goal:
X : TopCat
T : (↑X : Type u_1) → Type u_1
P : LocalPredicate T
x : (↑X : Type u_1)
w :
  ∀ (t : T x),
    ∃ (U : OpenNhds x) (f : (y : ↥(↑U : Opens (↑X : Type u_1))) → T (↑y : (↑X : Type u_1))) (_ :
      P.toPrelocalPredicate (T := T).pred (T := T) f),
      f (Subtype.mk (p := fun (x_2 : (↑X : Type u_1)) ↦ x_2 ∈ (↑U : Opens (↑X : Type u_1))) x ⋯) = t
U : OpenNhds x
f : (y : ↥(↑U : Opens (↑X : Type u_1))) → T (↑y : (↑X : Type u_1))
h : P.toPrelocalPredicate (T := T).pred (T := T) f
⊢ (fun (X : Type u_1) ↦ X) ((subsheafToTypes (T := T) P).presheaf.stalk x)

Tactic:
exact (subsheafToTypes P).presheaf.germ _ x U.2 ⟨f, h⟩

Premises used: CategoryTheory.ConcreteCategory.hom, Subtype.mk, TopCat.Presheaf.germ, TopCat.subsheafToTypes, TopCat.Sheaf.presheaf, DFunLike.coe, Subtype.property
-- Module: Mathlib.Topology.Sheaves.LocalPredicate
Goal:
X : TopCat
T : (↑X : Type u_1) → Type u_1
P : LocalPredicate T
x : (↑X : Type u_1)
w :
  ∀ (t : T x),
    ∃ (U : OpenNhds x) (f : (y : ↥(↑U : Opens (↑X : Type u_1))) → T (↑y : (↑X : Type u_1))) (_ :
      P.toPrelocalPredicate (T := T).pred (T := T) f),
      f (Subtype.mk (p := fun (x_2 : (↑X : Type u_1)) ↦ x_2 ∈ (↑U : Opens (↑X : Type u_1))) x ⋯) = t
U : OpenNhds x
f : (y : ↥(↑U : Opens (↑X : Type u_1))) → T (↑y : (↑X : Type u_1))
h : P.toPrelocalPredicate (T := T).pred (T := T) f
⊢ Eq (α := (fun (X : Type u_1) ↦ X) (T x))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (stalkToFiber (T := T) P x) :
          (a : (fun (X : Type u_1) ↦ X) ((subsheafToTypes P).presheaf.stalk x)) → (fun (X : Type u_1) ↦ X) (T x))
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
              ((subsheafToTypes (T := T) P).presheaf.germ (↑U : Opens (↑X : Type u_1)) x ⋯) :
            (a : (fun (X : Type u_1) ↦ X) ((subsheafToTypes P).presheaf.obj (op (↑U : Opens (↑X : Type u_1))))) →
              (fun (X : Type u_1) ↦ X) ((subsheafToTypes P).presheaf.stalk x))
          (Subtype.mk (p := fun (f : (x_1 : ↥(unop (op (↑U : Opens (↑X : Type u_1))))) → T (↑x_1 : (↑X : Type u_1))) ↦
            P.toPrelocalPredicate (T := T).pred (T := T) f) f h)) :
      (fun (X : Type u_1) ↦ X) (T x))
    (f (Subtype.mk (p := fun (x_1 : (↑X : Type u_1)) ↦ x_1 ∈ (↑U : Opens (↑X : Type u_1))) x ⋯) :
      T (↑(Subtype.mk (p := fun (x_1 : (↑X : Type u_1)) ↦ x_1 ∈ (↑U : Opens (↑X : Type u_1))) x ⋯) : (↑X : Type u_1)))

Tactic:
stalkToFiber_germ P U.1 x U.2 ⟨f, h⟩

Premises used: Set.Mem, TopCat.stalkToFiber_germ, Subtype.mk, Subtype.val, Subtype.property
-- Module: Mathlib.Topology.Sheaves.LocalPredicate
Goal:
X : TopCat
T : (↑X : Type u_1) → Type u_1
P : LocalPredicate T
x : (↑X : Type u_1)
w :
  ∀ (t : T x),
    ∃ (U : OpenNhds x) (f : (y : ↥(↑U : Opens (↑X : Type u_1))) → T (↑y : (↑X : Type u_1))) (_ :
      P.toPrelocalPredicate (T := T).pred (T := T) f),
      f (Subtype.mk (p := fun (x_2 : (↑X : Type u_1)) ↦ x_2 ∈ (↑U : Opens (↑X : Type u_1))) x ⋯) = t
U : OpenNhds x
f : (y : ↥(↑U : Opens (↑X : Type u_1))) → T (↑y : (↑X : Type u_1))
h : P.toPrelocalPredicate (T := T).pred (T := T) f
⊢ Eq (α := (fun (X : Type u_1) ↦ X) (T x))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (stalkToFiber (T := T) P x) :
          (a : (fun (X : Type u_1) ↦ X) ((subsheafToTypes P).presheaf.stalk x)) → (fun (X : Type u_1) ↦ X) (T x))
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
              ((subsheafToTypes (T := T) P).presheaf.germ (↑U : Opens (↑X : Type u_1)) x ⋯) :
            (a : (fun (X : Type u_1) ↦ X) ((subsheafToTypes P).presheaf.obj (op (↑U : Opens (↑X : Type u_1))))) →
              (fun (X : Type u_1) ↦ X) ((subsheafToTypes P).presheaf.stalk x))
          (Subtype.mk (p := fun (f : (x_1 : ↥(unop (op (↑U : Opens (↑X : Type u_1))))) → T (↑x_1 : (↑X : Type u_1))) ↦
            P.toPrelocalPredicate (T := T).pred (T := T) f) f h)) :
      (fun (X : Type u_1) ↦ X) (T x))
    (f (Subtype.mk (p := fun (x_1 : (↑X : Type u_1)) ↦ x_1 ∈ (↑U : Opens (↑X : Type u_1))) x ⋯) :
      T (↑(Subtype.mk (p := fun (x_1 : (↑X : Type u_1)) ↦ x_1 ∈ (↑U : Opens (↑X : Type u_1))) x ⋯) : (↑X : Type u_1)))

Tactic:
exact stalkToFiber_germ P U.1 x U.2 ⟨f, h⟩

Premises used: TopCat.stalkToFiber_germ, Subtype.mk, Subtype.val, Subtype.property
-- Module: Mathlib.Topology.Sheaves.LocalPredicate
Goal:
X : TopCat
T : (↑X : Type u_1) → Type u_1
P : LocalPredicate T
x : (↑X : Type u_1)
w :
  ∀ (U V : OpenNhds x) (fU : (y : ↥(↑U : Opens (↑X : Type u_1))) → T (↑y : (↑X : Type u_1))),
    P.toPrelocalPredicate (T := T).pred (T := T) fU →
      ∀ (fV : (y : ↥(↑V : Opens (↑X : Type u_1))) → T (↑y : (↑X : Type u_1))),
        P.toPrelocalPredicate (T := T).pred (T := T) fV →
          Eq (α :=
              T
                (↑(Subtype.mk (p := fun (x_3 : (↑X : Type u_1)) ↦ x_3 ∈ (↑U : Opens (↑X : Type u_1))) x ⋯) :
                  (↑X : Type u_1)))
              (fU (Subtype.mk (p := fun (x_3 : (↑X : Type u_1)) ↦ x_3 ∈ (↑U : Opens (↑X : Type u_1))) x ⋯))
              (fV (Subtype.mk (p := fun (x_3 : (↑X : Type u_1)) ↦ x_3 ∈ (↑V : Opens (↑X : Type u_1))) x ⋯)) →
            ∃ (W : OpenNhds x) (iU : W ⟶ U) (iV : W ⟶ V),
              ∀ (w : ↥(↑W : Opens (↑X : Type u_1))),
                Eq (α :=
                  T (↑((iU : (a : ↥(↑W : Opens (↑X : Type u_1))) → ↥(↑U : Opens (↑X : Type u_1))) w) : (↑X : Type u_1)))
                  (fU ((iU : (a : ↥(↑W : Opens (↑X : Type u_1))) → ↥(↑U : Opens (↑X : Type u_1))) w))
                  (fV ((iV : (a : ↥(↑W : Opens (↑X : Type u_1))) → ↥(↑V : Opens (↑X : Type u_1))) w))
U : (OpenNhds x)ᵒᵖ
fU : (x_1 : ↥(unop ((OpenNhds.inclusion x).op.obj U))) → T (↑x_1 : (↑X : Type u_1))
hU : P.toPrelocalPredicate (T := T).pred (T := T) fU
V : (OpenNhds x)ᵒᵖ
fV : (x_1 : ↥(unop ((OpenNhds.inclusion x).op.obj V))) → T (↑x_1 : (↑X : Type u_1))
hV : P.toPrelocalPredicate (T := T).pred (T := T) fV
h :
  Eq (α := T x)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((P.cocone (T := T) x).ι.app U) :
          (a : { f : (x_1 : ↥((OpenNhds.inclusion x).obj (unop U))) → T (↑x_1 : (↑X : Type u_1)) // P.pred f }) →
            (P.cocone x).pt)
        (Subtype.mk (p := fun (f : (x_1 : ↥((OpenNhds.inclusion x).obj (unop U))) → T (↑x_1 : (↑X : Type u_1))) ↦
          P.toPrelocalPredicate (T := T).pred (T := T) f) fU hU) :
      (P.cocone (T := T) x).pt)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((P.cocone (T := T) x).ι.app V) :
          (a : { f : (x_1 : ↥((OpenNhds.inclusion x).obj (unop V))) → T (↑x_1 : (↑X : Type u_1)) // P.pred f }) →
            (P.cocone x).pt)
        (Subtype.mk (p := fun (f : (x_1 : ↥((OpenNhds.inclusion x).obj (unop V))) → T (↑x_1 : (↑X : Type u_1))) ↦
          P.toPrelocalPredicate (T := T).pred (T := T) f) fV hV) :
      (P.cocone (T := T) x).pt)
⊢ ∃ (W : OpenNhds x) (iU : W ⟶ unop U) (iV : W ⟶ unop V),
    ∀ (w : ↥(↑W : Opens (↑X : Type u_1))),
      Eq (α :=
        T (↑((iU : (a : ↥(↑W : Opens (↑X : Type u_1))) → ↥(↑(unop U) : Opens (↑X : Type u_1))) w) : (↑X : Type u_1)))
        (fU ((iU : (a : ↥(↑W : Opens (↑X : Type u_1))) → ↥(↑(unop U) : Opens (↑X : Type u_1))) w))
        (fV ((iV : (a : ↥(↑W : Opens (↑X : Type u_1))) → ↥(↑(unop V) : Opens (↑X : Type u_1))) w))

Tactic:
specialize w (unop U) (unop V) fU hU fV hV h

Premises used: Opposite.unop
-- Module: Mathlib.Topology.Sheaves.LocalPredicate
Goal:
X : TopCat
T : (↑X : Type u_1) → Type u_1
P : LocalPredicate T
x : (↑X : Type u_1)
U : (OpenNhds x)ᵒᵖ
fU : (x_1 : ↥(unop ((OpenNhds.inclusion x).op.obj U))) → T (↑x_1 : (↑X : Type u_1))
hU : P.toPrelocalPredicate (T := T).pred (T := T) fU
V : (OpenNhds x)ᵒᵖ
fV : (x_1 : ↥(unop ((OpenNhds.inclusion x).op.obj V))) → T (↑x_1 : (↑X : Type u_1))
hV : P.toPrelocalPredicate (T := T).pred (T := T) fV
h :
  Eq (α := T x)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((P.cocone (T := T) x).ι.app U) :
          (a : { f : (x_1 : ↥((OpenNhds.inclusion x).obj (unop U))) → T (↑x_1 : (↑X : Type u_1)) // P.pred f }) →
            (P.cocone x).pt)
        (Subtype.mk (p := fun (f : (x_1 : ↥((OpenNhds.inclusion x).obj (unop U))) → T (↑x_1 : (↑X : Type u_1))) ↦
          P.toPrelocalPredicate (T := T).pred (T := T) f) fU hU) :
      (P.cocone (T := T) x).pt)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((P.cocone (T := T) x).ι.app V) :
          (a : { f : (x_1 : ↥((OpenNhds.inclusion x).obj (unop V))) → T (↑x_1 : (↑X : Type u_1)) // P.pred f }) →
            (P.cocone x).pt)
        (Subtype.mk (p := fun (f : (x_1 : ↥((OpenNhds.inclusion x).obj (unop V))) → T (↑x_1 : (↑X : Type u_1))) ↦
          P.toPrelocalPredicate (T := T).pred (T := T) f) fV hV) :
      (P.cocone (T := T) x).pt)
W : OpenNhds x
iU : W ⟶ unop U
iV : W ⟶ unop V
w :
  ∀ (w : ↥(↑W : Opens (↑X : Type u_1))),
    Eq (α :=
      T (↑((iU : (a : ↥(↑W : Opens (↑X : Type u_1))) → ↥(↑(unop U) : Opens (↑X : Type u_1))) w) : (↑X : Type u_1)))
      (fU ((iU : (a : ↥(↑W : Opens (↑X : Type u_1))) → ↥(↑(unop U) : Opens (↑X : Type u_1))) w))
      (fV ((iV : (a : ↥(↑W : Opens (↑X : Type u_1))) → ↥(↑(unop V) : Opens (↑X : Type u_1))) w))
refine_1 :
  (W : Opens (↑X : Type u_1)) →
    (m : x ∈ W) →
      (iU : Subtype.mk (p := fun (U : Opens (↑X : Type u_1)) ↦ x ∈ U) W m ⟶ unop U) →
        (iV : Subtype.mk (p := fun (U : Opens (↑X : Type u_1)) ↦ x ∈ U) W m ⟶ unop V) →
          (w :
              ∀ (w : ↥(↑(Subtype.mk (p := fun (U : Opens (↑X : Type u_1)) ↦ x ∈ U) W m) : Opens (↑X : Type u_1))),
                Eq (α :=
                  T
                    (↑((iU : (a : ↥(↑⟨W, m⟩ : Opens (↑X : Type u_1))) → ↥(↑(unop U) : Opens (↑X : Type u_1))) w) :
                      (↑X : Type u_1)))
                  (fU ((iU : (a : ↥(↑⟨W, m⟩ : Opens (↑X : Type u_1))) → ↥(↑(unop U) : Opens (↑X : Type u_1))) w))
                  (fV ((iV : (a : ↥(↑⟨W, m⟩ : Opens (↑X : Type u_1))) → ↥(↑(unop V) : Opens (↑X : Type u_1))) w))) →
            (↑(unop (op (Subtype.mk (p := fun (U : Opens (↑X : Type u_1)) ↦ x ∈ U) W m))) : Opens (↑X : Type u_1)) ⟶
              (↑(unop U) : Opens (↑X : Type u_1))
⊢ (↑(unop (op W)) : Opens (↑X : Type u_1)) ⟶ (↑(unop U) : Opens (↑X : Type u_1))

Tactic:
rcases W with ⟨W, m⟩