mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.UniformSpace.Uniformizable

Goal state before:
pp: X : Type u_1
inst✝ : UniformSpace X
x : X
K : Set X
hK : IsClosed K
hx : x ∉ K
O : Set (X × X)
hOu : O ∈ 𝓤 X
hOo : IsOpen O
hbO : ball x O ⊆ Kᶜ
u3 : SetRel X X
hu3u : u3 ∈ 𝓤 X
left✝ : u3.IsSymm
hu3O✝ : u3 ○ u3 ○ u3 ⊆ O
hu3O : u3 ○ interior u3 ○ u3 ⊆ O
⊢ ⋂ d ∈ 𝓤 X, d ○ (interior u3 ○ d) ⊆ O

Tactic:
← comp_assoc

Goal state after:
X : Type u_1
inst✝ : UniformSpace X
x : X
K : Set X
hK : IsClosed K
hx : x ∉ K
O : Set (X × X)
hOu : O ∈ 𝓤 X
hOo : IsOpen O
hbO : ball x O ⊆ Kᶜ
u3 : SetRel X X
hu3u : u3 ∈ 𝓤 X
left✝ : u3.IsSymm
hu3O✝ : u3 ○ u3 ○ u3 ⊆ O
hu3O : u3 ○ interior u3 ○ u3 ⊆ O
⊢ ⋂ d ∈ 𝓤 X, d ○ interior u3 ○ d ⊆ O
Module: Mathlib.Topology.UniformSpace.OfCompactT2

Goal state before:
pp: case a
γ : Type u_1
inst✝² : TopologicalSpace γ
inst✝¹ : CompactSpace γ
inst✝ : R1Space γ
x : γ
| ⨆ i, ⨆ (_ : Inseparable x i), comap (fun x_2 ↦ x) (𝓝 i) ⊓ 𝓝 i

pp: case a
γ : Type u_1
inst✝² : TopologicalSpace γ
inst✝¹ : CompactSpace γ
inst✝ : R1Space γ
x : γ
| ⨆ i, ⨆ (_ : ¬Inseparable x i), comap (fun x_2 ↦ x) (𝓝 i) ⊓ 𝓝 i

Tactic:
· enter [1, i, 1, hi]
        rw [← hi.nhds_eq, comap_const_of_mem fun V => mem_of_mem_nhds]

Goal state after:
case a
γ : Type u_1
inst✝² : TopologicalSpace γ
inst✝¹ : CompactSpace γ
inst✝ : R1Space γ
x : γ
| ⨆ i, ⨆ (_ : ¬Inseparable x i), comap (fun x_2 ↦ x) (𝓝 i) ⊓ 𝓝 i