[GOAL]
𝕜 : Type u_1
inst✝⁴ : NormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F✝ : Type u_3
inst✝¹ : SeminormedAddCommGroup F✝
inst✝ : NormedSpace ℝ F✝
F : Subspace 𝕜 E
hFc : IsClosed ↑F
hF : ∃ x, ¬x ∈ F
r : ℝ
hr : r < 1
⊢ ∃ x₀, ¬x₀ ∈ F ∧ ∀ (y : E), y ∈ F → r * ‖x₀‖ ≤ ‖x₀ - y‖
[PROOFSTEP]
classical
obtain ⟨x, hx⟩ : ∃ x : E, x ∉ F := hF
let d := Metric.infDist x F
have hFn : (F : Set E).Nonempty := ⟨_, F.zero_mem⟩
have hdp : 0 < d := lt_of_le_of_ne Metric.infDist_nonneg fun heq => hx ((hFc.mem_iff_infDist_zero hFn).2 heq.symm)
let r' := max r 2⁻¹
have hr' : r' < 1 := by
  simp [hr]
  norm_num
have hlt : 0 < r' := lt_of_lt_of_le (by norm_num) (le_max_right r 2⁻¹)
have hdlt : d < d / r' := (lt_div_iff hlt).mpr ((mul_lt_iff_lt_one_right hdp).2 hr')
obtain ⟨y₀, hy₀F, hxy₀⟩ : ∃ y ∈ F, dist x y < d / r' := (Metric.infDist_lt_iff hFn).mp hdlt
have x_ne_y₀ : x - y₀ ∉ F := by
  by_contra h
  have : x - y₀ + y₀ ∈ F := F.add_mem h hy₀F
  simp only [neg_add_cancel_right, sub_eq_add_neg] at this 
  exact hx this
refine' ⟨x - y₀, x_ne_y₀, fun y hy => le_of_lt _⟩
have hy₀y : y₀ + y ∈ F := F.add_mem hy₀F hy
calc
  r * ‖x - y₀‖ ≤ r' * ‖x - y₀‖ := by gcongr; apply le_max_left
  _ < d := by
    rw [← dist_eq_norm]
    exact (lt_div_iff' hlt).1 hxy₀
  _ ≤ dist x (y₀ + y) := (Metric.infDist_le_dist_of_mem hy₀y)
  _ = ‖x - y₀ - y‖ := by rw [sub_sub, dist_eq_norm]
[GOAL]
𝕜 : Type u_1
inst✝⁴ : NormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F✝ : Type u_3
inst✝¹ : SeminormedAddCommGroup F✝
inst✝ : NormedSpace ℝ F✝
F : Subspace 𝕜 E
hFc : IsClosed ↑F
hF : ∃ x, ¬x ∈ F
r : ℝ
hr : r < 1
⊢ ∃ x₀, ¬x₀ ∈ F ∧ ∀ (y : E), y ∈ F → r * ‖x₀‖ ≤ ‖x₀ - y‖
[PROOFSTEP]
obtain ⟨x, hx⟩ : ∃ x : E, x ∉ F := hF
[GOAL]
case intro
𝕜 : Type u_1
inst✝⁴ : NormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F✝ : Type u_3
inst✝¹ : SeminormedAddCommGroup F✝
inst✝ : NormedSpace ℝ F✝
F : Subspace 𝕜 E
hFc : IsClosed ↑F
r : ℝ
hr : r < 1
x : E
hx : ¬x ∈ F
⊢ ∃ x₀, ¬x₀ ∈ F ∧ ∀ (y : E), y ∈ F → r * ‖x₀‖ ≤ ‖x₀ - y‖
[PROOFSTEP]
let d := Metric.infDist x F
[GOAL]
case intro
𝕜 : Type u_1
inst✝⁴ : NormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F✝ : Type u_3
inst✝¹ : SeminormedAddCommGroup F✝
inst✝ : NormedSpace ℝ F✝
F : Subspace 𝕜 E
hFc : IsClosed ↑F
r : ℝ
hr : r < 1
x : E
hx : ¬x ∈ F
d : ℝ := infDist x ↑F
⊢ ∃ x₀, ¬x₀ ∈ F ∧ ∀ (y : E), y ∈ F → r * ‖x₀‖ ≤ ‖x₀ - y‖
[PROOFSTEP]
have hFn : (F : Set E).Nonempty := ⟨_, F.zero_mem⟩
[GOAL]
case intro
𝕜 : Type u_1
inst✝⁴ : NormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F✝ : Type u_3
inst✝¹ : SeminormedAddCommGroup F✝
inst✝ : NormedSpace ℝ F✝
F : Subspace 𝕜 E
hFc : IsClosed ↑F
r : ℝ
hr : r < 1
x : E
hx : ¬x ∈ F
d : ℝ := infDist x ↑F
hFn : Set.Nonempty ↑F
⊢ ∃ x₀, ¬x₀ ∈ F ∧ ∀ (y : E), y ∈ F → r * ‖x₀‖ ≤ ‖x₀ - y‖
[PROOFSTEP]
have hdp : 0 < d := lt_of_le_of_ne Metric.infDist_nonneg fun heq => hx ((hFc.mem_iff_infDist_zero hFn).2 heq.symm)
[GOAL]
case intro
𝕜 : Type u_1
inst✝⁴ : NormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F✝ : Type u_3
inst✝¹ : SeminormedAddCommGroup F✝
inst✝ : NormedSpace ℝ F✝
F : Subspace 𝕜 E
hFc : IsClosed ↑F
r : ℝ
hr : r < 1
x : E
hx : ¬x ∈ F
d : ℝ := infDist x ↑F
hFn : Set.Nonempty ↑F
hdp : 0 < d
⊢ ∃ x₀, ¬x₀ ∈ F ∧ ∀ (y : E), y ∈ F → r * ‖x₀‖ ≤ ‖x₀ - y‖
[PROOFSTEP]
let r' := max r 2⁻¹
[GOAL]
case intro
𝕜 : Type u_1
inst✝⁴ : NormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F✝ : Type u_3
inst✝¹ : SeminormedAddCommGroup F✝
inst✝ : NormedSpace ℝ F✝
F : Subspace 𝕜 E
hFc : IsClosed ↑F
r : ℝ
hr : r < 1
x : E
hx : ¬x ∈ F
d : ℝ := infDist x ↑F
hFn : Set.Nonempty ↑F
hdp : 0 < d
r' : ℝ := max r 2⁻¹
⊢ ∃ x₀, ¬x₀ ∈ F ∧ ∀ (y : E), y ∈ F → r * ‖x₀‖ ≤ ‖x₀ - y‖
[PROOFSTEP]
have hr' : r' < 1 := by
  simp [hr]
  norm_num
[GOAL]
𝕜 : Type u_1
inst✝⁴ : NormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F✝ : Type u_3
inst✝¹ : SeminormedAddCommGroup F✝
inst✝ : NormedSpace ℝ F✝
F : Subspace 𝕜 E
hFc : IsClosed ↑F
r : ℝ
hr : r < 1
x : E
hx : ¬x ∈ F
d : ℝ := infDist x ↑F
hFn : Set.Nonempty ↑F
hdp : 0 < d
r' : ℝ := max r 2⁻¹
⊢ r' < 1
[PROOFSTEP]
simp [hr]
[GOAL]
𝕜 : Type u_1
inst✝⁴ : NormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F✝ : Type u_3
inst✝¹ : SeminormedAddCommGroup F✝
inst✝ : NormedSpace ℝ F✝
F : Subspace 𝕜 E
hFc : IsClosed ↑F
r : ℝ
hr : r < 1
x : E
hx : ¬x ∈ F
d : ℝ := infDist x ↑F
hFn : Set.Nonempty ↑F
hdp : 0 < d
r' : ℝ := max r 2⁻¹
⊢ 2⁻¹ < 1
[PROOFSTEP]
norm_num
[GOAL]
case intro
𝕜 : Type u_1
inst✝⁴ : NormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F✝ : Type u_3
inst✝¹ : SeminormedAddCommGroup F✝
inst✝ : NormedSpace ℝ F✝
F : Subspace 𝕜 E
hFc : IsClosed ↑F
r : ℝ
hr : r < 1
x : E
hx : ¬x ∈ F
d : ℝ := infDist x ↑F
hFn : Set.Nonempty ↑F
hdp : 0 < d
r' : ℝ := max r 2⁻¹
hr' : r' < 1
⊢ ∃ x₀, ¬x₀ ∈ F ∧ ∀ (y : E), y ∈ F → r * ‖x₀‖ ≤ ‖x₀ - y‖
[PROOFSTEP]
have hlt : 0 < r' := lt_of_lt_of_le (by norm_num) (le_max_right r 2⁻¹)
[GOAL]
𝕜 : Type u_1
inst✝⁴ : NormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F✝ : Type u_3
inst✝¹ : SeminormedAddCommGroup F✝
inst✝ : NormedSpace ℝ F✝
F : Subspace 𝕜 E
hFc : IsClosed ↑F
r : ℝ
hr : r < 1
x : E
hx : ¬x ∈ F
d : ℝ := infDist x ↑F
hFn : Set.Nonempty ↑F
hdp : 0 < d
r' : ℝ := max r 2⁻¹
hr' : r' < 1
⊢ 0 < 2⁻¹
[PROOFSTEP]
norm_num
[GOAL]
case intro
𝕜 : Type u_1
inst✝⁴ : NormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F✝ : Type u_3
inst✝¹ : SeminormedAddCommGroup F✝
inst✝ : NormedSpace ℝ F✝
F : Subspace 𝕜 E
hFc : IsClosed ↑F
r : ℝ
hr : r < 1
x : E
hx : ¬x ∈ F
d : ℝ := infDist x ↑F
hFn : Set.Nonempty ↑F
hdp : 0 < d
r' : ℝ := max r 2⁻¹
hr' : r' < 1
hlt : 0 < r'
⊢ ∃ x₀, ¬x₀ ∈ F ∧ ∀ (y : E), y ∈ F → r * ‖x₀‖ ≤ ‖x₀ - y‖
[PROOFSTEP]
have hdlt : d < d / r' := (lt_div_iff hlt).mpr ((mul_lt_iff_lt_one_right hdp).2 hr')
[GOAL]
case intro
𝕜 : Type u_1
inst✝⁴ : NormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F✝ : Type u_3
inst✝¹ : SeminormedAddCommGroup F✝
inst✝ : NormedSpace ℝ F✝
F : Subspace 𝕜 E
hFc : IsClosed ↑F
r : ℝ
hr : r < 1
x : E
hx : ¬x ∈ F
d : ℝ := infDist x ↑F
hFn : Set.Nonempty ↑F
hdp : 0 < d
r' : ℝ := max r 2⁻¹
hr' : r' < 1
hlt : 0 < r'
hdlt : d < d / r'
⊢ ∃ x₀, ¬x₀ ∈ F ∧ ∀ (y : E), y ∈ F → r * ‖x₀‖ ≤ ‖x₀ - y‖
[PROOFSTEP]
obtain ⟨y₀, hy₀F, hxy₀⟩ : ∃ y ∈ F, dist x y < d / r' := (Metric.infDist_lt_iff hFn).mp hdlt
[GOAL]
case intro.intro.intro
𝕜 : Type u_1
inst✝⁴ : NormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F✝ : Type u_3
inst✝¹ : SeminormedAddCommGroup F✝
inst✝ : NormedSpace ℝ F✝
F : Subspace 𝕜 E
hFc : IsClosed ↑F
r : ℝ
hr : r < 1
x : E
hx : ¬x ∈ F
d : ℝ := infDist x ↑F
hFn : Set.Nonempty ↑F
hdp : 0 < d
r' : ℝ := max r 2⁻¹
hr' : r' < 1
hlt : 0 < r'
hdlt : d < d / r'
y₀ : E
hy₀F : y₀ ∈ F
hxy₀ : dist x y₀ < d / r'
⊢ ∃ x₀, ¬x₀ ∈ F ∧ ∀ (y : E), y ∈ F → r * ‖x₀‖ ≤ ‖x₀ - y‖
[PROOFSTEP]
have x_ne_y₀ : x - y₀ ∉ F := by
  by_contra h
  have : x - y₀ + y₀ ∈ F := F.add_mem h hy₀F
  simp only [neg_add_cancel_right, sub_eq_add_neg] at this 
  exact hx this
[GOAL]
𝕜 : Type u_1
inst✝⁴ : NormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F✝ : Type u_3
inst✝¹ : SeminormedAddCommGroup F✝
inst✝ : NormedSpace ℝ F✝
F : Subspace 𝕜 E
hFc : IsClosed ↑F
r : ℝ
hr : r < 1
x : E
hx : ¬x ∈ F
d : ℝ := infDist x ↑F
hFn : Set.Nonempty ↑F
hdp : 0 < d
r' : ℝ := max r 2⁻¹
hr' : r' < 1
hlt : 0 < r'
hdlt : d < d / r'
y₀ : E
hy₀F : y₀ ∈ F
hxy₀ : dist x y₀ < d / r'
⊢ ¬x - y₀ ∈ F
[PROOFSTEP]
by_contra h
[GOAL]
𝕜 : Type u_1
inst✝⁴ : NormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F✝ : Type u_3
inst✝¹ : SeminormedAddCommGroup F✝
inst✝ : NormedSpace ℝ F✝
F : Subspace 𝕜 E
hFc : IsClosed ↑F
r : ℝ
hr : r < 1
x : E
hx : ¬x ∈ F
d : ℝ := infDist x ↑F
hFn : Set.Nonempty ↑F
hdp : 0 < d
r' : ℝ := max r 2⁻¹
hr' : r' < 1
hlt : 0 < r'
hdlt : d < d / r'
y₀ : E
hy₀F : y₀ ∈ F
hxy₀ : dist x y₀ < d / r'
h : x - y₀ ∈ F
⊢ False
[PROOFSTEP]
have : x - y₀ + y₀ ∈ F := F.add_mem h hy₀F
[GOAL]
𝕜 : Type u_1
inst✝⁴ : NormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F✝ : Type u_3
inst✝¹ : SeminormedAddCommGroup F✝
inst✝ : NormedSpace ℝ F✝
F : Subspace 𝕜 E
hFc : IsClosed ↑F
r : ℝ
hr : r < 1
x : E
hx : ¬x ∈ F
d : ℝ := infDist x ↑F
hFn : Set.Nonempty ↑F
hdp : 0 < d
r' : ℝ := max r 2⁻¹
hr' : r' < 1
hlt : 0 < r'
hdlt : d < d / r'
y₀ : E
hy₀F : y₀ ∈ F
hxy₀ : dist x y₀ < d / r'
h : x - y₀ ∈ F
this : x - y₀ + y₀ ∈ F
⊢ False
[PROOFSTEP]
simp only [neg_add_cancel_right, sub_eq_add_neg] at this 
[GOAL]
𝕜 : Type u_1
inst✝⁴ : NormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F✝ : Type u_3
inst✝¹ : SeminormedAddCommGroup F✝
inst✝ : NormedSpace ℝ F✝
F : Subspace 𝕜 E
hFc : IsClosed ↑F
r : ℝ
hr : r < 1
x : E
hx : ¬x ∈ F
d : ℝ := infDist x ↑F
hFn : Set.Nonempty ↑F
hdp : 0 < d
r' : ℝ := max r 2⁻¹
hr' : r' < 1
hlt : 0 < r'
hdlt : d < d / r'
y₀ : E
hy₀F : y₀ ∈ F
hxy₀ : dist x y₀ < d / r'
h : x - y₀ ∈ F
this : x ∈ F
⊢ False
[PROOFSTEP]
exact hx this
[GOAL]
case intro.intro.intro
𝕜 : Type u_1
inst✝⁴ : NormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F✝ : Type u_3
inst✝¹ : SeminormedAddCommGroup F✝
inst✝ : NormedSpace ℝ F✝
F : Subspace 𝕜 E
hFc : IsClosed ↑F
r : ℝ
hr : r < 1
x : E
hx : ¬x ∈ F
d : ℝ := infDist x ↑F
hFn : Set.Nonempty ↑F
hdp : 0 < d
r' : ℝ := max r 2⁻¹
hr' : r' < 1
hlt : 0 < r'
hdlt : d < d / r'
y₀ : E
hy₀F : y₀ ∈ F
hxy₀ : dist x y₀ < d / r'
x_ne_y₀ : ¬x - y₀ ∈ F
⊢ ∃ x₀, ¬x₀ ∈ F ∧ ∀ (y : E), y ∈ F → r * ‖x₀‖ ≤ ‖x₀ - y‖
[PROOFSTEP]
refine' ⟨x - y₀, x_ne_y₀, fun y hy => le_of_lt _⟩
[GOAL]
case intro.intro.intro
𝕜 : Type u_1
inst✝⁴ : NormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F✝ : Type u_3
inst✝¹ : SeminormedAddCommGroup F✝
inst✝ : NormedSpace ℝ F✝
F : Subspace 𝕜 E
hFc : IsClosed ↑F
r : ℝ
hr : r < 1
x : E
hx : ¬x ∈ F
d : ℝ := infDist x ↑F
hFn : Set.Nonempty ↑F
hdp : 0 < d
r' : ℝ := max r 2⁻¹
hr' : r' < 1
hlt : 0 < r'
hdlt : d < d / r'
y₀ : E
hy₀F : y₀ ∈ F
hxy₀ : dist x y₀ < d / r'
x_ne_y₀ : ¬x - y₀ ∈ F
y : E
hy : y ∈ F
⊢ r * ‖x - y₀‖ < ‖x - y₀ - y‖
[PROOFSTEP]
have hy₀y : y₀ + y ∈ F := F.add_mem hy₀F hy
[GOAL]
case intro.intro.intro
𝕜 : Type u_1
inst✝⁴ : NormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F✝ : Type u_3
inst✝¹ : SeminormedAddCommGroup F✝
inst✝ : NormedSpace ℝ F✝
F : Subspace 𝕜 E
hFc : IsClosed ↑F
r : ℝ
hr : r < 1
x : E
hx : ¬x ∈ F
d : ℝ := infDist x ↑F
hFn : Set.Nonempty ↑F
hdp : 0 < d
r' : ℝ := max r 2⁻¹
hr' : r' < 1
hlt : 0 < r'
hdlt : d < d / r'
y₀ : E
hy₀F : y₀ ∈ F
hxy₀ : dist x y₀ < d / r'
x_ne_y₀ : ¬x - y₀ ∈ F
y : E
hy : y ∈ F
hy₀y : y₀ + y ∈ F
⊢ r * ‖x - y₀‖ < ‖x - y₀ - y‖
[PROOFSTEP]
calc
  r * ‖x - y₀‖ ≤ r' * ‖x - y₀‖ := by gcongr; apply le_max_left
  _ < d := by
    rw [← dist_eq_norm]
    exact (lt_div_iff' hlt).1 hxy₀
  _ ≤ dist x (y₀ + y) := (Metric.infDist_le_dist_of_mem hy₀y)
  _ = ‖x - y₀ - y‖ := by rw [sub_sub, dist_eq_norm]
[GOAL]
𝕜 : Type u_1
inst✝⁴ : NormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F✝ : Type u_3
inst✝¹ : SeminormedAddCommGroup F✝
inst✝ : NormedSpace ℝ F✝
F : Subspace 𝕜 E
hFc : IsClosed ↑F
r : ℝ
hr : r < 1
x : E
hx : ¬x ∈ F
d : ℝ := infDist x ↑F
hFn : Set.Nonempty ↑F
hdp : 0 < d
r' : ℝ := max r 2⁻¹
hr' : r' < 1
hlt : 0 < r'
hdlt : d < d / r'
y₀ : E
hy₀F : y₀ ∈ F
hxy₀ : dist x y₀ < d / r'
x_ne_y₀ : ¬x - y₀ ∈ F
y : E
hy : y ∈ F
hy₀y : y₀ + y ∈ F
⊢ r * ‖x - y₀‖ ≤ r' * ‖x - y₀‖
[PROOFSTEP]
gcongr
[GOAL]
case h
𝕜 : Type u_1
inst✝⁴ : NormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F✝ : Type u_3
inst✝¹ : SeminormedAddCommGroup F✝
inst✝ : NormedSpace ℝ F✝
F : Subspace 𝕜 E
hFc : IsClosed ↑F
r : ℝ
hr : r < 1
x : E
hx : ¬x ∈ F
d : ℝ := infDist x ↑F
hFn : Set.Nonempty ↑F
hdp : 0 < d
r' : ℝ := max r 2⁻¹
hr' : r' < 1
hlt : 0 < r'
hdlt : d < d / r'
y₀ : E
hy₀F : y₀ ∈ F
hxy₀ : dist x y₀ < d / r'
x_ne_y₀ : ¬x - y₀ ∈ F
y : E
hy : y ∈ F
hy₀y : y₀ + y ∈ F
⊢ r ≤ r'
[PROOFSTEP]
apply le_max_left
[GOAL]
𝕜 : Type u_1
inst✝⁴ : NormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F✝ : Type u_3
inst✝¹ : SeminormedAddCommGroup F✝
inst✝ : NormedSpace ℝ F✝
F : Subspace 𝕜 E
hFc : IsClosed ↑F
r : ℝ
hr : r < 1
x : E
hx : ¬x ∈ F
d : ℝ := infDist x ↑F
hFn : Set.Nonempty ↑F
hdp : 0 < d
r' : ℝ := max r 2⁻¹
hr' : r' < 1
hlt : 0 < r'
hdlt : d < d / r'
y₀ : E
hy₀F : y₀ ∈ F
hxy₀ : dist x y₀ < d / r'
x_ne_y₀ : ¬x - y₀ ∈ F
y : E
hy : y ∈ F
hy₀y : y₀ + y ∈ F
⊢ r' * ‖x - y₀‖ < d
[PROOFSTEP]
rw [← dist_eq_norm]
[GOAL]
𝕜 : Type u_1
inst✝⁴ : NormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F✝ : Type u_3
inst✝¹ : SeminormedAddCommGroup F✝
inst✝ : NormedSpace ℝ F✝
F : Subspace 𝕜 E
hFc : IsClosed ↑F
r : ℝ
hr : r < 1
x : E
hx : ¬x ∈ F
d : ℝ := infDist x ↑F
hFn : Set.Nonempty ↑F
hdp : 0 < d
r' : ℝ := max r 2⁻¹
hr' : r' < 1
hlt : 0 < r'
hdlt : d < d / r'
y₀ : E
hy₀F : y₀ ∈ F
hxy₀ : dist x y₀ < d / r'
x_ne_y₀ : ¬x - y₀ ∈ F
y : E
hy : y ∈ F
hy₀y : y₀ + y ∈ F
⊢ r' * dist x y₀ < d
[PROOFSTEP]
exact (lt_div_iff' hlt).1 hxy₀
[GOAL]
𝕜 : Type u_1
inst✝⁴ : NormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F✝ : Type u_3
inst✝¹ : SeminormedAddCommGroup F✝
inst✝ : NormedSpace ℝ F✝
F : Subspace 𝕜 E
hFc : IsClosed ↑F
r : ℝ
hr : r < 1
x : E
hx : ¬x ∈ F
d : ℝ := infDist x ↑F
hFn : Set.Nonempty ↑F
hdp : 0 < d
r' : ℝ := max r 2⁻¹
hr' : r' < 1
hlt : 0 < r'
hdlt : d < d / r'
y₀ : E
hy₀F : y₀ ∈ F
hxy₀ : dist x y₀ < d / r'
x_ne_y₀ : ¬x - y₀ ∈ F
y : E
hy : y ∈ F
hy₀y : y₀ + y ∈ F
⊢ dist x (y₀ + y) = ‖x - y₀ - y‖
[PROOFSTEP]
rw [sub_sub, dist_eq_norm]
[GOAL]
𝕜 : Type u_1
inst✝⁴ : NormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F✝ : Type u_3
inst✝¹ : SeminormedAddCommGroup F✝
inst✝ : NormedSpace ℝ F✝
c : 𝕜
hc : 1 < ‖c‖
R : ℝ
hR : ‖c‖ < R
F : Subspace 𝕜 E
hFc : IsClosed ↑F
hF : ∃ x, ¬x ∈ F
⊢ ∃ x₀, ‖x₀‖ ≤ R ∧ ∀ (y : E), y ∈ F → 1 ≤ ‖x₀ - y‖
[PROOFSTEP]
have Rpos : 0 < R := (norm_nonneg _).trans_lt hR
[GOAL]
𝕜 : Type u_1
inst✝⁴ : NormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F✝ : Type u_3
inst✝¹ : SeminormedAddCommGroup F✝
inst✝ : NormedSpace ℝ F✝
c : 𝕜
hc : 1 < ‖c‖
R : ℝ
hR : ‖c‖ < R
F : Subspace 𝕜 E
hFc : IsClosed ↑F
hF : ∃ x, ¬x ∈ F
Rpos : 0 < R
⊢ ∃ x₀, ‖x₀‖ ≤ R ∧ ∀ (y : E), y ∈ F → 1 ≤ ‖x₀ - y‖
[PROOFSTEP]
have : ‖c‖ / R < 1 := by
  rw [div_lt_iff Rpos]
  simpa using hR
[GOAL]
𝕜 : Type u_1
inst✝⁴ : NormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F✝ : Type u_3
inst✝¹ : SeminormedAddCommGroup F✝
inst✝ : NormedSpace ℝ F✝
c : 𝕜
hc : 1 < ‖c‖
R : ℝ
hR : ‖c‖ < R
F : Subspace 𝕜 E
hFc : IsClosed ↑F
hF : ∃ x, ¬x ∈ F
Rpos : 0 < R
⊢ ‖c‖ / R < 1
[PROOFSTEP]
rw [div_lt_iff Rpos]
[GOAL]
𝕜 : Type u_1
inst✝⁴ : NormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F✝ : Type u_3
inst✝¹ : SeminormedAddCommGroup F✝
inst✝ : NormedSpace ℝ F✝
c : 𝕜
hc : 1 < ‖c‖
R : ℝ
hR : ‖c‖ < R
F : Subspace 𝕜 E
hFc : IsClosed ↑F
hF : ∃ x, ¬x ∈ F
Rpos : 0 < R
⊢ ‖c‖ < 1 * R
[PROOFSTEP]
simpa using hR
[GOAL]
𝕜 : Type u_1
inst✝⁴ : NormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F✝ : Type u_3
inst✝¹ : SeminormedAddCommGroup F✝
inst✝ : NormedSpace ℝ F✝
c : 𝕜
hc : 1 < ‖c‖
R : ℝ
hR : ‖c‖ < R
F : Subspace 𝕜 E
hFc : IsClosed ↑F
hF : ∃ x, ¬x ∈ F
Rpos : 0 < R
this : ‖c‖ / R < 1
⊢ ∃ x₀, ‖x₀‖ ≤ R ∧ ∀ (y : E), y ∈ F → 1 ≤ ‖x₀ - y‖
[PROOFSTEP]
rcases riesz_lemma hFc hF this with ⟨x, xF, hx⟩
[GOAL]
case intro.intro
𝕜 : Type u_1
inst✝⁴ : NormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F✝ : Type u_3
inst✝¹ : SeminormedAddCommGroup F✝
inst✝ : NormedSpace ℝ F✝
c : 𝕜
hc : 1 < ‖c‖
R : ℝ
hR : ‖c‖ < R
F : Subspace 𝕜 E
hFc : IsClosed ↑F
hF : ∃ x, ¬x ∈ F
Rpos : 0 < R
this : ‖c‖ / R < 1
x : E
xF : ¬x ∈ F
hx : ∀ (y : E), y ∈ F → ‖c‖ / R * ‖x‖ ≤ ‖x - y‖
⊢ ∃ x₀, ‖x₀‖ ≤ R ∧ ∀ (y : E), y ∈ F → 1 ≤ ‖x₀ - y‖
[PROOFSTEP]
have x0 : x ≠ 0 := fun H => by simp [H] at xF 
[GOAL]
𝕜 : Type u_1
inst✝⁴ : NormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F✝ : Type u_3
inst✝¹ : SeminormedAddCommGroup F✝
inst✝ : NormedSpace ℝ F✝
c : 𝕜
hc : 1 < ‖c‖
R : ℝ
hR : ‖c‖ < R
F : Subspace 𝕜 E
hFc : IsClosed ↑F
hF : ∃ x, ¬x ∈ F
Rpos : 0 < R
this : ‖c‖ / R < 1
x : E
xF : ¬x ∈ F
hx : ∀ (y : E), y ∈ F → ‖c‖ / R * ‖x‖ ≤ ‖x - y‖
H : x = 0
⊢ False
[PROOFSTEP]
simp [H] at xF 
[GOAL]
case intro.intro
𝕜 : Type u_1
inst✝⁴ : NormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F✝ : Type u_3
inst✝¹ : SeminormedAddCommGroup F✝
inst✝ : NormedSpace ℝ F✝
c : 𝕜
hc : 1 < ‖c‖
R : ℝ
hR : ‖c‖ < R
F : Subspace 𝕜 E
hFc : IsClosed ↑F
hF : ∃ x, ¬x ∈ F
Rpos : 0 < R
this : ‖c‖ / R < 1
x : E
xF : ¬x ∈ F
hx : ∀ (y : E), y ∈ F → ‖c‖ / R * ‖x‖ ≤ ‖x - y‖
x0 : x ≠ 0
⊢ ∃ x₀, ‖x₀‖ ≤ R ∧ ∀ (y : E), y ∈ F → 1 ≤ ‖x₀ - y‖
[PROOFSTEP]
obtain ⟨d, d0, dxlt, ledx, -⟩ : ∃ d : 𝕜, d ≠ 0 ∧ ‖d • x‖ < R ∧ R / ‖c‖ ≤ ‖d • x‖ ∧ ‖d‖⁻¹ ≤ R⁻¹ * ‖c‖ * ‖x‖ :=
  rescale_to_shell hc Rpos x0
[GOAL]
case intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
inst✝⁴ : NormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F✝ : Type u_3
inst✝¹ : SeminormedAddCommGroup F✝
inst✝ : NormedSpace ℝ F✝
c : 𝕜
hc : 1 < ‖c‖
R : ℝ
hR : ‖c‖ < R
F : Subspace 𝕜 E
hFc : IsClosed ↑F
hF : ∃ x, ¬x ∈ F
Rpos : 0 < R
this : ‖c‖ / R < 1
x : E
xF : ¬x ∈ F
hx : ∀ (y : E), y ∈ F → ‖c‖ / R * ‖x‖ ≤ ‖x - y‖
x0 : x ≠ 0
d : 𝕜
d0 : d ≠ 0
dxlt : ‖d • x‖ < R
ledx : R / ‖c‖ ≤ ‖d • x‖
⊢ ∃ x₀, ‖x₀‖ ≤ R ∧ ∀ (y : E), y ∈ F → 1 ≤ ‖x₀ - y‖
[PROOFSTEP]
refine' ⟨d • x, dxlt.le, fun y hy => _⟩
[GOAL]
case intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
inst✝⁴ : NormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F✝ : Type u_3
inst✝¹ : SeminormedAddCommGroup F✝
inst✝ : NormedSpace ℝ F✝
c : 𝕜
hc : 1 < ‖c‖
R : ℝ
hR : ‖c‖ < R
F : Subspace 𝕜 E
hFc : IsClosed ↑F
hF : ∃ x, ¬x ∈ F
Rpos : 0 < R
this : ‖c‖ / R < 1
x : E
xF : ¬x ∈ F
hx : ∀ (y : E), y ∈ F → ‖c‖ / R * ‖x‖ ≤ ‖x - y‖
x0 : x ≠ 0
d : 𝕜
d0 : d ≠ 0
dxlt : ‖d • x‖ < R
ledx : R / ‖c‖ ≤ ‖d • x‖
y : E
hy : y ∈ F
⊢ 1 ≤ ‖d • x - y‖
[PROOFSTEP]
set y' := d⁻¹ • y
[GOAL]
case intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
inst✝⁴ : NormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F✝ : Type u_3
inst✝¹ : SeminormedAddCommGroup F✝
inst✝ : NormedSpace ℝ F✝
c : 𝕜
hc : 1 < ‖c‖
R : ℝ
hR : ‖c‖ < R
F : Subspace 𝕜 E
hFc : IsClosed ↑F
hF : ∃ x, ¬x ∈ F
Rpos : 0 < R
this : ‖c‖ / R < 1
x : E
xF : ¬x ∈ F
hx : ∀ (y : E), y ∈ F → ‖c‖ / R * ‖x‖ ≤ ‖x - y‖
x0 : x ≠ 0
d : 𝕜
d0 : d ≠ 0
dxlt : ‖d • x‖ < R
ledx : R / ‖c‖ ≤ ‖d • x‖
y : E
hy : y ∈ F
y' : E := d⁻¹ • y
⊢ 1 ≤ ‖d • x - y‖
[PROOFSTEP]
have yy' : y = d • y' := by simp [smul_smul, mul_inv_cancel d0]
[GOAL]
𝕜 : Type u_1
inst✝⁴ : NormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F✝ : Type u_3
inst✝¹ : SeminormedAddCommGroup F✝
inst✝ : NormedSpace ℝ F✝
c : 𝕜
hc : 1 < ‖c‖
R : ℝ
hR : ‖c‖ < R
F : Subspace 𝕜 E
hFc : IsClosed ↑F
hF : ∃ x, ¬x ∈ F
Rpos : 0 < R
this : ‖c‖ / R < 1
x : E
xF : ¬x ∈ F
hx : ∀ (y : E), y ∈ F → ‖c‖ / R * ‖x‖ ≤ ‖x - y‖
x0 : x ≠ 0
d : 𝕜
d0 : d ≠ 0
dxlt : ‖d • x‖ < R
ledx : R / ‖c‖ ≤ ‖d • x‖
y : E
hy : y ∈ F
y' : E := d⁻¹ • y
⊢ y = d • y'
[PROOFSTEP]
simp [smul_smul, mul_inv_cancel d0]
[GOAL]
case intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
inst✝⁴ : NormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F✝ : Type u_3
inst✝¹ : SeminormedAddCommGroup F✝
inst✝ : NormedSpace ℝ F✝
c : 𝕜
hc : 1 < ‖c‖
R : ℝ
hR : ‖c‖ < R
F : Subspace 𝕜 E
hFc : IsClosed ↑F
hF : ∃ x, ¬x ∈ F
Rpos : 0 < R
this : ‖c‖ / R < 1
x : E
xF : ¬x ∈ F
hx : ∀ (y : E), y ∈ F → ‖c‖ / R * ‖x‖ ≤ ‖x - y‖
x0 : x ≠ 0
d : 𝕜
d0 : d ≠ 0
dxlt : ‖d • x‖ < R
ledx : R / ‖c‖ ≤ ‖d • x‖
y : E
hy : y ∈ F
y' : E := d⁻¹ • y
yy' : y = d • y'
⊢ 1 ≤ ‖d • x - y‖
[PROOFSTEP]
calc
  1 = ‖c‖ / R * (R / ‖c‖) := by field_simp [Rpos.ne', (zero_lt_one.trans hc).ne']
  _ ≤ ‖c‖ / R * ‖d • x‖ := by gcongr
  _ = ‖d‖ * (‖c‖ / R * ‖x‖) := by
    simp [norm_smul]
    ring
  _ ≤ ‖d‖ * ‖x - y'‖ := by gcongr; exact hx y' (by simp [Submodule.smul_mem _ _ hy])
  _ = ‖d • x - y‖ := by rw [yy', ← smul_sub, norm_smul]
[GOAL]
𝕜 : Type u_1
inst✝⁴ : NormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F✝ : Type u_3
inst✝¹ : SeminormedAddCommGroup F✝
inst✝ : NormedSpace ℝ F✝
c : 𝕜
hc : 1 < ‖c‖
R : ℝ
hR : ‖c‖ < R
F : Subspace 𝕜 E
hFc : IsClosed ↑F
hF : ∃ x, ¬x ∈ F
Rpos : 0 < R
this : ‖c‖ / R < 1
x : E
xF : ¬x ∈ F
hx : ∀ (y : E), y ∈ F → ‖c‖ / R * ‖x‖ ≤ ‖x - y‖
x0 : x ≠ 0
d : 𝕜
d0 : d ≠ 0
dxlt : ‖d • x‖ < R
ledx : R / ‖c‖ ≤ ‖d • x‖
y : E
hy : y ∈ F
y' : E := d⁻¹ • y
yy' : y = d • y'
⊢ 1 = ‖c‖ / R * (R / ‖c‖)
[PROOFSTEP]
field_simp [Rpos.ne', (zero_lt_one.trans hc).ne']
[GOAL]
𝕜 : Type u_1
inst✝⁴ : NormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F✝ : Type u_3
inst✝¹ : SeminormedAddCommGroup F✝
inst✝ : NormedSpace ℝ F✝
c : 𝕜
hc : 1 < ‖c‖
R : ℝ
hR : ‖c‖ < R
F : Subspace 𝕜 E
hFc : IsClosed ↑F
hF : ∃ x, ¬x ∈ F
Rpos : 0 < R
this : ‖c‖ / R < 1
x : E
xF : ¬x ∈ F
hx : ∀ (y : E), y ∈ F → ‖c‖ / R * ‖x‖ ≤ ‖x - y‖
x0 : x ≠ 0
d : 𝕜
d0 : d ≠ 0
dxlt : ‖d • x‖ < R
ledx : R / ‖c‖ ≤ ‖d • x‖
y : E
hy : y ∈ F
y' : E := d⁻¹ • y
yy' : y = d • y'
⊢ ‖c‖ / R * (R / ‖c‖) ≤ ‖c‖ / R * ‖d • x‖
[PROOFSTEP]
gcongr
[GOAL]
𝕜 : Type u_1
inst✝⁴ : NormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F✝ : Type u_3
inst✝¹ : SeminormedAddCommGroup F✝
inst✝ : NormedSpace ℝ F✝
c : 𝕜
hc : 1 < ‖c‖
R : ℝ
hR : ‖c‖ < R
F : Subspace 𝕜 E
hFc : IsClosed ↑F
hF : ∃ x, ¬x ∈ F
Rpos : 0 < R
this : ‖c‖ / R < 1
x : E
xF : ¬x ∈ F
hx : ∀ (y : E), y ∈ F → ‖c‖ / R * ‖x‖ ≤ ‖x - y‖
x0 : x ≠ 0
d : 𝕜
d0 : d ≠ 0
dxlt : ‖d • x‖ < R
ledx : R / ‖c‖ ≤ ‖d • x‖
y : E
hy : y ∈ F
y' : E := d⁻¹ • y
yy' : y = d • y'
⊢ ‖c‖ / R * ‖d • x‖ = ‖d‖ * (‖c‖ / R * ‖x‖)
[PROOFSTEP]
simp [norm_smul]
[GOAL]
𝕜 : Type u_1
inst✝⁴ : NormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F✝ : Type u_3
inst✝¹ : SeminormedAddCommGroup F✝
inst✝ : NormedSpace ℝ F✝
c : 𝕜
hc : 1 < ‖c‖
R : ℝ
hR : ‖c‖ < R
F : Subspace 𝕜 E
hFc : IsClosed ↑F
hF : ∃ x, ¬x ∈ F
Rpos : 0 < R
this : ‖c‖ / R < 1
x : E
xF : ¬x ∈ F
hx : ∀ (y : E), y ∈ F → ‖c‖ / R * ‖x‖ ≤ ‖x - y‖
x0 : x ≠ 0
d : 𝕜
d0 : d ≠ 0
dxlt : ‖d • x‖ < R
ledx : R / ‖c‖ ≤ ‖d • x‖
y : E
hy : y ∈ F
y' : E := d⁻¹ • y
yy' : y = d • y'
⊢ ‖c‖ / R * (‖d‖ * ‖x‖) = ‖d‖ * (‖c‖ / R * ‖x‖)
[PROOFSTEP]
ring
[GOAL]
𝕜 : Type u_1
inst✝⁴ : NormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F✝ : Type u_3
inst✝¹ : SeminormedAddCommGroup F✝
inst✝ : NormedSpace ℝ F✝
c : 𝕜
hc : 1 < ‖c‖
R : ℝ
hR : ‖c‖ < R
F : Subspace 𝕜 E
hFc : IsClosed ↑F
hF : ∃ x, ¬x ∈ F
Rpos : 0 < R
this : ‖c‖ / R < 1
x : E
xF : ¬x ∈ F
hx : ∀ (y : E), y ∈ F → ‖c‖ / R * ‖x‖ ≤ ‖x - y‖
x0 : x ≠ 0
d : 𝕜
d0 : d ≠ 0
dxlt : ‖d • x‖ < R
ledx : R / ‖c‖ ≤ ‖d • x‖
y : E
hy : y ∈ F
y' : E := d⁻¹ • y
yy' : y = d • y'
⊢ ‖d‖ * (‖c‖ / R * ‖x‖) ≤ ‖d‖ * ‖x - y'‖
[PROOFSTEP]
gcongr
[GOAL]
case h
𝕜 : Type u_1
inst✝⁴ : NormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F✝ : Type u_3
inst✝¹ : SeminormedAddCommGroup F✝
inst✝ : NormedSpace ℝ F✝
c : 𝕜
hc : 1 < ‖c‖
R : ℝ
hR : ‖c‖ < R
F : Subspace 𝕜 E
hFc : IsClosed ↑F
hF : ∃ x, ¬x ∈ F
Rpos : 0 < R
this : ‖c‖ / R < 1
x : E
xF : ¬x ∈ F
hx : ∀ (y : E), y ∈ F → ‖c‖ / R * ‖x‖ ≤ ‖x - y‖
x0 : x ≠ 0
d : 𝕜
d0 : d ≠ 0
dxlt : ‖d • x‖ < R
ledx : R / ‖c‖ ≤ ‖d • x‖
y : E
hy : y ∈ F
y' : E := d⁻¹ • y
yy' : y = d • y'
⊢ ‖c‖ / R * ‖x‖ ≤ ‖x - y'‖
[PROOFSTEP]
exact hx y' (by simp [Submodule.smul_mem _ _ hy])
[GOAL]
𝕜 : Type u_1
inst✝⁴ : NormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F✝ : Type u_3
inst✝¹ : SeminormedAddCommGroup F✝
inst✝ : NormedSpace ℝ F✝
c : 𝕜
hc : 1 < ‖c‖
R : ℝ
hR : ‖c‖ < R
F : Subspace 𝕜 E
hFc : IsClosed ↑F
hF : ∃ x, ¬x ∈ F
Rpos : 0 < R
this : ‖c‖ / R < 1
x : E
xF : ¬x ∈ F
hx : ∀ (y : E), y ∈ F → ‖c‖ / R * ‖x‖ ≤ ‖x - y‖
x0 : x ≠ 0
d : 𝕜
d0 : d ≠ 0
dxlt : ‖d • x‖ < R
ledx : R / ‖c‖ ≤ ‖d • x‖
y : E
hy : y ∈ F
y' : E := d⁻¹ • y
yy' : y = d • y'
⊢ y' ∈ F
[PROOFSTEP]
simp [Submodule.smul_mem _ _ hy]
[GOAL]
𝕜 : Type u_1
inst✝⁴ : NormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F✝ : Type u_3
inst✝¹ : SeminormedAddCommGroup F✝
inst✝ : NormedSpace ℝ F✝
c : 𝕜
hc : 1 < ‖c‖
R : ℝ
hR : ‖c‖ < R
F : Subspace 𝕜 E
hFc : IsClosed ↑F
hF : ∃ x, ¬x ∈ F
Rpos : 0 < R
this : ‖c‖ / R < 1
x : E
xF : ¬x ∈ F
hx : ∀ (y : E), y ∈ F → ‖c‖ / R * ‖x‖ ≤ ‖x - y‖
x0 : x ≠ 0
d : 𝕜
d0 : d ≠ 0
dxlt : ‖d • x‖ < R
ledx : R / ‖c‖ ≤ ‖d • x‖
y : E
hy : y ∈ F
y' : E := d⁻¹ • y
yy' : y = d • y'
⊢ ‖d‖ * ‖x - y'‖ = ‖d • x - y‖
[PROOFSTEP]
rw [yy', ← smul_sub, norm_smul]
[GOAL]
𝕜 : Type u_1
inst✝⁴ : NormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x : F
s : Set F
hx : x ∈ s
⊢ closedBall x (infDist x sᶜ) ⊆ closure s
[PROOFSTEP]
cases' eq_or_ne (infDist x sᶜ) 0 with h₀ h₀
[GOAL]
case inl
𝕜 : Type u_1
inst✝⁴ : NormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x : F
s : Set F
hx : x ∈ s
h₀ : infDist x sᶜ = 0
⊢ closedBall x (infDist x sᶜ) ⊆ closure s
[PROOFSTEP]
rw [h₀, closedBall_zero']
[GOAL]
case inl
𝕜 : Type u_1
inst✝⁴ : NormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x : F
s : Set F
hx : x ∈ s
h₀ : infDist x sᶜ = 0
⊢ closure {x} ⊆ closure s
[PROOFSTEP]
exact closure_mono (singleton_subset_iff.2 hx)
[GOAL]
case inr
𝕜 : Type u_1
inst✝⁴ : NormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x : F
s : Set F
hx : x ∈ s
h₀ : infDist x sᶜ ≠ 0
⊢ closedBall x (infDist x sᶜ) ⊆ closure s
[PROOFSTEP]
rw [← closure_ball x h₀]
[GOAL]
case inr
𝕜 : Type u_1
inst✝⁴ : NormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x : F
s : Set F
hx : x ∈ s
h₀ : infDist x sᶜ ≠ 0
⊢ closure (ball x (infDist x sᶜ)) ⊆ closure s
[PROOFSTEP]
exact closure_mono ball_infDist_compl_subset
