awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
s t : Set X
⊢ closure (s ∪ t) = closure s ∪ closure t

Tactic:
simp [closure_eq_compl_interior_compl, compl_inter]

Premises used: Set.compl_inter, closure_eq_compl_interior_compl
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
ι : Type u_1
s : Set ι
hs : s.Finite
f : ι → Set X
⊢ Eq.{u + 1} (α := Set X) (closure (⋃ i ∈ s, f i)) (⋃ i ∈ s, closure (f i))

Tactic:
simp [closure_eq_compl_interior_compl, hs.interior_biInter]

Premises used: Set.Finite.interior_biInter, closure_eq_compl_interior_compl
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
S : Set (Set X)
hS : S.Finite
rw : Eq.{u + 1} (α := Set X) (closure (⋃ i ∈ S, i)) (⋃ s ∈ S, closure s)
rw₁ rw₂ : Eq.{u + 1} (α := Set X) (⋃ i ∈ S, closure i) (⋃ s ∈ S, closure s)
⊢ closure (⋃₀ S) = ⋃ s ∈ S, closure s

Tactic:
rw [sUnion_eq_biUnion, hS.closure_biUnion]

Premises used: Set.Finite.closure_biUnion, Set.sUnion_eq_biUnion
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
ι : Type u_1
s : Finset ι
f : ι → Set X
⊢ Eq.{u + 1} (α := Set X) (closure (⋃ i ∈ s, f i)) (⋃ i ∈ s, closure (f i))

Tactic:
s.finite_toSet.closure_biUnion f

Premises used: Set.Finite.closure_biUnion, Finset.finite_toSet
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
ι : Sort v
inst_1 : Finite ι
f : ι → Set X
rw : closure (⋃₀ range f) = ⋃ (i : ι), closure (f i)
rw₁ : Eq.{u + 1} (α := Set X) (⋃ s ∈ range f, closure s) (⋃ (i : ι), closure (f i))
rw₂ rw₃ : Eq.{u + 1} (α := Set X) (⋃ (y : ι), closure (f y)) (⋃ (i : ι), closure (f i))
⊢ Eq.{u + 1} (α := Set X) (closure (⋃ (i : ι), f i)) (⋃ (i : ι), closure (f i))

Tactic:
rw [← sUnion_range, (finite_range _).closure_sUnion, biUnion_range]

Premises used: Set.sUnion_range, Set.biUnion_range, Set.finite_range, Set.Finite.closure_sUnion
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
n : ℕ
f : ℕ → Set X
⊢ Eq.{u + 1} (α := Set X) (closure (⋃ (m : ℕ), ⋃ (_ : m < n), f m)) (⋃ (m : ℕ), ⋃ (_ : m < n), closure (f m))

Tactic:
(finite_lt_nat n).closure_biUnion f

Premises used: Set.Mem, Set.Finite.closure_biUnion, Set.finite_lt_nat, Nat.lt
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
n : ℕ
f : ℕ → Set X
⊢ Eq.{u + 1} (α := Set X) (closure (⋃ (m : ℕ), ⋃ (_ : m ≤ n), f m)) (⋃ (m : ℕ), ⋃ (_ : m ≤ n), closure (f m))

Tactic:
(finite_le_nat n).closure_biUnion f

Premises used: Set.Mem, setOf, Set.Finite.closure_biUnion, Set.finite_le_nat
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
s t : Set X
⊢ closure t ⊆ closure (s ∩ t) ∪ closure sᶜ

Tactic:
(closure_mono <| subset_inter_union_compl_left ..).trans_eq closure_union

Premises used: LE.le.trans_eq, closure_mono, closure_union, Set.subset_inter_union_compl_left
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
s t : Set X
⊢ closure s ⊆ closure (s ∩ t) ∪ closure tᶜ

Tactic:
(closure_mono <| subset_inter_union_compl_right ..).trans_eq closure_union

Premises used: LE.le.trans_eq, closure_mono, closure_union, Set.subset_inter_union_compl_right
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
⊢ interior s ⊆ closure s

Tactic:
Subset.trans interior_subset subset_closure

Premises used: interior_subset, Set.Subset.trans, subset_closure
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
⊢ interior sᶜ = (closure s)ᶜ

Tactic:
simp [closure_eq_compl_interior_compl]

Premises used: closure_eq_compl_interior_compl
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
⊢ closure sᶜ = (interior s)ᶜ

Tactic:
simp [closure_eq_compl_interior_compl]

Premises used: closure_eq_compl_interior_compl
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
⊢ interior s = (closure sᶜ)ᶜ

Tactic:
simp
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
s t : Set X
h : Disjoint (closure s) (closure t)
⊢ interior sᶜ ∪ interior tᶜ = univ

Tactic:
simpa [disjoint_iff, ← compl_inter] using h

Premises used: disjoint_iff, Set.compl_inter
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
s t : Set X
h : Disjoint (closure s) (closure t)
⊢ interior sᶜ ∪ interior tᶜ = univ

Tactic:
have full : interior sᶜ ∪ interior tᶜ = univ := by simpa [disjoint_iff, ← compl_inter] using h
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
s t : Set X
h : Disjoint (closure s) (closure t)
full : interior sᶜ ∪ interior tᶜ = univ
⊢ interior (s ∪ t) = interior s ∪ interior t

Tactic:
subset_antisymm ?_ subset_interior_union

Premises used: subset_antisymm, subset_interior_union
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
s t : Set X
h : Disjoint (closure s) (closure t)
full : interior sᶜ ∪ interior tᶜ = univ
refine : interior (s ∪ t) ⊆ interior s ∪ interior t
⊢ interior (s ∪ t) = interior s ∪ interior t

Tactic:
refine subset_antisymm ?_ subset_interior_union

Premises used: subset_antisymm, subset_interior_union
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
s t : Set X
h : Disjoint (closure s) (closure t)
full : interior sᶜ ∪ interior tᶜ = univ
rw : interior (s ∪ t) ∩ interior sᶜ ∪ interior (s ∪ t) ∩ interior tᶜ ⊆ interior s ∪ interior t
⊢ interior (s ∪ t) ⊆ interior s ∪ interior t

Tactic:
rw [← (interior _).inter_univ, ← full, inter_union_distrib_left]

Premises used: Set.inter_univ, interior, Set.inter_union_distrib_left
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
s t : Set X
h : Disjoint (closure s) (closure t)
full : interior sᶜ ∪ interior tᶜ = univ
⊢ interior (s ∪ t) ∩ interior sᶜ ∪ interior (s ∪ t) ∩ interior tᶜ ⊆ interior s ∪ interior t

Tactic:
union_subset
    (interior_union_inter_interior_compl_left_subset.trans subset_union_right)
    (interior_union_inter_interior_compl_right_subset.trans subset_union_left)

Premises used: Set.subset_union_right, HasSubset.Subset.trans, Set.union_subset, Set.subset_union_left, interior_union_inter_interior_compl_left_subset, interior_union_inter_interior_compl_right_subset
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
s t : Set X
h : Disjoint (closure s) (closure t)
full : interior sᶜ ∪ interior tᶜ = univ
⊢ interior (s ∪ t) ∩ interior sᶜ ∪ interior (s ∪ t) ∩ interior tᶜ ⊆ interior s ∪ interior t

Tactic:
exact union_subset
    (interior_union_inter_interior_compl_left_subset.trans subset_union_right)
    (interior_union_inter_interior_compl_right_subset.trans subset_union_left)

Premises used: Set.subset_union_right, HasSubset.Subset.trans, Set.union_subset, Set.subset_union_left, interior_union_inter_interior_compl_left_subset, interior_union_inter_interior_compl_right_subset
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
s t : Set X
h : Codisjoint (interior s) (interior t)
rw : (closure (s ∩ t))ᶜ = (closure s ∩ closure t)ᶜ
⊢ closure (s ∩ t) = closure s ∩ closure t

Tactic:
rw [← compl_inj_iff]

Premises used: compl_inj_iff
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
s t : Set X
h : Codisjoint (interior s) (interior t)
simp : interior (sᶜ ∪ tᶜ) = interior sᶜ ∪ interior tᶜ
⊢ (closure (s ∩ t))ᶜ = (closure s ∩ closure t)ᶜ

Tactic:
simp only [← interior_compl, compl_inter]

Premises used: Set.compl_inter, interior_compl
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
s t : Set X
h : Codisjoint (interior s) (interior t)
h₁ : Disjoint (closure sᶜ) (closure tᶜ)
⊢ interior (sᶜ ∪ tᶜ) = interior sᶜ ∪ interior tᶜ

Tactic:
apply interior_union_of_disjoint_closure

Premises used: interior_union_of_disjoint_closure
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
s t : Set X
h : Codisjoint (interior s) (interior t)
⊢ Disjoint (closure sᶜ) (closure tᶜ)

Tactic:
simpa only [closure_compl, disjoint_compl_left_iff, ← codisjoint_iff_compl_le_left]

Premises used: codisjoint_iff_compl_le_left, disjoint_compl_left_iff, closure_compl
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
x : X
s : Set X
⊢ x ∈ closure s ↔ ∀ (o : Set X), IsOpen o → x ∈ o → (o ∩ s).Nonempty

Tactic:
⟨fun h o oo ao =>
    by_contradiction fun os =>
      have : s ⊆ oᶜ := fun x xs xo => os ⟨x, xo, xs⟩
      closure_minimal this (isClosed_compl_iff.2 oo) h ao,
    fun H _ ⟨h₁, h₂⟩ =>
    by_contradiction fun nc =>
      let ⟨_, hc, hs⟩ := H _ h₁.isOpen_compl nc
      hc (h₂ hs)⟩

Premises used: Iff.mpr, False, IsClosed.isOpen_compl, closure_minimal, Compl.compl, Membership.mem, _private.0.mem_closure_iff.match_2, And.intro, Iff.intro, by_contradiction, Exists.intro, _private.0.mem_closure_iff.match_1, isClosed_compl_iff
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
s t : Set X
h : IsOpen t
⊢ (closure s ∩ t).Nonempty ↔ (s ∩ t).Nonempty

Tactic:
⟨fun ⟨_x, hxcs, hxt⟩ => inter_comm t s ▸ mem_closure_iff.1 hxcs t h hxt, fun h =>
    h.mono <| inf_le_inf_right t subset_closure⟩

Premises used: mem_closure_iff, subset_closure, Eq.rec, inf_le_inf_right, Set.Nonempty.mono, Inter.inter, Set.inter_comm, Set.Nonempty, _private.0.closure_inter_open_nonempty_iff.match_1, Iff.intro, Iff.mp
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
l : Filter X
⊢ l ≤ l.lift' closure

Tactic:
le_lift'.2 fun _ h => mem_of_superset h subset_closure

Premises used: Iff.mpr, subset_closure, Filter.le_lift', Filter.mem_of_superset
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
ι : Sort v
l : Filter X
p : ι → Prop
s : ι → Set X
h : l.HasBasis p s
⊢ (l.lift' closure).HasBasis p fun (i : ι) ↦ closure (s i)

Tactic:
h.lift' (monotone_closure X)

Premises used: closure, Filter.HasBasis.lift', Set.sInter, monotone_closure
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
ι : Sort v
l : Filter X
p : ι → Prop
s : ι → Set X
h : l.HasBasis p s
hc : ∀ (i : ι), p i → IsClosed (s i)
⊢ l.lift' closure = l

Tactic:
le_antisymm (h.ge_iff.2 fun i hi => (hc i hi).closure_eq ▸ mem_lift' (h.mem_of_mem hi))
    l.le_lift'_closure

Premises used: Iff.mpr, IsClosed.closure_eq, Eq.rec, Filter.mem_lift', Filter.HasBasis.ge_iff, le_antisymm, Filter.le_lift'_closure, Filter.HasBasis.mem_of_mem
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
l : Filter X
h : l = ⊥
rw : Eq.{u + 1} (α := Filter X) (𝓟 (closure ∅)) ⊥
rw₁ : Eq.{u + 1} (α := Filter X) (𝓟 ∅) ⊥
rw₂ rw₃ : Eq.{u + 1} (α := Filter X) ⊥ ⊥
⊢ Eq.{u + 1} (α := Filter X) (Filter.lift' ⊥ closure) ⊥

Tactic:
rw [lift'_bot (monotone_closure _), closure_empty, principal_empty]

Premises used: Filter.lift'_bot, Filter.principal_empty, closure_empty, monotone_closure
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
⊢ Dense s ↔ closure s = univ

Tactic:
eq_univ_iff_forall.symm

Premises used: Set.eq_univ_iff_forall, Dense, Iff.symm
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
rw : interior s = ∅ ↔ closure sᶜ = univ
rw₁ : interior s = ∅ ↔ (interior s)ᶜ = univ
rw₂ rw₃ : interior s = ∅ ↔ interior s = ∅
⊢ interior s = ∅ ↔ Dense sᶜ

Tactic:
rw [dense_iff_closure_eq, closure_compl, compl_univ_iff]

Premises used: dense_iff_closure_eq, closure_compl, Set.compl_univ_iff
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
h rwa rwa₁ rwa₂ rwa₃ : Dense s
⊢ Dense sᶜᶜ

Tactic:
rwa [compl_compl]

Premises used: compl_compl
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
rw : (∀ (x : X), x ∈ closure (closure s)) ↔ Dense s
rw₁ : (∀ (x : X), x ∈ closure (closure s)) ↔ ∀ (x : X), x ∈ closure s
rw₂ rw₃ : (∀ (x : X), x ∈ closure s) ↔ ∀ (x : X), x ∈ closure s
⊢ Dense (closure s) ↔ Dense s

Tactic:
rw [Dense, Dense, closure_closure]

Premises used: Dense, closure_closure
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
⊢ Dense.{u} (X := X) univ

Tactic:
fun _ => subset_closure trivial

Premises used: trivial, subset_closure, Dense
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
mp : Dense s → ∀ (U : Set X), IsOpen U → U.Nonempty → (U ∩ s).Nonempty
mpr : (∀ (U : Set X), IsOpen U → U.Nonempty → (U ∩ s).Nonempty) → Dense s
⊢ Dense s ↔ ∀ (U : Set X), IsOpen U → U.Nonempty → (U ∩ s).Nonempty

Tactic:
constructor
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
h : Dense s
U : Set X
U_op : IsOpen U
x : X
x_in : x ∈ U
⊢ (U ∩ s).Nonempty

Tactic:
mem_closure_iff.1 (h _) U U_op x_in

Premises used: mem_closure_iff, Iff.mp
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
h : Dense s
U : Set X
U_op : IsOpen U
x : X
x_in : x ∈ U
⊢ (U ∩ s).Nonempty

Tactic:
exact mem_closure_iff.1 (h _) U U_op x_in

Premises used: mem_closure_iff, Iff.mp
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
h : ∀ (U : Set X), IsOpen U → U.Nonempty → (U ∩ s).Nonempty
x : X
mpr : ∀ (o : Set X), IsOpen o → x ∈ o → (o ∩ s).Nonempty
⊢ x ∈ closure s

Tactic:
rw [mem_closure_iff]

Premises used: mem_closure_iff
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
h : ∀ (U : Set X), IsOpen U → U.Nonempty → (U ∩ s).Nonempty
x : X
U : Set X
U_op : IsOpen U
x_in : x ∈ U
⊢ (U ∩ s).Nonempty

Tactic:
h U U_op ⟨_, x_in⟩

Premises used: Exists.intro
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
h : ∀ (U : Set X), IsOpen U → U.Nonempty → (U ∩ s).Nonempty
x : X
U : Set X
U_op : IsOpen U
x_in : x ∈ U
⊢ (U ∩ s).Nonempty

Tactic:
exact h U U_op ⟨_, x_in⟩

Premises used: Exists.intro
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : Dense s
U : Set X
ho : IsOpen U
hne : U.Nonempty
⊢ ∃ x ∈ s, x ∈ U

Tactic:
let ⟨x, hx⟩ := hs.inter_open_nonempty U ho hne
  ⟨x, hx.2, hx.1⟩

Premises used: _private.0.Dense.exists_mem_open.match_1, Membership.mem, Exists, Dense.inter_open_nonempty, And, And.right, And.left, And.intro, Exists.intro
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : Dense s
⊢ s.Nonempty ↔ Nonempty X

Tactic:
⟨fun ⟨x, _⟩ => ⟨x⟩, fun ⟨x⟩ =>
    let ⟨y, hy⟩ := hs.inter_open_nonempty _ isOpen_univ ⟨x, trivial⟩
    ⟨y, hy.2⟩⟩

Premises used: trivial, Set.univ, _private.0.Dense.nonempty_iff.match_2, _private.0.Dense.nonempty_iff.match_1, _private.0.Dense.nonempty_iff.match_3, Nonempty.intro, isOpen_univ, Dense.inter_open_nonempty, Set.Nonempty, And.right, Iff.intro, Exists.intro, Nonempty
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
h : Nonempty X
hs : Dense s
⊢ s.Nonempty

Tactic:
hs.nonempty_iff.2 h

Premises used: Iff.mpr, Dense.nonempty_iff
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
s₁ s₂ : Set X
h : s₁ ⊆ s₂
hd : Dense s₁
⊢ Dense s₂

Tactic:
fun x =>
  closure_mono h (hd x)

Premises used: Dense, closure_mono
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
α : Type u_1
β : Type u_2
f : α → X
g : β → α
h : DenseRange (f ∘ g)
⊢ DenseRange f

Tactic:
Dense.mono (range_comp_subset_range g f) h

Premises used: Set.range_comp_subset_range, Dense.mono, DenseRange
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
x : X
mp : Dense (X := X) {x}ᶜ → ¬IsOpen (X := X) {x}
mpr : ¬IsOpen (X := X) {x} → Dense (X := X) {x}ᶜ
⊢ Dense (X := X) {x}ᶜ ↔ ¬IsOpen (X := X) {x}

Tactic:
constructor
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
x : X
hd : Dense (X := X) {x}ᶜ
ho : IsOpen (X := X) {x}
⊢ False

Tactic:
(hd.inter_open_nonempty _ ho (singleton_nonempty _)).ne_empty (inter_compl_self _)

Premises used: Set.singleton_nonempty, Set.Nonempty.ne_empty, Dense.inter_open_nonempty, Set.inter_compl_self
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
x : X
hd : Dense (X := X) {x}ᶜ
ho : IsOpen (X := X) {x}
⊢ False

Tactic:
exact (hd.inter_open_nonempty _ ho (singleton_nonempty _)).ne_empty (inter_compl_self _)

Premises used: Set.singleton_nonempty, Set.Nonempty.ne_empty, Dense.inter_open_nonempty, Set.inter_compl_self
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
x : X
⊢ ¬IsOpen (X := X) {x} → Dense (X := X) {x}ᶜ

Tactic:
fun ho => dense_iff_inter_open.2 fun U hU hne => inter_compl_nonempty_iff.2 fun hUx => ?_

Premises used: Iff.mpr, dense_iff_inter_open, Set.inter_compl_nonempty_iff
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
x : X
mpr : ∀ (ho : ¬IsOpen (X := X) {x}) (U : Set X) (hU : IsOpen U) (hne : U.Nonempty) (hUx : U ⊆ {x}), False
⊢ ¬IsOpen (X := X) {x} → Dense (X := X) {x}ᶜ

Tactic:
refine fun ho => dense_iff_inter_open.2 fun U hU hne => inter_compl_nonempty_iff.2 fun hUx => ?_

Premises used: Iff.mpr, dense_iff_inter_open, Set.inter_compl_nonempty_iff
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
x : X
ho : ¬IsOpen (X := X) {x}
U : Set X
hU : IsOpen U
hne : U.Nonempty
hUx : U ⊆ {x}
⊢ U = {x}

Tactic:
eq_singleton_iff_nonempty_unique_mem.2 ⟨hne, hUx⟩

Premises used: Iff.mpr, Set.eq_singleton_iff_nonempty_unique_mem, And.intro
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
x : X
ho : ¬IsOpen (X := X) {x}
U : Set X
hU : IsOpen U
hne : U.Nonempty
hUx : U ⊆ {x}
⊢ IsOpen (X := X) {x}

Tactic:
obtain rfl : U = {x} := eq_singleton_iff_nonempty_unique_mem.2 ⟨hne, hUx⟩

Premises used: Iff.mpr, Set.eq_singleton_iff_nonempty_unique_mem, And.intro, rfl
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
x : X
ho : ¬IsOpen (X := X) {x}
U : Set X
hU : IsOpen U
hne : U.Nonempty
hUx : U ⊆ {x}
hU₁ : IsOpen (X := X) {x}
⊢ Set.Nonempty (α := X) {x}

Tactic:
obtain rfl : U = {x} := eq_singleton_iff_nonempty_unique_mem.2 ⟨hne, hUx⟩

Premises used: Iff.mpr, Set.eq_singleton_iff_nonempty_unique_mem, And.intro, rfl
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
x : X
ho : ¬IsOpen (X := X) {x}
U : Set X
hU : IsOpen U
hne : U.Nonempty
hUx : U ⊆ {x}
hU₁ : IsOpen (X := X) {x}
hne₁ : Set.Nonempty (α := X) {x}
⊢ Subset (α := Set X) {x} {x}

Tactic:
obtain rfl : U = {x} := eq_singleton_iff_nonempty_unique_mem.2 ⟨hne, hUx⟩

Premises used: Iff.mpr, Set.eq_singleton_iff_nonempty_unique_mem, And.intro, rfl
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
x : X
ho : ¬IsOpen (X := X) {x}
hU : IsOpen (X := X) {x}
hne : Set.Nonempty (α := X) {x}
hUx : Subset (α := Set X) {x} {x}
⊢ False

Tactic:
ho hU
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
x : X
ho : ¬IsOpen (X := X) {x}
hU : IsOpen (X := X) {x}
hne : Set.Nonempty (α := X) {x}
hUx : Subset (α := Set X) {x} {x}
⊢ False

Tactic:
exact ho hU
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : Dense s
P : X → Prop
mem : ∀ x ∈ s, P x
isClosed : IsClosed.{u} (X := X) {x : X | P x}
x : X
⊢ P x

Tactic:
hs.closure_eq.symm.subset.trans (isClosed.closure_subset_iff.mpr mem) (Set.mem_univ _)

Premises used: Iff.mpr, Set.Mem, setOf, HasSubset.Subset.trans, Dense.closure_eq, Eq.subset, IsClosed.closure_subset_iff, Set.mem_univ, Eq.symm
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
s_open : IsOpen s
⊢ s ⊆ interior (closure s)

Tactic:
s_open.subset_interior_iff.mpr subset_closure

Premises used: Iff.mpr, subset_closure, IsOpen.subset_interior_iff
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
s_closed : IsClosed s
⊢ closure (interior s) ⊆ s

Tactic:
s_closed.closure_subset_iff.mpr interior_subset

Premises used: Iff.mpr, interior_subset, IsClosed.closure_subset_iff
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
⊢ closure (interior (closure (interior s))) = closure (interior s)

Tactic:
isClosed_closure.closure_interior_subset.antisymm
    (closure_mono isOpen_interior.subset_interior_closure)

Premises used: isOpen_interior, closure_mono, IsOpen.subset_interior_closure, HasSubset.Subset.antisymm, IsClosed.closure_interior_subset, isClosed_closure
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
⊢ interior (closure (interior (closure s))) = interior (closure s)

Tactic:
(interior_mono isClosed_closure.closure_interior_subset).antisymm
    isOpen_interior.subset_interior_closure

Premises used: interior_mono, isOpen_interior, IsOpen.subset_interior_closure, HasSubset.Subset.antisymm, IsClosed.closure_interior_subset, isClosed_closure
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
⊢ closure s \ interior s = frontier s

Tactic:
rfl

Premises used: frontier, rfl
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
rw : interior s ∩ frontier s = ∅
rw₁ : interior s ∩ (closure s \ interior s) = ∅
rw₂ : interior s ∩ (closure s ∩ (interior s)ᶜ) = ∅
rw₃ : interior s ∩ closure s ∩ (interior s)ᶜ = ∅
rw₄ : (interior s)ᶜ ∩ (interior s ∩ closure s) = ∅
rw₅ : (interior s)ᶜ ∩ interior s ∩ closure s = ∅
rw₆ : ∅ ∩ closure s = ∅
rw₇ rw₈ : Eq.{u + 1} (α := Set X) ∅ ∅
⊢ Disjoint (interior s) (frontier s)

Tactic:
rw [disjoint_iff_inter_eq_empty, ← closure_diff_interior, diff_eq,
    ← inter_assoc, inter_comm, ← inter_assoc, compl_inter_self, empty_inter]

Premises used: Set.empty_inter, Set.diff_eq, Set.disjoint_iff_inter_eq_empty, Set.inter_comm, Set.compl_inter_self, closure_diff_interior, Set.inter_assoc
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
rw : closure s \ (closure s \ interior s) = interior s
rw₁ : closure s ∩ interior s = interior s
rw₂ rw₃ : interior s = interior s
⊢ closure s \ frontier s = interior s

Tactic:
rw [frontier, diff_diff_right_self, inter_eq_self_of_subset_right interior_subset_closure]

Premises used: frontier, Set.diff_diff_right_self, Set.inter_eq_self_of_subset_right, interior_subset_closure
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
rw : s \ (closure s \ interior s) = interior s
rw₁ : s \ closure s ∪ s ∩ interior s = interior s
rw₂ : ∅ ∪ s ∩ interior s = interior s
rw₃ : ∅ ∪ interior s = interior s
rw₄ rw₅ : interior s = interior s
⊢ s \ frontier s = interior s

Tactic:
rw [frontier, diff_diff_right, diff_eq_empty.2 subset_closure,
    inter_eq_self_of_subset_right interior_subset, empty_union]

Premises used: Iff.mpr, frontier, interior_subset, subset_closure, Set.empty_union, Set.inter_eq_self_of_subset_right, Set.diff_diff_right, Set.diff_eq_empty
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
x : X
hx : x ∈ s
⊢ x ∈ interior s ↔ x ∉ frontier s

Tactic:
simp [← self_diff_frontier, hx]

Premises used: self_diff_frontier
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
x : X
hx : x ∈ s
⊢ x ∈ frontier s ↔ x ∉ interior s

Tactic:
simp [← self_diff_frontier, hx]

Premises used: self_diff_frontier
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
rw : frontier s = closure s ∩ (interior s)ᶜ
rw₁ : closure s \ interior s = closure s ∩ (interior s)ᶜ
rw₂ rw₃ : closure s ∩ (interior s)ᶜ = closure s ∩ (interior s)ᶜ
⊢ frontier s = closure s ∩ closure sᶜ

Tactic:
rw [closure_compl, frontier, diff_eq]

Premises used: frontier, Set.diff_eq, closure_compl
-- Module: Mathlib.Topology.Closure
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
⊢ frontier s ⊆ closure s

Tactic:
diff_subset

Premises used: frontier, Set.diff_subset