𝕜 : Type ?u.190458
E : Type ?u.190461
F : Type u_1
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Set F
h : Convex ℝ K
u v : F
hv : v ∈ K
this : Nonempty ↑K := Nonempty.intro { val := v, property := hv }
⊢ (‖u - v‖ = ⨅ (w : ↑K), ‖u - ↑w‖) ↔ ∀ (w : F), w ∈ K → inner (u - v) (w - v) ≤ 0
𝕜 : Type ?u.190458
E : Type ?u.190461
F : Type u_1
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Set F
h : Convex ℝ K
u v : F
hv : v ∈ K
⊢ (‖u - v‖ = ⨅ (w : ↑K), ‖u - ↑w‖) ↔ ∀ (w : F), w ∈ K → inner (u - v) (w - v) ≤ 0
letI : Nonempty K := ⟨⟨v, hv⟩⟩
case mp
𝕜 : Type ?u.190458
E : Type ?u.190461
F : Type u_1
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Set F
h : Convex ℝ K
u v : F
hv : v ∈ K
this : Nonempty ↑K := Nonempty.intro { val := v, property := hv }
⊢ (‖u - v‖ = ⨅ (w : ↑K), ‖u - ↑w‖) → ∀ (w : F), w ∈ K → inner (u - v) (w - v) ≤ 0

case mpr
𝕜 : Type ?u.190458
E : Type ?u.190461
F : Type u_1
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Set F
h : Convex ℝ K
u v : F
hv : v ∈ K
this : Nonempty ↑K := Nonempty.intro { val := v, property := hv }
⊢ (∀ (w : F), w ∈ K → inner (u - v) (w - v) ≤ 0) → ‖u - v‖ = ⨅ (w : ↑K), ‖u - ↑w‖
𝕜 : Type ?u.190458
E : Type ?u.190461
F : Type u_1
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Set F
h : Convex ℝ K
u v : F
hv : v ∈ K
this : Nonempty ↑K := Nonempty.intro { val := v, property := hv }
⊢ (‖u - v‖ = ⨅ (w : ↑K), ‖u - ↑w‖) ↔ ∀ (w : F), w ∈ K → inner (u - v) (w - v) ≤ 0
constructor
case mp
𝕜 : Type ?u.190458
E : Type ?u.190461
F : Type u_1
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Set F
h : Convex ℝ K
u v : F
hv : v ∈ K
this : Nonempty ↑K := Nonempty.intro { val := v, property := hv }
eq : ‖u - v‖ = ⨅ (w : ↑K), ‖u - ↑w‖
w : F
hw : w ∈ K
⊢ inner (u - v) (w - v) ≤ 0
case mp
𝕜 : Type ?u.190458
E : Type ?u.190461
F : Type u_1
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Set F
h : Convex ℝ K
u v : F
hv : v ∈ K
this : Nonempty ↑K := Nonempty.intro { val := v, property := hv }
⊢ (‖u - v‖ = ⨅ (w : ↑K), ‖u - ↑w‖) → ∀ (w : F), w ∈ K → inner (u - v) (w - v) ≤ 0
intro eq w hw
case mp
𝕜 : Type ?u.190458
E : Type ?u.190461
F : Type u_1
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Set F
h : Convex ℝ K
u v : F
hv : v ∈ K
this : Nonempty ↑K := Nonempty.intro { val := v, property := hv }
eq : ‖u - v‖ = ⨅ (w : ↑K), ‖u - ↑w‖
w : F
hw : w ∈ K
δ : ℝ := ⨅ (w : ↑K), ‖u - ↑w‖
⊢ inner (u - v) (w - v) ≤ 0
case mp
𝕜 : Type ?u.190458
E : Type ?u.190461
F : Type u_1
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Set F
h : Convex ℝ K
u v : F
hv : v ∈ K
this : Nonempty ↑K := Nonempty.intro { val := v, property := hv }
eq : ‖u - v‖ = ⨅ (w : ↑K), ‖u - ↑w‖
w : F
hw : w ∈ K
⊢ inner (u - v) (w - v) ≤ 0
let δ := ⨅ w : K, ‖u - w‖
case mp
𝕜 : Type ?u.190458
E : Type ?u.190461
F : Type u_1
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Set F
h : Convex ℝ K
u v : F
hv : v ∈ K
this : Nonempty ↑K := Nonempty.intro { val := v, property := hv }
eq : ‖u - v‖ = ⨅ (w : ↑K), ‖u - ↑w‖
w : F
hw : w ∈ K
δ : ℝ := ⨅ (w : ↑K), ‖u - ↑w‖
p : ℝ := inner (u - v) (w - v)
⊢ inner (u - v) (w - v) ≤ 0
case mp
𝕜 : Type ?u.190458
E : Type ?u.190461
F : Type u_1
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Set F
h : Convex ℝ K
u v : F
hv : v ∈ K
this : Nonempty ↑K := Nonempty.intro { val := v, property := hv }
eq : ‖u - v‖ = ⨅ (w : ↑K), ‖u - ↑w‖
w : F
hw : w ∈ K
δ : ℝ := ⨅ (w : ↑K), ‖u - ↑w‖
⊢ inner (u - v) (w - v) ≤ 0
let p := ⟪u - v, w - v⟫_ℝ
case mp
𝕜 : Type ?u.190458
E : Type ?u.190461
F : Type u_1
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Set F
h : Convex ℝ K
u v : F
hv : v ∈ K
this : Nonempty ↑K := Nonempty.intro { val := v, property := hv }
eq : ‖u - v‖ = ⨅ (w : ↑K), ‖u - ↑w‖
w : F
hw : w ∈ K
δ : ℝ := ⨅ (w : ↑K), ‖u - ↑w‖
p : ℝ := inner (u - v) (w - v)
q : ℝ := ‖w - v‖ ^ 2
⊢ inner (u - v) (w - v) ≤ 0
case mp
𝕜 : Type ?u.190458
E : Type ?u.190461
F : Type u_1
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Set F
h : Convex ℝ K
u v : F
hv : v ∈ K
this : Nonempty ↑K := Nonempty.intro { val := v, property := hv }
eq : ‖u - v‖ = ⨅ (w : ↑K), ‖u - ↑w‖
w : F
hw : w ∈ K
δ : ℝ := ⨅ (w : ↑K), ‖u - ↑w‖
p : ℝ := inner (u - v) (w - v)
⊢ inner (u - v) (w - v) ≤ 0
let q := ‖w - v‖ ^ 2
case mp
𝕜 : Type ?u.190458
E : Type ?u.190461
F : Type u_1
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Set F
h : Convex ℝ K
u v : F
hv : v ∈ K
this : Nonempty ↑K := Nonempty.intro { val := v, property := hv }
eq : ‖u - v‖ = ⨅ (w : ↑K), ‖u - ↑w‖
w : F
hw : w ∈ K
δ : ℝ := ⨅ (w : ↑K), ‖u - ↑w‖
p : ℝ := inner (u - v) (w - v)
q : ℝ := ‖w - v‖ ^ 2
δ_le : ∀ (w : ↑K), δ ≤ ‖u - ↑w‖
⊢ inner (u - v) (w - v) ≤ 0
case mp
𝕜 : Type ?u.190458
E : Type ?u.190461
F : Type u_1
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Set F
h : Convex ℝ K
u v : F
hv : v ∈ K
this : Nonempty ↑K := Nonempty.intro { val := v, property := hv }
eq : ‖u - v‖ = ⨅ (w : ↑K), ‖u - ↑w‖
w : F
hw : w ∈ K
δ : ℝ := ⨅ (w : ↑K), ‖u - ↑w‖
p : ℝ := inner (u - v) (w - v)
q : ℝ := ‖w - v‖ ^ 2
⊢ inner (u - v) (w - v) ≤ 0
have δ_le (w : K) : δ ≤ ‖u - w‖ := ciInf_le ⟨0, fun _ ⟨_, h⟩ => h ▸ norm_nonneg _⟩ _
case mp
𝕜 : Type ?u.190458
E : Type ?u.190461
F : Type u_1
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Set F
h : Convex ℝ K
u v : F
hv : v ∈ K
this : Nonempty ↑K := Nonempty.intro { val := v, property := hv }
eq : ‖u - v‖ = ⨅ (w : ↑K), ‖u - ↑w‖
w : F
hw : w ∈ K
δ : ℝ := ⨅ (w : ↑K), ‖u - ↑w‖
p : ℝ := inner (u - v) (w - v)
q : ℝ := ‖w - v‖ ^ 2
δ_le : ∀ (w : ↑K), δ ≤ ‖u - ↑w‖
δ_le' : ∀ (w : F), w ∈ K → δ ≤ ‖u - w‖
⊢ inner (u - v) (w - v) ≤ 0
case mp
𝕜 : Type ?u.190458
E : Type ?u.190461
F : Type u_1
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Set F
h : Convex ℝ K
u v : F
hv : v ∈ K
this : Nonempty ↑K := Nonempty.intro { val := v, property := hv }
eq : ‖u - v‖ = ⨅ (w : ↑K), ‖u - ↑w‖
w : F
hw : w ∈ K
δ : ℝ := ⨅ (w : ↑K), ‖u - ↑w‖
p : ℝ := inner (u - v) (w - v)
q : ℝ := ‖w - v‖ ^ 2
δ_le : ∀ (w : ↑K), δ ≤ ‖u - ↑w‖
⊢ inner (u - v) (w - v) ≤ 0
have δ_le' (w) (hw : w ∈ K) : δ ≤ ‖u - w‖ := δ_le ⟨w, hw⟩
case mp
𝕜 : Type ?u.190458
E : Type ?u.190461
F : Type u_1
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Set F
h : Convex ℝ K
u v : F
hv : v ∈ K
this✝ : Nonempty ↑K := Nonempty.intro { val := v, property := hv }
eq : ‖u - v‖ = ⨅ (w : ↑K), ‖u - ↑w‖
w : F
hw : w ∈ K
δ : ℝ := ⨅ (w : ↑K), ‖u - ↑w‖
p : ℝ := inner (u - v) (w - v)
q : ℝ := ‖w - v‖ ^ 2
δ_le : ∀ (w : ↑K), δ ≤ ‖u - ↑w‖
δ_le' : ∀ (w : F), w ∈ K → δ ≤ ‖u - w‖
this : ∀ (θ : ℝ), 0 < θ → θ ≤ 1 → 2 * p ≤ θ * q
⊢ inner (u - v) (w - v) ≤ 0
case mp
𝕜 : Type ?u.190458
E : Type ?u.190461
F : Type u_1
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Set F
h : Convex ℝ K
u v : F
hv : v ∈ K
this : Nonempty ↑K := Nonempty.intro { val := v, property := hv }
eq : ‖u - v‖ = ⨅ (w : ↑K), ‖u - ↑w‖
w : F
hw : w ∈ K
δ : ℝ := ⨅ (w : ↑K), ‖u - ↑w‖
p : ℝ := inner (u - v) (w - v)
q : ℝ := ‖w - v‖ ^ 2
δ_le : ∀ (w : ↑K), δ ≤ ‖u - ↑w‖
δ_le' : ∀ (w : F), w ∈ K → δ ≤ ‖u - w‖
⊢ inner (u - v) (w - v) ≤ 0
have (θ : ℝ) (hθ₁ : 0 < θ) (hθ₂ : θ ≤ 1) : 2 * p ≤ θ * q := by
  have : ‖u - v‖ ^ 2 ≤ ‖u - v‖ ^ 2 - 2 * θ * ⟪u - v, w - v⟫_ℝ + θ * θ * ‖w - v‖ ^ 2 :=
    calc ‖u - v‖ ^ 2
      _ ≤ ‖u - (θ • w + (1 - θ) • v)‖ ^ 2 := by
        simp only [sq]; apply mul_self_le_mul_self (norm_nonneg _)
        rw [eq]; apply δ_le'
        apply h hw hv
        exacts [le_of_lt hθ₁, sub_nonneg.2 hθ₂, add_sub_cancel'_right _ _]
      _ = ‖u - v - θ • (w - v)‖ ^ 2 := by
        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]
        rw [this]
      _ = ‖u - v‖ ^ 2 - 2 * θ * inner (u - v) (w - v) + θ * θ * ‖w - v‖ ^ 2 := by
        rw [@norm_sub_sq ℝ, inner_smul_right, norm_smul]
        simp only [sq]
        show
          ‖u - v‖ * ‖u - v‖ - 2 * (θ * inner (u - v) (w - v)) +
            absR θ * ‖w - v‖ * (absR θ * ‖w - v‖) =
          ‖u - v‖ * ‖u - v‖ - 2 * θ * inner (u - v) (w - v) + θ * θ * (‖w - v‖ * ‖w - v‖)
        rw [abs_of_pos hθ₁]; ring
  have eq₁ :
    ‖u - v‖ ^ 2 - 2 * θ * inner (u - v) (w - v) + θ * θ * ‖w - v‖ ^ 2 =
      ‖u - v‖ ^ 2 + (θ * θ * ‖w - v‖ ^ 2 - 2 * θ * inner (u - v) (w - v)) := by
    abel
  rw [eq₁, le_add_iff_nonneg_right] at this
  have eq₂ :
    θ * θ * ‖w - v‖ ^ 2 - 2 * θ * inner (u - v) (w - v) =
      θ * (θ * ‖w - v‖ ^ 2 - 2 * inner (u - v) (w - v))
  ring
  rw [eq₂] at this
  have := le_of_sub_nonneg (nonneg_of_mul_nonneg_right this hθ₁)
  exact this
case pos
𝕜 : Type ?u.190458
E : Type ?u.190461
F : Type u_1
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Set F
h : Convex ℝ K
u v : F
hv : v ∈ K
this✝ : Nonempty ↑K := Nonempty.intro { val := v, property := hv }
eq : ‖u - v‖ = ⨅ (w : ↑K), ‖u - ↑w‖
w : F
hw : w ∈ K
δ : ℝ := ⨅ (w : ↑K), ‖u - ↑w‖
p : ℝ := inner (u - v) (w - v)
q : ℝ := ‖w - v‖ ^ 2
δ_le : ∀ (w : ↑K), δ ≤ ‖u - ↑w‖
δ_le' : ∀ (w : F), w ∈ K → δ ≤ ‖u - w‖
this : ∀ (θ : ℝ), 0 < θ → θ ≤ 1 → 2 * p ≤ θ * q
hq : q = 0
⊢ inner (u - v) (w - v) ≤ 0

case neg
𝕜 : Type ?u.190458
E : Type ?u.190461
F : Type u_1
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Set F
h : Convex ℝ K
u v : F
hv : v ∈ K
this✝ : Nonempty ↑K := Nonempty.intro { val := v, property := hv }
eq : ‖u - v‖ = ⨅ (w : ↑K), ‖u - ↑w‖
w : F
hw : w ∈ K
δ : ℝ := ⨅ (w : ↑K), ‖u - ↑w‖
p : ℝ := inner (u - v) (w - v)
q : ℝ := ‖w - v‖ ^ 2
δ_le : ∀ (w : ↑K), δ ≤ ‖u - ↑w‖
δ_le' : ∀ (w : F), w ∈ K → δ ≤ ‖u - w‖
this : ∀ (θ : ℝ), 0 < θ → θ ≤ 1 → 2 * p ≤ θ * q
hq : ¬q = 0
⊢ inner (u - v) (w - v) ≤ 0
case mp
𝕜 : Type ?u.190458
E : Type ?u.190461
F : Type u_1
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Set F
h : Convex ℝ K
u v : F
hv : v ∈ K
this✝ : Nonempty ↑K := Nonempty.intro { val := v, property := hv }
eq : ‖u - v‖ = ⨅ (w : ↑K), ‖u - ↑w‖
w : F
hw : w ∈ K
δ : ℝ := ⨅ (w : ↑K), ‖u - ↑w‖
p : ℝ := inner (u - v) (w - v)
q : ℝ := ‖w - v‖ ^ 2
δ_le : ∀ (w : ↑K), δ ≤ ‖u - ↑w‖
δ_le' : ∀ (w : F), w ∈ K → δ ≤ ‖u - w‖
this : ∀ (θ : ℝ), 0 < θ → θ ≤ 1 → 2 * p ≤ θ * q
⊢ inner (u - v) (w - v) ≤ 0
by_cases hq : q = 0
𝕜 : Type ?u.190458
E : Type ?u.190461
F : Type u_1
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Set F
h : Convex ℝ K
u v : F
hv : v ∈ K
this✝ : Nonempty ↑K := Nonempty.intro { val := v, property := hv }
eq : ‖u - v‖ = ⨅ (w : ↑K), ‖u - ↑w‖
w : F
hw : w ∈ K
δ : ℝ := ⨅ (w : ↑K), ‖u - ↑w‖
p : ℝ := inner (u - v) (w - v)
q : ℝ := ‖w - v‖ ^ 2
δ_le : ∀ (w : ↑K), δ ≤ ‖u - ↑w‖
δ_le' : ∀ (w : F), w ∈ K → δ ≤ ‖u - w‖
θ : ℝ
hθ₁ : 0 < θ
hθ₂ : θ ≤ 1
this : ‖u - v‖ ^ 2 ≤ ‖u - v‖ ^ 2 - 2 * θ * inner (u - v) (w - v) + θ * θ * ‖w - v‖ ^ 2
⊢ 2 * p ≤ θ * q
𝕜 : Type ?u.190458
E : Type ?u.190461
F : Type u_1
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Set F
h : Convex ℝ K
u v : F
hv : v ∈ K
this : Nonempty ↑K := Nonempty.intro { val := v, property := hv }
eq : ‖u - v‖ = ⨅ (w : ↑K), ‖u - ↑w‖
w : F
hw : w ∈ K
δ : ℝ := ⨅ (w : ↑K), ‖u - ↑w‖
p : ℝ := inner (u - v) (w - v)
q : ℝ := ‖w - v‖ ^ 2
δ_le : ∀ (w : ↑K), δ ≤ ‖u - ↑w‖
δ_le' : ∀ (w : F), w ∈ K → δ ≤ ‖u - w‖
θ : ℝ
hθ₁ : 0 < θ
hθ₂ : θ ≤ 1
⊢ 2 * p ≤ θ * q
have : ‖u - v‖ ^ 2 ≤ ‖u - v‖ ^ 2 - 2 * θ * ⟪u - v, w - v⟫_ℝ + θ * θ * ‖w - v‖ ^ 2 :=
  calc ‖u - v‖ ^ 2
    _ ≤ ‖u - (θ • w + (1 - θ) • v)‖ ^ 2 := by
      simp only [sq]; apply mul_self_le_mul_self (norm_nonneg _)
      rw [eq]; apply δ_le'
      apply h hw hv
      exacts [le_of_lt hθ₁, sub_nonneg.2 hθ₂, add_sub_cancel'_right _ _]
    _ = ‖u - v - θ • (w - v)‖ ^ 2 := by
      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]
      rw [this]
    _ = ‖u - v‖ ^ 2 - 2 * θ * inner (u - v) (w - v) + θ * θ * ‖w - v‖ ^ 2 := by
      rw [@norm_sub_sq ℝ, inner_smul_right, norm_smul]
      simp only [sq]
      show
        ‖u - v‖ * ‖u - v‖ - 2 * (θ * inner (u - v) (w - v)) +
          absR θ * ‖w - v‖ * (absR θ * ‖w - v‖) =
        ‖u - v‖ * ‖u - v‖ - 2 * θ * inner (u - v) (w - v) + θ * θ * (‖w - v‖ * ‖w - v‖)
      rw [abs_of_pos hθ₁]; ring
𝕜 : Type ?u.190458
E : Type ?u.190461
F : Type u_1
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Set F
h : Convex ℝ K
u v : F
hv : v ∈ K
this✝ : Nonempty ↑K := Nonempty.intro { val := v, property := hv }
eq : ‖u - v‖ = ⨅ (w : ↑K), ‖u - ↑w‖
w : F
hw : w ∈ K
δ : ℝ := ⨅ (w : ↑K), ‖u - ↑w‖
p : ℝ := inner (u - v) (w - v)
q : ℝ := ‖w - v‖ ^ 2
δ_le : ∀ (w : ↑K), δ ≤ ‖u - ↑w‖
δ_le' : ∀ (w : F), w ∈ K → δ ≤ ‖u - w‖
θ : ℝ
hθ₁ : 0 < θ
hθ₂ : θ ≤ 1
this : ‖u - v‖ ^ 2 ≤ ‖u - v‖ ^ 2 - 2 * θ * inner (u - v) (w - v) + θ * θ * ‖w - v‖ ^ 2
eq₁ :
  ‖u - v‖ ^ 2 - 2 * θ * inner (u - v) (w - v) + θ * θ * ‖w - v‖ ^ 2 =
    ‖u - v‖ ^ 2 + (θ * θ * ‖w - v‖ ^ 2 - 2 * θ * inner (u - v) (w - v))
⊢ 2 * p ≤ θ * q
𝕜 : Type ?u.190458
E : Type ?u.190461
F : Type u_1
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Set F
h : Convex ℝ K
u v : F
hv : v ∈ K
this✝ : Nonempty ↑K := Nonempty.intro { val := v, property := hv }
eq : ‖u - v‖ = ⨅ (w : ↑K), ‖u - ↑w‖
w : F
hw : w ∈ K
δ : ℝ := ⨅ (w : ↑K), ‖u - ↑w‖
p : ℝ := inner (u - v) (w - v)
q : ℝ := ‖w - v‖ ^ 2
δ_le : ∀ (w : ↑K), δ ≤ ‖u - ↑w‖
δ_le' : ∀ (w : F), w ∈ K → δ ≤ ‖u - w‖
θ : ℝ
hθ₁ : 0 < θ
hθ₂ : θ ≤ 1
this : ‖u - v‖ ^ 2 ≤ ‖u - v‖ ^ 2 - 2 * θ * inner (u - v) (w - v) + θ * θ * ‖w - v‖ ^ 2
⊢ 2 * p ≤ θ * q
have eq₁ :
  ‖u - v‖ ^ 2 - 2 * θ * inner (u - v) (w - v) + θ * θ * ‖w - v‖ ^ 2 =
    ‖u - v‖ ^ 2 + (θ * θ * ‖w - v‖ ^ 2 - 2 * θ * inner (u - v) (w - v)) := by
  abel
𝕜 : Type ?u.190458
E : Type ?u.190461
F : Type u_1
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Set F
h : Convex ℝ K
u v : F
hv : v ∈ K
this✝ : Nonempty ↑K := Nonempty.intro { val := v, property := hv }
eq : ‖u - v‖ = ⨅ (w : ↑K), ‖u - ↑w‖
w : F
hw : w ∈ K
δ : ℝ := ⨅ (w : ↑K), ‖u - ↑w‖
p : ℝ := inner (u - v) (w - v)
q : ℝ := ‖w - v‖ ^ 2
δ_le : ∀ (w : ↑K), δ ≤ ‖u - ↑w‖
δ_le' : ∀ (w : F), w ∈ K → δ ≤ ‖u - w‖
θ : ℝ
hθ₁ : 0 < θ
hθ₂ : θ ≤ 1
this : 0 ≤ θ * θ * ‖w - v‖ ^ 2 - 2 * θ * inner (u - v) (w - v)
eq₁ :
  ‖u - v‖ ^ 2 - 2 * θ * inner (u - v) (w - v) + θ * θ * ‖w - v‖ ^ 2 =
    ‖u - v‖ ^ 2 + (θ * θ * ‖w - v‖ ^ 2 - 2 * θ * inner (u - v) (w - v))
⊢ 2 * p ≤ θ * q
𝕜 : Type ?u.190458
E : Type ?u.190461
F : Type u_1
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Set F
h : Convex ℝ K
u v : F
hv : v ∈ K
this✝ : Nonempty ↑K := Nonempty.intro { val := v, property := hv }
eq : ‖u - v‖ = ⨅ (w : ↑K), ‖u - ↑w‖
w : F
hw : w ∈ K
δ : ℝ := ⨅ (w : ↑K), ‖u - ↑w‖
p : ℝ := inner (u - v) (w - v)
q : ℝ := ‖w - v‖ ^ 2
δ_le : ∀ (w : ↑K), δ ≤ ‖u - ↑w‖
δ_le' : ∀ (w : F), w ∈ K → δ ≤ ‖u - w‖
θ : ℝ
hθ₁ : 0 < θ
hθ₂ : θ ≤ 1
this : ‖u - v‖ ^ 2 ≤ ‖u - v‖ ^ 2 - 2 * θ * inner (u - v) (w - v) + θ * θ * ‖w - v‖ ^ 2
eq₁ :
  ‖u - v‖ ^ 2 - 2 * θ * inner (u - v) (w - v) + θ * θ * ‖w - v‖ ^ 2 =
    ‖u - v‖ ^ 2 + (θ * θ * ‖w - v‖ ^ 2 - 2 * θ * inner (u - v) (w - v))
⊢ 2 * p ≤ θ * q
rw [eq₁, le_add_iff_nonneg_right] at this
case eq₂
𝕜 : Type ?u.190458
E : Type ?u.190461
F : Type u_1
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Set F
h : Convex ℝ K
u v : F
hv : v ∈ K
this✝ : Nonempty ↑K := Nonempty.intro { val := v, property := hv }
eq : ‖u - v‖ = ⨅ (w : ↑K), ‖u - ↑w‖
w : F
hw : w ∈ K
δ : ℝ := ⨅ (w : ↑K), ‖u - ↑w‖
p : ℝ := inner (u - v) (w - v)
q : ℝ := ‖w - v‖ ^ 2
δ_le : ∀ (w : ↑K), δ ≤ ‖u - ↑w‖
δ_le' : ∀ (w : F), w ∈ K → δ ≤ ‖u - w‖
θ : ℝ
hθ₁ : 0 < θ
hθ₂ : θ ≤ 1
this : 0 ≤ θ * θ * ‖w - v‖ ^ 2 - 2 * θ * inner (u - v) (w - v)
eq₁ :
  ‖u - v‖ ^ 2 - 2 * θ * inner (u - v) (w - v) + θ * θ * ‖w - v‖ ^ 2 =
    ‖u - v‖ ^ 2 + (θ * θ * ‖w - v‖ ^ 2 - 2 * θ * inner (u - v) (w - v))
⊢ θ * θ * ‖w - v‖ ^ 2 - 2 * θ * inner (u - v) (w - v) = θ * (θ * ‖w - v‖ ^ 2 - 2 * inner (u - v) (w - v))

𝕜 : Type ?u.190458
E : Type ?u.190461
F : Type u_1
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Set F
h : Convex ℝ K
u v : F
hv : v ∈ K
this✝ : Nonempty ↑K := Nonempty.intro { val := v, property := hv }
eq : ‖u - v‖ = ⨅ (w : ↑K), ‖u - ↑w‖
w : F
hw : w ∈ K
δ : ℝ := ⨅ (w : ↑K), ‖u - ↑w‖
p : ℝ := inner (u - v) (w - v)
q : ℝ := ‖w - v‖ ^ 2
δ_le : ∀ (w : ↑K), δ ≤ ‖u - ↑w‖
δ_le' : ∀ (w : F), w ∈ K → δ ≤ ‖u - w‖
θ : ℝ
hθ₁ : 0 < θ
hθ₂ : θ ≤ 1
this : 0 ≤ θ * θ * ‖w - v‖ ^ 2 - 2 * θ * inner (u - v) (w - v)
eq₁ :
  ‖u - v‖ ^ 2 - 2 * θ * inner (u - v) (w - v) + θ * θ * ‖w - v‖ ^ 2 =
    ‖u - v‖ ^ 2 + (θ * θ * ‖w - v‖ ^ 2 - 2 * θ * inner (u - v) (w - v))
eq₂ : θ * θ * ‖w - v‖ ^ 2 - 2 * θ * inner (u - v) (w - v) = θ * (θ * ‖w - v‖ ^ 2 - 2 * inner (u - v) (w - v))
⊢ 2 * p ≤ θ * q
𝕜 : Type ?u.190458
E : Type ?u.190461
F : Type u_1
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Set F
h : Convex ℝ K
u v : F
hv : v ∈ K
this✝ : Nonempty ↑K := Nonempty.intro { val := v, property := hv }
eq : ‖u - v‖ = ⨅ (w : ↑K), ‖u - ↑w‖
w : F
hw : w ∈ K
δ : ℝ := ⨅ (w : ↑K), ‖u - ↑w‖
p : ℝ := inner (u - v) (w - v)
q : ℝ := ‖w - v‖ ^ 2
δ_le : ∀ (w : ↑K), δ ≤ ‖u - ↑w‖
δ_le' : ∀ (w : F), w ∈ K → δ ≤ ‖u - w‖
θ : ℝ
hθ₁ : 0 < θ
hθ₂ : θ ≤ 1
this : 0 ≤ θ * θ * ‖w - v‖ ^ 2 - 2 * θ * inner (u - v) (w - v)
eq₁ :
  ‖u - v‖ ^ 2 - 2 * θ * inner (u - v) (w - v) + θ * θ * ‖w - v‖ ^ 2 =
    ‖u - v‖ ^ 2 + (θ * θ * ‖w - v‖ ^ 2 - 2 * θ * inner (u - v) (w - v))
⊢ 2 * p ≤ θ * q
have eq₂ :
  θ * θ * ‖w - v‖ ^ 2 - 2 * θ * inner (u - v) (w - v) =
    θ * (θ * ‖w - v‖ ^ 2 - 2 * inner (u - v) (w - v))
𝕜 : Type ?u.190458
E : Type ?u.190461
F : Type u_1
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Set F
h : Convex ℝ K
u v : F
hv : v ∈ K
this✝ : Nonempty ↑K := Nonempty.intro { val := v, property := hv }
eq : ‖u - v‖ = ⨅ (w : ↑K), ‖u - ↑w‖
w : F
hw : w ∈ K
δ : ℝ := ⨅ (w : ↑K), ‖u - ↑w‖
p : ℝ := inner (u - v) (w - v)
q : ℝ := ‖w - v‖ ^ 2
δ_le : ∀ (w : ↑K), δ ≤ ‖u - ↑w‖
δ_le' : ∀ (w : F), w ∈ K → δ ≤ ‖u - w‖
θ : ℝ
hθ₁ : 0 < θ
hθ₂ : θ ≤ 1
this : 0 ≤ θ * θ * ‖w - v‖ ^ 2 - 2 * θ * inner (u - v) (w - v)
eq₁ :
  ‖u - v‖ ^ 2 - 2 * θ * inner (u - v) (w - v) + θ * θ * ‖w - v‖ ^ 2 =
    ‖u - v‖ ^ 2 + (θ * θ * ‖w - v‖ ^ 2 - 2 * θ * inner (u - v) (w - v))
eq₂ : θ * θ * ‖w - v‖ ^ 2 - 2 * θ * inner (u - v) (w - v) = θ * (θ * ‖w - v‖ ^ 2 - 2 * inner (u - v) (w - v))
⊢ 2 * p ≤ θ * q
case eq₂
𝕜 : Type ?u.190458
E : Type ?u.190461
F : Type u_1
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Set F
h : Convex ℝ K
u v : F
hv : v ∈ K
this✝ : Nonempty ↑K := Nonempty.intro { val := v, property := hv }
eq : ‖u - v‖ = ⨅ (w : ↑K), ‖u - ↑w‖
w : F
hw : w ∈ K
δ : ℝ := ⨅ (w : ↑K), ‖u - ↑w‖
p : ℝ := inner (u - v) (w - v)
q : ℝ := ‖w - v‖ ^ 2
δ_le : ∀ (w : ↑K), δ ≤ ‖u - ↑w‖
δ_le' : ∀ (w : F), w ∈ K → δ ≤ ‖u - w‖
θ : ℝ
hθ₁ : 0 < θ
hθ₂ : θ ≤ 1
this : 0 ≤ θ * θ * ‖w - v‖ ^ 2 - 2 * θ * inner (u - v) (w - v)
eq₁ :
  ‖u - v‖ ^ 2 - 2 * θ * inner (u - v) (w - v) + θ * θ * ‖w - v‖ ^ 2 =
    ‖u - v‖ ^ 2 + (θ * θ * ‖w - v‖ ^ 2 - 2 * θ * inner (u - v) (w - v))
⊢ θ * θ * ‖w - v‖ ^ 2 - 2 * θ * inner (u - v) (w - v) = θ * (θ * ‖w - v‖ ^ 2 - 2 * inner (u - v) (w - v))

𝕜 : Type ?u.190458
E : Type ?u.190461
F : Type u_1
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Set F
h : Convex ℝ K
u v : F
hv : v ∈ K
this✝ : Nonempty ↑K := Nonempty.intro { val := v, property := hv }
eq : ‖u - v‖ = ⨅ (w : ↑K), ‖u - ↑w‖
w : F
hw : w ∈ K
δ : ℝ := ⨅ (w : ↑K), ‖u - ↑w‖
p : ℝ := inner (u - v) (w - v)
q : ℝ := ‖w - v‖ ^ 2
δ_le : ∀ (w : ↑K), δ ≤ ‖u - ↑w‖
δ_le' : ∀ (w : F), w ∈ K → δ ≤ ‖u - w‖
θ : ℝ
hθ₁ : 0 < θ
hθ₂ : θ ≤ 1
this : 0 ≤ θ * θ * ‖w - v‖ ^ 2 - 2 * θ * inner (u - v) (w - v)
eq₁ :
  ‖u - v‖ ^ 2 - 2 * θ * inner (u - v) (w - v) + θ * θ * ‖w - v‖ ^ 2 =
    ‖u - v‖ ^ 2 + (θ * θ * ‖w - v‖ ^ 2 - 2 * θ * inner (u - v) (w - v))
eq₂ : θ * θ * ‖w - v‖ ^ 2 - 2 * θ * inner (u - v) (w - v) = θ * (θ * ‖w - v‖ ^ 2 - 2 * inner (u - v) (w - v))
⊢ 2 * p ≤ θ * q
ring
𝕜 : Type ?u.190458
E : Type ?u.190461
F : Type u_1
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Set F
h : Convex ℝ K
u v : F
hv : v ∈ K
this✝ : Nonempty ↑K := Nonempty.intro { val := v, property := hv }
eq : ‖u - v‖ = ⨅ (w : ↑K), ‖u - ↑w‖
w : F
hw : w ∈ K
δ : ℝ := ⨅ (w : ↑K), ‖u - ↑w‖
p : ℝ := inner (u - v) (w - v)
q : ℝ := ‖w - v‖ ^ 2
δ_le : ∀ (w : ↑K), δ ≤ ‖u - ↑w‖
δ_le' : ∀ (w : F), w ∈ K → δ ≤ ‖u - w‖
θ : ℝ
hθ₁ : 0 < θ
hθ₂ : θ ≤ 1
this : 0 ≤ θ * (θ * ‖w - v‖ ^ 2 - 2 * inner (u - v) (w - v))
eq₁ :
  ‖u - v‖ ^ 2 - 2 * θ * inner (u - v) (w - v) + θ * θ * ‖w - v‖ ^ 2 =
    ‖u - v‖ ^ 2 + (θ * θ * ‖w - v‖ ^ 2 - 2 * θ * inner (u - v) (w - v))
eq₂ : θ * θ * ‖w - v‖ ^ 2 - 2 * θ * inner (u - v) (w - v) = θ * (θ * ‖w - v‖ ^ 2 - 2 * inner (u - v) (w - v))
⊢ 2 * p ≤ θ * q
𝕜 : Type ?u.190458
E : Type ?u.190461
F : Type u_1
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Set F
h : Convex ℝ K
u v : F
hv : v ∈ K
this✝ : Nonempty ↑K := Nonempty.intro { val := v, property := hv }
eq : ‖u - v‖ = ⨅ (w : ↑K), ‖u - ↑w‖
w : F
hw : w ∈ K
δ : ℝ := ⨅ (w : ↑K), ‖u - ↑w‖
p : ℝ := inner (u - v) (w - v)
q : ℝ := ‖w - v‖ ^ 2
δ_le : ∀ (w : ↑K), δ ≤ ‖u - ↑w‖
δ_le' : ∀ (w : F), w ∈ K → δ ≤ ‖u - w‖
θ : ℝ
hθ₁ : 0 < θ
hθ₂ : θ ≤ 1
this : 0 ≤ θ * θ * ‖w - v‖ ^ 2 - 2 * θ * inner (u - v) (w - v)
eq₁ :
  ‖u - v‖ ^ 2 - 2 * θ * inner (u - v) (w - v) + θ * θ * ‖w - v‖ ^ 2 =
    ‖u - v‖ ^ 2 + (θ * θ * ‖w - v‖ ^ 2 - 2 * θ * inner (u - v) (w - v))
eq₂ : θ * θ * ‖w - v‖ ^ 2 - 2 * θ * inner (u - v) (w - v) = θ * (θ * ‖w - v‖ ^ 2 - 2 * inner (u - v) (w - v))
⊢ 2 * p ≤ θ * q
rw [eq₂] at this
𝕜 : Type ?u.190458
E : Type ?u.190461
F : Type u_1
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Set F
h : Convex ℝ K
u v : F
hv : v ∈ K
this✝¹ : Nonempty ↑K := Nonempty.intro { val := v, property := hv }
eq : ‖u - v‖ = ⨅ (w : ↑K), ‖u - ↑w‖
w : F
hw : w ∈ K
δ : ℝ := ⨅ (w : ↑K), ‖u - ↑w‖
p : ℝ := inner (u - v) (w - v)
q : ℝ := ‖w - v‖ ^ 2
δ_le : ∀ (w : ↑K), δ ≤ ‖u - ↑w‖
δ_le' : ∀ (w : F), w ∈ K → δ ≤ ‖u - w‖
θ : ℝ
hθ₁ : 0 < θ
hθ₂ : θ ≤ 1
this✝ : 0 ≤ θ * (θ * ‖w - v‖ ^ 2 - 2 * inner (u - v) (w - v))
eq₁ :
  ‖u - v‖ ^ 2 - 2 * θ * inner (u - v) (w - v) + θ * θ * ‖w - v‖ ^ 2 =
    ‖u - v‖ ^ 2 + (θ * θ * ‖w - v‖ ^ 2 - 2 * θ * inner (u - v) (w - v))
eq₂ : θ * θ * ‖w - v‖ ^ 2 - 2 * θ * inner (u - v) (w - v) = θ * (θ * ‖w - v‖ ^ 2 - 2 * inner (u - v) (w - v))
this : 2 * inner (u - v) (w - v) ≤ θ * ‖w - v‖ ^ 2
⊢ 2 * p ≤ θ * q
𝕜 : Type ?u.190458
E : Type ?u.190461
F : Type u_1
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Set F
h : Convex ℝ K
u v : F
hv : v ∈ K
this✝ : Nonempty ↑K := Nonempty.intro { val := v, property := hv }
eq : ‖u - v‖ = ⨅ (w : ↑K), ‖u - ↑w‖
w : F
hw : w ∈ K
δ : ℝ := ⨅ (w : ↑K), ‖u - ↑w‖
p : ℝ := inner (u - v) (w - v)
q : ℝ := ‖w - v‖ ^ 2
δ_le : ∀ (w : ↑K), δ ≤ ‖u - ↑w‖
δ_le' : ∀ (w : F), w ∈ K → δ ≤ ‖u - w‖
θ : ℝ
hθ₁ : 0 < θ
hθ₂ : θ ≤ 1
this : 0 ≤ θ * (θ * ‖w - v‖ ^ 2 - 2 * inner (u - v) (w - v))
eq₁ :
  ‖u - v‖ ^ 2 - 2 * θ * inner (u - v) (w - v) + θ * θ * ‖w - v‖ ^ 2 =
    ‖u - v‖ ^ 2 + (θ * θ * ‖w - v‖ ^ 2 - 2 * θ * inner (u - v) (w - v))
eq₂ : θ * θ * ‖w - v‖ ^ 2 - 2 * θ * inner (u - v) (w - v) = θ * (θ * ‖w - v‖ ^ 2 - 2 * inner (u - v) (w - v))
⊢ 2 * p ≤ θ * q
have := le_of_sub_nonneg (nonneg_of_mul_nonneg_right this hθ₁)
no goals
𝕜 : Type ?u.190458
E : Type ?u.190461
F : Type u_1
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Set F
h : Convex ℝ K
u v : F
hv : v ∈ K
this✝¹ : Nonempty ↑K := Nonempty.intro { val := v, property := hv }
eq : ‖u - v‖ = ⨅ (w : ↑K), ‖u - ↑w‖
w : F
hw : w ∈ K
δ : ℝ := ⨅ (w : ↑K), ‖u - ↑w‖
p : ℝ := inner (u - v) (w - v)
q : ℝ := ‖w - v‖ ^ 2
δ_le : ∀ (w : ↑K), δ ≤ ‖u - ↑w‖
δ_le' : ∀ (w : F), w ∈ K → δ ≤ ‖u - w‖
θ : ℝ
hθ₁ : 0 < θ
hθ₂ : θ ≤ 1
this✝ : 0 ≤ θ * (θ * ‖w - v‖ ^ 2 - 2 * inner (u - v) (w - v))
eq₁ :
  ‖u - v‖ ^ 2 - 2 * θ * inner (u - v) (w - v) + θ * θ * ‖w - v‖ ^ 2 =
    ‖u - v‖ ^ 2 + (θ * θ * ‖w - v‖ ^ 2 - 2 * θ * inner (u - v) (w - v))
eq₂ : θ * θ * ‖w - v‖ ^ 2 - 2 * θ * inner (u - v) (w - v) = θ * (θ * ‖w - v‖ ^ 2 - 2 * inner (u - v) (w - v))
this : 2 * inner (u - v) (w - v) ≤ θ * ‖w - v‖ ^ 2
⊢ 2 * p ≤ θ * q
exact this
𝕜 : Type ?u.190458
E : Type ?u.190461
F : Type u_1
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Set F
h : Convex ℝ K
u v : F
hv : v ∈ K
this : Nonempty ↑K := Nonempty.intro { val := v, property := hv }
eq : ‖u - v‖ = ⨅ (w : ↑K), ‖u - ↑w‖
w : F
hw : w ∈ K
δ : ℝ := ⨅ (w : ↑K), ‖u - ↑w‖
p : ℝ := inner (u - v) (w - v)
q : ℝ := ‖w - v‖ ^ 2
δ_le : ∀ (w : ↑K), δ ≤ ‖u - ↑w‖
δ_le' : ∀ (w : F), w ∈ K → δ ≤ ‖u - w‖
θ : ℝ
hθ₁ : 0 < θ
hθ₂ : θ ≤ 1
⊢ ‖u - v‖ * ‖u - v‖ ≤ ‖u - (θ • w + (1 - θ) • v)‖ * ‖u - (θ • w + (1 - θ) • v)‖
𝕜 : Type ?u.190458
E : Type ?u.190461
F : Type u_1
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Set F
h : Convex ℝ K
u v : F
hv : v ∈ K
this : Nonempty ↑K := Nonempty.intro { val := v, property := hv }
eq : ‖u - v‖ = ⨅ (w : ↑K), ‖u - ↑w‖
w : F
hw : w ∈ K
δ : ℝ := ⨅ (w : ↑K), ‖u - ↑w‖
p : ℝ := inner (u - v) (w - v)
q : ℝ := ‖w - v‖ ^ 2
δ_le : ∀ (w : ↑K), δ ≤ ‖u - ↑w‖
δ_le' : ∀ (w : F), w ∈ K → δ ≤ ‖u - w‖
θ : ℝ
hθ₁ : 0 < θ
hθ₂ : θ ≤ 1
⊢ ‖u - v‖ ^ 2 ≤ ‖u - (θ • w + (1 - θ) • v)‖ ^ 2
simp only [sq]
𝕜 : Type ?u.190458
E : Type ?u.190461
F : Type u_1
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Set F
h : Convex ℝ K
u v : F
hv : v ∈ K
this : Nonempty ↑K := Nonempty.intro { val := v, property := hv }
eq : ‖u - v‖ = ⨅ (w : ↑K), ‖u - ↑w‖
w : F
hw : w ∈ K
δ : ℝ := ⨅ (w : ↑K), ‖u - ↑w‖
p : ℝ := inner (u - v) (w - v)
q : ℝ := ‖w - v‖ ^ 2
δ_le : ∀ (w : ↑K), δ ≤ ‖u - ↑w‖
δ_le' : ∀ (w : F), w ∈ K → δ ≤ ‖u - w‖
θ : ℝ
hθ₁ : 0 < θ
hθ₂ : θ ≤ 1
⊢ ‖u - v‖ ≤ ‖u - (θ • w + (1 - θ) • v)‖
𝕜 : Type ?u.190458
E : Type ?u.190461
F : Type u_1
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Set F
h : Convex ℝ K
u v : F
hv : v ∈ K
this : Nonempty ↑K := Nonempty.intro { val := v, property := hv }
eq : ‖u - v‖ = ⨅ (w : ↑K), ‖u - ↑w‖
w : F
hw : w ∈ K
δ : ℝ := ⨅ (w : ↑K), ‖u - ↑w‖
p : ℝ := inner (u - v) (w - v)
q : ℝ := ‖w - v‖ ^ 2
δ_le : ∀ (w : ↑K), δ ≤ ‖u - ↑w‖
δ_le' : ∀ (w : F), w ∈ K → δ ≤ ‖u - w‖
θ : ℝ
hθ₁ : 0 < θ
hθ₂ : θ ≤ 1
⊢ ‖u - v‖ * ‖u - v‖ ≤ ‖u - (θ • w + (1 - θ) • v)‖ * ‖u - (θ • w + (1 - θ) • v)‖
apply mul_self_le_mul_self (norm_nonneg _)
𝕜 : Type ?u.190458
E : Type ?u.190461
F : Type u_1
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Set F
h : Convex ℝ K
u v : F
hv : v ∈ K
this : Nonempty ↑K := Nonempty.intro { val := v, property := hv }
eq : ‖u - v‖ = ⨅ (w : ↑K), ‖u - ↑w‖
w : F
hw : w ∈ K
δ : ℝ := ⨅ (w : ↑K), ‖u - ↑w‖
p : ℝ := inner (u - v) (w - v)
q : ℝ := ‖w - v‖ ^ 2
δ_le : ∀ (w : ↑K), δ ≤ ‖u - ↑w‖
δ_le' : ∀ (w : F), w ∈ K → δ ≤ ‖u - w‖
θ : ℝ
hθ₁ : 0 < θ
hθ₂ : θ ≤ 1
⊢ (⨅ (w : ↑K), ‖u - ↑w‖) ≤ ‖u - (θ • w + (1 - θ) • v)‖
𝕜 : Type ?u.190458
E : Type ?u.190461
F : Type u_1
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Set F
h : Convex ℝ K
u v : F
hv : v ∈ K
this : Nonempty ↑K := Nonempty.intro { val := v, property := hv }
eq : ‖u - v‖ = ⨅ (w : ↑K), ‖u - ↑w‖
w : F
hw : w ∈ K
δ : ℝ := ⨅ (w : ↑K), ‖u - ↑w‖
p : ℝ := inner (u - v) (w - v)
q : ℝ := ‖w - v‖ ^ 2
δ_le : ∀ (w : ↑K), δ ≤ ‖u - ↑w‖
δ_le' : ∀ (w : F), w ∈ K → δ ≤ ‖u - w‖
θ : ℝ
hθ₁ : 0 < θ
hθ₂ : θ ≤ 1
⊢ ‖u - v‖ ≤ ‖u - (θ • w + (1 - θ) • v)‖
rw [eq]
case hw
𝕜 : Type ?u.190458
E : Type ?u.190461
F : Type u_1
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Set F
h : Convex ℝ K
u v : F
hv : v ∈ K
this : Nonempty ↑K := Nonempty.intro { val := v, property := hv }
eq : ‖u - v‖ = ⨅ (w : ↑K), ‖u - ↑w‖
w : F
hw : w ∈ K
δ : ℝ := ⨅ (w : ↑K), ‖u - ↑w‖
p : ℝ := inner (u - v) (w - v)
q : ℝ := ‖w - v‖ ^ 2
δ_le : ∀ (w : ↑K), δ ≤ ‖u - ↑w‖
δ_le' : ∀ (w : F), w ∈ K → δ ≤ ‖u - w‖
θ : ℝ
hθ₁ : 0 < θ
hθ₂ : θ ≤ 1
⊢ θ • w + (1 - θ) • v ∈ K
𝕜 : Type ?u.190458
E : Type ?u.190461
F : Type u_1
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Set F
h : Convex ℝ K
u v : F
hv : v ∈ K
this : Nonempty ↑K := Nonempty.intro { val := v, property := hv }
eq : ‖u - v‖ = ⨅ (w : ↑K), ‖u - ↑w‖
w : F
hw : w ∈ K
δ : ℝ := ⨅ (w : ↑K), ‖u - ↑w‖
p : ℝ := inner (u - v) (w - v)
q : ℝ := ‖w - v‖ ^ 2
δ_le : ∀ (w : ↑K), δ ≤ ‖u - ↑w‖
δ_le' : ∀ (w : F), w ∈ K → δ ≤ ‖u - w‖
θ : ℝ
hθ₁ : 0 < θ
hθ₂ : θ ≤ 1
⊢ (⨅ (w : ↑K), ‖u - ↑w‖) ≤ ‖u - (θ • w + (1 - θ) • v)‖
apply δ_le'
case hw.a
𝕜 : Type ?u.190458
E : Type ?u.190461
F : Type u_1
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Set F
h : Convex ℝ K
u v : F
hv : v ∈ K
this : Nonempty ↑K := Nonempty.intro { val := v, property := hv }
eq : ‖u - v‖ = ⨅ (w : ↑K), ‖u - ↑w‖
w : F
hw : w ∈ K
δ : ℝ := ⨅ (w : ↑K), ‖u - ↑w‖
p : ℝ := inner (u - v) (w - v)
q : ℝ := ‖w - v‖ ^ 2
δ_le : ∀ (w : ↑K), δ ≤ ‖u - ↑w‖
δ_le' : ∀ (w : F), w ∈ K → δ ≤ ‖u - w‖
θ : ℝ
hθ₁ : 0 < θ
hθ₂ : θ ≤ 1
⊢ 0 ≤ θ

case hw.a
𝕜 : Type ?u.190458
E : Type ?u.190461
F : Type u_1
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Set F
h : Convex ℝ K
u v : F
hv : v ∈ K
this : Nonempty ↑K := Nonempty.intro { val := v, property := hv }
eq : ‖u - v‖ = ⨅ (w : ↑K), ‖u - ↑w‖
w : F
hw : w ∈ K
δ : ℝ := ⨅ (w : ↑K), ‖u - ↑w‖
p : ℝ := inner (u - v) (w - v)
q : ℝ := ‖w - v‖ ^ 2
δ_le : ∀ (w : ↑K), δ ≤ ‖u - ↑w‖
δ_le' : ∀ (w : F), w ∈ K → δ ≤ ‖u - w‖
θ : ℝ
hθ₁ : 0 < θ
hθ₂ : θ ≤ 1
⊢ 0 ≤ 1 - θ

case hw.a
𝕜 : Type ?u.190458
E : Type ?u.190461
F : Type u_1
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Set F
h : Convex ℝ K
u v : F
hv : v ∈ K
this : Nonempty ↑K := Nonempty.intro { val := v, property := hv }
eq : ‖u - v‖ = ⨅ (w : ↑K), ‖u - ↑w‖
w : F
hw : w ∈ K
δ : ℝ := ⨅ (w : ↑K), ‖u - ↑w‖
p : ℝ := inner (u - v) (w - v)
q : ℝ := ‖w - v‖ ^ 2
δ_le : ∀ (w : ↑K), δ ≤ ‖u - ↑w‖
δ_le' : ∀ (w : F), w ∈ K → δ ≤ ‖u - w‖
θ : ℝ
hθ₁ : 0 < θ
hθ₂ : θ ≤ 1
⊢ θ + (1 - θ) = 1
case hw
𝕜 : Type ?u.190458
E : Type ?u.190461
F : Type u_1
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Set F
h : Convex ℝ K
u v : F
hv : v ∈ K
this : Nonempty ↑K := Nonempty.intro { val := v, property := hv }
eq : ‖u - v‖ = ⨅ (w : ↑K), ‖u - ↑w‖
w : F
hw : w ∈ K
δ : ℝ := ⨅ (w : ↑K), ‖u - ↑w‖
p : ℝ := inner (u - v) (w - v)
q : ℝ := ‖w - v‖ ^ 2
δ_le : ∀ (w : ↑K), δ ≤ ‖u - ↑w‖
δ_le' : ∀ (w : F), w ∈ K → δ ≤ ‖u - w‖
θ : ℝ
hθ₁ : 0 < θ
hθ₂ : θ ≤ 1
⊢ θ • w + (1 - θ) • v ∈ K
apply h hw hv
no goals
case hw.a
𝕜 : Type ?u.190458
E : Type ?u.190461
F : Type u_1
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Set F
h : Convex ℝ K
u v : F
hv : v ∈ K
this : Nonempty ↑K := Nonempty.intro { val := v, property := hv }
eq : ‖u - v‖ = ⨅ (w : ↑K), ‖u - ↑w‖
w : F
hw : w ∈ K
δ : ℝ := ⨅ (w : ↑K), ‖u - ↑w‖
p : ℝ := inner (u - v) (w - v)
q : ℝ := ‖w - v‖ ^ 2
δ_le : ∀ (w : ↑K), δ ≤ ‖u - ↑w‖
δ_le' : ∀ (w : F), w ∈ K → δ ≤ ‖u - w‖
θ : ℝ
hθ₁ : 0 < θ
hθ₂ : θ ≤ 1
⊢ 0 ≤ θ

case hw.a
𝕜 : Type ?u.190458
E : Type ?u.190461
F : Type u_1
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Set F
h : Convex ℝ K
u v : F
hv : v ∈ K
this : Nonempty ↑K := Nonempty.intro { val := v, property := hv }
eq : ‖u - v‖ = ⨅ (w : ↑K), ‖u - ↑w‖
w : F
hw : w ∈ K
δ : ℝ := ⨅ (w : ↑K), ‖u - ↑w‖
p : ℝ := inner (u - v) (w - v)
q : ℝ := ‖w - v‖ ^ 2
δ_le : ∀ (w : ↑K), δ ≤ ‖u - ↑w‖
δ_le' : ∀ (w : F), w ∈ K → δ ≤ ‖u - w‖
θ : ℝ
hθ₁ : 0 < θ
hθ₂ : θ ≤ 1
⊢ 0 ≤ 1 - θ

case hw.a
𝕜 : Type ?u.190458
E : Type ?u.190461
F : Type u_1
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Set F
h : Convex ℝ K
u v : F
hv : v ∈ K
this : Nonempty ↑K := Nonempty.intro { val := v, property := hv }
eq : ‖u - v‖ = ⨅ (w : ↑K), ‖u - ↑w‖
w : F
hw : w ∈ K
δ : ℝ := ⨅ (w : ↑K), ‖u - ↑w‖
p : ℝ := inner (u - v) (w - v)
q : ℝ := ‖w - v‖ ^ 2
δ_le : ∀ (w : ↑K), δ ≤ ‖u - ↑w‖
δ_le' : ∀ (w : F), w ∈ K → δ ≤ ‖u - w‖
θ : ℝ
hθ₁ : 0 < θ
hθ₂ : θ ≤ 1
⊢ θ + (1 - θ) = 1
exacts [le_of_lt hθ₁, sub_nonneg.2 hθ₂, add_sub_cancel'_right _ _]
𝕜 : Type ?u.190458
E : Type ?u.190461
F : Type u_1
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Set F
h : Convex ℝ K
u v : F
hv : v ∈ K
this✝ : Nonempty ↑K := Nonempty.intro { val := v, property := hv }
eq : ‖u - v‖ = ⨅ (w : ↑K), ‖u - ↑w‖
w : F
hw : w ∈ K
δ : ℝ := ⨅ (w : ↑K), ‖u - ↑w‖
p : ℝ := inner (u - v) (w - v)
q : ℝ := ‖w - v‖ ^ 2
δ_le : ∀ (w : ↑K), δ ≤ ‖u - ↑w‖
δ_le' : ∀ (w : F), w ∈ K → δ ≤ ‖u - w‖
θ : ℝ
hθ₁ : 0 < θ
hθ₂ : θ ≤ 1
this : u - (θ • w + (1 - θ) • v) = u - v - θ • (w - v)
⊢ ‖u - (θ • w + (1 - θ) • v)‖ ^ 2 = ‖u - v - θ • (w - v)‖ ^ 2
𝕜 : Type ?u.190458
E : Type ?u.190461
F : Type u_1
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Set F
h : Convex ℝ K
u v : F
hv : v ∈ K
this : Nonempty ↑K := Nonempty.intro { val := v, property := hv }
eq : ‖u - v‖ = ⨅ (w : ↑K), ‖u - ↑w‖
w : F
hw : w ∈ K
δ : ℝ := ⨅ (w : ↑K), ‖u - ↑w‖
p : ℝ := inner (u - v) (w - v)
q : ℝ := ‖w - v‖ ^ 2
δ_le : ∀ (w : ↑K), δ ≤ ‖u - ↑w‖
δ_le' : ∀ (w : F), w ∈ K → δ ≤ ‖u - w‖
θ : ℝ
hθ₁ : 0 < θ
hθ₂ : θ ≤ 1
⊢ ‖u - (θ • w + (1 - θ) • v)‖ ^ 2 = ‖u - v - θ • (w - v)‖ ^ 2
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]
no goals
𝕜 : Type ?u.190458
E : Type ?u.190461
F : Type u_1
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Set F
h : Convex ℝ K
u v : F
hv : v ∈ K
this✝ : Nonempty ↑K := Nonempty.intro { val := v, property := hv }
eq : ‖u - v‖ = ⨅ (w : ↑K), ‖u - ↑w‖
w : F
hw : w ∈ K
δ : ℝ := ⨅ (w : ↑K), ‖u - ↑w‖
p : ℝ := inner (u - v) (w - v)
q : ℝ := ‖w - v‖ ^ 2
δ_le : ∀ (w : ↑K), δ ≤ ‖u - ↑w‖
δ_le' : ∀ (w : F), w ∈ K → δ ≤ ‖u - w‖
θ : ℝ
hθ₁ : 0 < θ
hθ₂ : θ ≤ 1
this : u - (θ • w + (1 - θ) • v) = u - v - θ • (w - v)
⊢ ‖u - (θ • w + (1 - θ) • v)‖ ^ 2 = ‖u - v - θ • (w - v)‖ ^ 2
rw [this]
𝕜 : Type ?u.190458
E : Type ?u.190461
F : Type u_1
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Set F
h : Convex ℝ K
u v : F
hv : v ∈ K
this : Nonempty ↑K := Nonempty.intro { val := v, property := hv }
eq : ‖u - v‖ = ⨅ (w : ↑K), ‖u - ↑w‖
w : F
hw : w ∈ K
δ : ℝ := ⨅ (w : ↑K), ‖u - ↑w‖
p : ℝ := inner (u - v) (w - v)
q : ℝ := ‖w - v‖ ^ 2
δ_le : ∀ (w : ↑K), δ ≤ ‖u - ↑w‖
δ_le' : ∀ (w : F), w ∈ K → δ ≤ ‖u - w‖
θ : ℝ
hθ₁ : 0 < θ
hθ₂ : θ ≤ 1
⊢ u - (θ • w + (v - θ • v)) = u - v - (θ • w - θ • v)
𝕜 : Type ?u.190458
E : Type ?u.190461
F : Type u_1
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Set F
h : Convex ℝ K
u v : F
hv : v ∈ K
this : Nonempty ↑K := Nonempty.intro { val := v, property := hv }
eq : ‖u - v‖ = ⨅ (w : ↑K), ‖u - ↑w‖
w : F
hw : w ∈ K
δ : ℝ := ⨅ (w : ↑K), ‖u - ↑w‖
p : ℝ := inner (u - v) (w - v)
q : ℝ := ‖w - v‖ ^ 2
δ_le : ∀ (w : ↑K), δ ≤ ‖u - ↑w‖
δ_le' : ∀ (w : F), w ∈ K → δ ≤ ‖u - w‖
θ : ℝ
hθ₁ : 0 < θ
hθ₂ : θ ≤ 1
⊢ u - (θ • w + (1 - θ) • v) = u - v - θ • (w - v)
rw [smul_sub, sub_smul, one_smul]
no goals
𝕜 : Type ?u.190458
E : Type ?u.190461
F : Type u_1
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Set F
h : Convex ℝ K
u v : F
hv : v ∈ K
this : Nonempty ↑K := Nonempty.intro { val := v, property := hv }
eq : ‖u - v‖ = ⨅ (w : ↑K), ‖u - ↑w‖
w : F
hw : w ∈ K
δ : ℝ := ⨅ (w : ↑K), ‖u - ↑w‖
p : ℝ := inner (u - v) (w - v)
q : ℝ := ‖w - v‖ ^ 2
δ_le : ∀ (w : ↑K), δ ≤ ‖u - ↑w‖
δ_le' : ∀ (w : F), w ∈ K → δ ≤ ‖u - w‖
θ : ℝ
hθ₁ : 0 < θ
hθ₂ : θ ≤ 1
⊢ u - (θ • w + (v - θ • v)) = u - v - (θ • w - θ • v)
simp only [sub_eq_add_neg, add_comm, add_left_comm, add_assoc, neg_add_rev]
𝕜 : Type ?u.190458
E : Type ?u.190461
F : Type u_1
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Set F
h : Convex ℝ K
u v : F
hv : v ∈ K
this : Nonempty ↑K := Nonempty.intro { val := v, property := hv }
eq : ‖u - v‖ = ⨅ (w : ↑K), ‖u - ↑w‖
w : F
hw : w ∈ K
δ : ℝ := ⨅ (w : ↑K), ‖u - ↑w‖
p : ℝ := inner (u - v) (w - v)
q : ℝ := ‖w - v‖ ^ 2
δ_le : ∀ (w : ↑K), δ ≤ ‖u - ↑w‖
δ_le' : ∀ (w : F), w ∈ K → δ ≤ ‖u - w‖
θ : ℝ
hθ₁ : 0 < θ
hθ₂ : θ ≤ 1
⊢ ‖u - v‖ ^ 2 - 2 * ↑re (θ * inner (u - v) (w - v)) + (‖θ‖ * ‖w - v‖) ^ 2 =
    ‖u - v‖ ^ 2 - 2 * θ * inner (u - v) (w - v) + θ * θ * ‖w - v‖ ^ 2
𝕜 : Type ?u.190458
E : Type ?u.190461
F : Type u_1
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Set F
h : Convex ℝ K
u v : F
hv : v ∈ K
this : Nonempty ↑K := Nonempty.intro { val := v, property := hv }
eq : ‖u - v‖ = ⨅ (w : ↑K), ‖u - ↑w‖
w : F
hw : w ∈ K
δ : ℝ := ⨅ (w : ↑K), ‖u - ↑w‖
p : ℝ := inner (u - v) (w - v)
q : ℝ := ‖w - v‖ ^ 2
δ_le : ∀ (w : ↑K), δ ≤ ‖u - ↑w‖
δ_le' : ∀ (w : F), w ∈ K → δ ≤ ‖u - w‖
θ : ℝ
hθ₁ : 0 < θ
hθ₂ : θ ≤ 1
⊢ ‖u - v - θ • (w - v)‖ ^ 2 = ‖u - v‖ ^ 2 - 2 * θ * inner (u - v) (w - v) + θ * θ * ‖w - v‖ ^ 2
rw [@norm_sub_sq ℝ, inner_smul_right, norm_smul]
𝕜 : Type ?u.190458
E : Type ?u.190461
F : Type u_1
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Set F
h : Convex ℝ K
u v : F
hv : v ∈ K
this : Nonempty ↑K := Nonempty.intro { val := v, property := hv }
eq : ‖u - v‖ = ⨅ (w : ↑K), ‖u - ↑w‖
w : F
hw : w ∈ K
δ : ℝ := ⨅ (w : ↑K), ‖u - ↑w‖
p : ℝ := inner (u - v) (w - v)
q : ℝ := ‖w - v‖ ^ 2
δ_le : ∀ (w : ↑K), δ ≤ ‖u - ↑w‖
δ_le' : ∀ (w : F), w ∈ K → δ ≤ ‖u - w‖
θ : ℝ
hθ₁ : 0 < θ
hθ₂ : θ ≤ 1
⊢ ‖u - v‖ * ‖u - v‖ - 2 * ↑re (θ * inner (u - v) (w - v)) + ‖θ‖ * ‖w - v‖ * (‖θ‖ * ‖w - v‖) =
    ‖u - v‖ * ‖u - v‖ - 2 * θ * inner (u - v) (w - v) + θ * θ * (‖w - v‖ * ‖w - v‖)
𝕜 : Type ?u.190458
E : Type ?u.190461
F : Type u_1
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Set F
h : Convex ℝ K
u v : F
hv : v ∈ K
this : Nonempty ↑K := Nonempty.intro { val := v, property := hv }
eq : ‖u - v‖ = ⨅ (w : ↑K), ‖u - ↑w‖
w : F
hw : w ∈ K
δ : ℝ := ⨅ (w : ↑K), ‖u - ↑w‖
p : ℝ := inner (u - v) (w - v)
q : ℝ := ‖w - v‖ ^ 2
δ_le : ∀ (w : ↑K), δ ≤ ‖u - ↑w‖
δ_le' : ∀ (w : F), w ∈ K → δ ≤ ‖u - w‖
θ : ℝ
hθ₁ : 0 < θ
hθ₂ : θ ≤ 1
⊢ ‖u - v‖ ^ 2 - 2 * ↑re (θ * inner (u - v) (w - v)) + (‖θ‖ * ‖w - v‖) ^ 2 =
    ‖u - v‖ ^ 2 - 2 * θ * inner (u - v) (w - v) + θ * θ * ‖w - v‖ ^ 2
simp only [sq]
𝕜 : Type ?u.190458
E : Type ?u.190461
F : Type u_1
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Set F
h : Convex ℝ K
u v : F
hv : v ∈ K
this : Nonempty ↑K := Nonempty.intro { val := v, property := hv }
eq : ‖u - v‖ = ⨅ (w : ↑K), ‖u - ↑w‖
w : F
hw : w ∈ K
δ : ℝ := ⨅ (w : ↑K), ‖u - ↑w‖
p : ℝ := inner (u - v) (w - v)
q : ℝ := ‖w - v‖ ^ 2
δ_le : ∀ (w : ↑K), δ ≤ ‖u - ↑w‖
δ_le' : ∀ (w : F), w ∈ K → δ ≤ ‖u - w‖
θ : ℝ
hθ₁ : 0 < θ
hθ₂ : θ ≤ 1
⊢ ‖u - v‖ * ‖u - v‖ - 2 * (θ * inner (u - v) (w - v)) + absR θ * ‖w - v‖ * (absR θ * ‖w - v‖) =
    ‖u - v‖ * ‖u - v‖ - 2 * θ * inner (u - v) (w - v) + θ * θ * (‖w - v‖ * ‖w - v‖)
𝕜 : Type ?u.190458
E : Type ?u.190461
F : Type u_1
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Set F
h : Convex ℝ K
u v : F
hv : v ∈ K
this : Nonempty ↑K := Nonempty.intro { val := v, property := hv }
eq : ‖u - v‖ = ⨅ (w : ↑K), ‖u - ↑w‖
w : F
hw : w ∈ K
δ : ℝ := ⨅ (w : ↑K), ‖u - ↑w‖
p : ℝ := inner (u - v) (w - v)
q : ℝ := ‖w - v‖ ^ 2
δ_le : ∀ (w : ↑K), δ ≤ ‖u - ↑w‖
δ_le' : ∀ (w : F), w ∈ K → δ ≤ ‖u - w‖
θ : ℝ
hθ₁ : 0 < θ
hθ₂ : θ ≤ 1
⊢ ‖u - v‖ * ‖u - v‖ - 2 * ↑re (θ * inner (u - v) (w - v)) + ‖θ‖ * ‖w - v‖ * (‖θ‖ * ‖w - v‖) =
    ‖u - v‖ * ‖u - v‖ - 2 * θ * inner (u - v) (w - v) + θ * θ * (‖w - v‖ * ‖w - v‖)
show
  ‖u - v‖ * ‖u - v‖ - 2 * (θ * inner (u - v) (w - v)) +
    absR θ * ‖w - v‖ * (absR θ * ‖w - v‖) =
  ‖u - v‖ * ‖u - v‖ - 2 * θ * inner (u - v) (w - v) + θ * θ * (‖w - v‖ * ‖w - v‖)
𝕜 : Type ?u.190458
E : Type ?u.190461
F : Type u_1
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Set F
h : Convex ℝ K
u v : F
hv : v ∈ K
this : Nonempty ↑K := Nonempty.intro { val := v, property := hv }
eq : ‖u - v‖ = ⨅ (w : ↑K), ‖u - ↑w‖
w : F
hw : w ∈ K
δ : ℝ := ⨅ (w : ↑K), ‖u - ↑w‖
p : ℝ := inner (u - v) (w - v)
q : ℝ := ‖w - v‖ ^ 2
δ_le : ∀ (w : ↑K), δ ≤ ‖u - ↑w‖
δ_le' : ∀ (w : F), w ∈ K → δ ≤ ‖u - w‖
θ : ℝ
hθ₁ : 0 < θ
hθ₂ : θ ≤ 1
⊢ ‖u - v‖ * ‖u - v‖ - 2 * (θ * inner (u - v) (w - v)) + θ * ‖w - v‖ * (θ * ‖w - v‖) =
    ‖u - v‖ * ‖u - v‖ - 2 * θ * inner (u - v) (w - v) + θ * θ * (‖w - v‖ * ‖w - v‖)
𝕜 : Type ?u.190458
E : Type ?u.190461
F : Type u_1
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Set F
h : Convex ℝ K
u v : F
hv : v ∈ K
this : Nonempty ↑K := Nonempty.intro { val := v, property := hv }
eq : ‖u - v‖ = ⨅ (w : ↑K), ‖u - ↑w‖
w : F
hw : w ∈ K
δ : ℝ := ⨅ (w : ↑K), ‖u - ↑w‖
p : ℝ := inner (u - v) (w - v)
q : ℝ := ‖w - v‖ ^ 2
δ_le : ∀ (w : ↑K), δ ≤ ‖u - ↑w‖
δ_le' : ∀ (w : F), w ∈ K → δ ≤ ‖u - w‖
θ : ℝ
hθ₁ : 0 < θ
hθ₂ : θ ≤ 1
⊢ ‖u - v‖ * ‖u - v‖ - 2 * (θ * inner (u - v) (w - v)) + absR θ * ‖w - v‖ * (absR θ * ‖w - v‖) =
    ‖u - v‖ * ‖u - v‖ - 2 * θ * inner (u - v) (w - v) + θ * θ * (‖w - v‖ * ‖w - v‖)
rw [abs_of_pos hθ₁]
no goals
𝕜 : Type ?u.190458
E : Type ?u.190461
F : Type u_1
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Set F
h : Convex ℝ K
u v : F
hv : v ∈ K
this : Nonempty ↑K := Nonempty.intro { val := v, property := hv }
eq : ‖u - v‖ = ⨅ (w : ↑K), ‖u - ↑w‖
w : F
hw : w ∈ K
δ : ℝ := ⨅ (w : ↑K), ‖u - ↑w‖
p : ℝ := inner (u - v) (w - v)
q : ℝ := ‖w - v‖ ^ 2
δ_le : ∀ (w : ↑K), δ ≤ ‖u - ↑w‖
δ_le' : ∀ (w : F), w ∈ K → δ ≤ ‖u - w‖
θ : ℝ
hθ₁ : 0 < θ
hθ₂ : θ ≤ 1
⊢ ‖u - v‖ * ‖u - v‖ - 2 * (θ * inner (u - v) (w - v)) + θ * ‖w - v‖ * (θ * ‖w - v‖) =
    ‖u - v‖ * ‖u - v‖ - 2 * θ * inner (u - v) (w - v) + θ * θ * (‖w - v‖ * ‖w - v‖)
ring
no goals
𝕜 : Type ?u.190458
E : Type ?u.190461
F : Type u_1
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Set F
h : Convex ℝ K
u v : F
hv : v ∈ K
this✝ : Nonempty ↑K := Nonempty.intro { val := v, property := hv }
eq : ‖u - v‖ = ⨅ (w : ↑K), ‖u - ↑w‖
w : F
hw : w ∈ K
δ : ℝ := ⨅ (w : ↑K), ‖u - ↑w‖
p : ℝ := inner (u - v) (w - v)
q : ℝ := ‖w - v‖ ^ 2
δ_le : ∀ (w : ↑K), δ ≤ ‖u - ↑w‖
δ_le' : ∀ (w : F), w ∈ K → δ ≤ ‖u - w‖
θ : ℝ
hθ₁ : 0 < θ
hθ₂ : θ ≤ 1
this : ‖u - v‖ ^ 2 ≤ ‖u - v‖ ^ 2 - 2 * θ * inner (u - v) (w - v) + θ * θ * ‖w - v‖ ^ 2
⊢ ‖u - v‖ ^ 2 - 2 * θ * inner (u - v) (w - v) + θ * θ * ‖w - v‖ ^ 2 =
    ‖u - v‖ ^ 2 + (θ * θ * ‖w - v‖ ^ 2 - 2 * θ * inner (u - v) (w - v))
abel
case pos
𝕜 : Type ?u.190458
E : Type ?u.190461
F : Type u_1
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Set F
h : Convex ℝ K
u v : F
hv : v ∈ K
this✝ : Nonempty ↑K := Nonempty.intro { val := v, property := hv }
eq : ‖u - v‖ = ⨅ (w : ↑K), ‖u - ↑w‖
w : F
hw : w ∈ K
δ : ℝ := ⨅ (w : ↑K), ‖u - ↑w‖
p : ℝ := inner (u - v) (w - v)
q : ℝ := ‖w - v‖ ^ 2
δ_le : ∀ (w : ↑K), δ ≤ ‖u - ↑w‖
δ_le' : ∀ (w : F), w ∈ K → δ ≤ ‖u - w‖
this : ∀ (θ : ℝ), 0 < θ → θ ≤ 1 → 2 * p ≤ θ * 0
hq : q = 0
⊢ inner (u - v) (w - v) ≤ 0
case pos
𝕜 : Type ?u.190458
E : Type ?u.190461
F : Type u_1
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Set F
h : Convex ℝ K
u v : F
hv : v ∈ K
this✝ : Nonempty ↑K := Nonempty.intro { val := v, property := hv }
eq : ‖u - v‖ = ⨅ (w : ↑K), ‖u - ↑w‖
w : F
hw : w ∈ K
δ : ℝ := ⨅ (w : ↑K), ‖u - ↑w‖
p : ℝ := inner (u - v) (w - v)
q : ℝ := ‖w - v‖ ^ 2
δ_le : ∀ (w : ↑K), δ ≤ ‖u - ↑w‖
δ_le' : ∀ (w : F), w ∈ K → δ ≤ ‖u - w‖
this : ∀ (θ : ℝ), 0 < θ → θ ≤ 1 → 2 * p ≤ θ * q
hq : q = 0
⊢ inner (u - v) (w - v) ≤ 0
rw [hq] at this
case pos
𝕜 : Type ?u.190458
E : Type ?u.190461
F : Type u_1
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Set F
h : Convex ℝ K
u v : F
hv : v ∈ K
this✝¹ : Nonempty ↑K := Nonempty.intro { val := v, property := hv }
eq : ‖u - v‖ = ⨅ (w : ↑K), ‖u - ↑w‖
w : F
hw : w ∈ K
δ : ℝ := ⨅ (w : ↑K), ‖u - ↑w‖
p : ℝ := inner (u - v) (w - v)
q : ℝ := ‖w - v‖ ^ 2
δ_le : ∀ (w : ↑K), δ ≤ ‖u - ↑w‖
δ_le' : ∀ (w : F), w ∈ K → δ ≤ ‖u - w‖
this✝ : ∀ (θ : ℝ), 0 < θ → θ ≤ 1 → 2 * p ≤ θ * 0
hq : q = 0
this : p ≤ 0
⊢ inner (u - v) (w - v) ≤ 0
case pos
𝕜 : Type ?u.190458
E : Type ?u.190461
F : Type u_1
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Set F
h : Convex ℝ K
u v : F
hv : v ∈ K
this✝ : Nonempty ↑K := Nonempty.intro { val := v, property := hv }
eq : ‖u - v‖ = ⨅ (w : ↑K), ‖u - ↑w‖
w : F
hw : w ∈ K
δ : ℝ := ⨅ (w : ↑K), ‖u - ↑w‖
p : ℝ := inner (u - v) (w - v)
q : ℝ := ‖w - v‖ ^ 2
δ_le : ∀ (w : ↑K), δ ≤ ‖u - ↑w‖
δ_le' : ∀ (w : F), w ∈ K → δ ≤ ‖u - w‖
this : ∀ (θ : ℝ), 0 < θ → θ ≤ 1 → 2 * p ≤ θ * 0
hq : q = 0
⊢ inner (u - v) (w - v) ≤ 0
have : p ≤ 0 := by
  have := this (1 : ℝ) (by norm_num) (by norm_num)
  linarith
no goals
case pos
𝕜 : Type ?u.190458
E : Type ?u.190461
F : Type u_1
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Set F
h : Convex ℝ K
u v : F
hv : v ∈ K
this✝¹ : Nonempty ↑K := Nonempty.intro { val := v, property := hv }
eq : ‖u - v‖ = ⨅ (w : ↑K), ‖u - ↑w‖
w : F
hw : w ∈ K
δ : ℝ := ⨅ (w : ↑K), ‖u - ↑w‖
p : ℝ := inner (u - v) (w - v)
q : ℝ := ‖w - v‖ ^ 2
δ_le : ∀ (w : ↑K), δ ≤ ‖u - ↑w‖
δ_le' : ∀ (w : F), w ∈ K → δ ≤ ‖u - w‖
this✝ : ∀ (θ : ℝ), 0 < θ → θ ≤ 1 → 2 * p ≤ θ * 0
hq : q = 0
this : p ≤ 0
⊢ inner (u - v) (w - v) ≤ 0
exact this
𝕜 : Type ?u.190458
E : Type ?u.190461
F : Type u_1
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Set F
h : Convex ℝ K
u v : F
hv : v ∈ K
this✝¹ : Nonempty ↑K := Nonempty.intro { val := v, property := hv }
eq : ‖u - v‖ = ⨅ (w : ↑K), ‖u - ↑w‖
w : F
hw : w ∈ K
δ : ℝ := ⨅ (w : ↑K), ‖u - ↑w‖
p : ℝ := inner (u - v) (w - v)
q : ℝ := ‖w - v‖ ^ 2
δ_le : ∀ (w : ↑K), δ ≤ ‖u - ↑w‖
δ_le' : ∀ (w : F), w ∈ K → δ ≤ ‖u - w‖
this✝ : ∀ (θ : ℝ), 0 < θ → θ ≤ 1 → 2 * p ≤ θ * 0
hq : q = 0
this : 2 * p ≤ 1 * 0
⊢ p ≤ 0
𝕜 : Type ?u.190458
E : Type ?u.190461
F : Type u_1
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Set F
h : Convex ℝ K
u v : F
hv : v ∈ K
this✝ : Nonempty ↑K := Nonempty.intro { val := v, property := hv }
eq : ‖u - v‖ = ⨅ (w : ↑K), ‖u - ↑w‖
w : F
hw : w ∈ K
δ : ℝ := ⨅ (w : ↑K), ‖u - ↑w‖
p : ℝ := inner (u - v) (w - v)
q : ℝ := ‖w - v‖ ^ 2
δ_le : ∀ (w : ↑K), δ ≤ ‖u - ↑w‖
δ_le' : ∀ (w : F), w ∈ K → δ ≤ ‖u - w‖
this : ∀ (θ : ℝ), 0 < θ → θ ≤ 1 → 2 * p ≤ θ * 0
hq : q = 0
⊢ p ≤ 0
have := this (1 : ℝ) (by norm_num) (by norm_num)
no goals
𝕜 : Type ?u.190458
E : Type ?u.190461
F : Type u_1
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Set F
h : Convex ℝ K
u v : F
hv : v ∈ K
this✝¹ : Nonempty ↑K := Nonempty.intro { val := v, property := hv }
eq : ‖u - v‖ = ⨅ (w : ↑K), ‖u - ↑w‖
w : F
hw : w ∈ K
δ : ℝ := ⨅ (w : ↑K), ‖u - ↑w‖
p : ℝ := inner (u - v) (w - v)
q : ℝ := ‖w - v‖ ^ 2
δ_le : ∀ (w : ↑K), δ ≤ ‖u - ↑w‖
δ_le' : ∀ (w : F), w ∈ K → δ ≤ ‖u - w‖
this✝ : ∀ (θ : ℝ), 0 < θ → θ ≤ 1 → 2 * p ≤ θ * 0
hq : q = 0
this : 2 * p ≤ 1 * 0
⊢ p ≤ 0
linarith
no goals
𝕜 : Type ?u.190458
E : Type ?u.190461
F : Type u_1
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Set F
h : Convex ℝ K
u v : F
hv : v ∈ K
this✝ : Nonempty ↑K := Nonempty.intro { val := v, property := hv }
eq : ‖u - v‖ = ⨅ (w : ↑K), ‖u - ↑w‖
w : F
hw : w ∈ K
δ : ℝ := ⨅ (w : ↑K), ‖u - ↑w‖
p : ℝ := inner (u - v) (w - v)
q : ℝ := ‖w - v‖ ^ 2
δ_le : ∀ (w : ↑K), δ ≤ ‖u - ↑w‖
δ_le' : ∀ (w : F), w ∈ K → δ ≤ ‖u - w‖
this : ∀ (θ : ℝ), 0 < θ → θ ≤ 1 → 2 * p ≤ θ * 0
hq : q = 0
⊢ 0 < 1
norm_num
no goals
𝕜 : Type ?u.190458
E : Type ?u.190461
F : Type u_1
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Set F
h : Convex ℝ K
u v : F
hv : v ∈ K
this✝ : Nonempty ↑K := Nonempty.intro { val := v, property := hv }
eq : ‖u - v‖ = ⨅ (w : ↑K), ‖u - ↑w‖
w : F
hw : w ∈ K
δ : ℝ := ⨅ (w : ↑K), ‖u - ↑w‖
p : ℝ := inner (u - v) (w - v)
q : ℝ := ‖w - v‖ ^ 2
δ_le : ∀ (w : ↑K), δ ≤ ‖u - ↑w‖
δ_le' : ∀ (w : F), w ∈ K → δ ≤ ‖u - w‖
this : ∀ (θ : ℝ), 0 < θ → θ ≤ 1 → 2 * p ≤ θ * 0
hq : q = 0
⊢ 1 ≤ 1
norm_num
case neg
𝕜 : Type ?u.190458
E : Type ?u.190461
F : Type u_1
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Set F
h : Convex ℝ K
u v : F
hv : v ∈ K
this✝ : Nonempty ↑K := Nonempty.intro { val := v, property := hv }
eq : ‖u - v‖ = ⨅ (w : ↑K), ‖u - ↑w‖
w : F
hw : w ∈ K
δ : ℝ := ⨅ (w : ↑K), ‖u - ↑w‖
p : ℝ := inner (u - v) (w - v)
q : ℝ := ‖w - v‖ ^ 2
δ_le : ∀ (w : ↑K), δ ≤ ‖u - ↑w‖
δ_le' : ∀ (w : F), w ∈ K → δ ≤ ‖u - w‖
this : ∀ (θ : ℝ), 0 < θ → θ ≤ 1 → 2 * p ≤ θ * q
hq : ¬q = 0
q_pos : 0 < q
⊢ inner (u - v) (w - v) ≤ 0
case neg
𝕜 : Type ?u.190458
E : Type ?u.190461
F : Type u_1
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Set F
h : Convex ℝ K
u v : F
hv : v ∈ K
this✝ : Nonempty ↑K := Nonempty.intro { val := v, property := hv }
eq : ‖u - v‖ = ⨅ (w : ↑K), ‖u - ↑w‖
w : F
hw : w ∈ K
δ : ℝ := ⨅ (w : ↑K), ‖u - ↑w‖
p : ℝ := inner (u - v) (w - v)
q : ℝ := ‖w - v‖ ^ 2
δ_le : ∀ (w : ↑K), δ ≤ ‖u - ↑w‖
δ_le' : ∀ (w : F), w ∈ K → δ ≤ ‖u - w‖
this : ∀ (θ : ℝ), 0 < θ → θ ≤ 1 → 2 * p ≤ θ * q
hq : ¬q = 0
⊢ inner (u - v) (w - v) ≤ 0
have q_pos : 0 < q := lt_of_le_of_ne (sq_nonneg _) fun h ↦ hq h.symm
case neg
𝕜 : Type ?u.190458
E : Type ?u.190461
F : Type u_1
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Set F
h : Convex ℝ K
u v : F
hv : v ∈ K
this✝ : Nonempty ↑K := Nonempty.intro { val := v, property := hv }
eq : ‖u - v‖ = ⨅ (w : ↑K), ‖u - ↑w‖
w : F
hw : w ∈ K
δ : ℝ := ⨅ (w : ↑K), ‖u - ↑w‖
p : ℝ := inner (u - v) (w - v)
q : ℝ := ‖w - v‖ ^ 2
δ_le : ∀ (w : ↑K), δ ≤ ‖u - ↑w‖
δ_le' : ∀ (w : F), w ∈ K → δ ≤ ‖u - w‖
this : ∀ (θ : ℝ), 0 < θ → θ ≤ 1 → 2 * p ≤ θ * q
hq : ¬q = 0
q_pos : 0 < q
hp : ¬inner (u - v) (w - v) ≤ 0
⊢ False
case neg
𝕜 : Type ?u.190458
E : Type ?u.190461
F : Type u_1
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Set F
h : Convex ℝ K
u v : F
hv : v ∈ K
this✝ : Nonempty ↑K := Nonempty.intro { val := v, property := hv }
eq : ‖u - v‖ = ⨅ (w : ↑K), ‖u - ↑w‖
w : F
hw : w ∈ K
δ : ℝ := ⨅ (w : ↑K), ‖u - ↑w‖
p : ℝ := inner (u - v) (w - v)
q : ℝ := ‖w - v‖ ^ 2
δ_le : ∀ (w : ↑K), δ ≤ ‖u - ↑w‖
δ_le' : ∀ (w : F), w ∈ K → δ ≤ ‖u - w‖
this : ∀ (θ : ℝ), 0 < θ → θ ≤ 1 → 2 * p ≤ θ * q
hq : ¬q = 0
q_pos : 0 < q
⊢ inner (u - v) (w - v) ≤ 0
by_contra hp
case neg
𝕜 : Type ?u.190458
E : Type ?u.190461
F : Type u_1
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Set F
h : Convex ℝ K
u v : F
hv : v ∈ K
this✝ : Nonempty ↑K := Nonempty.intro { val := v, property := hv }
eq : ‖u - v‖ = ⨅ (w : ↑K), ‖u - ↑w‖
w : F
hw : w ∈ K
δ : ℝ := ⨅ (w : ↑K), ‖u - ↑w‖
p : ℝ := inner (u - v) (w - v)
q : ℝ := ‖w - v‖ ^ 2
δ_le : ∀ (w : ↑K), δ ≤ ‖u - ↑w‖
δ_le' : ∀ (w : F), w ∈ K → δ ≤ ‖u - w‖
this : ∀ (θ : ℝ), 0 < θ → θ ≤ 1 → 2 * p ≤ θ * q
hq : ¬q = 0
q_pos : 0 < q
hp : 0 < inner (u - v) (w - v)
⊢ False
case neg
𝕜 : Type ?u.190458
E : Type ?u.190461
F : Type u_1
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Set F
h : Convex ℝ K
u v : F
hv : v ∈ K
this✝ : Nonempty ↑K := Nonempty.intro { val := v, property := hv }
eq : ‖u - v‖ = ⨅ (w : ↑K), ‖u - ↑w‖
w : F
hw : w ∈ K
δ : ℝ := ⨅ (w : ↑K), ‖u - ↑w‖
p : ℝ := inner (u - v) (w - v)
q : ℝ := ‖w - v‖ ^ 2
δ_le : ∀ (w : ↑K), δ ≤ ‖u - ↑w‖
δ_le' : ∀ (w : F), w ∈ K → δ ≤ ‖u - w‖
this : ∀ (θ : ℝ), 0 < θ → θ ≤ 1 → 2 * p ≤ θ * q
hq : ¬q = 0
q_pos : 0 < q
hp : ¬inner (u - v) (w - v) ≤ 0
⊢ False
rw [not_le] at hp
case neg
𝕜 : Type ?u.190458
E : Type ?u.190461
F : Type u_1
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Set F
h : Convex ℝ K
u v : F
hv : v ∈ K
this✝ : Nonempty ↑K := Nonempty.intro { val := v, property := hv }
eq : ‖u - v‖ = ⨅ (w : ↑K), ‖u - ↑w‖
w : F
hw : w ∈ K
δ : ℝ := ⨅ (w : ↑K), ‖u - ↑w‖
p : ℝ := inner (u - v) (w - v)
q : ℝ := ‖w - v‖ ^ 2
δ_le : ∀ (w : ↑K), δ ≤ ‖u - ↑w‖
δ_le' : ∀ (w : F), w ∈ K → δ ≤ ‖u - w‖
this : ∀ (θ : ℝ), 0 < θ → θ ≤ 1 → 2 * p ≤ θ * q
hq : ¬q = 0
q_pos : 0 < q
hp : 0 < inner (u - v) (w - v)
θ : ℝ := min 1 (p / q)
⊢ False
case neg
𝕜 : Type ?u.190458
E : Type ?u.190461
F : Type u_1
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Set F
h : Convex ℝ K
u v : F
hv : v ∈ K
this✝ : Nonempty ↑K := Nonempty.intro { val := v, property := hv }
eq : ‖u - v‖ = ⨅ (w : ↑K), ‖u - ↑w‖
w : F
hw : w ∈ K
δ : ℝ := ⨅ (w : ↑K), ‖u - ↑w‖
p : ℝ := inner (u - v) (w - v)
q : ℝ := ‖w - v‖ ^ 2
δ_le : ∀ (w : ↑K), δ ≤ ‖u - ↑w‖
δ_le' : ∀ (w : F), w ∈ K → δ ≤ ‖u - w‖
this : ∀ (θ : ℝ), 0 < θ → θ ≤ 1 → 2 * p ≤ θ * q
hq : ¬q = 0
q_pos : 0 < q
hp : 0 < inner (u - v) (w - v)
⊢ False
let θ := min (1 : ℝ) (p / q)
case neg
𝕜 : Type ?u.190458
E : Type ?u.190461
F : Type u_1
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Set F
h : Convex ℝ K
u v : F
hv : v ∈ K
this✝ : Nonempty ↑K := Nonempty.intro { val := v, property := hv }
eq : ‖u - v‖ = ⨅ (w : ↑K), ‖u - ↑w‖
w : F
hw : w ∈ K
δ : ℝ := ⨅ (w : ↑K), ‖u - ↑w‖
p : ℝ := inner (u - v) (w - v)
q : ℝ := ‖w - v‖ ^ 2
δ_le : ∀ (w : ↑K), δ ≤ ‖u - ↑w‖
δ_le' : ∀ (w : F), w ∈ K → δ ≤ ‖u - w‖
this : ∀ (θ : ℝ), 0 < θ → θ ≤ 1 → 2 * p ≤ θ * q
hq : ¬q = 0
q_pos : 0 < q
hp : 0 < inner (u - v) (w - v)
θ : ℝ := min 1 (p / q)
eq₁ : θ * q ≤ p
⊢ False
case neg
𝕜 : Type ?u.190458
E : Type ?u.190461
F : Type u_1
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Set F
h : Convex ℝ K
u v : F
hv : v ∈ K
this✝ : Nonempty ↑K := Nonempty.intro { val := v, property := hv }
eq : ‖u - v‖ = ⨅ (w : ↑K), ‖u - ↑w‖
w : F
hw : w ∈ K
δ : ℝ := ⨅ (w : ↑K), ‖u - ↑w‖
p : ℝ := inner (u - v) (w - v)
q : ℝ := ‖w - v‖ ^ 2
δ_le : ∀ (w : ↑K), δ ≤ ‖u - ↑w‖
δ_le' : ∀ (w : F), w ∈ K → δ ≤ ‖u - w‖
this : ∀ (θ : ℝ), 0 < θ → θ ≤ 1 → 2 * p ≤ θ * q
hq : ¬q = 0
q_pos : 0 < q
hp : 0 < inner (u - v) (w - v)
θ : ℝ := min 1 (p / q)
⊢ False
have eq₁ : θ * q ≤ p :=
  calc
    θ * q ≤ p / q * q := mul_le_mul_of_nonneg_right (min_le_right _ _) (sq_nonneg _)
    _ = p := div_mul_cancel _ hq
case neg
𝕜 : Type ?u.190458
E : Type ?u.190461
F : Type u_1
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Set F
h : Convex ℝ K
u v : F
hv : v ∈ K
this✝¹ : Nonempty ↑K := Nonempty.intro { val := v, property := hv }
eq : ‖u - v‖ = ⨅ (w : ↑K), ‖u - ↑w‖
w : F
hw : w ∈ K
δ : ℝ := ⨅ (w : ↑K), ‖u - ↑w‖
p : ℝ := inner (u - v) (w - v)
q : ℝ := ‖w - v‖ ^ 2
δ_le : ∀ (w : ↑K), δ ≤ ‖u - ↑w‖
δ_le' : ∀ (w : F), w ∈ K → δ ≤ ‖u - w‖
this✝ : ∀ (θ : ℝ), 0 < θ → θ ≤ 1 → 2 * p ≤ θ * q
hq : ¬q = 0
q_pos : 0 < q
hp : 0 < inner (u - v) (w - v)
θ : ℝ := min 1 (p / q)
eq₁ : θ * q ≤ p
this : 2 * p ≤ p
⊢ False
case neg
𝕜 : Type ?u.190458
E : Type ?u.190461
F : Type u_1
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Set F
h : Convex ℝ K
u v : F
hv : v ∈ K
this✝ : Nonempty ↑K := Nonempty.intro { val := v, property := hv }
eq : ‖u - v‖ = ⨅ (w : ↑K), ‖u - ↑w‖
w : F
hw : w ∈ K
δ : ℝ := ⨅ (w : ↑K), ‖u - ↑w‖
p : ℝ := inner (u - v) (w - v)
q : ℝ := ‖w - v‖ ^ 2
δ_le : ∀ (w : ↑K), δ ≤ ‖u - ↑w‖
δ_le' : ∀ (w : F), w ∈ K → δ ≤ ‖u - w‖
this : ∀ (θ : ℝ), 0 < θ → θ ≤ 1 → 2 * p ≤ θ * q
hq : ¬q = 0
q_pos : 0 < q
hp : 0 < inner (u - v) (w - v)
θ : ℝ := min 1 (p / q)
eq₁ : θ * q ≤ p
⊢ False
have : 2 * p ≤ p :=
  calc
    2 * p ≤ θ * q := by
      refine' this θ (lt_min (by norm_num) (div_pos hp q_pos)) (by norm_num)
    _ ≤ p := eq₁
no goals
case neg
𝕜 : Type ?u.190458
E : Type ?u.190461
F : Type u_1
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Set F
h : Convex ℝ K
u v : F
hv : v ∈ K
this✝¹ : Nonempty ↑K := Nonempty.intro { val := v, property := hv }
eq : ‖u - v‖ = ⨅ (w : ↑K), ‖u - ↑w‖
w : F
hw : w ∈ K
δ : ℝ := ⨅ (w : ↑K), ‖u - ↑w‖
p : ℝ := inner (u - v) (w - v)
q : ℝ := ‖w - v‖ ^ 2
δ_le : ∀ (w : ↑K), δ ≤ ‖u - ↑w‖
δ_le' : ∀ (w : F), w ∈ K → δ ≤ ‖u - w‖
this✝ : ∀ (θ : ℝ), 0 < θ → θ ≤ 1 → 2 * p ≤ θ * q
hq : ¬q = 0
q_pos : 0 < q
hp : 0 < inner (u - v) (w - v)
θ : ℝ := min 1 (p / q)
eq₁ : θ * q ≤ p
this : 2 * p ≤ p
⊢ False
linarith
no goals
𝕜 : Type ?u.190458
E : Type ?u.190461
F : Type u_1
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Set F
h : Convex ℝ K
u v : F
hv : v ∈ K
this✝ : Nonempty ↑K := Nonempty.intro { val := v, property := hv }
eq : ‖u - v‖ = ⨅ (w : ↑K), ‖u - ↑w‖
w : F
hw : w ∈ K
δ : ℝ := ⨅ (w : ↑K), ‖u - ↑w‖
p : ℝ := inner (u - v) (w - v)
q : ℝ := ‖w - v‖ ^ 2
δ_le : ∀ (w : ↑K), δ ≤ ‖u - ↑w‖
δ_le' : ∀ (w : F), w ∈ K → δ ≤ ‖u - w‖
this : ∀ (θ : ℝ), 0 < θ → θ ≤ 1 → 2 * p ≤ θ * q
hq : ¬q = 0
q_pos : 0 < q
hp : 0 < inner (u - v) (w - v)
θ : ℝ := min 1 (p / q)
eq₁ : θ * q ≤ p
⊢ 2 * p ≤ θ * q
refine' this θ (lt_min (by norm_num) (div_pos hp q_pos)) (by norm_num)
no goals
𝕜 : Type ?u.190458
E : Type ?u.190461
F : Type u_1
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Set F
h : Convex ℝ K
u v : F
hv : v ∈ K
this✝ : Nonempty ↑K := Nonempty.intro { val := v, property := hv }
eq : ‖u - v‖ = ⨅ (w : ↑K), ‖u - ↑w‖
w : F
hw : w ∈ K
δ : ℝ := ⨅ (w : ↑K), ‖u - ↑w‖
p : ℝ := inner (u - v) (w - v)
q : ℝ := ‖w - v‖ ^ 2
δ_le : ∀ (w : ↑K), δ ≤ ‖u - ↑w‖
δ_le' : ∀ (w : F), w ∈ K → δ ≤ ‖u - w‖
this : ∀ (θ : ℝ), 0 < θ → θ ≤ 1 → 2 * p ≤ θ * q
hq : ¬q = 0
q_pos : 0 < q
hp : 0 < inner (u - v) (w - v)
θ : ℝ := min 1 (p / q)
eq₁ : θ * q ≤ p
⊢ 0 < 1
norm_num
no goals
𝕜 : Type ?u.190458
E : Type ?u.190461
F : Type u_1
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Set F
h : Convex ℝ K
u v : F
hv : v ∈ K
this✝ : Nonempty ↑K := Nonempty.intro { val := v, property := hv }
eq : ‖u - v‖ = ⨅ (w : ↑K), ‖u - ↑w‖
w : F
hw : w ∈ K
δ : ℝ := ⨅ (w : ↑K), ‖u - ↑w‖
p : ℝ := inner (u - v) (w - v)
q : ℝ := ‖w - v‖ ^ 2
δ_le : ∀ (w : ↑K), δ ≤ ‖u - ↑w‖
δ_le' : ∀ (w : F), w ∈ K → δ ≤ ‖u - w‖
this : ∀ (θ : ℝ), 0 < θ → θ ≤ 1 → 2 * p ≤ θ * q
hq : ¬q = 0
q_pos : 0 < q
hp : 0 < inner (u - v) (w - v)
θ : ℝ := min 1 (p / q)
eq₁ : θ * q ≤ p
⊢ θ ≤ 1
norm_num
case mpr
𝕜 : Type ?u.190458
E : Type ?u.190461
F : Type u_1
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Set F
h✝ : Convex ℝ K
u v : F
hv : v ∈ K
this : Nonempty ↑K := Nonempty.intro { val := v, property := hv }
h : ∀ (w : F), w ∈ K → inner (u - v) (w - v) ≤ 0
⊢ ‖u - v‖ = ⨅ (w : ↑K), ‖u - ↑w‖
case mpr
𝕜 : Type ?u.190458
E : Type ?u.190461
F : Type u_1
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Set F
h : Convex ℝ K
u v : F
hv : v ∈ K
this : Nonempty ↑K := Nonempty.intro { val := v, property := hv }
⊢ (∀ (w : F), w ∈ K → inner (u - v) (w - v) ≤ 0) → ‖u - v‖ = ⨅ (w : ↑K), ‖u - ↑w‖
intro h
case mpr.a
𝕜 : Type ?u.190458
E : Type ?u.190461
F : Type u_1
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Set F
h✝ : Convex ℝ K
u v : F
hv : v ∈ K
this : Nonempty ↑K := Nonempty.intro { val := v, property := hv }
h : ∀ (w : F), w ∈ K → inner (u - v) (w - v) ≤ 0
⊢ ‖u - v‖ ≤ ⨅ (w : ↑K), ‖u - ↑w‖

case mpr.a
𝕜 : Type ?u.190458
E : Type ?u.190461
F : Type u_1
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Set F
h✝ : Convex ℝ K
u v : F
hv : v ∈ K
this : Nonempty ↑K := Nonempty.intro { val := v, property := hv }
h : ∀ (w : F), w ∈ K → inner (u - v) (w - v) ≤ 0
⊢ (⨅ (w : ↑K), ‖u - ↑w‖) ≤ ‖u - v‖
case mpr
𝕜 : Type ?u.190458
E : Type ?u.190461
F : Type u_1
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Set F
h✝ : Convex ℝ K
u v : F
hv : v ∈ K
this : Nonempty ↑K := Nonempty.intro { val := v, property := hv }
h : ∀ (w : F), w ∈ K → inner (u - v) (w - v) ≤ 0
⊢ ‖u - v‖ = ⨅ (w : ↑K), ‖u - ↑w‖
apply le_antisymm
case mpr.a.H
𝕜 : Type ?u.190458
E : Type ?u.190461
F : Type u_1
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Set F
h✝ : Convex ℝ K
u v : F
hv : v ∈ K
this : Nonempty ↑K := Nonempty.intro { val := v, property := hv }
h : ∀ (w : F), w ∈ K → inner (u - v) (w - v) ≤ 0
⊢ ∀ (x : ↑K), ‖u - v‖ ≤ ‖u - ↑x‖
case mpr.a
𝕜 : Type ?u.190458
E : Type ?u.190461
F : Type u_1
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Set F
h✝ : Convex ℝ K
u v : F
hv : v ∈ K
this : Nonempty ↑K := Nonempty.intro { val := v, property := hv }
h : ∀ (w : F), w ∈ K → inner (u - v) (w - v) ≤ 0
⊢ ‖u - v‖ ≤ ⨅ (w : ↑K), ‖u - ↑w‖
apply le_ciInf
case mpr.a.H
𝕜 : Type ?u.190458
E : Type ?u.190461
F : Type u_1
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Set F
h✝ : Convex ℝ K
u v : F
hv : v ∈ K
this : Nonempty ↑K := Nonempty.intro { val := v, property := hv }
h : ∀ (w : F), w ∈ K → inner (u - v) (w - v) ≤ 0
w : ↑K
⊢ ‖u - v‖ ≤ ‖u - ↑w‖
case mpr.a.H
𝕜 : Type ?u.190458
E : Type ?u.190461
F : Type u_1
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Set F
h✝ : Convex ℝ K
u v : F
hv : v ∈ K
this : Nonempty ↑K := Nonempty.intro { val := v, property := hv }
h : ∀ (w : F), w ∈ K → inner (u - v) (w - v) ≤ 0
⊢ ∀ (x : ↑K), ‖u - v‖ ≤ ‖u - ↑x‖
intro w
case mpr.a.H
𝕜 : Type ?u.190458
E : Type ?u.190461
F : Type u_1
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Set F
h✝ : Convex ℝ K
u v : F
hv : v ∈ K
this : Nonempty ↑K := Nonempty.intro { val := v, property := hv }
h : ∀ (w : F), w ∈ K → inner (u - v) (w - v) ≤ 0
w : ↑K
⊢ ‖u - v‖ * ‖u - v‖ ≤ ‖u - ↑w‖ * ‖u - ↑w‖
case mpr.a.H
𝕜 : Type ?u.190458
E : Type ?u.190461
F : Type u_1
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Set F
h✝ : Convex ℝ K
u v : F
hv : v ∈ K
this : Nonempty ↑K := Nonempty.intro { val := v, property := hv }
h : ∀ (w : F), w ∈ K → inner (u - v) (w - v) ≤ 0
w : ↑K
⊢ ‖u - v‖ ≤ ‖u - ↑w‖
apply nonneg_le_nonneg_of_sq_le_sq (norm_nonneg _)
case mpr.a.H
𝕜 : Type ?u.190458
E : Type ?u.190461
F : Type u_1
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Set F
h✝ : Convex ℝ K
u v : F
hv : v ∈ K
this✝ : Nonempty ↑K := Nonempty.intro { val := v, property := hv }
h : ∀ (w : F), w ∈ K → inner (u - v) (w - v) ≤ 0
w : ↑K
this : inner (u - v) (↑w - v) ≤ 0
⊢ ‖u - v‖ * ‖u - v‖ ≤ ‖u - ↑w‖ * ‖u - ↑w‖
case mpr.a.H
𝕜 : Type ?u.190458
E : Type ?u.190461
F : Type u_1
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Set F
h✝ : Convex ℝ K
u v : F
hv : v ∈ K
this : Nonempty ↑K := Nonempty.intro { val := v, property := hv }
h : ∀ (w : F), w ∈ K → inner (u - v) (w - v) ≤ 0
w : ↑K
⊢ ‖u - v‖ * ‖u - v‖ ≤ ‖u - ↑w‖ * ‖u - ↑w‖
have := h w w.2
no goals
case mpr.a.H
𝕜 : Type ?u.190458
E : Type ?u.190461
F : Type u_1
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Set F
h✝ : Convex ℝ K
u v : F
hv : v ∈ K
this✝ : Nonempty ↑K := Nonempty.intro { val := v, property := hv }
h : ∀ (w : F), w ∈ K → inner (u - v) (w - v) ≤ 0
w : ↑K
this : inner (u - v) (↑w - v) ≤ 0
⊢ ‖u - v‖ * ‖u - v‖ ≤ ‖u - ↑w‖ * ‖u - ↑w‖
calc
  ‖u - v‖ * ‖u - v‖ ≤ ‖u - v‖ * ‖u - v‖ - 2 * inner (u - v) ((w : F) - v) := by linarith
  _ ≤ ‖u - v‖ ^ 2 - 2 * inner (u - v) ((w : F) - v) + ‖(w : F) - v‖ ^ 2 := by
    rw [sq]
    refine' le_add_of_nonneg_right _
    exact sq_nonneg _
  _ = ‖u - v - (w - v)‖ ^ 2 := (@norm_sub_sq ℝ _ _ _ _ _ _).symm
  _ = ‖u - w‖ * ‖u - w‖ := by
    have : u - v - (w - v) = u - w := by abel
    rw [this, sq]
no goals
𝕜 : Type ?u.190458
E : Type ?u.190461
F : Type u_1
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Set F
h✝ : Convex ℝ K
u v : F
hv : v ∈ K
this✝ : Nonempty ↑K := Nonempty.intro { val := v, property := hv }
h : ∀ (w : F), w ∈ K → inner (u - v) (w - v) ≤ 0
w : ↑K
this : inner (u - v) (↑w - v) ≤ 0
⊢ ‖u - v‖ * ‖u - v‖ ≤ ‖u - v‖ * ‖u - v‖ - 2 * inner (u - v) (↑w - v)
linarith
𝕜 : Type ?u.190458
E : Type ?u.190461
F : Type u_1
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Set F
h✝ : Convex ℝ K
u v : F
hv : v ∈ K
this✝ : Nonempty ↑K := Nonempty.intro { val := v, property := hv }
h : ∀ (w : F), w ∈ K → inner (u - v) (w - v) ≤ 0
w : ↑K
this : inner (u - v) (↑w - v) ≤ 0
⊢ ‖u - v‖ * ‖u - v‖ - 2 * inner (u - v) (↑w - v) ≤ ‖u - v‖ * ‖u - v‖ - 2 * inner (u - v) (↑w - v) + ‖↑w - v‖ ^ 2
𝕜 : Type ?u.190458
E : Type ?u.190461
F : Type u_1
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Set F
h✝ : Convex ℝ K
u v : F
hv : v ∈ K
this✝ : Nonempty ↑K := Nonempty.intro { val := v, property := hv }
h : ∀ (w : F), w ∈ K → inner (u - v) (w - v) ≤ 0
w : ↑K
this : inner (u - v) (↑w - v) ≤ 0
⊢ ‖u - v‖ * ‖u - v‖ - 2 * inner (u - v) (↑w - v) ≤ ‖u - v‖ ^ 2 - 2 * inner (u - v) (↑w - v) + ‖↑w - v‖ ^ 2
rw [sq]
𝕜 : Type ?u.190458
E : Type ?u.190461
F : Type u_1
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Set F
h✝ : Convex ℝ K
u v : F
hv : v ∈ K
this✝ : Nonempty ↑K := Nonempty.intro { val := v, property := hv }
h : ∀ (w : F), w ∈ K → inner (u - v) (w - v) ≤ 0
w : ↑K
this : inner (u - v) (↑w - v) ≤ 0
⊢ 0 ≤ ‖↑w - v‖ ^ 2
𝕜 : Type ?u.190458
E : Type ?u.190461
F : Type u_1
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Set F
h✝ : Convex ℝ K
u v : F
hv : v ∈ K
this✝ : Nonempty ↑K := Nonempty.intro { val := v, property := hv }
h : ∀ (w : F), w ∈ K → inner (u - v) (w - v) ≤ 0
w : ↑K
this : inner (u - v) (↑w - v) ≤ 0
⊢ ‖u - v‖ * ‖u - v‖ - 2 * inner (u - v) (↑w - v) ≤ ‖u - v‖ * ‖u - v‖ - 2 * inner (u - v) (↑w - v) + ‖↑w - v‖ ^ 2
refine' le_add_of_nonneg_right _
no goals
𝕜 : Type ?u.190458
E : Type ?u.190461
F : Type u_1
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Set F
h✝ : Convex ℝ K
u v : F
hv : v ∈ K
this✝ : Nonempty ↑K := Nonempty.intro { val := v, property := hv }
h : ∀ (w : F), w ∈ K → inner (u - v) (w - v) ≤ 0
w : ↑K
this : inner (u - v) (↑w - v) ≤ 0
⊢ 0 ≤ ‖↑w - v‖ ^ 2
exact sq_nonneg _
𝕜 : Type ?u.190458
E : Type ?u.190461
F : Type u_1
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Set F
h✝ : Convex ℝ K
u v : F
hv : v ∈ K
this✝¹ : Nonempty ↑K := Nonempty.intro { val := v, property := hv }
h : ∀ (w : F), w ∈ K → inner (u - v) (w - v) ≤ 0
w : ↑K
this✝ : inner (u - v) (↑w - v) ≤ 0
this : u - v - (↑w - v) = u - ↑w
⊢ ‖u - v - (↑w - v)‖ ^ 2 = ‖u - ↑w‖ * ‖u - ↑w‖
𝕜 : Type ?u.190458
E : Type ?u.190461
F : Type u_1
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Set F
h✝ : Convex ℝ K
u v : F
hv : v ∈ K
this✝ : Nonempty ↑K := Nonempty.intro { val := v, property := hv }
h : ∀ (w : F), w ∈ K → inner (u - v) (w - v) ≤ 0
w : ↑K
this : inner (u - v) (↑w - v) ≤ 0
⊢ ‖u - v - (↑w - v)‖ ^ 2 = ‖u - ↑w‖ * ‖u - ↑w‖
have : u - v - (w - v) = u - w := by abel
no goals
𝕜 : Type ?u.190458
E : Type ?u.190461
F : Type u_1
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Set F
h✝ : Convex ℝ K
u v : F
hv : v ∈ K
this✝¹ : Nonempty ↑K := Nonempty.intro { val := v, property := hv }
h : ∀ (w : F), w ∈ K → inner (u - v) (w - v) ≤ 0
w : ↑K
this✝ : inner (u - v) (↑w - v) ≤ 0
this : u - v - (↑w - v) = u - ↑w
⊢ ‖u - v - (↑w - v)‖ ^ 2 = ‖u - ↑w‖ * ‖u - ↑w‖
rw [this, sq]
no goals
𝕜 : Type ?u.190458
E : Type ?u.190461
F : Type u_1
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Set F
h✝ : Convex ℝ K
u v : F
hv : v ∈ K
this✝ : Nonempty ↑K := Nonempty.intro { val := v, property := hv }
h : ∀ (w : F), w ∈ K → inner (u - v) (w - v) ≤ 0
w : ↑K
this : inner (u - v) (↑w - v) ≤ 0
⊢ u - v - (↑w - v) = u - ↑w
abel
case mpr.a
𝕜 : Type ?u.190458
E : Type ?u.190461
F : Type u_1
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Set F
h✝ : Convex ℝ K
u v : F
hv : v ∈ K
this : Nonempty ↑K := Nonempty.intro { val := v, property := hv }
h : ∀ (w : F), w ∈ K → inner (u - v) (w - v) ≤ 0
⊢ (⨅ (w : ↑K), ‖u - ↑w‖) ≤ (fun w => ‖u - ↑w‖) { val := v, property := hv }
case mpr.a
𝕜 : Type ?u.190458
E : Type ?u.190461
F : Type u_1
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Set F
h✝ : Convex ℝ K
u v : F
hv : v ∈ K
this : Nonempty ↑K := Nonempty.intro { val := v, property := hv }
h : ∀ (w : F), w ∈ K → inner (u - v) (w - v) ≤ 0
⊢ (⨅ (w : ↑K), ‖u - ↑w‖) ≤ ‖u - v‖
show (⨅ w : K, ‖u - w‖) ≤ (fun w : K => ‖u - w‖) ⟨v, hv⟩
case mpr.a.H
𝕜 : Type ?u.190458
E : Type ?u.190461
F : Type u_1
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Set F
h✝ : Convex ℝ K
u v : F
hv : v ∈ K
this : Nonempty ↑K := Nonempty.intro { val := v, property := hv }
h : ∀ (w : F), w ∈ K → inner (u - v) (w - v) ≤ 0
⊢ BddBelow (Set.range fun w => ‖u - ↑w‖)
case mpr.a
𝕜 : Type ?u.190458
E : Type ?u.190461
F : Type u_1
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Set F
h✝ : Convex ℝ K
u v : F
hv : v ∈ K
this : Nonempty ↑K := Nonempty.intro { val := v, property := hv }
h : ∀ (w : F), w ∈ K → inner (u - v) (w - v) ≤ 0
⊢ (⨅ (w : ↑K), ‖u - ↑w‖) ≤ (fun w => ‖u - ↑w‖) { val := v, property := hv }
apply ciInf_le
case mpr.a.H
𝕜 : Type ?u.190458
E : Type ?u.190461
F : Type u_1
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Set F
h✝ : Convex ℝ K
u v : F
hv : v ∈ K
this : Nonempty ↑K := Nonempty.intro { val := v, property := hv }
h : ∀ (w : F), w ∈ K → inner (u - v) (w - v) ≤ 0
⊢ 0 ∈ lowerBounds (Set.range fun w => ‖u - ↑w‖)
case mpr.a.H
𝕜 : Type ?u.190458
E : Type ?u.190461
F : Type u_1
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Set F
h✝ : Convex ℝ K
u v : F
hv : v ∈ K
this : Nonempty ↑K := Nonempty.intro { val := v, property := hv }
h : ∀ (w : F), w ∈ K → inner (u - v) (w - v) ≤ 0
⊢ BddBelow (Set.range fun w => ‖u - ↑w‖)
use 0
case mpr.a.H.intro
𝕜 : Type ?u.190458
E : Type ?u.190461
F : Type u_1
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Set F
h✝ : Convex ℝ K
u v : F
hv : v ∈ K
this : Nonempty ↑K := Nonempty.intro { val := v, property := hv }
h : ∀ (w : F), w ∈ K → inner (u - v) (w - v) ≤ 0
z : ↑K
⊢ 0 ≤ (fun w => ‖u - ↑w‖) z
case mpr.a.H
𝕜 : Type ?u.190458
E : Type ?u.190461
F : Type u_1
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Set F
h✝ : Convex ℝ K
u v : F
hv : v ∈ K
this : Nonempty ↑K := Nonempty.intro { val := v, property := hv }
h : ∀ (w : F), w ∈ K → inner (u - v) (w - v) ≤ 0
⊢ 0 ∈ lowerBounds (Set.range fun w => ‖u - ↑w‖)
rintro y ⟨z, rfl⟩
no goals
case mpr.a.H.intro
𝕜 : Type ?u.190458
E : Type ?u.190461
F : Type u_1
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Set F
h✝ : Convex ℝ K
u v : F
hv : v ∈ K
this : Nonempty ↑K := Nonempty.intro { val := v, property := hv }
h : ∀ (w : F), w ∈ K → inner (u - v) (w - v) ≤ 0
z : ↑K
⊢ 0 ≤ (fun w => ‖u - ↑w‖) z
exact norm_nonneg _