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_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_2 : ∀ (θ : ℝ) (hθ₁ : 0 < θ) (hθ₂ : θ ≤ 1), 2 * p ≤ θ * 0
hq : q = 0
this : 2 * p ≤ HMul.hMul (α := ℝ) 1 0
linarith : 0 < p → 2 * p - HMul.hMul (α := ℝ) 1 0 + 2 * (0 - p) = 0
linarith₁ : 0 < p → GT.gt (α := ℝ) 2 0
⊢ p ≤ 0

Tactic:
linarith
-- 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
⊢ p ≤ 0

Tactic:
have : p ≤ 0 := by
        have := this (1 : ℝ) (by simp) (by simp)
        linarith
-- 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_2 : ∀ (θ : ℝ) (hθ₁ : 0 < θ) (hθ₂ : θ ≤ 1), 2 * p ≤ θ * 0
hq : q = 0
this : p ≤ 0
⊢ ⟪u - v, w - v⟫_ℝ ≤ 0

Tactic:
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_2 : ∀ (θ : ℝ) (hθ₁ : 0 < θ) (hθ₂ : θ ≤ 1), 2 * p ≤ θ * 0
hq : q = 0
this : p ≤ 0
⊢ ⟪u - v, w - v⟫_ℝ ≤ 0

Tactic:
exact 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
⊢ 0 < q

Tactic:
have q_pos : 0 < q := lt_of_le_of_ne (sq_nonneg _) fun h ↦ hq h.symm
-- 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
q_pos : 0 < q
neg : ∀ (hp : ¬⟪u - v, w - v⟫_ℝ ≤ 0), False
⊢ ⟪u - v, w - v⟫_ℝ ≤ 0

Tactic:
by_contra hp
-- 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
q_pos : 0 < q
hp : ¬⟪u - v, w - v⟫_ℝ ≤ 0
⊢ 0 < ⟪u - v, w - v⟫_ℝ

Tactic:
rw [not_le] at hp

Premises used: not_le
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Minimal
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
K : Set F
h : Convex ℝ K
u v : F
hv : v ∈ K
this_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
q_pos : 0 < q
hp : 0 < ⟪u - v, w - v⟫_ℝ
θ : ℝ := min 1 (p / q)
⊢ θ * q ≤ p

Tactic:
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
-- 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
q_pos : 0 < q
hp : 0 < ⟪u - v, w - v⟫_ℝ
θ : ℝ := min 1 (p / q)
eq₁ : θ * q ≤ p
⊢ 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 ≤ θ * q
hq : ¬q = 0
q_pos : 0 < q
hp : 0 < ⟪u - v, w - v⟫_ℝ
θ : ℝ := min 1 (p / q)
eq₁ : θ * q ≤ p
⊢ θ ≤ 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 ≤ θ * q
hq : ¬q = 0
q_pos : 0 < q
hp : 0 < ⟪u - v, w - v⟫_ℝ
θ : ℝ := min 1 (p / q)
eq₁ : θ * q ≤ p
⊢ 2 * p ≤ θ * q

Tactic:
exact this θ (lt_min (by simp) (div_pos hp q_pos)) (by simp [θ])

Premises used: lt_min, div_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_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
q_pos : 0 < q
hp : 0 < ⟪u - v, w - v⟫_ℝ
θ : ℝ := min 1 (p / q)
eq₁ : θ * q ≤ p
⊢ 2 * p ≤ p

Tactic:
have : 2 * p ≤ p :=
        calc
          2 * p ≤ θ * q := by
            exact this θ (lt_min (by simp) (div_pos hp q_pos)) (by simp [θ])
          _ ≤ p := eq₁
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Minimal
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
K : Set F
h : Convex ℝ K
u v : F
hv : v ∈ K
this_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_2 : ∀ (θ : ℝ) (hθ₁ : 0 < θ) (hθ₂ : θ ≤ 1), 2 * p ≤ θ * q
hq : ¬q = 0
q_pos : 0 < q
hp : 0 < ⟪u - v, w - v⟫_ℝ
θ : ℝ := min 1 (p / q)
eq₁ : θ * q ≤ p
this : 2 * p ≤ p
linarith : 0 - ⟪u - v, w - v⟫_ℝ + (2 * p - p) = 0
⊢ False

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

Tactic:
apply le_antisymm

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

Tactic:
apply le_ciInf

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

Tactic:
apply nonneg_le_nonneg_of_sq_le_sq (norm_nonneg _)

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

Tactic:
have := h w w.2
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Minimal
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
K : Set F
h_1 : Convex ℝ K
u v : F
hv : v ∈ K
this_1 : Nonempty.{u_3 + 1} (↑K : Type u_3) := ⋯
h : ∀ w ∈ K, ⟪u - v, w - v⟫_ℝ ≤ 0
w : (↑K : Type u_3)
this : ⟪u - v, (↑w : F) - v⟫_ℝ ≤ 0
linarith :
  ‖u - v‖ * ‖u - v‖ - 2 * ⟪u - v, (↑w : F) - v⟫_ℝ < ‖u - v‖ * ‖u - v‖ →
    2 * (⟪u - v, (↑w : F) - v⟫_ℝ - 0) + (‖u - v‖ * ‖u - v‖ - 2 * ⟪u - v, (↑w : F) - v⟫_ℝ - ‖u - v‖ * ‖u - v‖) = 0
linarith₁ : ‖u - v‖ * ‖u - v‖ - 2 * ⟪u - v, (↑w : F) - v⟫_ℝ < ‖u - v‖ * ‖u - v‖ → GT.gt (α := ℝ) 2 0
⊢ ‖u - v‖ * ‖u - v‖ ≤ ‖u - v‖ * ‖u - v‖ - 2 * ⟪u - v, (↑w : F) - v⟫_ℝ

Tactic:
linarith
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Minimal
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
K : Set F
h_1 : Convex ℝ K
u v : F
hv : v ∈ K
this_1 : Nonempty.{u_3 + 1} (↑K : Type u_3) := ⋯
h : ∀ w ∈ K, ⟪u - v, w - v⟫_ℝ ≤ 0
w : (↑K : Type u_3)
this : ⟪u - v, (↑w : F) - v⟫_ℝ ≤ 0
rw :
  ‖u - v‖ * ‖u - v‖ - 2 * ⟪u - v, (↑w : F) - v⟫_ℝ ≤
    ‖u - v‖ * ‖u - v‖ - 2 * ⟪u - v, (↑w : F) - v⟫_ℝ + HPow.hPow (β := ℕ) ‖(↑w : F) - v‖ 2
⊢ ‖u - v‖ * ‖u - v‖ - 2 * ⟪u - v, (↑w : F) - v⟫_ℝ ≤
    HPow.hPow (β := ℕ) ‖u - v‖ 2 - 2 * ⟪u - v, (↑w : F) - v⟫_ℝ + HPow.hPow (β := ℕ) ‖(↑w : F) - v‖ 2

Tactic:
rw [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_1 : Convex ℝ K
u v : F
hv : v ∈ K
this_1 : Nonempty.{u_3 + 1} (↑K : Type u_3) := ⋯
h : ∀ w ∈ K, ⟪u - v, w - v⟫_ℝ ≤ 0
w : (↑K : Type u_3)
this : ⟪u - v, (↑w : F) - v⟫_ℝ ≤ 0
⊢ ‖u - v‖ * ‖u - v‖ - 2 * ⟪u - v, (↑w : F) - v⟫_ℝ ≤
    ‖u - v‖ * ‖u - v‖ - 2 * ⟪u - v, (↑w : F) - v⟫_ℝ + HPow.hPow (β := ℕ) ‖(↑w : F) - v‖ 2

Tactic:
le_add_of_nonneg_right ?_

Premises used: le_add_of_nonneg_right
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Minimal
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
K : Set F
h_1 : Convex ℝ K
u v : F
hv : v ∈ K
this_1 : Nonempty.{u_3 + 1} (↑K : Type u_3) := ⋯
h : ∀ w ∈ K, ⟪u - v, w - v⟫_ℝ ≤ 0
w : (↑K : Type u_3)
this : ⟪u - v, (↑w : F) - v⟫_ℝ ≤ 0
refine : 0 ≤ HPow.hPow (β := ℕ) ‖(↑w : F) - v‖ 2
⊢ ‖u - v‖ * ‖u - v‖ - 2 * ⟪u - v, (↑w : F) - v⟫_ℝ ≤
    ‖u - v‖ * ‖u - v‖ - 2 * ⟪u - v, (↑w : F) - v⟫_ℝ + HPow.hPow (β := ℕ) ‖(↑w : F) - v‖ 2

Tactic:
refine le_add_of_nonneg_right ?_

Premises used: le_add_of_nonneg_right
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Minimal
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
K : Set F
h_1 : Convex ℝ K
u v : F
hv : v ∈ K
this_1 : Nonempty.{u_3 + 1} (↑K : Type u_3) := ⋯
h : ∀ w ∈ K, ⟪u - v, w - v⟫_ℝ ≤ 0
w : (↑K : Type u_3)
this : ⟪u - v, (↑w : F) - v⟫_ℝ ≤ 0
⊢ 0 ≤ HPow.hPow (β := ℕ) ‖(↑w : F) - v‖ 2

Tactic:
sq_nonneg _

Premises used: sq_nonneg
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Minimal
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
K : Set F
h_1 : Convex ℝ K
u v : F
hv : v ∈ K
this_1 : Nonempty.{u_3 + 1} (↑K : Type u_3) := ⋯
h : ∀ w ∈ K, ⟪u - v, w - v⟫_ℝ ≤ 0
w : (↑K : Type u_3)
this : ⟪u - v, (↑w : F) - v⟫_ℝ ≤ 0
⊢ 0 ≤ HPow.hPow (β := ℕ) ‖(↑w : F) - v‖ 2

Tactic:
exact sq_nonneg _

Premises used: sq_nonneg
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Minimal
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
K : Set F
h_1 : Convex ℝ K
u v : F
hv : v ∈ K
this_1 : Nonempty.{u_3 + 1} (↑K : Type u_3) := ⋯
h : ∀ w ∈ K, ⟪u - v, w - v⟫_ℝ ≤ 0
w : (↑K : Type u_3)
this : ⟪u - v, (↑w : F) - v⟫_ℝ ≤ 0
⊢ HPow.hPow (β := ℕ) ‖u - v‖ 2 - 2 * ⟪u - v, (↑w : F) - v⟫_ℝ + HPow.hPow (β := ℕ) ‖(↑w : F) - v‖ 2 =
    HPow.hPow (β := ℕ) ‖u - v - ((↑w : F) - v)‖ 2

Tactic:
(@norm_sub_sq ℝ _ _ _ _ _ _).symm

Premises used: norm_sub_sq, Eq.symm
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Minimal
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
K : Set F
h_1 : Convex ℝ K
u v : F
hv : v ∈ K
this_1 : Nonempty.{u_3 + 1} (↑K : Type u_3) := ⋯
h : ∀ w ∈ K, ⟪u - v, w - v⟫_ℝ ≤ 0
w : (↑K : Type u_3)
this : ⟪u - v, (↑w : F) - v⟫_ℝ ≤ 0
⊢ u - v - ((↑w : F) - v) = u - (↑w : F)

Tactic:
abel
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Minimal
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
K : Set F
h_1 : Convex ℝ K
u v : F
hv : v ∈ K
this_1 : Nonempty.{u_3 + 1} (↑K : Type u_3) := ⋯
h : ∀ w ∈ K, ⟪u - v, w - v⟫_ℝ ≤ 0
w : (↑K : Type u_3)
this : ⟪u - v, (↑w : F) - v⟫_ℝ ≤ 0
⊢ u - v - ((↑w : F) - v) = u - (↑w : F)

Tactic:
have : u - v - (w - v) = u - w := by abel
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Minimal
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
K : Set F
h_1 : Convex ℝ K
u v : F
hv : v ∈ K
this_1 : Nonempty.{u_3 + 1} (↑K : Type u_3) := ⋯
h : ∀ w ∈ K, ⟪u - v, w - v⟫_ℝ ≤ 0
w : (↑K : Type u_3)
this_2 : ⟪u - v, (↑w : F) - v⟫_ℝ ≤ 0
this : u - v - ((↑w : F) - v) = u - (↑w : F)
rw : HPow.hPow (β := ℕ) ‖u - (↑w : F)‖ 2 = ‖u - (↑w : F)‖ * ‖u - (↑w : F)‖
rw₁ rw₂ : ‖u - (↑w : F)‖ * ‖u - (↑w : F)‖ = ‖u - (↑w : F)‖ * ‖u - (↑w : F)‖
⊢ HPow.hPow (β := ℕ) ‖u - v - ((↑w : F) - v)‖ 2 = ‖u - (↑w : F)‖ * ‖u - (↑w : F)‖

Tactic:
rw [this, 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_1 : Convex ℝ K
u v : F
hv : v ∈ K
this_1 : Nonempty.{u_3 + 1} (↑K : Type u_3) := ⋯
h : ∀ w ∈ K, ⟪u - v, w - v⟫_ℝ ≤ 0
w : (↑K : Type u_3)
this : ⟪u - v, (↑w : F) - v⟫_ℝ ≤ 0
w₁ : ‖u - v‖ * ‖u - v‖ ≤ ‖u - v‖ * ‖u - v‖ - 2 * ⟪u - v, (↑w : F) - v⟫_ℝ
w₂ :
  ‖u - v‖ * ‖u - v‖ - 2 * ⟪u - v, (↑w : F) - v⟫_ℝ ≤
    HPow.hPow (β := ℕ) ‖u - v‖ 2 - 2 * ⟪u - v, (↑w : F) - v⟫_ℝ + HPow.hPow (β := ℕ) ‖(↑w : F) - v‖ 2
w₃ : HPow.hPow (β := ℕ) ‖u - v - ((↑w : F) - v)‖ 2 = ‖u - (↑w : F)‖ * ‖u - (↑w : F)‖
⊢ ‖u - v‖ * ‖u - v‖ ≤ ‖u - (↑w : F)‖ * ‖u - (↑w : F)‖

Tactic:
calc
        ‖u - v‖ * ‖u - v‖ ≤ ‖u - v‖ * ‖u - v‖ - 2 * ⟪u - v, w - v⟫_ℝ := by linarith
        _ ≤ ‖u - v‖ ^ 2 - 2 * ⟪u - v, w - v⟫_ℝ + ‖w - 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]

Premises used: norm_sub_sq, HSub.hSub, Eq.symm, Subtype.val
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Minimal
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
K : Set F
h_1 : Convex ℝ K
u v : F
hv : v ∈ K
this : Nonempty.{u_3 + 1} (↑K : Type u_3) := ⋯
h : ∀ w ∈ K, ⟪u - v, w - v⟫_ℝ ≤ 0
mpr :
  LE.le (α := ℝ) (⨅ (w : (↑K : Type u_3)), ‖u - (↑w : F)‖)
    ((fun (w : (↑K : Type u_3)) ↦ ‖u - (↑w : F)‖) (Subtype.mk (p := fun (x : F) ↦ x ∈ K) v hv))
⊢ ⨅ (w : (↑K : Type u_3)), ‖u - (↑w : F)‖ ≤ ‖u - v‖

Tactic:
change ⨅ w : K, ‖u - w‖ ≤ (fun w : K => ‖u - w‖) ⟨v, hv⟩

Premises used: Norm.norm, HSub.hSub, Subtype.mk, Subtype.val
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Minimal
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
K : Set F
h_1 : Convex ℝ K
u v : F
hv : v ∈ K
this : Nonempty.{u_3 + 1} (↑K : Type u_3) := ⋯
h : ∀ w ∈ K, ⟪u - v, w - v⟫_ℝ ≤ 0
mpr : BddBelow (α := ℝ) (Set.range fun (w : (↑K : Type u_3)) ↦ ‖u - (↑w : F)‖)
⊢ LE.le (α := ℝ) (⨅ (w : (↑K : Type u_3)), ‖u - (↑w : F)‖)
    ((fun (w : (↑K : Type u_3)) ↦ ‖u - (↑w : F)‖) (Subtype.mk (p := fun (x : F) ↦ x ∈ K) v hv))

Tactic:
apply ciInf_le

Premises used: ciInf_le
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Minimal
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
K : Set F
h_1 : Convex ℝ K
u v : F
hv : v ∈ K
this : Nonempty.{u_3 + 1} (↑K : Type u_3) := ⋯
h : ∀ w ∈ K, ⟪u - v, w - v⟫_ℝ ≤ 0
h₁ : Membership.mem (γ := Set ℝ) (lowerBounds (Set.range fun (w : (↑K : Type u_3)) ↦ ‖u - (↑w : F)‖)) 0
⊢ BddBelow (α := ℝ) (Set.range fun (w : (↑K : Type u_3)) ↦ ‖u - (↑w : F)‖)

Tactic:
use 0
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Minimal
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
K : Set F
h_1 : Convex ℝ K
u v : F
hv : v ∈ K
this : Nonempty.{u_3 + 1} (↑K : Type u_3) := ⋯
h : ∀ w ∈ K, ⟪u - v, w - v⟫_ℝ ≤ 0
z : (↑K : Type u_3)
⊢ LE.le (α := ℝ) 0 ((fun (w : (↑K : Type u_3)) ↦ ‖u - (↑w : F)‖) z)

Tactic:
norm_nonneg _

Premises used: norm_nonneg
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Minimal
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
K : Set F
h_1 : Convex ℝ K
u v : F
hv : v ∈ K
this : Nonempty.{u_3 + 1} (↑K : Type u_3) := ⋯
h : ∀ w ∈ K, ⟪u - v, w - v⟫_ℝ ≤ 0
z : (↑K : Type u_3)
⊢ LE.le (α := ℝ) 0 ((fun (w : (↑K : Type u_3)) ↦ ‖u - (↑w : F)‖) z)

Tactic:
exact norm_nonneg _

Premises used: norm_nonneg
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Minimal
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
h : IsComplete (↑K : Set E)
this : InnerProductSpace ℝ E := rclikeToReal 𝕜 E
K' : Submodule ℝ E := restrictScalars ℝ K
⊢ ∀ (u : E), ∃ v ∈ K, ‖u - v‖ = ⨅ (w : (↑(↑K : Set E) : Type u_2)), ‖u - (↑w : E)‖

Tactic:
exists_norm_eq_iInf_of_complete_convex ⟨0, K'.zero_mem⟩ h K'.convex

Premises used: Submodule.convex, Submodule.zero_mem, Exists.intro, exists_norm_eq_iInf_of_complete_convex, OfNat.ofNat
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Minimal
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
h : IsComplete (↑K : Set E)
this : InnerProductSpace ℝ E := rclikeToReal 𝕜 E
K' : Submodule ℝ E := restrictScalars ℝ K
⊢ ∀ (u : E), ∃ v ∈ K, ‖u - v‖ = ⨅ (w : (↑(↑K : Set E) : Type u_2)), ‖u - (↑w : E)‖

Tactic:
exact exists_norm_eq_iInf_of_complete_convex ⟨0, K'.zero_mem⟩ h K'.convex

Premises used: Submodule.convex, Submodule.zero_mem, Exists.intro, exists_norm_eq_iInf_of_complete_convex, OfNat.ofNat
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Minimal
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
K : Submodule ℝ F
u v : F
hv : v ∈ K
h : ‖u - v‖ = ⨅ (w : (↑(↑K : Set F) : Type u_3)), ‖u - (↑w : F)‖
h₁ : Convex ℝ (↑K : Set F)
hv₁ : v ∈ (↑K : Set F)
⊢ ∀ w ∈ K, ⟪u - v, w - v⟫_ℝ ≤ 0

Tactic:
rwa [norm_eq_iInf_iff_real_inner_le_zero] at h

Premises used: norm_eq_iInf_iff_real_inner_le_zero
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Minimal
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
K : Submodule ℝ F
u v : F
hv : v ∈ K
h : ‖u - v‖ = ⨅ (w : (↑(↑K : Set F) : Type u_3)), ‖u - (↑w : F)‖
⊢ Convex ℝ (↑K : Set F)

Tactic:
K.convex

Premises used: Submodule.convex
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Minimal
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
K : Submodule ℝ F
u v : F
hv : v ∈ K
h : ‖u - v‖ = ⨅ (w : (↑(↑K : Set F) : Type u_3)), ‖u - (↑w : F)‖
⊢ v ∈ (↑K : Set F)

Tactic:
hv
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Minimal
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
K : Submodule ℝ F
u v : F
hv : v ∈ K
h : ‖u - v‖ = ⨅ (w : (↑(↑K : Set F) : Type u_3)), ‖u - (↑w : F)‖
⊢ Convex ℝ (↑K : Set F)

Tactic:
exacts [K.convex, hv]

Premises used: Submodule.convex
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Minimal
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
K : Submodule ℝ F
u v : F
hv : v ∈ K
h : ‖u - v‖ = ⨅ (w : (↑(↑K : Set F) : Type u_3)), ‖u - (↑w : F)‖
⊢ ∀ w ∈ K, ⟪u - v, w - v⟫_ℝ ≤ 0

Tactic:
have h : ∀ w ∈ K, ⟪u - v, w - v⟫_ℝ ≤ 0 := by
        rwa [norm_eq_iInf_iff_real_inner_le_zero] at h
        exacts [K.convex, hv]
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Minimal
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
K : Submodule ℝ F
u v : F
hv : v ∈ K
h_1 : ‖u - v‖ = ⨅ (w : (↑(↑K : Set F) : Type u_3)), ‖u - (↑w : F)‖
h : ∀ w ∈ K, ⟪u - v, w - v⟫_ℝ ≤ 0
w : F
hw : w ∈ K
w' : F := w + v
⊢ w' ∈ K

Tactic:
have : w' ∈ K := Submodule.add_mem _ hw hv
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Minimal
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
K : Submodule ℝ F
u v : F
hv : v ∈ K
h_1 : ‖u - v‖ = ⨅ (w : (↑(↑K : Set F) : Type u_3)), ‖u - (↑w : F)‖
h : ∀ w ∈ K, ⟪u - v, w - v⟫_ℝ ≤ 0
w : F
hw : w ∈ K
w' : F := w + v
this : w' ∈ K
⊢ ⟪u - v, w' - v⟫_ℝ ≤ 0

Tactic:
have h₁ := h w' this
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Minimal
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
K : Submodule ℝ F
u v : F
hv : v ∈ K
h_1 : ‖u - v‖ = ⨅ (w : (↑(↑K : Set F) : Type u_3)), ‖u - (↑w : F)‖
h : ∀ w ∈ K, ⟪u - v, w - v⟫_ℝ ≤ 0
w : F
hw : w ∈ K
w' : F := w + v
this : w' ∈ K
h₁ : ⟪u - v, w' - v⟫_ℝ ≤ 0
⊢ w' - v = w

Tactic:
simp only [w', add_neg_cancel_right, sub_eq_add_neg]

Premises used: add_neg_cancel_right, sub_eq_add_neg