-- Mathlib/Topology/LocallyConstant/Basic.lean
theorem tfae (f : X → Y) :
    TFAE [IsLocallyConstant f,
      ∀ x, ∀ᶠ x' in 𝓝 x, f x' = f x,
      ∀ x, IsOpen { x' | f x' = f x },
      ∀ y, IsOpen (f ⁻¹' {y}),
      ∀ x, ∃ U : Set X, IsOpen U ∧ x ∈ U ∧ ∀ x' ∈ U, f x' = f x]

Proof state:
X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
f : X → Y
tfae_1_to_4 : IsLocallyConstant f → ∀ (y : Y), IsOpen (f ⁻¹' {y})
⊢ [IsLocallyConstant f, ∀ (x : X), ∀ᶠ (x' : X) in 𝓝 x, f x' = f x, ∀ (x : X), IsOpen {x' | f x' = f x},
      ∀ (y : Y), IsOpen (f ⁻¹' {y}), ∀ (x : X), ∃ U, IsOpen U ∧ x ∈ U ∧ ∀ x' ∈ U, f x' = f x].TFAE

Tactic:
tfae_have 4 → 3 := fun h x => h (f x)

Result:
X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
f : X → Y
tfae_1_to_4 : IsLocallyConstant f → ∀ (y : Y), IsOpen (f ⁻¹' {y})
tfae_4_to_3 : (∀ (y : Y), IsOpen (f ⁻¹' {y})) → ∀ (x : X), IsOpen {x' | f x' = f x}
⊢ [IsLocallyConstant f, ∀ (x : X), ∀ᶠ (x' : X) in 𝓝 x, f x' = f x, ∀ (x : X), IsOpen {x' | f x' = f x},
      ∀ (y : Y), IsOpen (f ⁻¹' {y}), ∀ (x : X), ∃ U, IsOpen U ∧ x ∈ U ∧ ∀ x' ∈ U, f x' = f x].TFAE

Proof state:
case intro.intro.intro
X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
f : X → Y
tfae_1_to_4 : IsLocallyConstant f → ∀ (y : Y), IsOpen (f ⁻¹' {y})
tfae_4_to_3 : (∀ (y : Y), IsOpen (f ⁻¹' {y})) → ∀ (x : X), IsOpen {x' | f x' = f x}
tfae_3_to_2 : (∀ (x : X), IsOpen {x' | f x' = f x}) → ∀ (x : X), ∀ᶠ (x' : X) in 𝓝 x, f x' = f x
tfae_2_to_5 : (∀ (x : X), ∀ᶠ (x' : X) in 𝓝 x, f x' = f x) → ∀ (x : X), ∃ U, IsOpen U ∧ x ∈ U ∧ ∀ x' ∈ U, f x' = f x
h : ∀ (x : X), ∃ U, IsOpen U ∧ x ∈ U ∧ ∀ x' ∈ U, f x' = f x
s : Set Y
x : X
hx : x ∈ f ⁻¹' s
U : Set X
hU : IsOpen U
hxU : x ∈ U
eq : ∀ x' ∈ U, f x' = f x
⊢ ∃ t ⊆ f ⁻¹' s, IsOpen t ∧ x ∈ t

Tactic:
exact ⟨U, fun x' hx' => mem_preimage.2 <| (eq x' hx').symm ▸ hx, hU, hxU⟩

Result:
no goals

Proof state:
case intro.intro.intro
X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
f : X → Y
tfae_1_to_4 : IsLocallyConstant f → ∀ (y : Y), IsOpen (f ⁻¹' {y})
tfae_4_to_3 : (∀ (y : Y), IsOpen (f ⁻¹' {y})) → ∀ (x : X), IsOpen {x' | f x' = f x}
tfae_3_to_2 : (∀ (x : X), IsOpen {x' | f x' = f x}) → ∀ (x : X), ∀ᶠ (x' : X) in 𝓝 x, f x' = f x
h : ∀ (x : X), ∀ᶠ (x' : X) in 𝓝 x, f x' = f x
x : X
U : Set X
eq : U ⊆ {x_1 | (fun x' => f x' = f x) x_1}
hU : IsOpen U
hx : x ∈ U
⊢ ∃ U, IsOpen U ∧ x ∈ U ∧ ∀ x' ∈ U, f x' = f x

Tactic:
exact ⟨U, hU, hx, eq⟩

Result:
no goals

Proof state:
X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
f : X → Y
tfae_1_to_4 : IsLocallyConstant f → ∀ (y : Y), IsOpen (f ⁻¹' {y})
tfae_4_to_3 : (∀ (y : Y), IsOpen (f ⁻¹' {y})) → ∀ (x : X), IsOpen {x' | f x' = f x}
tfae_3_to_2 : (∀ (x : X), IsOpen {x' | f x' = f x}) → ∀ (x : X), ∀ᶠ (x' : X) in 𝓝 x, f x' = f x
tfae_2_to_5 : (∀ (x : X), ∀ᶠ (x' : X) in 𝓝 x, f x' = f x) → ∀ (x : X), ∃ U, IsOpen U ∧ x ∈ U ∧ ∀ x' ∈ U, f x' = f x
h : ∀ (x : X), ∃ U, IsOpen U ∧ x ∈ U ∧ ∀ x' ∈ U, f x' = f x
s : Set Y
⊢ IsOpen (f ⁻¹' s)

Tactic:
refine isOpen_iff_forall_mem_open.2 fun x hx ↦ ?_

Result:
X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
f : X → Y
tfae_1_to_4 : IsLocallyConstant f → ∀ (y : Y), IsOpen (f ⁻¹' {y})
tfae_4_to_3 : (∀ (y : Y), IsOpen (f ⁻¹' {y})) → ∀ (x : X), IsOpen {x' | f x' = f x}
tfae_3_to_2 : (∀ (x : X), IsOpen {x' | f x' = f x}) → ∀ (x : X), ∀ᶠ (x' : X) in 𝓝 x, f x' = f x
tfae_2_to_5 : (∀ (x : X), ∀ᶠ (x' : X) in 𝓝 x, f x' = f x) → ∀ (x : X), ∃ U, IsOpen U ∧ x ∈ U ∧ ∀ x' ∈ U, f x' = f x
h : ∀ (x : X), ∃ U, IsOpen U ∧ x ∈ U ∧ ∀ x' ∈ U, f x' = f x
s : Set Y
x : X
hx : x ∈ f ⁻¹' s
⊢ ∃ t ⊆ f ⁻¹' s, IsOpen t ∧ x ∈ t

Proof state:
X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
f : X → Y
tfae_1_to_4 : IsLocallyConstant f → ∀ (y : Y), IsOpen (f ⁻¹' {y})
tfae_4_to_3 : (∀ (y : Y), IsOpen (f ⁻¹' {y})) → ∀ (x : X), IsOpen {x' | f x' = f x}
⊢ [IsLocallyConstant f, ∀ (x : X), ∀ᶠ (x' : X) in 𝓝 x, f x' = f x, ∀ (x : X), IsOpen {x' | f x' = f x},
      ∀ (y : Y), IsOpen (f ⁻¹' {y}), ∀ (x : X), ∃ U, IsOpen U ∧ x ∈ U ∧ ∀ x' ∈ U, f x' = f x].TFAE

Tactic:
tfae_have 3 → 2 := fun h x => IsOpen.mem_nhds (h x) rfl

Result:
X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
f : X → Y
tfae_1_to_4 : IsLocallyConstant f → ∀ (y : Y), IsOpen (f ⁻¹' {y})
tfae_4_to_3 : (∀ (y : Y), IsOpen (f ⁻¹' {y})) → ∀ (x : X), IsOpen {x' | f x' = f x}
tfae_3_to_2 : (∀ (x : X), IsOpen {x' | f x' = f x}) → ∀ (x : X), ∀ᶠ (x' : X) in 𝓝 x, f x' = f x
⊢ [IsLocallyConstant f, ∀ (x : X), ∀ᶠ (x' : X) in 𝓝 x, f x' = f x, ∀ (x : X), IsOpen {x' | f x' = f x},
      ∀ (y : Y), IsOpen (f ⁻¹' {y}), ∀ (x : X), ∃ U, IsOpen U ∧ x ∈ U ∧ ∀ x' ∈ U, f x' = f x].TFAE

Proof state:
X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
f : X → Y
tfae_1_to_4 : IsLocallyConstant f → ∀ (y : Y), IsOpen (f ⁻¹' {y})
tfae_4_to_3 : (∀ (y : Y), IsOpen (f ⁻¹' {y})) → ∀ (x : X), IsOpen {x' | f x' = f x}
tfae_3_to_2 : (∀ (x : X), IsOpen {x' | f x' = f x}) → ∀ (x : X), ∀ᶠ (x' : X) in 𝓝 x, f x' = f x
tfae_2_to_5 : (∀ (x : X), ∀ᶠ (x' : X) in 𝓝 x, f x' = f x) → ∀ (x : X), ∃ U, IsOpen U ∧ x ∈ U ∧ ∀ x' ∈ U, f x' = f x
tfae_5_to_1 : (∀ (x : X), ∃ U, IsOpen U ∧ x ∈ U ∧ ∀ x' ∈ U, f x' = f x) → IsLocallyConstant f
⊢ [IsLocallyConstant f, ∀ (x : X), ∀ᶠ (x' : X) in 𝓝 x, f x' = f x, ∀ (x : X), IsOpen {x' | f x' = f x},
      ∀ (y : Y), IsOpen (f ⁻¹' {y}), ∀ (x : X), ∃ U, IsOpen U ∧ x ∈ U ∧ ∀ x' ∈ U, f x' = f x].TFAE

Tactic:
tfae_finish

Result:
no goals

Proof state:
X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
f : X → Y
tfae_1_to_4 : IsLocallyConstant f → ∀ (y : Y), IsOpen (f ⁻¹' {y})
tfae_4_to_3 : (∀ (y : Y), IsOpen (f ⁻¹' {y})) → ∀ (x : X), IsOpen {x' | f x' = f x}
tfae_3_to_2 : (∀ (x : X), IsOpen {x' | f x' = f x}) → ∀ (x : X), ∀ᶠ (x' : X) in 𝓝 x, f x' = f x
h : ∀ (x : X), ∀ᶠ (x' : X) in 𝓝 x, f x' = f x
x : X
⊢ ∃ U, IsOpen U ∧ x ∈ U ∧ ∀ x' ∈ U, f x' = f x

Tactic:
rcases mem_nhds_iff.1 (h x) with ⟨U, eq, hU, hx⟩

Result:
case intro.intro.intro
X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
f : X → Y
tfae_1_to_4 : IsLocallyConstant f → ∀ (y : Y), IsOpen (f ⁻¹' {y})
tfae_4_to_3 : (∀ (y : Y), IsOpen (f ⁻¹' {y})) → ∀ (x : X), IsOpen {x' | f x' = f x}
tfae_3_to_2 : (∀ (x : X), IsOpen {x' | f x' = f x}) → ∀ (x : X), ∀ᶠ (x' : X) in 𝓝 x, f x' = f x
h : ∀ (x : X), ∀ᶠ (x' : X) in 𝓝 x, f x' = f x
x : X
U : Set X
eq : U ⊆ {x_1 | (fun x' => f x' = f x) x_1}
hU : IsOpen U
hx : x ∈ U
⊢ ∃ U, IsOpen U ∧ x ∈ U ∧ ∀ x' ∈ U, f x' = f x

Proof state:
X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
f : X → Y
tfae_1_to_4 : IsLocallyConstant f → ∀ (y : Y), IsOpen (f ⁻¹' {y})
tfae_4_to_3 : (∀ (y : Y), IsOpen (f ⁻¹' {y})) → ∀ (x : X), IsOpen {x' | f x' = f x}
tfae_3_to_2 : (∀ (x : X), IsOpen {x' | f x' = f x}) → ∀ (x : X), ∀ᶠ (x' : X) in 𝓝 x, f x' = f x
tfae_2_to_5 : (∀ (x : X), ∀ᶠ (x' : X) in 𝓝 x, f x' = f x) → ∀ (x : X), ∃ U, IsOpen U ∧ x ∈ U ∧ ∀ x' ∈ U, f x' = f x
h : ∀ (x : X), ∃ U, IsOpen U ∧ x ∈ U ∧ ∀ x' ∈ U, f x' = f x
s : Set Y
x : X
hx : x ∈ f ⁻¹' s
⊢ ∃ t ⊆ f ⁻¹' s, IsOpen t ∧ x ∈ t

Tactic:
rcases h x with ⟨U, hU, hxU, eq⟩

Result:
case intro.intro.intro
X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
f : X → Y
tfae_1_to_4 : IsLocallyConstant f → ∀ (y : Y), IsOpen (f ⁻¹' {y})
tfae_4_to_3 : (∀ (y : Y), IsOpen (f ⁻¹' {y})) → ∀ (x : X), IsOpen {x' | f x' = f x}
tfae_3_to_2 : (∀ (x : X), IsOpen {x' | f x' = f x}) → ∀ (x : X), ∀ᶠ (x' : X) in 𝓝 x, f x' = f x
tfae_2_to_5 : (∀ (x : X), ∀ᶠ (x' : X) in 𝓝 x, f x' = f x) → ∀ (x : X), ∃ U, IsOpen U ∧ x ∈ U ∧ ∀ x' ∈ U, f x' = f x
h : ∀ (x : X), ∃ U, IsOpen U ∧ x ∈ U ∧ ∀ x' ∈ U, f x' = f x
s : Set Y
x : X
hx : x ∈ f ⁻¹' s
U : Set X
hU : IsOpen U
hxU : x ∈ U
eq : ∀ x' ∈ U, f x' = f x
⊢ ∃ t ⊆ f ⁻¹' s, IsOpen t ∧ x ∈ t