feat(topology/metric_space/basic): emetric.ball x ∞ = univ (#8745)

* add `@[simp]` to `metric.emetric_ball`,
  `metric.emetric_ball_nnreal`, and
  `metric.emetric_closed_ball_nnreal`;
* add `@[simp]` lemmas `metric.emetric_ball_top` and
  `emetric.closed_ball_top`.

Author: urkud

src/topology/metric_space/basic.lean

@@ -763,15 +763,15 @@ instance pseudo_metric_space.to_pseudo_emetric_space : pseudo_emetric_space α :
   ..‹pseudo_metric_space α› }
 
 /-- Balls defined using the distance or the edistance coincide -/
-lemma metric.emetric_ball {x : α} {ε : ℝ} : emetric.ball x (ennreal.of_real ε) = ball x ε :=
+@[simp] lemma metric.emetric_ball {x : α} {ε : ℝ} : emetric.ball x (ennreal.of_real ε) = ball x ε :=
 begin
   ext y,
   simp only [emetric.mem_ball, mem_ball, edist_dist],
   exact ennreal.of_real_lt_of_real_iff_of_nonneg dist_nonneg
 end
 
 /-- Balls defined using the distance or the edistance coincide -/
-lemma metric.emetric_ball_nnreal {x : α} {ε : ℝ≥0} : emetric.ball x ε = ball x ε :=
+@[simp] lemma metric.emetric_ball_nnreal {x : α} {ε : ℝ≥0} : emetric.ball x ε = ball x ε :=
 by { convert metric.emetric_ball, simp }
 
 /-- Closed balls defined using the distance or the edistance coincide -/
@@ -780,10 +780,13 @@ lemma metric.emetric_closed_ball {x : α} {ε : ℝ} (h : 0 ≤ ε) :
 by ext y; simp [edist_dist]; rw ennreal.of_real_le_of_real_iff h
 
 /-- Closed balls defined using the distance or the edistance coincide -/
-lemma metric.emetric_closed_ball_nnreal {x : α} {ε : ℝ≥0} :
+@[simp] lemma metric.emetric_closed_ball_nnreal {x : α} {ε : ℝ≥0} :
   emetric.closed_ball x ε = closed_ball x ε :=
 by { convert metric.emetric_closed_ball ε.2, simp }
 
+@[simp] lemma metric.emetric_ball_top (x : α) : emetric.ball x ⊤ = univ :=
+eq_univ_of_forall $ λ y, edist_lt_top _ _
+
 /-- Build a new pseudometric space from an old one where the bundled uniform structure is provably
 (but typically non-definitionaly) equal to some given uniform structure.
 See Note [forgetful inheritance].

src/topology/metric_space/emetric_space.lean

@@ -482,8 +482,11 @@ def closed_ball (x : α) (ε : ℝ≥0∞) := {y | edist y x ≤ ε}
 
 @[simp] theorem mem_closed_ball : y ∈ closed_ball x ε ↔ edist y x ≤ ε := iff.rfl
 
+@[simp] theorem closed_ball_top (x : α) : closed_ball x ∞ = univ :=
+eq_univ_of_forall $ λ y, @le_top _ _ (edist y x)
+
 theorem ball_subset_closed_ball : ball x ε ⊆ closed_ball x ε :=
-assume y, by simp; intros h; apply le_of_lt h
+assume y hy, le_of_lt hy
 
 theorem pos_of_mem_ball (hy : y ∈ ball x ε) : 0 < ε :=
 lt_of_le_of_lt (zero_le _) hy