chore(TangentCone): fix a name (#34224)

Rename `zero_mem_tangentCone` to `zero_mem_tangentConeAt`.

Author: urkud

Mathlib/Analysis/Calculus/TangentCone/Basic.lean

@@ -126,7 +126,7 @@ theorem tangentConeAt_closure : tangentConeAt 𝕜 (closure s) x = tangentConeAt
     (squeeze_zero' (.of_forall fun _ ↦ dist_nonneg) (hd'.mono fun _ ↦ le_of_lt) u_lim)⟩
 
 /-- The tangent cone at a non-isolated point contains `0`. -/
-theorem zero_mem_tangentCone {s : Set E} {x : E} (hx : x ∈ closure s) :
+theorem zero_mem_tangentConeAt {s : Set E} {x : E} (hx : x ∈ closure s) :
     0 ∈ tangentConeAt 𝕜 s x := by
   /- Take a sequence `d n` tending to `0` such that `x + d n ∈ s`. Taking `c n` of the order
   of `1 / (d n) ^ (1/2)`, then `c n` tends to infinity, but `c n • d n` tends to `0`. By definition,
@@ -157,6 +157,9 @@ theorem zero_mem_tangentCone {s : Set E} {x : E} (hx : x ∈ closure s) :
   refine squeeze_zero_norm Hle ?_
   simpa using tendsto_const_nhds.mul u_lim
 
+@[deprecated (since := "2026-01-21")]
+alias zero_mem_tangentCone := zero_mem_tangentConeAt
+
 /-- If `x` is not an accumulation point of `s`, then the tangent cone of `s` at `x`
 is a subset of `{0}`. -/
 theorem tangentConeAt_subset_zero (hx : ¬AccPt x (𝓟 s)) : tangentConeAt 𝕜 s x ⊆ 0 := by

Mathlib/Analysis/Calculus/TangentCone/DimOne.lean

@@ -27,7 +27,7 @@ theorem tangentConeAt_eq_univ {s : Set 𝕜} {x : 𝕜} (hx : AccPt x (𝓟 s))
   apply eq_univ_iff_forall.2 (fun y ↦ ?_)
   -- first deal with the case of `0`, which has to be handled separately.
   rcases eq_or_ne y 0 with rfl | hy
-  · exact zero_mem_tangentCone (mem_closure_iff_clusterPt.mpr hx.clusterPt)
+  · exact zero_mem_tangentConeAt (mem_closure_iff_clusterPt.mpr hx.clusterPt)
   /- Assume now `y` is a fixed nonzero scalar. Take a sequence `d n` tending to `0` such
   that `x + d n ∈ s`. Let `c n = y / d n`. Then `‖c n‖` tends to infinity, and `c n • d n`
   converges to `y` (as it is equal to `y`). By definition, this shows that `y` belongs to the