-- Mathlib/Topology/DiscreteSubset.lean
lemma mem_codiscrete_subtype_iff_mem_codiscreteWithin {S : Set X} {U : Set S} :
    U ∈ codiscrete S ↔ (↑) '' U ∈ codiscreteWithin S

Proof state:
case h'.h.e'_5.h
X : Type u_1
inst✝ : TopologicalSpace X
S : Set X
U : Set ↑S
x : X
hx : x ∈ S
this : Tendsto Subtype.val (𝓝[≠] ⟨x, hx⟩) (𝓝[≠] x)
a✝ : (S \ Subtype.val '' U)ᶜ ∈ 𝓝[≠] x
x✝ : ↑S
⊢ x✝ ∈ U ↔ x✝ ∈ Subtype.val ⁻¹' (S \ Subtype.val '' U)ᶜ

Tactic:
simp

Result:
no goals

Proof state:
case a.h.h.a.mp.intro.intro
X : Type u_1
inst✝ : TopologicalSpace X
S : Set X
U : Set ↑S
x : X
hx : x ∈ S
t : Set X
ht1 : t ∈ 𝓝[Subtype.val '' {⟨x, hx⟩}ᶜ] ↑⟨x, hx⟩
ht2 : Subtype.val ⁻¹' t ⊆ U
⊢ (S \ Subtype.val '' U)ᶜ ∈ 𝓝[≠] x

Tactic:
rw [mem_nhdsWithin] at ht1 ⊢

Result:
case a.h.h.a.mp.intro.intro
X : Type u_1
inst✝ : TopologicalSpace X
S : Set X
U : Set ↑S
x : X
hx : x ∈ S
t : Set X
ht1 : ∃ u, IsOpen u ∧ ↑⟨x, hx⟩ ∈ u ∧ u ∩ Subtype.val '' {⟨x, hx⟩}ᶜ ⊆ t
ht2 : Subtype.val ⁻¹' t ⊆ U
⊢ ∃ u, IsOpen u ∧ x ∈ u ∧ u ∩ {x}ᶜ ⊆ (S \ Subtype.val '' U)ᶜ

Proof state:
case a.h.h.a.mp.intro.intro.intro.intro.intro
X : Type u_1
inst✝ : TopologicalSpace X
S : Set X
U : Set ↑S
x : X
hx : x ∈ S
t : Set X
ht2 : Subtype.val ⁻¹' t ⊆ U
u : Set X
hu1 : IsOpen u
hu2 : ↑⟨x, hx⟩ ∈ u
hu3 : u ∩ Subtype.val '' {⟨x, hx⟩}ᶜ ⊆ t
v : X
hv : v ∈ u ∩ {x}ᶜ
⊢ v ∈ (S \ Subtype.val '' U)ᶜ

Tactic:
simpa using fun hv2 ↦ ⟨hv2, ht2 <| hu3 <| by simpa [hv2]⟩

Result:
no goals

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
S : Set X
U : Set ↑S
x : X
hx : x ∈ S
⊢ ∀ x_1 ∈ {⟨x, hx⟩}ᶜ, ↑x_1 ∈ {x}ᶜ

Tactic:
simp

Result:
no goals

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
S : Set X
U : Set ↑S
x : X
hx : x ∈ S
this : Tendsto Subtype.val (𝓝[≠] ⟨x, hx⟩) (𝓝[≠] x)
⊢ (S \ Subtype.val '' U)ᶜ ∈ 𝓝[≠] x → U ∈ 𝓝[≠] ⟨x, hx⟩

Tactic:
convert tendsto_def.mp this _

Result:
case h'.h.e'_5
X : Type u_1
inst✝ : TopologicalSpace X
S : Set X
U : Set ↑S
x : X
hx : x ∈ S
this : Tendsto Subtype.val (𝓝[≠] ⟨x, hx⟩) (𝓝[≠] x)
a✝ : (S \ Subtype.val '' U)ᶜ ∈ 𝓝[≠] x
⊢ U = Subtype.val ⁻¹' (S \ Subtype.val '' U)ᶜ

Proof state:
case h'.h.e'_5
X : Type u_1
inst✝ : TopologicalSpace X
S : Set X
U : Set ↑S
x : X
hx : x ∈ S
this : Tendsto Subtype.val (𝓝[≠] ⟨x, hx⟩) (𝓝[≠] x)
a✝ : (S \ Subtype.val '' U)ᶜ ∈ 𝓝[≠] x
⊢ U = Subtype.val ⁻¹' (S \ Subtype.val '' U)ᶜ

Tactic:
ext

Result:
case h'.h.e'_5.h
X : Type u_1
inst✝ : TopologicalSpace X
S : Set X
U : Set ↑S
x : X
hx : x ∈ S
this : Tendsto Subtype.val (𝓝[≠] ⟨x, hx⟩) (𝓝[≠] x)
a✝ : (S \ Subtype.val '' U)ᶜ ∈ 𝓝[≠] x
x✝ : ↑S
⊢ x✝ ∈ U ↔ x✝ ∈ Subtype.val ⁻¹' (S \ Subtype.val '' U)ᶜ

Proof state:
case a.h.h.a.mp
X : Type u_1
inst✝ : TopologicalSpace X
S : Set X
U : Set ↑S
x : X
hx : x ∈ S
⊢ (∃ t ∈ 𝓝[Subtype.val '' {⟨x, hx⟩}ᶜ] ↑⟨x, hx⟩, Subtype.val ⁻¹' t ⊆ U) → (S \ Subtype.val '' U)ᶜ ∈ 𝓝[≠] x

Tactic:
rintro ⟨t, ht1, ht2⟩

Result:
case a.h.h.a.mp.intro.intro
X : Type u_1
inst✝ : TopologicalSpace X
S : Set X
U : Set ↑S
x : X
hx : x ∈ S
t : Set X
ht1 : t ∈ 𝓝[Subtype.val '' {⟨x, hx⟩}ᶜ] ↑⟨x, hx⟩
ht2 : Subtype.val ⁻¹' t ⊆ U
⊢ (S \ Subtype.val '' U)ᶜ ∈ 𝓝[≠] x

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
S : Set X
U : Set ↑S
⊢ U ∈ codiscrete ↑S ↔ Subtype.val '' U ∈ codiscreteWithin S

Tactic:
simp [mem_codiscrete, disjoint_principal_right, compl_compl, Subtype.forall,
  mem_codiscreteWithin]

Result:
X : Type u_1
inst✝ : TopologicalSpace X
S : Set X
U : Set ↑S
⊢ (∀ (a : X) (b : a ∈ S), U ∈ 𝓝[≠] ⟨a, b⟩) ↔ ∀ x ∈ S, (S \ Subtype.val '' U)ᶜ ∈ 𝓝[≠] x

Proof state:
case a.h.h.a
X : Type u_1
inst✝ : TopologicalSpace X
S : Set X
U : Set ↑S
x : X
hx : x ∈ S
⊢ U ∈ 𝓝[≠] ⟨x, hx⟩ ↔ (S \ Subtype.val '' U)ᶜ ∈ 𝓝[≠] x

Tactic:
constructor

Result:
case a.h.h.a.mp
X : Type u_1
inst✝ : TopologicalSpace X
S : Set X
U : Set ↑S
x : X
hx : x ∈ S
⊢ U ∈ 𝓝[≠] ⟨x, hx⟩ → (S \ Subtype.val '' U)ᶜ ∈ 𝓝[≠] x

case a.h.h.a.mpr
X : Type u_1
inst✝ : TopologicalSpace X
S : Set X
U : Set ↑S
x : X
hx : x ∈ S
⊢ (S \ Subtype.val '' U)ᶜ ∈ 𝓝[≠] x → U ∈ 𝓝[≠] ⟨x, hx⟩

Proof state:
case a.h.h.a.mp.intro.intro
X : Type u_1
inst✝ : TopologicalSpace X
S : Set X
U : Set ↑S
x : X
hx : x ∈ S
t : Set X
ht1 : ∃ u, IsOpen u ∧ ↑⟨x, hx⟩ ∈ u ∧ u ∩ Subtype.val '' {⟨x, hx⟩}ᶜ ⊆ t
ht2 : Subtype.val ⁻¹' t ⊆ U
⊢ ∃ u, IsOpen u ∧ x ∈ u ∧ u ∩ {x}ᶜ ⊆ (S \ Subtype.val '' U)ᶜ

Tactic:
obtain ⟨u, hu1, hu2, hu3⟩ := ht1

Result:
case a.h.h.a.mp.intro.intro.intro.intro.intro
X : Type u_1
inst✝ : TopologicalSpace X
S : Set X
U : Set ↑S
x : X
hx : x ∈ S
t : Set X
ht2 : Subtype.val ⁻¹' t ⊆ U
u : Set X
hu1 : IsOpen u
hu2 : ↑⟨x, hx⟩ ∈ u
hu3 : u ∩ Subtype.val '' {⟨x, hx⟩}ᶜ ⊆ t
⊢ ∃ u, IsOpen u ∧ x ∈ u ∧ u ∩ {x}ᶜ ⊆ (S \ Subtype.val '' U)ᶜ

Proof state:
case a.h.h.a.mpr
X : Type u_1
inst✝ : TopologicalSpace X
S : Set X
U : Set ↑S
x : X
hx : x ∈ S
⊢ (S \ Subtype.val '' U)ᶜ ∈ 𝓝[≠] x → U ∈ 𝓝[≠] ⟨x, hx⟩

Tactic:
suffices Tendsto (↑) (𝓝[≠] (⟨x, hx⟩ : S)) (𝓝[≠] x) by convert tendsto_def.mp this _; ext; simp

Result:
case a.h.h.a.mpr
X : Type u_1
inst✝ : TopologicalSpace X
S : Set X
U : Set ↑S
x : X
hx : x ∈ S
⊢ Tendsto Subtype.val (𝓝[≠] ⟨x, hx⟩) (𝓝[≠] x)

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
S : Set X
U : Set ↑S
x : X
hx : x ∈ S
t : Set X
ht2 : Subtype.val ⁻¹' t ⊆ U
u : Set X
hu1 : IsOpen u
hu2 : ↑⟨x, hx⟩ ∈ u
hu3 : u ∩ Subtype.val '' {⟨x, hx⟩}ᶜ ⊆ t
v : X
hv : v ∈ u ∩ {x}ᶜ
hv2 : v ∈ S
⊢ ↑⟨v, ⋯⟩ ∈ u ∩ Subtype.val '' {⟨x, hx⟩}ᶜ

Tactic:
simpa [hv2]

Result:
no goals

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
S : Set X
U : Set ↑S
⊢ (∀ (a : X) (b : a ∈ S), U ∈ 𝓝[≠] ⟨a, b⟩) ↔ ∀ x ∈ S, (S \ Subtype.val '' U)ᶜ ∈ 𝓝[≠] x

Tactic:
congr! with x hx

Result:
case a.h.h.a
X : Type u_1
inst✝ : TopologicalSpace X
S : Set X
U : Set ↑S
x : X
hx : x ∈ S
⊢ U ∈ 𝓝[≠] ⟨x, hx⟩ ↔ (S \ Subtype.val '' U)ᶜ ∈ 𝓝[≠] x

Proof state:
case a.h.h.a.mp
X : Type u_1
inst✝ : TopologicalSpace X
S : Set X
U : Set ↑S
x : X
hx : x ∈ S
⊢ U ∈ 𝓝[≠] ⟨x, hx⟩ → (S \ Subtype.val '' U)ᶜ ∈ 𝓝[≠] x

Tactic:
rw [nhdsWithin_subtype, mem_comap]

Result:
case a.h.h.a.mp
X : Type u_1
inst✝ : TopologicalSpace X
S : Set X
U : Set ↑S
x : X
hx : x ∈ S
⊢ (∃ t ∈ 𝓝[Subtype.val '' {⟨x, hx⟩}ᶜ] ↑⟨x, hx⟩, Subtype.val ⁻¹' t ⊆ U) → (S \ Subtype.val '' U)ᶜ ∈ 𝓝[≠] x

Proof state:
case a.h.h.a.mp.intro.intro.intro.intro.intro
X : Type u_1
inst✝ : TopologicalSpace X
S : Set X
U : Set ↑S
x : X
hx : x ∈ S
t : Set X
ht2 : Subtype.val ⁻¹' t ⊆ U
u : Set X
hu1 : IsOpen u
hu2 : ↑⟨x, hx⟩ ∈ u
hu3 : u ∩ Subtype.val '' {⟨x, hx⟩}ᶜ ⊆ t
⊢ ∃ u, IsOpen u ∧ x ∈ u ∧ u ∩ {x}ᶜ ⊆ (S \ Subtype.val '' U)ᶜ

Tactic:
refine ⟨u, hu1, hu2, fun v hv ↦ ?_⟩

Result:
case a.h.h.a.mp.intro.intro.intro.intro.intro
X : Type u_1
inst✝ : TopologicalSpace X
S : Set X
U : Set ↑S
x : X
hx : x ∈ S
t : Set X
ht2 : Subtype.val ⁻¹' t ⊆ U
u : Set X
hu1 : IsOpen u
hu2 : ↑⟨x, hx⟩ ∈ u
hu3 : u ∩ Subtype.val '' {⟨x, hx⟩}ᶜ ⊆ t
v : X
hv : v ∈ u ∩ {x}ᶜ
⊢ v ∈ (S \ Subtype.val '' U)ᶜ

Proof state:
case a.h.h.a.mpr
X : Type u_1
inst✝ : TopologicalSpace X
S : Set X
U : Set ↑S
x : X
hx : x ∈ S
⊢ Tendsto Subtype.val (𝓝[≠] ⟨x, hx⟩) (𝓝[≠] x)

Tactic:
exact tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within _
  continuous_subtype_val.continuousWithinAt <| eventually_mem_nhdsWithin.mono (by simp)

Result:
no goals