Theorem: UniformSpace.thickening_comp (RMT4/uniform.lean)

State before:
ι : Type u_1
α : Type u_2
β : Type u_3
a : α
s t : Set α
x u v : Set (α × α)
⊢ thickening v (thickening u s) = thickening (u ○ v) s
Tactic:
ext
State after:
case h
ι : Type u_1
α : Type u_2
β : Type u_3
a : α
s t : Set α
x u v : Set (α × α)
x✝ : α
⊢ x✝ ∈ thickening v (thickening u s) ↔ x✝ ∈ thickening (u ○ v) s

State before:
case h
ι : Type u_1
α : Type u_2
β : Type u_3
a : α
s t : Set α
x u v : Set (α × α)
x✝ : α
⊢ x✝ ∈ thickening v (thickening u s) ↔ x✝ ∈ thickening (u ○ v) s
Tactic:
simp [thickening, ball]
State after:
no goals