-- Mathlib/Topology/UniformSpace/Basic.lean
theorem nhds_le_uniformity (x : α) : 𝓝 (x, x) ≤ 𝓤 α

Proof state:
α : Type ua
inst✝ : UniformSpace α
x : α
V : Set (α × α)
V_in : V ∈ 𝓤 α
w : Set (α × α)
w_in : w ∈ 𝓤 α
w_symm : SymmetricRel w
w_sub : w ○ w ⊆ V
⊢ ball x w ×ˢ ball x w ∈ 𝓝 x ×ˢ 𝓝 x

Tactic:
exact prod_mem_prod (ball_mem_nhds x w_in) (ball_mem_nhds x w_in)

Result:
no goals

Proof state:
α : Type ua
inst✝ : UniformSpace α
x : α
⊢ 𝓝 (x, x) ≤ 𝓤 α

Tactic:
intro V V_in

Result:
α : Type ua
inst✝ : UniformSpace α
x : α
V : Set (α × α)
V_in : V ∈ 𝓤 α
⊢ V ∈ 𝓝 (x, x)

Proof state:
case intro.intro.intro
α : Type ua
inst✝ : UniformSpace α
x : α
V : Set (α × α)
V_in : V ∈ 𝓤 α
w : Set (α × α)
w_in : w ∈ 𝓤 α
w_symm : SymmetricRel w
w_sub : w ○ w ⊆ V
⊢ V ∈ 𝓝 (x, x)

Tactic:
have : ball x w ×ˢ ball x w ∈ 𝓝 (x, x) := by
  rw [nhds_prod_eq]
  exact prod_mem_prod (ball_mem_nhds x w_in) (ball_mem_nhds x w_in)

Result:
case intro.intro.intro
α : Type ua
inst✝ : UniformSpace α
x : α
V : Set (α × α)
V_in : V ∈ 𝓤 α
w : Set (α × α)
w_in : w ∈ 𝓤 α
w_symm : SymmetricRel w
w_sub : w ○ w ⊆ V
this : ball x w ×ˢ ball x w ∈ 𝓝 (x, x)
⊢ V ∈ 𝓝 (x, x)

Proof state:
α : Type ua
inst✝ : UniformSpace α
x : α
V : Set (α × α)
V_in : V ∈ 𝓤 α
⊢ V ∈ 𝓝 (x, x)

Tactic:
rcases comp_symm_mem_uniformity_sets V_in with ⟨w, w_in, w_symm, w_sub⟩

Result:
case intro.intro.intro
α : Type ua
inst✝ : UniformSpace α
x : α
V : Set (α × α)
V_in : V ∈ 𝓤 α
w : Set (α × α)
w_in : w ∈ 𝓤 α
w_symm : SymmetricRel w
w_sub : w ○ w ⊆ V
⊢ V ∈ 𝓝 (x, x)

Proof state:
case intro.intro.intro
α : Type ua
inst✝ : UniformSpace α
x : α
V : Set (α × α)
V_in : V ∈ 𝓤 α
w : Set (α × α)
w_in : w ∈ 𝓤 α
w_symm : SymmetricRel w
w_sub : w ○ w ⊆ V
this : ball x w ×ˢ ball x w ∈ 𝓝 (x, x)
⊢ V ∈ 𝓝 (x, x)

Tactic:
apply mem_of_superset this

Result:
case intro.intro.intro
α : Type ua
inst✝ : UniformSpace α
x : α
V : Set (α × α)
V_in : V ∈ 𝓤 α
w : Set (α × α)
w_in : w ∈ 𝓤 α
w_symm : SymmetricRel w
w_sub : w ○ w ⊆ V
this : ball x w ×ˢ ball x w ∈ 𝓝 (x, x)
⊢ ball x w ×ˢ ball x w ⊆ V

Proof state:
α : Type ua
inst✝ : UniformSpace α
x : α
V : Set (α × α)
V_in : V ∈ 𝓤 α
w : Set (α × α)
w_in : w ∈ 𝓤 α
w_symm : SymmetricRel w
w_sub : w ○ w ⊆ V
⊢ ball x w ×ˢ ball x w ∈ 𝓝 (x, x)

Tactic:
rw [nhds_prod_eq]

Result:
α : Type ua
inst✝ : UniformSpace α
x : α
V : Set (α × α)
V_in : V ∈ 𝓤 α
w : Set (α × α)
w_in : w ∈ 𝓤 α
w_symm : SymmetricRel w
w_sub : w ○ w ⊆ V
⊢ ball x w ×ˢ ball x w ∈ 𝓝 x ×ˢ 𝓝 x

Proof state:
case intro.intro.intro.mk.intro
α : Type ua
inst✝ : UniformSpace α
x : α
V : Set (α × α)
V_in : V ∈ 𝓤 α
w : Set (α × α)
w_in : w ∈ 𝓤 α
w_symm : SymmetricRel w
w_sub : w ○ w ⊆ V
this : ball x w ×ˢ ball x w ∈ 𝓝 (x, x)
u v : α
u_in : (u, v).1 ∈ ball x w
v_in : (u, v).2 ∈ ball x w
⊢ (u, v) ∈ V

Tactic:
exact w_sub (mem_comp_of_mem_ball w_symm u_in v_in)

Result:
no goals

Proof state:
case intro.intro.intro
α : Type ua
inst✝ : UniformSpace α
x : α
V : Set (α × α)
V_in : V ∈ 𝓤 α
w : Set (α × α)
w_in : w ∈ 𝓤 α
w_symm : SymmetricRel w
w_sub : w ○ w ⊆ V
this : ball x w ×ˢ ball x w ∈ 𝓝 (x, x)
⊢ ball x w ×ˢ ball x w ⊆ V

Tactic:
rintro ⟨u, v⟩ ⟨u_in, v_in⟩

Result:
case intro.intro.intro.mk.intro
α : Type ua
inst✝ : UniformSpace α
x : α
V : Set (α × α)
V_in : V ∈ 𝓤 α
w : Set (α × α)
w_in : w ∈ 𝓤 α
w_symm : SymmetricRel w
w_sub : w ○ w ⊆ V
this : ball x w ×ˢ ball x w ∈ 𝓝 (x, x)
u v : α
u_in : (u, v).1 ∈ ball x w
v_in : (u, v).2 ∈ ball x w
⊢ (u, v) ∈ V