case empty
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : T1Space α
inst✝ : ∀ (x : α), NeBot (𝓝[{x}ᶜ] x)
s : Set α
hs : Dense s
⊢ Dense (s \ ↑∅)

case insert
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : T1Space α
inst✝ : ∀ (x : α), NeBot (𝓝[{x}ᶜ] x)
s : Set α
hs : Dense s
a✝² : α
s✝ : Finset α
a✝¹ : ¬a✝² ∈ s✝
a✝ : Dense (s \ ↑s✝)
⊢ Dense (s \ ↑(insert a✝² s✝))
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : T1Space α
inst✝ : ∀ (x : α), NeBot (𝓝[{x}ᶜ] x)
s : Set α
hs : Dense s
t : Finset α
⊢ Dense (s \ ↑t)
induction t using Finset.induction_on
case insert
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : T1Space α
inst✝ : ∀ (x : α), NeBot (𝓝[{x}ᶜ] x)
s : Set α
hs : Dense s
a✝² : α
s✝ : Finset α
a✝¹ : ¬a✝² ∈ s✝
a✝ : Dense (s \ ↑s✝)
⊢ Dense (s \ ↑(insert a✝² s✝))
case empty
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : T1Space α
inst✝ : ∀ (x : α), NeBot (𝓝[{x}ᶜ] x)
s : Set α
hs : Dense s
⊢ Dense (s \ ↑∅)

case insert
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : T1Space α
inst✝ : ∀ (x : α), NeBot (𝓝[{x}ᶜ] x)
s : Set α
hs : Dense s
a✝² : α
s✝ : Finset α
a✝¹ : ¬a✝² ∈ s✝
a✝ : Dense (s \ ↑s✝)
⊢ Dense (s \ ↑(insert a✝² s✝))
case empty =>  simpa using hs
no goals
case insert
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : T1Space α
inst✝ : ∀ (x : α), NeBot (𝓝[{x}ᶜ] x)
s : Set α
hs : Dense s
a✝² : α
s✝ : Finset α
a✝¹ : ¬a✝² ∈ s✝
a✝ : Dense (s \ ↑s✝)
⊢ Dense (s \ ↑(insert a✝² s✝))
case insert ih =>
  rw [Finset.coe_insert, ← union_singleton, ← diff_diff]
  exact ih.diff_singleton _
no goals
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : T1Space α
inst✝ : ∀ (x : α), NeBot (𝓝[{x}ᶜ] x)
s : Set α
hs : Dense s
⊢ Dense (s \ ↑∅)
simpa using hs
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : T1Space α
inst✝ : ∀ (x : α), NeBot (𝓝[{x}ᶜ] x)
s : Set α
hs : Dense s
a✝¹ : α
s✝ : Finset α
a✝ : ¬a✝¹ ∈ s✝
ih : Dense (s \ ↑s✝)
⊢ Dense ((s \ ↑s✝) \ {a✝¹})
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : T1Space α
inst✝ : ∀ (x : α), NeBot (𝓝[{x}ᶜ] x)
s : Set α
hs : Dense s
a✝¹ : α
s✝ : Finset α
a✝ : ¬a✝¹ ∈ s✝
ih : Dense (s \ ↑s✝)
⊢ Dense (s \ ↑(insert a✝¹ s✝))
rw [Finset.coe_insert, ← union_singleton, ← diff_diff]
no goals
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : T1Space α
inst✝ : ∀ (x : α), NeBot (𝓝[{x}ᶜ] x)
s : Set α
hs : Dense s
a✝¹ : α
s✝ : Finset α
a✝ : ¬a✝¹ ∈ s✝
ih : Dense (s \ ↑s✝)
⊢ Dense ((s \ ↑s✝) \ {a✝¹})
exact ih.diff_singleton _