refactor(Combinatorics/SimpleGraph/Metric): inline ext in ball_top

Author: Fieldnote-Echo

Mathlib/Combinatorics/SimpleGraph/Metric.lean

@@ -431,8 +431,7 @@ theorem ball_two : G.ball c 2 = insert c (G.neighborSet c) := by
 /-- The ball of radius `⊤` is the connected component of the center. -/
 theorem ball_top :
     G.ball c ⊤ = (G.connectedComponentMk c).supp := by
-  ext v
-  simp [lt_top_iff_ne_top, edist_ne_top_iff_reachable]
+  simp [Set.ext_iff, lt_top_iff_ne_top, edist_ne_top_iff_reachable]
 
 /-- A vertex is in the ball of radius `⊤` iff it is reachable from the center. -/
 theorem mem_ball_top : v ∈ G.ball c ⊤ ↔ G.Reachable v c := by