𝕜 : Type u_2
E : Type u_1
F : Type ?u.265347
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
u v : E
hv : v ∈ K
this : InnerProductSpace ℝ E := InnerProductSpace.isROrCToReal 𝕜 E
⊢ (‖u - v‖ = ⨅ (w : { x // x ∈ K }), ‖u - ↑w‖) ↔ ∀ (w : E), w ∈ K → inner (u - v) w = 0
𝕜 : Type u_2
E : Type u_1
F : Type ?u.265347
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
u v : E
hv : v ∈ K
⊢ (‖u - v‖ = ⨅ (w : { x // x ∈ K }), ‖u - ↑w‖) ↔ ∀ (w : E), w ∈ K → inner (u - v) w = 0
letI : InnerProductSpace ℝ E := InnerProductSpace.isROrCToReal 𝕜 E
𝕜 : Type u_2
E : Type u_1
F : Type ?u.265347
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
u v : E
hv : v ∈ K
this✝ : InnerProductSpace ℝ E := InnerProductSpace.isROrCToReal 𝕜 E
this : Module ℝ E := RestrictScalars.module ℝ 𝕜 E
⊢ (‖u - v‖ = ⨅ (w : { x // x ∈ K }), ‖u - ↑w‖) ↔ ∀ (w : E), w ∈ K → inner (u - v) w = 0
𝕜 : Type u_2
E : Type u_1
F : Type ?u.265347
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
u v : E
hv : v ∈ K
this : InnerProductSpace ℝ E := InnerProductSpace.isROrCToReal 𝕜 E
⊢ (‖u - v‖ = ⨅ (w : { x // x ∈ K }), ‖u - ↑w‖) ↔ ∀ (w : E), w ∈ K → inner (u - v) w = 0
letI : Module ℝ E := RestrictScalars.module ℝ 𝕜 E
𝕜 : Type u_2
E : Type u_1
F : Type ?u.265347
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
u v : E
hv : v ∈ K
this✝ : InnerProductSpace ℝ E := InnerProductSpace.isROrCToReal 𝕜 E
this : Module ℝ E := RestrictScalars.module ℝ 𝕜 E
K' : Submodule ℝ E := Submodule.restrictScalars ℝ K
⊢ (‖u - v‖ = ⨅ (w : { x // x ∈ K }), ‖u - ↑w‖) ↔ ∀ (w : E), w ∈ K → inner (u - v) w = 0
𝕜 : Type u_2
E : Type u_1
F : Type ?u.265347
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
u v : E
hv : v ∈ K
this✝ : InnerProductSpace ℝ E := InnerProductSpace.isROrCToReal 𝕜 E
this : Module ℝ E := RestrictScalars.module ℝ 𝕜 E
⊢ (‖u - v‖ = ⨅ (w : { x // x ∈ K }), ‖u - ↑w‖) ↔ ∀ (w : E), w ∈ K → inner (u - v) w = 0
let K' : Submodule ℝ E := K.restrictScalars ℝ
case mp
𝕜 : Type u_2
E : Type u_1
F : Type ?u.265347
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
u v : E
hv : v ∈ K
this✝ : InnerProductSpace ℝ E := InnerProductSpace.isROrCToReal 𝕜 E
this : Module ℝ E := RestrictScalars.module ℝ 𝕜 E
K' : Submodule ℝ E := Submodule.restrictScalars ℝ K
⊢ (‖u - v‖ = ⨅ (w : { x // x ∈ K }), ‖u - ↑w‖) → ∀ (w : E), w ∈ K → inner (u - v) w = 0

case mpr
𝕜 : Type u_2
E : Type u_1
F : Type ?u.265347
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
u v : E
hv : v ∈ K
this✝ : InnerProductSpace ℝ E := InnerProductSpace.isROrCToReal 𝕜 E
this : Module ℝ E := RestrictScalars.module ℝ 𝕜 E
K' : Submodule ℝ E := Submodule.restrictScalars ℝ K
⊢ (∀ (w : E), w ∈ K → inner (u - v) w = 0) → ‖u - v‖ = ⨅ (w : { x // x ∈ K }), ‖u - ↑w‖
𝕜 : Type u_2
E : Type u_1
F : Type ?u.265347
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
u v : E
hv : v ∈ K
this✝ : InnerProductSpace ℝ E := InnerProductSpace.isROrCToReal 𝕜 E
this : Module ℝ E := RestrictScalars.module ℝ 𝕜 E
K' : Submodule ℝ E := Submodule.restrictScalars ℝ K
⊢ (‖u - v‖ = ⨅ (w : { x // x ∈ K }), ‖u - ↑w‖) ↔ ∀ (w : E), w ∈ K → inner (u - v) w = 0
constructor
case mp
𝕜 : Type u_2
E : Type u_1
F : Type ?u.265347
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
u v : E
hv : v ∈ K
this✝ : InnerProductSpace ℝ E := InnerProductSpace.isROrCToReal 𝕜 E
this : Module ℝ E := RestrictScalars.module ℝ 𝕜 E
K' : Submodule ℝ E := Submodule.restrictScalars ℝ K
H : ‖u - v‖ = ⨅ (w : { x // x ∈ K }), ‖u - ↑w‖
⊢ ∀ (w : E), w ∈ K → inner (u - v) w = 0
case mp
𝕜 : Type u_2
E : Type u_1
F : Type ?u.265347
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
u v : E
hv : v ∈ K
this✝ : InnerProductSpace ℝ E := InnerProductSpace.isROrCToReal 𝕜 E
this : Module ℝ E := RestrictScalars.module ℝ 𝕜 E
K' : Submodule ℝ E := Submodule.restrictScalars ℝ K
⊢ (‖u - v‖ = ⨅ (w : { x // x ∈ K }), ‖u - ↑w‖) → ∀ (w : E), w ∈ K → inner (u - v) w = 0
intro H
case mp
𝕜 : Type u_2
E : Type u_1
F : Type ?u.265347
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
u v : E
hv : v ∈ K
this✝ : InnerProductSpace ℝ E := InnerProductSpace.isROrCToReal 𝕜 E
this : Module ℝ E := RestrictScalars.module ℝ 𝕜 E
K' : Submodule ℝ E := Submodule.restrictScalars ℝ K
H : ‖u - v‖ = ⨅ (w : { x // x ∈ K }), ‖u - ↑w‖
A : ∀ (w : E), w ∈ K → ↑re (inner (u - v) w) = 0
⊢ ∀ (w : E), w ∈ K → inner (u - v) w = 0
case mp
𝕜 : Type u_2
E : Type u_1
F : Type ?u.265347
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
u v : E
hv : v ∈ K
this✝ : InnerProductSpace ℝ E := InnerProductSpace.isROrCToReal 𝕜 E
this : Module ℝ E := RestrictScalars.module ℝ 𝕜 E
K' : Submodule ℝ E := Submodule.restrictScalars ℝ K
H : ‖u - v‖ = ⨅ (w : { x // x ∈ K }), ‖u - ↑w‖
⊢ ∀ (w : E), w ∈ K → inner (u - v) w = 0
have A : ∀ w ∈ K, re ⟪u - v, w⟫ = 0 := (norm_eq_iInf_iff_real_inner_eq_zero K' hv).1 H
case mp
𝕜 : Type u_2
E : Type u_1
F : Type ?u.265347
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
u v : E
hv : v ∈ K
this✝ : InnerProductSpace ℝ E := InnerProductSpace.isROrCToReal 𝕜 E
this : Module ℝ E := RestrictScalars.module ℝ 𝕜 E
K' : Submodule ℝ E := Submodule.restrictScalars ℝ K
H : ‖u - v‖ = ⨅ (w : { x // x ∈ K }), ‖u - ↑w‖
A : ∀ (w : E), w ∈ K → ↑re (inner (u - v) w) = 0
w : E
hw : w ∈ K
⊢ inner (u - v) w = 0
case mp
𝕜 : Type u_2
E : Type u_1
F : Type ?u.265347
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
u v : E
hv : v ∈ K
this✝ : InnerProductSpace ℝ E := InnerProductSpace.isROrCToReal 𝕜 E
this : Module ℝ E := RestrictScalars.module ℝ 𝕜 E
K' : Submodule ℝ E := Submodule.restrictScalars ℝ K
H : ‖u - v‖ = ⨅ (w : { x // x ∈ K }), ‖u - ↑w‖
A : ∀ (w : E), w ∈ K → ↑re (inner (u - v) w) = 0
⊢ ∀ (w : E), w ∈ K → inner (u - v) w = 0
intro w hw
case mp.hre
𝕜 : Type u_2
E : Type u_1
F : Type ?u.265347
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
u v : E
hv : v ∈ K
this✝ : InnerProductSpace ℝ E := InnerProductSpace.isROrCToReal 𝕜 E
this : Module ℝ E := RestrictScalars.module ℝ 𝕜 E
K' : Submodule ℝ E := Submodule.restrictScalars ℝ K
H : ‖u - v‖ = ⨅ (w : { x // x ∈ K }), ‖u - ↑w‖
A : ∀ (w : E), w ∈ K → ↑re (inner (u - v) w) = 0
w : E
hw : w ∈ K
⊢ ↑re (inner (u - v) w) = ↑re 0

case mp.him
𝕜 : Type u_2
E : Type u_1
F : Type ?u.265347
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
u v : E
hv : v ∈ K
this✝ : InnerProductSpace ℝ E := InnerProductSpace.isROrCToReal 𝕜 E
this : Module ℝ E := RestrictScalars.module ℝ 𝕜 E
K' : Submodule ℝ E := Submodule.restrictScalars ℝ K
H : ‖u - v‖ = ⨅ (w : { x // x ∈ K }), ‖u - ↑w‖
A : ∀ (w : E), w ∈ K → ↑re (inner (u - v) w) = 0
w : E
hw : w ∈ K
⊢ ↑im (inner (u - v) w) = ↑im 0
case mp
𝕜 : Type u_2
E : Type u_1
F : Type ?u.265347
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
u v : E
hv : v ∈ K
this✝ : InnerProductSpace ℝ E := InnerProductSpace.isROrCToReal 𝕜 E
this : Module ℝ E := RestrictScalars.module ℝ 𝕜 E
K' : Submodule ℝ E := Submodule.restrictScalars ℝ K
H : ‖u - v‖ = ⨅ (w : { x // x ∈ K }), ‖u - ↑w‖
A : ∀ (w : E), w ∈ K → ↑re (inner (u - v) w) = 0
w : E
hw : w ∈ K
⊢ inner (u - v) w = 0
apply ext
no goals
case mp.hre
𝕜 : Type u_2
E : Type u_1
F : Type ?u.265347
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
u v : E
hv : v ∈ K
this✝ : InnerProductSpace ℝ E := InnerProductSpace.isROrCToReal 𝕜 E
this : Module ℝ E := RestrictScalars.module ℝ 𝕜 E
K' : Submodule ℝ E := Submodule.restrictScalars ℝ K
H : ‖u - v‖ = ⨅ (w : { x // x ∈ K }), ‖u - ↑w‖
A : ∀ (w : E), w ∈ K → ↑re (inner (u - v) w) = 0
w : E
hw : w ∈ K
⊢ ↑re (inner (u - v) w) = ↑re 0
simp [A w hw]
case mp.him
𝕜 : Type u_2
E : Type u_1
F : Type ?u.265347
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
u v : E
hv : v ∈ K
this✝ : InnerProductSpace ℝ E := InnerProductSpace.isROrCToReal 𝕜 E
this : Module ℝ E := RestrictScalars.module ℝ 𝕜 E
K' : Submodule ℝ E := Submodule.restrictScalars ℝ K
H : ‖u - v‖ = ⨅ (w : { x // x ∈ K }), ‖u - ↑w‖
A : ∀ (w : E), w ∈ K → ↑re (inner (u - v) w) = 0
w : E
hw : w ∈ K
⊢ ↑im 0 = ↑im (inner (u - v) w)
case mp.him
𝕜 : Type u_2
E : Type u_1
F : Type ?u.265347
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
u v : E
hv : v ∈ K
this✝ : InnerProductSpace ℝ E := InnerProductSpace.isROrCToReal 𝕜 E
this : Module ℝ E := RestrictScalars.module ℝ 𝕜 E
K' : Submodule ℝ E := Submodule.restrictScalars ℝ K
H : ‖u - v‖ = ⨅ (w : { x // x ∈ K }), ‖u - ↑w‖
A : ∀ (w : E), w ∈ K → ↑re (inner (u - v) w) = 0
w : E
hw : w ∈ K
⊢ ↑im (inner (u - v) w) = ↑im 0
symm
no goals
case mp.him
𝕜 : Type u_2
E : Type u_1
F : Type ?u.265347
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
u v : E
hv : v ∈ K
this✝ : InnerProductSpace ℝ E := InnerProductSpace.isROrCToReal 𝕜 E
this : Module ℝ E := RestrictScalars.module ℝ 𝕜 E
K' : Submodule ℝ E := Submodule.restrictScalars ℝ K
H : ‖u - v‖ = ⨅ (w : { x // x ∈ K }), ‖u - ↑w‖
A : ∀ (w : E), w ∈ K → ↑re (inner (u - v) w) = 0
w : E
hw : w ∈ K
⊢ ↑im 0 = ↑im (inner (u - v) w)
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
no goals
𝕜 : Type u_2
E : Type u_1
F : Type ?u.265347
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
u v : E
hv : v ∈ K
this✝ : InnerProductSpace ℝ E := InnerProductSpace.isROrCToReal 𝕜 E
this : Module ℝ E := RestrictScalars.module ℝ 𝕜 E
K' : Submodule ℝ E := Submodule.restrictScalars ℝ K
H : ‖u - v‖ = ⨅ (w : { x // x ∈ K }), ‖u - ↑w‖
A : ∀ (w : E), w ∈ K → ↑re (inner (u - v) w) = 0
w : E
hw : w ∈ K
⊢ ↑re (inner (u - v) (-I • w)) = ↑re (-I * inner (u - v) w)
rw [inner_smul_right]
no goals
𝕜 : Type u_2
E : Type u_1
F : Type ?u.265347
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
u v : E
hv : v ∈ K
this✝ : InnerProductSpace ℝ E := InnerProductSpace.isROrCToReal 𝕜 E
this : Module ℝ E := RestrictScalars.module ℝ 𝕜 E
K' : Submodule ℝ E := Submodule.restrictScalars ℝ K
H : ‖u - v‖ = ⨅ (w : { x // x ∈ K }), ‖u - ↑w‖
A : ∀ (w : E), w ∈ K → ↑re (inner (u - v) w) = 0
w : E
hw : w ∈ K
⊢ ↑re (-I * inner (u - v) w) = ↑im (inner (u - v) w)
simp
case mpr
𝕜 : Type u_2
E : Type u_1
F : Type ?u.265347
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
u v : E
hv : v ∈ K
this✝ : InnerProductSpace ℝ E := InnerProductSpace.isROrCToReal 𝕜 E
this : Module ℝ E := RestrictScalars.module ℝ 𝕜 E
K' : Submodule ℝ E := Submodule.restrictScalars ℝ K
H : ∀ (w : E), w ∈ K → inner (u - v) w = 0
⊢ ‖u - v‖ = ⨅ (w : { x // x ∈ K }), ‖u - ↑w‖
case mpr
𝕜 : Type u_2
E : Type u_1
F : Type ?u.265347
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
u v : E
hv : v ∈ K
this✝ : InnerProductSpace ℝ E := InnerProductSpace.isROrCToReal 𝕜 E
this : Module ℝ E := RestrictScalars.module ℝ 𝕜 E
K' : Submodule ℝ E := Submodule.restrictScalars ℝ K
⊢ (∀ (w : E), w ∈ K → inner (u - v) w = 0) → ‖u - v‖ = ⨅ (w : { x // x ∈ K }), ‖u - ↑w‖
intro H
case mpr
𝕜 : Type u_2
E : Type u_1
F : Type ?u.265347
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
u v : E
hv : v ∈ K
this✝¹ : InnerProductSpace ℝ E := InnerProductSpace.isROrCToReal 𝕜 E
this✝ : Module ℝ E := RestrictScalars.module ℝ 𝕜 E
K' : Submodule ℝ E := Submodule.restrictScalars ℝ K
H : ∀ (w : E), w ∈ K → inner (u - v) w = 0
this : ∀ (w : E), w ∈ K' → inner (u - v) w = 0
⊢ ‖u - v‖ = ⨅ (w : { x // x ∈ K }), ‖u - ↑w‖
case mpr
𝕜 : Type u_2
E : Type u_1
F : Type ?u.265347
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
u v : E
hv : v ∈ K
this✝ : InnerProductSpace ℝ E := InnerProductSpace.isROrCToReal 𝕜 E
this : Module ℝ E := RestrictScalars.module ℝ 𝕜 E
K' : Submodule ℝ E := Submodule.restrictScalars ℝ K
H : ∀ (w : E), w ∈ K → inner (u - v) w = 0
⊢ ‖u - v‖ = ⨅ (w : { x // x ∈ K }), ‖u - ↑w‖
have : ∀ w ∈ K', ⟪u - v, w⟫_ℝ = 0 := by
  intro w hw
  rw [real_inner_eq_re_inner, H w hw]
  exact zero_re'
no goals
case mpr
𝕜 : Type u_2
E : Type u_1
F : Type ?u.265347
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
u v : E
hv : v ∈ K
this✝¹ : InnerProductSpace ℝ E := InnerProductSpace.isROrCToReal 𝕜 E
this✝ : Module ℝ E := RestrictScalars.module ℝ 𝕜 E
K' : Submodule ℝ E := Submodule.restrictScalars ℝ K
H : ∀ (w : E), w ∈ K → inner (u - v) w = 0
this : ∀ (w : E), w ∈ K' → inner (u - v) w = 0
⊢ ‖u - v‖ = ⨅ (w : { x // x ∈ K }), ‖u - ↑w‖
exact (norm_eq_iInf_iff_real_inner_eq_zero K' hv).2 this
𝕜 : Type u_2
E : Type u_1
F : Type ?u.265347
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
u v : E
hv : v ∈ K
this✝ : InnerProductSpace ℝ E := InnerProductSpace.isROrCToReal 𝕜 E
this : Module ℝ E := RestrictScalars.module ℝ 𝕜 E
K' : Submodule ℝ E := Submodule.restrictScalars ℝ K
H : ∀ (w : E), w ∈ K → inner (u - v) w = 0
w : E
hw : w ∈ K'
⊢ inner (u - v) w = 0
𝕜 : Type u_2
E : Type u_1
F : Type ?u.265347
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
u v : E
hv : v ∈ K
this✝ : InnerProductSpace ℝ E := InnerProductSpace.isROrCToReal 𝕜 E
this : Module ℝ E := RestrictScalars.module ℝ 𝕜 E
K' : Submodule ℝ E := Submodule.restrictScalars ℝ K
H : ∀ (w : E), w ∈ K → inner (u - v) w = 0
⊢ ∀ (w : E), w ∈ K' → inner (u - v) w = 0
intro w hw
𝕜 : Type u_2
E : Type u_1
F : Type ?u.265347
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
u v : E
hv : v ∈ K
this✝ : InnerProductSpace ℝ E := InnerProductSpace.isROrCToReal 𝕜 E
this : Module ℝ E := RestrictScalars.module ℝ 𝕜 E
K' : Submodule ℝ E := Submodule.restrictScalars ℝ K
H : ∀ (w : E), w ∈ K → inner (u - v) w = 0
w : E
hw : w ∈ K'
⊢ ↑re 0 = 0
𝕜 : Type u_2
E : Type u_1
F : Type ?u.265347
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
u v : E
hv : v ∈ K
this✝ : InnerProductSpace ℝ E := InnerProductSpace.isROrCToReal 𝕜 E
this : Module ℝ E := RestrictScalars.module ℝ 𝕜 E
K' : Submodule ℝ E := Submodule.restrictScalars ℝ K
H : ∀ (w : E), w ∈ K → inner (u - v) w = 0
w : E
hw : w ∈ K'
⊢ inner (u - v) w = 0
rw [real_inner_eq_re_inner, H w hw]
no goals
𝕜 : Type u_2
E : Type u_1
F : Type ?u.265347
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
u v : E
hv : v ∈ K
this✝ : InnerProductSpace ℝ E := InnerProductSpace.isROrCToReal 𝕜 E
this : Module ℝ E := RestrictScalars.module ℝ 𝕜 E
K' : Submodule ℝ E := Submodule.restrictScalars ℝ K
H : ∀ (w : E), w ∈ K → inner (u - v) w = 0
w : E
hw : w ∈ K'
⊢ ↑re 0 = 0
exact zero_re'