-- Mathlib/Analysis/InnerProductSpace/Projection.lean
theorem norm_eq_iInf_iff_real_inner_eq_zero (K : Submodule ℝ F) {u : F} {v : F} (hv : v ∈ K) :
    (‖u - v‖ = ⨅ w : (↑K : Set F), ‖u - w‖) ↔ ∀ w ∈ K, ⟪u - v, w⟫_ℝ = 0 :=
  Iff.intro
    (by
      intro h
      have h : ∀ w ∈ K, ⟪u - v, w - v⟫_ℝ ≤ 0

Proof state:
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
K : Submodule ℝ F
u v : F
hv : v ∈ K
h✝ : ‖u - v‖ = ⨅ w, ‖u - ↑w‖
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
h₂ : w' - v = w
⊢ ⟪u - v, w⟫_ℝ ≤ 0

Tactic:
rw [h₂] at h₁

Result:
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
K : Submodule ℝ F
u v : F
hv : v ∈ K
h✝ : ‖u - v‖ = ⨅ w, ‖u - ↑w‖
h : ∀ w ∈ K, ⟪u - v, w - v⟫_ℝ ≤ 0
w : F
hw : w ∈ K
w' : F := w + v
this : w' ∈ K
h₁ : ⟪u - v, w⟫_ℝ ≤ 0
h₂ : w' - v = w
⊢ ⟪u - v, w⟫_ℝ ≤ 0

Proof state:
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
K : Submodule ℝ F
u v : F
hv : v ∈ K
h✝ : ‖u - v‖ = ⨅ w, ‖u - ↑w‖
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

Tactic:
have h₂ : w'' - v = -w := by
  simp only [w'', neg_inj, add_neg_cancel_right, sub_eq_add_neg]

Result:
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
K : Submodule ℝ F
u v : F
hv : v ∈ K
h✝ : ‖u - v‖ = ⨅ w, ‖u - ↑w‖
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

Proof state:
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : 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
h₁ : ⟪u - v, w'⟫_ℝ = 0
⊢ ⟪u - v, w - v⟫_ℝ ≤ 0

Tactic:
exact le_of_eq h₁

Result:
no goals

Proof state:
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
K : Submodule ℝ F
u v : F
hv : v ∈ K
h✝ : ‖u - v‖ = ⨅ w, ‖u - ↑w‖
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

Tactic:
have : w'' ∈ K := Submodule.add_mem _ (Submodule.neg_mem _ hw) hv

Result:
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
K : Submodule ℝ F
u v : F
hv : v ∈ K
h✝ : ‖u - v‖ = ⨅ w, ‖u - ↑w‖
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

Proof state:
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
K : Submodule ℝ F
u v : F
hv : v ∈ K
h : ‖u - v‖ = ⨅ w, ‖u - ↑w‖
⊢ ∀ w ∈ K, ⟪u - v, w⟫_ℝ = 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]

Result:
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
K : Submodule ℝ F
u v : F
hv : v ∈ K
h✝ : ‖u - v‖ = ⨅ w, ‖u - ↑w‖
h : ∀ w ∈ K, ⟪u - v, w - v⟫_ℝ ≤ 0
⊢ ∀ w ∈ K, ⟪u - v, w⟫_ℝ = 0

Proof state:
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
K : Submodule ℝ F
u v : F
hv : v ∈ K
h✝ : ‖u - v‖ = ⨅ w, ‖u - ↑w‖
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]

Result:
no goals

Proof state:
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
K : Submodule ℝ F
u v : F
hv : v ∈ K
h : ∀ w ∈ K, ⟪u - v, w⟫_ℝ = 0
w : F
hw : w ∈ K
⊢ ⟪u - v, w - v⟫_ℝ ≤ 0

Tactic:
let w' := w - v

Result:
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : 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

Proof state:
case h
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : 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
⊢ Convex ℝ ↑K

case hv
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : 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
⊢ v ∈ ↑K

Tactic:
exacts [Submodule.convex _, hv]

Result:
no goals

Proof state:
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : 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

Tactic:
have : w' ∈ K := Submodule.sub_mem _ hw hv

Result:
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : 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

Proof state:
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
K : Submodule ℝ F
u v : F
hv : v ∈ K
h✝ : ‖u - v‖ = ⨅ w, ‖u - ↑w‖
h : ∀ w ∈ K, ⟪u - v, w - v⟫_ℝ ≤ 0
w : F
hw : w ∈ K
le : ⟪u - v, w⟫_ℝ ≤ 0
⊢ ⟪u - v, w⟫_ℝ ≥ 0

Tactic:
let w'' := -w + v

Result:
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
K : Submodule ℝ F
u v : F
hv : v ∈ K
h✝ : ‖u - v‖ = ⨅ w, ‖u - ↑w‖
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

Proof state:
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
K : Submodule ℝ F
u v : F
hv : v ∈ K
h✝ : ‖u - v‖ = ⨅ w, ‖u - ↑w‖
h : ∀ w ∈ K, ⟪u - v, w - v⟫_ℝ ≤ 0
w : F
hw : w ∈ K
w' : F := w + v
this : w' ∈ K
⊢ ⟪u - v, w⟫_ℝ ≤ 0

Tactic:
have h₁ := h w' this

Result:
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
K : Submodule ℝ F
u v : F
hv : v ∈ K
h✝ : ‖u - v‖ = ⨅ w, ‖u - ↑w‖
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

Proof state:
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
K : Submodule ℝ F
u v : F
hv : v ∈ K
h✝ : ‖u - v‖ = ⨅ w, ‖u - ↑w‖
h : ∀ w ∈ K, ⟪u - v, w - v⟫_ℝ ≤ 0
w : F
hw : w ∈ K
⊢ ⟪u - v, w⟫_ℝ ≤ 0

Tactic:
let w' := w + v

Result:
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
K : Submodule ℝ F
u v : F
hv : v ∈ K
h✝ : ‖u - v‖ = ⨅ w, ‖u - ↑w‖
h : ∀ w ∈ K, ⟪u - v, w - v⟫_ℝ ≤ 0
w : F
hw : w ∈ K
w' : F := w + v
⊢ ⟪u - v, w⟫_ℝ ≤ 0

Proof state:
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : 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

Tactic:
have h₁ := h w' this

Result:
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : 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
h₁ : ⟪u - v, w'⟫_ℝ = 0
⊢ ⟪u - v, w - v⟫_ℝ ≤ 0

Proof state:
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
K : Submodule ℝ F
u v : F
hv : v ∈ K
h✝ : ‖u - v‖ = ⨅ w, ‖u - ↑w‖
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

Tactic:
have h₂ : w' - v = w := by
  simp only [w', add_neg_cancel_right, sub_eq_add_neg]

Result:
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
K : Submodule ℝ F
u v : F
hv : v ∈ K
h✝ : ‖u - v‖ = ⨅ w, ‖u - ↑w‖
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
h₂ : w' - v = w
⊢ ⟪u - v, w⟫_ℝ ≤ 0

Proof state:
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
K : Submodule ℝ F
u v : F
hv : v ∈ K
h✝ : ‖u - v‖ = ⨅ w, ‖u - ↑w‖
h : ∀ w ∈ K, ⟪u - v, w - v⟫_ℝ ≤ 0
⊢ ∀ w ∈ K, ⟪u - v, w⟫_ℝ = 0

Tactic:
intro w hw

Result:
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
K : Submodule ℝ F
u v : F
hv : v ∈ K
h✝ : ‖u - v‖ = ⨅ w, ‖u - ↑w‖
h : ∀ w ∈ K, ⟪u - v, w - v⟫_ℝ ≤ 0
w : F
hw : w ∈ K
⊢ ⟪u - v, w⟫_ℝ = 0