awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Category.TopCat.GrothendieckTopology
Goal:
X Y : TopCat
𝒰 : precoverage.ZeroHypercover Y
heq :
  ∀ (i : 𝒰.I₀) (y : (↑(𝒰.X i) : Type u_1)),
    Eq (α := (↑Y : Type u_1))
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC := carrier)
              (𝒰.f i) :
            (a : (↑(𝒰.X i) : Type u_1)) → (↑Y : Type u_1))
          y :
        (↑Y : Type u_1))
      ((↑(Subtype.mk (p := fun (x : (↑Y : Type u_1)) ↦
              Membership.mem (γ := Set (↑Y : Type u_1))
                (Set.range (ι := (↑(𝒰.X i) : Type u_1))
                  (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
                        carrier) (𝒰.f i)) :
                    (a : (↑(𝒰.X i) : Type u_1)) → (↑Y : Type u_1)))
                x)
              ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
                    carrier) (𝒰.f i) :
                  (a : (↑(𝒰.X i) : Type u_1)) → (↑Y : Type u_1))
                y)
              ⋯) :
          (↑Y : Type u_1)) :
        (↑Y : Type u_1))
x_1 : (i : 𝒰.I₀) → Functor.obj (Functor.obj yoneda X) (Opposite.op (𝒰.X i))
hx : Presieve.Arrows.Compatible (Functor.obj yoneda X) 𝒰.f x_1
x : (↑Y : Type u_1)
refine_1 :
  ∀ (i : 𝒰.I₀)
    (hi :
      Membership.mem (γ := Set (↑Y : Type u_1))
        (Set.range (ι := (↑(𝒰.X i) : Type u_1))
          (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC := carrier)
                (𝒰.f i)) :
            (a : (↑(𝒰.X i) : Type u_1)) → (↑Y : Type u_1)))
        x),
    ∃ (i : 𝒰.I₀),
      (fun (i : 𝒰.I₀) ↦
            (Set.range (ι := (↑(𝒰.X i) : Type u_1))
                (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
                      carrier) (𝒰.f i)) :
                  (a : (↑(𝒰.X i) : Type u_1)) → (↑Y : Type u_1)) :
              Set (↑Y : Type u_1)))
          i ∈
        nhds x
⊢ ∃ (i : 𝒰.I₀),
    (fun (i : 𝒰.I₀) ↦
          (Set.range (ι := (↑(𝒰.X i) : Type u_1))
              (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
                    carrier) (𝒰.f i)) :
                (a : (↑(𝒰.X i) : Type u_1)) → (↑Y : Type u_1)) :
            Set (↑Y : Type u_1)))
        i ∈
      nhds x

Tactic:
obtain ⟨i, hi⟩ := exists_mem_zeroHypercover_range 𝒰 x

Premises used: TopCat.exists_mem_zeroHypercover_range
-- Module: Mathlib.Topology.Category.TopCat.GrothendieckTopology
Goal:
X Y : TopCat
𝒰 : precoverage.ZeroHypercover Y
heq :
  ∀ (i : 𝒰.I₀) (y : (↑(𝒰.X i) : Type u_1)),
    Eq (α := (↑Y : Type u_1))
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC := carrier)
              (𝒰.f i) :
            (a : (↑(𝒰.X i) : Type u_1)) → (↑Y : Type u_1))
          y :
        (↑Y : Type u_1))
      ((↑(Subtype.mk (p := fun (x : (↑Y : Type u_1)) ↦
              Membership.mem (γ := Set (↑Y : Type u_1))
                (Set.range (ι := (↑(𝒰.X i) : Type u_1))
                  (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
                        carrier) (𝒰.f i)) :
                    (a : (↑(𝒰.X i) : Type u_1)) → (↑Y : Type u_1)))
                x)
              ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
                    carrier) (𝒰.f i) :
                  (a : (↑(𝒰.X i) : Type u_1)) → (↑Y : Type u_1))
                y)
              ⋯) :
          (↑Y : Type u_1)) :
        (↑Y : Type u_1))
x_1 : (i : 𝒰.I₀) → Functor.obj (Functor.obj yoneda X) (Opposite.op (𝒰.X i))
hx : Presieve.Arrows.Compatible (Functor.obj yoneda X) 𝒰.f x_1
x : (↑Y : Type u_1)
i : 𝒰.I₀
hi :
  Membership.mem (γ := Set (↑Y : Type u_1))
    (Set.range (ι := (↑(𝒰.X i) : Type u_1))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC := carrier)
            (𝒰.f i)) :
        (a : (↑(𝒰.X i) : Type u_1)) → (↑Y : Type u_1)))
    x
⊢ ∃ (i : 𝒰.I₀),
    (fun (i : 𝒰.I₀) ↦
          (Set.range (ι := (↑(𝒰.X i) : Type u_1))
              (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
                    carrier) (𝒰.f i)) :
                (a : (↑(𝒰.X i) : Type u_1)) → (↑Y : Type u_1)) :
            Set (↑Y : Type u_1)))
        i ∈
      nhds x

Tactic:
⟨i, (isOpenEmbedding_f_zeroHypercover 𝒰 i).isOpen_range.mem_nhds hi⟩

Premises used: TopCat.isOpenEmbedding_f_zeroHypercover, Topology.IsOpenEmbedding.isOpen_range, IsOpen.mem_nhds, Exists.intro
-- Module: Mathlib.Topology.Category.TopCat.GrothendieckTopology
Goal:
X Y : TopCat
𝒰 : precoverage.ZeroHypercover Y
heq :
  ∀ (i : 𝒰.I₀) (y : (↑(𝒰.X i) : Type u_1)),
    Eq (α := (↑Y : Type u_1))
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC := carrier)
              (𝒰.f i) :
            (a : (↑(𝒰.X i) : Type u_1)) → (↑Y : Type u_1))
          y :
        (↑Y : Type u_1))
      ((↑(Subtype.mk (p := fun (x : (↑Y : Type u_1)) ↦
              Membership.mem (γ := Set (↑Y : Type u_1))
                (Set.range (ι := (↑(𝒰.X i) : Type u_1))
                  (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
                        carrier) (𝒰.f i)) :
                    (a : (↑(𝒰.X i) : Type u_1)) → (↑Y : Type u_1)))
                x)
              ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
                    carrier) (𝒰.f i) :
                  (a : (↑(𝒰.X i) : Type u_1)) → (↑Y : Type u_1))
                y)
              ⋯) :
          (↑Y : Type u_1)) :
        (↑Y : Type u_1))
x_1 : (i : 𝒰.I₀) → Functor.obj (Functor.obj yoneda X) (Opposite.op (𝒰.X i))
hx : Presieve.Arrows.Compatible (Functor.obj yoneda X) 𝒰.f x_1
x : (↑Y : Type u_1)
i : 𝒰.I₀
hi :
  Membership.mem (γ := Set (↑Y : Type u_1))
    (Set.range (ι := (↑(𝒰.X i) : Type u_1))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC := carrier)
            (𝒰.f i)) :
        (a : (↑(𝒰.X i) : Type u_1)) → (↑Y : Type u_1)))
    x
⊢ ∃ (i : 𝒰.I₀),
    (fun (i : 𝒰.I₀) ↦
          (Set.range (ι := (↑(𝒰.X i) : Type u_1))
              (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
                    carrier) (𝒰.f i)) :
                (a : (↑(𝒰.X i) : Type u_1)) → (↑Y : Type u_1)) :
            Set (↑Y : Type u_1)))
        i ∈
      nhds x

Tactic:
exact ⟨i, (isOpenEmbedding_f_zeroHypercover 𝒰 i).isOpen_range.mem_nhds hi⟩
-- Module: Mathlib.Topology.Category.TopCat.GrothendieckTopology
Goal:
X Y : TopCat
𝒰 : precoverage.ZeroHypercover Y
heq :
  ∀ (i : 𝒰.I₀) (y : (↑(𝒰.X i) : Type u_1)),
    Eq (α := (↑Y : Type u_1))
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC := carrier)
              (𝒰.f i) :
            (a : (↑(𝒰.X i) : Type u_1)) → (↑Y : Type u_1))
          y :
        (↑Y : Type u_1))
      ((↑(Subtype.mk (p := fun (x : (↑Y : Type u_1)) ↦
              Membership.mem (γ := Set (↑Y : Type u_1))
                (Set.range (ι := (↑(𝒰.X i) : Type u_1))
                  (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
                        carrier) (𝒰.f i)) :
                    (a : (↑(𝒰.X i) : Type u_1)) → (↑Y : Type u_1)))
                x)
              ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
                    carrier) (𝒰.f i) :
                  (a : (↑(𝒰.X i) : Type u_1)) → (↑Y : Type u_1))
                y)
              ⋯) :
          (↑Y : Type u_1)) :
        (↑Y : Type u_1))
x : (i : 𝒰.I₀) → Functor.obj (Functor.obj yoneda X) (Opposite.op (𝒰.X i))
hx : Presieve.Arrows.Compatible (Functor.obj yoneda X) 𝒰.f x
f : (fun (X : Type u_1) ↦ X) (Functor.obj (Functor.obj yoneda X) (Opposite.op Y))
hf :
  (fun (t : (fun (X : Type u_1) ↦ X) (Functor.obj (Functor.obj yoneda X) (Opposite.op Y))) ↦
      ∀ (i : 𝒰.I₀),
        (ConcreteCategory.hom (FC := TypeCat.Fun) (CategoryTheory.Functor.map (Functor.obj yoneda X) (𝒰.f i).op) :
              (a : (fun (X : Type u_1) ↦ X) ((yoneda.obj X).obj (Opposite.op Y))) →
                (fun (X : Type u_1) ↦ X) ((yoneda.obj X).obj (Opposite.op (𝒰.X i))))
            t =
          x i)
    f
i : 𝒰.I₀
y : (↑(𝒰.X i) : Type u_1)
⊢ Eq (α := (↑X : Type u_1))
    ((Hom.hom
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (CategoryTheory.Functor.map (Functor.obj yoneda X) (𝒰.f i).op) :
                (a : (fun (X : Type u_1) ↦ X) ((yoneda.obj X).obj (Opposite.op Y))) →
                  (fun (X : Type u_1) ↦ X) ((yoneda.obj X).obj (Opposite.op (𝒰.X i))))
              f) :
          (a : (↑(Opposite.unop (Opposite.op (𝒰.X i))) : Type u_1)) → (↑X : Type u_1))
        y :
      (↑X : Type u_1))
    ((Hom.hom (x i) : (a : (↑(Opposite.unop (Opposite.op (𝒰.X i))) : Type u_1)) → (↑X : Type u_1)) y : (↑X : Type u_1))

Tactic:
have := congr($(hf i).hom y)
-- Module: Mathlib.Topology.Category.TopCat.GrothendieckTopology
Goal:
⊢ precoverage ≤ Precoverage.comap uliftFunctor precoverage

Tactic:
Precoverage.le_of_zeroHypercover fun X E ↦ ?_

Premises used: CategoryTheory.Precoverage.le_of_zeroHypercover
-- Module: Mathlib.Topology.Category.TopCat.GrothendieckTopology
Goal:
refine :
  ∀ (X : TopCat.{u}) (E : precoverage.ZeroHypercover X),
    E.presieve₀ ∈ (Precoverage.comap uliftFunctor precoverage).coverings X
⊢ precoverage ≤ Precoverage.comap uliftFunctor precoverage

Tactic:
refine Precoverage.le_of_zeroHypercover fun X E ↦ ?_

Premises used: CategoryTheory.Precoverage.le_of_zeroHypercover
-- Module: Mathlib.Topology.Category.TopCat.GrothendieckTopology
Goal:
X : TopCat
E : precoverage.ZeroHypercover X
⊢ E.presieve₀ ∈ (Precoverage.comap uliftFunctor precoverage).coverings X

Tactic:
⟨?_, ?_⟩

Premises used: Set.Mem, setOf, Set.inter, And.intro
-- Module: Mathlib.Topology.Category.TopCat.GrothendieckTopology
Goal:
X : TopCat
E : precoverage.ZeroHypercover X
refine_1 :
  Membership.mem (γ := Set (Presieve (uliftFunctor.obj X)))
    (Precoverage.coverings
      (Precoverage.comap
        (forget TopCat (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max v u)), (↑Y : Type (max v u)))) (CC := carrier))
        Types.jointlySurjectivePrecoverage)
      (uliftFunctor.obj X))
    (Presieve.map uliftFunctor E.presieve₀)
refine_2 :
  Membership.mem (γ := Set (Presieve (uliftFunctor.obj X))) (isOpenEmbedding.precoverage.coverings (uliftFunctor.obj X))
    (Presieve.map uliftFunctor E.presieve₀)
⊢ E.presieve₀ ∈ (Precoverage.comap uliftFunctor precoverage).coverings X

Tactic:
refine ⟨?_, ?_⟩
-- Module: Mathlib.Topology.Category.TopCat.GrothendieckTopology
Goal:
X : TopCat
E : precoverage.ZeroHypercover X
refine_1 :
  ∀
    (x :
      ToType (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max v u)), (↑Y : Type (max v u)))) (CC := carrier)
        (uliftFunctor.obj X)),
    ∃ (i : E.I₀) (y :
      ToType (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max v u)), (↑Y : Type (max v u)))) (CC := carrier)
        (uliftFunctor.obj (E.X i))),
      (ConcreteCategory.hom (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max v u)), (↑Y : Type (max v u)))) (CC := carrier)
              (uliftFunctor.map (E.f i)) :
            (a : (↑(uliftFunctor.obj (E.X i)) : Type (max v u))) → (↑(uliftFunctor.obj X) : Type (max v u)))
          y =
        x
⊢ Membership.mem (γ := Set (Presieve (uliftFunctor.obj X)))
    (Precoverage.coverings
      (Precoverage.comap
        (forget TopCat (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max v u)), (↑Y : Type (max v u)))) (CC := carrier))
        Types.jointlySurjectivePrecoverage)
      (uliftFunctor.obj X))
    (Presieve.map uliftFunctor E.presieve₀)

Tactic:
simp only [Presieve.map_ofArrows, Precoverage.mem_comap_iff,
      Types.ofArrows_mem_jointlySurjectivePrecoverage_iff, ConcreteCategory.hom_ofHom,
      Set.mem_range, TypeCat.Fun.coe_mk]

Premises used: Set.mem_range, TypeCat.Fun.coe_mk, CategoryTheory.Presieve.map_ofArrows, CategoryTheory.ConcreteCategory.hom_ofHom, CategoryTheory.Types.ofArrows_mem_jointlySurjectivePrecoverage_iff, CategoryTheory.Precoverage.mem_comap_iff
-- Module: Mathlib.Topology.Category.TopCat.GrothendieckTopology
Goal:
X : TopCat
E : precoverage.ZeroHypercover X
x : (↑X : Type u)
refine_1 :
  ∀ (i : E.I₀) (y : (↑(E.X i) : Type u)),
    ∃ (i_1 : E.I₀) (y_1 :
      ToType (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max v u)), (↑Y : Type (max v u)))) (CC := carrier)
        (uliftFunctor.obj (E.X i_1))),
      Eq (α :=
        ToType (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max v u)), (↑Y : Type (max v u)))) (CC := carrier)
          (uliftFunctor.obj X))
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max v u)), (↑Y : Type (max v u)))) (CC :=
                carrier) (uliftFunctor.map (E.f i_1)) :
              (a : (↑(uliftFunctor.obj (E.X i_1)) : Type (max v u))) → (↑(uliftFunctor.obj X) : Type (max v u)))
            y_1 :
          (↑(uliftFunctor.obj X) : Type (max v u)))
        ({
            down :=
              (ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                    (E.f i) :
                  (a : (↑(E.X i) : Type u)) → (↑X : Type u))
                y } :
          ULift.{v, u} (↑X : Type u))
⊢ ∃ (i : E.I₀) (y :
    ToType (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max v u)), (↑Y : Type (max v u)))) (CC := carrier)
      (uliftFunctor.obj (E.X i))),
    (ConcreteCategory.hom (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max v u)), (↑Y : Type (max v u)))) (CC := carrier)
            (uliftFunctor.map (E.f i)) :
          (a : (↑(uliftFunctor.obj (E.X i)) : Type (max v u))) → (↑(uliftFunctor.obj X) : Type (max v u)))
        y =
      { down := x : ULift.{v, u} (↑X : Type u) }

Tactic:
obtain ⟨i, y, rfl⟩ := exists_mem_zeroHypercover_range E x

Premises used: TopCat.exists_mem_zeroHypercover_range, rfl
-- Module: Mathlib.Topology.Category.TopCat.GrothendieckTopology
Goal:
X : TopCat
E : precoverage.ZeroHypercover X
i : E.I₀
y : (↑(E.X i) : Type u)
h :
  Eq (α :=
    ToType (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max v u)), (↑Y : Type (max v u)))) (CC := carrier)
      (uliftFunctor.obj X))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max v u)), (↑Y : Type (max v u)))) (CC := carrier)
            (uliftFunctor.map (E.f i)) :
          (a : (↑(uliftFunctor.obj (E.X i)) : Type (max v u))) → (↑(uliftFunctor.obj X) : Type (max v u)))
        { down := y } :
      (↑(uliftFunctor.obj X) : Type (max v u)))
    ({
        down :=
          (ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                (E.f i) :
              (a : (↑(E.X i) : Type u)) → (↑X : Type u))
            y } :
      ULift.{v, u} (↑X : Type u))
⊢ ∃ (i_1 : E.I₀) (y_1 :
    ToType (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max v u)), (↑Y : Type (max v u)))) (CC := carrier)
      (uliftFunctor.obj (E.X i_1))),
    Eq (α :=
      ToType (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max v u)), (↑Y : Type (max v u)))) (CC := carrier)
        (uliftFunctor.obj X))
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max v u)), (↑Y : Type (max v u)))) (CC :=
              carrier) (uliftFunctor.map (E.f i_1)) :
            (a : (↑(uliftFunctor.obj (E.X i_1)) : Type (max v u))) → (↑(uliftFunctor.obj X) : Type (max v u)))
          y_1 :
        (↑(uliftFunctor.obj X) : Type (max v u)))
      ({
          down :=
            (ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                  (E.f i) :
                (a : (↑(E.X i) : Type u)) → (↑X : Type u))
              y } :
        ULift.{v, u} (↑X : Type u))

Tactic:
use i, ⟨y⟩
-- Module: Mathlib.Topology.Category.TopCat.GrothendieckTopology
Goal:
X : TopCat
E : precoverage.ZeroHypercover X
i : E.I₀
y : (↑(E.X i) : Type u)
⊢ Eq (α :=
    ToType (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max v u)), (↑Y : Type (max v u)))) (CC := carrier)
      (uliftFunctor.obj X))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max v u)), (↑Y : Type (max v u)))) (CC := carrier)
            (uliftFunctor.map (E.f i)) :
          (a : (↑(uliftFunctor.obj (E.X i)) : Type (max v u))) → (↑(uliftFunctor.obj X) : Type (max v u)))
        { down := y } :
      (↑(uliftFunctor.obj X) : Type (max v u)))
    ({
        down :=
          (ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                (E.f i) :
              (a : (↑(E.X i) : Type u)) → (↑X : Type u))
            y } :
      ULift.{v, u} (↑X : Type u))

Tactic:
rfl
-- Module: Mathlib.Topology.Category.TopCat.GrothendieckTopology
Goal:
X : TopCat
E : precoverage.ZeroHypercover X
refine_2 :
  ∀ (i : E.I₀),
    Topology.IsOpenEmbedding (X := (↑(uliftFunctor.obj (E.X i)) : Type (max u v))) (Y :=
      (↑(uliftFunctor.obj X) : Type (max u v)))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max u v)), (↑Y : Type (max u v)))) (CC :=
            carrier) (uliftFunctor.map (E.f i))) :
        (a : (↑(uliftFunctor.obj (E.X i)) : Type (max u v))) → (↑(uliftFunctor.obj X) : Type (max u v)))
⊢ Membership.mem (γ := Set (Presieve (uliftFunctor.obj X))) (isOpenEmbedding.precoverage.coverings (uliftFunctor.obj X))
    (Presieve.map uliftFunctor E.presieve₀)

Tactic:
simp only [Presieve.map_ofArrows, MorphismProperty.ofArrows_mem_precoverage,
      isOpenEmbedding_iff]

Premises used: TopCat.isOpenEmbedding_iff, CategoryTheory.MorphismProperty.ofArrows_mem_precoverage, CategoryTheory.Presieve.map_ofArrows
-- Module: Mathlib.Topology.Category.TopCat.GrothendieckTopology
Goal:
X : TopCat
E : precoverage.ZeroHypercover X
i : E.I₀
⊢ Topology.IsOpenEmbedding (X := (↑(uliftFunctor.obj (E.X i)) : Type (max u v))) (Y :=
    (↑(uliftFunctor.obj X) : Type (max u v)))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max u v)), (↑Y : Type (max u v)))) (CC := carrier)
          (uliftFunctor.map (E.f i))) :
      (a : (↑(uliftFunctor.obj (E.X i)) : Type (max u v))) → (↑(uliftFunctor.obj X) : Type (max u v)))

Tactic:
(isOpenEmbedding_f_zeroHypercover _ _).uliftMap

Premises used: Topology.IsOpenEmbedding.uliftMap, TopCat.isOpenEmbedding_f_zeroHypercover, ULift.map
-- Module: Mathlib.Topology.Category.TopCat.GrothendieckTopology
Goal:
X : TopCat
E : precoverage.ZeroHypercover X
i : E.I₀
⊢ Topology.IsOpenEmbedding (X := (↑(uliftFunctor.obj (E.X i)) : Type (max u v))) (Y :=
    (↑(uliftFunctor.obj X) : Type (max u v)))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max u v)), (↑Y : Type (max u v)))) (CC := carrier)
          (uliftFunctor.map (E.f i))) :
      (a : (↑(uliftFunctor.obj (E.X i)) : Type (max u v))) → (↑(uliftFunctor.obj X) : Type (max u v)))

Tactic:
exact (isOpenEmbedding_f_zeroHypercover _ _).uliftMap

Premises used: Topology.IsOpenEmbedding.uliftMap, TopCat.isOpenEmbedding_f_zeroHypercover
-- Module: Mathlib.Topology.Category.TopCat.GrothendieckTopology
Goal:
h : precoverage ≤ Precoverage.comap uliftFunctor precoverage
⊢ uliftFunctor.IsContinuous grothendieckTopology grothendieckTopology

Tactic:
apply Functor.isContinuous_toGrothendieck_of_pullbacksPreservedBy

Premises used: CategoryTheory.Functor.isContinuous_toGrothendieck_of_pullbacksPreservedBy
-- Module: Mathlib.Topology.Category.TopCat.GrothendieckTopology
Goal:
⊢ precoverage ≤ Precoverage.comap uliftFunctor precoverage

Tactic:
apply precoverage_le_comap_uliftFunctor

Premises used: TopCat.precoverage_le_comap_uliftFunctor
-- Module: Mathlib.Topology.Category.TopCat.Limits.Basic
Goal:
J : Type v
inst : Category.{w, v} J
F : J ⥤ TopCat
S : Cone F
x : (↑S.1 : Type (max u v))
i j : J
f : i ⟶ j
dsimp :
  Eq (α := (↑(F.obj j) : Type (max u v)))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max u v)), (↑Y : Type (max u v)))) (CC := carrier)
            (F.map f) :
          (a : (↑(F.obj i) : Type (max u v))) → (↑(F.obj j) : Type (max u v)))
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max u v)), (↑Y : Type (max u v)))) (CC :=
              carrier) (S.π.app i) :
            (a : (↑S.pt : Type (max u v))) → (↑(F.obj i) : Type (max u v)))
          x) :
      (↑(F.obj j) : Type (max u v)))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max u v)), (↑Y : Type (max u v)))) (CC := carrier)
            (S.π.app j) :
          (a : (↑S.pt : Type (max u v))) → (↑(F.obj j) : Type (max u v)))
        x :
      (↑(F.obj j) : Type (max u v)))
⊢ Eq (α := (↑(F.obj j) : Type (max u v)))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max u v)), (↑Y : Type (max u v)))) (CC := carrier)
          (F.map f) :
        (a : (↑(F.obj i) : Type (max u v))) → (↑(F.obj j) : Type (max u v)))
      ((fun (x_1 : J) ↦
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max u v)), (↑Y : Type (max u v)))) (CC :=
                  carrier) (S.π.app x_1) :
                (a : (↑(((Functor.const J).obj S.pt).obj x_1) : Type (max u v))) → (↑(F.obj x_1) : Type (max u v)))
              x :
            (↑(F.obj x_1) : Type (max u v))))
        i))
    ((fun (x_1 : J) ↦
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max u v)), (↑Y : Type (max u v)))) (CC :=
                carrier) (S.π.app x_1) :
              (a : (↑(((Functor.const J).obj S.pt).obj x_1) : Type (max u v))) → (↑(F.obj x_1) : Type (max u v)))
            x :
          (↑(F.obj x_1) : Type (max u v))))
      j)

Tactic:
dsimp
-- Module: Mathlib.Topology.Category.TopCat.Limits.Basic
Goal:
J : Type v
inst : Category.{w, v} J
F : J ⥤ TopCat
S : Cone F
x : (↑S.1 : Type (max u v))
i j : J
f : i ⟶ j
rw :
  Eq (α := (↑(F.obj j) : Type (max u v)))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max u v)), (↑Y : Type (max u v)))) (CC := carrier)
            (F.map f) :
          (a : (↑(F.obj i) : Type (max u v))) → (↑(F.obj j) : Type (max u v)))
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max u v)), (↑Y : Type (max u v)))) (CC :=
              carrier) (S.π.app i) :
            (a : (↑S.pt : Type (max u v))) → (↑(F.obj i) : Type (max u v)))
          x) :
      (↑(F.obj j) : Type (max u v)))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max u v)), (↑Y : Type (max u v)))) (CC := carrier)
            (S.π.app i ≫ F.map f) :
          (a : (↑S.pt : Type (max u v))) → (↑(F.obj j) : Type (max u v)))
        x :
      (↑(F.obj j) : Type (max u v)))
⊢ Eq (α := (↑(F.obj j) : Type (max u v)))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max u v)), (↑Y : Type (max u v)))) (CC := carrier)
            (F.map f) :
          (a : (↑(F.obj i) : Type (max u v))) → (↑(F.obj j) : Type (max u v)))
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max u v)), (↑Y : Type (max u v)))) (CC :=
              carrier) (S.π.app i) :
            (a : (↑S.pt : Type (max u v))) → (↑(F.obj i) : Type (max u v)))
          x) :
      (↑(F.obj j) : Type (max u v)))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max u v)), (↑Y : Type (max u v)))) (CC := carrier)
            (S.π.app j) :
          (a : (↑S.pt : Type (max u v))) → (↑(F.obj j) : Type (max u v)))
        x :
      (↑(F.obj j) : Type (max u v)))

Tactic:
rw [← S.w f]

Premises used: CategoryTheory.Limits.Cone.w