no goals
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
E : Set α
x : α
x_mem : x ∈ closure E
⊢ thickenedIndicatorAux δ E x = 1
rw [← thickenedIndicatorAux_closure_eq, thickenedIndicatorAux_one δ (closure E) x_mem]