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

Tactic:
exact h i
-- Module: Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing
Goal:
X : TopCat
F : Presheaf (Type u_4) X
ι : Type u_5
U : ι → Opens (↑X : Type x)
sf : (i : ι) → ToType (FC := TypeCat.Fun) (F.obj (op (U i)))
s : ToType (FC := TypeCat.Fun) (F.obj (op (iSup U)))
h : F.IsGluing (FC := TypeCat.Fun) U sf s
i j : ι
pair :
  Eq (α := (fun (X : Type u_4) ↦ X) ((Functor.op (Pairwise.diagram U) ⋙ F).obj (op (Pairwise.pair i j))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            ((Functor.mapCone F (Cocone.op (Pairwise.cocone U))).π.app (op (Pairwise.single i)) ≫
              (Functor.op (Pairwise.diagram U) ⋙ F).map (op (Pairwise.Hom.left i j))) :
          (a :
              (fun (X : Type u_4) ↦ X)
                (((Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ).obj (Functor.mapCone F (Pairwise.cocone U).op).pt).obj
                  (op (Pairwise.pair i j)))) →
            (fun (X : Type u_4) ↦ X) (((Pairwise.diagram U).op ⋙ F).obj (op (Pairwise.pair i j))))
        s :
      (fun (X : Type u_4) ↦ X) ((Functor.op (Pairwise.diagram U) ⋙ F).obj (op (Pairwise.pair i j))))
    (objPairwiseOfFamily sf (op (Pairwise.pair i j)) :
      (Functor.op (Pairwise.diagram U) ⋙ F).obj (op (Pairwise.pair i j)))
⊢ Eq (α := (fun (X : Type u_4) ↦ X) ((Functor.op (Pairwise.diagram U) ⋙ F).obj (op (Pairwise.pair i j))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            ((Functor.mapCone F (Cocone.op (Pairwise.cocone U))).π.app (op (Pairwise.pair i j))) :
          (a :
              (fun (X : Type u_4) ↦ X)
                (((Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ).obj (Functor.mapCone F (Pairwise.cocone U).op).pt).obj
                  (op (Pairwise.pair i j)))) →
            (fun (X : Type u_4) ↦ X) (((Pairwise.diagram U).op ⋙ F).obj (op (Pairwise.pair i j))))
        s :
      (fun (X : Type u_4) ↦ X) ((Functor.op (Pairwise.diagram U) ⋙ F).obj (op (Pairwise.pair i j))))
    (objPairwiseOfFamily sf (op (Pairwise.pair i j)) :
      (Functor.op (Pairwise.diagram U) ⋙ F).obj (op (Pairwise.pair i j)))

Tactic:
rw [← (F.mapCone (Pairwise.cocone U).op).w (op <| Pairwise.Hom.left i j)]

Premises used: CategoryTheory.Pairwise.Hom.left, Opposite.op, CategoryTheory.Limits.Cone.w, CategoryTheory.Functor.mapCone, CategoryTheory.Pairwise.cocone, CategoryTheory.Limits.Cocone.op
-- Module: Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing
Goal:
X : TopCat
F : Presheaf (Type u_4) X
ι : Type u_5
U : ι → Opens (↑X : Type x)
sf : (i : ι) → ToType (FC := TypeCat.Fun) (F.obj (op (U i)))
s : ToType (FC := TypeCat.Fun) (F.obj (op (iSup U)))
h : F.IsGluing (FC := TypeCat.Fun) U sf s
i j : ι
⊢ Eq (α := (fun (X : Type u_4) ↦ X) ((Functor.op (Pairwise.diagram U) ⋙ F).obj (op (Pairwise.pair i j))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            ((Functor.mapCone F (Cocone.op (Pairwise.cocone U))).π.app (op (Pairwise.single i)) ≫
              (Functor.op (Pairwise.diagram U) ⋙ F).map (op (Pairwise.Hom.left i j))) :
          (a :
              (fun (X : Type u_4) ↦ X)
                (((Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ).obj (Functor.mapCone F (Pairwise.cocone U).op).pt).obj
                  (op (Pairwise.pair i j)))) →
            (fun (X : Type u_4) ↦ X) (((Pairwise.diagram U).op ⋙ F).obj (op (Pairwise.pair i j))))
        s :
      (fun (X : Type u_4) ↦ X) ((Functor.op (Pairwise.diagram U) ⋙ F).obj (op (Pairwise.pair i j))))
    (objPairwiseOfFamily sf (op (Pairwise.pair i j)) :
      (Functor.op (Pairwise.diagram U) ⋙ F).obj (op (Pairwise.pair i j)))

Tactic:
congr_arg _ (h i)

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

Tactic:
exact congr_arg _ (h i)

Premises used: congr_arg
-- Module: Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing
Goal:
X : TopCat
F : Presheaf (Type u_4) X
ι : Type u_5
U : ι → Opens (↑X : Type x)
h : F.IsSheaf
sf : (i : ι) → F.obj (op (U i))
cpt : F.IsCompatible (FC := TypeCat.Fun) U sf
simp_rw :
  ∃! s : F.obj (op (iSup U)),
    ∀ (i : (CategoryTheory.Pairwise ι)ᵒᵖ),
      (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 =
        objPairwiseOfFamily sf i
⊢ ∃! s : F.obj (op (iSup U)), F.IsGluing (FC := TypeCat.Fun) U sf s

Tactic:
simp_rw [isGluing_iff_pairwise]

Premises used: TopCat.Presheaf.isGluing_iff_pairwise
-- Module: Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing
Goal:
X : TopCat
F : Presheaf (Type u_4) X
ι : Type u_5
U : ι → Opens (↑X : Type x)
h : F.IsSheaf
sf : (i : ι) → F.obj (op (U i))
cpt : F.IsCompatible (FC := TypeCat.Fun) U sf
⊢ ∃! s : F.obj (op (iSup U)),
    ∀ (i : (CategoryTheory.Pairwise ι)ᵒᵖ),
      (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 =
        objPairwiseOfFamily sf i

Tactic:
(Types.isLimit_iff _).mp (h.isSheafPairwiseIntersections U) _ cpt.sectionPairwise.prop

Premises used: iSup, Subtype.prop, TopCat.Presheaf.IsCompatible.sectionPairwise, Iff.mp, TopCat.Presheaf.IsSheaf.isSheafPairwiseIntersections, CategoryTheory.Limits.Types.isLimit_iff
-- Module: Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing
Goal:
X : TopCat
F : Presheaf (Type u_4) X
ι : Type u_5
U : ι → Opens (↑X : Type x)
h : F.IsSheaf
sf : (i : ι) → F.obj (op (U i))
cpt : F.IsCompatible (FC := TypeCat.Fun) U sf
⊢ ∃! s : F.obj (op (iSup U)),
    ∀ (i : (CategoryTheory.Pairwise ι)ᵒᵖ),
      (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 =
        objPairwiseOfFamily sf i

Tactic:
exact (Types.isLimit_iff _).mp (h.isSheafPairwiseIntersections U) _ cpt.sectionPairwise.prop

Premises used: Subtype.prop, TopCat.Presheaf.IsCompatible.sectionPairwise, Iff.mp, TopCat.Presheaf.IsSheaf.isSheafPairwiseIntersections, CategoryTheory.Limits.Types.isLimit_iff
-- Module: Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing
Goal:
X : TopCat
F : Presheaf (Type u_4) X
simp_rw :
  (∀ ⦃ι : Type x⦄ (U : ι → Opens (↑X : Type x)),
      ∀ s ∈ (Functor.op (Pairwise.diagram U) ⋙ F).sections,
        ∃! x : (Functor.mapCone F (Cocone.op (Pairwise.cocone U))).pt,
          ∀ (j : (CategoryTheory.Pairwise ι)ᵒᵖ),
            (ConcreteCategory.hom (FC := TypeCat.Fun) ((Functor.mapCone F (Cocone.op (Pairwise.cocone U))).π.app j) :
                  (a :
                      ((Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ).obj
                            (Functor.mapCone F (Pairwise.cocone U).op).pt).obj
                        j) →
                    ((Pairwise.diagram U).op ⋙ F).obj j)
                x =
              s j) ↔
    ∀ ⦃ι : Type x⦄ (U : ι → Opens (↑X : Type x)) (sf : (i : ι) → ToType (FC := TypeCat.Fun) (F.obj (op (U i)))),
      F.IsCompatible (FC := TypeCat.Fun) U sf →
        ∃! s : ToType (FC := TypeCat.Fun) (F.obj (op (iSup U))),
          ∀ (i : (CategoryTheory.Pairwise ι)ᵒᵖ),
            (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 =
              objPairwiseOfFamily sf i
⊢ F.IsSheaf ↔ F.IsSheafUniqueGluing (FC := TypeCat.Fun)

Tactic:
simp_rw [isSheaf_iff_isSheafPairwiseIntersections, IsSheafPairwiseIntersections,
    Types.isLimit_iff, IsSheafUniqueGluing, isGluing_iff_pairwise]

Premises used: TopCat.Presheaf.IsSheafPairwiseIntersections, TopCat.Presheaf.isSheaf_iff_isSheafPairwiseIntersections, TopCat.Presheaf.IsSheafUniqueGluing, TopCat.Presheaf.isGluing_iff_pairwise, CategoryTheory.Limits.Types.isLimit_iff
-- Module: Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing
Goal:
X : TopCat
F : Presheaf (Type u_4) X
⊢ (∀ ⦃ι : Type x⦄ (U : ι → Opens (↑X : Type x)),
      ∀ s ∈ (Functor.op (Pairwise.diagram U) ⋙ F).sections,
        ∃! x : (Functor.mapCone F (Cocone.op (Pairwise.cocone U))).pt,
          ∀ (j : (CategoryTheory.Pairwise ι)ᵒᵖ),
            (ConcreteCategory.hom (FC := TypeCat.Fun) ((Functor.mapCone F (Cocone.op (Pairwise.cocone U))).π.app j) :
                  (a :
                      ((Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ).obj
                            (Functor.mapCone F (Pairwise.cocone U).op).pt).obj
                        j) →
                    ((Pairwise.diagram U).op ⋙ F).obj j)
                x =
              s j) ↔
    ∀ ⦃ι : Type x⦄ (U : ι → Opens (↑X : Type x)) (sf : (i : ι) → ToType (FC := TypeCat.Fun) (F.obj (op (U i)))),
      F.IsCompatible (FC := TypeCat.Fun) U sf →
        ∃! s : ToType (FC := TypeCat.Fun) (F.obj (op (iSup U))),
          ∀ (i : (CategoryTheory.Pairwise ι)ᵒᵖ),
            (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 =
              objPairwiseOfFamily sf i

Tactic:
forall₂_congr fun ι U ↦ ⟨fun h sf cpt ↦ ?_, fun h s hs ↦ ?_⟩

Premises used: forall₂_congr, Iff.intro
-- Module: Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing
Goal:
X : TopCat
F : Presheaf (Type u_4) X
ι : Type x
U : ι → Opens (↑X : Type x)
h :
  ∀ s ∈ (Functor.op (Pairwise.diagram U) ⋙ F).sections,
    ∃! x : (Functor.mapCone F (Cocone.op (Pairwise.cocone U))).pt,
      ∀ (j : (CategoryTheory.Pairwise ι)ᵒᵖ),
        (ConcreteCategory.hom (FC := TypeCat.Fun) ((Functor.mapCone F (Cocone.op (Pairwise.cocone U))).π.app j) :
              (a :
                  ((Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ).obj (Functor.mapCone F (Pairwise.cocone U).op).pt).obj
                    j) →
                ((Pairwise.diagram U).op ⋙ F).obj j)
            x =
          s j
sf : (i : ι) → ToType (FC := TypeCat.Fun) (F.obj (op (U i)))
cpt : F.IsCompatible (FC := TypeCat.Fun) U sf
⊢ ∃! s : ToType (FC := TypeCat.Fun) (F.obj (op (iSup U))),
    ∀ (i : (CategoryTheory.Pairwise ι)ᵒᵖ),
      (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 =
        objPairwiseOfFamily sf i

Tactic:
h _ cpt.sectionPairwise.prop

Premises used: iSup, Subtype.prop, TopCat.Presheaf.IsCompatible.sectionPairwise
-- Module: Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing
Goal:
X : TopCat
F : Presheaf (Type u_4) X
ι : Type x
U : ι → Opens (↑X : Type x)
h :
  ∀ s ∈ (Functor.op (Pairwise.diagram U) ⋙ F).sections,
    ∃! x : (Functor.mapCone F (Cocone.op (Pairwise.cocone U))).pt,
      ∀ (j : (CategoryTheory.Pairwise ι)ᵒᵖ),
        (ConcreteCategory.hom (FC := TypeCat.Fun) ((Functor.mapCone F (Cocone.op (Pairwise.cocone U))).π.app j) :
              (a :
                  ((Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ).obj (Functor.mapCone F (Pairwise.cocone U).op).pt).obj
                    j) →
                ((Pairwise.diagram U).op ⋙ F).obj j)
            x =
          s j
sf : (i : ι) → ToType (FC := TypeCat.Fun) (F.obj (op (U i)))
cpt : F.IsCompatible (FC := TypeCat.Fun) U sf
⊢ ∃! s : ToType (FC := TypeCat.Fun) (F.obj (op (iSup U))),
    ∀ (i : (CategoryTheory.Pairwise ι)ᵒᵖ),
      (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 =
        objPairwiseOfFamily sf i

Tactic:
exact h _ cpt.sectionPairwise.prop

Premises used: Subtype.prop, TopCat.Presheaf.IsCompatible.sectionPairwise
-- Module: Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing
Goal:
X : TopCat
F : Presheaf (Type u_4) X
ι : Type x
U : ι → Opens (↑X : Type x)
h :
  ∀ (sf : (i : ι) → ToType (FC := TypeCat.Fun) (F.obj (op (U i)))),
    F.IsCompatible (FC := TypeCat.Fun) U sf →
      ∃! s : ToType (FC := TypeCat.Fun) (F.obj (op (iSup U))),
        ∀ (i : (CategoryTheory.Pairwise ι)ᵒᵖ),
          (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 =
            objPairwiseOfFamily sf i
s : (j : (CategoryTheory.Pairwise ι)ᵒᵖ) → (Functor.op (Pairwise.diagram U) ⋙ F).obj j
hs : s ∈ (Functor.op (Pairwise.diagram U) ⋙ F).sections
⊢ ∃! 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)

Tactic:
specialize h (fun i ↦ s <| op <| Pairwise.single i) fun i j ↦
      (hs <| op <| Pairwise.Hom.left i j).trans (hs <| op <| Pairwise.Hom.right i j).symm

Premises used: CategoryTheory.Pairwise.Hom.right, CategoryTheory.Pairwise.Hom.left, CategoryTheory.Pairwise.single, Opposite.op, Eq.symm, Eq.trans
-- 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)
⊢ ∃! 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)

Tactic:
h
-- 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)
h₁ :
  (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 ι)ᵒᵖ),
      s = objPairwiseOfFamily fun (i : ι) ↦ s (op (Pairwise.single i))
⊢ ∃! x : (Functor.mapCone F (Cocone.op (Pairwise.cocone U))).pt,
    ∀ (j : (CategoryTheory.Pairwise ι)ᵒᵖ),
      (ConcreteCategory.hom (FC := TypeCat.Fun) ((Functor.mapCone F (Cocone.op (Pairwise.cocone U))).π.app j) :
            (a :
                ((Functor.const (CategoryTheory.Pairwise ι)ᵒᵖ).obj (Functor.mapCone F (Pairwise.cocone U).op).pt).obj
                  j) →
              ((Pairwise.diagram U).op ⋙ F).obj j)
          x =
        s j

Tactic:
convert! h
-- 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 ι)ᵒᵖ
h₁ :
  ∀ (i : ι),
    s (op (Pairwise.single i)) = objPairwiseOfFamily (fun (i : ι) ↦ s (op (Pairwise.single i))) (op (Pairwise.single i))
h₂ :
  ∀ (i j : ι),
    s (op (Pairwise.pair i j)) = objPairwiseOfFamily (fun (i : ι) ↦ s (op (Pairwise.single i))) (op (Pairwise.pair i j))
⊢ s = objPairwiseOfFamily fun (i : ι) ↦ s (op (Pairwise.single i))

Tactic:
ext (i | ⟨i, j⟩)
-- 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 : ι
⊢ s (op (Pairwise.single i)) = objPairwiseOfFamily (fun (i : ι) ↦ s (op (Pairwise.single i))) (op (Pairwise.single i))

Tactic:
rfl