no goals
𝕜 : Type u_1
inst✝⁴ : NormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F✝ : Type ?u.309
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‖
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]
case intro
𝕜 : Type u_1
inst✝⁴ : NormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F✝ : Type ?u.309
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‖
𝕜 : Type u_1
inst✝⁴ : NormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F✝ : Type ?u.309
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‖
obtain ⟨x, hx⟩ : ∃ x : E, x ∉ F := hF
case intro
𝕜 : Type u_1
inst✝⁴ : NormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F✝ : Type ?u.309
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‖
case intro
𝕜 : Type u_1
inst✝⁴ : NormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F✝ : Type ?u.309
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‖
let d := Metric.infDist x F
case intro
𝕜 : Type u_1
inst✝⁴ : NormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F✝ : Type ?u.309
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‖
case intro
𝕜 : Type u_1
inst✝⁴ : NormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F✝ : Type ?u.309
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‖
have hFn : (F : Set E).Nonempty := ⟨_, F.zero_mem⟩
case intro
𝕜 : Type u_1
inst✝⁴ : NormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F✝ : Type ?u.309
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‖
case intro
𝕜 : Type u_1
inst✝⁴ : NormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F✝ : Type ?u.309
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‖
have hdp : 0 < d :=
  lt_of_le_of_ne Metric.infDist_nonneg fun heq =>
    hx ((hFc.mem_iff_infDist_zero hFn).2 heq.symm)
case intro
𝕜 : Type u_1
inst✝⁴ : NormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F✝ : Type ?u.309
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‖
case intro
𝕜 : Type u_1
inst✝⁴ : NormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F✝ : Type ?u.309
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‖
let r' := max r 2⁻¹
case intro
𝕜 : Type u_1
inst✝⁴ : NormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F✝ : Type ?u.309
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‖
case intro
𝕜 : Type u_1
inst✝⁴ : NormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F✝ : Type ?u.309
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‖
have hr' : r' < 1 := by
  simp [hr]
  norm_num
case intro
𝕜 : Type u_1
inst✝⁴ : NormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F✝ : Type ?u.309
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‖
case intro
𝕜 : Type u_1
inst✝⁴ : NormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F✝ : Type ?u.309
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‖
have hlt : 0 < r' := lt_of_lt_of_le (by norm_num) (le_max_right r 2⁻¹)
case intro
𝕜 : Type u_1
inst✝⁴ : NormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F✝ : Type ?u.309
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‖
case intro
𝕜 : Type u_1
inst✝⁴ : NormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F✝ : Type ?u.309
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‖
have hdlt : d < d / r' := (lt_div_iff hlt).mpr ((mul_lt_iff_lt_one_right hdp).2 hr')
case intro.intro.intro
𝕜 : Type u_1
inst✝⁴ : NormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F✝ : Type ?u.309
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‖
case intro
𝕜 : Type u_1
inst✝⁴ : NormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F✝ : Type ?u.309
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‖
obtain ⟨y₀, hy₀F, hxy₀⟩ : ∃ y ∈ F, dist x y < d / r' := (Metric.infDist_lt_iff hFn).mp hdlt
case intro.intro.intro
𝕜 : Type u_1
inst✝⁴ : NormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F✝ : Type ?u.309
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‖
case intro.intro.intro
𝕜 : Type u_1
inst✝⁴ : NormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F✝ : Type ?u.309
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‖
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
case intro.intro.intro
𝕜 : Type u_1
inst✝⁴ : NormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F✝ : Type ?u.309
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‖
case intro.intro.intro
𝕜 : Type u_1
inst✝⁴ : NormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F✝ : Type ?u.309
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‖
refine' ⟨x - y₀, x_ne_y₀, fun y hy => le_of_lt _⟩
case intro.intro.intro
𝕜 : Type u_1
inst✝⁴ : NormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F✝ : Type ?u.309
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‖
case intro.intro.intro
𝕜 : Type u_1
inst✝⁴ : NormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F✝ : Type ?u.309
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‖
have hy₀y : y₀ + y ∈ F := F.add_mem hy₀F hy
no goals
case intro.intro.intro
𝕜 : Type u_1
inst✝⁴ : NormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F✝ : Type ?u.309
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‖
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]
𝕜 : Type u_1
inst✝⁴ : NormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F✝ : Type ?u.309
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
𝕜 : Type u_1
inst✝⁴ : NormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F✝ : Type ?u.309
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
simp [hr]
no goals
𝕜 : Type u_1
inst✝⁴ : NormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F✝ : Type ?u.309
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
norm_num
no goals
𝕜 : Type u_1
inst✝⁴ : NormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F✝ : Type ?u.309
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⁻¹
norm_num
𝕜 : Type u_1
inst✝⁴ : NormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F✝ : Type ?u.309
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
𝕜 : Type u_1
inst✝⁴ : NormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F✝ : Type ?u.309
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
by_contra h
𝕜 : Type u_1
inst✝⁴ : NormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F✝ : Type ?u.309
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
𝕜 : Type u_1
inst✝⁴ : NormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F✝ : Type ?u.309
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
have : x - y₀ + y₀ ∈ F := F.add_mem h hy₀F
𝕜 : Type u_1
inst✝⁴ : NormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F✝ : Type ?u.309
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
𝕜 : Type u_1
inst✝⁴ : NormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F✝ : Type ?u.309
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
simp only [neg_add_cancel_right, sub_eq_add_neg] at this
no goals
𝕜 : Type u_1
inst✝⁴ : NormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F✝ : Type ?u.309
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
exact hx this
case h
𝕜 : Type u_1
inst✝⁴ : NormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F✝ : Type ?u.309
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'
𝕜 : Type u_1
inst✝⁴ : NormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F✝ : Type ?u.309
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₀‖
gcongr
no goals
case h
𝕜 : Type u_1
inst✝⁴ : NormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F✝ : Type ?u.309
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'
apply le_max_left
𝕜 : Type u_1
inst✝⁴ : NormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F✝ : Type ?u.309
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
𝕜 : Type u_1
inst✝⁴ : NormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F✝ : Type ?u.309
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
rw [← dist_eq_norm]
no goals
𝕜 : Type u_1
inst✝⁴ : NormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F✝ : Type ?u.309
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
exact (lt_div_iff' hlt).1 hxy₀
no goals
𝕜 : Type u_1
inst✝⁴ : NormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F✝ : Type ?u.309
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‖
rw [sub_sub, dist_eq_norm]