awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.LocallyClosed
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
tfae_1_to_2 : ∀ (a : IsLocallyClosed s), IsOpen[inst] (coborder s)
tfae_2_to_3 : ∀ (a : IsOpen[inst] (coborder s)), ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsClosed[instTopologicalSpaceSubtype] (U ↓∩ s)
⊢ ∀ (a : ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsClosed[instTopologicalSpaceSubtype] (U ↓∩ s)),
    ∀ x ∈ s, ∃ (U : Set X), x ∈ U ∧ IsOpen[inst] U ∧ U ∩ closure[inst] s ⊆ s

Tactic:
3 → 4

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Topology.LocallyClosed
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
tfae_1_to_2 : ∀ (a : IsLocallyClosed s), IsOpen[inst] (coborder s)
tfae_2_to_3 : ∀ (a : IsOpen[inst] (coborder s)), ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsClosed[instTopologicalSpaceSubtype] (U ↓∩ s)
h : ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsClosed[instTopologicalSpaceSubtype] (U ↓∩ s)
x : X
hx : x ∈ s
obtain :
  ∀ (t : Set X) (ht : t ∈ 𝓝 x) (ht' : IsClosed[instTopologicalSpaceSubtype] (t ↓∩ s)),
    ∃ (U : Set X), x ∈ U ∧ IsOpen[inst] U ∧ U ∩ closure[inst] s ⊆ s
⊢ ∃ (U : Set X), x ∈ U ∧ IsOpen[inst] U ∧ U ∩ closure[inst] s ⊆ s

Tactic:
obtain ⟨t, ht, ht'⟩ := h x hx
-- Module: Mathlib.Topology.LocallyClosed
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
tfae_1_to_2 : ∀ (a : IsLocallyClosed s), IsOpen[inst] (coborder s)
tfae_2_to_3 : ∀ (a : IsOpen[inst] (coborder s)), ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsClosed[instTopologicalSpaceSubtype] (U ↓∩ s)
h : ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsClosed[instTopologicalSpaceSubtype] (U ↓∩ s)
x : X
hx : x ∈ s
t : Set X
ht : t ∈ 𝓝 x
ht' : IsClosed[instTopologicalSpaceSubtype] (t ↓∩ s)
obtain :
  ∀ (U : Set X) (hUt : U ⊆ t) (hU : IsOpen[inst] U) (hxU : x ∈ U),
    ∃ (U : Set X), x ∈ U ∧ IsOpen[inst] U ∧ U ∩ closure[inst] s ⊆ s
⊢ ∃ (U : Set X), x ∈ U ∧ IsOpen[inst] U ∧ U ∩ closure[inst] s ⊆ s

Tactic:
obtain ⟨U, hUt, hU, hxU⟩ := mem_nhds_iff.mp ht

Premises used: mem_nhds_iff, Iff.mp
-- Module: Mathlib.Topology.LocallyClosed
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
tfae_1_to_2 : ∀ (a : IsLocallyClosed s), IsOpen[inst] (coborder s)
tfae_2_to_3 : ∀ (a : IsOpen[inst] (coborder s)), ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsClosed[instTopologicalSpaceSubtype] (U ↓∩ s)
h : ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsClosed[instTopologicalSpaceSubtype] (U ↓∩ s)
x : X
hx : x ∈ s
t : Set X
ht : t ∈ 𝓝 x
ht' : IsClosed[instTopologicalSpaceSubtype] (t ↓∩ s)
U : Set X
hUt : U ⊆ t
hU : IsOpen[inst] U
hxU : x ∈ U
rw :
  ∀ (ht' : t ∩ closure[inst] (t ∩ s) ⊆ s) (U : Set X) (hUt : U ⊆ t) (hU : IsOpen[inst] U) (hxU : x ∈ U),
    ∃ (U : Set X), x ∈ U ∧ IsOpen[inst] U ∧ U ∩ closure[inst] s ⊆ s
⊢ ∃ (U : Set X), x ∈ U ∧ IsOpen[inst] U ∧ U ∩ closure[inst] s ⊆ s

Tactic:
rw [isClosed_preimage_val] at ht'

Premises used: isClosed_preimage_val
-- Module: Mathlib.Topology.LocallyClosed
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
tfae_1_to_2 : ∀ (a : IsLocallyClosed s), IsOpen[inst] (coborder s)
tfae_2_to_3 : ∀ (a : IsOpen[inst] (coborder s)), ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsClosed[instTopologicalSpaceSubtype] (U ↓∩ s)
h : ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsClosed[instTopologicalSpaceSubtype] (U ↓∩ s)
x : X
hx : x ∈ s
t : Set X
ht : t ∈ 𝓝 x
ht' : t ∩ closure[inst] (t ∩ s) ⊆ s
U : Set X
hUt : U ⊆ t
hU : IsOpen[inst] U
hxU : x ∈ U
⊢ ∃ (U : Set X), x ∈ U ∧ IsOpen[inst] U ∧ U ∩ closure[inst] s ⊆ s

Tactic:
⟨U, hxU, hU, (subset_inter (inter_subset_left.trans hUt) (hU.inter_closure.trans
      (closure_mono <| inter_subset_inter hUt subset_rfl))).trans ht'⟩

Premises used: IsOpen.inter_closure, HasSubset.Subset.trans, Set.inter_subset_left, closure_mono, Set.inter_subset_inter, Set.subset_inter, And.intro, Exists.intro, subset_rfl
-- Module: Mathlib.Topology.LocallyClosed
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
tfae_1_to_2 : ∀ (a : IsLocallyClosed s), IsOpen[inst] (coborder s)
tfae_2_to_3 : ∀ (a : IsOpen[inst] (coborder s)), ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsClosed[instTopologicalSpaceSubtype] (U ↓∩ s)
h : ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsClosed[instTopologicalSpaceSubtype] (U ↓∩ s)
x : X
hx : x ∈ s
t : Set X
ht : t ∈ 𝓝 x
ht' : t ∩ closure[inst] (t ∩ s) ⊆ s
U : Set X
hUt : U ⊆ t
hU : IsOpen[inst] U
hxU : x ∈ U
⊢ ∃ (U : Set X), x ∈ U ∧ IsOpen[inst] U ∧ U ∩ closure[inst] s ⊆ s

Tactic:
exact ⟨U, hxU, hU, (subset_inter (inter_subset_left.trans hUt) (hU.inter_closure.trans
      (closure_mono <| inter_subset_inter hUt subset_rfl))).trans ht'⟩
-- Module: Mathlib.Topology.LocallyClosed
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
tfae_1_to_2 : ∀ (a : IsLocallyClosed s), IsOpen[inst] (coborder s)
tfae_2_to_3 : ∀ (a : IsOpen[inst] (coborder s)), ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsClosed[instTopologicalSpaceSubtype] (U ↓∩ s)
⊢ ∀ (a : ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsClosed[instTopologicalSpaceSubtype] (U ↓∩ s)),
    ∀ x ∈ s, ∃ (U : Set X), x ∈ U ∧ IsOpen[inst] U ∧ U ∩ closure[inst] s ⊆ s

Tactic:
tfae_have 3 → 4
  | h, x, hx => by
    obtain ⟨t, ht, ht'⟩ := h x hx
    obtain ⟨U, hUt, hU, hxU⟩ := mem_nhds_iff.mp ht
    rw [isClosed_preimage_val] at ht'
    exact ⟨U, hxU, hU, (subset_inter (inter_subset_left.trans hUt) (hU.inter_closure.trans
      (closure_mono <| inter_subset_inter hUt subset_rfl))).trans ht'⟩
-- Module: Mathlib.Topology.LocallyClosed
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
tfae_1_to_2 : ∀ (a : IsLocallyClosed s), IsOpen[inst] (coborder s)
tfae_2_to_3 : ∀ (a : IsOpen[inst] (coborder s)), ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsClosed[instTopologicalSpaceSubtype] (U ↓∩ s)
tfae_3_to_4 :
  ∀ (a : ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsClosed[instTopologicalSpaceSubtype] (U ↓∩ s)),
    ∀ x ∈ s, ∃ (U : Set X), x ∈ U ∧ IsOpen[inst] U ∧ U ∩ closure[inst] s ⊆ s
⊢ ∀ x ∈ s, ∃ (U : Set X), x ∈ U ∧ IsOpen[inst] U ∧ U ∩ closure[inst] s ⊆ s

Tactic:
4

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Topology.LocallyClosed
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
tfae_1_to_2 : ∀ (a : IsLocallyClosed s), IsOpen[inst] (coborder s)
tfae_2_to_3 : ∀ (a : IsOpen[inst] (coborder s)), ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsClosed[instTopologicalSpaceSubtype] (U ↓∩ s)
tfae_3_to_4 :
  ∀ (a : ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsClosed[instTopologicalSpaceSubtype] (U ↓∩ s)),
    ∀ x ∈ s, ∃ (U : Set X), x ∈ U ∧ IsOpen[inst] U ∧ U ∩ closure[inst] s ⊆ s
⊢ IsOpen[instTopologicalSpaceSubtype] (closure[inst] s ↓∩ s)

Tactic:
5

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Topology.LocallyClosed
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
tfae_1_to_2 : ∀ (a : IsLocallyClosed s), IsOpen[inst] (coborder s)
tfae_2_to_3 : ∀ (a : IsOpen[inst] (coborder s)), ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsClosed[instTopologicalSpaceSubtype] (U ↓∩ s)
tfae_3_to_4 :
  ∀ (a : ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsClosed[instTopologicalSpaceSubtype] (U ↓∩ s)),
    ∀ x ∈ s, ∃ (U : Set X), x ∈ U ∧ IsOpen[inst] U ∧ U ∩ closure[inst] s ⊆ s
⊢ ∀ (a : ∀ x ∈ s, ∃ (U : Set X), x ∈ U ∧ IsOpen[inst] U ∧ U ∩ closure[inst] s ⊆ s),
    IsOpen[instTopologicalSpaceSubtype] (closure[inst] s ↓∩ s)

Tactic:
4 → 5

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Topology.LocallyClosed
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
tfae_1_to_2 : ∀ (a : IsLocallyClosed s), IsOpen[inst] (coborder s)
tfae_2_to_3 : ∀ (a : IsOpen[inst] (coborder s)), ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsClosed[instTopologicalSpaceSubtype] (U ↓∩ s)
tfae_3_to_4 :
  ∀ (a : ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsClosed[instTopologicalSpaceSubtype] (U ↓∩ s)),
    ∀ x ∈ s, ∃ (U : Set X), x ∈ U ∧ IsOpen[inst] U ∧ U ∩ closure[inst] s ⊆ s
h : ∀ x ∈ s, ∃ (U : Set X), x ∈ U ∧ IsOpen[inst] U ∧ U ∩ closure[inst] s ⊆ s
H : ∀ x ∈ s, ∃ (U : Set X), x ∈ U ∧ IsOpen[inst] U ∧ U ∩ closure[inst] s ⊆ s := h
choose :
  ∀ (U : (x : X) → x ∈ s → Set X) (hxU : ∀ (x : X) (a : x ∈ s), x ∈ U x a)
    (hU : ∀ (x : X) (a : x ∈ s), IsOpen[inst] (U x a)) (e : ∀ (x : X) (a : x ∈ s), U x a ∩ closure[inst] s ⊆ s),
    IsOpen[instTopologicalSpaceSubtype] (closure[inst] s ↓∩ s)
⊢ IsOpen[instTopologicalSpaceSubtype] (closure[inst] s ↓∩ s)

Tactic:
choose U hxU hU e using H
-- Module: Mathlib.Topology.LocallyClosed
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
tfae_1_to_2 : ∀ (a : IsLocallyClosed s), IsOpen[inst] (coborder s)
tfae_2_to_3 : ∀ (a : IsOpen[inst] (coborder s)), ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsClosed[instTopologicalSpaceSubtype] (U ↓∩ s)
tfae_3_to_4 :
  ∀ (a : ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsClosed[instTopologicalSpaceSubtype] (U ↓∩ s)),
    ∀ x ∈ s, ∃ (U : Set X), x ∈ U ∧ IsOpen[inst] U ∧ U ∩ closure[inst] s ⊆ s
h : ∀ x ∈ s, ∃ (U : Set X), x ∈ U ∧ IsOpen[inst] U ∧ U ∩ closure[inst] s ⊆ s
U : (x : X) → x ∈ s → Set X
hxU : ∀ (x : X) (a : x ∈ s), x ∈ U x a
hU : ∀ (x : X) (a : x ∈ s), IsOpen[inst] (U x a)
e : ∀ (x : X) (a : x ∈ s), U x a ∩ closure[inst] s ⊆ s
⊢ IsOpen[instTopologicalSpaceSubtype] (closure[inst] s ↓∩ s)

Tactic:
⟨⋃ x ∈ s, U x ‹_›, isOpen_iUnion (isOpen_iUnion <| hU ·), ext fun x ↦ ⟨?_, ?_⟩⟩

Premises used: Set.ext, isOpen_iUnion, And.intro, Iff.intro, Exists.intro, IsOpen, Set.iUnion
-- Module: Mathlib.Topology.LocallyClosed
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
tfae_1_to_2 : ∀ (a : IsLocallyClosed s), IsOpen[inst] (coborder s)
tfae_2_to_3 : ∀ (a : IsOpen[inst] (coborder s)), ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsClosed[instTopologicalSpaceSubtype] (U ↓∩ s)
tfae_3_to_4 :
  ∀ (a : ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsClosed[instTopologicalSpaceSubtype] (U ↓∩ s)),
    ∀ x ∈ s, ∃ (U : Set X), x ∈ U ∧ IsOpen[inst] U ∧ U ∩ closure[inst] s ⊆ s
h : ∀ x ∈ s, ∃ (U : Set X), x ∈ U ∧ IsOpen[inst] U ∧ U ∩ closure[inst] s ⊆ s
U : (x : X) → x ∈ s → Set X
hxU : ∀ (x : X) (a : x ∈ s), x ∈ U x a
hU : ∀ (x : X) (a : x ∈ s), IsOpen[inst] (U x a)
e : ∀ (x : X) (a : x ∈ s), U x a ∩ closure[inst] s ⊆ s
refine_1 :
  ∀ (x : { x : X // x ∈ closure[inst] s }),
    Membership.mem (γ := Set { x : X // x ∈ closure[inst] s })
        (Subtype.val (p := fun (x : X) ↦ x ∈ closure[inst] s) ⁻¹' ⋃ (x : X), ⋃ (h : x ∈ s), U x h) x →
      Membership.mem (γ := Set { x : X // x ∈ closure[inst] s }) (closure[inst] s ↓∩ s) x
refine_2 :
  ∀ (x : { x : X // x ∈ closure[inst] s }),
    Membership.mem (γ := Set { x : X // x ∈ closure[inst] s }) (closure[inst] s ↓∩ s) x →
      Membership.mem (γ := Set { x : X // x ∈ closure[inst] s })
        (Subtype.val (p := fun (x : X) ↦ x ∈ closure[inst] s) ⁻¹' ⋃ (x : X), ⋃ (h : x ∈ s), U x h) x
⊢ IsOpen[instTopologicalSpaceSubtype] (closure[inst] s ↓∩ s)

Tactic:
refine ⟨⋃ x ∈ s, U x ‹_›, isOpen_iUnion (isOpen_iUnion <| hU ·), ext fun x ↦ ⟨?_, ?_⟩⟩
-- Module: Mathlib.Topology.LocallyClosed
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
tfae_1_to_2 : ∀ (a : IsLocallyClosed s), IsOpen[inst] (coborder s)
tfae_2_to_3 : ∀ (a : IsOpen[inst] (coborder s)), ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsClosed[instTopologicalSpaceSubtype] (U ↓∩ s)
tfae_3_to_4 :
  ∀ (a : ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsClosed[instTopologicalSpaceSubtype] (U ↓∩ s)),
    ∀ x ∈ s, ∃ (U : Set X), x ∈ U ∧ IsOpen[inst] U ∧ U ∩ closure[inst] s ⊆ s
h : ∀ x ∈ s, ∃ (U : Set X), x ∈ U ∧ IsOpen[inst] U ∧ U ∩ closure[inst] s ⊆ s
U : (x : X) → x ∈ s → Set X
hxU_1 : ∀ (x : X) (a : x ∈ s), x ∈ U x a
hU : ∀ (x : X) (a : x ∈ s), IsOpen[inst] (U x a)
e : ∀ (x : X) (a : x ∈ s), U x a ∩ closure[inst] s ⊆ s
x : { x : X // x ∈ closure[inst] s }
y : X
hy : y ∈ s
hxU : Membership.mem (γ := Set X) ((fun (h : y ∈ s) ↦ U y h) hy) (↑x : X)
⊢ Membership.mem (γ := Set { x : X // x ∈ closure[inst] s }) (closure[inst] s ↓∩ s) x

Tactic:
e y hy ⟨hxU, x.2⟩

Premises used: Set.Mem, setOf, Set.preimage, And.intro, Subtype.property
-- Module: Mathlib.Topology.LocallyClosed
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
tfae_1_to_2 : ∀ (a : IsLocallyClosed s), IsOpen[inst] (coborder s)
tfae_2_to_3 : ∀ (a : IsOpen[inst] (coborder s)), ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsClosed[instTopologicalSpaceSubtype] (U ↓∩ s)
tfae_3_to_4 :
  ∀ (a : ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsClosed[instTopologicalSpaceSubtype] (U ↓∩ s)),
    ∀ x ∈ s, ∃ (U : Set X), x ∈ U ∧ IsOpen[inst] U ∧ U ∩ closure[inst] s ⊆ s
h : ∀ x ∈ s, ∃ (U : Set X), x ∈ U ∧ IsOpen[inst] U ∧ U ∩ closure[inst] s ⊆ s
U : (x : X) → x ∈ s → Set X
hxU_1 : ∀ (x : X) (a : x ∈ s), x ∈ U x a
hU : ∀ (x : X) (a : x ∈ s), IsOpen[inst] (U x a)
e : ∀ (x : X) (a : x ∈ s), U x a ∩ closure[inst] s ⊆ s
x : { x : X // x ∈ closure[inst] s }
y : X
hy : y ∈ s
hxU : Membership.mem (γ := Set X) ((fun (h : y ∈ s) ↦ U y h) hy) (↑x : X)
⊢ Membership.mem (γ := Set { x : X // x ∈ closure[inst] s }) (closure[inst] s ↓∩ s) x

Tactic:
exact e y hy ⟨hxU, x.2⟩

Premises used: And.intro, Subtype.property
-- Module: Mathlib.Topology.LocallyClosed
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
tfae_1_to_2 : ∀ (a : IsLocallyClosed s), IsOpen[inst] (coborder s)
tfae_2_to_3 : ∀ (a : IsOpen[inst] (coborder s)), ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsClosed[instTopologicalSpaceSubtype] (U ↓∩ s)
tfae_3_to_4 :
  ∀ (a : ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsClosed[instTopologicalSpaceSubtype] (U ↓∩ s)),
    ∀ x ∈ s, ∃ (U : Set X), x ∈ U ∧ IsOpen[inst] U ∧ U ∩ closure[inst] s ⊆ s
h : ∀ x ∈ s, ∃ (U : Set X), x ∈ U ∧ IsOpen[inst] U ∧ U ∩ closure[inst] s ⊆ s
U : (x : X) → x ∈ s → Set X
hxU : ∀ (x : X) (a : x ∈ s), x ∈ U x a
hU : ∀ (x : X) (a : x ∈ s), IsOpen[inst] (U x a)
e : ∀ (x : X) (a : x ∈ s), U x a ∩ closure[inst] s ⊆ s
x : { x : X // x ∈ closure[inst] s }
⊢ Membership.mem (γ := Set { x : X // x ∈ closure[inst] s }) (closure[inst] s ↓∩ s) x →
    Membership.mem (γ := Set { x : X // x ∈ closure[inst] s })
      (Subtype.val (p := fun (x : X) ↦ x ∈ closure[inst] s) ⁻¹' ⋃ (x : X), ⋃ (h : x ∈ s), U x h) x

Tactic:
(subset_iUnion₂ _ _ <| hxU x ·)

Premises used: Set.subset_iUnion₂, Set.Mem, iSup, setOf, Set.preimage, Subtype.val, Set.iUnion
-- Module: Mathlib.Topology.LocallyClosed
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
tfae_1_to_2 : ∀ (a : IsLocallyClosed s), IsOpen[inst] (coborder s)
tfae_2_to_3 : ∀ (a : IsOpen[inst] (coborder s)), ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsClosed[instTopologicalSpaceSubtype] (U ↓∩ s)
tfae_3_to_4 :
  ∀ (a : ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsClosed[instTopologicalSpaceSubtype] (U ↓∩ s)),
    ∀ x ∈ s, ∃ (U : Set X), x ∈ U ∧ IsOpen[inst] U ∧ U ∩ closure[inst] s ⊆ s
h : ∀ x ∈ s, ∃ (U : Set X), x ∈ U ∧ IsOpen[inst] U ∧ U ∩ closure[inst] s ⊆ s
U : (x : X) → x ∈ s → Set X
hxU : ∀ (x : X) (a : x ∈ s), x ∈ U x a
hU : ∀ (x : X) (a : x ∈ s), IsOpen[inst] (U x a)
e : ∀ (x : X) (a : x ∈ s), U x a ∩ closure[inst] s ⊆ s
x : { x : X // x ∈ closure[inst] s }
⊢ Membership.mem (γ := Set { x : X // x ∈ closure[inst] s }) (closure[inst] s ↓∩ s) x →
    Membership.mem (γ := Set { x : X // x ∈ closure[inst] s })
      (Subtype.val (p := fun (x : X) ↦ x ∈ closure[inst] s) ⁻¹' ⋃ (x : X), ⋃ (h : x ∈ s), U x h) x

Tactic:
exact (subset_iUnion₂ _ _ <| hxU x ·)

Premises used: Set.subset_iUnion₂, Subtype.val
-- Module: Mathlib.Topology.LocallyClosed
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
tfae_1_to_2 : ∀ (a : IsLocallyClosed s), IsOpen[inst] (coborder s)
tfae_2_to_3 : ∀ (a : IsOpen[inst] (coborder s)), ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsClosed[instTopologicalSpaceSubtype] (U ↓∩ s)
tfae_3_to_4 :
  ∀ (a : ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsClosed[instTopologicalSpaceSubtype] (U ↓∩ s)),
    ∀ x ∈ s, ∃ (U : Set X), x ∈ U ∧ IsOpen[inst] U ∧ U ∩ closure[inst] s ⊆ s
⊢ ∀ (a : ∀ x ∈ s, ∃ (U : Set X), x ∈ U ∧ IsOpen[inst] U ∧ U ∩ closure[inst] s ⊆ s),
    IsOpen[instTopologicalSpaceSubtype] (closure[inst] s ↓∩ s)

Tactic:
tfae_have 4 → 5
  | H => by
    choose U hxU hU e using H
    refine ⟨⋃ x ∈ s, U x ‹_›, isOpen_iUnion (isOpen_iUnion <| hU ·), ext fun x ↦ ⟨?_, ?_⟩⟩
    · rintro ⟨_, ⟨⟨y, rfl⟩, ⟨_, ⟨hy, rfl⟩, hxU⟩⟩⟩
      exact e y hy ⟨hxU, x.2⟩
    · exact (subset_iUnion₂ _ _ <| hxU x ·)
-- Module: Mathlib.Topology.LocallyClosed
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
tfae_1_to_2 : ∀ (a : IsLocallyClosed s), IsOpen[inst] (coborder s)
tfae_2_to_3 : ∀ (a : IsOpen[inst] (coborder s)), ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsClosed[instTopologicalSpaceSubtype] (U ↓∩ s)
tfae_3_to_4 :
  ∀ (a : ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsClosed[instTopologicalSpaceSubtype] (U ↓∩ s)),
    ∀ x ∈ s, ∃ (U : Set X), x ∈ U ∧ IsOpen[inst] U ∧ U ∩ closure[inst] s ⊆ s
tfae_4_to_5 :
  ∀ (a : ∀ x ∈ s, ∃ (U : Set X), x ∈ U ∧ IsOpen[inst] U ∧ U ∩ closure[inst] s ⊆ s),
    IsOpen[instTopologicalSpaceSubtype] (closure[inst] s ↓∩ s)
⊢ IsOpen[instTopologicalSpaceSubtype] (closure[inst] s ↓∩ s)

Tactic:
5

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Topology.LocallyClosed
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
tfae_1_to_2 : ∀ (a : IsLocallyClosed s), IsOpen[inst] (coborder s)
tfae_2_to_3 : ∀ (a : IsOpen[inst] (coborder s)), ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsClosed[instTopologicalSpaceSubtype] (U ↓∩ s)
tfae_3_to_4 :
  ∀ (a : ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsClosed[instTopologicalSpaceSubtype] (U ↓∩ s)),
    ∀ x ∈ s, ∃ (U : Set X), x ∈ U ∧ IsOpen[inst] U ∧ U ∩ closure[inst] s ⊆ s
tfae_4_to_5 :
  ∀ (a : ∀ x ∈ s, ∃ (U : Set X), x ∈ U ∧ IsOpen[inst] U ∧ U ∩ closure[inst] s ⊆ s),
    IsOpen[instTopologicalSpaceSubtype] (closure[inst] s ↓∩ s)
⊢ IsLocallyClosed s

Tactic:
1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Topology.LocallyClosed
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
tfae_1_to_2 : ∀ (a : IsLocallyClosed s), IsOpen[inst] (coborder s)
tfae_2_to_3 : ∀ (a : IsOpen[inst] (coborder s)), ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsClosed[instTopologicalSpaceSubtype] (U ↓∩ s)
tfae_3_to_4 :
  ∀ (a : ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsClosed[instTopologicalSpaceSubtype] (U ↓∩ s)),
    ∀ x ∈ s, ∃ (U : Set X), x ∈ U ∧ IsOpen[inst] U ∧ U ∩ closure[inst] s ⊆ s
tfae_4_to_5 :
  ∀ (a : ∀ x ∈ s, ∃ (U : Set X), x ∈ U ∧ IsOpen[inst] U ∧ U ∩ closure[inst] s ⊆ s),
    IsOpen[instTopologicalSpaceSubtype] (closure[inst] s ↓∩ s)
⊢ ∀ (a : IsOpen[instTopologicalSpaceSubtype] (closure[inst] s ↓∩ s)), IsLocallyClosed s

Tactic:
5 → 1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Topology.LocallyClosed
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
tfae_1_to_2 : ∀ (a : IsLocallyClosed s), IsOpen[inst] (coborder s)
tfae_2_to_3 : ∀ (a : IsOpen[inst] (coborder s)), ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsClosed[instTopologicalSpaceSubtype] (U ↓∩ s)
tfae_3_to_4 :
  ∀ (a : ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsClosed[instTopologicalSpaceSubtype] (U ↓∩ s)),
    ∀ x ∈ s, ∃ (U : Set X), x ∈ U ∧ IsOpen[inst] U ∧ U ∩ closure[inst] s ⊆ s
tfae_4_to_5 :
  ∀ (a : ∀ x ∈ s, ∃ (U : Set X), x ∈ U ∧ IsOpen[inst] U ∧ U ∩ closure[inst] s ⊆ s),
    IsOpen[instTopologicalSpaceSubtype] (closure[inst] s ↓∩ s)
h : IsOpen[instTopologicalSpaceSubtype] (closure[inst] s ↓∩ s)
H : IsOpen[instTopologicalSpaceSubtype] (closure[inst] s ↓∩ s) := h
⊢ IsLocallyClosed.{u_1} (X := X)
    (range (ι := (↑(closure[inst] s) : Type u_1)) (Subtype.val (p := fun (x : X) ↦ x ∈ closure[inst] s)))

Tactic:
simpa using isClosed_closure.isLocallyClosed

Premises used: IsClosed.isLocallyClosed, isClosed_closure
-- Module: Mathlib.Topology.LocallyClosed
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
tfae_1_to_2 : ∀ (a : IsLocallyClosed s), IsOpen[inst] (coborder s)
tfae_2_to_3 : ∀ (a : IsOpen[inst] (coborder s)), ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsClosed[instTopologicalSpaceSubtype] (U ↓∩ s)
tfae_3_to_4 :
  ∀ (a : ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsClosed[instTopologicalSpaceSubtype] (U ↓∩ s)),
    ∀ x ∈ s, ∃ (U : Set X), x ∈ U ∧ IsOpen[inst] U ∧ U ∩ closure[inst] s ⊆ s
tfae_4_to_5 :
  ∀ (a : ∀ x ∈ s, ∃ (U : Set X), x ∈ U ∧ IsOpen[inst] U ∧ U ∩ closure[inst] s ⊆ s),
    IsOpen[instTopologicalSpaceSubtype] (closure[inst] s ↓∩ s)
h_1 : IsOpen[instTopologicalSpaceSubtype] (closure[inst] s ↓∩ s)
H : IsOpen[instTopologicalSpaceSubtype] (closure[inst] s ↓∩ s) := h_1
h : s = ↑(closure[inst] s ↓∩ s)
⊢ IsLocallyClosed s

Tactic:
convert!
      H.isLocallyClosed.image IsInducing.subtypeVal
        (by simpa using isClosed_closure.isLocallyClosed)

Premises used: IsLocallyClosed.image, IsOpen.isLocallyClosed, Topology.IsInducing.subtypeVal
-- Module: Mathlib.Topology.LocallyClosed
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
tfae_1_to_2 : ∀ (a : IsLocallyClosed s), IsOpen[inst] (coborder s)
tfae_2_to_3 : ∀ (a : IsOpen[inst] (coborder s)), ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsClosed[instTopologicalSpaceSubtype] (U ↓∩ s)
tfae_3_to_4 :
  ∀ (a : ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsClosed[instTopologicalSpaceSubtype] (U ↓∩ s)),
    ∀ x ∈ s, ∃ (U : Set X), x ∈ U ∧ IsOpen[inst] U ∧ U ∩ closure[inst] s ⊆ s
tfae_4_to_5 :
  ∀ (a : ∀ x ∈ s, ∃ (U : Set X), x ∈ U ∧ IsOpen[inst] U ∧ U ∩ closure[inst] s ⊆ s),
    IsOpen[instTopologicalSpaceSubtype] (closure[inst] s ↓∩ s)
h : IsOpen[instTopologicalSpaceSubtype] (closure[inst] s ↓∩ s)
H : IsOpen[instTopologicalSpaceSubtype] (closure[inst] s ↓∩ s) := h
⊢ s = ↑(closure[inst] s ↓∩ s)

Tactic:
simpa using subset_closure

Premises used: subset_closure
-- Module: Mathlib.Topology.LocallyClosed
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
tfae_1_to_2 : ∀ (a : IsLocallyClosed s), IsOpen[inst] (coborder s)
tfae_2_to_3 : ∀ (a : IsOpen[inst] (coborder s)), ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsClosed[instTopologicalSpaceSubtype] (U ↓∩ s)
tfae_3_to_4 :
  ∀ (a : ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsClosed[instTopologicalSpaceSubtype] (U ↓∩ s)),
    ∀ x ∈ s, ∃ (U : Set X), x ∈ U ∧ IsOpen[inst] U ∧ U ∩ closure[inst] s ⊆ s
tfae_4_to_5 :
  ∀ (a : ∀ x ∈ s, ∃ (U : Set X), x ∈ U ∧ IsOpen[inst] U ∧ U ∩ closure[inst] s ⊆ s),
    IsOpen[instTopologicalSpaceSubtype] (closure[inst] s ↓∩ s)
⊢ ∀ (a : IsOpen[instTopologicalSpaceSubtype] (closure[inst] s ↓∩ s)), IsLocallyClosed s

Tactic:
tfae_have 5 → 1
  | H => by
    convert!
      H.isLocallyClosed.image IsInducing.subtypeVal
        (by simpa using isClosed_closure.isLocallyClosed)
    simpa using subset_closure
-- Module: Mathlib.Topology.LocallyClosed
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
tfae_1_to_2 : ∀ (a : IsLocallyClosed s), IsOpen[inst] (coborder s)
tfae_2_to_3 : ∀ (a : IsOpen[inst] (coborder s)), ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsClosed[instTopologicalSpaceSubtype] (U ↓∩ s)
tfae_3_to_4 :
  ∀ (a : ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsClosed[instTopologicalSpaceSubtype] (U ↓∩ s)),
    ∀ x ∈ s, ∃ (U : Set X), x ∈ U ∧ IsOpen[inst] U ∧ U ∩ closure[inst] s ⊆ s
tfae_4_to_5 :
  ∀ (a : ∀ x ∈ s, ∃ (U : Set X), x ∈ U ∧ IsOpen[inst] U ∧ U ∩ closure[inst] s ⊆ s),
    IsOpen[instTopologicalSpaceSubtype] (closure[inst] s ↓∩ s)
tfae_5_to_1 : ∀ (a : IsOpen[instTopologicalSpaceSubtype] (closure[inst] s ↓∩ s)), IsLocallyClosed s
⊢ [IsLocallyClosed s, IsOpen[inst] (coborder s), ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsClosed[instTopologicalSpaceSubtype] (U ↓∩ s),
      ∀ x ∈ s, ∃ (U : Set X), x ∈ U ∧ IsOpen[inst] U ∧ U ∩ closure[inst] s ⊆ s,
      IsOpen[instTopologicalSpaceSubtype] (closure[inst] s ↓∩ s)].TFAE

Tactic:
tfae_finish
-- Module: Mathlib.Topology.LocallyClosed
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
⊢ IsLocallyClosed s ↔ IsOpen[inst] (coborder s)

Tactic:
(isLocallyClosed_tfae s).out 0 1

Premises used: List.TFAE.out, isLocallyClosed_tfae, OfNat.ofNat
-- Module: Mathlib.Topology.LocallyClosed
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
hs : IsLocallyClosed s
⊢ IsOpen[instTopologicalSpaceSubtype] (closure[inst] s ↓∩ s)

Tactic:
((isLocallyClosed_tfae s).out 0 4).mp hs

Premises used: List.TFAE.out, isLocallyClosed_tfae, Iff.mp, OfNat.ofNat
-- Module: Mathlib.Topology.LocallyConstant.Algebra
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : One Y
⊢ Eq (α := (a : X) → Y) (⇑1 : (a : X) → Y) 1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.LocallyConstant.Algebra
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : One Y
x : X
⊢ Eq.{u_2 + 1} (α := Y) ((1 : (a : X) → Y) x : Y) (1 : Y)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.LocallyConstant.Algebra
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : Inv Y
f : LocallyConstant X Y
⊢ Eq (α := (a : X) → Y) (⇑f⁻¹ : (a : X) → Y) (⇑f : (a : X) → Y)⁻¹

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.LocallyConstant.Algebra
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : Inv Y
f : LocallyConstant X Y
x : X
⊢ Eq.{u_2 + 1} (α := Y) ((f⁻¹ : (a : X) → Y) x : Y) (((f : (a : X) → Y) x)⁻¹ : Y)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.LocallyConstant.Algebra
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : Mul Y
f g : LocallyConstant X Y
⊢ (⇑(f * g) : (a : X) → Y) = HMul.hMul (α := (a : X) → Y) (⇑f : (a : X) → Y) (⇑g : (a : X) → Y)

Tactic:
rfl

Premises used: rfl