-- Mathlib/Topology/UniformSpace/UniformEmbedding.lean
theorem closure_image_mem_nhds_of_isUniformInducing {s : Set (α × α)} {e : α → β} (b : β)
    (he₁ : IsUniformInducing e) (he₂ : IsDenseInducing e) (hs : s ∈ 𝓤 α) :
    ∃ a, closure (e '' { a' | (a, a') ∈ s }) ∈ 𝓝 b

Proof state:
case intro.intro.intro.intro.intro
α : Type u
β : Type v
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
s : Set (α × α)
e : α → β
b : β
he₁ : IsUniformInducing e
he₂ : IsDenseInducing e
hs✝ : s ∈ 𝓤 α
U : Set (β × β)
hs : Prod.map e e ⁻¹' U ⊆ s
hU : U ∈ 𝓤 β
hUo : IsOpen U
hsymm : SymmetricRel U
a : α
ha : e a ∈ UniformSpace.ball b U
ho : IsOpen (UniformSpace.ball (e a) U)
y : β
hy : y ∈ UniformSpace.ball (e a) U
V : Set β
hV : V ∈ 𝓝 y
⊢ (V ∩ e '' UniformSpace.ball a (Prod.map e e ⁻¹' U)).Nonempty

Tactic:
rcases he₂.dense.mem_nhds (inter_mem hV (ho.mem_nhds hy)) with ⟨x, hxV, hxU⟩

Result:
case intro.intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
s : Set (α × α)
e : α → β
b : β
he₁ : IsUniformInducing e
he₂ : IsDenseInducing e
hs✝ : s ∈ 𝓤 α
U : Set (β × β)
hs : Prod.map e e ⁻¹' U ⊆ s
hU : U ∈ 𝓤 β
hUo : IsOpen U
hsymm : SymmetricRel U
a : α
ha : e a ∈ UniformSpace.ball b U
ho : IsOpen (UniformSpace.ball (e a) U)
y : β
hy : y ∈ UniformSpace.ball (e a) U
V : Set β
hV : V ∈ 𝓝 y
x : α
hxV : e x ∈ V
hxU : e x ∈ UniformSpace.ball (e a) U
⊢ (V ∩ e '' UniformSpace.ball a (Prod.map e e ⁻¹' U)).Nonempty

Proof state:
α : Type u
β : Type v
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
s : Set (α × α)
e : α → β
b : β
he₁ : IsUniformInducing e
he₂ : IsDenseInducing e
hs : s ∈ 𝓤 α
⊢ ∃ U, (U ∈ 𝓤 β ∧ IsOpen U ∧ SymmetricRel U) ∧ Prod.map e e ⁻¹' U ⊆ s

Tactic:
rwa [← he₁.comap_uniformity, (uniformity_hasBasis_open_symmetric.comap _).mem_iff] at hs

Result:
no goals

Proof state:
case intro.intro.intro.intro
α : Type u
β : Type v
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
s : Set (α × α)
e : α → β
b : β
he₁ : IsUniformInducing e
he₂ : IsDenseInducing e
hs✝ : s ∈ 𝓤 α
U : Set (β × β)
hs : Prod.map e e ⁻¹' U ⊆ s
hU : U ∈ 𝓤 β
hUo : IsOpen U
hsymm : SymmetricRel U
⊢ ∃ a, closure (e '' {a' | (a, a') ∈ s}) ∈ 𝓝 b

Tactic:
rcases he₂.dense.mem_nhds (UniformSpace.ball_mem_nhds b hU) with ⟨a, ha⟩

Result:
case intro.intro.intro.intro.intro
α : Type u
β : Type v
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
s : Set (α × α)
e : α → β
b : β
he₁ : IsUniformInducing e
he₂ : IsDenseInducing e
hs✝ : s ∈ 𝓤 α
U : Set (β × β)
hs : Prod.map e e ⁻¹' U ⊆ s
hU : U ∈ 𝓤 β
hUo : IsOpen U
hsymm : SymmetricRel U
a : α
ha : e a ∈ UniformSpace.ball b U
⊢ ∃ a, closure (e '' {a' | (a, a') ∈ s}) ∈ 𝓝 b

Proof state:
case intro.intro.intro.intro.intro
α : Type u
β : Type v
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
s : Set (α × α)
e : α → β
b : β
he₁ : IsUniformInducing e
he₂ : IsDenseInducing e
hs✝ : s ∈ 𝓤 α
U : Set (β × β)
hs : Prod.map e e ⁻¹' U ⊆ s
hU : U ∈ 𝓤 β
hUo : IsOpen U
hsymm : SymmetricRel U
a : α
ha : e a ∈ UniformSpace.ball b U
ho : IsOpen (UniformSpace.ball (e a) U)
y : β
hy : y ∈ UniformSpace.ball (e a) U
⊢ y ∈ closure (e '' UniformSpace.ball a (Prod.map e e ⁻¹' U))

Tactic:
refine mem_closure_iff_nhds.2 fun V hV => ?_

Result:
case intro.intro.intro.intro.intro
α : Type u
β : Type v
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
s : Set (α × α)
e : α → β
b : β
he₁ : IsUniformInducing e
he₂ : IsDenseInducing e
hs✝ : s ∈ 𝓤 α
U : Set (β × β)
hs : Prod.map e e ⁻¹' U ⊆ s
hU : U ∈ 𝓤 β
hUo : IsOpen U
hsymm : SymmetricRel U
a : α
ha : e a ∈ UniformSpace.ball b U
ho : IsOpen (UniformSpace.ball (e a) U)
y : β
hy : y ∈ UniformSpace.ball (e a) U
V : Set β
hV : V ∈ 𝓝 y
⊢ (V ∩ e '' UniformSpace.ball a (Prod.map e e ⁻¹' U)).Nonempty

Proof state:
case intro.intro.intro.intro.intro
α : Type u
β : Type v
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
s : Set (α × α)
e : α → β
b : β
he₁ : IsUniformInducing e
he₂ : IsDenseInducing e
hs✝ : s ∈ 𝓤 α
U : Set (β × β)
hs : Prod.map e e ⁻¹' U ⊆ s
hU : U ∈ 𝓤 β
hUo : IsOpen U
hsymm : SymmetricRel U
a : α
ha : e a ∈ UniformSpace.ball b U
⊢ closure (e '' UniformSpace.ball a (Prod.map e e ⁻¹' U)) ∈ 𝓝 b

Tactic:
have ho : IsOpen (UniformSpace.ball (e a) U) := UniformSpace.isOpen_ball (e a) hUo

Result:
case intro.intro.intro.intro.intro
α : Type u
β : Type v
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
s : Set (α × α)
e : α → β
b : β
he₁ : IsUniformInducing e
he₂ : IsDenseInducing e
hs✝ : s ∈ 𝓤 α
U : Set (β × β)
hs : Prod.map e e ⁻¹' U ⊆ s
hU : U ∈ 𝓤 β
hUo : IsOpen U
hsymm : SymmetricRel U
a : α
ha : e a ∈ UniformSpace.ball b U
ho : IsOpen (UniformSpace.ball (e a) U)
⊢ closure (e '' UniformSpace.ball a (Prod.map e e ⁻¹' U)) ∈ 𝓝 b

Proof state:
case intro.intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
s : Set (α × α)
e : α → β
b : β
he₁ : IsUniformInducing e
he₂ : IsDenseInducing e
hs✝ : s ∈ 𝓤 α
U : Set (β × β)
hs : Prod.map e e ⁻¹' U ⊆ s
hU : U ∈ 𝓤 β
hUo : IsOpen U
hsymm : SymmetricRel U
a : α
ha : e a ∈ UniformSpace.ball b U
ho : IsOpen (UniformSpace.ball (e a) U)
y : β
hy : y ∈ UniformSpace.ball (e a) U
V : Set β
hV : V ∈ 𝓝 y
x : α
hxV : e x ∈ V
hxU : e x ∈ UniformSpace.ball (e a) U
⊢ (V ∩ e '' UniformSpace.ball a (Prod.map e e ⁻¹' U)).Nonempty

Tactic:
exact ⟨e x, hxV, mem_image_of_mem e hxU⟩

Result:
no goals

Proof state:
α : Type u
β : Type v
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
s : Set (α × α)
e : α → β
b : β
he₁ : IsUniformInducing e
he₂ : IsDenseInducing e
hs : s ∈ 𝓤 α
⊢ ∃ a, closure (e '' {a' | (a, a') ∈ s}) ∈ 𝓝 b

Tactic:
obtain ⟨U, ⟨hU, hUo, hsymm⟩, hs⟩ :
  ∃ U, (U ∈ 𝓤 β ∧ IsOpen U ∧ SymmetricRel U) ∧ Prod.map e e ⁻¹' U ⊆ s := by
    rwa [← he₁.comap_uniformity, (uniformity_hasBasis_open_symmetric.comap _).mem_iff] at hs

Result:
case intro.intro.intro.intro
α : Type u
β : Type v
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
s : Set (α × α)
e : α → β
b : β
he₁ : IsUniformInducing e
he₂ : IsDenseInducing e
hs✝ : s ∈ 𝓤 α
U : Set (β × β)
hs : Prod.map e e ⁻¹' U ⊆ s
hU : U ∈ 𝓤 β
hUo : IsOpen U
hsymm : SymmetricRel U
⊢ ∃ a, closure (e '' {a' | (a, a') ∈ s}) ∈ 𝓝 b

Proof state:
case intro.intro.intro.intro.intro
α : Type u
β : Type v
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
s : Set (α × α)
e : α → β
b : β
he₁ : IsUniformInducing e
he₂ : IsDenseInducing e
hs✝ : s ∈ 𝓤 α
U : Set (β × β)
hs : Prod.map e e ⁻¹' U ⊆ s
hU : U ∈ 𝓤 β
hUo : IsOpen U
hsymm : SymmetricRel U
a : α
ha : e a ∈ UniformSpace.ball b U
ho : IsOpen (UniformSpace.ball (e a) U)
⊢ closure (e '' UniformSpace.ball a (Prod.map e e ⁻¹' U)) ∈ 𝓝 b

Tactic:
refine mem_of_superset (ho.mem_nhds <| (UniformSpace.mem_ball_symmetry hsymm).2 ha) fun y hy => ?_

Result:
case intro.intro.intro.intro.intro
α : Type u
β : Type v
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
s : Set (α × α)
e : α → β
b : β
he₁ : IsUniformInducing e
he₂ : IsDenseInducing e
hs✝ : s ∈ 𝓤 α
U : Set (β × β)
hs : Prod.map e e ⁻¹' U ⊆ s
hU : U ∈ 𝓤 β
hUo : IsOpen U
hsymm : SymmetricRel U
a : α
ha : e a ∈ UniformSpace.ball b U
ho : IsOpen (UniformSpace.ball (e a) U)
y : β
hy : y ∈ UniformSpace.ball (e a) U
⊢ y ∈ closure (e '' UniformSpace.ball a (Prod.map e e ⁻¹' U))