-- Mathlib/Analysis/InnerProductSpace/Projection.lean
theorem exists_norm_eq_iInf_of_complete_convex {K : Set F} (ne : K.Nonempty) (h₁ : IsComplete K)
    (h₂ : Convex ℝ K) : ∀ u : F, ∃ v ∈ K, ‖u - v‖ = ⨅ w : K, ‖u - w‖ := fun u => by
  let δ := ⨅ w : K, ‖u - w‖
  letI : Nonempty K := ne.to_subtype
  have zero_le_δ : 0 ≤ δ := le_ciInf fun _ => norm_nonneg _
  have δ_le : ∀ w : K, δ ≤ ‖u - w‖ := ciInf_le ⟨0, Set.forall_mem_range.2 fun _ => norm_nonneg _⟩
  have δ_le' : ∀ w ∈ K, δ ≤ ‖u - w‖ := fun w hw => δ_le ⟨w, hw⟩
  -- Step 1: since `δ` is the infimum, can find a sequence `w : ℕ → K` in `K`
  -- such that `‖u - w n‖ < δ + 1 / (n + 1)` (which implies `‖u - w n‖ --> δ`);
  -- maybe this should be a separate lemma
  have exists_seq : ∃ w : ℕ → K, ∀ n, ‖u - w n‖ < δ + 1 / (n + 1)

Proof state:
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
K : Set F
ne : K.Nonempty
h₁ : IsComplete K
h₂ : Convex ℝ K
u : F
δ : ℝ := ⨅ w, ‖u - ↑w‖
this : Nonempty ↑K := Set.Nonempty.to_subtype ne
zero_le_δ : 0 ≤ δ
δ_le : ∀ (w : ↑K), δ ≤ ‖u - ↑w‖
δ_le' : ∀ w ∈ K, δ ≤ ‖u - w‖
w : ℕ → ↑K
hw : ∀ (n : ℕ), ‖u - ↑(w n)‖ < δ + 1 / (↑n + 1)
norm_tendsto : Tendsto (fun n => ‖u - ↑(w n)‖) atTop (𝓝 δ)
b : ℕ → ℝ := fun n => 8 * δ * (1 / (↑n + 1)) + 4 * (1 / (↑n + 1)) * (1 / (↑n + 1))
⊢ √(8 * δ * 0 + 4 * 0 * 0) = 0

Tactic:
simp

Result:
no goals

Proof state:
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
K : Set F
ne : K.Nonempty
h₁ : IsComplete K
h₂ : Convex ℝ K
u : F
δ : ℝ := ⨅ w, ‖u - ↑w‖
this : Nonempty ↑K := Set.Nonempty.to_subtype ne
zero_le_δ : 0 ≤ δ
δ_le : ∀ (w : ↑K), δ ≤ ‖u - ↑w‖
δ_le' : ∀ w ∈ K, δ ≤ ‖u - w‖
w : ℕ → ↑K
hw : ∀ (n : ℕ), ‖u - ↑(w n)‖ < δ + 1 / (↑n + 1)
norm_tendsto : Tendsto (fun n => ‖u - ↑(w n)‖) atTop (𝓝 δ)
b✝ : ℕ → ℝ := fun n => 8 * δ * (1 / (↑n + 1)) + 4 * (1 / (↑n + 1)) * (1 / (↑n + 1))
p q N : ℕ
hp : N ≤ p
hq : N ≤ q
wp : F := ↑(w p)
wq : F := ↑(w q)
a : F := u - wq
b : F := u - wp
half : ℝ := 1 / 2
div : ℝ := 1 / (↑N + 1)
⊢ ‖1 • u + 1 • u - 1 • (wq + wp)‖ * ‖1 • u + 1 • u - 1 • (wq + wp)‖ + ‖wp - wq‖ * ‖wp - wq‖ =
    ‖a + b‖ * ‖a + b‖ + ‖a - b‖ * ‖a - b‖

Tactic:
simp only [one_smul]

Result:
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
K : Set F
ne : K.Nonempty
h₁ : IsComplete K
h₂ : Convex ℝ K
u : F
δ : ℝ := ⨅ w, ‖u - ↑w‖
this : Nonempty ↑K := Set.Nonempty.to_subtype ne
zero_le_δ : 0 ≤ δ
δ_le : ∀ (w : ↑K), δ ≤ ‖u - ↑w‖
δ_le' : ∀ w ∈ K, δ ≤ ‖u - w‖
w : ℕ → ↑K
hw : ∀ (n : ℕ), ‖u - ↑(w n)‖ < δ + 1 / (↑n + 1)
norm_tendsto : Tendsto (fun n => ‖u - ↑(w n)‖) atTop (𝓝 δ)
b✝ : ℕ → ℝ := fun n => 8 * δ * (1 / (↑n + 1)) + 4 * (1 / (↑n + 1)) * (1 / (↑n + 1))
p q N : ℕ
hp : N ≤ p
hq : N ≤ q
wp : F := ↑(w p)
wq : F := ↑(w q)
a : F := u - wq
b : F := u - wp
half : ℝ := 1 / 2
div : ℝ := 1 / (↑N + 1)
⊢ ‖u + u - (wq + wp)‖ * ‖u + u - (wq + wp)‖ + ‖wp - wq‖ * ‖wp - wq‖ = ‖a + b‖ * ‖a + b‖ + ‖a - b‖ * ‖a - b‖

Proof state:
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
K : Set F
ne : K.Nonempty
h₁ : IsComplete K
h₂ : Convex ℝ K
u : F
δ : ℝ := ⨅ w, ‖u - ↑w‖
this : Nonempty ↑K := Set.Nonempty.to_subtype ne
zero_le_δ : 0 ≤ δ
δ_le : ∀ (w : ↑K), δ ≤ ‖u - ↑w‖
δ_le' : ∀ w ∈ K, δ ≤ ‖u - w‖
⊢ ∃ v ∈ K, ‖u - v‖ = ⨅ w, ‖u - ↑w‖

Tactic:
have exists_seq : ∃ w : ℕ → K, ∀ n, ‖u - w n‖ < δ + 1 / (n + 1) := by
  have hδ : ∀ n : ℕ, δ < δ + 1 / (n + 1) := fun n =>
    lt_add_of_le_of_pos le_rfl Nat.one_div_pos_of_nat
  have h := fun n => exists_lt_of_ciInf_lt (hδ n)
  let w : ℕ → K := fun n => Classical.choose (h n)
  exact ⟨w, fun n => Classical.choose_spec (h n)⟩

Result:
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
K : Set F
ne : K.Nonempty
h₁ : IsComplete K
h₂ : Convex ℝ K
u : F
δ : ℝ := ⨅ w, ‖u - ↑w‖
this : Nonempty ↑K := Set.Nonempty.to_subtype ne
zero_le_δ : 0 ≤ δ
δ_le : ∀ (w : ↑K), δ ≤ ‖u - ↑w‖
δ_le' : ∀ w ∈ K, δ ≤ ‖u - w‖
exists_seq : ∃ w, ∀ (n : ℕ), ‖u - ↑(w n)‖ < δ + 1 / (↑n + 1)
⊢ ∃ v ∈ K, ‖u - v‖ = ⨅ w, ‖u - ↑w‖

Proof state:
case h
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
K : Set F
ne : K.Nonempty
h₁ : IsComplete K
h₂ : Convex ℝ K
u : F
δ : ℝ := ⨅ w, ‖u - ↑w‖
this : Nonempty ↑K := Set.Nonempty.to_subtype ne
zero_le_δ : 0 ≤ δ
δ_le : ∀ (w : ↑K), δ ≤ ‖u - ↑w‖
δ_le' : ∀ w ∈ K, δ ≤ ‖u - w‖
w : ℕ → ↑K
hw : ∀ (n : ℕ), ‖u - ↑(w n)‖ < δ + 1 / (↑n + 1)
norm_tendsto : Tendsto (fun n => ‖u - ↑(w n)‖) atTop (𝓝 δ)
b : ℕ → ℝ := fun n => 8 * δ * (1 / (↑n + 1)) + 4 * (1 / (↑n + 1)) * (1 / (↑n + 1))
⊢ (∀ (n : ℕ), 0 ≤ (fun n => √(b n)) n) ∧
    (∀ (n m N : ℕ), N ≤ n → N ≤ m → dist ↑(w n) ↑(w m) ≤ (fun n => √(b n)) N) ∧ Tendsto (fun n => √(b n)) atTop (𝓝 0)

Tactic:
constructor

Result:
case h.left
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
K : Set F
ne : K.Nonempty
h₁ : IsComplete K
h₂ : Convex ℝ K
u : F
δ : ℝ := ⨅ w, ‖u - ↑w‖
this : Nonempty ↑K := Set.Nonempty.to_subtype ne
zero_le_δ : 0 ≤ δ
δ_le : ∀ (w : ↑K), δ ≤ ‖u - ↑w‖
δ_le' : ∀ w ∈ K, δ ≤ ‖u - w‖
w : ℕ → ↑K
hw : ∀ (n : ℕ), ‖u - ↑(w n)‖ < δ + 1 / (↑n + 1)
norm_tendsto : Tendsto (fun n => ‖u - ↑(w n)‖) atTop (𝓝 δ)
b : ℕ → ℝ := fun n => 8 * δ * (1 / (↑n + 1)) + 4 * (1 / (↑n + 1)) * (1 / (↑n + 1))
⊢ ∀ (n : ℕ), 0 ≤ √(b n)

case h.right
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
K : Set F
ne : K.Nonempty
h₁ : IsComplete K
h₂ : Convex ℝ K
u : F
δ : ℝ := ⨅ w, ‖u - ↑w‖
this : Nonempty ↑K := Set.Nonempty.to_subtype ne
zero_le_δ : 0 ≤ δ
δ_le : ∀ (w : ↑K), δ ≤ ‖u - ↑w‖
δ_le' : ∀ w ∈ K, δ ≤ ‖u - w‖
w : ℕ → ↑K
hw : ∀ (n : ℕ), ‖u - ↑(w n)‖ < δ + 1 / (↑n + 1)
norm_tendsto : Tendsto (fun n => ‖u - ↑(w n)‖) atTop (𝓝 δ)
b : ℕ → ℝ := fun n => 8 * δ * (1 / (↑n + 1)) + 4 * (1 / (↑n + 1)) * (1 / (↑n + 1))
⊢ (∀ (n m N : ℕ), N ≤ n → N ≤ m → dist ↑(w n) ↑(w m) ≤ √(b N)) ∧ Tendsto (fun n => √(b n)) atTop (𝓝 0)

Proof state:
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
K : Set F
ne : K.Nonempty
h₁ : IsComplete K
h₂ : Convex ℝ K
u : F
δ : ℝ := ⨅ w, ‖u - ↑w‖
this : Nonempty ↑K := Set.Nonempty.to_subtype ne
zero_le_δ : 0 ≤ δ
δ_le : ∀ (w : ↑K), δ ≤ ‖u - ↑w‖
δ_le' : ∀ w ∈ K, δ ≤ ‖u - w‖
w : ℕ → ↑K
hw : ∀ (n : ℕ), ‖u - ↑(w n)‖ < δ + 1 / (↑n + 1)
norm_tendsto : Tendsto (fun n => ‖u - ↑(w n)‖) atTop (𝓝 δ)
b✝ : ℕ → ℝ := fun n => 8 * δ * (1 / (↑n + 1)) + 4 * (1 / (↑n + 1)) * (1 / (↑n + 1))
p q N : ℕ
hp : N ≤ p
hq : N ≤ q
wp : F := ↑(w p)
wq : F := ↑(w q)
a : F := u - wq
b : F := u - wp
half : ℝ := 1 / 2
div : ℝ := 1 / (↑N + 1)
eq₁ : wp - wq = a - b
⊢ u + u - (wq + wp) = a + b

Tactic:
show u + u - (wq + wp) = u - wq + (u - wp)

Result:
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
K : Set F
ne : K.Nonempty
h₁ : IsComplete K
h₂ : Convex ℝ K
u : F
δ : ℝ := ⨅ w, ‖u - ↑w‖
this : Nonempty ↑K := Set.Nonempty.to_subtype ne
zero_le_δ : 0 ≤ δ
δ_le : ∀ (w : ↑K), δ ≤ ‖u - ↑w‖
δ_le' : ∀ w ∈ K, δ ≤ ‖u - w‖
w : ℕ → ↑K
hw : ∀ (n : ℕ), ‖u - ↑(w n)‖ < δ + 1 / (↑n + 1)
norm_tendsto : Tendsto (fun n => ‖u - ↑(w n)‖) atTop (𝓝 δ)
b✝ : ℕ → ℝ := fun n => 8 * δ * (1 / (↑n + 1)) + 4 * (1 / (↑n + 1)) * (1 / (↑n + 1))
p q N : ℕ
hp : N ≤ p
hq : N ≤ q
wp : F := ↑(w p)
wq : F := ↑(w q)
a : F := u - wq
b : F := u - wp
half : ℝ := 1 / 2
div : ℝ := 1 / (↑N + 1)
eq₁ : wp - wq = a - b
⊢ u + u - (wq + wp) = u - wq + (u - wp)