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
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‖ - HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((re : (a : ℝ) → ℝ) (θ * ⟪u - v, w - v⟫_ℝ) : ℝ) +
      ‖θ‖ * ‖w - v‖ * (‖θ‖ * ‖w - v‖) =
    ‖u - v‖ * ‖u - v‖ - 2 * θ * ⟪u - v, w - v⟫_ℝ + θ * θ * (‖w - v‖ * ‖w - v‖)
⊢ 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

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
w₁ :
  ‖u - v‖ * ‖u - v‖ - 2 * (θ * ⟪u - v, w - v⟫_ℝ) + |θ| * ‖w - v‖ * (|θ| * ‖w - v‖) =
    ‖u - v‖ * ‖u - v‖ - 2 * θ * ⟪u - v, w - v⟫_ℝ + θ * θ * (‖w - v‖ * ‖w - v‖)
⊢ ‖u - v‖ * ‖u - v‖ - HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((re : (a : ℝ) → ℝ) (θ * ⟪u - v, w - v⟫_ℝ) : ℝ) +
      ‖θ‖ * ‖w - v‖ * (‖θ‖ * ‖w - v‖) =
    ‖u - v‖ * ‖u - v‖ - 2 * θ * ⟪u - v, w - v⟫_ℝ + θ * θ * (‖w - v‖ * ‖w - v‖)

Tactic:
change
              ‖u - v‖ * ‖u - v‖ - 2 * (θ * ⟪u - v, w - v⟫_ℝ) +
                absR θ * ‖w - v‖ * (absR θ * ‖w - v‖) =
              ‖u - v‖ * ‖u - v‖ - 2 * θ * ⟪u - v, w - v⟫_ℝ + θ * θ * (‖w - v‖ * ‖w - v‖)

Premises used: Norm.norm, Real, HMul.hMul, Inner.inner, abs, HSub.hSub
-- 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 - v‖ * ‖u - v‖ - 2 * (θ * ⟪u - v, w - v⟫_ℝ) + θ * ‖w - v‖ * (θ * ‖w - v‖) =
    ‖u - v‖ * ‖u - v‖ - 2 * θ * ⟪u - v, w - v⟫_ℝ + θ * θ * (‖w - v‖ * ‖w - v‖)
⊢ ‖u - v‖ * ‖u - v‖ - 2 * (θ * ⟪u - v, w - v⟫_ℝ) + |θ| * ‖w - v‖ * (|θ| * ‖w - v‖) =
    ‖u - v‖ * ‖u - v‖ - 2 * θ * ⟪u - v, w - v⟫_ℝ + θ * θ * (‖w - v‖ * ‖w - v‖)

Tactic:
rw [abs_of_pos hθ₁]

Premises used: abs_of_pos
-- 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 - v‖ * ‖u - v‖ - 2 * (θ * ⟪u - v, w - v⟫_ℝ) + θ * ‖w - v‖ * (θ * ‖w - v‖) =
    ‖u - v‖ * ‖u - v‖ - 2 * θ * ⟪u - v, w - v⟫_ℝ + θ * θ * (‖w - v‖ * ‖w - v‖)

Tactic:
ring
-- 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
⊢ HPow.hPow (β := ℕ) ‖u - v‖ 2 ≤
    HPow.hPow (β := ℕ) ‖u - v‖ 2 - 2 * θ * ⟪u - v, w - v⟫_ℝ + θ * θ * HPow.hPow (β := ℕ) ‖w - v‖ 2

Tactic:
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 _ _]
          _ = ‖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 * θ * ⟪u - v, w - v⟫_ℝ + θ * θ * ‖w - v‖ ^ 2 := by
            rw [@norm_sub_sq ℝ, inner_smul_right, norm_smul]
            simp only [sq]
            change
              ‖u - v‖ * ‖u - v‖ - 2 * (θ * ⟪u - v, w - v⟫_ℝ) +
                absR θ * ‖w - v‖ * (absR θ * ‖w - v‖) =
              ‖u - v‖ * ‖u - v‖ - 2 * θ * ⟪u - v, w - v⟫_ℝ + θ * θ * (‖w - v‖ * ‖w - v‖)
            rw [abs_of_pos hθ₁]; ring
-- 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 :
  HPow.hPow (β := ℕ) ‖u - v‖ 2 ≤
    HPow.hPow (β := ℕ) ‖u - v‖ 2 - 2 * θ * ⟪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‖ 2 + (θ * θ * HPow.hPow (β := ℕ) ‖w - v‖ 2 - 2 * θ * ⟪u - v, w - v⟫_ℝ)

Tactic:
abel
-- 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 :
  HPow.hPow (β := ℕ) ‖u - v‖ 2 ≤
    HPow.hPow (β := ℕ) ‖u - v‖ 2 - 2 * θ * ⟪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‖ 2 + (θ * θ * HPow.hPow (β := ℕ) ‖w - v‖ 2 - 2 * θ * ⟪u - v, w - v⟫_ℝ)

Tactic:
have eq₁ :
        ‖u - v‖ ^ 2 - 2 * θ * ⟪u - v, w - v⟫_ℝ + θ * θ * ‖w - v‖ ^ 2 =
          ‖u - v‖ ^ 2 + (θ * θ * ‖w - v‖ ^ 2 - 2 * θ * ⟪u - v, w - v⟫_ℝ) := by
        abel
-- 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 :
  HPow.hPow (β := ℕ) ‖u - v‖ 2 ≤
    HPow.hPow (β := ℕ) ‖u - v‖ 2 - 2 * θ * ⟪u - v, w - v⟫_ℝ + θ * θ * HPow.hPow (β := ℕ) ‖w - v‖ 2
eq₁ :
  HPow.hPow (β := ℕ) ‖u - v‖ 2 - 2 * θ * ⟪u - v, w - v⟫_ℝ + θ * θ * HPow.hPow (β := ℕ) ‖w - v‖ 2 =
    HPow.hPow (β := ℕ) ‖u - v‖ 2 + (θ * θ * HPow.hPow (β := ℕ) ‖w - v‖ 2 - 2 * θ * ⟪u - v, w - v⟫_ℝ)
⊢ 0 ≤ θ * θ * HPow.hPow (β := ℕ) ‖w - v‖ 2 - 2 * θ * ⟪u - v, w - v⟫_ℝ

Tactic:
rw [eq₁, le_add_iff_nonneg_right] at this

Premises used: le_add_iff_nonneg_right
-- 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 :
  HPow.hPow (β := ℕ) ‖u - v‖ 2 ≤
    HPow.hPow (β := ℕ) ‖u - v‖ 2 - 2 * θ * ⟪u - v, w - v⟫_ℝ + θ * θ * HPow.hPow (β := ℕ) ‖w - v‖ 2
eq₁ :
  HPow.hPow (β := ℕ) ‖u - v‖ 2 - 2 * θ * ⟪u - v, w - v⟫_ℝ + θ * θ * HPow.hPow (β := ℕ) ‖w - v‖ 2 =
    HPow.hPow (β := ℕ) ‖u - v‖ 2 + (θ * θ * HPow.hPow (β := ℕ) ‖w - v‖ 2 - 2 * θ * ⟪u - v, w - v⟫_ℝ)
this₁ : 0 ≤ θ * θ * HPow.hPow (β := ℕ) ‖w - v‖ 2 - 2 * θ * ⟪u - v, w - v⟫_ℝ
⊢ HPow.hPow (β := ℕ) ‖u - v‖ 2 - 2 * θ * ⟪u - v, w - v⟫_ℝ + θ * θ * HPow.hPow (β := ℕ) ‖w - v‖ 2 =
    HPow.hPow (β := ℕ) ‖u - v‖ 2 + (θ * θ * HPow.hPow (β := ℕ) ‖w - v‖ 2 - 2 * θ * ⟪u - v, w - v⟫_ℝ)

Tactic:
rw [eq₁, le_add_iff_nonneg_right] at this

Premises used: le_add_iff_nonneg_right
-- 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 : 0 ≤ θ * θ * HPow.hPow (β := ℕ) ‖w - v‖ 2 - 2 * θ * ⟪u - v, w - v⟫_ℝ
eq₁ :
  HPow.hPow (β := ℕ) ‖u - v‖ 2 - 2 * θ * ⟪u - v, w - v⟫_ℝ + θ * θ * HPow.hPow (β := ℕ) ‖w - v‖ 2 =
    HPow.hPow (β := ℕ) ‖u - v‖ 2 + (θ * θ * HPow.hPow (β := ℕ) ‖w - v‖ 2 - 2 * θ * ⟪u - v, w - v⟫_ℝ)
⊢ θ * θ * HPow.hPow (β := ℕ) ‖w - v‖ 2 - 2 * θ * ⟪u - v, w - v⟫_ℝ =
    θ * (θ * HPow.hPow (β := ℕ) ‖w - v‖ 2 - 2 * ⟪u - v, w - v⟫_ℝ)

Tactic:
ring
-- 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 : 0 ≤ θ * θ * HPow.hPow (β := ℕ) ‖w - v‖ 2 - 2 * θ * ⟪u - v, w - v⟫_ℝ
eq₁ :
  HPow.hPow (β := ℕ) ‖u - v‖ 2 - 2 * θ * ⟪u - v, w - v⟫_ℝ + θ * θ * HPow.hPow (β := ℕ) ‖w - v‖ 2 =
    HPow.hPow (β := ℕ) ‖u - v‖ 2 + (θ * θ * HPow.hPow (β := ℕ) ‖w - v‖ 2 - 2 * θ * ⟪u - v, w - v⟫_ℝ)
⊢ θ * θ * HPow.hPow (β := ℕ) ‖w - v‖ 2 - 2 * θ * ⟪u - v, w - v⟫_ℝ =
    θ * (θ * HPow.hPow (β := ℕ) ‖w - v‖ 2 - 2 * ⟪u - v, w - v⟫_ℝ)

Tactic:
have eq₂ :
        θ * θ * ‖w - v‖ ^ 2 - 2 * θ * ⟪u - v, w - v⟫_ℝ =
          θ * (θ * ‖w - v‖ ^ 2 - 2 * ⟪u - v, w - v⟫_ℝ) := by ring
-- 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 : 0 ≤ θ * θ * HPow.hPow (β := ℕ) ‖w - v‖ 2 - 2 * θ * ⟪u - v, w - v⟫_ℝ
eq₁ :
  HPow.hPow (β := ℕ) ‖u - v‖ 2 - 2 * θ * ⟪u - v, w - v⟫_ℝ + θ * θ * HPow.hPow (β := ℕ) ‖w - v‖ 2 =
    HPow.hPow (β := ℕ) ‖u - v‖ 2 + (θ * θ * HPow.hPow (β := ℕ) ‖w - v‖ 2 - 2 * θ * ⟪u - v, w - v⟫_ℝ)
eq₂ :
  θ * θ * HPow.hPow (β := ℕ) ‖w - v‖ 2 - 2 * θ * ⟪u - v, w - v⟫_ℝ =
    θ * (θ * HPow.hPow (β := ℕ) ‖w - v‖ 2 - 2 * ⟪u - v, w - v⟫_ℝ)
⊢ 0 ≤ θ * (θ * HPow.hPow (β := ℕ) ‖w - v‖ 2 - 2 * ⟪u - v, w - v⟫_ℝ)

Tactic:
rw [eq₂] at 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_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 : 0 ≤ θ * θ * HPow.hPow (β := ℕ) ‖w - v‖ 2 - 2 * θ * ⟪u - v, w - v⟫_ℝ
eq₁ :
  HPow.hPow (β := ℕ) ‖u - v‖ 2 - 2 * θ * ⟪u - v, w - v⟫_ℝ + θ * θ * HPow.hPow (β := ℕ) ‖w - v‖ 2 =
    HPow.hPow (β := ℕ) ‖u - v‖ 2 + (θ * θ * HPow.hPow (β := ℕ) ‖w - v‖ 2 - 2 * θ * ⟪u - v, w - v⟫_ℝ)
eq₂ :
  θ * θ * HPow.hPow (β := ℕ) ‖w - v‖ 2 - 2 * θ * ⟪u - v, w - v⟫_ℝ =
    θ * (θ * HPow.hPow (β := ℕ) ‖w - v‖ 2 - 2 * ⟪u - v, w - v⟫_ℝ)
this₁ : 0 ≤ θ * (θ * HPow.hPow (β := ℕ) ‖w - v‖ 2 - 2 * ⟪u - v, w - v⟫_ℝ)
⊢ HPow.hPow (β := ℕ) ‖u - v‖ 2 - 2 * θ * ⟪u - v, w - v⟫_ℝ + θ * θ * HPow.hPow (β := ℕ) ‖w - v‖ 2 =
    HPow.hPow (β := ℕ) ‖u - v‖ 2 + (θ * θ * HPow.hPow (β := ℕ) ‖w - v‖ 2 - 2 * θ * ⟪u - v, w - v⟫_ℝ)

Tactic:
rw [eq₂] at 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_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 : 0 ≤ θ * θ * HPow.hPow (β := ℕ) ‖w - v‖ 2 - 2 * θ * ⟪u - v, w - v⟫_ℝ
eq₁ :
  HPow.hPow (β := ℕ) ‖u - v‖ 2 - 2 * θ * ⟪u - v, w - v⟫_ℝ + θ * θ * HPow.hPow (β := ℕ) ‖w - v‖ 2 =
    HPow.hPow (β := ℕ) ‖u - v‖ 2 + (θ * θ * HPow.hPow (β := ℕ) ‖w - v‖ 2 - 2 * θ * ⟪u - v, w - v⟫_ℝ)
eq₂ :
  θ * θ * HPow.hPow (β := ℕ) ‖w - v‖ 2 - 2 * θ * ⟪u - v, w - v⟫_ℝ =
    θ * (θ * HPow.hPow (β := ℕ) ‖w - v‖ 2 - 2 * ⟪u - v, w - v⟫_ℝ)
this₁ : 0 ≤ θ * (θ * HPow.hPow (β := ℕ) ‖w - v‖ 2 - 2 * ⟪u - v, w - v⟫_ℝ)
eq₃ :
  HPow.hPow (β := ℕ) ‖u - v‖ 2 - 2 * θ * ⟪u - v, w - v⟫_ℝ + θ * θ * HPow.hPow (β := ℕ) ‖w - v‖ 2 =
    HPow.hPow (β := ℕ) ‖u - v‖ 2 + (θ * θ * HPow.hPow (β := ℕ) ‖w - v‖ 2 - 2 * θ * ⟪u - v, w - v⟫_ℝ)
⊢ θ * θ * HPow.hPow (β := ℕ) ‖w - v‖ 2 - 2 * θ * ⟪u - v, w - v⟫_ℝ =
    θ * (θ * HPow.hPow (β := ℕ) ‖w - v‖ 2 - 2 * ⟪u - v, w - v⟫_ℝ)

Tactic:
rw [eq₂] at 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_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 : 0 ≤ θ * (θ * HPow.hPow (β := ℕ) ‖w - v‖ 2 - 2 * ⟪u - v, w - v⟫_ℝ)
eq₁ :
  HPow.hPow (β := ℕ) ‖u - v‖ 2 - 2 * θ * ⟪u - v, w - v⟫_ℝ + θ * θ * HPow.hPow (β := ℕ) ‖w - v‖ 2 =
    HPow.hPow (β := ℕ) ‖u - v‖ 2 + (θ * θ * HPow.hPow (β := ℕ) ‖w - v‖ 2 - 2 * θ * ⟪u - v, w - v⟫_ℝ)
eq₂ :
  θ * θ * HPow.hPow (β := ℕ) ‖w - v‖ 2 - 2 * θ * ⟪u - v, w - v⟫_ℝ =
    θ * (θ * HPow.hPow (β := ℕ) ‖w - v‖ 2 - 2 * ⟪u - v, w - v⟫_ℝ)
⊢ 2 * p ≤ θ * q

Tactic:
le_of_sub_nonneg (nonneg_of_mul_nonneg_right this hθ₁)

Premises used: nonneg_of_mul_nonneg_right, le_of_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_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 : 0 ≤ θ * (θ * HPow.hPow (β := ℕ) ‖w - v‖ 2 - 2 * ⟪u - v, w - v⟫_ℝ)
eq₁ :
  HPow.hPow (β := ℕ) ‖u - v‖ 2 - 2 * θ * ⟪u - v, w - v⟫_ℝ + θ * θ * HPow.hPow (β := ℕ) ‖w - v‖ 2 =
    HPow.hPow (β := ℕ) ‖u - v‖ 2 + (θ * θ * HPow.hPow (β := ℕ) ‖w - v‖ 2 - 2 * θ * ⟪u - v, w - v⟫_ℝ)
eq₂ :
  θ * θ * HPow.hPow (β := ℕ) ‖w - v‖ 2 - 2 * θ * ⟪u - v, w - v⟫_ℝ =
    θ * (θ * HPow.hPow (β := ℕ) ‖w - v‖ 2 - 2 * ⟪u - v, w - v⟫_ℝ)
⊢ 2 * p ≤ θ * q

Tactic:
exact le_of_sub_nonneg (nonneg_of_mul_nonneg_right this hθ₁)

Premises used: nonneg_of_mul_nonneg_right, le_of_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), 2 * p ≤ θ * q

Tactic:
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 _ _]
          _ = ‖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 * θ * ⟪u - v, w - v⟫_ℝ + θ * θ * ‖w - v‖ ^ 2 := by
            rw [@norm_sub_sq ℝ, inner_smul_right, norm_smul]
            simp only [sq]
            change
              ‖u - v‖ * ‖u - v‖ - 2 * (θ * ⟪u - v, w - v⟫_ℝ) +
                absR θ * ‖w - v‖ * (absR θ * ‖w - v‖) =
              ‖u - v‖ * ‖u - v‖ - 2 * θ * ⟪u - v, w - v⟫_ℝ + θ * θ * (‖w - v‖ * ‖w - v‖)
            rw [abs_of_pos hθ₁]; ring
      have eq₁ :
        ‖u - v‖ ^ 2 - 2 * θ * ⟪u - v, w - v⟫_ℝ + θ * θ * ‖w - v‖ ^ 2 =
          ‖u - v‖ ^ 2 + (θ * θ * ‖w - v‖ ^ 2 - 2 * θ * ⟪u - v, w - v⟫_ℝ) := by
        abel
      rw [eq₁, le_add_iff_nonneg_right] at this
      have eq₂ :
        θ * θ * ‖w - v‖ ^ 2 - 2 * θ * ⟪u - v, w - v⟫_ℝ =
          θ * (θ * ‖w - v‖ ^ 2 - 2 * ⟪u - v, w - v⟫_ℝ) := by ring
      rw [eq₂] at this
      exact le_of_sub_nonneg (nonneg_of_mul_nonneg_right this hθ₁)
-- 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‖
this : ∀ (θ : ℝ) (hθ₁ : 0 < θ) (hθ₂ : θ ≤ 1), 2 * p ≤ θ * q
pos : ∀ (hq : q = 0), ⟪u - v, w - v⟫_ℝ ≤ 0
neg : ∀ (hq : ¬q = 0), ⟪u - v, w - v⟫_ℝ ≤ 0
⊢ ⟪u - v, w - v⟫_ℝ ≤ 0

Tactic:
by_cases hq : q = 0
-- 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‖
this : ∀ (θ : ℝ) (hθ₁ : 0 < θ) (hθ₂ : θ ≤ 1), 2 * p ≤ θ * q
hq : q = 0
⊢ ∀ (θ : ℝ) (hθ₁ : 0 < θ) (hθ₂ : θ ≤ 1), 2 * p ≤ θ * 0

Tactic:
rw [hq] at 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_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‖
this : ∀ (θ : ℝ) (hθ₁ : 0 < θ) (hθ₂ : θ ≤ 1), 2 * p ≤ θ * q
hq : q = 0
this₁ : ∀ (θ : ℝ) (hθ₁ : 0 < θ) (hθ₂ : θ ≤ 1), 2 * p ≤ θ * 0
⊢ q = 0

Tactic:
rw [hq] at 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_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‖
this : ∀ (θ : ℝ) (hθ₁ : 0 < θ) (hθ₂ : θ ≤ 1), 2 * p ≤ θ * 0
hq : q = 0
⊢ LT.lt (α := ℝ) 0 1

Tactic:
simp
-- 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‖
this : ∀ (θ : ℝ) (hθ₁ : 0 < θ) (hθ₂ : θ ≤ 1), 2 * p ≤ θ * 0
hq : q = 0
⊢ LE.le (α := ℝ) 1 1

Tactic:
simp
-- 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‖
this : ∀ (θ : ℝ) (hθ₁ : 0 < θ) (hθ₂ : θ ≤ 1), 2 * p ≤ θ * 0
hq : q = 0
⊢ 2 * p ≤ HMul.hMul (α := ℝ) 1 0

Tactic:
have := this (1 : ℝ) (by simp) (by simp)