case inl
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
x : E
K : Set E
hK : IsCompact K
hx : x ∈ K
hx' : x ∈ interior K
⊢ ∃ y, y ∈ frontier K ∧ Metric.infDist x (Kᶜ) = dist x y

case inr
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
x : E
K : Set E
hK : IsCompact K
hx : x ∈ K
hx' : x ∈ frontier K
⊢ ∃ y, y ∈ frontier K ∧ Metric.infDist x (Kᶜ) = dist x y
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
x : E
K : Set E
hK : IsCompact K
hx : x ∈ K
⊢ ∃ y, y ∈ frontier K ∧ Metric.infDist x (Kᶜ) = dist x y
obtain hx' | hx' : x ∈ interior K ∪ frontier K := by
  rw [← closure_eq_interior_union_frontier]
  exact subset_closure hx
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
x : E
K : Set E
hK : IsCompact K
hx : x ∈ K
⊢ x ∈ closure K
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
x : E
K : Set E
hK : IsCompact K
hx : x ∈ K
⊢ x ∈ interior K ∪ frontier K
rw [← closure_eq_interior_union_frontier]
no goals
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
x : E
K : Set E
hK : IsCompact K
hx : x ∈ K
⊢ x ∈ closure K
exact subset_closure hx
case inl
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
x : E
K : Set E
hK : IsCompact K
hx : x ∈ K
hx' : ∃ i, 0 < i ∧ Metric.closedBall x i ⊆ K
⊢ ∃ y, y ∈ frontier K ∧ Metric.infDist x (Kᶜ) = dist x y
case inl
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
x : E
K : Set E
hK : IsCompact K
hx : x ∈ K
hx' : x ∈ interior K
⊢ ∃ y, y ∈ frontier K ∧ Metric.infDist x (Kᶜ) = dist x y
rw [mem_interior_iff_mem_nhds, Metric.nhds_basis_closedBall.mem_iff] at hx'
case inl.intro.intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
x : E
K : Set E
hK : IsCompact K
hx : x ∈ K
r : ℝ
hr₀ : 0 < r
hrK : Metric.closedBall x r ⊆ K
⊢ ∃ y, y ∈ frontier K ∧ Metric.infDist x (Kᶜ) = dist x y
case inl
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
x : E
K : Set E
hK : IsCompact K
hx : x ∈ K
hx' : ∃ i, 0 < i ∧ Metric.closedBall x i ⊆ K
⊢ ∃ y, y ∈ frontier K ∧ Metric.infDist x (Kᶜ) = dist x y
rcases hx' with ⟨r, hr₀, hrK⟩
case inl.intro.intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
x : E
K : Set E
hK : IsCompact K
hx : x ∈ K
r : ℝ
hr₀ : 0 < r
hrK : Metric.closedBall x r ⊆ K
this : FiniteDimensional ℝ E
⊢ ∃ y, y ∈ frontier K ∧ Metric.infDist x (Kᶜ) = dist x y
case inl.intro.intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
x : E
K : Set E
hK : IsCompact K
hx : x ∈ K
r : ℝ
hr₀ : 0 < r
hrK : Metric.closedBall x r ⊆ K
⊢ ∃ y, y ∈ frontier K ∧ Metric.infDist x (Kᶜ) = dist x y
have : FiniteDimensional ℝ E :=
  finiteDimensional_of_isCompact_closedBall ℝ hr₀
    (isCompact_of_isClosed_subset hK Metric.isClosed_ball hrK)
no goals
case inl.intro.intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
x : E
K : Set E
hK : IsCompact K
hx : x ∈ K
r : ℝ
hr₀ : 0 < r
hrK : Metric.closedBall x r ⊆ K
this : FiniteDimensional ℝ E
⊢ ∃ y, y ∈ frontier K ∧ Metric.infDist x (Kᶜ) = dist x y
exact exists_mem_frontier_infDist_compl_eq_dist hx hK.ne_univ
case inr
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
x : E
K : Set E
hK : IsCompact K
hx : x ∈ K
hx' : x ∈ frontier K
⊢ Metric.infDist x (Kᶜ) = dist x x
case inr
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
x : E
K : Set E
hK : IsCompact K
hx : x ∈ K
hx' : x ∈ frontier K
⊢ ∃ y, y ∈ frontier K ∧ Metric.infDist x (Kᶜ) = dist x y
refine' ⟨x, hx', _⟩
case inr
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
x : E
K : Set E
hK : IsCompact K
hx : x ∈ K
hx' : x ∈ closure K ∩ closure (Kᶜ)
⊢ Metric.infDist x (Kᶜ) = dist x x
case inr
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
x : E
K : Set E
hK : IsCompact K
hx : x ∈ K
hx' : x ∈ frontier K
⊢ Metric.infDist x (Kᶜ) = dist x x
rw [frontier_eq_closure_inter_closure] at hx'
no goals
case inr
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
x : E
K : Set E
hK : IsCompact K
hx : x ∈ K
hx' : x ∈ closure K ∩ closure (Kᶜ)
⊢ Metric.infDist x (Kᶜ) = dist x x
rw [Metric.infDist_zero_of_mem_closure hx'.2, dist_self]