awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : 0 < ⟪u - v, w - v⟫_ℝ
θ : ℝ := min 1 (p / q)
⊢ False
have eq₁ : θ * 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
-- 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 : 0 < ⟪u - v, w - v⟫_ℝ
θ : ℝ := min 1 (p / q)
eq₁ : θ * q ≤ p
⊢ False
have this₁ : 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₁
-- 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 ≤ θ * 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
⊢ False
have linarith : 0 - ⟪u - v, w - v⟫_ℝ + (2 * p - 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_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
⊢ ‖u - v‖ = ⨅ (w : (↑K : Type u_3)), ‖u - (↑w : F)‖
have mpr : ‖u - v‖ ≤ ⨅ (w : (↑K : Type u_3)), ‖u - (↑w : F)‖
Tactic: apply le_antisymm
-- 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_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)‖
⊢ ‖u - v‖ = ⨅ (w : (↑K : Type u_3)), ‖u - (↑w : F)‖
have mpr₁ : ⨅ (w : (↑K : Type u_3)), ‖u - (↑w : F)‖ ≤ ‖u - v‖
Tactic: apply le_antisymm
-- 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_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
⊢ ‖u - v‖ ≤ ⨅ (w : (↑K : Type u_3)), ‖u - (↑w : F)‖
have mpr : ∀ (x : (↑K : Type u_3)), ‖u - v‖ ≤ ‖u - (↑x : F)‖
Tactic: apply le_ciInf
-- 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_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‖ ≤ ‖u - (↑w : F)‖
have mpr : ‖u - v‖ * ‖u - v‖ ≤ ‖u - (↑w : F)‖ * ‖u - (↑w : F)‖
Tactic: apply nonneg_le_nonneg_of_sq_le_sq (norm_nonneg _)
-- 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_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‖ * ‖u - v‖ ≤ ‖u - (↑w : F)‖ * ‖u - (↑w : F)‖
have this₁ : ⟪u - v, (↑w : F) - v⟫_ℝ ≤ 0
Tactic: have := h w w.2
-- 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_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‖ ≤ ‖u - v‖ * ‖u - v‖ - 2 * ⟪u - v, (↑w : F) - v⟫_ℝ
have 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
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_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
⊢ ‖u - v‖ * ‖u - v‖ ≤ ‖u - v‖ * ‖u - v‖ - 2 * ⟪u - v, (↑w : F) - v⟫_ℝ
have linarith₁ : ‖u - v‖ * ‖u - v‖ - 2 * ⟪u - v, (↑w : F) - v⟫_ℝ < ‖u - v‖ * ‖u - v‖ → GT.gt (α := ℝ) 2 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_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⟫_ℝ ≤
    HPow.hPow (β := ℕ) ‖u - v‖ 2 - 2 * ⟪u - v, (↑w : F) - v⟫_ℝ + HPow.hPow (β := ℕ) ‖(↑w : F) - v‖ 2
have 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
Tactic: rw [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_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
have refine : 0 ≤ HPow.hPow (β := ℕ) ‖(↑w : F) - v‖ 2
Tactic: refine le_add_of_nonneg_right ?_
-- 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_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 - ((↑w : F) - v)‖ 2 = ‖u - (↑w : F)‖ * ‖u - (↑w : F)‖
have this₁ : u - v - ((↑w : F) - v) = u - (↑w : F)
Tactic: have : u - v - (w - v) = u - w := by abel
-- 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_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)
⊢ HPow.hPow (β := ℕ) ‖u - v - ((↑w : F) - v)‖ 2 = ‖u - (↑w : F)‖ * ‖u - (↑w : F)‖
have rw : HPow.hPow (β := ℕ) ‖u - (↑w : F)‖ 2 = ‖u - (↑w : F)‖ * ‖u - (↑w : F)‖
Tactic: rw [this, 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_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)‖
⊢ HPow.hPow (β := ℕ) ‖u - v - ((↑w : F) - v)‖ 2 = ‖u - (↑w : F)‖ * ‖u - (↑w : F)‖
have rw₁ : ‖u - (↑w : F)‖ * ‖u - (↑w : F)‖ = ‖u - (↑w : F)‖ * ‖u - (↑w : F)‖
Tactic: rw [this, 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_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‖ ≤ ‖u - (↑w : F)‖ * ‖u - (↑w : F)‖
have w₁ : ‖u - v‖ * ‖u - v‖ ≤ ‖u - v‖ * ‖u - v‖ - 2 * ⟪u - v, (↑w : F) - v⟫_ℝ
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]
-- 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_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⟫_ℝ
⊢ ‖u - v‖ * ‖u - v‖ ≤ ‖u - (↑w : F)‖ * ‖u - (↑w : F)‖
have 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
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]
-- 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_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
⊢ ‖u - v‖ * ‖u - v‖ ≤ ‖u - (↑w : F)‖ * ‖u - (↑w : F)‖
have w₃ : HPow.hPow (β := ℕ) ‖u - v - ((↑w : F) - v)‖ 2 = ‖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]
-- 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_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 - (↑w : F)‖ ≤ ‖u - v‖
have 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))
Tactic: change ⨅ w : K, ‖u - w‖ ≤ (fun w : K => ‖u - w‖) ⟨v, 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_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
⊢ 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))
have mpr : BddBelow (α := ℝ) (Set.range fun (w : (↑K : Type u_3)) ↦ ‖u - (↑w : F)‖)
Tactic: apply ciInf_le
-- 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_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
⊢ BddBelow (α := ℝ) (Set.range fun (w : (↑K : Type u_3)) ↦ ‖u - (↑w : F)‖)
have h₁ : Membership.mem (γ := Set ℝ) (lowerBounds (Set.range fun (w : (↑K : Type u_3)) ↦ ‖u - (↑w : F)‖)) 0
Tactic: use 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 : 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
have h₁ : Convex ℝ (↑K : Set F)
Tactic: rwa [norm_eq_iInf_iff_real_inner_le_zero] at 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 : 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)
⊢ ∀ w ∈ K, ⟪u - v, w - v⟫_ℝ ≤ 0
have hv₁ : v ∈ (↑K : Set F)
Tactic: rwa [norm_eq_iInf_iff_real_inner_le_zero] at 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 : 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⟫_ℝ = 0
have h₁ : ∀ 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]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Minimal (hypothesis)
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
⊢ ⟪u - v, w⟫_ℝ ≤ 0
have this : w' ∈ K
Tactic: have : w' ∈ K := Submodule.add_mem _ hw hv
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Minimal (hypothesis)
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⟫_ℝ ≤ 0
have h₁ : ⟪u - v, w' - v⟫_ℝ ≤ 0
Tactic: have h₁ := h w' this
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Minimal (hypothesis)
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
⊢ ⟪u - v, w⟫_ℝ ≤ 0
have h₂ : w' - v = w
Tactic: have h₂ : w' - v = w := by
          simp only [w', add_neg_cancel_right, sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Minimal (hypothesis)
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
⊢ ⟪u - v, w⟫_ℝ = 0
have le : ⟪u - v, w⟫_ℝ ≤ 0
Tactic: have le : ⟪u - v, w⟫_ℝ ≤ 0 := by
        let w' := w + v
        have : w' ∈ K := Submodule.add_mem _ hw hv
        have h₁ := h w' this
        have h₂ : w' - v = w := by
          simp only [w', add_neg_cancel_right, sub_eq_add_neg]
        rw [h₂] at h₁
        exact 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 : 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
le : ⟪u - v, w⟫_ℝ ≤ 0
w'' : F := -w + v
⊢ ⟪u - v, w⟫_ℝ ≥ 0
have this : w'' ∈ K
Tactic: have : w'' ∈ K := Submodule.add_mem _ (Submodule.neg_mem _ hw) hv
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Minimal (hypothesis)
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
le : ⟪u - v, w⟫_ℝ ≤ 0
w'' : F := -w + v
this : w'' ∈ K
⊢ ⟪u - v, w⟫_ℝ ≥ 0
have h₁ : ⟪u - v, w'' - v⟫_ℝ ≤ 0
Tactic: have h₁ := h w'' this
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Minimal (hypothesis)
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
le : ⟪u - v, w⟫_ℝ ≤ 0
w'' : F := -w + v
this : w'' ∈ K
h₁ : ⟪u - v, w'' - v⟫_ℝ ≤ 0
⊢ ⟪u - v, w⟫_ℝ ≥ 0
have h₂ : w'' - v = -w
Tactic: have h₂ : w'' - v = -w := by
          simp only [w'', add_neg_cancel_right, sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Minimal (hypothesis)
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
le : ⟪u - v, w⟫_ℝ ≤ 0
w'' : F := -w + v
this : w'' ∈ K
h₁ : ⟪u - v, w'' - v⟫_ℝ ≤ 0
h₂ : w'' - v = -w
⊢ ⟪u - v, w⟫_ℝ ≥ 0
have h₃ : -⟪u - v, w⟫_ℝ ≤ 0
Tactic: rw [h₂, inner_neg_right] at h₁
Cleared hypotheses: h₁, 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 : 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
le : ⟪u - v, w⟫_ℝ ≤ 0
w'' : F := -w + v
this : w'' ∈ K
h₁ : -⟪u - v, w⟫_ℝ ≤ 0
h₂ : w'' - v = -w
⊢ ⟪u - v, w⟫_ℝ ≥ 0
have linarith : ⟪u - v, w⟫_ℝ < 0 → -⟪u - v, w⟫_ℝ - 0 + (⟪u - v, w⟫_ℝ - 0) = 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 : 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
le : ⟪u - v, w⟫_ℝ ≤ 0
⊢ ⟪u - v, w⟫_ℝ = 0
have ge : ⟪u - v, w⟫_ℝ ≥ 0
Tactic: have ge : ⟪u - v, w⟫_ℝ ≥ 0 := by
        let w'' := -w + v
        have : w'' ∈ K := Submodule.add_mem _ (Submodule.neg_mem _ hw) hv
        have h₁ := h w'' this
        have h₂ : w'' - v = -w := by
          simp only [w'', add_neg_cancel_right, sub_eq_add_neg]
        rw [h₂, inner_neg_right] at h₁
        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 : Submodule ℝ F
u v : F
hv : v ∈ K
h : ∀ w ∈ K, ⟪u - v, w⟫_ℝ = 0
w : F
hw : w ∈ K
w' : F := w - v
⊢ ⟪u - v, w - v⟫_ℝ ≤ 0
have this : w' ∈ K
Tactic: have : w' ∈ K := Submodule.sub_mem _ hw hv
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Minimal (hypothesis)
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
K : Submodule ℝ F
u v : F
hv : v ∈ K
h : ∀ w ∈ K, ⟪u - v, w⟫_ℝ = 0
w : F
hw : w ∈ K
w' : F := w - v
this : w' ∈ K
⊢ ⟪u - v, w - v⟫_ℝ ≤ 0
have h₁ : ⟪u - v, w'⟫_ℝ = 0
Tactic: have h₁ := h w' this
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Minimal (hypothesis)
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
K : Submodule ℝ F
u v : F
hv : v ∈ K
h : ∀ w ∈ K, ⟪u - v, w⟫_ℝ = 0
⊢ ‖u - v‖ = ⨅ (w : (↑(↑K : Set F) : Type u_3)), ‖u - (↑w : F)‖
have this : ∀ w ∈ K, ⟪u - v, w - v⟫_ℝ ≤ 0
Tactic: have : ∀ w ∈ K, ⟪u - v, w - v⟫_ℝ ≤ 0 := by
        intro w hw
        let w' := w - v
        have : w' ∈ K := Submodule.sub_mem _ hw hv
        have h₁ := h w' this
        exact le_of_eq 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 : Submodule ℝ F
u v : F
hv : v ∈ K
h : ∀ w ∈ K, ⟪u - v, w⟫_ℝ = 0
this : ∀ w ∈ K, ⟪u - v, w - v⟫_ℝ ≤ 0
⊢ ‖u - v‖ = ⨅ (w : (↑(↑K : Set F) : Type u_3)), ‖u - (↑w : F)‖
have h₁ : Convex ℝ (↑K : Set F)
Tactic: rwa [norm_eq_iInf_iff_real_inner_le_zero]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Minimal (goal)
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
K : Submodule ℝ F
u v : F
hv : v ∈ K
h : ∀ w ∈ K, ⟪u - v, w⟫_ℝ = 0
this : ∀ w ∈ K, ⟪u - v, w - v⟫_ℝ ≤ 0
h₁ : Convex ℝ (↑K : Set F)
⊢ ‖u - v‖ = ⨅ (w : (↑(↑K : Set F) : Type u_3)), ‖u - (↑w : F)‖
have hv₁ : v ∈ (↑K : Set F)
Tactic: rwa [norm_eq_iInf_iff_real_inner_le_zero]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Minimal (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
u v : E
hv : v ∈ K
this : InnerProductSpace ℝ E := rclikeToReal 𝕜 E
K' : Submodule ℝ E := restrictScalars ℝ K
⊢ ‖u - v‖ = ⨅ (w : ↥K), ‖u - (↑w : E)‖ ↔ ∀ w ∈ K, ⟪u - v, w⟫_𝕜 = 0
have mp : ‖u - v‖ = ⨅ (w : ↥K), ‖u - (↑w : E)‖ → ∀ w ∈ K, ⟪u - v, w⟫_𝕜 = 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Minimal (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
u v : E
hv : v ∈ K
this : InnerProductSpace ℝ E := rclikeToReal 𝕜 E
K' : Submodule ℝ E := restrictScalars ℝ K
mp : ‖u - v‖ = ⨅ (w : ↥K), ‖u - (↑w : E)‖ → ∀ w ∈ K, ⟪u - v, w⟫_𝕜 = 0
⊢ ‖u - v‖ = ⨅ (w : ↥K), ‖u - (↑w : E)‖ ↔ ∀ w ∈ K, ⟪u - v, w⟫_𝕜 = 0
have mpr : (∀ w ∈ K, ⟪u - v, w⟫_𝕜 = 0) → ‖u - v‖ = ⨅ (w : ↥K), ‖u - (↑w : E)‖
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Minimal (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
u v : E
hv : v ∈ K
this : InnerProductSpace ℝ E := rclikeToReal 𝕜 E
K' : Submodule ℝ E := restrictScalars ℝ K
H : ‖u - v‖ = ⨅ (w : ↥K), ‖u - (↑w : E)‖
⊢ ∀ w ∈ K, ⟪u - v, w⟫_𝕜 = 0
have A : ∀ w ∈ K, Eq (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪u - v, w⟫_𝕜 : ℝ) (0 : ℝ)
Tactic: have A : ∀ w ∈ K, re ⟪u - v, w⟫ = 0 := (K'.norm_eq_iInf_iff_real_inner_eq_zero hv).1 H