-- Mathlib/Analysis/InnerProductSpace/Projection.lean
theorem norm_eq_iInf_iff_inner_eq_zero {u : E} {v : E} (hv : v ∈ K) :
    (‖u - v‖ = ⨅ w : K, ‖u - w‖) ↔ ∀ w ∈ K, ⟪u - v, w⟫ = 0

Proof state:
case mpr
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
u v : E
hv : v ∈ K
this✝¹ : InnerProductSpace ℝ E := rclikeToReal 𝕜 E
this✝ : Module ℝ E := RestrictScalars.module ℝ 𝕜 E
K' : Submodule ℝ E := Submodule.restrictScalars ℝ K
H : ∀ w ∈ K, ⟪u - v, w⟫_𝕜 = 0
this : ∀ w ∈ K', ⟪u - v, w⟫_ℝ = 0
⊢ ‖u - v‖ = ⨅ w, ‖u - ↑w‖

Tactic:
exact (norm_eq_iInf_iff_real_inner_eq_zero K' hv).2 this

Result:
no goals

Proof state:
case mp.him
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
u v : E
hv : v ∈ K
this✝ : InnerProductSpace ℝ E := rclikeToReal 𝕜 E
this : Module ℝ E := RestrictScalars.module ℝ 𝕜 E
K' : Submodule ℝ E := Submodule.restrictScalars ℝ K
H : ‖u - v‖ = ⨅ w, ‖u - ↑w‖
A : ∀ w ∈ K, re ⟪u - v, w⟫_𝕜 = 0
w : E
hw : w ∈ K
⊢ im 0 = im ⟪u - v, w⟫_𝕜

Tactic:
calc
  im (0 : 𝕜) = 0 := im.map_zero
  _ = re ⟪u - v, (-I : 𝕜) • w⟫ := (A _ (K.smul_mem (-I) hw)).symm
  _ = re (-I * ⟪u - v, w⟫) := by rw [inner_smul_right]
  _ = im ⟪u - v, w⟫ := by simp

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
u v : E
hv : v ∈ K
this✝ : InnerProductSpace ℝ E := rclikeToReal 𝕜 E
this : Module ℝ E := RestrictScalars.module ℝ 𝕜 E
K' : Submodule ℝ E := Submodule.restrictScalars ℝ K
H : ∀ w ∈ K, ⟪u - v, w⟫_𝕜 = 0
w : E
hw : w ∈ K'
⊢ ⟪u - v, w⟫_ℝ = 0

Tactic:
rw [real_inner_eq_re_inner, H w hw]

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
u v : E
hv : v ∈ K
this✝ : InnerProductSpace ℝ E := rclikeToReal 𝕜 E
this : Module ℝ E := RestrictScalars.module ℝ 𝕜 E
K' : Submodule ℝ E := Submodule.restrictScalars ℝ K
H : ∀ w ∈ K, ⟪u - v, w⟫_𝕜 = 0
w : E
hw : w ∈ K'
⊢ re 0 = 0

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
u v : E
hv : v ∈ K
⊢ ‖u - v‖ = ⨅ w, ‖u - ↑w‖ ↔ ∀ w ∈ K, ⟪u - v, w⟫_𝕜 = 0

Tactic:
letI : InnerProductSpace ℝ E := InnerProductSpace.rclikeToReal 𝕜 E

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
u v : E
hv : v ∈ K
this : InnerProductSpace ℝ E := rclikeToReal 𝕜 E
⊢ ‖u - v‖ = ⨅ w, ‖u - ↑w‖ ↔ ∀ w ∈ K, ⟪u - v, w⟫_𝕜 = 0

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
u v : E
hv : v ∈ K
this✝ : InnerProductSpace ℝ E := rclikeToReal 𝕜 E
this : Module ℝ E := RestrictScalars.module ℝ 𝕜 E
K' : Submodule ℝ E := Submodule.restrictScalars ℝ K
H : ∀ w ∈ K, ⟪u - v, w⟫_𝕜 = 0
w : E
hw : w ∈ K'
⊢ re 0 = 0

Tactic:
exact zero_re'

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
u v : E
hv : v ∈ K
this✝ : InnerProductSpace ℝ E := rclikeToReal 𝕜 E
this : Module ℝ E := RestrictScalars.module ℝ 𝕜 E
K' : Submodule ℝ E := Submodule.restrictScalars ℝ K
H : ‖u - v‖ = ⨅ w, ‖u - ↑w‖
A : ∀ w ∈ K, re ⟪u - v, w⟫_𝕜 = 0
w : E
hw : w ∈ K
⊢ re ⟪u - v, -I • w⟫_𝕜 = re (-I * ⟪u - v, w⟫_𝕜)

Tactic:
rw [inner_smul_right]

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
u v : E
hv : v ∈ K
this✝ : InnerProductSpace ℝ E := rclikeToReal 𝕜 E
this : Module ℝ E := RestrictScalars.module ℝ 𝕜 E
K' : Submodule ℝ E := Submodule.restrictScalars ℝ K
⊢ ‖u - v‖ = ⨅ w, ‖u - ↑w‖ ↔ ∀ w ∈ K, ⟪u - v, w⟫_𝕜 = 0

Tactic:
constructor

Result:
case mp
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
u v : E
hv : v ∈ K
this✝ : InnerProductSpace ℝ E := rclikeToReal 𝕜 E
this : Module ℝ E := RestrictScalars.module ℝ 𝕜 E
K' : Submodule ℝ E := Submodule.restrictScalars ℝ K
⊢ ‖u - v‖ = ⨅ w, ‖u - ↑w‖ → ∀ w ∈ K, ⟪u - v, w⟫_𝕜 = 0

case mpr
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
u v : E
hv : v ∈ K
this✝ : InnerProductSpace ℝ E := rclikeToReal 𝕜 E
this : Module ℝ E := RestrictScalars.module ℝ 𝕜 E
K' : Submodule ℝ E := Submodule.restrictScalars ℝ K
⊢ (∀ w ∈ K, ⟪u - v, w⟫_𝕜 = 0) → ‖u - v‖ = ⨅ w, ‖u - ↑w‖

Proof state:
case mpr
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
u v : E
hv : v ∈ K
this✝ : InnerProductSpace ℝ E := rclikeToReal 𝕜 E
this : Module ℝ E := RestrictScalars.module ℝ 𝕜 E
K' : Submodule ℝ E := Submodule.restrictScalars ℝ K
⊢ (∀ w ∈ K, ⟪u - v, w⟫_𝕜 = 0) → ‖u - v‖ = ⨅ w, ‖u - ↑w‖

Tactic:
intro H

Result:
case mpr
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
u v : E
hv : v ∈ K
this✝ : InnerProductSpace ℝ E := rclikeToReal 𝕜 E
this : Module ℝ E := RestrictScalars.module ℝ 𝕜 E
K' : Submodule ℝ E := Submodule.restrictScalars ℝ K
H : ∀ w ∈ K, ⟪u - v, w⟫_𝕜 = 0
⊢ ‖u - v‖ = ⨅ w, ‖u - ↑w‖

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
u v : E
hv : v ∈ K
this✝ : InnerProductSpace ℝ E := rclikeToReal 𝕜 E
this : Module ℝ E := RestrictScalars.module ℝ 𝕜 E
K' : Submodule ℝ E := Submodule.restrictScalars ℝ K
H : ‖u - v‖ = ⨅ w, ‖u - ↑w‖
A : ∀ w ∈ K, re ⟪u - v, w⟫_𝕜 = 0
w : E
hw : w ∈ K
⊢ re (-I * ⟪u - v, w⟫_𝕜) = im ⟪u - v, w⟫_𝕜

Tactic:
simp

Result:
no goals

Proof state:
case mp
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
u v : E
hv : v ∈ K
this✝ : InnerProductSpace ℝ E := rclikeToReal 𝕜 E
this : Module ℝ E := RestrictScalars.module ℝ 𝕜 E
K' : Submodule ℝ E := Submodule.restrictScalars ℝ K
H : ‖u - v‖ = ⨅ w, ‖u - ↑w‖
A : ∀ w ∈ K, re ⟪u - v, w⟫_𝕜 = 0
w : E
hw : w ∈ K
⊢ ⟪u - v, w⟫_𝕜 = 0

Tactic:
apply RCLike.ext

Result:
case mp.hre
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
u v : E
hv : v ∈ K
this✝ : InnerProductSpace ℝ E := rclikeToReal 𝕜 E
this : Module ℝ E := RestrictScalars.module ℝ 𝕜 E
K' : Submodule ℝ E := Submodule.restrictScalars ℝ K
H : ‖u - v‖ = ⨅ w, ‖u - ↑w‖
A : ∀ w ∈ K, re ⟪u - v, w⟫_𝕜 = 0
w : E
hw : w ∈ K
⊢ re ⟪u - v, w⟫_𝕜 = re 0

case mp.him
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
u v : E
hv : v ∈ K
this✝ : InnerProductSpace ℝ E := rclikeToReal 𝕜 E
this : Module ℝ E := RestrictScalars.module ℝ 𝕜 E
K' : Submodule ℝ E := Submodule.restrictScalars ℝ K
H : ‖u - v‖ = ⨅ w, ‖u - ↑w‖
A : ∀ w ∈ K, re ⟪u - v, w⟫_𝕜 = 0
w : E
hw : w ∈ K
⊢ im ⟪u - v, w⟫_𝕜 = im 0

Proof state:
case mp
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
u v : E
hv : v ∈ K
this✝ : InnerProductSpace ℝ E := rclikeToReal 𝕜 E
this : Module ℝ E := RestrictScalars.module ℝ 𝕜 E
K' : Submodule ℝ E := Submodule.restrictScalars ℝ K
H : ‖u - v‖ = ⨅ w, ‖u - ↑w‖
A : ∀ w ∈ K, re ⟪u - v, w⟫_𝕜 = 0
⊢ ∀ w ∈ K, ⟪u - v, w⟫_𝕜 = 0

Tactic:
intro w hw

Result:
case mp
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
u v : E
hv : v ∈ K
this✝ : InnerProductSpace ℝ E := rclikeToReal 𝕜 E
this : Module ℝ E := RestrictScalars.module ℝ 𝕜 E
K' : Submodule ℝ E := Submodule.restrictScalars ℝ K
H : ‖u - v‖ = ⨅ w, ‖u - ↑w‖
A : ∀ w ∈ K, re ⟪u - v, w⟫_𝕜 = 0
w : E
hw : w ∈ K
⊢ ⟪u - v, w⟫_𝕜 = 0