awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Sheaves.CommRingCat
Goal:
X_1 : TopCat
R : TopCommRingCat
X : TopCommRingCat
x : TopCatᵒᵖ
x_1 :
  (↑(Functor.obj
        { obj := fun (X_2 : TopCatᵒᵖ) ↦ continuousFunctions X_2 X,
          map := fun {x x_2 : TopCatᵒᵖ} (f : x ⟶ x_2) ↦ continuousFunctions.pullback f X, map_id := ⋯, map_comp := ⋯ }
        x) :
    Type u)
⊢ Eq (α :=
    (↑(Functor.obj
          { obj := fun (X_2 : TopCatᵒᵖ) ↦ continuousFunctions X_2 X,
            map := fun {x x_2 : TopCatᵒᵖ} (f : x ⟶ x_2) ↦ continuousFunctions.pullback f X, map_id := ⋯, map_comp := ⋯ }
          x) :
      Type u))
    ((CommRingCat.Hom.hom
            (NatTrans.app { app := fun (X_2 : TopCatᵒᵖ) ↦ continuousFunctions.map X_2 (𝟙 X), naturality := ⋯ } x) :
          (a :
              (↑({ obj := fun (X_2 : TopCatᵒᵖ) ↦ continuousFunctions X_2 X,
                        map := fun {x x_2 : TopCatᵒᵖ} (f : x ⟶ x_2) ↦ continuousFunctions.pullback f X, map_id := ⋯,
                        map_comp := ⋯ }.obj
                    x) :
                Type u)) →
            (↑({ obj := fun (X_2 : TopCatᵒᵖ) ↦ continuousFunctions X_2 X,
                      map := fun {x x_2 : TopCatᵒᵖ} (f : x ⟶ x_2) ↦ continuousFunctions.pullback f X, map_id := ⋯,
                      map_comp := ⋯ }.obj
                  x) :
              Type u))
        x_1 :
      (↑(Functor.obj
            { obj := fun (X_2 : TopCatᵒᵖ) ↦ continuousFunctions X_2 X,
              map := fun {x x_2 : TopCatᵒᵖ} (f : x ⟶ x_2) ↦ continuousFunctions.pullback f X, map_id := ⋯,
              map_comp := ⋯ }
            x) :
        Type u))
    ((CommRingCat.Hom.hom
            (NatTrans.app
              (𝟙
                { obj := fun (X_2 : TopCatᵒᵖ) ↦ continuousFunctions X_2 X,
                  map := fun {x x_2 : TopCatᵒᵖ} (f : x ⟶ x_2) ↦ continuousFunctions.pullback f X, map_id := ⋯,
                  map_comp := ⋯ })
              x) :
          (a :
              (↑({ obj := fun (X_2 : TopCatᵒᵖ) ↦ continuousFunctions X_2 X,
                        map := fun {x x_2 : TopCatᵒᵖ} (f : x ⟶ x_2) ↦ continuousFunctions.pullback f X, map_id := ⋯,
                        map_comp := ⋯ }.obj
                    x) :
                Type u)) →
            (↑({ obj := fun (X_2 : TopCatᵒᵖ) ↦ continuousFunctions X_2 X,
                      map := fun {x x_2 : TopCatᵒᵖ} (f : x ⟶ x_2) ↦ continuousFunctions.pullback f X, map_id := ⋯,
                      map_comp := ⋯ }.obj
                  x) :
              Type u))
        x_1 :
      (↑(Functor.obj
            { obj := fun (X_2 : TopCatᵒᵖ) ↦ continuousFunctions X_2 X,
              map := fun {x x_2 : TopCatᵒᵖ} (f : x ⟶ x_2) ↦ continuousFunctions.pullback f X, map_id := ⋯,
              map_comp := ⋯ }
            x) :
        Type u))

Tactic:
rfl
-- Module: Mathlib.Topology.Sheaves.CommRingCat
Goal:
X : TopCat
F : Presheaf CommRingCat X
U : Opens (↑X : Type v)
x : ↥U
⊢ Eq (α := (↑(F.obj (op U)) : Type v) →+* (↑(F.stalk (↑x : (↑X : Type v))) : Type v))
    (algebraMap (↑(F.obj (op U)) : Type v) (↑(F.stalk (↑x : (↑X : Type v))) : Type v))
    (CommRingCat.Hom.hom (F.germ U (↑x : (↑X : Type v)) ⋯))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Sheaves.CommRingCat
Goal:
X : TopCat
F : Sheaf CommRingCat X
U V : Opens (↑X : Type w)
x :
  (↑(F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).obj (op (U ⊔ V))) :
    Type u_1)
⊢ Eq (α :=
    (↑(F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).obj (op U)) : Type u_1))
    ((↑((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
                  CommRingCat.carrier) (F.objSupIsoProdEqLocus U V).hom :
                (a : (↑(F.obj.obj (op (U ⊔ V))) : Type u_1)) →
                  (↑(CommRingCat.of
                        ↥(((CommRingCat.Hom.hom (F.obj.map (homOfLE ⋯).op)).comp
                                (RingHom.fst (↑(F.obj.obj (op U)) : Type u_1) (↑(F.obj.obj (op V)) : Type u_1))).eqLocus
                            ((CommRingCat.Hom.hom (F.obj.map (homOfLE ⋯).op)).comp
                              (RingHom.snd (↑(F.obj.obj (op U)) : Type u_1) (↑(F.obj.obj (op V)) : Type u_1))))) :
                    Type u_1))
              x) :
          (↑(F.obj.obj (op U)) : Type u_1) × (↑(F.obj.obj (op V)) : Type u_1)).1 :
      (↑(F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).obj (op U)) :
        Type u_1))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (X :=
            F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).obj (op (U ⊔ V)))
            (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).map
              (Quiver.Hom.op (homOfLE ⋯))) :
          (a : (↑(F.obj.obj (op (U ⊔ V))) : Type u_1)) → (↑(F.obj.obj (op U)) : Type u_1))
        x :
      (↑(F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).obj (op U)) :
        Type u_1))

Tactic:
ConcreteCategory.congr_hom
    ((F.isLimitPullbackCone U V).conePointUniqueUpToIso_hom_comp
      (CommRingCat.pullbackConeIsLimit _ _) WalkingCospan.left)
    x

Premises used: CommRingCat.pullbackConeIsLimit, CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso_hom_comp, TopCat.Sheaf.isLimitPullbackCone, CategoryTheory.ConcreteCategory.congr_hom, CategoryTheory.Limits.WalkingCospan.left
-- Module: Mathlib.Topology.Sheaves.CommRingCat
Goal:
X : TopCat
F : Sheaf CommRingCat X
U V : Opens (↑X : Type w)
x :
  (↑(F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).obj (op (U ⊔ V))) :
    Type u_1)
⊢ Eq (α :=
    (↑(F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).obj (op V)) : Type u_1))
    ((↑((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
                  CommRingCat.carrier) (F.objSupIsoProdEqLocus U V).hom :
                (a : (↑(F.obj.obj (op (U ⊔ V))) : Type u_1)) →
                  (↑(CommRingCat.of
                        ↥(((CommRingCat.Hom.hom (F.obj.map (homOfLE ⋯).op)).comp
                                (RingHom.fst (↑(F.obj.obj (op U)) : Type u_1) (↑(F.obj.obj (op V)) : Type u_1))).eqLocus
                            ((CommRingCat.Hom.hom (F.obj.map (homOfLE ⋯).op)).comp
                              (RingHom.snd (↑(F.obj.obj (op U)) : Type u_1) (↑(F.obj.obj (op V)) : Type u_1))))) :
                    Type u_1))
              x) :
          (↑(F.obj.obj (op U)) : Type u_1) × (↑(F.obj.obj (op V)) : Type u_1)).2 :
      (↑(F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).obj (op V)) :
        Type u_1))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (X :=
            F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).obj (op (U ⊔ V)))
            (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).map
              (Quiver.Hom.op (homOfLE ⋯))) :
          (a : (↑(F.obj.obj (op (U ⊔ V))) : Type u_1)) → (↑(F.obj.obj (op V)) : Type u_1))
        x :
      (↑(F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).obj (op V)) :
        Type u_1))

Tactic:
ConcreteCategory.congr_hom
    ((F.isLimitPullbackCone U V).conePointUniqueUpToIso_hom_comp
      (CommRingCat.pullbackConeIsLimit _ _) WalkingCospan.right)
    x

Premises used: CommRingCat.pullbackConeIsLimit, CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso_hom_comp, CategoryTheory.Limits.WalkingCospan.right, TopCat.Sheaf.isLimitPullbackCone, CategoryTheory.ConcreteCategory.congr_hom
-- Module: Mathlib.Topology.Sheaves.CommRingCat
Goal:
X : TopCat
F : Sheaf CommRingCat X
U V : Opens (↑X : Type w)
x :
  (↑(CommRingCat.of
        ↥(RingHom.eqLocus
            (RingHom.comp
              (CommRingCat.Hom.hom
                (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).map
                  (Quiver.Hom.op (homOfLE ⋯))))
              (RingHom.fst
                (↑(F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).obj (op U)) :
                  Type u_1)
                (↑(F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).obj (op V)) :
                  Type u_1)))
            (RingHom.comp
              (CommRingCat.Hom.hom
                (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).map
                  (Quiver.Hom.op (homOfLE ⋯))))
              (RingHom.snd
                (↑(F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).obj (op U)) :
                  Type u_1)
                (↑(F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).obj (op V)) :
                  Type u_1))))) :
    Type u_1)
⊢ (ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
          CommRingCat.carrier) (X :=
          F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).obj (op (U ⊔ V)))
          (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).map
            (Quiver.Hom.op (homOfLE ⋯))) :
        (a : (↑(F.obj.obj (op (U ⊔ V))) : Type u_1)) → (↑(F.obj.obj (op U)) : Type u_1))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
              CommRingCat.carrier) (F.objSupIsoProdEqLocus U V).inv :
            (a :
                (↑(CommRingCat.of
                      ↥(((CommRingCat.Hom.hom (F.obj.map (homOfLE ⋯).op)).comp
                              (RingHom.fst (↑(F.obj.obj (op U)) : Type u_1) (↑(F.obj.obj (op V)) : Type u_1))).eqLocus
                          ((CommRingCat.Hom.hom (F.obj.map (homOfLE ⋯).op)).comp
                            (RingHom.snd (↑(F.obj.obj (op U)) : Type u_1) (↑(F.obj.obj (op V)) : Type u_1))))) :
                  Type u_1)) →
              (↑(F.obj.obj (op (U ⊔ V))) : Type u_1))
          x :
        (↑(F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).obj (op (U ⊔ V))) :
          Type u_1)) =
    (↑x : (↑(F.obj.obj (op U)) : Type u_1) × (↑(F.obj.obj (op V)) : Type u_1)).1

Tactic:
ConcreteCategory.congr_hom
    ((F.isLimitPullbackCone U V).conePointUniqueUpToIso_inv_comp
      (CommRingCat.pullbackConeIsLimit _ _) WalkingCospan.left)
    x

Premises used: CommRingCat.pullbackConeIsLimit, Set.Mem, setOf, CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso_inv_comp, TopCat.Sheaf.isLimitPullbackCone, CategoryTheory.ConcreteCategory.congr_hom, CategoryTheory.Limits.WalkingCospan.left
-- Module: Mathlib.Topology.Sheaves.CommRingCat
Goal:
X : TopCat
F : Sheaf CommRingCat X
U V : Opens (↑X : Type w)
x :
  (↑(CommRingCat.of
        ↥(RingHom.eqLocus
            (RingHom.comp
              (CommRingCat.Hom.hom
                (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).map
                  (Quiver.Hom.op (homOfLE ⋯))))
              (RingHom.fst
                (↑(F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).obj (op U)) :
                  Type u_1)
                (↑(F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).obj (op V)) :
                  Type u_1)))
            (RingHom.comp
              (CommRingCat.Hom.hom
                (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).map
                  (Quiver.Hom.op (homOfLE ⋯))))
              (RingHom.snd
                (↑(F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).obj (op U)) :
                  Type u_1)
                (↑(F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).obj (op V)) :
                  Type u_1))))) :
    Type u_1)
⊢ (ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
          CommRingCat.carrier) (X :=
          F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).obj (op (U ⊔ V)))
          (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).map
            (Quiver.Hom.op (homOfLE ⋯))) :
        (a : (↑(F.obj.obj (op (U ⊔ V))) : Type u_1)) → (↑(F.obj.obj (op V)) : Type u_1))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
              CommRingCat.carrier) (F.objSupIsoProdEqLocus U V).inv :
            (a :
                (↑(CommRingCat.of
                      ↥(((CommRingCat.Hom.hom (F.obj.map (homOfLE ⋯).op)).comp
                              (RingHom.fst (↑(F.obj.obj (op U)) : Type u_1) (↑(F.obj.obj (op V)) : Type u_1))).eqLocus
                          ((CommRingCat.Hom.hom (F.obj.map (homOfLE ⋯).op)).comp
                            (RingHom.snd (↑(F.obj.obj (op U)) : Type u_1) (↑(F.obj.obj (op V)) : Type u_1))))) :
                  Type u_1)) →
              (↑(F.obj.obj (op (U ⊔ V))) : Type u_1))
          x :
        (↑(F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).obj (op (U ⊔ V))) :
          Type u_1)) =
    (↑x : (↑(F.obj.obj (op U)) : Type u_1) × (↑(F.obj.obj (op V)) : Type u_1)).2

Tactic:
ConcreteCategory.congr_hom
    ((F.isLimitPullbackCone U V).conePointUniqueUpToIso_inv_comp
      (CommRingCat.pullbackConeIsLimit _ _) WalkingCospan.right)
    x

Premises used: CommRingCat.pullbackConeIsLimit, Set.Mem, CategoryTheory.Limits.WalkingCospan.right, setOf, CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso_inv_comp, TopCat.Sheaf.isLimitPullbackCone, CategoryTheory.ConcreteCategory.congr_hom
-- Module: Mathlib.Topology.Sheaves.EtaleSpace
Goal:
X : TopCat
C : Type u
inst : Category.{v, u} C
CC : C → Type v
FC : C → C → Type w
inst_1 : (X Y : C) → FunLike.{w + 1, v + 1, v + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory C FC (CC := CC)
inst_3 : Limits.HasColimits.{v, u} C
F : Presheaf C X
g : F.EtaleSpace (CC := CC) (FC := FC)
U : Opens (↑X : Type v)
h : g.base (CC := CC) (FC := FC) ∈ U
s : ToType (FC := FC) (CC := CC) (F.obj (op U))
hs :
  (ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ U (g.base (CC := CC) (FC := FC)) h) :
        (a : CC (F.obj (op U))) → CC (F.stalk g.base))
      s =
    g.germ (CC := CC) (FC := FC)
simp :
  Membership.mem (γ := Filter (F.EtaleSpace (CC := CC) (FC := FC)))
    (⨅ (s : Set (F.EtaleSpace (CC := CC) (FC := FC))),
      ⨅ (_ : g ∈ s),
        ⨅ (i : Opens (↑X : Type v)),
          ⨅ (i_1 : ToType (FC := FC) (CC := CC) (F.obj (op i))),
            ⨅ (_ :
              {g : F.EtaleSpace (CC := CC) (FC := FC) |
                  ∃ (h : g.base (CC := CC) (FC := FC) ∈ i),
                    g.germ (CC := CC) (FC := FC) =
                      (ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ i (g.base (CC := CC) (FC := FC)) h) :
                          (a : CC (F.obj (op i))) → CC (F.stalk g.base))
                        i_1} =
                s),
              𝓟 s)
    {x : F.EtaleSpace (CC := CC) (FC := FC) |
      ∃ (hgU : x.base (CC := CC) (FC := FC) ∈ U),
        x.germ (CC := CC) (FC := FC) =
          (ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ U (x.base (CC := CC) (FC := FC)) hgU) :
              (a : CC (F.obj (op U))) → CC (F.stalk x.base))
            s}
⊢ ∀ᶠ (g' : F.EtaleSpace (CC := CC) (FC := FC)) in 𝓝 g,
    ∃ (hgU : g'.base (CC := CC) (FC := FC) ∈ U),
      g'.germ (CC := CC) (FC := FC) =
        (ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ U (g'.base (CC := CC) (FC := FC)) hgU) :
            (a : CC (F.obj (op U))) → CC (F.stalk g'.base))
          s

Tactic:
simp only [nhds_generateFrom, Filter.Eventually, mem_setOf_eq, iInf_and, iInf_exists]

Premises used: Filter.Eventually, TopologicalSpace.nhds_generateFrom, Set.mem_setOf_eq, iInf_and, iInf_exists
-- Module: Mathlib.Topology.Sheaves.EtaleSpace
Goal:
X : TopCat
C : Type u
inst : Category.{v, u} C
CC : C → Type v
FC : C → C → Type w
inst_1 : (X Y : C) → FunLike.{w + 1, v + 1, v + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory C FC (CC := CC)
inst_3 : Limits.HasColimits.{v, u} C
F : Presheaf C X
g : F.EtaleSpace (CC := CC) (FC := FC)
U : Opens (↑X : Type v)
h : g.base (CC := CC) (FC := FC) ∈ U
s : ToType (FC := FC) (CC := CC) (F.obj (op U))
hs :
  (ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ U (g.base (CC := CC) (FC := FC)) h) :
        (a : CC (F.obj (op U))) → CC (F.stalk g.base))
      s =
    g.germ (CC := CC) (FC := FC)
⊢ Membership.mem (γ := Filter (F.EtaleSpace (CC := CC) (FC := FC)))
    (⨅ (s : Set (F.EtaleSpace (CC := CC) (FC := FC))),
      ⨅ (_ : g ∈ s),
        ⨅ (i : Opens (↑X : Type v)),
          ⨅ (i_1 : ToType (FC := FC) (CC := CC) (F.obj (op i))),
            ⨅ (_ :
              {g : F.EtaleSpace (CC := CC) (FC := FC) |
                  ∃ (h : g.base (CC := CC) (FC := FC) ∈ i),
                    g.germ (CC := CC) (FC := FC) =
                      (ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ i (g.base (CC := CC) (FC := FC)) h) :
                          (a : CC (F.obj (op i))) → CC (F.stalk g.base))
                        i_1} =
                s),
              𝓟 s)
    {x : F.EtaleSpace (CC := CC) (FC := FC) |
      ∃ (hgU : x.base (CC := CC) (FC := FC) ∈ U),
        x.germ (CC := CC) (FC := FC) =
          (ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ U (x.base (CC := CC) (FC := FC)) hgU) :
              (a : CC (F.obj (op U))) → CC (F.stalk x.base))
            s}

Tactic:
mem_iInf_of_mem _ <| mem_iInf_of_mem ?_ <| mem_iInf_of_mem U <| mem_iInf_of_mem s <|
    mem_iInf_of_mem rfl <| mem_principal_self _

Premises used: Filter.mem_principal_self, Filter.mem_iInf_of_mem, rfl
-- Module: Mathlib.Topology.Sheaves.EtaleSpace
Goal:
X : TopCat
C : Type u
inst : Category.{v, u} C
CC : C → Type v
FC : C → C → Type w
inst_1 : (X Y : C) → FunLike.{w + 1, v + 1, v + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory C FC (CC := CC)
inst_3 : Limits.HasColimits.{v, u} C
F : Presheaf C X
g : F.EtaleSpace (CC := CC) (FC := FC)
U : Opens (↑X : Type v)
h : g.base (CC := CC) (FC := FC) ∈ U
s : ToType (FC := FC) (CC := CC) (F.obj (op U))
hs :
  (ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ U (g.base (CC := CC) (FC := FC)) h) :
        (a : CC (F.obj (op U))) → CC (F.stalk g.base))
      s =
    g.germ (CC := CC) (FC := FC)
refine :
  Membership.mem (γ := Set (F.EtaleSpace (CC := CC) (FC := FC)))
    {g : F.EtaleSpace (CC := CC) (FC := FC) |
      ∃ (h : g.base (CC := CC) (FC := FC) ∈ U),
        g.germ (CC := CC) (FC := FC) =
          (ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ U (g.base (CC := CC) (FC := FC)) h) :
              (a : CC (F.obj (op U))) → CC (F.stalk g.base))
            s}
    g
⊢ Membership.mem (γ := Filter (F.EtaleSpace (CC := CC) (FC := FC)))
    (⨅ (s : Set (F.EtaleSpace (CC := CC) (FC := FC))),
      ⨅ (_ : g ∈ s),
        ⨅ (i : Opens (↑X : Type v)),
          ⨅ (i_1 : ToType (FC := FC) (CC := CC) (F.obj (op i))),
            ⨅ (_ :
              {g : F.EtaleSpace (CC := CC) (FC := FC) |
                  ∃ (h : g.base (CC := CC) (FC := FC) ∈ i),
                    g.germ (CC := CC) (FC := FC) =
                      (ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ i (g.base (CC := CC) (FC := FC)) h) :
                          (a : CC (F.obj (op i))) → CC (F.stalk g.base))
                        i_1} =
                s),
              𝓟 s)
    {x : F.EtaleSpace (CC := CC) (FC := FC) |
      ∃ (hgU : x.base (CC := CC) (FC := FC) ∈ U),
        x.germ (CC := CC) (FC := FC) =
          (ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ U (x.base (CC := CC) (FC := FC)) hgU) :
              (a : CC (F.obj (op U))) → CC (F.stalk x.base))
            s}

Tactic:
refine mem_iInf_of_mem _ <| mem_iInf_of_mem ?_ <| mem_iInf_of_mem U <| mem_iInf_of_mem s <|
    mem_iInf_of_mem rfl <| mem_principal_self _

Premises used: Filter.mem_principal_self, Filter.mem_iInf_of_mem, rfl
-- Module: Mathlib.Topology.Sheaves.EtaleSpace
Goal:
X : TopCat
C : Type u
inst : Category.{v, u} C
CC : C → Type v
FC : C → C → Type w
inst_1 : (X Y : C) → FunLike.{w + 1, v + 1, v + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory C FC (CC := CC)
inst_3 : Limits.HasColimits.{v, u} C
F : Presheaf C X
g : F.EtaleSpace (CC := CC) (FC := FC)
U : Opens (↑X : Type v)
h : g.base (CC := CC) (FC := FC) ∈ U
s : ToType (FC := FC) (CC := CC) (F.obj (op U))
hs :
  (ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ U (g.base (CC := CC) (FC := FC)) h) :
        (a : CC (F.obj (op U))) → CC (F.stalk g.base))
      s =
    g.germ (CC := CC) (FC := FC)
⊢ Membership.mem (γ := Set (F.EtaleSpace (CC := CC) (FC := FC)))
    {g : F.EtaleSpace (CC := CC) (FC := FC) |
      ∃ (h : g.base (CC := CC) (FC := FC) ∈ U),
        g.germ (CC := CC) (FC := FC) =
          (ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ U (g.base (CC := CC) (FC := FC)) h) :
              (a : CC (F.obj (op U))) → CC (F.stalk g.base))
            s}
    g

Tactic:
simp [*]
-- Module: Mathlib.Topology.Sheaves.EtaleSpace
Goal:
X : TopCat
C : Type u
inst : Category.{v, u} C
CC : C → Type v
FC : C → C → Type w
inst_1 : (X Y : C) → FunLike.{w + 1, v + 1, v + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory C FC (CC := CC)
inst_3 : Limits.HasColimits.{v, u} C
F : Presheaf C X
inst_4 : Limits.PreservesFilteredColimits (forget C (FC := FC) (CC := CC))
rw : ∀ (x : F.EtaleSpace (CC := CC) (FC := FC)), ContinuousAt (base (CC := CC) (FC := FC)) x
⊢ Continuous (X := F.EtaleSpace (CC := CC) (FC := FC)) (base (CC := CC) (FC := FC))

Tactic:
rw [continuous_iff_continuousAt]

Premises used: continuous_iff_continuousAt
-- Module: Mathlib.Topology.Sheaves.EtaleSpace
Goal:
X : TopCat
C : Type u
inst : Category.{v, u} C
CC : C → Type v
FC : C → C → Type w
inst_1 : (X Y : C) → FunLike.{w + 1, v + 1, v + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory C FC (CC := CC)
inst_3 : Limits.HasColimits.{v, u} C
F : Presheaf C X
inst_4 : Limits.PreservesFilteredColimits (forget C (FC := FC) (CC := CC))
x : F.EtaleSpace (CC := CC) (FC := FC)
rw :
  ∀ (i : Set (↑X : Type v)),
    x.base (CC := CC) (FC := FC) ∈ i ∧ IsOpen i →
      ∀ᶠ (x : F.EtaleSpace (CC := CC) (FC := FC)) in 𝓝 x, x.base (CC := CC) (FC := FC) ∈ i
⊢ ContinuousAt (base (CC := CC) (FC := FC)) x

Tactic:
rw [ContinuousAt, (nhds_basis_opens _).tendsto_right_iff]

Premises used: ContinuousAt, Filter.HasBasis.tendsto_right_iff, nhds_basis_opens
-- Module: Mathlib.Topology.Sheaves.EtaleSpace
Goal:
X : TopCat
C : Type u
inst : Category.{v, u} C
CC : C → Type v
FC : C → C → Type w
inst_1 : (X Y : C) → FunLike.{w + 1, v + 1, v + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory C FC (CC := CC)
inst_3 : Limits.HasColimits.{v, u} C
F : Presheaf C X
inst_4 : Limits.PreservesFilteredColimits (forget C (FC := FC) (CC := CC))
x : F.EtaleSpace (CC := CC) (FC := FC)
U : Set (↑X : Type v)
hxU : x.base (CC := CC) (FC := FC) ∈ U
hUo : IsOpen U
⊢ IsOpen U

Tactic:
hUo
-- Module: Mathlib.Topology.Sheaves.EtaleSpace
Goal:
X : TopCat
C : Type u
inst : Category.{v, u} C
CC : C → Type v
FC : C → C → Type w
inst_1 : (X Y : C) → FunLike.{w + 1, v + 1, v + 1} (FC X Y) (CC X) (CC Y)
inst_2 : ConcreteCategory C FC (CC := CC)
inst_3 : Limits.HasColimits.{v, u} C
F : Presheaf C X
inst_4 : Limits.PreservesFilteredColimits (forget C (FC := FC) (CC := CC))
x : F.EtaleSpace (CC := CC) (FC := FC)
U : Set (↑X : Type v)
hxU : x.base (CC := CC) (FC := FC) ∈ U
hUo : IsOpen U
lift :
  ∀ (U : Opens (↑X : Type v)) (hxU : x.base (CC := CC) (FC := FC) ∈ (↑U : Set (↑X : Type v))),
    ∀ᶠ (x : F.EtaleSpace (CC := CC) (FC := FC)) in 𝓝 x, x.base (CC := CC) (FC := FC) ∈ (↑U : Set (↑X : Type v))
⊢ ∀ᶠ (x : F.EtaleSpace (CC := CC) (FC := FC)) in 𝓝 x, x.base (CC := CC) (FC := FC) ∈ U

Tactic:
lift U to Opens X using hUo

Premises used: TopologicalSpace.Opens, TopCat.carrier