-- 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)
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)
x✝ : IsOpen (closure s ↓∩ s)
H : IsOpen (closure s ↓∩ s) := x✝
⊢ IsLocallyClosed (range Subtype.val)

Tactic:
simpa using isClosed_closure.isLocallyClosed

Result:
no goals

Proof state:
case refine_1.intro.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)
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
x : { x // x ∈ closure s }
y : X
hy : y ∈ s
hxU : ↑x ∈ (fun h => U y h) hy
⊢ x ∈ closure s ↓∩ s

Tactic:
exact e y hy ⟨hxU, x.2⟩

Result:
no goals

Proof state:
case h.e'_3
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)
x✝ : IsOpen (closure s ↓∩ s)
H : IsOpen (closure s ↓∩ s) := x✝
⊢ s = ↑(closure s ↓∩ s)

Tactic:
simpa using subset_closure

Result:
no goals

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

Tactic:
nth_rw 1 [← hZ.closure_eq]

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

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 (coborder (U ∩ Z))

Tactic:
rw [coborder_eq_union_frontier_compl, inter_union_distrib_right, this,
  inter_univ]

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 (U ∪ (frontier (U ∩ Z))ᶜ)

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

Tactic:
rw [← compl_subset_iff_union, compl_subset_compl]

Result:
X : Type u_1
inst✝ : TopologicalSpace X
U Z : Set X
hU : IsOpen U
hZ : IsClosed Z
⊢ frontier (U ∩ Z) ⊆ closure 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' : IsClosed (t ↓∩ s)
U : Set X
hUt : U ⊆ t
hU : IsOpen U
hxU : x ∈ U
⊢ ∃ U, x ∈ U ∧ IsOpen U ∧ U ∩ closure s ⊆ s

Tactic:
rw [isClosed_preimage_val] at 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' : 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

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)
x✝ : IsOpen (closure s ↓∩ s)
H : IsOpen (closure s ↓∩ s) := x✝
⊢ IsLocallyClosed s

Tactic:
convert H.isLocallyClosed.image IsInducing.subtypeVal
  (by simpa using isClosed_closure.isLocallyClosed)

Result:
case h.e'_3
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)
x✝ : IsOpen (closure s ↓∩ s)
H : IsOpen (closure s ↓∩ s) := x✝
⊢ s = ↑(closure s ↓∩ s)

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
U Z : Set X
hU : IsOpen U
hZ : IsClosed Z
⊢ frontier (U ∩ Z) ⊆ closure Z

Tactic:
refine frontier_subset_closure.trans (closure_mono inter_subset_right)

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)
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)
⊢ [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 5 → 1
| H => by
  convert H.isLocallyClosed.image IsInducing.subtypeVal
    (by simpa using isClosed_closure.isLocallyClosed)
  simpa using subset_closure

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
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