awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
U₁ U₂ V : Opens (↑X : Type x)
i₁ : U₁ ⟶ V
i₂ : U₂ ⟶ V
hcover : V ≤ U₁ ⊔ U₂
s t :
  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))
h₁ :
  Eq (α := CC (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).obj (op U₁)))
    ((ConcreteCategory.hom (FC := FC) (CC := CC)
            (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).map i₁.op) :
          (a : CC (F.obj.obj (op V))) → CC (F.obj.obj (op U₁)))
        s :
      CC (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).obj (op U₁)))
    ((ConcreteCategory.hom (FC := FC) (CC := CC)
            (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).map i₁.op) :
          (a : CC (F.obj.obj (op V))) → CC (F.obj.obj (op U₁)))
        t :
      CC (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).obj (op U₁)))
h₂ :
  Eq (α := CC (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).obj (op U₂)))
    ((ConcreteCategory.hom (FC := FC) (CC := CC)
            (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).map i₂.op) :
          (a : CC (F.obj.obj (op V))) → CC (F.obj.obj (op U₂)))
        s :
      CC (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).obj (op U₂)))
    ((ConcreteCategory.hom (FC := FC) (CC := CC)
            (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).map i₂.op) :
          (a : CC (F.obj.obj (op V))) → CC (F.obj.obj (op U₂)))
        t :
      CC (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).obj (op U₂)))
⊢ U₂ ≤ ⨆ (t : Bool), if t = true then U₁ else U₂

Tactic:
le_iSup (fun t : Bool => if t then U₁ else U₂) false

Premises used: Set.Mem, le_iSup, Bool.true, Bool.false, Eq, ite
-- 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
U₁ U₂ V : Opens (↑X : Type x)
i₁ : U₁ ⟶ V
i₂ : U₂ ⟶ V
hcover : V ≤ U₁ ⊔ U₂
s t :
  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))
h₁ :
  Eq (α := CC (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).obj (op U₁)))
    ((ConcreteCategory.hom (FC := FC) (CC := CC)
            (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).map i₁.op) :
          (a : CC (F.obj.obj (op V))) → CC (F.obj.obj (op U₁)))
        s :
      CC (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).obj (op U₁)))
    ((ConcreteCategory.hom (FC := FC) (CC := CC)
            (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).map i₁.op) :
          (a : CC (F.obj.obj (op V))) → CC (F.obj.obj (op U₁)))
        t :
      CC (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).obj (op U₁)))
h₂ :
  Eq (α := CC (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).obj (op U₂)))
    ((ConcreteCategory.hom (FC := FC) (CC := CC)
            (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).map i₂.op) :
          (a : CC (F.obj.obj (op V))) → CC (F.obj.obj (op U₂)))
        s :
      CC (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).obj (op U₂)))
    ((ConcreteCategory.hom (FC := FC) (CC := CC)
            (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).map i₂.op) :
          (a : CC (F.obj.obj (op V))) → CC (F.obj.obj (op U₂)))
        t :
      CC (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).obj (op U₂)))
⊢ U₂ ≤ ⨆ (t : Bool), if t = true then U₁ else U₂

Tactic:
exact le_iSup (fun t : Bool => if t then U₁ else U₂) false

Premises used: le_iSup, Bool.true, Bool.false, Eq, ite
-- 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)
G : Sheaf.{x, v_1, u_1} C X
f : F ⟶ G
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)))
t :
  ToType.{u_3, v_1, u_1, u_2} (FC := FC) (CC := CC)
    (G.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).obj (op V))
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 :
  IsGluing (FC := FC) (CC := CC)
    (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x)))) U sf s
hV : ∀ (i : ι), U i ≤ V
ht :
  ∀ (i : ι),
    Eq.{u_3 + 1} (α :=
      CC (G.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).obj (op (U i))))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (f.hom.app (op (U i))) :
            (a : CC (F.obj.obj (op (U i)))) → CC (G.obj.obj (op (U i))))
          (sf i) :
        CC (G.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).obj (op (U i))))
      ((ConcreteCategory.hom (FC := FC) (CC := CC)
              (G.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).map
                (homOfLE ⋯).op) :
            (a : CC (G.obj.obj (op V))) → CC (G.obj.obj (op (U i))))
          t :
        CC (G.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).obj (op (U i))))
⊢ Eq (α :=
    CC (G.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).obj (op (iSup U))))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (f.hom.app (op (iSup U))) :
          (a : CC (F.obj.obj (op (iSup U)))) → CC (G.obj.obj (op (iSup U))))
        s :
      CC (G.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).obj (op (iSup U))))
    ((ConcreteCategory.hom (FC := FC) (CC := CC)
            (G.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).map
              (homOfLE ⋯).op) :
          (a : CC (G.obj.obj (op V))) → CC (G.obj.obj (op (iSup U))))
        t :
      CC (G.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).obj (op (iSup U))))

Tactic:
eq_of_locally_eq G U _ _ (fun _ ↦ ?_)

Premises used: TopCat.Sheaf.eq_of_locally_eq
-- 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)
G : Sheaf.{x, v_1, u_1} C X
f : F ⟶ G
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)))
t :
  ToType.{u_3, v_1, u_1, u_2} (FC := FC) (CC := CC)
    (G.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).obj (op V))
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 :
  IsGluing (FC := FC) (CC := CC)
    (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x)))) U sf s
hV : ∀ (i : ι), U i ≤ V
ht :
  ∀ (i : ι),
    Eq.{u_3 + 1} (α :=
      CC (G.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).obj (op (U i))))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (f.hom.app (op (U i))) :
            (a : CC (F.obj.obj (op (U i)))) → CC (G.obj.obj (op (U i))))
          (sf i) :
        CC (G.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).obj (op (U i))))
      ((ConcreteCategory.hom (FC := FC) (CC := CC)
              (G.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).map
                (homOfLE ⋯).op) :
            (a : CC (G.obj.obj (op V))) → CC (G.obj.obj (op (U i))))
          t :
        CC (G.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).obj (op (U i))))
x : ι
⊢ Eq (α := CC (G.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).obj (op (U x))))
    ((ConcreteCategory.hom (FC := FC) (CC := CC)
            (G.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).map
              (homOfLE ⋯).op) :
          (a : CC (G.obj.obj (op V))) → CC (G.obj.obj (op (U x))))
        t :
      CC (G.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).obj (op (U x))))
    ((ConcreteCategory.hom (FC := FC) (CC := CC)
            (G.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).map
              ((homOfLE ⋯).op ≫ (leSupr U x).op)) :
          (a : CC (G.obj.obj (op V))) → CC (G.obj.obj (op (U x))))
        t :
      CC (G.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type x))).obj (op (U x))))

Tactic:
rfl
-- Module: Mathlib.Topology.Sheaves.SheafOfFunctions
Goal:
X : TopCat
T : Type u_1
⊢ (X.presheafToType T).IsSheaf

Tactic:
toTypes_isSheaf X fun _ => T

Premises used: TopCat.presheafToType, TopCat.Presheaf.toTypes_isSheaf
-- Module: Mathlib.Topology.Sheaves.Sheafify
Goal:
X : TopCat
F : Presheaf (Type v) X
U U' : (Opens (↑X : Type v))ᵒᵖ
f : U ⟶ U'
h :
  ∀ (x : F.obj U),
    TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (F.map f ≫
            ↾fun (f : F.obj U') ↦
              Subtype.mk (p := fun (f : (x : ↥(unop U')) → (fun (x : (↑X : Type v)) ↦ F.stalk x) (↑x : (↑X : Type v))) ↦
                (Sheafify.isLocallyGerm F).toPrelocalPredicate (T := fun (x : (↑X : Type v)) ↦ F.stalk x).pred (T :=
                  fun (x : (↑X : Type v)) ↦ F.stalk x) f)
                (fun (x : ↥(unop U')) ↦
                  (ConcreteCategory.hom (FC := TypeCat.Fun) (F.germ (unop U') (↑x : (↑X : Type v)) ⋯) :
                      (a : (fun (X : Type v) ↦ X) (F.obj (op (unop U')))) →
                        (fun (X : Type v) ↦ X) (F.stalk (↑x : (↑X : Type v))))
                    f)
                ⋯))
        x =
      TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          ((↾fun (f : F.obj U) ↦
              Subtype.mk (p := fun (f : (x : ↥(unop U)) → (fun (x : (↑X : Type v)) ↦ F.stalk x) (↑x : (↑X : Type v))) ↦
                (Sheafify.isLocallyGerm F).toPrelocalPredicate (T := fun (x : (↑X : Type v)) ↦ F.stalk x).pred (T :=
                  fun (x : (↑X : Type v)) ↦ F.stalk x) f)
                (fun (x : ↥(unop U)) ↦
                  (ConcreteCategory.hom (FC := TypeCat.Fun) (F.germ (unop U) (↑x : (↑X : Type v)) ⋯) :
                      (a : (fun (X : Type v) ↦ X) (F.obj (op (unop U)))) →
                        (fun (X : Type v) ↦ X) (F.stalk (↑x : (↑X : Type v))))
                    f)
                ⋯) ≫
            F.sheafify.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v))).map f))
        x
⊢ (F.map f ≫
      ↾fun (f : F.obj U') ↦
        Subtype.mk (p := fun (f : (x : ↥(unop U')) → (fun (x : (↑X : Type v)) ↦ F.stalk x) (↑x : (↑X : Type v))) ↦
          (Sheafify.isLocallyGerm F).toPrelocalPredicate (T := fun (x : (↑X : Type v)) ↦ F.stalk x).pred (T :=
            fun (x : (↑X : Type v)) ↦ F.stalk x) f)
          (fun (x : ↥(unop U')) ↦
            (ConcreteCategory.hom (FC := TypeCat.Fun) (F.germ (unop U') (↑x : (↑X : Type v)) ⋯) :
                (a : (fun (X : Type v) ↦ X) (F.obj (op (unop U')))) →
                  (fun (X : Type v) ↦ X) (F.stalk (↑x : (↑X : Type v))))
              f)
          ⋯) =
    (↾fun (f : F.obj U) ↦
        Subtype.mk (p := fun (f : (x : ↥(unop U)) → (fun (x : (↑X : Type v)) ↦ F.stalk x) (↑x : (↑X : Type v))) ↦
          (Sheafify.isLocallyGerm F).toPrelocalPredicate (T := fun (x : (↑X : Type v)) ↦ F.stalk x).pred (T :=
            fun (x : (↑X : Type v)) ↦ F.stalk x) f)
          (fun (x : ↥(unop U)) ↦
            (ConcreteCategory.hom (FC := TypeCat.Fun) (F.germ (unop U) (↑x : (↑X : Type v)) ⋯) :
                (a : (fun (X : Type v) ↦ X) (F.obj (op (unop U)))) →
                  (fun (X : Type v) ↦ X) (F.stalk (↑x : (↑X : Type v))))
              f)
          ⋯) ≫
      F.sheafify.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v))).map f

Tactic:
ext x
-- Module: Mathlib.Topology.Sheaves.Sheafify
Goal:
X : TopCat
F : Presheaf (Type v) X
U U' : (Opens (↑X : Type v))ᵒᵖ
f : U ⟶ U'
x : F.obj U
u : (↑X : Type v)
m : u ∈ unop U'
⊢ (↑(TypeCat.Fun.toFun
            (ConcreteCategory.hom (FC := TypeCat.Fun)
              (F.map f ≫
                ↾fun (f : F.obj U') ↦
                  Subtype.mk (p :=
                    fun (f : (x : ↥(unop U')) → (fun (x : (↑X : Type v)) ↦ F.stalk x) (↑x : (↑X : Type v))) ↦
                    (Sheafify.isLocallyGerm F).toPrelocalPredicate (T := fun (x : (↑X : Type v)) ↦ F.stalk x).pred (T :=
                      fun (x : (↑X : Type v)) ↦ F.stalk x) f)
                    (fun (x : ↥(unop U')) ↦
                      (ConcreteCategory.hom (FC := TypeCat.Fun) (F.germ (unop U') (↑x : (↑X : Type v)) ⋯) :
                          (a : (fun (X : Type v) ↦ X) (F.obj (op (unop U')))) →
                            (fun (X : Type v) ↦ X) (F.stalk (↑x : (↑X : Type v))))
                        f)
                    ⋯))
            x) :
        (x : ↥(unop U')) → (fun (x : (↑X : Type v)) ↦ F.stalk x) (↑x : (↑X : Type v)))
      (Subtype.mk (p := fun (x : (↑X : Type v)) ↦ x ∈ unop U') u m) =
    (↑(TypeCat.Fun.toFun
            (ConcreteCategory.hom (FC := TypeCat.Fun)
              ((↾fun (f : F.obj U) ↦
                  Subtype.mk (p :=
                    fun (f : (x : ↥(unop U)) → (fun (x : (↑X : Type v)) ↦ F.stalk x) (↑x : (↑X : Type v))) ↦
                    (Sheafify.isLocallyGerm F).toPrelocalPredicate (T := fun (x : (↑X : Type v)) ↦ F.stalk x).pred (T :=
                      fun (x : (↑X : Type v)) ↦ F.stalk x) f)
                    (fun (x : ↥(unop U)) ↦
                      (ConcreteCategory.hom (FC := TypeCat.Fun) (F.germ (unop U) (↑x : (↑X : Type v)) ⋯) :
                          (a : (fun (X : Type v) ↦ X) (F.obj (op (unop U)))) →
                            (fun (X : Type v) ↦ X) (F.stalk (↑x : (↑X : Type v))))
                        f)
                    ⋯) ≫
                F.sheafify.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v))).map f))
            x) :
        (x : ↥(unop U')) → (fun (x : (↑X : Type v)) ↦ F.stalk x) (↑x : (↑X : Type v)))
      (Subtype.mk (p := fun (x : (↑X : Type v)) ↦ x ∈ unop U') u m)

Tactic:
germ_res_apply F f.unop u m x

Premises used: TopCat.Presheaf.germ_res_apply, Set.Mem, Quiver.Hom.op, Quiver.Hom.unop
-- Module: Mathlib.Topology.Sheaves.Sheafify
Goal:
X : TopCat
F : Presheaf (Type v) X
U U' : (Opens (↑X : Type v))ᵒᵖ
f : U ⟶ U'
x : F.obj U
u : (↑X : Type v)
m : u ∈ unop U'
⊢ (↑(TypeCat.Fun.toFun
            (ConcreteCategory.hom (FC := TypeCat.Fun)
              (F.map f ≫
                ↾fun (f : F.obj U') ↦
                  Subtype.mk (p :=
                    fun (f : (x : ↥(unop U')) → (fun (x : (↑X : Type v)) ↦ F.stalk x) (↑x : (↑X : Type v))) ↦
                    (Sheafify.isLocallyGerm F).toPrelocalPredicate (T := fun (x : (↑X : Type v)) ↦ F.stalk x).pred (T :=
                      fun (x : (↑X : Type v)) ↦ F.stalk x) f)
                    (fun (x : ↥(unop U')) ↦
                      (ConcreteCategory.hom (FC := TypeCat.Fun) (F.germ (unop U') (↑x : (↑X : Type v)) ⋯) :
                          (a : (fun (X : Type v) ↦ X) (F.obj (op (unop U')))) →
                            (fun (X : Type v) ↦ X) (F.stalk (↑x : (↑X : Type v))))
                        f)
                    ⋯))
            x) :
        (x : ↥(unop U')) → (fun (x : (↑X : Type v)) ↦ F.stalk x) (↑x : (↑X : Type v)))
      (Subtype.mk (p := fun (x : (↑X : Type v)) ↦ x ∈ unop U') u m) =
    (↑(TypeCat.Fun.toFun
            (ConcreteCategory.hom (FC := TypeCat.Fun)
              ((↾fun (f : F.obj U) ↦
                  Subtype.mk (p :=
                    fun (f : (x : ↥(unop U)) → (fun (x : (↑X : Type v)) ↦ F.stalk x) (↑x : (↑X : Type v))) ↦
                    (Sheafify.isLocallyGerm F).toPrelocalPredicate (T := fun (x : (↑X : Type v)) ↦ F.stalk x).pred (T :=
                      fun (x : (↑X : Type v)) ↦ F.stalk x) f)
                    (fun (x : ↥(unop U)) ↦
                      (ConcreteCategory.hom (FC := TypeCat.Fun) (F.germ (unop U) (↑x : (↑X : Type v)) ⋯) :
                          (a : (fun (X : Type v) ↦ X) (F.obj (op (unop U)))) →
                            (fun (X : Type v) ↦ X) (F.stalk (↑x : (↑X : Type v))))
                        f)
                    ⋯) ≫
                F.sheafify.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type v))).map f))
            x) :
        (x : ↥(unop U')) → (fun (x : (↑X : Type v)) ↦ F.stalk x) (↑x : (↑X : Type v)))
      (Subtype.mk (p := fun (x : (↑X : Type v)) ↦ x ∈ unop U') u m)

Tactic:
exact germ_res_apply F f.unop u m x

Premises used: TopCat.Presheaf.germ_res_apply, Quiver.Hom.unop
-- Module: Mathlib.Topology.Sheaves.Sheafify
Goal:
X : TopCat
F : Presheaf (Type v) X
x : (↑X : Type v)
w :
  ∀ (t : F.stalk x),
    ∃ (U : OpenNhds x) (f : (y : ↥(↑U : Opens (↑X : Type v))) → F.stalk (↑y : (↑X : Type v))) (_ :
      (Sheafify.isLocallyGerm F).toPrelocalPredicate (T := fun (x : (↑X : Type v)) ↦ F.stalk x).pred (T :=
        fun (x : (↑X : Type v)) ↦ F.stalk x) f),
      f (Subtype.mk (p := fun (x_2 : (↑X : Type v)) ↦ x_2 ∈ (↑U : Opens (↑X : Type v))) x ⋯) = t
⊢ Function.Surjective (α := (fun (X : Type v) ↦ X) (F.sheafify.presheaf.stalk x)) (β :=
    (fun (X : Type v) ↦ X) (F.stalk x))
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (F.stalkToFiber x)) :
      (a : (fun (X : Type v) ↦ X) (F.sheafify.presheaf.stalk x)) → (fun (X : Type v) ↦ X) (F.stalk x))

Tactic:
apply TopCat.stalkToFiber_surjective

Premises used: TopCat.stalkToFiber_surjective
-- Module: Mathlib.Topology.Sheaves.Sheafify
Goal:
X : TopCat
F : Presheaf (Type v) X
x : (↑X : Type v)
t : F.stalk x
w :
  ∀ (U : Opens (↑X : Type v)) (m : x ∈ U) (s : ToType (FC := TypeCat.Fun) (F.obj (op U))),
    ∃ (U_1 : OpenNhds x) (f : (y : ↥(↑U_1 : Opens (↑X : Type v))) → F.stalk (↑y : (↑X : Type v))) (_ :
      (Sheafify.isLocallyGerm F).toPrelocalPredicate (T := fun (x : (↑X : Type v)) ↦ F.stalk x).pred (T :=
        fun (x : (↑X : Type v)) ↦ F.stalk x) f),
      Eq.{v + 1} (α :=
        F.stalk
          (↑(Subtype.mk (p := fun (x_2 : (↑X : Type v)) ↦ x_2 ∈ (↑U_1 : Opens (↑X : Type v))) x ⋯) : (↑X : Type v)))
        (f (Subtype.mk (p := fun (x_2 : (↑X : Type v)) ↦ x_2 ∈ (↑U_1 : Opens (↑X : Type v))) x ⋯))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.germ U x m) : (a : F.obj (op U)) → F.stalk x) s)
⊢ ∃ (U : OpenNhds x) (f : (y : ↥(↑U : Opens (↑X : Type v))) → F.stalk (↑y : (↑X : Type v))) (_ :
    (Sheafify.isLocallyGerm F).toPrelocalPredicate (T := fun (x : (↑X : Type v)) ↦ F.stalk x).pred (T :=
      fun (x : (↑X : Type v)) ↦ F.stalk x) f),
    f (Subtype.mk (p := fun (x_2 : (↑X : Type v)) ↦ x_2 ∈ (↑U : Opens (↑X : Type v))) x ⋯) = t

Tactic:
obtain ⟨U, m, s, rfl⟩ := F.exists_germ_eq t

Premises used: TopCat.Presheaf.exists_germ_eq, rfl
-- Module: Mathlib.Topology.Sheaves.Sheafify
Goal:
X : TopCat
F : Presheaf (Type v) X
x : (↑X : Type v)
U : Opens (↑X : Type v)
m : x ∈ U
s : ToType (FC := TypeCat.Fun) (F.obj (op U))
h :
  ∃ (f :
    (y : ↥(↑(Subtype.mk (p := fun (U : Opens (↑X : Type v)) ↦ x ∈ U) U m) : Opens (↑X : Type v))) →
      F.stalk (↑y : (↑X : Type v)))
    (_ :
    (Sheafify.isLocallyGerm F).toPrelocalPredicate (T := fun (x : (↑X : Type v)) ↦ F.stalk x).pred (T :=
      fun (x : (↑X : Type v)) ↦ F.stalk x) f),
    Eq.{v + 1} (α :=
      F.stalk
        (↑(Subtype.mk (p := fun (x_2 : (↑X : Type v)) ↦
              x_2 ∈ (↑(Subtype.mk (p := fun (U : Opens (↑X : Type v)) ↦ x ∈ U) U m) : Opens (↑X : Type v))) x ⋯) :
          (↑X : Type v)))
      (f
        (Subtype.mk (p := fun (x_2 : (↑X : Type v)) ↦
          x_2 ∈ (↑(Subtype.mk (p := fun (U : Opens (↑X : Type v)) ↦ x ∈ U) U m) : Opens (↑X : Type v))) x ⋯))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.germ U x m) : (a : F.obj (op U)) → F.stalk x) s)
⊢ ∃ (U_1 : OpenNhds x) (f : (y : ↥(↑U_1 : Opens (↑X : Type v))) → F.stalk (↑y : (↑X : Type v))) (_ :
    (Sheafify.isLocallyGerm F).toPrelocalPredicate (T := fun (x : (↑X : Type v)) ↦ F.stalk x).pred (T :=
      fun (x : (↑X : Type v)) ↦ F.stalk x) f),
    Eq.{v + 1} (α :=
      F.stalk (↑(Subtype.mk (p := fun (x_2 : (↑X : Type v)) ↦ x_2 ∈ (↑U_1 : Opens (↑X : Type v))) x ⋯) : (↑X : Type v)))
      (f (Subtype.mk (p := fun (x_2 : (↑X : Type v)) ↦ x_2 ∈ (↑U_1 : Opens (↑X : Type v))) x ⋯))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.germ U x m) : (a : F.obj (op U)) → F.stalk x) s)

Tactic:
use ⟨U, m⟩
-- Module: Mathlib.Topology.Sheaves.Sheafify
Goal:
X : TopCat
F : Presheaf (Type v) X
x : (↑X : Type v)
U : Opens (↑X : Type v)
m : x ∈ U
s : ToType (FC := TypeCat.Fun) (F.obj (op U))
⊢ (y : ↥(↑(Subtype.mk (p := fun (U : Opens (↑X : Type v)) ↦ x ∈ U) U m) : Opens (↑X : Type v))) →
    F.stalk (↑y : (↑X : Type v))

Tactic:
exact fun y => F.germ _ _ y.2 s

Premises used: CategoryTheory.ConcreteCategory.hom, TopCat.Presheaf.germ, DFunLike.coe