awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing
Goal:
X : TopCat
F : Presheaf (Type u_4) X
ι : Type x
U : ι → Opens (↑X : Type x)
s : (j : (CategoryTheory.Pairwise ι)ᵒᵖ) → (Functor.op (Pairwise.diagram U) ⋙ F).obj j
hs : s ∈ (Functor.op (Pairwise.diagram U) ⋙ F).sections
h :
  ∃! s_1 : ToType (FC := TypeCat.Fun) (F.obj (op (iSup U))),
    ∀ (i : (CategoryTheory.Pairwise ι)ᵒᵖ),
      Eq (α := (Functor.op (Pairwise.diagram U) ⋙ F).obj i)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) ((Functor.mapCone F (Cocone.op (Pairwise.cocone U))).π.app i) :
              (a :
                  ((Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ).obj (Functor.mapCone F (Pairwise.cocone U).op).pt).obj
                    i) →
                ((Pairwise.diagram U).op ⋙ F).obj i)
            s_1 :
          (Functor.op (Pairwise.diagram U) ⋙ F).obj i)
        (objPairwiseOfFamily (fun (i : ι) ↦ s (op (Pairwise.single i))) i : (Functor.op (Pairwise.diagram U) ⋙ F).obj i)
e_1 : (Functor.mapCone F (Cocone.op (Pairwise.cocone U))).pt = ToType (FC := TypeCat.Fun) (F.obj (op (iSup U)))
x : (Functor.mapCone F (Cocone.op (Pairwise.cocone U))).pt
a : (CategoryTheory.Pairwise ι)ᵒᵖ
i j : ι
⊢ s (op (Pairwise.pair i j)) = objPairwiseOfFamily (fun (i : ι) ↦ s (op (Pairwise.single i))) (op (Pairwise.pair i j))

Tactic:
(hs <| op <| Pairwise.Hom.left i j).symm

Premises used: CategoryTheory.Pairwise.Hom.left, Set.Mem, Quiver.Hom.op, Quiver.Hom.unop, CategoryTheory.Pairwise.diagramObj, Opposite.op, CategoryTheory.homOfLE, TopologicalSpace.Opens.infLELeft, Eq.symm, CategoryTheory.Pairwise.diagramMap, TopCat.Presheaf.objPairwiseOfFamily
-- Module: Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing
Goal:
X : TopCat
F : Presheaf (Type u_4) X
ι : Type x
U : ι → Opens (↑X : Type x)
s : (j : (CategoryTheory.Pairwise ι)ᵒᵖ) → (Functor.op (Pairwise.diagram U) ⋙ F).obj j
hs : s ∈ (Functor.op (Pairwise.diagram U) ⋙ F).sections
h :
  ∃! s_1 : ToType (FC := TypeCat.Fun) (F.obj (op (iSup U))),
    ∀ (i : (CategoryTheory.Pairwise ι)ᵒᵖ),
      Eq (α := (Functor.op (Pairwise.diagram U) ⋙ F).obj i)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) ((Functor.mapCone F (Cocone.op (Pairwise.cocone U))).π.app i) :
              (a :
                  ((Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ).obj (Functor.mapCone F (Pairwise.cocone U).op).pt).obj
                    i) →
                ((Pairwise.diagram U).op ⋙ F).obj i)
            s_1 :
          (Functor.op (Pairwise.diagram U) ⋙ F).obj i)
        (objPairwiseOfFamily (fun (i : ι) ↦ s (op (Pairwise.single i))) i : (Functor.op (Pairwise.diagram U) ⋙ F).obj i)
e_1 : (Functor.mapCone F (Cocone.op (Pairwise.cocone U))).pt = ToType (FC := TypeCat.Fun) (F.obj (op (iSup U)))
x : (Functor.mapCone F (Cocone.op (Pairwise.cocone U))).pt
a : (CategoryTheory.Pairwise ι)ᵒᵖ
i j : ι
⊢ s (op (Pairwise.pair i j)) = objPairwiseOfFamily (fun (i : ι) ↦ s (op (Pairwise.single i))) (op (Pairwise.pair i j))

Tactic:
exact (hs <| op <| Pairwise.Hom.left i j).symm

Premises used: CategoryTheory.Pairwise.Hom.left, Opposite.op, Eq.symm
-- Module: Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing
Goal:
X : TopCat
F : Presheaf (Type u_4) X
Fsh : F.IsSheafUniqueGluing (FC := TypeCat.Fun)
⊢ F.IsSheaf

Tactic:
(isSheaf_iff_isSheafUniqueGluing_types F).mpr Fsh

Premises used: Iff.mpr, TopCat.Presheaf.isSheaf_iff_isSheafUniqueGluing_types
-- Module: Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
FC : C → C → Type u_2
CC : C → Type u_3
inst_1 : (X Y : C) → FunLike.{u_2 + 1, u_3 + 1, u_3 + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{u_3, v_1, u_1, u_2} C FC (CC := CC)
inst_3 : HasLimitsOfSize.{x, x, v_1, u_1} C
inst_4 : Functor.ReflectsIsomorphisms.{v_1, u_1, u_3, u_3 + 1} (forget C (FC := FC) (CC := CC))
inst_5 : PreservesLimitsOfSize.{x, x, v_1, u_3, u_1, u_3 + 1} (forget C (FC := FC) (CC := CC))
X : TopCat
F : Presheaf.{x, v_1, u_1} C X
h : F.IsSheaf
ι : Type u_4
U : ι → Opens (↑X : Type x)
sf : (i : ι) → ToType.{u_3, v_1, u_1, u_2} (FC := FC) (CC := CC) (F.obj (op (U i)))
cpt : F.IsCompatible (FC := FC) (CC := CC) U sf
⊢ ∃! s : ToType.{u_3, v_1, u_1, u_2} (FC := FC) (CC := CC) (F.obj (op (iSup U))),
    F.IsGluing (FC := FC) (CC := CC) U sf s

Tactic:
((isSheaf_iff_isSheaf_comp' (forget C) F).mp h).isSheafUniqueGluing_types sf cpt

Premises used: TopCat.Presheaf.IsSheaf.isSheafUniqueGluing_types, CategoryTheory.Functor.comp, TopCat.Presheaf, TopCat.Presheaf.IsGluing, TopCat.Presheaf.isSheaf_iff_isSheaf_comp', CategoryTheory.forget, Iff.mp
-- Module: Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
FC : C → C → Type u_2
CC : C → Type u_3
inst_1 : (X Y : C) → FunLike.{u_2 + 1, u_3 + 1, u_3 + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{u_3, v_1, u_1, u_2} C FC (CC := CC)
inst_3 : HasLimitsOfSize.{x, x, v_1, u_1} C
inst_4 : Functor.ReflectsIsomorphisms.{v_1, u_1, u_3, u_3 + 1} (forget C (FC := FC) (CC := CC))
inst_5 : PreservesLimitsOfSize.{x, x, v_1, u_3, u_1, u_3 + 1} (forget C (FC := FC) (CC := CC))
X : TopCat
F : Presheaf.{x, v_1, u_1} C X
⊢ F.IsSheaf ↔ F.IsSheafUniqueGluing (FC := FC) (CC := CC)

Tactic:
Iff.trans (isSheaf_iff_isSheaf_comp' (forget C) F)
    (isSheaf_iff_isSheafUniqueGluing_types (F ⋙ forget C))

Premises used: TopCat.Presheaf.isSheaf_iff_isSheafUniqueGluing_types, CategoryTheory.Functor.comp, TopCat.Presheaf.isSheaf_iff_isSheaf_comp', CategoryTheory.forget, Iff.trans
-- Module: Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
FC : C → C → Type u_2
CC : C → Type u_3
inst_1 : (X Y : C) → FunLike.{u_2 + 1, u_3 + 1, u_3 + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{u_3, v_1, u_1, u_2} C FC (CC := CC)
inst_3 : HasLimitsOfSize.{x, x, v_1, u_1} C
inst_4 : Functor.ReflectsIsomorphisms.{v_1, u_1, u_3, u_3 + 1} (CategoryTheory.forget C (FC := FC) (CC := CC))
inst_5 : PreservesLimitsOfSize.{x, x, v_1, u_3, u_1, u_3 + 1} (CategoryTheory.forget C (FC := FC) (CC := CC))
X : TopCat
F : Sheaf.{x, v_1, u_1} C X
ι : Type u_4
U : ι → Opens (↑X : Type x)
sf :
  (i : ι) →
    ToType.{u_3, v_1, u_1, u_2} (FC := FC) (CC := CC)
      (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).obj (op (U i)))
h :
  IsCompatible (FC := FC) (CC := CC)
    (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x)))) U sf
⊢ ∃! s :
    ToType.{u_3, v_1, u_1, u_2} (FC := FC) (CC := CC)
      (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).obj (op (iSup U))),
    IsGluing (FC := FC) (CC := CC)
      (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x)))) U sf s

Tactic:
IsSheaf.isSheafUniqueGluing F.property U sf h

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.property, TopCat.Presheaf.IsSheaf.isSheafUniqueGluing
-- Module: Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
FC : C → C → Type u_2
CC : C → Type u_3
inst_1 : (X Y : C) → FunLike.{u_2 + 1, u_3 + 1, u_3 + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{u_3, v_1, u_1, u_2} C FC (CC := CC)
inst_3 : HasLimitsOfSize.{x, x, v_1, u_1} C
inst_4 : Functor.ReflectsIsomorphisms.{v_1, u_1, u_3, u_3 + 1} (CategoryTheory.forget C (FC := FC) (CC := CC))
inst_5 : PreservesLimitsOfSize.{x, x, v_1, u_3, u_1, u_3 + 1} (CategoryTheory.forget C (FC := FC) (CC := CC))
X : TopCat
F : Sheaf.{x, v_1, u_1} C X
ι : Type u_4
U : ι → Opens (↑X : Type x)
V : Opens (↑X : Type x)
iUV : (i : ι) → U i ⟶ V
hcover : V ≤ iSup U
sf :
  (i : ι) →
    ToType.{u_3, v_1, u_1, u_2} (FC := FC) (CC := CC)
      (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).obj (op (U i)))
h :
  IsCompatible (FC := FC) (CC := CC)
    (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x)))) U sf
⊢ V = iSup U

Tactic:
have V_eq_supr_U : V = iSup U := le_antisymm hcover (iSup_le fun i => (iUV i).le)
-- Module: Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
FC : C → C → Type u_2
CC : C → Type u_3
inst_1 : (X Y : C) → FunLike.{u_2 + 1, u_3 + 1, u_3 + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{u_3, v_1, u_1, u_2} C FC (CC := CC)
inst_3 : HasLimitsOfSize.{x, x, v_1, u_1} C
inst_4 : Functor.ReflectsIsomorphisms.{v_1, u_1, u_3, u_3 + 1} (CategoryTheory.forget C (FC := FC) (CC := CC))
inst_5 : PreservesLimitsOfSize.{x, x, v_1, u_3, u_1, u_3 + 1} (CategoryTheory.forget C (FC := FC) (CC := CC))
X : TopCat
F : Sheaf.{x, v_1, u_1} C X
ι : Type u_4
U : ι → Opens (↑X : Type x)
V : Opens (↑X : Type x)
iUV : (i : ι) → U i ⟶ V
hcover : V ≤ iSup U
sf :
  (i : ι) →
    ToType.{u_3, v_1, u_1, u_2} (FC := FC) (CC := CC)
      (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).obj (op (U i)))
h :
  IsCompatible (FC := FC) (CC := CC)
    (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x)))) U sf
V_eq_supr_U : V = iSup U
obtain :
  ∀
    (gl :
      ToType.{u_3, v_1, u_1, u_2} (FC := FC) (CC := CC)
        (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).obj (op (iSup U))))
    (gl_spec :
      IsGluing (FC := FC) (CC := CC)
        (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x)))) U sf gl)
    (gl_uniq :
      ∀
        (y :
          ToType.{u_3, v_1, u_1, u_2} (FC := FC) (CC := CC)
            (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).obj
              (op (iSup U)))),
        (fun
                (s :
                  ToType.{u_3, v_1, u_1, u_2} (FC := FC) (CC := CC)
                    (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).obj
                      (op (iSup U)))) ↦
              IsGluing (FC := FC) (CC := CC)
                (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x)))) U sf s)
            y →
          y = gl),
    ∃! s :
      ToType.{u_3, v_1, u_1, u_2} (FC := FC) (CC := CC)
        (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).obj (op V)),
      ∀ (i : ι),
        (ConcreteCategory.hom (FC := FC) (CC := CC)
                (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).map
                  (iUV i).op) :
              (a : CC (F.obj.obj (op V))) → CC (F.obj.obj (op (U i))))
            s =
          sf i
⊢ ∃! s :
    ToType.{u_3, v_1, u_1, u_2} (FC := FC) (CC := CC)
      (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).obj (op V)),
    ∀ (i : ι),
      (ConcreteCategory.hom (FC := FC) (CC := CC)
              (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).map (iUV i).op) :
            (a : CC (F.obj.obj (op V))) → CC (F.obj.obj (op (U i))))
          s =
        sf i

Tactic:
obtain ⟨gl, gl_spec, gl_uniq⟩ := F.existsUnique_gluing U sf h

Premises used: TopCat.Sheaf.existsUnique_gluing
-- Module: Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
FC : C → C → Type u_2
CC : C → Type u_3
inst_1 : (X Y : C) → FunLike.{u_2 + 1, u_3 + 1, u_3 + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{u_3, v_1, u_1, u_2} C FC (CC := CC)
inst_3 : HasLimitsOfSize.{x, x, v_1, u_1} C
inst_4 : Functor.ReflectsIsomorphisms.{v_1, u_1, u_3, u_3 + 1} (CategoryTheory.forget C (FC := FC) (CC := CC))
inst_5 : PreservesLimitsOfSize.{x, x, v_1, u_3, u_1, u_3 + 1} (CategoryTheory.forget C (FC := FC) (CC := CC))
X : TopCat
F : Sheaf.{x, v_1, u_1} C X
ι : Type u_4
U : ι → Opens (↑X : Type x)
V : Opens (↑X : Type x)
iUV : (i : ι) → U i ⟶ V
hcover : V ≤ iSup U
sf :
  (i : ι) →
    ToType.{u_3, v_1, u_1, u_2} (FC := FC) (CC := CC)
      (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).obj (op (U i)))
h :
  IsCompatible (FC := FC) (CC := CC)
    (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x)))) U sf
V_eq_supr_U : V = iSup U
gl :
  ToType.{u_3, v_1, u_1, u_2} (FC := FC) (CC := CC)
    (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).obj (op (iSup U)))
gl_spec :
  IsGluing (FC := FC) (CC := CC)
    (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x)))) U sf gl
gl_uniq :
  ∀
    (y :
      ToType.{u_3, v_1, u_1, u_2} (FC := FC) (CC := CC)
        (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).obj (op (iSup U)))),
    (fun
            (s :
              ToType.{u_3, v_1, u_1, u_2} (FC := FC) (CC := CC)
                (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).obj
                  (op (iSup U)))) ↦
          IsGluing (FC := FC) (CC := CC)
            (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x)))) U sf s)
        y →
      y = gl
⊢ ∃! s :
    ToType.{u_3, v_1, u_1, u_2} (FC := FC) (CC := CC)
      (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).obj (op V)),
    ∀ (i : ι),
      (ConcreteCategory.hom (FC := FC) (CC := CC)
              (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).map (iUV i).op) :
            (a : CC (F.obj.obj (op V))) → CC (F.obj.obj (op (U i))))
          s =
        sf i

Tactic:
⟨F.1.map (eqToHom V_eq_supr_U).op gl, ?_, ?_⟩

Premises used: CategoryTheory.ConcreteCategory.hom, Quiver.Hom.op, CategoryTheory.eqToHom, CategoryTheory.ObjectProperty.FullSubcategory.obj, CategoryTheory.Functor.map, ExistsUnique, And.intro, Exists.intro, DFunLike.coe
-- Module: Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
FC : C → C → Type u_2
CC : C → Type u_3
inst_1 : (X Y : C) → FunLike.{u_2 + 1, u_3 + 1, u_3 + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{u_3, v_1, u_1, u_2} C FC (CC := CC)
inst_3 : HasLimitsOfSize.{x, x, v_1, u_1} C
inst_4 : Functor.ReflectsIsomorphisms.{v_1, u_1, u_3, u_3 + 1} (CategoryTheory.forget C (FC := FC) (CC := CC))
inst_5 : PreservesLimitsOfSize.{x, x, v_1, u_3, u_1, u_3 + 1} (CategoryTheory.forget C (FC := FC) (CC := CC))
X : TopCat
F : Sheaf.{x, v_1, u_1} C X
ι : Type u_4
U : ι → Opens (↑X : Type x)
V : Opens (↑X : Type x)
iUV : (i : ι) → U i ⟶ V
hcover : V ≤ iSup U
sf :
  (i : ι) →
    ToType.{u_3, v_1, u_1, u_2} (FC := FC) (CC := CC)
      (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).obj (op (U i)))
h :
  IsCompatible (FC := FC) (CC := CC)
    (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x)))) U sf
V_eq_supr_U : V = iSup U
gl :
  ToType.{u_3, v_1, u_1, u_2} (FC := FC) (CC := CC)
    (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).obj (op (iSup U)))
gl_spec :
  IsGluing (FC := FC) (CC := CC)
    (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x)))) U sf gl
gl_uniq :
  ∀
    (y :
      ToType.{u_3, v_1, u_1, u_2} (FC := FC) (CC := CC)
        (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).obj (op (iSup U)))),
    (fun
            (s :
              ToType.{u_3, v_1, u_1, u_2} (FC := FC) (CC := CC)
                (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).obj
                  (op (iSup U)))) ↦
          IsGluing (FC := FC) (CC := CC)
            (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x)))) U sf s)
        y →
      y = gl
i : ι
refine_1 :
  (ConcreteCategory.hom (FC := FC) (CC := CC)
          (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).map
            (Quiver.Hom.op (eqToHom V_eq_supr_U) ≫ (iUV i).op)) :
        (a : CC (F.obj.obj (op (iSup U)))) → CC (F.obj.obj (op (U i))))
      gl =
    sf i
⊢ (ConcreteCategory.hom (FC := FC) (CC := CC)
          (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).map (iUV i).op) :
        (a : CC (F.obj.obj (op V))) → CC (F.obj.obj (op (U i))))
      ((ConcreteCategory.hom (FC := FC) (CC := CC)
              (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).map
                (Quiver.Hom.op (eqToHom V_eq_supr_U))) :
            (a : CC (F.obj.obj (op (iSup U)))) → CC (F.obj.obj (op V)))
          gl :
        CC (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).obj (op V))) =
    sf i

Tactic:
rw [← ConcreteCategory.comp_apply, ← F.1.map_comp]

Premises used: CategoryTheory.ConcreteCategory.comp_apply, CategoryTheory.ObjectProperty.FullSubcategory.obj, CategoryTheory.Functor.map_comp
-- Module: Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
FC : C → C → Type u_2
CC : C → Type u_3
inst_1 : (X Y : C) → FunLike.{u_2 + 1, u_3 + 1, u_3 + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{u_3, v_1, u_1, u_2} C FC (CC := CC)
inst_3 : HasLimitsOfSize.{x, x, v_1, u_1} C
inst_4 : Functor.ReflectsIsomorphisms.{v_1, u_1, u_3, u_3 + 1} (CategoryTheory.forget C (FC := FC) (CC := CC))
inst_5 : PreservesLimitsOfSize.{x, x, v_1, u_3, u_1, u_3 + 1} (CategoryTheory.forget C (FC := FC) (CC := CC))
X : TopCat
F : Sheaf.{x, v_1, u_1} C X
ι : Type u_4
U : ι → Opens (↑X : Type x)
V : Opens (↑X : Type x)
iUV : (i : ι) → U i ⟶ V
hcover : V ≤ iSup U
sf :
  (i : ι) →
    ToType.{u_3, v_1, u_1, u_2} (FC := FC) (CC := CC)
      (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).obj (op (U i)))
h :
  IsCompatible (FC := FC) (CC := CC)
    (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x)))) U sf
V_eq_supr_U : V = iSup U
gl :
  ToType.{u_3, v_1, u_1, u_2} (FC := FC) (CC := CC)
    (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).obj (op (iSup U)))
gl_spec :
  IsGluing (FC := FC) (CC := CC)
    (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x)))) U sf gl
gl_uniq :
  ∀
    (y :
      ToType.{u_3, v_1, u_1, u_2} (FC := FC) (CC := CC)
        (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).obj (op (iSup U)))),
    (fun
            (s :
              ToType.{u_3, v_1, u_1, u_2} (FC := FC) (CC := CC)
                (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).obj
                  (op (iSup U)))) ↦
          IsGluing (FC := FC) (CC := CC)
            (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x)))) U sf s)
        y →
      y = gl
i : ι
⊢ (ConcreteCategory.hom (FC := FC) (CC := CC)
          (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).map
            (Quiver.Hom.op (eqToHom V_eq_supr_U) ≫ (iUV i).op)) :
        (a : CC (F.obj.obj (op (iSup U)))) → CC (F.obj.obj (op (U i))))
      gl =
    sf i

Tactic:
gl_spec i

Premises used: Set.Mem, iSup, TopologicalSpace.Opens.leSupr, CategoryTheory.homOfLE
-- Module: Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
FC : C → C → Type u_2
CC : C → Type u_3
inst_1 : (X Y : C) → FunLike.{u_2 + 1, u_3 + 1, u_3 + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory.{u_3, v_1, u_1, u_2} C FC (CC := CC)
inst_3 : HasLimitsOfSize.{x, x, v_1, u_1} C
inst_4 : Functor.ReflectsIsomorphisms.{v_1, u_1, u_3, u_3 + 1} (CategoryTheory.forget C (FC := FC) (CC := CC))
inst_5 : PreservesLimitsOfSize.{x, x, v_1, u_3, u_1, u_3 + 1} (CategoryTheory.forget C (FC := FC) (CC := CC))
X : TopCat
F : Sheaf.{x, v_1, u_1} C X
ι : Type u_4
U : ι → Opens (↑X : Type x)
V : Opens (↑X : Type x)
iUV : (i : ι) → U i ⟶ V
hcover : V ≤ iSup U
sf :
  (i : ι) →
    ToType.{u_3, v_1, u_1, u_2} (FC := FC) (CC := CC)
      (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).obj (op (U i)))
h :
  IsCompatible (FC := FC) (CC := CC)
    (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x)))) U sf
V_eq_supr_U : V = iSup U
gl :
  ToType.{u_3, v_1, u_1, u_2} (FC := FC) (CC := CC)
    (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).obj (op (iSup U)))
gl_spec :
  IsGluing (FC := FC) (CC := CC)
    (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x)))) U sf gl
gl_uniq :
  ∀
    (y :
      ToType.{u_3, v_1, u_1, u_2} (FC := FC) (CC := CC)
        (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).obj (op (iSup U)))),
    (fun
            (s :
              ToType.{u_3, v_1, u_1, u_2} (FC := FC) (CC := CC)
                (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).obj
                  (op (iSup U)))) ↦
          IsGluing (FC := FC) (CC := CC)
            (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x)))) U sf s)
        y →
      y = gl
i : ι
⊢ (ConcreteCategory.hom (FC := FC) (CC := CC)
          (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).map
            (Quiver.Hom.op (eqToHom V_eq_supr_U) ≫ (iUV i).op)) :
        (a : CC (F.obj.obj (op (iSup U)))) → CC (F.obj.obj (op (U i))))
      gl =
    sf i

Tactic:
exact gl_spec i