awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Minimal (goal)
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 + (1 - θ) • v ∈ K
have hw₁ : 0 ≤ θ
Tactic: apply h hw hv
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Minimal (goal)
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
K : Set F
h : Convex ℝ K
u v : F
hv : v ∈ K
this : Nonempty.{u_3 + 1} (↑K : Type u_3) := ⋯
eq : ‖u - v‖ = ⨅ (w : (↑K : Type u_3)), ‖u - (↑w : F)‖
w : F
hw : w ∈ K
δ : ℝ := ⨅ (w : (↑K : Type u_3)), ‖u - (↑w : F)‖
p : ℝ := ⟪u - v, w - v⟫_ℝ
q : ℝ := HPow.hPow (β := ℕ) ‖w - v‖ 2
δ_le : ∀ (w : (↑K : Type u_3)), δ ≤ ‖u - (↑w : F)‖
δ_le' : ∀ (w : F) (hw : w ∈ K), δ ≤ ‖u - w‖
θ : ℝ
hθ₁ : 0 < θ
hθ₂ : θ ≤ 1
hw₁ : 0 ≤ θ
⊢ θ • w + (1 - θ) • v ∈ K
have hw₂ : 0 ≤ 1 - θ
Tactic: apply h hw hv
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Minimal (goal)
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
K : Set F
h : Convex ℝ K
u v : F
hv : v ∈ K
this : Nonempty.{u_3 + 1} (↑K : Type u_3) := ⋯
eq : ‖u - v‖ = ⨅ (w : (↑K : Type u_3)), ‖u - (↑w : F)‖
w : F
hw : w ∈ K
δ : ℝ := ⨅ (w : (↑K : Type u_3)), ‖u - (↑w : F)‖
p : ℝ := ⟪u - v, w - v⟫_ℝ
q : ℝ := HPow.hPow (β := ℕ) ‖w - v‖ 2
δ_le : ∀ (w : (↑K : Type u_3)), δ ≤ ‖u - (↑w : F)‖
δ_le' : ∀ (w : F) (hw : w ∈ K), δ ≤ ‖u - w‖
θ : ℝ
hθ₁ : 0 < θ
hθ₂ : θ ≤ 1
hw₁ : 0 ≤ θ
hw₂ : 0 ≤ 1 - θ
⊢ θ • w + (1 - θ) • v ∈ K
have hw₃ : θ + (1 - θ) = 1
Tactic: apply h hw hv
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Minimal (goal)
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
K : Set F
h : Convex ℝ K
u v : F
hv : v ∈ K
this : Nonempty.{u_3 + 1} (↑K : Type u_3) := ⋯
eq : ‖u - v‖ = ⨅ (w : (↑K : Type u_3)), ‖u - (↑w : F)‖
w : F
hw : w ∈ K
δ : ℝ := ⨅ (w : (↑K : Type u_3)), ‖u - (↑w : F)‖
p : ℝ := ⟪u - v, w - v⟫_ℝ
q : ℝ := HPow.hPow (β := ℕ) ‖w - v‖ 2
δ_le : ∀ (w : (↑K : Type u_3)), δ ≤ ‖u - (↑w : F)‖
δ_le' : ∀ (w : F) (hw : w ∈ K), δ ≤ ‖u - w‖
θ : ℝ
hθ₁ : 0 < θ
hθ₂ : θ ≤ 1
⊢ u - (θ • w + (1 - θ) • v) = u - v - θ • (w - v)
have rw : u - (θ • w + (v - θ • v)) = u - v - (θ • w - θ • v)
Tactic: rw [smul_sub, sub_smul, one_smul]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Minimal (hypothesis)
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 - (θ • w + (1 - θ) • v)‖ 2 = HPow.hPow (β := ℕ) ‖u - v - θ • (w - v)‖ 2
have this₁ : u - (θ • w + (1 - θ) • v) = u - v - θ • (w - v)
Tactic: have : u - (θ • w + (1 - θ) • v) = u - v - θ • (w - v) := by
              rw [smul_sub, sub_smul, one_smul]
              simp only [sub_eq_add_neg, add_comm, add_left_comm, add_assoc, neg_add_rev]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Minimal (goal)
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
K : Set F
h : Convex ℝ K
u v : F
hv : v ∈ K
this_1 : Nonempty.{u_3 + 1} (↑K : Type u_3) := ⋯
eq : ‖u - v‖ = ⨅ (w : (↑K : Type u_3)), ‖u - (↑w : F)‖
w : F
hw : w ∈ K
δ : ℝ := ⨅ (w : (↑K : Type u_3)), ‖u - (↑w : F)‖
p : ℝ := ⟪u - v, w - v⟫_ℝ
q : ℝ := HPow.hPow (β := ℕ) ‖w - v‖ 2
δ_le : ∀ (w : (↑K : Type u_3)), δ ≤ ‖u - (↑w : F)‖
δ_le' : ∀ (w : F) (hw : w ∈ K), δ ≤ ‖u - w‖
θ : ℝ
hθ₁ : 0 < θ
hθ₂ : θ ≤ 1
this : u - (θ • w + (1 - θ) • v) = u - v - θ • (w - v)
⊢ HPow.hPow (β := ℕ) ‖u - (θ • w + (1 - θ) • v)‖ 2 = HPow.hPow (β := ℕ) ‖u - v - θ • (w - v)‖ 2
have rw : HPow.hPow (β := ℕ) ‖u - v - θ • (w - v)‖ 2 = HPow.hPow (β := ℕ) ‖u - v - θ • (w - v)‖ 2
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Minimal (goal)
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 - θ • (w - v)‖ 2 =
    HPow.hPow (β := ℕ) ‖u - v‖ 2 - 2 * θ * ⟪u - v, w - v⟫_ℝ + θ * θ * HPow.hPow (β := ℕ) ‖w - v‖ 2
have rw : HPow.hPow (β := ℕ) ‖u - v‖ 2 - HMul.hMul (α := ℝ) (β := ℝ) (2 : ℝ) ((re : (a : ℝ) → ℝ) (θ * ⟪u - v, w - v⟫_ℝ) : ℝ) +
    HPow.hPow (β := ℕ) (‖θ‖ * ‖w - v‖) 2 =
  HPow.hPow (β := ℕ) ‖u - v‖ 2 - 2 * θ * ⟪u - v, w - v⟫_ℝ + θ * θ * HPow.hPow (β := ℕ) ‖w - v‖ 2
Tactic: rw [@norm_sub_sq ℝ, inner_smul_right, norm_smul]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Minimal (goal)
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 - 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
have 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‖)
Tactic: simp only [sq]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Minimal (goal)
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‖ - 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‖)
have 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‖)
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‖)
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Minimal (goal)
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‖)
have 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‖)
Tactic: rw [abs_of_pos hθ₁]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Minimal (hypothesis)
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
have this₁ : 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
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Minimal (hypothesis)
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
⊢ 2 * p ≤ θ * q
have 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⟫_ℝ)
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
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Minimal (hypothesis)
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⟫_ℝ)
⊢ 2 * p ≤ θ * q
have this₁ : 0 ≤ θ * θ * HPow.hPow (β := ℕ) ‖w - v‖ 2 - 2 * θ * ⟪u - v, w - v⟫_ℝ
Tactic: rw [eq₁, le_add_iff_nonneg_right] at this
Cleared hypotheses: this, eq₁
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Minimal (hypothesis)
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⟫_ℝ)
⊢ 2 * p ≤ θ * q
have eq₂ : θ * θ * 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
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Minimal (hypothesis)
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
have this₁ : 0 ≤ θ * (θ * HPow.hPow (β := ℕ) ‖w - v‖ 2 - 2 * ⟪u - v, w - v⟫_ℝ)
Tactic: rw [eq₂] at this
Cleared hypotheses: this, eq₁, eq₂
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Minimal (hypothesis)
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‖
⊢ ⟪u - v, w - v⟫_ℝ ≤ 0
have this₁ : ∀ (θ : ℝ) (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θ₁)
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Minimal (goal)
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
⊢ ⟪u - v, w - v⟫_ℝ ≤ 0
have pos : ∀ (hq : q = 0), ⟪u - v, w - v⟫_ℝ ≤ 0
Tactic: by_cases hq : q = 0
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Minimal (goal)
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
⊢ ⟪u - v, w - v⟫_ℝ ≤ 0
have neg : ∀ (hq : ¬q = 0), ⟪u - v, w - v⟫_ℝ ≤ 0
Tactic: by_cases hq : q = 0
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Minimal (hypothesis)
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
⊢ ⟪u - v, w - v⟫_ℝ ≤ 0
have this₁ : ∀ (θ : ℝ) (hθ₁ : 0 < θ) (hθ₂ : θ ≤ 1), 2 * p ≤ θ * 0
Tactic: rw [hq] at this
Cleared hypotheses: this, hq
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Minimal (hypothesis)
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
have this₁ : 2 * p ≤ HMul.hMul (α := ℝ) 1 0
Tactic: have := this (1 : ℝ) (by simp) (by simp)
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Minimal (goal)
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
⊢ p ≤ 0
have linarith : 0 < p → 2 * p - HMul.hMul (α := ℝ) 1 0 + 2 * (0 - p) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Minimal (goal)
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
⊢ p ≤ 0
have linarith₁ : 0 < p → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Minimal (hypothesis)
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
⊢ ⟪u - v, w - v⟫_ℝ ≤ 0
have q_pos : 0 < q
Tactic: have q_pos : 0 < q := lt_of_le_of_ne (sq_nonneg _) fun h ↦ hq h.symm
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Minimal (goal)
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
⊢ ⟪u - v, w - v⟫_ℝ ≤ 0
have neg : ∀ (hp : ¬⟪u - v, w - v⟫_ℝ ≤ 0), False
Tactic: by_contra hp
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Minimal (hypothesis)
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
⊢ False
have hp₁ : 0 < ⟪u - v, w - v⟫_ℝ
Tactic: rw [not_le] at hp
Cleared hypotheses: hp