-- Mathlib/Topology/JacobsonSpace.lean
lemma jacobsonSpace_iff_locallyClosed :
    JacobsonSpace X ↔ ∀ Z, Z.Nonempty → IsLocallyClosed Z → (Z ∩ closedPoints X).Nonempty

Proof state:
case mp
X : Type u_1
inst✝ : TopologicalSpace X
⊢ (∀ {Z : Set X}, IsClosed Z → closure (Z ∩ closedPoints X) = Z) →
    ∀ (Z : Set X), Z.Nonempty → IsLocallyClosed Z → (Z ∩ closedPoints X).Nonempty

Tactic:
simp_rw [isLocallyClosed_iff_isOpen_coborder, coborder, isOpen_compl_iff,
  Set.nonempty_iff_ne_empty]

Result:
case mp
X : Type u_1
inst✝ : TopologicalSpace X
⊢ (∀ {Z : Set X}, IsClosed Z → closure (Z ∩ closedPoints X) = Z) →
    ∀ (Z : Set X), Z ≠ ∅ → IsClosed (closure Z \ Z) → Z ∩ closedPoints X ≠ ∅

Proof state:
case mpr
X : Type u_1
inst✝ : TopologicalSpace X
H : ∀ (Z : Set X), Z.Nonempty → IsLocallyClosed Z → (Z ∩ closedPoints X).Nonempty
Z : Set X
hZ : IsClosed Z
H' : ((closure (Z ∩ closedPoints X))ᶜ ∩ Z).Nonempty
this : ((closure (Z ∩ closedPoints X))ᶜ ∩ Z ∩ closedPoints X).Nonempty
⊢ False

Tactic:
rw [Set.nonempty_iff_ne_empty, Set.inter_assoc, ne_eq,
  ← Set.disjoint_iff_inter_eq_empty, Set.disjoint_compl_left_iff_subset] at this

Result:
case mpr
X : Type u_1
inst✝ : TopologicalSpace X
H : ∀ (Z : Set X), Z.Nonempty → IsLocallyClosed Z → (Z ∩ closedPoints X).Nonempty
Z : Set X
hZ : IsClosed Z
H' : ((closure (Z ∩ closedPoints X))ᶜ ∩ Z).Nonempty
this : ¬Z ∩ closedPoints X ⊆ closure (Z ∩ closedPoints X)
⊢ False

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
H : ∀ {Z : Set X}, IsClosed Z → closure (Z ∩ closedPoints X) = Z
Z : Set X
hZ : Z ≠ ∅
hZ' : IsClosed (closure Z \ Z)
e : Z ∩ closedPoints X = ∅
⊢ Z ⊆ closure Z \ Z

Tactic:
refine subset_closure.trans ?_

Result:
X : Type u_1
inst✝ : TopologicalSpace X
H : ∀ {Z : Set X}, IsClosed Z → closure (Z ∩ closedPoints X) = Z
Z : Set X
hZ : Z ≠ ∅
hZ' : IsClosed (closure Z \ Z)
e : Z ∩ closedPoints X = ∅
⊢ closure Z ⊆ closure Z \ Z

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
⊢ JacobsonSpace X ↔ ∀ (Z : Set X), Z.Nonempty → IsLocallyClosed Z → (Z ∩ closedPoints X).Nonempty

Tactic:
rw [jacobsonSpace_iff]

Result:
X : Type u_1
inst✝ : TopologicalSpace X
⊢ (∀ {Z : Set X}, IsClosed Z → closure (Z ∩ closedPoints X) = Z) ↔
    ∀ (Z : Set X), Z.Nonempty → IsLocallyClosed Z → (Z ∩ closedPoints X).Nonempty

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
⊢ (∀ {Z : Set X}, IsClosed Z → closure (Z ∩ closedPoints X) = Z) ↔
    ∀ (Z : Set X), Z.Nonempty → IsLocallyClosed Z → (Z ∩ closedPoints X).Nonempty

Tactic:
constructor

Result:
case mp
X : Type u_1
inst✝ : TopologicalSpace X
⊢ (∀ {Z : Set X}, IsClosed Z → closure (Z ∩ closedPoints X) = Z) →
    ∀ (Z : Set X), Z.Nonempty → IsLocallyClosed Z → (Z ∩ closedPoints X).Nonempty

case mpr
X : Type u_1
inst✝ : TopologicalSpace X
⊢ (∀ (Z : Set X), Z.Nonempty → IsLocallyClosed Z → (Z ∩ closedPoints X).Nonempty) →
    ∀ {Z : Set X}, IsClosed Z → closure (Z ∩ closedPoints X) = Z

Proof state:
case mp
X : Type u_1
inst✝ : TopologicalSpace X
⊢ (∀ {Z : Set X}, IsClosed Z → closure (Z ∩ closedPoints X) = Z) →
    ∀ (Z : Set X), Z ≠ ∅ → IsClosed (closure Z \ Z) → Z ∩ closedPoints X ≠ ∅

Tactic:
intros H Z hZ hZ' e

Result:
case mp
X : Type u_1
inst✝ : TopologicalSpace X
H : ∀ {Z : Set X}, IsClosed Z → closure (Z ∩ closedPoints X) = Z
Z : Set X
hZ : Z ≠ ∅
hZ' : IsClosed (closure Z \ Z)
e : Z ∩ closedPoints X = ∅
⊢ False

Proof state:
case mpr
X : Type u_1
inst✝ : TopologicalSpace X
H : ∀ (Z : Set X), Z.Nonempty → IsLocallyClosed Z → (Z ∩ closedPoints X).Nonempty
Z : Set X
hZ : IsClosed Z
⊢ ¬((closure (Z ∩ closedPoints X))ᶜ ∩ Z).Nonempty

Tactic:
intro H'

Result:
case mpr
X : Type u_1
inst✝ : TopologicalSpace X
H : ∀ (Z : Set X), Z.Nonempty → IsLocallyClosed Z → (Z ∩ closedPoints X).Nonempty
Z : Set X
hZ : IsClosed Z
H' : ((closure (Z ∩ closedPoints X))ᶜ ∩ Z).Nonempty
⊢ False

Proof state:
case mp
X : Type u_1
inst✝ : TopologicalSpace X
H : ∀ {Z : Set X}, IsClosed Z → closure (Z ∩ closedPoints X) = Z
Z : Set X
hZ : Z ≠ ∅
hZ' : IsClosed (closure Z \ Z)
e : Z ∩ closedPoints X = ∅
this : Z ⊆ closure Z \ Z
⊢ False

Tactic:
rw [Set.subset_diff, disjoint_self, Set.bot_eq_empty] at this

Result:
case mp
X : Type u_1
inst✝ : TopologicalSpace X
H : ∀ {Z : Set X}, IsClosed Z → closure (Z ∩ closedPoints X) = Z
Z : Set X
hZ : Z ≠ ∅
hZ' : IsClosed (closure Z \ Z)
e : Z ∩ closedPoints X = ∅
this : Z ⊆ closure Z ∧ Z = ∅
⊢ False

Proof state:
case mpr
X : Type u_1
inst✝ : TopologicalSpace X
H : ∀ (Z : Set X), Z.Nonempty → IsLocallyClosed Z → (Z ∩ closedPoints X).Nonempty
Z : Set X
hZ : IsClosed Z
H' : ((closure (Z ∩ closedPoints X))ᶜ ∩ Z).Nonempty
⊢ False

Tactic:
have := H _ H' (isClosed_closure.isOpen_compl.isLocallyClosed.inter hZ.isLocallyClosed)

Result:
case mpr
X : Type u_1
inst✝ : TopologicalSpace X
H : ∀ (Z : Set X), Z.Nonempty → IsLocallyClosed Z → (Z ∩ closedPoints X).Nonempty
Z : Set X
hZ : IsClosed Z
H' : ((closure (Z ∩ closedPoints X))ᶜ ∩ Z).Nonempty
this : ((closure (Z ∩ closedPoints X))ᶜ ∩ Z ∩ closedPoints X).Nonempty
⊢ False

Proof state:
case mpr
X : Type u_1
inst✝ : TopologicalSpace X
H : ∀ (Z : Set X), Z.Nonempty → IsLocallyClosed Z → (Z ∩ closedPoints X).Nonempty
Z : Set X
hZ : IsClosed Z
⊢ Z ⊆ closure (Z ∩ closedPoints X)

Tactic:
rw [← Set.disjoint_compl_left_iff_subset, Set.disjoint_iff_inter_eq_empty,
  ← Set.not_nonempty_iff_eq_empty]

Result:
case mpr
X : Type u_1
inst✝ : TopologicalSpace X
H : ∀ (Z : Set X), Z.Nonempty → IsLocallyClosed Z → (Z ∩ closedPoints X).Nonempty
Z : Set X
hZ : IsClosed Z
⊢ ¬((closure (Z ∩ closedPoints X))ᶜ ∩ Z).Nonempty

Proof state:
case mp
X : Type u_1
inst✝ : TopologicalSpace X
H : ∀ {Z : Set X}, IsClosed Z → closure (Z ∩ closedPoints X) = Z
Z : Set X
hZ : Z ≠ ∅
hZ' : IsClosed (closure Z \ Z)
e : Z ∩ closedPoints X = ∅
⊢ False

Tactic:
have : Z ⊆ closure Z \ Z := by
  refine subset_closure.trans ?_
  nth_rw 1 [← H isClosed_closure]
  rw [hZ'.closure_subset_iff, Set.subset_diff, Set.disjoint_iff, Set.inter_assoc,
    Set.inter_comm _ Z, e]
  exact ⟨Set.inter_subset_left, Set.inter_subset_right⟩

Result:
case mp
X : Type u_1
inst✝ : TopologicalSpace X
H : ∀ {Z : Set X}, IsClosed Z → closure (Z ∩ closedPoints X) = Z
Z : Set X
hZ : Z ≠ ∅
hZ' : IsClosed (closure Z \ Z)
e : Z ∩ closedPoints X = ∅
this : Z ⊆ closure Z \ Z
⊢ False

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
H : ∀ {Z : Set X}, IsClosed Z → closure (Z ∩ closedPoints X) = Z
Z : Set X
hZ : Z ≠ ∅
hZ' : IsClosed (closure Z \ Z)
e : Z ∩ closedPoints X = ∅
⊢ closure Z ∩ closedPoints X ⊆ closure Z ∧ closure Z ∩ ∅ ⊆ ∅

Tactic:
exact ⟨Set.inter_subset_left, Set.inter_subset_right⟩

Result:
no goals

Proof state:
case mpr
X : Type u_1
inst✝ : TopologicalSpace X
⊢ (∀ (Z : Set X), Z.Nonempty → IsLocallyClosed Z → (Z ∩ closedPoints X).Nonempty) →
    ∀ {Z : Set X}, IsClosed Z → closure (Z ∩ closedPoints X) = Z

Tactic:
intro H Z hZ

Result:
case mpr
X : Type u_1
inst✝ : TopologicalSpace X
H : ∀ (Z : Set X), Z.Nonempty → IsLocallyClosed Z → (Z ∩ closedPoints X).Nonempty
Z : Set X
hZ : IsClosed Z
⊢ closure (Z ∩ closedPoints X) = Z

Proof state:
case mpr
X : Type u_1
inst✝ : TopologicalSpace X
H : ∀ (Z : Set X), Z.Nonempty → IsLocallyClosed Z → (Z ∩ closedPoints X).Nonempty
Z : Set X
hZ : IsClosed Z
⊢ closure (Z ∩ closedPoints X) = Z

Tactic:
refine subset_antisymm (hZ.closure_subset_iff.mpr Set.inter_subset_left) ?_

Result:
case mpr
X : Type u_1
inst✝ : TopologicalSpace X
H : ∀ (Z : Set X), Z.Nonempty → IsLocallyClosed Z → (Z ∩ closedPoints X).Nonempty
Z : Set X
hZ : IsClosed Z
⊢ Z ⊆ closure (Z ∩ closedPoints X)