-- Mathlib/Topology/Bases.lean
theorem IsTopologicalBasis.diff_empty {s : Set (Set α)} (h : IsTopologicalBasis s) :
    IsTopologicalBasis (s \ {∅})

Proof state:
case refine_2
α : Type u
t✝ : TopologicalSpace α
s : Set (Set α)
h : IsTopologicalBasis s
t : Set α
ht : t ∈ s
⊢ IsOpen t

Tactic:
obtain rfl | he := eq_or_ne t ∅

Result:
case refine_2.inl
α : Type u
t : TopologicalSpace α
s : Set (Set α)
h : IsTopologicalBasis s
ht : ∅ ∈ s
⊢ IsOpen ∅

case refine_2.inr
α : Type u
t✝ : TopologicalSpace α
s : Set (Set α)
h : IsTopologicalBasis s
t : Set α
ht : t ∈ s
he : t ≠ ∅
⊢ IsOpen t

Proof state:
α : Type u
t : TopologicalSpace α
s : Set (Set α)
h : IsTopologicalBasis s
⊢ ⋃₀ (s \ {∅}) = univ

Tactic:
rw [sUnion_diff_singleton_empty, h.sUnion_eq]

Result:
no goals

Proof state:
case refine_2
α : Type u
t : TopologicalSpace α
s : Set (Set α)
h : IsTopologicalBasis s
⊢ generateFrom s = generateFrom (s \ {∅})

Tactic:
refine le_antisymm (generateFrom_anti diff_subset) (le_generateFrom fun t ht => ?_)

Result:
case refine_2
α : Type u
t✝ : TopologicalSpace α
s : Set (Set α)
h : IsTopologicalBasis s
t : Set α
ht : t ∈ s
⊢ IsOpen t

Proof state:
case refine_1.intro.intro.intro.intro
α : Type u
t : TopologicalSpace α
s : Set (Set α)
h : IsTopologicalBasis s
t₁ : Set α
h₁ : t₁ ∈ s
t₂ : Set α
h₂ : t₂ ∈ s
x : α
hx : x ∈ t₁ ∩ t₂
t₃ : Set α
h₃ : t₃ ∈ s
hs : x ∈ t₃ ∧ t₃ ⊆ t₁ ∩ t₂
⊢ ∃ t₃ ∈ s \ {∅}, x ∈ t₃ ∧ t₃ ⊆ t₁ ∩ t₂

Tactic:
exact ⟨t₃, ⟨h₃, Nonempty.ne_empty ⟨x, hs.1⟩⟩, hs⟩

Result:
no goals

Proof state:
case refine_1.intro.intro
α : Type u
t : TopologicalSpace α
s : Set (Set α)
h : IsTopologicalBasis s
t₁ : Set α
h₁ : t₁ ∈ s
t₂ : Set α
h₂ : t₂ ∈ s
x : α
hx : x ∈ t₁ ∩ t₂
⊢ ∃ t₃ ∈ s \ {∅}, x ∈ t₃ ∧ t₃ ⊆ t₁ ∩ t₂

Tactic:
obtain ⟨t₃, h₃, hs⟩ := h.exists_subset_inter _ h₁ _ h₂ x hx

Result:
case refine_1.intro.intro.intro.intro
α : Type u
t : TopologicalSpace α
s : Set (Set α)
h : IsTopologicalBasis s
t₁ : Set α
h₁ : t₁ ∈ s
t₂ : Set α
h₂ : t₂ ∈ s
x : α
hx : x ∈ t₁ ∩ t₂
t₃ : Set α
h₃ : t₃ ∈ s
hs : x ∈ t₃ ∧ t₃ ⊆ t₁ ∩ t₂
⊢ ∃ t₃ ∈ s \ {∅}, x ∈ t₃ ∧ t₃ ⊆ t₁ ∩ t₂

Proof state:
case refine_2.inr
α : Type u
t✝ : TopologicalSpace α
s : Set (Set α)
h : IsTopologicalBasis s
t : Set α
ht : t ∈ s
he : t ≠ ∅
⊢ IsOpen t

Tactic:
exact .basic t ⟨ht, he⟩

Result:
no goals

Proof state:
case refine_2.inl
α : Type u
t : TopologicalSpace α
s : Set (Set α)
h : IsTopologicalBasis s
ht : ∅ ∈ s
⊢ IsOpen ∅

Tactic:
exact @isOpen_empty _ (generateFrom _)

Result:
no goals

Proof state:
case refine_2
α : Type u
t : TopologicalSpace α
s : Set (Set α)
h : IsTopologicalBasis s
⊢ t = generateFrom (s \ {∅})

Tactic:
rw [h.eq_generateFrom]

Result:
case refine_2
α : Type u
t : TopologicalSpace α
s : Set (Set α)
h : IsTopologicalBasis s
⊢ generateFrom s = generateFrom (s \ {∅})

Proof state:
case refine_1
α : Type u
t : TopologicalSpace α
s : Set (Set α)
h : IsTopologicalBasis s
⊢ ∀ t₁ ∈ s \ {∅}, ∀ t₂ ∈ s \ {∅}, ∀ x ∈ t₁ ∩ t₂, ∃ t₃ ∈ s \ {∅}, x ∈ t₃ ∧ t₃ ⊆ t₁ ∩ t₂

Tactic:
rintro t₁ ⟨h₁, -⟩ t₂ ⟨h₂, -⟩ x hx

Result:
case refine_1.intro.intro
α : Type u
t : TopologicalSpace α
s : Set (Set α)
h : IsTopologicalBasis s
t₁ : Set α
h₁ : t₁ ∈ s
t₂ : Set α
h₂ : t₂ ∈ s
x : α
hx : x ∈ t₁ ∩ t₂
⊢ ∃ t₃ ∈ s \ {∅}, x ∈ t₃ ∧ t₃ ⊆ t₁ ∩ t₂

Proof state:
α : Type u
t : TopologicalSpace α
s : Set (Set α)
h : IsTopologicalBasis s
⊢ IsTopologicalBasis (s \ {∅})

Tactic:
refine ⟨?_, by rw [sUnion_diff_singleton_empty, h.sUnion_eq], ?_⟩

Result:
case refine_1
α : Type u
t : TopologicalSpace α
s : Set (Set α)
h : IsTopologicalBasis s
⊢ ∀ t₁ ∈ s \ {∅}, ∀ t₂ ∈ s \ {∅}, ∀ x ∈ t₁ ∩ t₂, ∃ t₃ ∈ s \ {∅}, x ∈ t₃ ∧ t₃ ⊆ t₁ ∩ t₂

case refine_2
α : Type u
t : TopologicalSpace α
s : Set (Set α)
h : IsTopologicalBasis s
⊢ t = generateFrom (s \ {∅})