awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Minimal
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
K : Set F
ne : K.Nonempty
h₁ : IsComplete K
h₂ : Convex ℝ K
u : F
δ : ℝ := ⨅ (w : (↑K : Type u_3)), ‖u - (↑w : F)‖
this : Nonempty.{u_3 + 1} (↑K : Type u_3) := ⋯
zero_le_δ : 0 ≤ δ
δ_le : ∀ (w : (↑K : Type u_3)), δ ≤ ‖u - (↑w : F)‖
δ_le' : ∀ w ∈ K, δ ≤ ‖u - w‖
w : ℕ → (↑K : Type u_3)
hw : ∀ (n : ℕ), ‖u - (↑(w n) : F)‖ < δ + 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
norm_tendsto : Tendsto (fun (n : ℕ) ↦ ‖u - (↑(w n) : F)‖) atTop (𝓝 δ)
b : (n : ℕ) → ℝ :=
  fun (n : ℕ) ↦
    8 * δ * (1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) +
      4 * (1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) * (1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
h : Tendsto (β := ℝ) (fun (x : ℝ) ↦ √(8 * δ * x + 4 * x * x)) (𝓝 0) (𝓝 0)
⊢ Tendsto (β := ℝ) (fun (n : ℕ) ↦ √(b n)) atTop (𝓝 0)

Tactic:
suffices Tendsto (fun x ↦ √(8 * δ * x + 4 * x * x) : ℝ → ℝ) (𝓝 0) (𝓝 0)
      from this.comp tendsto_one_div_add_atTop_nhds_zero_nat
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Minimal
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
K : Set F
ne : K.Nonempty
h₁ : IsComplete K
h₂ : Convex ℝ K
u : F
δ : ℝ := ⨅ (w : (↑K : Type u_3)), ‖u - (↑w : F)‖
this : Nonempty.{u_3 + 1} (↑K : Type u_3) := ⋯
zero_le_δ : 0 ≤ δ
δ_le : ∀ (w : (↑K : Type u_3)), δ ≤ ‖u - (↑w : F)‖
δ_le' : ∀ w ∈ K, δ ≤ ‖u - w‖
w : ℕ → (↑K : Type u_3)
hw : ∀ (n : ℕ), ‖u - (↑(w n) : F)‖ < δ + 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
norm_tendsto : Tendsto (fun (n : ℕ) ↦ ‖u - (↑(w n) : F)‖) atTop (𝓝 δ)
b : (n : ℕ) → ℝ :=
  fun (n : ℕ) ↦
    8 * δ * (1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) +
      4 * (1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) * (1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
⊢ Continuous (Y := ℝ) fun (x : ℝ) ↦ √(8 * δ * x + 4 * x * x)

Tactic:
fun_prop
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Minimal
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
K : Set F
ne : K.Nonempty
h₁ : IsComplete K
h₂ : Convex ℝ K
u : F
δ : ℝ := ⨅ (w : (↑K : Type u_3)), ‖u - (↑w : F)‖
this : Nonempty.{u_3 + 1} (↑K : Type u_3) := ⋯
zero_le_δ : 0 ≤ δ
δ_le : ∀ (w : (↑K : Type u_3)), δ ≤ ‖u - (↑w : F)‖
δ_le' : ∀ w ∈ K, δ ≤ ‖u - w‖
w : ℕ → (↑K : Type u_3)
hw : ∀ (n : ℕ), ‖u - (↑(w n) : F)‖ < δ + 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
norm_tendsto : Tendsto (fun (n : ℕ) ↦ ‖u - (↑(w n) : F)‖) atTop (𝓝 δ)
b : (n : ℕ) → ℝ :=
  fun (n : ℕ) ↦
    8 * δ * (1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) +
      4 * (1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) * (1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
⊢ √(8 * δ * 0 + HMul.hMul (α := ℝ) 4 0 * 0) = 0

Tactic:
simp
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Minimal
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
K : Set F
ne : K.Nonempty
h₁ : IsComplete K
h₂ : Convex ℝ K
u : F
δ : ℝ := ⨅ (w : (↑K : Type u_3)), ‖u - (↑w : F)‖
this : Nonempty.{u_3 + 1} (↑K : Type u_3) := ⋯
zero_le_δ : 0 ≤ δ
δ_le : ∀ (w : (↑K : Type u_3)), δ ≤ ‖u - (↑w : F)‖
δ_le' : ∀ w ∈ K, δ ≤ ‖u - w‖
w : ℕ → (↑K : Type u_3)
hw : ∀ (n : ℕ), ‖u - (↑(w n) : F)‖ < δ + 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
norm_tendsto : Tendsto (fun (n : ℕ) ↦ ‖u - (↑(w n) : F)‖) atTop (𝓝 δ)
b : (n : ℕ) → ℝ :=
  fun (n : ℕ) ↦
    8 * δ * (1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) +
      4 * (1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) * (1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ √(8 * δ * x + 4 * x * x)) (𝓝 0) (𝓝 0)

Tactic:
exact Continuous.tendsto' (by fun_prop) _ _ (by simp)

Premises used: Continuous.tendsto'
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Minimal
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
K : Set F
ne : K.Nonempty
h₁ : IsComplete K
h₂ : Convex ℝ K
u : F
δ : ℝ := ⨅ (w : (↑K : Type u_3)), ‖u - (↑w : F)‖
this : Nonempty.{u_3 + 1} (↑K : Type u_3) := ⋯
zero_le_δ : 0 ≤ δ
δ_le : ∀ (w : (↑K : Type u_3)), δ ≤ ‖u - (↑w : F)‖
δ_le' : ∀ w ∈ K, δ ≤ ‖u - w‖
w : ℕ → (↑K : Type u_3)
hw : ∀ (n : ℕ), ‖u - (↑(w n) : F)‖ < δ + 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
norm_tendsto : Tendsto (fun (n : ℕ) ↦ ‖u - (↑(w n) : F)‖) atTop (𝓝 δ)
seq_is_cauchy : CauchySeq.{u_3, 0} (α := F) fun (n : ℕ) ↦ (↑(w n) : F)
rcases :
  ∀ (v : F) (hv : v ∈ K) (w_tendsto : Tendsto (fun (n : ℕ) ↦ (↑(w n) : F)) atTop (𝓝 v)),
    ∃ v ∈ K, ‖u - v‖ = ⨅ (w : (↑K : Type u_3)), ‖u - (↑w : F)‖
⊢ ∃ v ∈ K, ‖u - v‖ = ⨅ (w : (↑K : Type u_3)), ‖u - (↑w : F)‖

Tactic:
rcases cauchySeq_tendsto_of_isComplete h₁ (fun n => Subtype.mem _) seq_is_cauchy with
    ⟨v, hv, w_tendsto⟩

Premises used: cauchySeq_tendsto_of_isComplete, Subtype.mem
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Minimal
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
K : Set F
ne : K.Nonempty
h₁ : IsComplete K
h₂ : Convex ℝ K
u : F
δ : ℝ := ⨅ (w : (↑K : Type u_3)), ‖u - (↑w : F)‖
this : Nonempty.{u_3 + 1} (↑K : Type u_3) := ⋯
zero_le_δ : 0 ≤ δ
δ_le : ∀ (w : (↑K : Type u_3)), δ ≤ ‖u - (↑w : F)‖
δ_le' : ∀ w ∈ K, δ ≤ ‖u - w‖
w : ℕ → (↑K : Type u_3)
hw : ∀ (n : ℕ), ‖u - (↑(w n) : F)‖ < δ + 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
norm_tendsto : Tendsto (fun (n : ℕ) ↦ ‖u - (↑(w n) : F)‖) atTop (𝓝 δ)
seq_is_cauchy : CauchySeq.{u_3, 0} (α := F) fun (n : ℕ) ↦ (↑(w n) : F)
v : F
hv : v ∈ K
w_tendsto : Tendsto (fun (n : ℕ) ↦ (↑(w n) : F)) atTop (𝓝 v)
right : ‖u - v‖ = ⨅ (w : (↑K : Type u_3)), ‖u - (↑w : F)‖
⊢ ∃ v ∈ K, ‖u - v‖ = ⨅ (w : (↑K : Type u_3)), ‖u - (↑w : F)‖

Tactic:
use v, hv
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Minimal
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
K : Set F
ne : K.Nonempty
h₁ : IsComplete K
h₂ : Convex ℝ K
u : F
δ : ℝ := ⨅ (w : (↑K : Type u_3)), ‖u - (↑w : F)‖
this : Nonempty.{u_3 + 1} (↑K : Type u_3) := ⋯
zero_le_δ : 0 ≤ δ
δ_le : ∀ (w : (↑K : Type u_3)), δ ≤ ‖u - (↑w : F)‖
δ_le' : ∀ w ∈ K, δ ≤ ‖u - w‖
w : ℕ → (↑K : Type u_3)
hw : ∀ (n : ℕ), ‖u - (↑(w n) : F)‖ < δ + 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
norm_tendsto : Tendsto (fun (n : ℕ) ↦ ‖u - (↑(w n) : F)‖) atTop (𝓝 δ)
seq_is_cauchy : CauchySeq.{u_3, 0} (α := F) fun (n : ℕ) ↦ (↑(w n) : F)
v : F
hv : v ∈ K
w_tendsto : Tendsto (fun (n : ℕ) ↦ (↑(w n) : F)) atTop (𝓝 v)
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] fun (v : F) ↦ ‖u - v‖

Tactic:
fun_prop
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Minimal
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
K : Set F
ne : K.Nonempty
h₁ : IsComplete K
h₂ : Convex ℝ K
u : F
δ : ℝ := ⨅ (w : (↑K : Type u_3)), ‖u - (↑w : F)‖
this : Nonempty.{u_3 + 1} (↑K : Type u_3) := ⋯
zero_le_δ : 0 ≤ δ
δ_le : ∀ (w : (↑K : Type u_3)), δ ≤ ‖u - (↑w : F)‖
δ_le' : ∀ w ∈ K, δ ≤ ‖u - w‖
w : ℕ → (↑K : Type u_3)
hw : ∀ (n : ℕ), ‖u - (↑(w n) : F)‖ < δ + 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
norm_tendsto : Tendsto (fun (n : ℕ) ↦ ‖u - (↑(w n) : F)‖) atTop (𝓝 δ)
seq_is_cauchy : CauchySeq.{u_3, 0} (α := F) fun (n : ℕ) ↦ (↑(w n) : F)
v : F
hv : v ∈ K
w_tendsto : Tendsto (fun (n : ℕ) ↦ (↑(w n) : F)) atTop (𝓝 v)
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] fun (v : F) ↦ ‖u - v‖

Tactic:
have h_cont : Continuous fun v => ‖u - v‖ := by fun_prop
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Minimal
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
K : Set F
ne : K.Nonempty
h₁ : IsComplete K
h₂ : Convex ℝ K
u : F
δ : ℝ := ⨅ (w : (↑K : Type u_3)), ‖u - (↑w : F)‖
this : Nonempty.{u_3 + 1} (↑K : Type u_3) := ⋯
zero_le_δ : 0 ≤ δ
δ_le : ∀ (w : (↑K : Type u_3)), δ ≤ ‖u - (↑w : F)‖
δ_le' : ∀ w ∈ K, δ ≤ ‖u - w‖
w : ℕ → (↑K : Type u_3)
hw : ∀ (n : ℕ), ‖u - (↑(w n) : F)‖ < δ + 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
norm_tendsto : Tendsto (fun (n : ℕ) ↦ ‖u - (↑(w n) : F)‖) atTop (𝓝 δ)
seq_is_cauchy : CauchySeq.{u_3, 0} (α := F) fun (n : ℕ) ↦ (↑(w n) : F)
v : F
hv : v ∈ K
w_tendsto : Tendsto (fun (n : ℕ) ↦ (↑(w n) : F)) atTop (𝓝 v)
h_cont : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] fun (v : F) ↦ ‖u - v‖
⊢ Tendsto (α := ℕ) (β := ℝ) ((fun (v : F) ↦ ‖u - v‖) ∘ fun (n : ℕ) ↦ (↑(w n) : F)) atTop (𝓝 ((fun (v : F) ↦ ‖u - v‖) v))

Tactic:
Tendsto.comp h_cont.continuousAt w_tendsto

Premises used: Continuous.continuousAt, Filter.Tendsto.comp
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Minimal
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
K : Set F
ne : K.Nonempty
h₁ : IsComplete K
h₂ : Convex ℝ K
u : F
δ : ℝ := ⨅ (w : (↑K : Type u_3)), ‖u - (↑w : F)‖
this : Nonempty.{u_3 + 1} (↑K : Type u_3) := ⋯
zero_le_δ : 0 ≤ δ
δ_le : ∀ (w : (↑K : Type u_3)), δ ≤ ‖u - (↑w : F)‖
δ_le' : ∀ w ∈ K, δ ≤ ‖u - w‖
w : ℕ → (↑K : Type u_3)
hw : ∀ (n : ℕ), ‖u - (↑(w n) : F)‖ < δ + 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
norm_tendsto : Tendsto (fun (n : ℕ) ↦ ‖u - (↑(w n) : F)‖) atTop (𝓝 δ)
seq_is_cauchy : CauchySeq.{u_3, 0} (α := F) fun (n : ℕ) ↦ (↑(w n) : F)
v : F
hv : v ∈ K
w_tendsto : Tendsto (fun (n : ℕ) ↦ (↑(w n) : F)) atTop (𝓝 v)
h_cont : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] fun (v : F) ↦ ‖u - v‖
⊢ Tendsto (fun (n : ℕ) ↦ ‖u - (↑(w n) : F)‖) atTop (𝓝 ‖u - v‖)

Tactic:
convert! Tendsto.comp h_cont.continuousAt w_tendsto

Premises used: Continuous.continuousAt, Filter.Tendsto.comp
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Minimal
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
K : Set F
ne : K.Nonempty
h₁ : IsComplete K
h₂ : Convex ℝ K
u : F
δ : ℝ := ⨅ (w : (↑K : Type u_3)), ‖u - (↑w : F)‖
this : Nonempty.{u_3 + 1} (↑K : Type u_3) := ⋯
zero_le_δ : 0 ≤ δ
δ_le : ∀ (w : (↑K : Type u_3)), δ ≤ ‖u - (↑w : F)‖
δ_le' : ∀ w ∈ K, δ ≤ ‖u - w‖
w : ℕ → (↑K : Type u_3)
hw : ∀ (n : ℕ), ‖u - (↑(w n) : F)‖ < δ + 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
norm_tendsto : Tendsto (fun (n : ℕ) ↦ ‖u - (↑(w n) : F)‖) atTop (𝓝 δ)
seq_is_cauchy : CauchySeq.{u_3, 0} (α := F) fun (n : ℕ) ↦ (↑(w n) : F)
v : F
hv : v ∈ K
w_tendsto : Tendsto (fun (n : ℕ) ↦ (↑(w n) : F)) atTop (𝓝 v)
h_cont : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] fun (v : F) ↦ ‖u - v‖
⊢ Tendsto (fun (n : ℕ) ↦ ‖u - (↑(w n) : F)‖) atTop (𝓝 ‖u - v‖)

Tactic:
have : Tendsto (fun n => ‖u - w n‖) atTop (𝓝 ‖u - v‖) := by
    convert! Tendsto.comp h_cont.continuousAt w_tendsto
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Minimal
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
K : Set F
ne : K.Nonempty
h₁ : IsComplete K
h₂ : Convex ℝ K
u : F
δ : ℝ := ⨅ (w : (↑K : Type u_3)), ‖u - (↑w : F)‖
this_1 : Nonempty.{u_3 + 1} (↑K : Type u_3) := ⋯
zero_le_δ : 0 ≤ δ
δ_le : ∀ (w : (↑K : Type u_3)), δ ≤ ‖u - (↑w : F)‖
δ_le' : ∀ w ∈ K, δ ≤ ‖u - w‖
w : ℕ → (↑K : Type u_3)
hw : ∀ (n : ℕ), ‖u - (↑(w n) : F)‖ < δ + 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
norm_tendsto : Tendsto (fun (n : ℕ) ↦ ‖u - (↑(w n) : F)‖) atTop (𝓝 δ)
seq_is_cauchy : CauchySeq.{u_3, 0} (α := F) fun (n : ℕ) ↦ (↑(w n) : F)
v : F
hv : v ∈ K
w_tendsto : Tendsto (fun (n : ℕ) ↦ (↑(w n) : F)) atTop (𝓝 v)
h_cont : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] fun (v : F) ↦ ‖u - v‖
this : Tendsto (fun (n : ℕ) ↦ ‖u - (↑(w n) : F)‖) atTop (𝓝 ‖u - v‖)
⊢ ‖u - v‖ = ⨅ (w : (↑K : Type u_3)), ‖u - (↑w : F)‖

Tactic:
tendsto_nhds_unique this norm_tendsto

Premises used: tendsto_nhds_unique
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Minimal
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
K : Set F
ne : K.Nonempty
h₁ : IsComplete K
h₂ : Convex ℝ K
u : F
δ : ℝ := ⨅ (w : (↑K : Type u_3)), ‖u - (↑w : F)‖
this_1 : Nonempty.{u_3 + 1} (↑K : Type u_3) := ⋯
zero_le_δ : 0 ≤ δ
δ_le : ∀ (w : (↑K : Type u_3)), δ ≤ ‖u - (↑w : F)‖
δ_le' : ∀ w ∈ K, δ ≤ ‖u - w‖
w : ℕ → (↑K : Type u_3)
hw : ∀ (n : ℕ), ‖u - (↑(w n) : F)‖ < δ + 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
norm_tendsto : Tendsto (fun (n : ℕ) ↦ ‖u - (↑(w n) : F)‖) atTop (𝓝 δ)
seq_is_cauchy : CauchySeq.{u_3, 0} (α := F) fun (n : ℕ) ↦ (↑(w n) : F)
v : F
hv : v ∈ K
w_tendsto : Tendsto (fun (n : ℕ) ↦ (↑(w n) : F)) atTop (𝓝 v)
h_cont : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] fun (v : F) ↦ ‖u - v‖
this : Tendsto (fun (n : ℕ) ↦ ‖u - (↑(w n) : F)‖) atTop (𝓝 ‖u - v‖)
⊢ ‖u - v‖ = ⨅ (w : (↑K : Type u_3)), ‖u - (↑w : F)‖

Tactic:
exact tendsto_nhds_unique this norm_tendsto

Premises used: tendsto_nhds_unique
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Minimal
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
K : Set F
h : Convex ℝ K
u v : F
hv : v ∈ K
this : Nonempty.{u_3 + 1} (↑K : Type u_3) := ⋯
mp : ‖u - v‖ = ⨅ (w : (↑K : Type u_3)), ‖u - (↑w : F)‖ → ∀ w ∈ K, ⟪u - v, w - v⟫_ℝ ≤ 0
mpr : (∀ w ∈ K, ⟪u - v, w - v⟫_ℝ ≤ 0) → ‖u - v‖ = ⨅ (w : (↑K : Type u_3)), ‖u - (↑w : F)‖
⊢ ‖u - v‖ = ⨅ (w : (↑K : Type u_3)), ‖u - (↑w : F)‖ ↔ ∀ w ∈ K, ⟪u - v, w - v⟫_ℝ ≤ 0

Tactic:
constructor
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Minimal
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
K : Set F
h : Convex ℝ K
u v : F
hv : v ∈ K
this : Nonempty.{u_3 + 1} (↑K : Type u_3) := ⋯
eq : ‖u - v‖ = ⨅ (w : (↑K : Type u_3)), ‖u - (↑w : F)‖
w : F
hw : w ∈ K
δ : ℝ := ⨅ (w : (↑K : Type u_3)), ‖u - (↑w : F)‖
p : ℝ := ⟪u - v, w - v⟫_ℝ
q : ℝ := HPow.hPow (β := ℕ) ‖w - v‖ 2
⊢ ∀ (w : (↑K : Type u_3)), δ ≤ ‖u - (↑w : F)‖

Tactic:
have δ_le (w : K) : δ ≤ ‖u - w‖ := ciInf_le ⟨0, fun _ ⟨_, h⟩ => h ▸ norm_nonneg _⟩ _
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Minimal
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
K : Set F
h : Convex ℝ K
u v : F
hv : v ∈ K
this : Nonempty.{u_3 + 1} (↑K : Type u_3) := ⋯
eq : ‖u - v‖ = ⨅ (w : (↑K : Type u_3)), ‖u - (↑w : F)‖
w : F
hw : w ∈ K
δ : ℝ := ⨅ (w : (↑K : Type u_3)), ‖u - (↑w : F)‖
p : ℝ := ⟪u - v, w - v⟫_ℝ
q : ℝ := HPow.hPow (β := ℕ) ‖w - v‖ 2
δ_le : ∀ (w : (↑K : Type u_3)), δ ≤ ‖u - (↑w : F)‖
⊢ ∀ (w : F) (hw : w ∈ K), δ ≤ ‖u - w‖

Tactic:
have δ_le' (w) (hw : w ∈ K) : δ ≤ ‖u - w‖ := δ_le ⟨w, hw⟩
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Minimal
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
K : Set F
h : Convex ℝ K
u v : F
hv : v ∈ K
this : Nonempty.{u_3 + 1} (↑K : Type u_3) := ⋯
eq : ‖u - v‖ = ⨅ (w : (↑K : Type u_3)), ‖u - (↑w : F)‖
w : F
hw : w ∈ K
δ : ℝ := ⨅ (w : (↑K : Type u_3)), ‖u - (↑w : F)‖
p : ℝ := ⟪u - v, w - v⟫_ℝ
q : ℝ := HPow.hPow (β := ℕ) ‖w - v‖ 2
δ_le : ∀ (w : (↑K : Type u_3)), δ ≤ ‖u - (↑w : F)‖
δ_le' : ∀ (w : F) (hw : w ∈ K), δ ≤ ‖u - w‖
θ : ℝ
hθ₁ : 0 < θ
hθ₂ : θ ≤ 1
simp : ‖u - v‖ * ‖u - v‖ ≤ ‖u - (θ • w + (1 - θ) • v)‖ * ‖u - (θ • w + (1 - θ) • v)‖
⊢ HPow.hPow (β := ℕ) ‖u - v‖ 2 ≤ HPow.hPow (β := ℕ) ‖u - (θ • w + (1 - θ) • v)‖ 2

Tactic:
simp only [sq]

Premises used: sq
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Minimal
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
K : Set F
h : Convex ℝ K
u v : F
hv : v ∈ K
this : Nonempty.{u_3 + 1} (↑K : Type u_3) := ⋯
eq : ‖u - v‖ = ⨅ (w : (↑K : Type u_3)), ‖u - (↑w : F)‖
w : F
hw : w ∈ K
δ : ℝ := ⨅ (w : (↑K : Type u_3)), ‖u - (↑w : F)‖
p : ℝ := ⟪u - v, w - v⟫_ℝ
q : ℝ := HPow.hPow (β := ℕ) ‖w - v‖ 2
δ_le : ∀ (w : (↑K : Type u_3)), δ ≤ ‖u - (↑w : F)‖
δ_le' : ∀ (w : F) (hw : w ∈ K), δ ≤ ‖u - w‖
θ : ℝ
hθ₁ : 0 < θ
hθ₂ : θ ≤ 1
apply : ‖u - v‖ ≤ ‖u - (θ • w + (1 - θ) • v)‖
⊢ ‖u - v‖ * ‖u - v‖ ≤ ‖u - (θ • w + (1 - θ) • v)‖ * ‖u - (θ • w + (1 - θ) • v)‖

Tactic:
apply mul_self_le_mul_self (norm_nonneg _)

Premises used: mul_self_le_mul_self, norm_nonneg
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Minimal
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
K : Set F
h : Convex ℝ K
u v : F
hv : v ∈ K
this : Nonempty.{u_3 + 1} (↑K : Type u_3) := ⋯
eq : ‖u - v‖ = ⨅ (w : (↑K : Type u_3)), ‖u - (↑w : F)‖
w : F
hw : w ∈ K
δ : ℝ := ⨅ (w : (↑K : Type u_3)), ‖u - (↑w : F)‖
p : ℝ := ⟪u - v, w - v⟫_ℝ
q : ℝ := HPow.hPow (β := ℕ) ‖w - v‖ 2
δ_le : ∀ (w : (↑K : Type u_3)), δ ≤ ‖u - (↑w : F)‖
δ_le' : ∀ (w : F) (hw : w ∈ K), δ ≤ ‖u - w‖
θ : ℝ
hθ₁ : 0 < θ
hθ₂ : θ ≤ 1
rw : ⨅ (w : (↑K : Type u_3)), ‖u - (↑w : F)‖ ≤ ‖u - (θ • w + (1 - θ) • v)‖
⊢ ‖u - v‖ ≤ ‖u - (θ • w + (1 - θ) • v)‖

Tactic:
rw [eq]
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Minimal
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
K : Set F
h : Convex ℝ K
u v : F
hv : v ∈ K
this : Nonempty.{u_3 + 1} (↑K : Type u_3) := ⋯
eq : ‖u - v‖ = ⨅ (w : (↑K : Type u_3)), ‖u - (↑w : F)‖
w : F
hw : w ∈ K
δ : ℝ := ⨅ (w : (↑K : Type u_3)), ‖u - (↑w : F)‖
p : ℝ := ⟪u - v, w - v⟫_ℝ
q : ℝ := HPow.hPow (β := ℕ) ‖w - v‖ 2
δ_le : ∀ (w : (↑K : Type u_3)), δ ≤ ‖u - (↑w : F)‖
δ_le' : ∀ (w : F) (hw : w ∈ K), δ ≤ ‖u - w‖
θ : ℝ
hθ₁ : 0 < θ
hθ₂ : θ ≤ 1
hw₁ : θ • w + (1 - θ) • v ∈ K
⊢ ⨅ (w : (↑K : Type u_3)), ‖u - (↑w : F)‖ ≤ ‖u - (θ • w + (1 - θ) • v)‖

Tactic:
apply δ_le'
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Minimal
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
K : Set F
h : Convex ℝ K
u v : F
hv : v ∈ K
this : Nonempty.{u_3 + 1} (↑K : Type u_3) := ⋯
eq : ‖u - v‖ = ⨅ (w : (↑K : Type u_3)), ‖u - (↑w : F)‖
w : F
hw : w ∈ K
δ : ℝ := ⨅ (w : (↑K : Type u_3)), ‖u - (↑w : F)‖
p : ℝ := ⟪u - v, w - v⟫_ℝ
q : ℝ := HPow.hPow (β := ℕ) ‖w - v‖ 2
δ_le : ∀ (w : (↑K : Type u_3)), δ ≤ ‖u - (↑w : F)‖
δ_le' : ∀ (w : F) (hw : w ∈ K), δ ≤ ‖u - w‖
θ : ℝ
hθ₁ : 0 < θ
hθ₂ : θ ≤ 1
hw₁ : 0 ≤ θ
hw₂ : 0 ≤ 1 - θ
hw₃ : θ + (1 - θ) = 1
⊢ θ • w + (1 - θ) • v ∈ K

Tactic:
apply h hw hv
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Minimal
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
K : Set F
h : Convex ℝ K
u v : F
hv : v ∈ K
this : Nonempty.{u_3 + 1} (↑K : Type u_3) := ⋯
eq : ‖u - v‖ = ⨅ (w : (↑K : Type u_3)), ‖u - (↑w : F)‖
w : F
hw : w ∈ K
δ : ℝ := ⨅ (w : (↑K : Type u_3)), ‖u - (↑w : F)‖
p : ℝ := ⟪u - v, w - v⟫_ℝ
q : ℝ := HPow.hPow (β := ℕ) ‖w - v‖ 2
δ_le : ∀ (w : (↑K : Type u_3)), δ ≤ ‖u - (↑w : F)‖
δ_le' : ∀ (w : F) (hw : w ∈ K), δ ≤ ‖u - w‖
θ : ℝ
hθ₁ : 0 < θ
hθ₂ : θ ≤ 1
⊢ 0 ≤ θ

Tactic:
le_of_lt hθ₁

Premises used: le_of_lt
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Minimal
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
K : Set F
h : Convex ℝ K
u v : F
hv : v ∈ K
this : Nonempty.{u_3 + 1} (↑K : Type u_3) := ⋯
eq : ‖u - v‖ = ⨅ (w : (↑K : Type u_3)), ‖u - (↑w : F)‖
w : F
hw : w ∈ K
δ : ℝ := ⨅ (w : (↑K : Type u_3)), ‖u - (↑w : F)‖
p : ℝ := ⟪u - v, w - v⟫_ℝ
q : ℝ := HPow.hPow (β := ℕ) ‖w - v‖ 2
δ_le : ∀ (w : (↑K : Type u_3)), δ ≤ ‖u - (↑w : F)‖
δ_le' : ∀ (w : F) (hw : w ∈ K), δ ≤ ‖u - w‖
θ : ℝ
hθ₁ : 0 < θ
hθ₂ : θ ≤ 1
⊢ 0 ≤ 1 - θ

Tactic:
sub_nonneg.2 hθ₂

Premises used: Iff.mpr, sub_nonneg
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Minimal
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
K : Set F
h : Convex ℝ K
u v : F
hv : v ∈ K
this : Nonempty.{u_3 + 1} (↑K : Type u_3) := ⋯
eq : ‖u - v‖ = ⨅ (w : (↑K : Type u_3)), ‖u - (↑w : F)‖
w : F
hw : w ∈ K
δ : ℝ := ⨅ (w : (↑K : Type u_3)), ‖u - (↑w : F)‖
p : ℝ := ⟪u - v, w - v⟫_ℝ
q : ℝ := HPow.hPow (β := ℕ) ‖w - v‖ 2
δ_le : ∀ (w : (↑K : Type u_3)), δ ≤ ‖u - (↑w : F)‖
δ_le' : ∀ (w : F) (hw : w ∈ K), δ ≤ ‖u - w‖
θ : ℝ
hθ₁ : 0 < θ
hθ₂ : θ ≤ 1
⊢ θ + (1 - θ) = 1

Tactic:
add_sub_cancel _ _

Premises used: add_sub_cancel
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Minimal
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
K : Set F
h : Convex ℝ K
u v : F
hv : v ∈ K
this : Nonempty.{u_3 + 1} (↑K : Type u_3) := ⋯
eq : ‖u - v‖ = ⨅ (w : (↑K : Type u_3)), ‖u - (↑w : F)‖
w : F
hw : w ∈ K
δ : ℝ := ⨅ (w : (↑K : Type u_3)), ‖u - (↑w : F)‖
p : ℝ := ⟪u - v, w - v⟫_ℝ
q : ℝ := HPow.hPow (β := ℕ) ‖w - v‖ 2
δ_le : ∀ (w : (↑K : Type u_3)), δ ≤ ‖u - (↑w : F)‖
δ_le' : ∀ (w : F) (hw : w ∈ K), δ ≤ ‖u - w‖
θ : ℝ
hθ₁ : 0 < θ
hθ₂ : θ ≤ 1
⊢ 0 ≤ θ

Tactic:
exacts [le_of_lt hθ₁, sub_nonneg.2 hθ₂, add_sub_cancel _ _]

Premises used: Iff.mpr, le_of_lt, add_sub_cancel, sub_nonneg
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Minimal
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
K : Set F
h : Convex ℝ K
u v : F
hv : v ∈ K
this : Nonempty.{u_3 + 1} (↑K : Type u_3) := ⋯
eq : ‖u - v‖ = ⨅ (w : (↑K : Type u_3)), ‖u - (↑w : F)‖
w : F
hw : w ∈ K
δ : ℝ := ⨅ (w : (↑K : Type u_3)), ‖u - (↑w : F)‖
p : ℝ := ⟪u - v, w - v⟫_ℝ
q : ℝ := HPow.hPow (β := ℕ) ‖w - v‖ 2
δ_le : ∀ (w : (↑K : Type u_3)), δ ≤ ‖u - (↑w : F)‖
δ_le' : ∀ (w : F) (hw : w ∈ K), δ ≤ ‖u - w‖
θ : ℝ
hθ₁ : 0 < θ
hθ₂ : θ ≤ 1
rw : u - (θ • w + (v - θ • v)) = u - v - (θ • w - θ • v)
⊢ u - (θ • w + (1 - θ) • v) = u - v - θ • (w - v)

Tactic:
rw [smul_sub, sub_smul, one_smul]

Premises used: sub_smul, one_smul, smul_sub
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Minimal
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
K : Set F
h : Convex ℝ K
u v : F
hv : v ∈ K
this : Nonempty.{u_3 + 1} (↑K : Type u_3) := ⋯
eq : ‖u - v‖ = ⨅ (w : (↑K : Type u_3)), ‖u - (↑w : F)‖
w : F
hw : w ∈ K
δ : ℝ := ⨅ (w : (↑K : Type u_3)), ‖u - (↑w : F)‖
p : ℝ := ⟪u - v, w - v⟫_ℝ
q : ℝ := HPow.hPow (β := ℕ) ‖w - v‖ 2
δ_le : ∀ (w : (↑K : Type u_3)), δ ≤ ‖u - (↑w : F)‖
δ_le' : ∀ (w : F) (hw : w ∈ K), δ ≤ ‖u - w‖
θ : ℝ
hθ₁ : 0 < θ
hθ₂ : θ ≤ 1
⊢ u - (θ • w + (v - θ • v)) = u - v - (θ • w - θ • v)

Tactic:
simp only [sub_eq_add_neg, add_comm, add_left_comm, add_assoc, neg_add_rev]

Premises used: neg_add_rev, add_left_comm, add_assoc, sub_eq_add_neg, add_comm
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Minimal
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
K : Set F
h : Convex ℝ K
u v : F
hv : v ∈ K
this : Nonempty.{u_3 + 1} (↑K : Type u_3) := ⋯
eq : ‖u - v‖ = ⨅ (w : (↑K : Type u_3)), ‖u - (↑w : F)‖
w : F
hw : w ∈ K
δ : ℝ := ⨅ (w : (↑K : Type u_3)), ‖u - (↑w : F)‖
p : ℝ := ⟪u - v, w - v⟫_ℝ
q : ℝ := HPow.hPow (β := ℕ) ‖w - v‖ 2
δ_le : ∀ (w : (↑K : Type u_3)), δ ≤ ‖u - (↑w : F)‖
δ_le' : ∀ (w : F) (hw : w ∈ K), δ ≤ ‖u - w‖
θ : ℝ
hθ₁ : 0 < θ
hθ₂ : θ ≤ 1
⊢ u - (θ • w + (1 - θ) • v) = u - v - θ • (w - v)

Tactic:
have : u - (θ • w + (1 - θ) • v) = u - v - θ • (w - v) := by
              rw [smul_sub, sub_smul, one_smul]
              simp only [sub_eq_add_neg, add_comm, add_left_comm, add_assoc, neg_add_rev]
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Minimal
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
K : Set F
h : Convex ℝ K
u v : F
hv : v ∈ K
this_1 : Nonempty.{u_3 + 1} (↑K : Type u_3) := ⋯
eq : ‖u - v‖ = ⨅ (w : (↑K : Type u_3)), ‖u - (↑w : F)‖
w : F
hw : w ∈ K
δ : ℝ := ⨅ (w : (↑K : Type u_3)), ‖u - (↑w : F)‖
p : ℝ := ⟪u - v, w - v⟫_ℝ
q : ℝ := HPow.hPow (β := ℕ) ‖w - v‖ 2
δ_le : ∀ (w : (↑K : Type u_3)), δ ≤ ‖u - (↑w : F)‖
δ_le' : ∀ (w : F) (hw : w ∈ K), δ ≤ ‖u - w‖
θ : ℝ
hθ₁ : 0 < θ
hθ₂ : θ ≤ 1
this : u - (θ • w + (1 - θ) • v) = u - v - θ • (w - v)
rw rw₁ : HPow.hPow (β := ℕ) ‖u - v - θ • (w - v)‖ 2 = HPow.hPow (β := ℕ) ‖u - v - θ • (w - v)‖ 2
⊢ HPow.hPow (β := ℕ) ‖u - (θ • w + (1 - θ) • v)‖ 2 = HPow.hPow (β := ℕ) ‖u - v - θ • (w - v)‖ 2

Tactic:
rw [this]
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Minimal
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
K : Set F
h : Convex ℝ K
u v : F
hv : v ∈ K
this : Nonempty.{u_3 + 1} (↑K : Type u_3) := ⋯
eq : ‖u - v‖ = ⨅ (w : (↑K : Type u_3)), ‖u - (↑w : F)‖
w : F
hw : w ∈ K
δ : ℝ := ⨅ (w : (↑K : Type u_3)), ‖u - (↑w : F)‖
p : ℝ := ⟪u - v, w - v⟫_ℝ
q : ℝ := HPow.hPow (β := ℕ) ‖w - v‖ 2
δ_le : ∀ (w : (↑K : Type u_3)), δ ≤ ‖u - (↑w : F)‖
δ_le' : ∀ (w : F) (hw : w ∈ K), δ ≤ ‖u - w‖
θ : ℝ
hθ₁ : 0 < θ
hθ₂ : θ ≤ 1
rw :
  HPow.hPow (β := ℕ) ‖u - v‖ 2 - HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((re : (a : ℝ) → ℝ) (θ * ⟪u - v, w - v⟫_ℝ) : ℝ) +
      HPow.hPow (β := ℕ) (‖θ‖ * ‖w - v‖) 2 =
    HPow.hPow (β := ℕ) ‖u - v‖ 2 - 2 * θ * ⟪u - v, w - v⟫_ℝ + θ * θ * HPow.hPow (β := ℕ) ‖w - v‖ 2
⊢ HPow.hPow (β := ℕ) ‖u - v - θ • (w - v)‖ 2 =
    HPow.hPow (β := ℕ) ‖u - v‖ 2 - 2 * θ * ⟪u - v, w - v⟫_ℝ + θ * θ * HPow.hPow (β := ℕ) ‖w - v‖ 2

Tactic:
rw [@norm_sub_sq ℝ, inner_smul_right, norm_smul]

Premises used: norm_smul, norm_sub_sq, inner_smul_right