-- Mathlib/Topology/Separation/Hausdorff.lean
theorem Set.InjOn.exists_mem_nhdsSet {X Y : Type*} [TopologicalSpace X] [TopologicalSpace Y]
    [T2Space Y] {f : X → Y} {s : Set X} (inj : InjOn f s) (sc : IsCompact s)
    (fc : ∀ x ∈ s, ContinuousAt f x) (loc : ∀ x ∈ s, ∃ u ∈ 𝓝 x, InjOn f u) :
    ∃ t ∈ 𝓝ˢ s, InjOn f t

Proof state:
case inr
X : Type u_3
Y : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : T2Space Y
f : X → Y
s : Set X
inj : InjOn f s
sc : IsCompact s
fc : ∀ x ∈ s, ContinuousAt f x
loc : ∀ x ∈ s, ∃ u ∈ 𝓝 x, InjOn f u
x✝¹ : X × X
x y : X
x✝ : (x, y) ∈ s ×ˢ s
hx : (x, y).1 ∈ s
hy : (x, y).2 ∈ s
hne : x ≠ y
⊢ ∀ᶠ (y : X × X) in 𝓝 (x, y), f y.1 = f y.2 → y.1 = y.2

Tactic:
suffices ∀ᶠ z in 𝓝 (x, y), f z.1 ≠ f z.2 from this.mono fun _ hne h ↦ absurd h hne

Result:
case inr
X : Type u_3
Y : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : T2Space Y
f : X → Y
s : Set X
inj : InjOn f s
sc : IsCompact s
fc : ∀ x ∈ s, ContinuousAt f x
loc : ∀ x ∈ s, ∃ u ∈ 𝓝 x, InjOn f u
x✝¹ : X × X
x y : X
x✝ : (x, y) ∈ s ×ˢ s
hx : (x, y).1 ∈ s
hy : (x, y).2 ∈ s
hne : x ≠ y
⊢ ∀ᶠ (z : X × X) in 𝓝 (x, y), f z.1 ≠ f z.2

Proof state:
X : Type u_3
Y : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : T2Space Y
f : X → Y
s : Set X
inj : InjOn f s
sc : IsCompact s
fc : ∀ x ∈ s, ContinuousAt f x
loc : ∀ x ∈ s, ∃ u ∈ 𝓝 x, InjOn f u
x✝¹ : X × X
x y : X
x✝ : (x, y) ∈ s ×ˢ s
hx : (x, y).1 ∈ s
hy : (x, y).2 ∈ s
⊢ ∀ᶠ (y : X × X) in 𝓝 (x, y), f y.1 = f y.2 → y.1 = y.2

Tactic:
rcases eq_or_ne x y with rfl | hne

Result:
case inl
X : Type u_3
Y : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : T2Space Y
f : X → Y
s : Set X
inj : InjOn f s
sc : IsCompact s
fc : ∀ x ∈ s, ContinuousAt f x
loc : ∀ x ∈ s, ∃ u ∈ 𝓝 x, InjOn f u
x✝¹ : X × X
x : X
x✝ : (x, x) ∈ s ×ˢ s
hx : (x, x).1 ∈ s
hy : (x, x).2 ∈ s
⊢ ∀ᶠ (y : X × X) in 𝓝 (x, x), f y.1 = f y.2 → y.1 = y.2

case inr
X : Type u_3
Y : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : T2Space Y
f : X → Y
s : Set X
inj : InjOn f s
sc : IsCompact s
fc : ∀ x ∈ s, ContinuousAt f x
loc : ∀ x ∈ s, ∃ u ∈ 𝓝 x, InjOn f u
x✝¹ : X × X
x y : X
x✝ : (x, y) ∈ s ×ˢ s
hx : (x, y).1 ∈ s
hy : (x, y).2 ∈ s
hne : x ≠ y
⊢ ∀ᶠ (y : X × X) in 𝓝 (x, y), f y.1 = f y.2 → y.1 = y.2

Proof state:
X : Type u_3
Y : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : T2Space Y
f : X → Y
s : Set X
inj : InjOn f s
sc : IsCompact s
fc : ∀ x ∈ s, ContinuousAt f x
loc : ∀ x ∈ s, ∃ u ∈ 𝓝 x, InjOn f u
this : ∀ x ∈ s ×ˢ s, ∀ᶠ (y : X × X) in 𝓝 x, f y.1 = f y.2 → y.1 = y.2
⊢ ∃ t ∈ 𝓝ˢ s, InjOn f t

Tactic:
rw [← eventually_nhdsSet_iff_forall, sc.nhdsSet_prod_eq sc] at this

Result:
X : Type u_3
Y : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : T2Space Y
f : X → Y
s : Set X
inj : InjOn f s
sc : IsCompact s
fc : ∀ x ∈ s, ContinuousAt f x
loc : ∀ x ∈ s, ∃ u ∈ 𝓝 x, InjOn f u
this : ∀ᶠ (x : X × X) in 𝓝ˢ s ×ˢ 𝓝ˢ s, f x.1 = f x.2 → x.1 = x.2
⊢ ∃ t ∈ 𝓝ˢ s, InjOn f t

Proof state:
case inr
X : Type u_3
Y : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : T2Space Y
f : X → Y
s : Set X
inj : InjOn f s
sc : IsCompact s
fc : ∀ x ∈ s, ContinuousAt f x
loc : ∀ x ∈ s, ∃ u ∈ 𝓝 x, InjOn f u
x✝¹ : X × X
x y : X
x✝ : (x, y) ∈ s ×ˢ s
hx : (x, y).1 ∈ s
hy : (x, y).2 ∈ s
hne : x ≠ y
⊢ Prod.map f f (x, y) ∈ (diagonal Y)ᶜ

Tactic:
exact inj.ne hx hy hne

Result:
no goals

Proof state:
case inr
X : Type u_3
Y : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : T2Space Y
f : X → Y
s : Set X
inj : InjOn f s
sc : IsCompact s
fc : ∀ x ∈ s, ContinuousAt f x
loc : ∀ x ∈ s, ∃ u ∈ 𝓝 x, InjOn f u
x✝¹ : X × X
x y : X
x✝ : (x, y) ∈ s ×ˢ s
hx : (x, y).1 ∈ s
hy : (x, y).2 ∈ s
hne : x ≠ y
⊢ ∀ᶠ (z : X × X) in 𝓝 (x, y), f z.1 ≠ f z.2

Tactic:
refine (fc x hx).prodMap' (fc y hy) <| isClosed_diagonal.isOpen_compl.mem_nhds ?_

Result:
case inr
X : Type u_3
Y : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : T2Space Y
f : X → Y
s : Set X
inj : InjOn f s
sc : IsCompact s
fc : ∀ x ∈ s, ContinuousAt f x
loc : ∀ x ∈ s, ∃ u ∈ 𝓝 x, InjOn f u
x✝¹ : X × X
x y : X
x✝ : (x, y) ∈ s ×ˢ s
hx : (x, y).1 ∈ s
hy : (x, y).2 ∈ s
hne : x ≠ y
⊢ Prod.map f f (x, y) ∈ (diagonal Y)ᶜ

Proof state:
X : Type u_3
Y : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : T2Space Y
f : X → Y
s : Set X
inj : InjOn f s
sc : IsCompact s
fc : ∀ x ∈ s, ContinuousAt f x
loc : ∀ x ∈ s, ∃ u ∈ 𝓝 x, InjOn f u
this : ∀ᶠ (x : X × X) in 𝓝ˢ s ×ˢ 𝓝ˢ s, f x.1 = f x.2 → x.1 = x.2
⊢ ∃ t ∈ 𝓝ˢ s, InjOn f t

Tactic:
exact eventually_prod_self_iff.1 this

Result:
no goals

Proof state:
case inl.intro.intro
X : Type u_3
Y : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : T2Space Y
f : X → Y
s : Set X
inj : InjOn f s
sc : IsCompact s
fc : ∀ x ∈ s, ContinuousAt f x
loc : ∀ x ∈ s, ∃ u ∈ 𝓝 x, InjOn f u
x✝¹ : X × X
x : X
x✝ : (x, x) ∈ s ×ˢ s
hx : (x, x).1 ∈ s
hy : (x, x).2 ∈ s
u : Set X
hu : u ∈ 𝓝 x
hf : InjOn f u
⊢ ∀ᶠ (y : X × X) in 𝓝 (x, x), f y.1 = f y.2 → y.1 = y.2

Tactic:
exact Filter.mem_of_superset (prod_mem_nhds hu hu) <| forall_prod_set.2 hf

Result:
no goals

Proof state:
case inl
X : Type u_3
Y : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : T2Space Y
f : X → Y
s : Set X
inj : InjOn f s
sc : IsCompact s
fc : ∀ x ∈ s, ContinuousAt f x
loc : ∀ x ∈ s, ∃ u ∈ 𝓝 x, InjOn f u
x✝¹ : X × X
x : X
x✝ : (x, x) ∈ s ×ˢ s
hx : (x, x).1 ∈ s
hy : (x, x).2 ∈ s
⊢ ∀ᶠ (y : X × X) in 𝓝 (x, x), f y.1 = f y.2 → y.1 = y.2

Tactic:
rcases loc x hx with ⟨u, hu, hf⟩

Result:
case inl.intro.intro
X : Type u_3
Y : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : T2Space Y
f : X → Y
s : Set X
inj : InjOn f s
sc : IsCompact s
fc : ∀ x ∈ s, ContinuousAt f x
loc : ∀ x ∈ s, ∃ u ∈ 𝓝 x, InjOn f u
x✝¹ : X × X
x : X
x✝ : (x, x) ∈ s ×ˢ s
hx : (x, x).1 ∈ s
hy : (x, x).2 ∈ s
u : Set X
hu : u ∈ 𝓝 x
hf : InjOn f u
⊢ ∀ᶠ (y : X × X) in 𝓝 (x, x), f y.1 = f y.2 → y.1 = y.2