awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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))
U : Opens (↑X : Type v)
hF_bij :
  ∀ (x : (↑X : Type v)) (hx : x ∈ U),
    Bijective.{v + 1, v + 1} (α := CC (F.obj (op U))) (β := CC (F.stalk x))
      (⇑(ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ U x hx)) : (a : CC (F.obj (op U))) → CC (F.stalk x))
x : (↑X : Type v)
hx : x ∈ U
g : F.EtaleSpace (CC := CC) (FC := FC)
hg :
  Membership.mem (γ := Set (F.EtaleSpace (CC := CC) (FC := FC)))
    (base (CC := CC) (FC := FC) ⁻¹' (↑U : Set (↑X : Type v))) g
f : CC (F.obj (op U))
hf :
  (ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ U (g.base (CC := CC) (FC := FC)) hg) :
        (a : CC (F.obj (op U))) → CC (F.stalk g.base))
      f =
    g.germ (CC := CC) (FC := FC)
g' : (↑(base (CC := CC) (FC := FC) ⁻¹' (↑U : Set (↑X : Type v))) : Type v)
hgU : (↑g' : F.EtaleSpace).base (CC := CC) (FC := FC) ∈ U
hgf :
  (↑g' : F.EtaleSpace).germ (CC := CC) (FC := FC) =
    (ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ U ((↑g' : F.EtaleSpace).base (CC := CC) (FC := FC)) hgU) :
        (a : CC (F.obj (op U))) → CC (F.stalk (↑g' : F.EtaleSpace).base))
      f
h :
  Eq (α := ToType (FC := FC) (CC := CC) (F.stalk x))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ U x hx) : (a : CC (F.obj (op U))) → CC (F.stalk x))
        (surjInv ⋯ ((↑g' : F.EtaleSpace).germ (CC := CC) (FC := FC))) :
      CC (F.stalk x))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ U x hx) : (a : CC (F.obj (op U))) → CC (F.stalk x))
        (surjInv ⋯ (g.germ (CC := CC) (FC := FC))) :
      CC (F.stalk x))
⊢ Eq (α := WithDiscreteTopology (ToType (FC := FC) (CC := CC) (F.stalk x)))
    (WithTopology.toTopology ⊥
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ U x hx) : (a : CC (F.obj (op U))) → CC (F.stalk x))
          (surjInv ⋯ ((↑g' : F.EtaleSpace).germ (CC := CC) (FC := FC)))) :
      WithTopology (ToType (FC := FC) (CC := CC) (F.stalk x)) ⊥)
    (WithTopology.toTopology ⊥
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ U x hx) : (a : CC (F.obj (op U))) → CC (F.stalk x))
          (surjInv ⋯ (g.germ (CC := CC) (FC := FC)))) :
      WithTopology (ToType (FC := FC) (CC := CC) (F.stalk x)) ⊥)

Tactic:
congr 1
-- 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))
U : Opens (↑X : Type v)
hF_bij :
  ∀ (x : (↑X : Type v)) (hx : x ∈ U),
    Bijective.{v + 1, v + 1} (α := CC (F.obj (op U))) (β := CC (F.stalk x))
      (⇑(ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ U x hx)) : (a : CC (F.obj (op U))) → CC (F.stalk x))
x : (↑X : Type v)
hx : x ∈ U
simp_rw :
  ∀ (x_1 : ↥U × WithDiscreteTopology (ToType (FC := FC) (CC := CC) (F.stalk x))),
    ContinuousAt (Y := (↑(base (CC := CC) (FC := FC) ⁻¹' (↑U : Set (↑X : Type v))) : Type v))
      (fun (x_2 : ↥U) ↦
        Subtype.mk (p := fun (x : F.EtaleSpace (CC := CC) (FC := FC)) ↦
          Membership.mem (γ := Set (F.EtaleSpace (CC := CC) (FC := FC)))
            (base (CC := CC) (FC := FC) ⁻¹' (↑U : Set (↑X : Type v))) x)
          (mk (CC := CC) (FC := FC) (↑x_2 : (↑X : Type v))
            ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ U (↑x_2 : (↑X : Type v)) ⋯) :
                (a : CC (F.obj (op U))) → CC (F.stalk (↑x_2 : (↑X : Type v))))
              (surjInv ⋯ x_1.2.ofTopology)))
          ⋯)
      x_1.1
⊢ Continuous (Y := (↑(base (CC := CC) (FC := FC) ⁻¹' (↑U : Set (↑X : Type v))) : Type v))
    fun (x_1 : ↥U × WithDiscreteTopology (ToType (FC := FC) (CC := CC) (F.stalk x))) ↦
    match (motive :=
      ↥U × WithDiscreteTopology (ToType (FC := FC) (CC := CC) (F.stalk x)) →
        (↑(base (CC := CC) (FC := FC) ⁻¹' (↑U : Set (↑X : Type v))) : Type v))
      x_1 with
    | (⟨y, hy⟩, WithTopology.toTopology .(⊥) g) =>
      Subtype.mk (p := fun (x : F.EtaleSpace (CC := CC) (FC := FC)) ↦
        Membership.mem (γ := Set (F.EtaleSpace (CC := CC) (FC := FC)))
          (base (CC := CC) (FC := FC) ⁻¹' (↑U : Set (↑X : Type v))) x)
        (mk (CC := CC) (FC := FC) y
          ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ U y hy) : (a : CC (F.obj (op U))) → CC (F.stalk y))
            (surjInv ⋯ g)))
        hy

Tactic:
simp_rw [continuous_iff_continuousAt, continuousAt_prod_of_discrete_right]

Premises used: continuousAt_prod_of_discrete_right, 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))
U : Opens (↑X : Type v)
hF_bij :
  ∀ (x : (↑X : Type v)) (hx : x ∈ U),
    Bijective.{v + 1, v + 1} (α := CC (F.obj (op U))) (β := CC (F.stalk x))
      (⇑(ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ U x hx)) : (a : CC (F.obj (op U))) → CC (F.stalk x))
x : (↑X : Type v)
hx : x ∈ U
y : ↥U
g : ToType (FC := FC) (CC := CC) (F.stalk x)
simp :
  ∀ (i : Set (F.EtaleSpace (CC := CC) (FC := FC)))
    (i_1 :
      mk (CC := CC) (FC := FC) (↑y : (↑X : Type v))
            ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ U (↑y : (↑X : Type v)) ⋯) :
                (a : CC (F.obj (op U))) → CC (F.stalk (↑y : (↑X : Type v))))
              (surjInv ⋯ g)) ∈
          i ∧
        ∃ (U : Opens (↑X : Type v)) (f : ToType (FC := FC) (CC := CC) (F.obj (op U))),
          {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))
                    f} =
            i),
    ∀ᶠ (a : ↥U) in 𝓝 y,
      mk (CC := CC) (FC := FC) (↑a : (↑X : Type v))
          ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ U (↑a : (↑X : Type v)) ⋯) :
              (a_1 : CC (F.obj (op U))) → CC (F.stalk (↑a : (↑X : Type v))))
            (surjInv ⋯ g)) ∈
        i
⊢ ContinuousAt (Y := (↑(base (CC := CC) (FC := FC) ⁻¹' (↑U : Set (↑X : Type v))) : Type v))
    (fun (x_1 : ↥U) ↦
      Subtype.mk (p := fun (x : F.EtaleSpace (CC := CC) (FC := FC)) ↦
        Membership.mem (γ := Set (F.EtaleSpace (CC := CC) (FC := FC)))
          (base (CC := CC) (FC := FC) ⁻¹' (↑U : Set (↑X : Type v))) x)
        (mk (CC := CC) (FC := FC) (↑x_1 : (↑X : Type v))
          ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ U (↑x_1 : (↑X : Type v)) ⋯) :
              (a : CC (F.obj (op U))) → CC (F.stalk (↑x_1 : (↑X : Type v))))
            (surjInv ⋯ (WithTopology.ofTopology (t := ⊥) (y, WithTopology.toTopology ⊥ g).2))))
        ⋯)
    (y, WithTopology.toTopology ⊥ g).1

Tactic:
simp only [ContinuousAt, nhds_subtype_eq_comap, tendsto_comap_iff, comp_def,
      nhds_generateFrom, tendsto_iInf, mem_setOf_eq, tendsto_principal]

Premises used: ContinuousAt, TopologicalSpace.nhds_generateFrom, Filter.tendsto_comap_iff, Filter.tendsto_principal, Set.mem_setOf_eq, nhds_subtype_eq_comap, Function.comp_def, Filter.tendsto_iInf
-- 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))
U : Opens (↑X : Type v)
hF_bij :
  ∀ (x : (↑X : Type v)) (hx : x ∈ U),
    Bijective.{v + 1, v + 1} (α := CC (F.obj (op U))) (β := CC (F.stalk x))
      (⇑(ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ U x hx)) : (a : CC (F.obj (op U))) → CC (F.stalk x))
x : (↑X : Type v)
hx : x ∈ U
y : ↥U
g : ToType (FC := FC) (CC := CC) (F.stalk x)
V : Opens (↑X : Type v)
f : ToType (FC := FC) (CC := CC) (F.obj (op V))
hmem :
  Membership.mem (γ := Set (F.EtaleSpace (CC := CC) (FC := FC)))
    {g : F.EtaleSpace (CC := CC) (FC := FC) |
      ∃ (h : g.base (CC := CC) (FC := FC) ∈ V),
        g.germ (CC := CC) (FC := FC) =
          (ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ V (g.base (CC := CC) (FC := FC)) h) :
              (a : CC (F.obj (op V))) → CC (F.stalk g.base))
            f}
    (mk (CC := CC) (FC := FC) (↑y : (↑X : Type v))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ U (↑y : (↑X : Type v)) ⋯) :
          (a : CC (F.obj (op U))) → CC (F.stalk (↑y : (↑X : Type v))))
        (surjInv ⋯ g)))
⊢ ∃ (h : (↑y : (↑X : Type v)) ∈ V),
    Eq (α := CC (F.stalk (↑y : (↑X : Type v))))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ U (↑y : (↑X : Type v)) ⋯) :
            (a : CC (F.obj (op U))) → CC (F.stalk (↑y : (↑X : Type v))))
          (surjInv ⋯ g) :
        CC (F.stalk (↑y : (↑X : Type v))))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ V (↑y : (↑X : Type v)) ⋯) :
            (a : CC (F.obj (op V))) → CC (F.stalk (↑y : (↑X : Type v))))
          f :
        CC (F.stalk (↑y : (↑X : Type v))))

Tactic:
simp only [mem_setOf_eq] at hmem

Premises used: Set.mem_setOf_eq
-- 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))
U : Opens (↑X : Type v)
hF_bij :
  ∀ (x : (↑X : Type v)) (hx : x ∈ U),
    Bijective.{v + 1, v + 1} (α := CC (F.obj (op U))) (β := CC (F.stalk x))
      (⇑(ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ U x hx)) : (a : CC (F.obj (op U))) → CC (F.stalk x))
x : (↑X : Type v)
hx : x ∈ U
y : ↥U
g : ToType (FC := FC) (CC := CC) (F.stalk x)
V : Opens (↑X : Type v)
f : ToType (FC := FC) (CC := CC) (F.obj (op V))
hmem :
  ∃ (h : (↑y : (↑X : Type v)) ∈ V),
    Eq (α := CC (F.stalk (↑y : (↑X : Type v))))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ U (↑y : (↑X : Type v)) ⋯) :
            (a : CC (F.obj (op U))) → CC (F.stalk (↑y : (↑X : Type v))))
          (surjInv ⋯ g) :
        CC (F.stalk (↑y : (↑X : Type v))))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ V (↑y : (↑X : Type v)) ⋯) :
            (a : CC (F.obj (op V))) → CC (F.stalk (↑y : (↑X : Type v))))
          f :
        CC (F.stalk (↑y : (↑X : Type v))))
⊢ (↑y : (↑X : Type v)) ∈ V

Tactic:
rcases hmem with ⟨hyV, hgf⟩
-- 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))
U : Opens (↑X : Type v)
hF_bij :
  ∀ (x : (↑X : Type v)) (hx : x ∈ U),
    Bijective.{v + 1, v + 1} (α := CC (F.obj (op U))) (β := CC (F.stalk x))
      (⇑(ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ U x hx)) : (a : CC (F.obj (op U))) → CC (F.stalk x))
x : (↑X : Type v)
hx : x ∈ U
y : ↥U
g : ToType (FC := FC) (CC := CC) (F.stalk x)
V : Opens (↑X : Type v)
f : ToType (FC := FC) (CC := CC) (F.obj (op V))
hmem :
  ∃ (h : (↑y : (↑X : Type v)) ∈ V),
    Eq (α := CC (F.stalk (↑y : (↑X : Type v))))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ U (↑y : (↑X : Type v)) ⋯) :
            (a : CC (F.obj (op U))) → CC (F.stalk (↑y : (↑X : Type v))))
          (surjInv ⋯ g) :
        CC (F.stalk (↑y : (↑X : Type v))))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ V (↑y : (↑X : Type v)) ⋯) :
            (a : CC (F.obj (op V))) → CC (F.stalk (↑y : (↑X : Type v))))
          f :
        CC (F.stalk (↑y : (↑X : Type v))))
hyV : (↑y : (↑X : Type v)) ∈ V
⊢ Eq (α := CC (F.stalk (↑y : (↑X : Type v))))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ U (↑y : (↑X : Type v)) ⋯) :
          (a : CC (F.obj (op U))) → CC (F.stalk (↑y : (↑X : Type v))))
        (surjInv ⋯ g) :
      CC (F.stalk (↑y : (↑X : Type v))))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ V (↑y : (↑X : Type v)) ⋯) :
          (a : CC (F.obj (op V))) → CC (F.stalk (↑y : (↑X : Type v))))
        f :
      CC (F.stalk (↑y : (↑X : Type v))))

Tactic:
rcases hmem with ⟨hyV, hgf⟩
-- 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))
U : Opens (↑X : Type v)
hF_bij :
  ∀ (x : (↑X : Type v)) (hx : x ∈ U),
    Bijective.{v + 1, v + 1} (α := CC (F.obj (op U))) (β := CC (F.stalk x))
      (⇑(ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ U x hx)) : (a : CC (F.obj (op U))) → CC (F.stalk x))
x : (↑X : Type v)
hx : x ∈ U
y : ↥U
g : ToType (FC := FC) (CC := CC) (F.stalk x)
V : Opens (↑X : Type v)
f : ToType (FC := FC) (CC := CC) (F.obj (op V))
hyV : (↑y : (↑X : Type v)) ∈ V
hgf :
  Eq (α := CC (F.stalk (↑y : (↑X : Type v))))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ U (↑y : (↑X : Type v)) ⋯) :
          (a : CC (F.obj (op U))) → CC (F.stalk (↑y : (↑X : Type v))))
        (surjInv ⋯ g) :
      CC (F.stalk (↑y : (↑X : Type v))))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ V (↑y : (↑X : Type v)) ⋯) :
          (a : CC (F.obj (op V))) → CC (F.stalk (↑y : (↑X : Type v))))
        f :
      CC (F.stalk (↑y : (↑X : Type v))))
W : Opens (↑X : Type v)
hyW : (↑y : (↑X : Type v)) ∈ W
ιWU : W ⟶ U
ιWV : W ⟶ V
hW :
  Eq (α := CC (F.obj (op W)))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map ιWU.op) : (a : CC (F.obj (op U))) → CC (F.obj (op W)))
        (surjInv ⋯ g) :
      CC (F.obj (op W)))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.map ιWV.op) : (a : CC (F.obj (op V))) → CC (F.obj (op W))) f :
      CC (F.obj (op W)))
z : ↥U
hz : Membership.mem (γ := Set ↥U) (Subtype.val (p := fun (x : (↑X : Type v)) ↦ x ∈ U) ⁻¹' (↑W : Set (↑X : Type v))) z
h :
  Eq (α := CC (F.stalk (↑z : (↑X : Type v))))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ U (↑z : (↑X : Type v)) ⋯) :
          (a : CC (F.obj (op U))) → CC (F.stalk (↑z : (↑X : Type v))))
        (surjInv ⋯ g) :
      CC (F.stalk (↑z : (↑X : Type v))))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ V (↑z : (↑X : Type v)) ⋯) :
          (a : CC (F.obj (op V))) → CC (F.stalk (↑z : (↑X : Type v))))
        f :
      CC (F.stalk (↑z : (↑X : Type v))))
⊢ ∃ (h : (↑z : (↑X : Type v)) ∈ V),
    Eq (α := CC (F.stalk (↑z : (↑X : Type v))))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ U (↑z : (↑X : Type v)) ⋯) :
            (a : CC (F.obj (op U))) → CC (F.stalk (↑z : (↑X : Type v))))
          (surjInv ⋯ g) :
        CC (F.stalk (↑z : (↑X : Type v))))
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ V (↑z : (↑X : Type v)) h) :
            (a : CC (F.obj (op V))) → CC (F.stalk (↑z : (↑X : Type v))))
          f :
        CC (F.stalk (↑z : (↑X : Type v))))

Tactic:
use ιWV.le hz

Premises used: Quiver.Hom.le
-- 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))
hF_bij :
  ∀ (x : (↑X : Type v)),
    ∃ (U : Opens (↑X : Type v)),
      x ∈ U ∧
        ∀ (y : (↑X : Type v)) (hyU : y ∈ U),
          Bijective.{v + 1, v + 1} (α := CC (F.obj (op U))) (β := CC (F.stalk y))
            (⇑(ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ U y hyU)) : (a : CC (F.obj (op U))) → CC (F.stalk y))
⊢ IsCoveringMap (E := F.EtaleSpace (CC := CC) (FC := FC)) (base (CC := CC) (FC := FC))

Tactic:
fun x ↦ .to_isEvenlyCovered_preimage (I := WithDiscreteTopology (ToType (F.stalk x))) ?_

Premises used: IsEvenlyCovered.to_isEvenlyCovered_preimage, IsCoveringMap
-- 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))
hF_bij :
  ∀ (x : (↑X : Type v)),
    ∃ (U : Opens (↑X : Type v)),
      x ∈ U ∧
        ∀ (y : (↑X : Type v)) (hyU : y ∈ U),
          Bijective.{v + 1, v + 1} (α := CC (F.obj (op U))) (β := CC (F.stalk y))
            (⇑(ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ U y hyU)) : (a : CC (F.obj (op U))) → CC (F.stalk y))
refine :
  ∀ (x : (↑X : Type v)),
    IsEvenlyCovered (E := F.EtaleSpace (CC := CC) (FC := FC)) (base (CC := CC) (FC := FC)) x
      (WithDiscreteTopology (ToType (FC := FC) (CC := CC) (F.stalk x)))
⊢ IsCoveringMap (E := F.EtaleSpace (CC := CC) (FC := FC)) (base (CC := CC) (FC := FC))

Tactic:
refine fun x ↦ .to_isEvenlyCovered_preimage (I := WithDiscreteTopology (ToType (F.stalk x))) ?_
-- 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))
hF_bij :
  ∀ (x : (↑X : Type v)),
    ∃ (U : Opens (↑X : Type v)),
      x ∈ U ∧
        ∀ (y : (↑X : Type v)) (hyU : y ∈ U),
          Bijective.{v + 1, v + 1} (α := CC (F.obj (op U))) (β := CC (F.stalk y))
            (⇑(ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ U y hyU)) : (a : CC (F.obj (op U))) → CC (F.stalk y))
x : (↑X : Type v)
right :
  ∃ (U : Set (↑X : Type v)),
    x ∈ U ∧
      IsOpen U ∧
        IsOpen (X := F.EtaleSpace (CC := CC) (FC := FC)) (base (CC := CC) (FC := FC) ⁻¹' U) ∧
          ∃ (H :
            (↑(base (CC := CC) (FC := FC) ⁻¹' U) : Type v) ≃ₜ
              (↑U : Type v) × WithDiscreteTopology (ToType (FC := FC) (CC := CC) (F.stalk x))),
            ∀ (x_1 : (↑(base (CC := CC) (FC := FC) ⁻¹' U) : Type v)),
              (↑((H : (a : (↑(base ⁻¹' U) : Type v)) → (↑U : Type v) × WithDiscreteTopology (ToType (F.stalk x)))
                        x_1).1 :
                  (↑X : Type v)) =
                (↑x_1 : F.EtaleSpace).base (CC := CC) (FC := FC)
⊢ IsEvenlyCovered (E := F.EtaleSpace (CC := CC) (FC := FC)) (base (CC := CC) (FC := FC)) x
    (WithDiscreteTopology (ToType (FC := FC) (CC := CC) (F.stalk x)))

Tactic:
use inferInstance
-- 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))
hF_bij :
  ∀ (x : (↑X : Type v)),
    ∃ (U : Opens (↑X : Type v)),
      x ∈ U ∧
        ∀ (y : (↑X : Type v)) (hyU : y ∈ U),
          Bijective.{v + 1, v + 1} (α := CC (F.obj (op U))) (β := CC (F.stalk y))
            (⇑(ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ U y hyU)) : (a : CC (F.obj (op U))) → CC (F.stalk y))
x : (↑X : Type v)
right :
  ∀ (U : Opens (↑X : Type v)) (hxU : x ∈ U)
    (hU_bij :
      ∀ (y : (↑X : Type v)) (hyU : y ∈ U),
        Bijective.{v + 1, v + 1} (α := CC (F.obj (op U))) (β := CC (F.stalk y))
          (⇑(ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ U y hyU)) : (a : CC (F.obj (op U))) → CC (F.stalk y))),
    ∃ (U : Set (↑X : Type v)),
      x ∈ U ∧
        IsOpen U ∧
          IsOpen (X := F.EtaleSpace (CC := CC) (FC := FC)) (base (CC := CC) (FC := FC) ⁻¹' U) ∧
            ∃ (H :
              (↑(base (CC := CC) (FC := FC) ⁻¹' U) : Type v) ≃ₜ
                (↑U : Type v) × WithDiscreteTopology (ToType (FC := FC) (CC := CC) (F.stalk x))),
              ∀ (x_1 : (↑(base (CC := CC) (FC := FC) ⁻¹' U) : Type v)),
                (↑((H : (a : (↑(base ⁻¹' U) : Type v)) → (↑U : Type v) × WithDiscreteTopology (ToType (F.stalk x)))
                          x_1).1 :
                    (↑X : Type v)) =
                  (↑x_1 : F.EtaleSpace).base (CC := CC) (FC := FC)
⊢ ∃ (U : Set (↑X : Type v)),
    x ∈ U ∧
      IsOpen U ∧
        IsOpen (X := F.EtaleSpace (CC := CC) (FC := FC)) (base (CC := CC) (FC := FC) ⁻¹' U) ∧
          ∃ (H :
            (↑(base (CC := CC) (FC := FC) ⁻¹' U) : Type v) ≃ₜ
              (↑U : Type v) × WithDiscreteTopology (ToType (FC := FC) (CC := CC) (F.stalk x))),
            ∀ (x_1 : (↑(base (CC := CC) (FC := FC) ⁻¹' U) : Type v)),
              (↑((H : (a : (↑(base ⁻¹' U) : Type v)) → (↑U : Type v) × WithDiscreteTopology (ToType (F.stalk x)))
                        x_1).1 :
                  (↑X : Type v)) =
                (↑x_1 : F.EtaleSpace).base (CC := CC) (FC := FC)

Tactic:
rcases hF_bij x with ⟨U, hxU, hU_bij⟩
-- 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))
hF_bij :
  ∀ (x : (↑X : Type v)),
    ∃ (U : Opens (↑X : Type v)),
      x ∈ U ∧
        ∀ (y : (↑X : Type v)) (hyU : y ∈ U),
          Bijective.{v + 1, v + 1} (α := CC (F.obj (op U))) (β := CC (F.stalk y))
            (⇑(ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ U y hyU)) : (a : CC (F.obj (op U))) → CC (F.stalk y))
x : (↑X : Type v)
U : Opens (↑X : Type v)
hxU : x ∈ U
hU_bij :
  ∀ (y : (↑X : Type v)) (hyU : y ∈ U),
    Bijective.{v + 1, v + 1} (α := CC (F.obj (op U))) (β := CC (F.stalk y))
      (⇑(ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ U y hyU)) : (a : CC (F.obj (op U))) → CC (F.stalk y))
h :
  ∀ (x_1 : (↑(base (CC := CC) (FC := FC) ⁻¹' (↑U : Set (↑X : Type v))) : Type v)),
    (↑((homeomorph (CC := CC) (FC := FC) U hU_bij x hxU :
                (a : (↑(base ⁻¹' (↑U : Set (↑X : Type v))) : Type v)) →
                  (↑(↑U : Set (↑X : Type v)) : Type v) × WithDiscreteTopology (ToType (F.stalk x)))
              x_1).1 :
        (↑X : Type v)) =
      (↑x_1 : F.EtaleSpace).base (CC := CC) (FC := FC)
⊢ ∃ (U : Set (↑X : Type v)),
    x ∈ U ∧
      IsOpen U ∧
        IsOpen (X := F.EtaleSpace (CC := CC) (FC := FC)) (base (CC := CC) (FC := FC) ⁻¹' U) ∧
          ∃ (H :
            (↑(base (CC := CC) (FC := FC) ⁻¹' U) : Type v) ≃ₜ
              (↑U : Type v) × WithDiscreteTopology (ToType (FC := FC) (CC := CC) (F.stalk x))),
            ∀ (x_1 : (↑(base (CC := CC) (FC := FC) ⁻¹' U) : Type v)),
              (↑((H : (a : (↑(base ⁻¹' U) : Type v)) → (↑U : Type v) × WithDiscreteTopology (ToType (F.stalk x)))
                        x_1).1 :
                  (↑X : Type v)) =
                (↑x_1 : F.EtaleSpace).base (CC := CC) (FC := FC)

Tactic:
use U, hxU, U.isOpen, U.isOpen.preimage (continuous_base F), homeomorph U hU_bij x hxU

Premises used: TopCat.Presheaf.EtaleSpace.continuous_base, TopologicalSpace.Opens.isOpen, IsOpen.preimage, TopCat.Presheaf.EtaleSpace.homeomorph