-- Mathlib/Topology/DiscreteSubset.lean
theorem isClosed_and_discrete_iff {S : Set X} :
    IsClosed S ∧ DiscreteTopology S ↔ ∀ x, Disjoint (𝓝[≠] x) (𝓟 S)

Proof state:
case a.mpr
X : Type u_1
inst✝ : TopologicalSpace X
S : Set X
x : X
H : Disjoint (𝓝[≠] x) (𝓟 S)
hx : x ∉ S
⊢ Disjoint (𝓝 x) (𝓟 S)

Tactic:
simpa [disjoint_iff, nhdsWithin, inf_assoc, hx] using H

Result:
no goals

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
S : Set X
⊢ IsClosed S ∧ DiscreteTopology ↑S ↔ ∀ (x : X), Disjoint (𝓝[≠] x) (𝓟 S)

Tactic:
rw [discreteTopology_subtype_iff, isClosed_iff_clusterPt, ← forall_and]

Result:
X : Type u_1
inst✝ : TopologicalSpace X
S : Set X
⊢ (∀ (x : X), (ClusterPt x (𝓟 S) → x ∈ S) ∧ (x ∈ S → 𝓝[≠] x ⊓ 𝓟 S = ⊥)) ↔ ∀ (x : X), Disjoint (𝓝[≠] x) (𝓟 S)

Proof state:
case a
X : Type u_1
inst✝ : TopologicalSpace X
S : Set X
x : X
⊢ (x ∉ S → Disjoint (𝓝 x) (𝓟 S)) ∧ (x ∈ S → Disjoint (𝓝[≠] x) (𝓟 S)) ↔ Disjoint (𝓝[≠] x) (𝓟 S)

Tactic:
constructor <;> intro H

Result:
case a.mp
X : Type u_1
inst✝ : TopologicalSpace X
S : Set X
x : X
H : (x ∉ S → Disjoint (𝓝 x) (𝓟 S)) ∧ (x ∈ S → Disjoint (𝓝[≠] x) (𝓟 S))
⊢ Disjoint (𝓝[≠] x) (𝓟 S)

case a.mpr
X : Type u_1
inst✝ : TopologicalSpace X
S : Set X
x : X
H : Disjoint (𝓝[≠] x) (𝓟 S)
⊢ (x ∉ S → Disjoint (𝓝 x) (𝓟 S)) ∧ (x ∈ S → Disjoint (𝓝[≠] x) (𝓟 S))

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
S : Set X
⊢ (∀ (x : X), (ClusterPt x (𝓟 S) → x ∈ S) ∧ (x ∈ S → 𝓝[≠] x ⊓ 𝓟 S = ⊥)) ↔ ∀ (x : X), Disjoint (𝓝[≠] x) (𝓟 S)

Tactic:
congrm (∀ x, ?_)

Result:
case a
X : Type u_1
inst✝ : TopologicalSpace X
S : Set X
x : X
⊢ (ClusterPt x (𝓟 S) → x ∈ S) ∧ (x ∈ S → 𝓝[≠] x ⊓ 𝓟 S = ⊥) ↔ Disjoint (𝓝[≠] x) (𝓟 S)

Proof state:
case a.mpr
X : Type u_1
inst✝ : TopologicalSpace X
S : Set X
x : X
H : Disjoint (𝓝[≠] x) (𝓟 S)
⊢ (x ∉ S → Disjoint (𝓝 x) (𝓟 S)) ∧ (x ∈ S → Disjoint (𝓝[≠] x) (𝓟 S))

Tactic:
refine ⟨fun hx ↦ ?_, fun _ ↦ H⟩

Result:
case a.mpr
X : Type u_1
inst✝ : TopologicalSpace X
S : Set X
x : X
H : Disjoint (𝓝[≠] x) (𝓟 S)
hx : x ∉ S
⊢ Disjoint (𝓝 x) (𝓟 S)

Proof state:
case a.mp
X : Type u_1
inst✝ : TopologicalSpace X
S : Set X
x : X
H : (x ∉ S → Disjoint (𝓝 x) (𝓟 S)) ∧ (x ∈ S → Disjoint (𝓝[≠] x) (𝓟 S))
⊢ Disjoint (𝓝[≠] x) (𝓟 S)

Tactic:
by_cases hx : x ∈ S

Result:
case pos
X : Type u_1
inst✝ : TopologicalSpace X
S : Set X
x : X
H : (x ∉ S → Disjoint (𝓝 x) (𝓟 S)) ∧ (x ∈ S → Disjoint (𝓝[≠] x) (𝓟 S))
hx : x ∈ S
⊢ Disjoint (𝓝[≠] x) (𝓟 S)

case neg
X : Type u_1
inst✝ : TopologicalSpace X
S : Set X
x : X
H : (x ∉ S → Disjoint (𝓝 x) (𝓟 S)) ∧ (x ∈ S → Disjoint (𝓝[≠] x) (𝓟 S))
hx : x ∉ S
⊢ Disjoint (𝓝[≠] x) (𝓟 S)

Proof state:
case pos
X : Type u_1
inst✝ : TopologicalSpace X
S : Set X
x : X
H : (x ∉ S → Disjoint (𝓝 x) (𝓟 S)) ∧ (x ∈ S → Disjoint (𝓝[≠] x) (𝓟 S))
hx : x ∈ S
⊢ Disjoint (𝓝[≠] x) (𝓟 S)

case neg
X : Type u_1
inst✝ : TopologicalSpace X
S : Set X
x : X
H : (x ∉ S → Disjoint (𝓝 x) (𝓟 S)) ∧ (x ∈ S → Disjoint (𝓝[≠] x) (𝓟 S))
hx : x ∉ S
⊢ Disjoint (𝓝[≠] x) (𝓟 S)

Tactic:
exacts [H.2 hx, (H.1 hx).mono_left nhdsWithin_le_nhds]

Result:
no goals

Proof state:
case a
X : Type u_1
inst✝ : TopologicalSpace X
S : Set X
x : X
⊢ (ClusterPt x (𝓟 S) → x ∈ S) ∧ (x ∈ S → 𝓝[≠] x ⊓ 𝓟 S = ⊥) ↔ Disjoint (𝓝[≠] x) (𝓟 S)

Tactic:
rw [← not_imp_not, clusterPt_iff_not_disjoint, not_not, ← disjoint_iff]

Result:
case a
X : Type u_1
inst✝ : TopologicalSpace X
S : Set X
x : X
⊢ (x ∉ S → Disjoint (𝓝 x) (𝓟 S)) ∧ (x ∈ S → Disjoint (𝓝[≠] x) (𝓟 S)) ↔ Disjoint (𝓝[≠] x) (𝓟 S)