awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Closure (goal)
Goal:
X : Type u
inst : TopologicalSpace X
ι : Sort v
inst_1 : Finite ι
f : ι → Set X
rw : interior (⋂₀ range f) = ⋂ (i : ι), interior (f i)
⊢ Eq.{u + 1} (α := Set X) (interior (⋂ (i : ι), f i)) (⋂ (i : ι), interior (f i))
have rw₁ : Eq.{u + 1} (α := Set X) (⋂ s ∈ range f, interior s) (⋂ (i : ι), interior (f i))
Tactic: rw [← sInter_range, (finite_range f).interior_sInter, biInter_range]
-- Lean 4 proof step from Mathlib.Topology.Closure (goal)
Goal:
X : Type u
inst : TopologicalSpace X
ι : Sort v
inst_1 : Finite ι
f : ι → Set X
rw : interior (⋂₀ range f) = ⋂ (i : ι), interior (f i)
rw₁ : Eq.{u + 1} (α := Set X) (⋂ s ∈ range f, interior s) (⋂ (i : ι), interior (f i))
⊢ Eq.{u + 1} (α := Set X) (interior (⋂ (i : ι), f i)) (⋂ (i : ι), interior (f i))
have rw₂ : Eq.{u + 1} (α := Set X) (⋂ (y : ι), interior (f y)) (⋂ (i : ι), interior (f i))
Tactic: rw [← sInter_range, (finite_range f).interior_sInter, biInter_range]
-- Lean 4 proof step from Mathlib.Topology.Closure (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s t : Set X
h₁ : IsClosed s
h₂ : interior t = ∅
x : X
h : x ∈ interior (s ∪ t)
u : Set X
hu₁ : IsOpen u
hu₂ : u ⊆ s ∪ t
hx₁ : x ∈ u
hx₂ : x ∉ s
this_1 : u \ s ⊆ t
this : u \ s ⊆ interior t
⊢ u \ s ⊆ ∅
have rwa : ∀ (this : u \ s ⊆ ∅), u \ s ⊆ ∅
Tactic: rwa [h₂] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.Closure (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
⊢ IsOpen s ↔ ∀ x ∈ s, ∃ t ⊆ s, IsOpen t ∧ x ∈ t
have rw : s ⊆ interior s ↔ ∀ x ∈ s, ∃ t ⊆ s, IsOpen t ∧ x ∈ t
Tactic: rw [← subset_interior_iff_isOpen]
-- Lean 4 proof step from Mathlib.Topology.Closure (goal)
Goal:
X : Type u
inst : TopologicalSpace X
S : Set (Set X)
⊢ interior (⋂₀ S) = interior (⋂ s ∈ S, s)
have rw : Eq.{u + 1} (α := Set X) (interior (⋂ i ∈ S, i)) (interior (⋂ s ∈ S, s))
Tactic: rw [sInter_eq_biInter]
-- Lean 4 proof step from Mathlib.Topology.Closure (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s t : Set X
⊢ s \ t ⊆ closure t ↔ s ⊆ closure t
have rw : s ⊆ t ∪ closure t ↔ s ⊆ closure t
Tactic: rw [diff_subset_iff, union_eq_self_of_subset_left subset_closure]
-- Lean 4 proof step from Mathlib.Topology.Closure (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s t : Set X
rw : s ⊆ t ∪ closure t ↔ s ⊆ closure t
⊢ s \ t ⊆ closure t ↔ s ⊆ closure t
have rw₁ : s ⊆ closure t ↔ s ⊆ closure t
Tactic: rw [diff_subset_iff, union_eq_self_of_subset_left subset_closure]
-- Lean 4 proof step from Mathlib.Topology.Closure (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
h : closure s ⊆ s
⊢ IsClosed s
have rw : IsClosed (closure s)
Tactic: rw [subset_closure.antisymm h]
-- Lean 4 proof step from Mathlib.Topology.Closure (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
⊢ closure s = (interior sᶜ)ᶜ
have rw : Eq.{u + 1} (α := Set X) (⋂₀ {t : Set X | IsClosed t ∧ s ⊆ t}) (⋂₀ {s_1 : Set X | IsOpen s_1ᶜ ∧ s_1ᶜ ⊆ sᶜ})
Tactic: rw [interior, closure, compl_sUnion, compl_image_set_of]
-- Lean 4 proof step from Mathlib.Topology.Closure (goal)
Goal:
X : Type u
inst : TopologicalSpace X
S : Set (Set X)
hS : S.Finite
⊢ closure (⋃₀ S) = ⋃ s ∈ S, closure s
have rw : Eq.{u + 1} (α := Set X) (closure (⋃ i ∈ S, i)) (⋃ s ∈ S, closure s)
Tactic: rw [sUnion_eq_biUnion, hS.closure_biUnion]
-- Lean 4 proof step from Mathlib.Topology.Closure (goal)
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)
⊢ closure (⋃₀ S) = ⋃ s ∈ S, closure s
have rw₁ : Eq.{u + 1} (α := Set X) (⋃ i ∈ S, closure i) (⋃ s ∈ S, closure s)
Tactic: rw [sUnion_eq_biUnion, hS.closure_biUnion]
-- Lean 4 proof step from Mathlib.Topology.Closure (goal)
Goal:
X : Type u
inst : TopologicalSpace X
ι : Sort v
inst_1 : Finite ι
f : ι → Set X
⊢ Eq.{u + 1} (α := Set X) (closure (⋃ (i : ι), f i)) (⋃ (i : ι), closure (f i))
have rw : closure (⋃₀ range f) = ⋃ (i : ι), closure (f i)
Tactic: rw [← sUnion_range, (finite_range _).closure_sUnion, biUnion_range]
-- Lean 4 proof step from Mathlib.Topology.Closure (goal)
Goal:
X : Type u
inst : TopologicalSpace X
ι : Sort v
inst_1 : Finite ι
f : ι → Set X
rw : closure (⋃₀ range f) = ⋃ (i : ι), closure (f i)
⊢ Eq.{u + 1} (α := Set X) (closure (⋃ (i : ι), f i)) (⋃ (i : ι), closure (f i))
have rw₁ : Eq.{u + 1} (α := Set X) (⋃ s ∈ range f, closure s) (⋃ (i : ι), closure (f i))
Tactic: rw [← sUnion_range, (finite_range _).closure_sUnion, biUnion_range]
-- Lean 4 proof step from Mathlib.Topology.Closure (goal)
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))
⊢ Eq.{u + 1} (α := Set X) (closure (⋃ (i : ι), f i)) (⋃ (i : ι), closure (f i))
have rw₂ : Eq.{u + 1} (α := Set X) (⋃ (y : ι), closure (f y)) (⋃ (i : ι), closure (f i))
Tactic: rw [← sUnion_range, (finite_range _).closure_sUnion, biUnion_range]
-- Lean 4 proof step from Mathlib.Topology.Closure (hypothesis)
Goal:
X : Type u
inst : TopologicalSpace X
s t : Set X
h : Disjoint (closure s) (closure t)
⊢ interior (s ∪ t) = interior s ∪ interior t
have full : interior sᶜ ∪ interior tᶜ = univ
Tactic: have full : interior sᶜ ∪ interior tᶜ = univ := by simpa [disjoint_iff, ← compl_inter] using h
-- Lean 4 proof step from Mathlib.Topology.Closure (goal)
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
have refine : interior (s ∪ t) ⊆ interior s ∪ interior t
Tactic: refine subset_antisymm ?_ subset_interior_union
-- Lean 4 proof step from Mathlib.Topology.Closure (goal)
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
have rw : interior (s ∪ t) ∩ interior sᶜ ∪ interior (s ∪ t) ∩ interior tᶜ ⊆ interior s ∪ interior t
Tactic: rw [← (interior _).inter_univ, ← full, inter_union_distrib_left]
-- Lean 4 proof step from Mathlib.Topology.Closure (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s t : Set X
h : Codisjoint (interior s) (interior t)
⊢ closure (s ∩ t) = closure s ∩ closure t
have rw : (closure (s ∩ t))ᶜ = (closure s ∩ closure t)ᶜ
Tactic: rw [← compl_inj_iff]
-- Lean 4 proof step from Mathlib.Topology.Closure (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s t : Set X
h : Codisjoint (interior s) (interior t)
⊢ (closure (s ∩ t))ᶜ = (closure s ∩ closure t)ᶜ
have simp : interior (sᶜ ∪ tᶜ) = interior sᶜ ∪ interior tᶜ
Tactic: simp only [← interior_compl, compl_inter]
-- Lean 4 proof step from Mathlib.Topology.Closure (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s t : Set X
h : Codisjoint (interior s) (interior t)
⊢ interior (sᶜ ∪ tᶜ) = interior sᶜ ∪ interior tᶜ
have h₁ : Disjoint (closure sᶜ) (closure tᶜ)
Tactic: apply interior_union_of_disjoint_closure
-- Lean 4 proof step from Mathlib.Topology.Closure (goal)
Goal:
X : Type u
inst : TopologicalSpace X
l : Filter X
h : l = ⊥
⊢ Eq.{u + 1} (α := Filter X) (Filter.lift' ⊥ closure) ⊥
have rw : Eq.{u + 1} (α := Filter X) (𝓟 (closure ∅)) ⊥
Tactic: rw [lift'_bot (monotone_closure _), closure_empty, principal_empty]
-- Lean 4 proof step from Mathlib.Topology.Closure (goal)
Goal:
X : Type u
inst : TopologicalSpace X
l : Filter X
h : l = ⊥
rw : Eq.{u + 1} (α := Filter X) (𝓟 (closure ∅)) ⊥
⊢ Eq.{u + 1} (α := Filter X) (Filter.lift' ⊥ closure) ⊥
have rw₁ : Eq.{u + 1} (α := Filter X) (𝓟 ∅) ⊥
Tactic: rw [lift'_bot (monotone_closure _), closure_empty, principal_empty]
-- Lean 4 proof step from Mathlib.Topology.Closure (goal)
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) (𝓟 ∅) ⊥
⊢ Eq.{u + 1} (α := Filter X) (Filter.lift' ⊥ closure) ⊥
have rw₂ : Eq.{u + 1} (α := Filter X) ⊥ ⊥
Tactic: rw [lift'_bot (monotone_closure _), closure_empty, principal_empty]
-- Lean 4 proof step from Mathlib.Topology.Closure (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
⊢ interior s = ∅ ↔ Dense sᶜ
have rw : interior s = ∅ ↔ closure sᶜ = univ
Tactic: rw [dense_iff_closure_eq, closure_compl, compl_univ_iff]
-- Lean 4 proof step from Mathlib.Topology.Closure (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
rw : interior s = ∅ ↔ closure sᶜ = univ
⊢ interior s = ∅ ↔ Dense sᶜ
have rw₁ : interior s = ∅ ↔ (interior s)ᶜ = univ
Tactic: rw [dense_iff_closure_eq, closure_compl, compl_univ_iff]
-- Lean 4 proof step from Mathlib.Topology.Closure (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
rw : interior s = ∅ ↔ closure sᶜ = univ
rw₁ : interior s = ∅ ↔ (interior s)ᶜ = univ
⊢ interior s = ∅ ↔ Dense sᶜ
have rw₂ : interior s = ∅ ↔ interior s = ∅
Tactic: rw [dense_iff_closure_eq, closure_compl, compl_univ_iff]
-- Lean 4 proof step from Mathlib.Topology.Closure (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
⊢ Dense (closure s) ↔ Dense s
have rw : (∀ (x : X), x ∈ closure (closure s)) ↔ Dense s
Tactic: rw [Dense, Dense, closure_closure]
-- Lean 4 proof step from Mathlib.Topology.Closure (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
rw : (∀ (x : X), x ∈ closure (closure s)) ↔ Dense s
⊢ Dense (closure s) ↔ Dense s
have rw₁ : (∀ (x : X), x ∈ closure (closure s)) ↔ ∀ (x : X), x ∈ closure s
Tactic: rw [Dense, Dense, closure_closure]
-- Lean 4 proof step from Mathlib.Topology.Closure (goal)
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
⊢ Dense (closure s) ↔ Dense s
have rw₂ : (∀ (x : X), x ∈ closure s) ↔ ∀ (x : X), x ∈ closure s
Tactic: rw [Dense, Dense, closure_closure]
-- Lean 4 proof step from Mathlib.Topology.Closure (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
⊢ Dense s ↔ ∀ (U : Set X), IsOpen U → U.Nonempty → (U ∩ s).Nonempty
have mp : Dense s → ∀ (U : Set X), IsOpen U → U.Nonempty → (U ∩ s).Nonempty
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Closure (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
mp : Dense s → ∀ (U : Set X), IsOpen U → U.Nonempty → (U ∩ s).Nonempty
⊢ Dense s ↔ ∀ (U : Set X), IsOpen U → U.Nonempty → (U ∩ s).Nonempty
have mpr : (∀ (U : Set X), IsOpen U → U.Nonempty → (U ∩ s).Nonempty) → Dense s
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Closure (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
h : ∀ (U : Set X), IsOpen U → U.Nonempty → (U ∩ s).Nonempty
x : X
⊢ x ∈ closure s
have mpr : ∀ (o : Set X), IsOpen o → x ∈ o → (o ∩ s).Nonempty
Tactic: rw [mem_closure_iff]
-- Lean 4 proof step from Mathlib.Topology.Closure (goal)
Goal:
X : Type u
inst : TopologicalSpace X
x : X
⊢ Dense (X := X) {x}ᶜ ↔ ¬IsOpen (X := X) {x}
have mp : Dense (X := X) {x}ᶜ → ¬IsOpen (X := X) {x}
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Closure (goal)
Goal:
X : Type u
inst : TopologicalSpace X
x : X
mp : Dense (X := X) {x}ᶜ → ¬IsOpen (X := X) {x}
⊢ Dense (X := X) {x}ᶜ ↔ ¬IsOpen (X := X) {x}
have mpr : ¬IsOpen (X := X) {x} → Dense (X := X) {x}ᶜ
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Closure (goal)
Goal:
X : Type u
inst : TopologicalSpace X
x : X
⊢ ¬IsOpen (X := X) {x} → Dense (X := X) {x}ᶜ
have mpr : ∀ (ho : ¬IsOpen (X := X) {x}) (U : Set X) (hU : IsOpen U) (hne : U.Nonempty) (hUx : U ⊆ {x}), False
Tactic: refine fun ho => dense_iff_inter_open.2 fun U hU hne => inter_compl_nonempty_iff.2 fun hUx => ?_
-- Lean 4 proof step from Mathlib.Topology.Closure (hypothesis)
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}
⊢ False
have hU₁ : IsOpen (X := X) {x}
Tactic: obtain rfl : U = {x} := eq_singleton_iff_nonempty_unique_mem.2 ⟨hne, hUx⟩
Cleared hypotheses: U, hU, hne, hUx
-- Lean 4 proof step from Mathlib.Topology.Closure (hypothesis)
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}
⊢ False
have hne₁ : Set.Nonempty (α := X) {x}
Tactic: obtain rfl : U = {x} := eq_singleton_iff_nonempty_unique_mem.2 ⟨hne, hUx⟩
Cleared hypotheses: U, hU, hne, hUx
-- Lean 4 proof step from Mathlib.Topology.Closure (hypothesis)
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}
⊢ False
have hUx₁ : Subset (α := Set X) {x} {x}
Tactic: obtain rfl : U = {x} := eq_singleton_iff_nonempty_unique_mem.2 ⟨hne, hUx⟩
Cleared hypotheses: U, hU, hne, hUx
-- Lean 4 proof step from Mathlib.Topology.Closure (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
⊢ Disjoint (interior s) (frontier s)
have rw : 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]
-- Lean 4 proof step from Mathlib.Topology.Closure (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
rw : interior s ∩ frontier s = ∅
⊢ Disjoint (interior s) (frontier s)
have rw₁ : interior s ∩ (closure s \ interior s) = ∅
Tactic: rw [disjoint_iff_inter_eq_empty, ← closure_diff_interior, diff_eq,
    ← inter_assoc, inter_comm, ← inter_assoc, compl_inter_self, empty_inter]
-- Lean 4 proof step from Mathlib.Topology.Closure (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
rw : interior s ∩ frontier s = ∅
rw₁ : interior s ∩ (closure s \ interior s) = ∅
⊢ Disjoint (interior s) (frontier s)
have rw₂ : interior s ∩ (closure s ∩ (interior s)ᶜ) = ∅
Tactic: rw [disjoint_iff_inter_eq_empty, ← closure_diff_interior, diff_eq,
    ← inter_assoc, inter_comm, ← inter_assoc, compl_inter_self, empty_inter]
-- Lean 4 proof step from Mathlib.Topology.Closure (goal)
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)ᶜ) = ∅
⊢ Disjoint (interior s) (frontier s)
have rw₃ : interior s ∩ closure s ∩ (interior s)ᶜ = ∅
Tactic: rw [disjoint_iff_inter_eq_empty, ← closure_diff_interior, diff_eq,
    ← inter_assoc, inter_comm, ← inter_assoc, compl_inter_self, empty_inter]
-- Lean 4 proof step from Mathlib.Topology.Closure (goal)
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)ᶜ = ∅
⊢ Disjoint (interior s) (frontier s)
have rw₄ : (interior s)ᶜ ∩ (interior s ∩ closure s) = ∅
Tactic: rw [disjoint_iff_inter_eq_empty, ← closure_diff_interior, diff_eq,
    ← inter_assoc, inter_comm, ← inter_assoc, compl_inter_self, empty_inter]
-- Lean 4 proof step from Mathlib.Topology.Closure (goal)
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) = ∅
⊢ Disjoint (interior s) (frontier s)
have rw₅ : (interior s)ᶜ ∩ interior s ∩ closure s = ∅
Tactic: rw [disjoint_iff_inter_eq_empty, ← closure_diff_interior, diff_eq,
    ← inter_assoc, inter_comm, ← inter_assoc, compl_inter_self, empty_inter]
-- Lean 4 proof step from Mathlib.Topology.Closure (goal)
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 = ∅
⊢ Disjoint (interior s) (frontier s)
have rw₆ : ∅ ∩ closure s = ∅
Tactic: rw [disjoint_iff_inter_eq_empty, ← closure_diff_interior, diff_eq,
    ← inter_assoc, inter_comm, ← inter_assoc, compl_inter_self, empty_inter]
-- Lean 4 proof step from Mathlib.Topology.Closure (goal)
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 = ∅
⊢ Disjoint (interior s) (frontier s)
have rw₇ : Eq.{u + 1} (α := Set X) ∅ ∅
Tactic: rw [disjoint_iff_inter_eq_empty, ← closure_diff_interior, diff_eq,
    ← inter_assoc, inter_comm, ← inter_assoc, compl_inter_self, empty_inter]
-- Lean 4 proof step from Mathlib.Topology.Closure (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
⊢ closure s \ frontier s = interior s
have rw : closure s \ (closure s \ interior s) = interior s
Tactic: rw [frontier, diff_diff_right_self, inter_eq_self_of_subset_right interior_subset_closure]
-- Lean 4 proof step from Mathlib.Topology.Closure (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
rw : closure s \ (closure s \ interior s) = interior s
⊢ closure s \ frontier s = interior s
have rw₁ : closure s ∩ interior s = interior s
Tactic: rw [frontier, diff_diff_right_self, inter_eq_self_of_subset_right interior_subset_closure]
-- Lean 4 proof step from Mathlib.Topology.Closure (goal)
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
⊢ closure s \ frontier s = interior s
have rw₂ : interior s = interior s
Tactic: rw [frontier, diff_diff_right_self, inter_eq_self_of_subset_right interior_subset_closure]
-- Lean 4 proof step from Mathlib.Topology.Closure (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
⊢ s \ frontier s = interior s
have rw : s \ (closure s \ interior 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]
-- Lean 4 proof step from Mathlib.Topology.Closure (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
rw : s \ (closure s \ interior s) = interior s
⊢ s \ frontier s = interior s
have rw₁ : s \ closure s ∪ s ∩ interior 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]
-- Lean 4 proof step from Mathlib.Topology.Closure (goal)
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
⊢ s \ frontier s = interior s
have rw₂ : ∅ ∪ s ∩ interior 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]
-- Lean 4 proof step from Mathlib.Topology.Closure (goal)
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
⊢ s \ frontier s = interior s
have rw₃ : ∅ ∪ interior 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]
-- Lean 4 proof step from Mathlib.Topology.Closure (goal)
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
⊢ s \ frontier s = interior s
have rw₄ : interior 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]
-- Lean 4 proof step from Mathlib.Topology.Closure (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
⊢ frontier s = closure s ∩ closure sᶜ
have rw : frontier s = closure s ∩ (interior s)ᶜ
Tactic: rw [closure_compl, frontier, diff_eq]
-- Lean 4 proof step from Mathlib.Topology.Closure (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
rw : frontier s = closure s ∩ (interior s)ᶜ
⊢ frontier s = closure s ∩ closure sᶜ
have rw₁ : closure s \ interior s = closure s ∩ (interior s)ᶜ
Tactic: rw [closure_compl, frontier, diff_eq]
-- Lean 4 proof step from Mathlib.Topology.Closure (goal)
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)ᶜ
⊢ frontier s = closure s ∩ closure sᶜ
have rw₂ : closure s ∩ (interior s)ᶜ = closure s ∩ (interior s)ᶜ
Tactic: rw [closure_compl, frontier, diff_eq]
-- Lean 4 proof step from Mathlib.Topology.Closure (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
⊢ frontier s ⊆ s ↔ IsClosed s
have rw : closure s \ interior s ⊆ s ↔ IsClosed s
Tactic: rw [frontier, diff_subset_iff, union_eq_right.mpr interior_subset, closure_subset_iff_isClosed]
-- Lean 4 proof step from Mathlib.Topology.Closure (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
rw : closure s \ interior s ⊆ s ↔ IsClosed s
⊢ frontier s ⊆ s ↔ IsClosed s
have rw₁ : closure s ⊆ interior s ∪ s ↔ IsClosed s
Tactic: rw [frontier, diff_subset_iff, union_eq_right.mpr interior_subset, closure_subset_iff_isClosed]
-- Lean 4 proof step from Mathlib.Topology.Closure (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
rw : closure s \ interior s ⊆ s ↔ IsClosed s
rw₁ : closure s ⊆ interior s ∪ s ↔ IsClosed s
⊢ frontier s ⊆ s ↔ IsClosed s
have rw₂ : closure s ⊆ s ↔ IsClosed s
Tactic: rw [frontier, diff_subset_iff, union_eq_right.mpr interior_subset, closure_subset_iff_isClosed]
-- Lean 4 proof step from Mathlib.Topology.Closure (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
rw : closure s \ interior s ⊆ s ↔ IsClosed s
rw₁ : closure s ⊆ interior s ∪ s ↔ IsClosed s
rw₂ : closure s ⊆ s ↔ IsClosed s
⊢ frontier s ⊆ s ↔ IsClosed s
have rw₃ : IsClosed s ↔ IsClosed s
Tactic: rw [frontier, diff_subset_iff, union_eq_right.mpr interior_subset, closure_subset_iff_isClosed]
-- Lean 4 proof step from Mathlib.Topology.Closure (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s t : Set X
⊢ frontier (s ∩ t) ⊆ frontier s ∩ closure t ∪ closure s ∩ frontier t
have simp : closure (s ∩ t) ∩ (closure sᶜ ∪ closure tᶜ) ⊆ closure s ∩ closure sᶜ ∩ closure t ∪ closure s ∩ (closure t ∩ closure tᶜ)
Tactic: simp only [frontier_eq_closure_inter_closure, compl_inter, closure_union]
-- Lean 4 proof step from Mathlib.Topology.Closure (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s t : Set X
⊢ closure (s ∩ t) ∩ (closure sᶜ ∪ closure tᶜ) ⊆
    closure s ∩ closure sᶜ ∩ closure t ∪ closure s ∩ (closure t ∩ closure tᶜ)
have refine : closure s ∩ closure t ∩ (closure sᶜ ∪ closure tᶜ) =
  closure s ∩ closure sᶜ ∩ closure t ∪ closure s ∩ (closure t ∩ closure tᶜ)
Tactic: refine (inter_subset_inter_left _ (closure_inter_subset_inter_closure s t)).trans_eq ?_
-- Lean 4 proof step from Mathlib.Topology.Closure (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : IsClosed s
⊢ frontier s = s \ interior s
have rw : closure s \ interior s = s \ interior s
Tactic: rw [frontier, hs.closure_eq]
-- Lean 4 proof step from Mathlib.Topology.Closure (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : IsClosed s
rw : closure s \ interior s = s \ interior s
⊢ frontier s = s \ interior s
have rw₁ : s \ interior s = s \ interior s
Tactic: rw [frontier, hs.closure_eq]
-- Lean 4 proof step from Mathlib.Topology.Closure (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : IsOpen s
⊢ frontier s = closure s \ s
have rw : closure s \ interior s = closure s \ s
Tactic: rw [frontier, hs.interior_eq]
-- Lean 4 proof step from Mathlib.Topology.Closure (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : IsOpen s
rw : closure s \ interior s = closure s \ s
⊢ frontier s = closure s \ s
have rw₁ : closure s \ s = closure s \ s
Tactic: rw [frontier, hs.interior_eq]
-- Lean 4 proof step from Mathlib.Topology.Closure (goal)
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : IsOpen s
⊢ s ∩ frontier s = ∅
have rw : s ∩ (closure s \ s) = ∅
Tactic: rw [hs.frontier_eq, inter_diff_self]