-- 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 : ∀ w ∈ K, ⟪u - v, w⟫_ℝ = 0
this : ∀ w ∈ K, ⟪u - v, w - v⟫_ℝ ≤ 0
⊢ ‖u - v‖ = ⨅ w, ‖u - ↑w‖

Tactic:
rwa [norm_eq_iInf_iff_real_inner_le_zero]

Result:
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

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:
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₁

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
⊢ ⟪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⟫_ℝ ≤ 0
h₂ : w' - v = w
⊢ ⟪u - v, w⟫_ℝ ≤ 0

Tactic:
exact 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
this : w'' ∈ K
h₁ : ⟪u - v, w'' - v⟫_ℝ ≤ 0
h₂ : w'' - v = -w
⊢ ⟪u - v, w⟫_ℝ ≥ 0

Tactic:
rw [h₂, inner_neg_right] 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
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

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
⊢ ⟪u - v, w⟫_ℝ ≤ 0

Tactic:
have : w' ∈ K := Submodule.add_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
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‖
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

Tactic:
linarith

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
⊢ ⟪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'', neg_inj, add_neg_cancel_right, sub_eq_add_neg]
  rw [h₂, inner_neg_right] at h₁
  linarith

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
ge : ⟪u - v, w⟫_ℝ ≥ 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
⊢ ‖u - v‖ = ⨅ w, ‖u - ↑w‖ → ∀ w ∈ K, ⟪u - v, w⟫_ℝ = 0

Tactic:
intro 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‖
⊢ ∀ 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
⊢ (∀ w ∈ K, ⟪u - v, w⟫_ℝ = 0) → ‖u - v‖ = ⨅ w, ‖u - ↑w‖

Tactic:
intro h

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
⊢ ‖u - v‖ = ⨅ w, ‖u - ↑w‖

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
ge : ⟪u - v, w⟫_ℝ ≥ 0
⊢ ⟪u - v, w⟫_ℝ = 0

Tactic:
exact le_antisymm le ge

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
this : w'' ∈ K
h₁ : ⟪u - v, w'' - v⟫_ℝ ≤ 0
⊢ w'' - v = -w

Tactic:
simp only [w'', neg_inj, 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 ∈ K, ⟪u - v, w - v⟫_ℝ ≤ 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 : ∀ w ∈ K, ⟪u - v, w⟫_ℝ = 0
w : F
hw : 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‖
⊢ ∀ w ∈ K, ⟪u - v, w - v⟫_ℝ ≤ 0

Tactic:
rwa [norm_eq_iInf_iff_real_inner_le_zero] at h

Result:
case h
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‖
⊢ Convex ℝ ↑K

case hv
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‖
⊢ v ∈ ↑K

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
⊢ ⟪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
le : ⟪u - v, w⟫_ℝ ≤ 0
w'' : F := -w + v
this : w'' ∈ K
h₁ : ⟪u - v, w'' - v⟫_ℝ ≤ 0
⊢ ⟪u - v, w⟫_ℝ ≥ 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 : ‖u - v‖ = ⨅ w, ‖u - ↑w‖
⊢ Convex ℝ ↑K

case hv
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‖
⊢ v ∈ ↑K

Tactic:
exacts [K.convex, hv]

Result:
no goals