-- Mathlib/Topology/UniformSpace/Basic.lean
theorem uniformity_eq_uniformity_interior : 𝓤 α = (𝓤 α).lift' interior :=
  le_antisymm
    (le_iInf₂ fun d hd => by
      let ⟨s, hs, hs_comp⟩ := comp3_mem_uniformity hd
      let ⟨t, ht, hst, ht_comp⟩ := nhdset_of_mem_uniformity s hs
      have : s ⊆ interior d :=
        calc
          s ⊆ t := hst
          _ ⊆ interior d :=
            ht.subset_interior_iff.mpr fun x (hx : x ∈ t) =>
              let ⟨x, y, h₁, h₂, h₃⟩ := ht_comp hx
              hs_comp ⟨x, h₁, y, h₂, h₃⟩
      have : interior d ∈ 𝓤 α

Proof state:
α : Type ua
inst✝ : UniformSpace α
d : Set (α × α)
hd : d ∈ 𝓤 α
s : Set (α × α)
hs : s ∈ 𝓤 α
hs_comp : s ○ (s ○ s) ⊆ d
t : Set (α × α)
ht : IsOpen t
hst : s ⊆ t
ht_comp : t ⊆ {p | ∃ x y, (p.1, x) ∈ s ∧ (x, y) ∈ s ∧ (y, p.2) ∈ s}
this✝ : s ⊆ interior d
this : interior d ∈ 𝓤 α
⊢ 𝓤 α ≤ (𝓟 ∘ interior) d

Tactic:
simp [this]

Result:
no goals

Proof state:
α : Type ua
inst✝ : UniformSpace α
d : Set (α × α)
hd : d ∈ 𝓤 α
s : Set (α × α)
hs : s ∈ 𝓤 α
hs_comp : s ○ (s ○ s) ⊆ d
t : Set (α × α)
ht : IsOpen t
hst : s ⊆ t
ht_comp : t ⊆ {p | ∃ x y, (p.1, x) ∈ s ∧ (x, y) ∈ s ∧ (y, p.2) ∈ s}
⊢ 𝓤 α ≤ (𝓟 ∘ interior) d

Tactic:
have : s ⊆ interior d :=
  calc
    s ⊆ t := hst
    _ ⊆ interior d :=
      ht.subset_interior_iff.mpr fun x (hx : x ∈ t) =>
        let ⟨x, y, h₁, h₂, h₃⟩ := ht_comp hx
        hs_comp ⟨x, h₁, y, h₂, h₃⟩

Result:
α : Type ua
inst✝ : UniformSpace α
d : Set (α × α)
hd : d ∈ 𝓤 α
s : Set (α × α)
hs : s ∈ 𝓤 α
hs_comp : s ○ (s ○ s) ⊆ d
t : Set (α × α)
ht : IsOpen t
hst : s ⊆ t
ht_comp : t ⊆ {p | ∃ x y, (p.1, x) ∈ s ∧ (x, y) ∈ s ∧ (y, p.2) ∈ s}
this : s ⊆ interior d
⊢ 𝓤 α ≤ (𝓟 ∘ interior) d

Proof state:
α : Type ua
inst✝ : UniformSpace α
d : Set (α × α)
hd : d ∈ 𝓤 α
s : Set (α × α)
hs : s ∈ 𝓤 α
hs_comp : s ○ (s ○ s) ⊆ d
⊢ 𝓤 α ≤ (𝓟 ∘ interior) d

Tactic:
let ⟨t, ht, hst, ht_comp⟩ := nhdset_of_mem_uniformity s hs

Result:
α : Type ua
inst✝ : UniformSpace α
d : Set (α × α)
hd : d ∈ 𝓤 α
s : Set (α × α)
hs : s ∈ 𝓤 α
hs_comp : s ○ (s ○ s) ⊆ d
t : Set (α × α)
ht : IsOpen t
hst : s ⊆ t
ht_comp : t ⊆ {p | ∃ x y, (p.1, x) ∈ s ∧ (x, y) ∈ s ∧ (y, p.2) ∈ s}
⊢ 𝓤 α ≤ (𝓟 ∘ interior) d

Proof state:
α : Type ua
inst✝ : UniformSpace α
d : Set (α × α)
hd : d ∈ 𝓤 α
s : Set (α × α)
hs : s ∈ 𝓤 α
hs_comp : s ○ (s ○ s) ⊆ d
t : Set (α × α)
ht : IsOpen t
hst : s ⊆ t
ht_comp : t ⊆ {p | ∃ x y, (p.1, x) ∈ s ∧ (x, y) ∈ s ∧ (y, p.2) ∈ s}
this : s ⊆ interior d
⊢ 𝓤 α ≤ (𝓟 ∘ interior) d

Tactic:
have : interior d ∈ 𝓤 α := by filter_upwards [hs] using this

Result:
α : Type ua
inst✝ : UniformSpace α
d : Set (α × α)
hd : d ∈ 𝓤 α
s : Set (α × α)
hs : s ∈ 𝓤 α
hs_comp : s ○ (s ○ s) ⊆ d
t : Set (α × α)
ht : IsOpen t
hst : s ⊆ t
ht_comp : t ⊆ {p | ∃ x y, (p.1, x) ∈ s ∧ (x, y) ∈ s ∧ (y, p.2) ∈ s}
this✝ : s ⊆ interior d
this : interior d ∈ 𝓤 α
⊢ 𝓤 α ≤ (𝓟 ∘ interior) d

Proof state:
α : Type ua
inst✝ : UniformSpace α
d : Set (α × α)
hd : d ∈ 𝓤 α
⊢ 𝓤 α ≤ (𝓟 ∘ interior) d

Tactic:
let ⟨s, hs, hs_comp⟩ := comp3_mem_uniformity hd

Result:
α : Type ua
inst✝ : UniformSpace α
d : Set (α × α)
hd : d ∈ 𝓤 α
s : Set (α × α)
hs : s ∈ 𝓤 α
hs_comp : s ○ (s ○ s) ⊆ d
⊢ 𝓤 α ≤ (𝓟 ∘ interior) d

Proof state:
α : Type ua
inst✝ : UniformSpace α
d : Set (α × α)
hd : d ∈ 𝓤 α
s : Set (α × α)
hs : s ∈ 𝓤 α
hs_comp : s ○ (s ○ s) ⊆ d
t : Set (α × α)
ht : IsOpen t
hst : s ⊆ t
ht_comp : t ⊆ {p | ∃ x y, (p.1, x) ∈ s ∧ (x, y) ∈ s ∧ (y, p.2) ∈ s}
this : s ⊆ interior d
⊢ interior d ∈ 𝓤 α

Tactic:
filter_upwards [hs] using this

Result:
no goals