∀ (R : Type u_1) {E : Type u_2} [inst : AddCommGroup E] [inst_1 : SMul R E] [inst_2 : TopologicalSpace E] (s : Set E)
  (x : E), tangentConeAt R s x = {y | ClusterPt y (⊤ • nhdsWithin 0 ((fun x_1 => x + x_1) ⁻¹' s))}