-- Mathlib/Topology/JacobsonSpace.lean
lemma JacobsonSpace.discreteTopology [JacobsonSpace X]
    (h : (closedPoints X).Finite) : DiscreteTopology X

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : JacobsonSpace X
h : (closedPoints X).Finite
this : closedPoints X = Set.univ
inst : Finite X
s : Set X
x : X
x✝ : x ∈ sᶜ
⊢ x ∈ Set.univ

Tactic:
trivial

Result:
no goals

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : JacobsonSpace X
h : (closedPoints X).Finite
⊢ DiscreteTopology X

Tactic:
have : closedPoints X = Set.univ := by
  rw [← Set.univ_subset_iff, ← closure_closedPoints,
    closure_subset_iff_isClosed, ← (closedPoints X).biUnion_of_singleton]
  exact h.isClosed_biUnion fun _ ↦ id

Result:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : JacobsonSpace X
h : (closedPoints X).Finite
this : closedPoints X = Set.univ
⊢ DiscreteTopology X

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : JacobsonSpace X
h : (closedPoints X).Finite
this : closedPoints X = Set.univ
⊢ DiscreteTopology X

Tactic:
have inst : Finite X := Set.finite_univ_iff.mp (this ▸ h)

Result:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : JacobsonSpace X
h : (closedPoints X).Finite
this : closedPoints X = Set.univ
inst : Finite X
⊢ DiscreteTopology X

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : JacobsonSpace X
h : (closedPoints X).Finite
⊢ IsClosed (⋃ x ∈ closedPoints X, {x})

Tactic:
exact h.isClosed_biUnion fun _ ↦ id

Result:
no goals

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : JacobsonSpace X
h : (closedPoints X).Finite
this : closedPoints X = Set.univ
inst : Finite X
⊢ DiscreteTopology X

Tactic:
rw [← forall_open_iff_discrete]

Result:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : JacobsonSpace X
h : (closedPoints X).Finite
this : closedPoints X = Set.univ
inst : Finite X
⊢ ∀ (s : Set X), IsOpen s

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : JacobsonSpace X
h : (closedPoints X).Finite
this : closedPoints X = Set.univ
inst : Finite X
s : Set X
x : X
x✝ : x ∈ sᶜ
⊢ IsClosed {x}

Tactic:
rw [← mem_closedPoints_iff, this]

Result:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : JacobsonSpace X
h : (closedPoints X).Finite
this : closedPoints X = Set.univ
inst : Finite X
s : Set X
x : X
x✝ : x ∈ sᶜ
⊢ x ∈ Set.univ

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : JacobsonSpace X
h : (closedPoints X).Finite
this : closedPoints X = Set.univ
inst : Finite X
s : Set X
⊢ IsClosed (⋃ x ∈ sᶜ, {x})

Tactic:
refine sᶜ.toFinite.isClosed_biUnion fun x _ ↦ ?_

Result:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : JacobsonSpace X
h : (closedPoints X).Finite
this : closedPoints X = Set.univ
inst : Finite X
s : Set X
x : X
x✝ : x ∈ sᶜ
⊢ IsClosed {x}

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : JacobsonSpace X
h : (closedPoints X).Finite
this : closedPoints X = Set.univ
inst : Finite X
⊢ ∀ (s : Set X), IsOpen s

Tactic:
intro s

Result:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : JacobsonSpace X
h : (closedPoints X).Finite
this : closedPoints X = Set.univ
inst : Finite X
s : Set X
⊢ IsOpen s

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : JacobsonSpace X
h : (closedPoints X).Finite
this : closedPoints X = Set.univ
inst : Finite X
s : Set X
⊢ IsOpen s

Tactic:
rw [← isClosed_compl_iff, ← sᶜ.biUnion_of_singleton]

Result:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : JacobsonSpace X
h : (closedPoints X).Finite
this : closedPoints X = Set.univ
inst : Finite X
s : Set X
⊢ IsClosed (⋃ x ∈ sᶜ, {x})

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : JacobsonSpace X
h : (closedPoints X).Finite
⊢ closedPoints X = Set.univ

Tactic:
rw [← Set.univ_subset_iff, ← closure_closedPoints,
  closure_subset_iff_isClosed, ← (closedPoints X).biUnion_of_singleton]

Result:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : JacobsonSpace X
h : (closedPoints X).Finite
⊢ IsClosed (⋃ x ∈ closedPoints X, {x})