case intro.intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
x : E
s : Set E
hx : x ∈ s
hs : s ≠ univ
y : E
hys : y ∈ closure (sᶜ)
hyd : Metric.infDist x (sᶜ) = dist x y
⊢ ∃ y, y ∈ frontier s ∧ Metric.infDist x (sᶜ) = dist x y
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
x : E
s : Set E
hx : x ∈ s
hs : s ≠ univ
⊢ ∃ y, y ∈ frontier s ∧ Metric.infDist x (sᶜ) = dist x y
rcases Metric.exists_mem_closure_infDist_eq_dist (nonempty_compl.2 hs) x with ⟨y, hys, hyd⟩
case intro.intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
x : E
s : Set E
hx : x ∈ s
hs : s ≠ univ
y : E
hys : y ∈ interior sᶜ
hyd : Metric.infDist x (sᶜ) = dist x y
⊢ ∃ y, y ∈ frontier s ∧ Metric.infDist x (sᶜ) = dist x y
case intro.intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
x : E
s : Set E
hx : x ∈ s
hs : s ≠ univ
y : E
hys : y ∈ closure (sᶜ)
hyd : Metric.infDist x (sᶜ) = dist x y
⊢ ∃ y, y ∈ frontier s ∧ Metric.infDist x (sᶜ) = dist x y
rw [closure_compl] at hys
case intro.intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
x : E
s : Set E
hx : x ∈ s
hs : s ≠ univ
y : E
hys : y ∈ interior sᶜ
hyd : Metric.infDist x (sᶜ) = dist x y
⊢ Metric.infDist x (sᶜ) = dist y x
case intro.intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
x : E
s : Set E
hx : x ∈ s
hs : s ≠ univ
y : E
hys : y ∈ interior sᶜ
hyd : Metric.infDist x (sᶜ) = dist x y
⊢ ∃ y, y ∈ frontier s ∧ Metric.infDist x (sᶜ) = dist x y
refine'
  ⟨y,
    ⟨Metric.closedBall_infDist_compl_subset_closure hx <| Metric.mem_closedBall.2 <| ge_of_eq _,
      hys⟩,
    hyd⟩
no goals
case intro.intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
x : E
s : Set E
hx : x ∈ s
hs : s ≠ univ
y : E
hys : y ∈ interior sᶜ
hyd : Metric.infDist x (sᶜ) = dist x y
⊢ Metric.infDist x (sᶜ) = dist y x
rwa [dist_comm]