-- Mathlib/Topology/UniformSpace/Defs.lean
theorem UniformSpace.ext {u₁ u₂ : UniformSpace α} (h : 𝓤[u₁] = 𝓤[u₂]) : u₁ = u₂

Proof state:
α : Type ua
u₁ u₂ : UniformSpace α
h : 𝓤 α = 𝓤 α
x : α
⊢ 𝓝 x = 𝓝 x

Tactic:
rw [u₁.nhds_eq_comap_uniformity, u₂.nhds_eq_comap_uniformity]

Result:
α : Type ua
u₁ u₂ : UniformSpace α
h : 𝓤 α = 𝓤 α
x : α
⊢ comap (Prod.mk x) UniformSpace.uniformity = comap (Prod.mk x) UniformSpace.uniformity

Proof state:
case mk.mk
α : Type ua
toTopologicalSpace✝¹ : TopologicalSpace α
uniformity✝¹ : Filter (α × α)
symm✝¹ : Tendsto Prod.swap uniformity✝¹ uniformity✝¹
comp✝¹ : (uniformity✝¹.lift' fun s => s ○ s) ≤ uniformity✝¹
nhds_eq_comap_uniformity✝¹ : ∀ (x : α), 𝓝 x = comap (Prod.mk x) uniformity✝¹
toTopologicalSpace✝ : TopologicalSpace α
uniformity✝ : Filter (α × α)
symm✝ : Tendsto Prod.swap uniformity✝ uniformity✝
comp✝ : (uniformity✝.lift' fun s => s ○ s) ≤ uniformity✝
nhds_eq_comap_uniformity✝ : ∀ (x : α), 𝓝 x = comap (Prod.mk x) uniformity✝
h : 𝓤 α = 𝓤 α
this : toTopologicalSpace = toTopologicalSpace
⊢ mk uniformity✝¹ symm✝¹ comp✝¹ nhds_eq_comap_uniformity✝¹ = mk uniformity✝ symm✝ comp✝ nhds_eq_comap_uniformity✝

Tactic:
congr

Result:
no goals

Proof state:
α : Type ua
u₁ u₂ : UniformSpace α
h : 𝓤 α = 𝓤 α
⊢ u₁ = u₂

Tactic:
have : u₁.toTopologicalSpace = u₂.toTopologicalSpace := TopologicalSpace.ext_nhds fun x ↦ by
  rw [u₁.nhds_eq_comap_uniformity, u₂.nhds_eq_comap_uniformity]
  exact congr_arg (comap _) h

Result:
α : Type ua
u₁ u₂ : UniformSpace α
h : 𝓤 α = 𝓤 α
this : toTopologicalSpace = toTopologicalSpace
⊢ u₁ = u₂

Proof state:
α : Type ua
u₁ u₂ : UniformSpace α
h : 𝓤 α = 𝓤 α
x : α
⊢ comap (Prod.mk x) UniformSpace.uniformity = comap (Prod.mk x) UniformSpace.uniformity

Tactic:
exact congr_arg (comap _) h

Result:
no goals

Proof state:
case mk
α : Type ua
u₂ : UniformSpace α
toTopologicalSpace✝ : TopologicalSpace α
uniformity✝ : Filter (α × α)
symm✝ : Tendsto Prod.swap uniformity✝ uniformity✝
comp✝ : (uniformity✝.lift' fun s => s ○ s) ≤ uniformity✝
nhds_eq_comap_uniformity✝ : ∀ (x : α), 𝓝 x = comap (Prod.mk x) uniformity✝
h : 𝓤 α = 𝓤 α
this : toTopologicalSpace = toTopologicalSpace
⊢ mk uniformity✝ symm✝ comp✝ nhds_eq_comap_uniformity✝ = u₂

Tactic:
cases u₂

Result:
case mk.mk
α : Type ua
toTopologicalSpace✝¹ : TopologicalSpace α
uniformity✝¹ : Filter (α × α)
symm✝¹ : Tendsto Prod.swap uniformity✝¹ uniformity✝¹
comp✝¹ : (uniformity✝¹.lift' fun s => s ○ s) ≤ uniformity✝¹
nhds_eq_comap_uniformity✝¹ : ∀ (x : α), 𝓝 x = comap (Prod.mk x) uniformity✝¹
toTopologicalSpace✝ : TopologicalSpace α
uniformity✝ : Filter (α × α)
symm✝ : Tendsto Prod.swap uniformity✝ uniformity✝
comp✝ : (uniformity✝.lift' fun s => s ○ s) ≤ uniformity✝
nhds_eq_comap_uniformity✝ : ∀ (x : α), 𝓝 x = comap (Prod.mk x) uniformity✝
h : 𝓤 α = 𝓤 α
this : toTopologicalSpace = toTopologicalSpace
⊢ mk uniformity✝¹ symm✝¹ comp✝¹ nhds_eq_comap_uniformity✝¹ = mk uniformity✝ symm✝ comp✝ nhds_eq_comap_uniformity✝

Proof state:
α : Type ua
u₁ u₂ : UniformSpace α
h : 𝓤 α = 𝓤 α
this : toTopologicalSpace = toTopologicalSpace
⊢ u₁ = u₂

Tactic:
cases u₁

Result:
case mk
α : Type ua
u₂ : UniformSpace α
toTopologicalSpace✝ : TopologicalSpace α
uniformity✝ : Filter (α × α)
symm✝ : Tendsto Prod.swap uniformity✝ uniformity✝
comp✝ : (uniformity✝.lift' fun s => s ○ s) ≤ uniformity✝
nhds_eq_comap_uniformity✝ : ∀ (x : α), 𝓝 x = comap (Prod.mk x) uniformity✝
h : 𝓤 α = 𝓤 α
this : toTopologicalSpace = toTopologicalSpace
⊢ mk uniformity✝ symm✝ comp✝ nhds_eq_comap_uniformity✝ = u₂