awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Sheaves.EtaleSpace (goal)
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)
⊢ 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)))
have 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 sorry)) : (a : CC (F.obj (op U))) → CC (F.stalk y)) :
        (a : CC (F.obj (op U))) → CC (F.stalk y)))
      sorry
      ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ U y hy) : (a : CC (F.obj (op U))) → CC (F.stalk y))
          (surjInv sorry g) :
        CC (F.stalk y))) =
  g
Tactic: congr
-- Lean 4 proof step from Mathlib.Topology.Sheaves.EtaleSpace (goal)
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)
⊢ (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
have e_snd : (ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ U x hx) : (a : CC (F.obj (op U))) → CC (F.stalk x)) (surjInv sorry g) =
  g
Tactic: rw [leftInverse_surjInv (hF_bij _ _), surjInv_eq (hF_bij _ _).surjective]
-- Lean 4 proof step from Mathlib.Topology.Sheaves.EtaleSpace (goal)
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
⊢ (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
have e_snd₁ : g = g
Tactic: rw [leftInverse_surjInv (hF_bij _ _), surjInv_eq (hF_bij _ _).surjective]
-- Lean 4 proof step from Mathlib.Topology.Sheaves.EtaleSpace (goal)
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 × 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)))))
have 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 sorry ((↑s : F.EtaleSpace).germ (CC := CC) (FC := FC))))
Tactic: refine .prodMk (by fun_prop) ?_
-- Lean 4 proof step from Mathlib.Topology.Sheaves.EtaleSpace (goal)
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 := 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))))
have 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 sorry ((↑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 sorry ((↑x_1 : F.EtaleSpace).germ (CC := CC) (FC := FC)))) :
            WithTopology (ToType (FC := FC) (CC := CC) (F.stalk x)) ⊥)
Tactic: simp_rw [continuous_iff_continuousAt, ContinuousAt, nhds_discrete, tendsto_pure, nhds_subtype,
      eventually_comap]
-- Lean 4 proof step from Mathlib.Topology.Sheaves.EtaleSpace (goal)
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
⊢ 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)) ⊥)
have 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 sorry ((↑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 sorry (g.germ (CC := CC) (FC := FC))) :
    CC (F.stalk x))
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Topology.Sheaves.EtaleSpace (goal)
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
⊢ 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))
have 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 sorry
        ((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)) :
    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 sorry (g.germ (CC := CC) (FC := FC))) :
    CC (F.stalk x))
Tactic: rw [hgf, ← hf, leftInverse_surjInv (hF_bij _ _), leftInverse_surjInv (hF_bij _ _)]
-- Lean 4 proof step from Mathlib.Topology.Sheaves.EtaleSpace (goal)
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 := (↑(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
have 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)) sorry) :
              (a : CC (F.obj (op U))) → CC (F.stalk (↑x_2 : (↑X : Type v))))
            (surjInv sorry x_1.2.ofTopology)))
        sorry)
    x_1.1
Tactic: simp_rw [continuous_iff_continuousAt, continuousAt_prod_of_discrete_right]
-- Lean 4 proof step from Mathlib.Topology.Sheaves.EtaleSpace (goal)
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)
⊢ 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
have 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)) sorry) :
              (a : CC (F.obj (op U))) → CC (F.stalk (↑y : (↑X : Type v))))
            (surjInv sorry 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)) sorry) :
            (a_1 : CC (F.obj (op U))) → CC (F.stalk (↑a : (↑X : Type v))))
          (surjInv sorry g)) ∈
      i
Tactic: simp only [ContinuousAt, nhds_subtype_eq_comap, tendsto_comap_iff, comp_def,
      nhds_generateFrom, tendsto_iInf, mem_setOf_eq, tendsto_principal]
-- Lean 4 proof step from Mathlib.Topology.Sheaves.EtaleSpace (hypothesis)
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)))
⊢ ∀ᶠ (a : ↥U) in 𝓝 y,
    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) (↑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)))
have 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)) sorry) :
          (a : CC (F.obj (op U))) → CC (F.stalk (↑y : (↑X : Type v))))
        (surjInv sorry g) :
      CC (F.stalk (↑y : (↑X : Type v))))
    ((ConcreteCategory.hom (FC := FC) (CC := CC) (F.germ V (↑y : (↑X : Type v)) sorry) :
          (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
Cleared hypotheses: hmem
-- Lean 4 proof step from Mathlib.Topology.Sheaves.EtaleSpace (hypothesis)
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))))
⊢ ∀ᶠ (a : ↥U) in 𝓝 y,
    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) (↑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)))
have hyV : (↑y : (↑X : Type v)) ∈ V
Tactic: rcases hmem with ⟨hyV, hgf⟩
Cleared hypotheses: hmem