-- Mathlib/Topology/LocallyClosed.lean
/--
A set `s` is locally closed if one of the equivalent conditions below hold
1. It is the intersection of some open set and some closed set.
2. The coborder `(closure s \ s)ᶜ` is open.
3. `s` is closed in some neighborhood of `x` for all `x ∈ s`.
4. Every `x ∈ s` has some open neighborhood `U` such that `U ∩ closure s ⊆ s`.
5. `s` is open in the closure of `s`.
-/
lemma isLocallyClosed_tfae (s : Set X) :
    List.TFAE
    [ IsLocallyClosed s,
      IsOpen (coborder s),
      ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsClosed (U ↓∩ s),
      ∀ x ∈ s, ∃ U, x ∈ U ∧ IsOpen U ∧ U ∩ closure s ⊆ s,
      IsOpen (closure s ↓∩ s)]

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
tfae_1_to_2 : IsLocallyClosed s → IsOpen (coborder s)
tfae_2_to_3 : IsOpen (coborder s) → ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsClosed (U ↓∩ s)
h : ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsClosed (U ↓∩ s)
x : X
hx : x ∈ s
⊢ ∃ U, x ∈ U ∧ IsOpen U ∧ U ∩ closure s ⊆ s

Tactic:
obtain ⟨t, ht, ht'⟩ := h x hx

Result:
case intro.intro
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
tfae_1_to_2 : IsLocallyClosed s → IsOpen (coborder s)
tfae_2_to_3 : IsOpen (coborder s) → ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsClosed (U ↓∩ s)
h : ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsClosed (U ↓∩ s)
x : X
hx : x ∈ s
t : Set X
ht : t ∈ 𝓝 x
ht' : IsClosed (t ↓∩ s)
⊢ ∃ U, x ∈ U ∧ IsOpen U ∧ U ∩ closure s ⊆ s

Proof state:
case intro.intro
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
tfae_1_to_2 : IsLocallyClosed s → IsOpen (coborder s)
tfae_2_to_3 : IsOpen (coborder s) → ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsClosed (U ↓∩ s)
h : ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsClosed (U ↓∩ s)
x : X
hx : x ∈ s
t : Set X
ht : t ∈ 𝓝 x
ht' : IsClosed (t ↓∩ s)
⊢ ∃ U, x ∈ U ∧ IsOpen U ∧ U ∩ closure s ⊆ s

Tactic:
obtain ⟨U, hUt, hU, hxU⟩ := mem_nhds_iff.mp ht

Result:
case intro.intro.intro.intro.intro
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
tfae_1_to_2 : IsLocallyClosed s → IsOpen (coborder s)
tfae_2_to_3 : IsOpen (coborder s) → ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsClosed (U ↓∩ s)
h : ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsClosed (U ↓∩ s)
x : X
hx : x ∈ s
t : Set X
ht : t ∈ 𝓝 x
ht' : IsClosed (t ↓∩ s)
U : Set X
hUt : U ⊆ t
hU : IsOpen U
hxU : x ∈ U
⊢ ∃ U, x ∈ U ∧ IsOpen U ∧ U ∩ closure s ⊆ s

Proof state:
case intro.intro.intro.intro
X : Type u_1
inst✝ : TopologicalSpace X
U Z : Set X
hU : IsOpen U
hZ : IsClosed Z
this : Z ∪ (frontier (U ∩ Z))ᶜ = univ
⊢ IsOpen (U ∪ (frontier (U ∩ Z))ᶜ)

Tactic:
exact hU.union isClosed_frontier.isOpen_compl

Result:
no goals

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ IsLocallyClosed s → IsOpen (coborder s)

Tactic:
rintro ⟨U, Z, hU, hZ, rfl⟩

Result:
case intro.intro.intro.intro
X : Type u_1
inst✝ : TopologicalSpace X
U Z : Set X
hU : IsOpen U
hZ : IsClosed Z
⊢ IsOpen (coborder (U ∩ Z))

Proof state:
case intro.intro.intro.intro.intro
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
tfae_1_to_2 : IsLocallyClosed s → IsOpen (coborder s)
tfae_2_to_3 : IsOpen (coborder s) → ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsClosed (U ↓∩ s)
h : ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsClosed (U ↓∩ s)
x : X
hx : x ∈ s
t : Set X
ht : t ∈ 𝓝 x
ht' : t ∩ closure (t ∩ s) ⊆ s
U : Set X
hUt : U ⊆ t
hU : IsOpen U
hxU : x ∈ U
⊢ ∃ U, x ∈ U ∧ IsOpen U ∧ U ∩ closure s ⊆ s

Tactic:
exact ⟨U, hxU, hU, (subset_inter (inter_subset_left.trans hUt) (hU.inter_closure.trans
  (closure_mono <| inter_subset_inter hUt subset_rfl))).trans ht'⟩

Result:
no goals

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
tfae_1_to_2 : IsLocallyClosed s → IsOpen (coborder s)
tfae_2_to_3 : IsOpen (coborder s) → ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsClosed (U ↓∩ s)
⊢ [IsLocallyClosed s, IsOpen (coborder s), ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsClosed (U ↓∩ s),
      ∀ x ∈ s, ∃ U, x ∈ U ∧ IsOpen U ∧ U ∩ closure s ⊆ s, IsOpen (closure s ↓∩ s)].TFAE

Tactic:
tfae_have 3 → 4
| h, x, hx => by
  obtain ⟨t, ht, ht'⟩ := h x hx
  obtain ⟨U, hUt, hU, hxU⟩ := mem_nhds_iff.mp ht
  rw [isClosed_preimage_val] at ht'
  exact ⟨U, hxU, hU, (subset_inter (inter_subset_left.trans hUt) (hU.inter_closure.trans
    (closure_mono <| inter_subset_inter hUt subset_rfl))).trans ht'⟩

Result:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
tfae_1_to_2 : IsLocallyClosed s → IsOpen (coborder s)
tfae_2_to_3 : IsOpen (coborder s) → ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsClosed (U ↓∩ s)
tfae_3_to_4 : (∀ x ∈ s, ∃ U ∈ 𝓝 x, IsClosed (U ↓∩ s)) → ∀ x ∈ s, ∃ U, x ∈ U ∧ IsOpen U ∧ U ∩ closure s ⊆ s
⊢ [IsLocallyClosed s, IsOpen (coborder s), ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsClosed (U ↓∩ s),
      ∀ x ∈ s, ∃ U, x ∈ U ∧ IsOpen U ∧ U ∩ closure s ⊆ s, IsOpen (closure s ↓∩ s)].TFAE

Proof state:
case intro.intro.intro.intro
X : Type u_1
inst✝ : TopologicalSpace X
U Z : Set X
hU : IsOpen U
hZ : IsClosed Z
⊢ IsOpen (coborder (U ∩ Z))

Tactic:
have : Z ∪ (frontier (U ∩ Z))ᶜ = univ := by
  nth_rw 1 [← hZ.closure_eq]
  rw [← compl_subset_iff_union, compl_subset_compl]
  refine frontier_subset_closure.trans (closure_mono inter_subset_right)

Result:
case intro.intro.intro.intro
X : Type u_1
inst✝ : TopologicalSpace X
U Z : Set X
hU : IsOpen U
hZ : IsClosed Z
this : Z ∪ (frontier (U ∩ Z))ᶜ = univ
⊢ IsOpen (coborder (U ∩ Z))

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
tfae_1_to_2 : IsLocallyClosed s → IsOpen (coborder s)
tfae_2_to_3 : IsOpen (coborder s) → ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsClosed (U ↓∩ s)
tfae_3_to_4 : (∀ x ∈ s, ∃ U ∈ 𝓝 x, IsClosed (U ↓∩ s)) → ∀ x ∈ s, ∃ U, x ∈ U ∧ IsOpen U ∧ U ∩ closure s ⊆ s
x✝ : ∀ x ∈ s, ∃ U, x ∈ U ∧ IsOpen U ∧ U ∩ closure s ⊆ s
H : ∀ x ∈ s, ∃ U, x ∈ U ∧ IsOpen U ∧ U ∩ closure s ⊆ s := x✝
⊢ IsOpen (closure s ↓∩ s)

Tactic:
choose U hxU hU e using H

Result:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
tfae_1_to_2 : IsLocallyClosed s → IsOpen (coborder s)
tfae_2_to_3 : IsOpen (coborder s) → ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsClosed (U ↓∩ s)
tfae_3_to_4 : (∀ x ∈ s, ∃ U ∈ 𝓝 x, IsClosed (U ↓∩ s)) → ∀ x ∈ s, ∃ U, x ∈ U ∧ IsOpen U ∧ U ∩ closure s ⊆ s
x✝ : ∀ x ∈ s, ∃ U, x ∈ U ∧ IsOpen U ∧ U ∩ closure s ⊆ s
U : (x : X) → x ∈ s → Set X
hxU : ∀ (x : X) (a : x ∈ s), x ∈ U x a
hU : ∀ (x : X) (a : x ∈ s), IsOpen (U x a)
e : ∀ (x : X) (a : x ∈ s), U x a ∩ closure s ⊆ s
⊢ IsOpen (closure s ↓∩ s)

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ [IsLocallyClosed s, IsOpen (coborder s), ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsClosed (U ↓∩ s),
      ∀ x ∈ s, ∃ U, x ∈ U ∧ IsOpen U ∧ U ∩ closure s ⊆ s, IsOpen (closure s ↓∩ s)].TFAE

Tactic:
tfae_have 1 → 2 := by
  rintro ⟨U, Z, hU, hZ, rfl⟩
  have : Z ∪ (frontier (U ∩ Z))ᶜ = univ := by
    nth_rw 1 [← hZ.closure_eq]
    rw [← compl_subset_iff_union, compl_subset_compl]
    refine frontier_subset_closure.trans (closure_mono inter_subset_right)
  rw [coborder_eq_union_frontier_compl, inter_union_distrib_right, this,
    inter_univ]
  exact hU.union isClosed_frontier.isOpen_compl

Result:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
tfae_1_to_2 : IsLocallyClosed s → IsOpen (coborder s)
⊢ [IsLocallyClosed s, IsOpen (coborder s), ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsClosed (U ↓∩ s),
      ∀ x ∈ s, ∃ U, x ∈ U ∧ IsOpen U ∧ U ∩ closure s ⊆ s, IsOpen (closure s ↓∩ s)].TFAE

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
tfae_1_to_2 : IsLocallyClosed s → IsOpen (coborder s)
tfae_2_to_3 : IsOpen (coborder s) → ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsClosed (U ↓∩ s)
tfae_3_to_4 : (∀ x ∈ s, ∃ U ∈ 𝓝 x, IsClosed (U ↓∩ s)) → ∀ x ∈ s, ∃ U, x ∈ U ∧ IsOpen U ∧ U ∩ closure s ⊆ s
tfae_4_to_5 : (∀ x ∈ s, ∃ U, x ∈ U ∧ IsOpen U ∧ U ∩ closure s ⊆ s) → IsOpen (closure s ↓∩ s)
tfae_5_to_1 : IsOpen (closure s ↓∩ s) → IsLocallyClosed s
⊢ [IsLocallyClosed s, IsOpen (coborder s), ∀ x ∈ s, ∃ U ∈ 𝓝 x, IsClosed (U ↓∩ s),
      ∀ x ∈ s, ∃ U, x ∈ U ∧ IsOpen U ∧ U ∩ closure s ⊆ s, IsOpen (closure s ↓∩ s)].TFAE

Tactic:
tfae_finish

Result:
no goals