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))
x : F.EtaleSpace (CC := CC) (FC := FC)
U : Opens (↑X : Type v)
hxU : x.base (CC := CC) (FC := FC) ∈ (↑U : Set (↑X : Type v))
rcases :
  ∀ (V : Opens (↑X : Type v)) (hVU : V ≤ U) (hxV : x.base (CC := CC) (FC := FC) ∈ V)
    (f : ToType (FC := FC) (CC := CC) (F.obj (op V)))
    (hf :
      (ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ V (x.base (CC := CC) (FC := FC)) hxV) :
            (a : CC (F.obj (op V))) → CC (F.stalk x.base))
          f =
        x.germ (CC := CC) (FC := FC)),
    ∀ᶠ (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 : Set (↑X : Type v))

Tactic:
rcases F.exists_le_germ_eq x.germ hxU with ⟨V, hVU, hxV, f, hf⟩

Premises used: TopCat.Presheaf.exists_le_germ_eq, TopCat.Presheaf.EtaleSpace.germ
-- 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 : Opens (↑X : Type v)
hxU : x.base (CC := CC) (FC := FC) ∈ (↑U : Set (↑X : Type v))
V : Opens (↑X : Type v)
hVU : V ≤ U
hxV : x.base (CC := CC) (FC := FC) ∈ V
f : ToType (FC := FC) (CC := CC) (F.obj (op V))
hf :
  (ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ V (x.base (CC := CC) (FC := FC)) hxV) :
        (a : CC (F.obj (op V))) → CC (F.stalk x.base))
      f =
    x.germ (CC := CC) (FC := FC)
⊢ ∀ᶠ (x : F.EtaleSpace (CC := CC) (FC := FC)) in 𝓝 x, x.base (CC := CC) (FC := FC) ∈ (↑U : Set (↑X : Type v))

Tactic:
x.eventually_nhds hxV f hf |>.mono ?_

Premises used: Filter.Eventually.mono, TopCat.Presheaf.EtaleSpace.eventually_nhds
-- 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 : Opens (↑X : Type v)
hxU : x.base (CC := CC) (FC := FC) ∈ (↑U : Set (↑X : Type v))
V : Opens (↑X : Type v)
hVU : V ≤ U
hxV : x.base (CC := CC) (FC := FC) ∈ V
f : ToType (FC := FC) (CC := CC) (F.obj (op V))
hf :
  (ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ V (x.base (CC := CC) (FC := FC)) hxV) :
        (a : CC (F.obj (op V))) → CC (F.stalk x.base))
      f =
    x.germ (CC := CC) (FC := FC)
refine :
  ∀ (x : F.EtaleSpace (CC := CC) (FC := FC)),
    (∃ (hgU : x.base (CC := CC) (FC := FC) ∈ V),
        x.germ (CC := CC) (FC := FC) =
          (ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ V (x.base (CC := CC) (FC := FC)) hgU) :
              (a : CC (F.obj (op V))) → CC (F.stalk x.base))
            f) →
      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))

Tactic:
refine x.eventually_nhds hxV f hf |>.mono ?_

Premises used: Filter.Eventually.mono, TopCat.Presheaf.EtaleSpace.eventually_nhds
-- 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 : Opens (↑X : Type v)
hxU : x.base (CC := CC) (FC := FC) ∈ (↑U : Set (↑X : Type v))
V : Opens (↑X : Type v)
hVU : V ≤ U
hxV : x.base (CC := CC) (FC := FC) ∈ V
f : ToType (FC := FC) (CC := CC) (F.obj (op V))
hf :
  (ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ V (x.base (CC := CC) (FC := FC)) hxV) :
        (a : CC (F.obj (op V))) → CC (F.stalk x.base))
      f =
    x.germ (CC := CC) (FC := FC)
⊢ ∀ (x : F.EtaleSpace (CC := CC) (FC := FC)),
    (∃ (hgU : x.base (CC := CC) (FC := FC) ∈ V),
        x.germ (CC := CC) (FC := FC) =
          (ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ V (x.base (CC := CC) (FC := FC)) hgU) :
              (a : CC (F.obj (op V))) → CC (F.stalk x.base))
            f) →
      x.base (CC := CC) (FC := FC) ∈ (↑U : Set (↑X : Type v))

Tactic:
aesop
-- 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))
α : Type u_1
l : Filter α
g : α → F.EtaleSpace (CC := CC) (FC := FC)
g₀ : F.EtaleSpace (CC := CC) (FC := FC)
h : Tendsto g l (𝓝 g₀)
rcases :
  ∀ (U : Opens (↑X : Type v)) (hU : 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)) hU) :
            (a : CC (F.obj (op U))) → CC (F.stalk g₀.base))
          s =
        g₀.germ (CC := CC) (FC := FC)),
    ∃ (U : Opens (↑X : Type v)),
      g₀.base (CC := CC) (FC := FC) ∈ U ∧
        ∃ (f : ToType (FC := FC) (CC := CC) (F.obj (op U))),
          ∀ᶠ (a : α) in l,
            ∃ (ha : (g a).base (CC := CC) (FC := FC) ∈ U),
              (g a).germ (CC := CC) (FC := FC) =
                (ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ U ((g a).base (CC := CC) (FC := FC)) ha) :
                    (a_1 : CC (F.obj (op U))) → CC (F.stalk (g a).base))
                  f
⊢ ∃ (U : Opens (↑X : Type v)),
    g₀.base (CC := CC) (FC := FC) ∈ U ∧
      ∃ (f : ToType (FC := FC) (CC := CC) (F.obj (op U))),
        ∀ᶠ (a : α) in l,
          ∃ (ha : (g a).base (CC := CC) (FC := FC) ∈ U),
            (g a).germ (CC := CC) (FC := FC) =
              (ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ U ((g a).base (CC := CC) (FC := FC)) ha) :
                  (a_1 : CC (F.obj (op U))) → CC (F.stalk (g a).base))
                f

Tactic:
rcases F.exists_germ_eq g₀.germ with ⟨U, hU, s, hs⟩

Premises used: TopCat.Presheaf.exists_germ_eq, TopCat.Presheaf.EtaleSpace.germ
-- 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))
α : Type u_1
l : Filter α
g : α → F.EtaleSpace (CC := CC) (FC := FC)
g₀ : F.EtaleSpace (CC := CC) (FC := FC)
h : Tendsto g l (𝓝 g₀)
U : Opens (↑X : Type v)
hU : 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)) hU) :
        (a : CC (F.obj (op U))) → CC (F.stalk g₀.base))
      s =
    g₀.germ (CC := CC) (FC := FC)
h₁ :
  ∀ᶠ (a : α) in l,
    ∃ (ha : (g a).base (CC := CC) (FC := FC) ∈ U),
      (g a).germ (CC := CC) (FC := FC) =
        (ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ U ((g a).base (CC := CC) (FC := FC)) ha) :
            (a_1 : CC (F.obj (op U))) → CC (F.stalk (g a).base))
          s
⊢ ∃ (U : Opens (↑X : Type v)),
    g₀.base (CC := CC) (FC := FC) ∈ U ∧
      ∃ (f : ToType (FC := FC) (CC := CC) (F.obj (op U))),
        ∀ᶠ (a : α) in l,
          ∃ (ha : (g a).base (CC := CC) (FC := FC) ∈ U),
            (g a).germ (CC := CC) (FC := FC) =
              (ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ U ((g a).base (CC := CC) (FC := FC)) ha) :
                  (a_1 : CC (F.obj (op U))) → CC (F.stalk (g a).base))
                f

Tactic:
use U, hU, s
-- 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))
α : Type u_1
l : Filter α
g : α → F.EtaleSpace (CC := CC) (FC := FC)
g₀ : F.EtaleSpace (CC := CC) (FC := FC)
h : Tendsto g l (𝓝 g₀)
U : Opens (↑X : Type v)
hU : 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)) hU) :
        (a : CC (F.obj (op U))) → CC (F.stalk g₀.base))
      s =
    g₀.germ (CC := CC) (FC := FC)
⊢ ∀ᶠ (a : α) in l,
    ∃ (ha : (g a).base (CC := CC) (FC := FC) ∈ U),
      (g a).germ (CC := CC) (FC := FC) =
        (ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ U ((g a).base (CC := CC) (FC := FC)) ha) :
            (a_1 : CC (F.obj (op U))) → CC (F.stalk (g a).base))
          s

Tactic:
h.eventually <| g₀.eventually_nhds hU s hs

Premises used: Filter.Tendsto.eventually, TopCat.Presheaf.EtaleSpace.eventually_nhds
-- 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))
α : Type u_1
l : Filter α
g : α → F.EtaleSpace (CC := CC) (FC := FC)
g₀ : F.EtaleSpace (CC := CC) (FC := FC)
h : Tendsto g l (𝓝 g₀)
U : Opens (↑X : Type v)
hU : 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)) hU) :
        (a : CC (F.obj (op U))) → CC (F.stalk g₀.base))
      s =
    g₀.germ (CC := CC) (FC := FC)
⊢ ∀ᶠ (a : α) in l,
    ∃ (ha : (g a).base (CC := CC) (FC := FC) ∈ U),
      (g a).germ (CC := CC) (FC := FC) =
        (ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ U ((g a).base (CC := CC) (FC := FC)) ha) :
            (a_1 : CC (F.obj (op U))) → CC (F.stalk (g a).base))
          s

Tactic:
exact h.eventually <| g₀.eventually_nhds hU s hs

Premises used: Filter.Tendsto.eventually, TopCat.Presheaf.EtaleSpace.eventually_nhds
-- 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
base : (↑X : Type v)
s : ToType (FC := FC) (CC := CC) (F.stalk base)
hs :
  Membership.mem (γ := Set (F.EtaleSpace (CC := CC) (FC := FC)))
    (EtaleSpace.base (CC := CC) (FC := FC) ⁻¹' (↑U : Set (↑X : Type v))) (mk (CC := CC) (FC := FC) base s)
e_val :
  (ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ U base ⋯) : (a : CC (F.obj (op U))) → CC (F.stalk base))
      (surjInv ⋯
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ U x hx) : (a : CC (F.obj (op U))) → CC (F.stalk x))
          (surjInv ⋯ s))) =
    s
⊢ Subtype.mk (p := fun (x : F.EtaleSpace (CC := CC) (FC := FC)) ↦
      Membership.mem (γ := Set (F.EtaleSpace (CC := CC) (FC := FC)))
        (EtaleSpace.base (CC := CC) (FC := FC) ⁻¹' (↑U : Set (↑X : Type v))) x)
      (mk (CC := CC) (FC := FC) base
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ U base ⋯) : (a : CC (F.obj (op U))) → CC (F.stalk base))
          (surjInv ⋯
            ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ U x hx) : (a : CC (F.obj (op U))) → CC (F.stalk x))
              (surjInv ⋯ s)))))
      ⋯ =
    Subtype.mk (p := fun (x : F.EtaleSpace (CC := CC) (FC := FC)) ↦
      Membership.mem (γ := Set (F.EtaleSpace (CC := CC) (FC := FC)))
        (EtaleSpace.base (CC := CC) (FC := FC) ⁻¹' (↑U : Set (↑X : Type v))) x)
      (mk (CC := CC) (FC := FC) base s) hs

Tactic:
congr 2
-- 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
base : (↑X : Type v)
s : ToType (FC := FC) (CC := CC) (F.stalk base)
hs :
  Membership.mem (γ := Set (F.EtaleSpace (CC := CC) (FC := FC)))
    (EtaleSpace.base (CC := CC) (FC := FC) ⁻¹' (↑U : Set (↑X : Type v))) (mk (CC := CC) (FC := FC) base s)
e_val :
  (ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ U base ⋯) : (a : CC (F.obj (op U))) → CC (F.stalk base))
      (surjInv ⋯ s) =
    s
e_val₁ e_val₂ : s = s
⊢ (ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ U base ⋯) : (a : CC (F.obj (op U))) → CC (F.stalk base))
      (surjInv ⋯
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ U x hx) : (a : CC (F.obj (op U))) → CC (F.stalk x))
          (surjInv ⋯ s))) =
    s

Tactic:
rw [leftInverse_surjInv (hF_bij _ _), surjInv_eq (hF_bij _ _).surjective]

Premises used: Function.surjInv_eq, Function.Bijective.surjective, Function.leftInverse_surjInv
-- 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 : (↑X : Type v)
hy : y ∈ U
g : ToType (FC := FC) (CC := CC) (F.stalk x)
e_snd :
  (ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ U x hx) : (a : CC (F.obj (op U))) → CC (F.stalk x))
      (surjInv (β := CC (F.stalk y)) (f :=
        ((⇑(ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ U y ⋯)) : (a : CC (F.obj (op U))) → CC (F.stalk y)) :
          (a : CC (F.obj (op U))) → CC (F.stalk y)))
        ⋯
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ U y hy) : (a : CC (F.obj (op U))) → CC (F.stalk y))
            (surjInv ⋯ g) :
          CC (F.stalk y))) =
    g
⊢ Eq (α := ↥U × WithDiscreteTopology (ToType (FC := FC) (CC := CC) (F.stalk x)))
    ((Subtype.mk (p := fun (x : (↑X : Type v)) ↦ x ∈ U) y ⋯,
        WithTopology.toTopology ⊥
          ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ U x hx) : (a : CC (F.obj (op U))) → CC (F.stalk x))
            (surjInv (β := CC (F.stalk y)) (f :=
              ((⇑(ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ U y ⋯)) :
                  (a : CC (F.obj (op U))) → CC (F.stalk y)) :
                (a : CC (F.obj (op U))) → CC (F.stalk y)))
              ⋯
              ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ U y hy) : (a : CC (F.obj (op U))) → CC (F.stalk y))
                  (surjInv ⋯ g) :
                CC (F.stalk y))))) :
      ↥U × WithDiscreteTopology (ToType (FC := FC) (CC := CC) (F.stalk x)))
    ((Subtype.mk (p := fun (x : (↑X : Type v)) ↦ x ∈ U) y hy, WithTopology.toTopology ⊥ g) :
      ↥U × WithDiscreteTopology (ToType (FC := FC) (CC := CC) (F.stalk x)))

Tactic:
congr
-- 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 : (↑X : Type v)
hy : y ∈ U
g : ToType (FC := FC) (CC := CC) (F.stalk x)
e_snd :
  (ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ U x hx) : (a : CC (F.obj (op U))) → CC (F.stalk x))
      (surjInv ⋯ g) =
    g
e_snd₁ e_snd₂ : g = g
⊢ (ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ U x hx) : (a : CC (F.obj (op U))) → CC (F.stalk x))
      (surjInv (β := CC (F.stalk y)) (f :=
        ((⇑(ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ U y ⋯)) : (a : CC (F.obj (op U))) → CC (F.stalk y)) :
          (a : CC (F.obj (op U))) → CC (F.stalk y)))
        ⋯
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ U y hy) : (a : CC (F.obj (op U))) → CC (F.stalk y))
            (surjInv ⋯ g) :
          CC (F.stalk y))) =
    g

Tactic:
rw [leftInverse_surjInv (hF_bij _ _), surjInv_eq (hF_bij _ _).surjective]

Premises used: Function.surjInv_eq, Function.Bijective.surjective, Function.leftInverse_surjInv
-- 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
⊢ Continuous (Y := ↥U) fun (s : (↑(base (CC := CC) (FC := FC) ⁻¹' (↑U : Set (↑X : Type v))) : Type v)) ↦
    Subtype.mk (p := fun (x : (↑X : Type v)) ↦ x ∈ U) ((↑s : F.EtaleSpace).base (CC := CC) (FC := FC)) ⋯

Tactic:
fun_prop
-- 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
refine :
  Continuous (Y := WithDiscreteTopology (ToType (FC := FC) (CC := CC) (F.stalk x)))
    fun (s : (↑(base (CC := CC) (FC := FC) ⁻¹' (↑U : Set (↑X : Type v))) : Type v)) ↦
    WithTopology.toTopology ⊥
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ U x hx) : (a : CC (F.obj (op U))) → CC (F.stalk x))
        (surjInv ⋯ ((↑s : F.EtaleSpace).germ (CC := CC) (FC := FC))))
⊢ Continuous (Y := ↥U × WithDiscreteTopology (ToType (FC := FC) (CC := CC) (F.stalk x)))
    fun (s : (↑(base (CC := CC) (FC := FC) ⁻¹' (↑U : Set (↑X : Type v))) : Type v)) ↦
    (Subtype.mk (p := fun (x : (↑X : Type v)) ↦ x ∈ U) ((↑s : F.EtaleSpace).base (CC := CC) (FC := FC)) ⋯,
      WithTopology.toTopology ⊥
        ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ U x hx) : (a : CC (F.obj (op U))) → CC (F.stalk x))
          (surjInv ⋯ ((↑s : F.EtaleSpace).germ (CC := CC) (FC := FC)))))

Tactic:
refine .prodMk (by fun_prop) ?_
-- 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 : (↑(base (CC := CC) (FC := FC) ⁻¹' (↑U : Set (↑X : Type v))) : Type v)),
    ∀ᶠ (b : F.EtaleSpace (CC := CC) (FC := FC)) in 𝓝 (↑x_1 : F.EtaleSpace),
      ∀ (a : (↑(base (CC := CC) (FC := FC) ⁻¹' (↑U : Set (↑X : Type v))) : Type v)),
        (↑a : F.EtaleSpace) = b →
          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 ⋯ ((↑a : 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 ⋯ ((↑x_1 : F.EtaleSpace).germ (CC := CC) (FC := FC)))) :
              WithTopology (ToType (FC := FC) (CC := CC) (F.stalk x)) ⊥)
⊢ Continuous (Y := WithDiscreteTopology (ToType (FC := FC) (CC := CC) (F.stalk x)))
    fun (s : (↑(base (CC := CC) (FC := FC) ⁻¹' (↑U : Set (↑X : Type v))) : Type v)) ↦
    WithTopology.toTopology ⊥
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ U x hx) : (a : CC (F.obj (op U))) → CC (F.stalk x))
        (surjInv ⋯ ((↑s : F.EtaleSpace).germ (CC := CC) (FC := FC))))

Tactic:
simp_rw [continuous_iff_continuousAt, ContinuousAt, nhds_discrete, tendsto_pure, nhds_subtype,
      eventually_comap]

Premises used: ContinuousAt, Filter.tendsto_pure, nhds_subtype, Filter.eventually_comap, nhds_discrete, continuous_iff_continuousAt