𝕜 : Type u_1
E : Type u_2
F : Type ?u.1095350
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
v : Set E
hv : Orthonormal 𝕜 Subtype.val
⊢ (∀ (u : Set E), u ⊇ v → Orthonormal 𝕜 Subtype.val → u = v) ↔ ∀ (x : E), x ∈ (span 𝕜 v)ᗮ → x = 0
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1095350
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
v : Set E
hv : Orthonormal 𝕜 Subtype.val
⊢ (∀ (u : Set E), u ⊇ v → Orthonormal 𝕜 Subtype.val → u = v) ↔ (span 𝕜 v)ᗮ = ⊥
rw [Submodule.eq_bot_iff]
case mp
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1095350
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
v : Set E
hv : Orthonormal 𝕜 Subtype.val
⊢ (∀ (u : Set E), u ⊇ v → Orthonormal 𝕜 Subtype.val → u = v) → ∀ (x : E), x ∈ (span 𝕜 v)ᗮ → x = 0

case mpr
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1095350
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
v : Set E
hv : Orthonormal 𝕜 Subtype.val
⊢ (∀ (x : E), x ∈ (span 𝕜 v)ᗮ → x = 0) → ∀ (u : Set E), u ⊇ v → Orthonormal 𝕜 Subtype.val → u = v
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1095350
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
v : Set E
hv : Orthonormal 𝕜 Subtype.val
⊢ (∀ (u : Set E), u ⊇ v → Orthonormal 𝕜 Subtype.val → u = v) ↔ ∀ (x : E), x ∈ (span 𝕜 v)ᗮ → x = 0
constructor
case mp
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1095350
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
v : Set E
hv : Orthonormal 𝕜 Subtype.val
⊢ (∃ x, x ∈ (span 𝕜 v)ᗮ ∧ x ≠ 0) → ∃ u, u ⊇ v ∧ Orthonormal 𝕜 Subtype.val ∧ u ≠ v
case mp
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1095350
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
v : Set E
hv : Orthonormal 𝕜 Subtype.val
⊢ (∀ (u : Set E), u ⊇ v → Orthonormal 𝕜 Subtype.val → u = v) → ∀ (x : E), x ∈ (span 𝕜 v)ᗮ → x = 0
contrapose!
case mp.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1095350
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
v : Set E
hv : Orthonormal 𝕜 Subtype.val
x : E
hx' : x ∈ (span 𝕜 v)ᗮ
hx : x ≠ 0
⊢ ∃ u, u ⊇ v ∧ Orthonormal 𝕜 Subtype.val ∧ u ≠ v
case mp
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1095350
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
v : Set E
hv : Orthonormal 𝕜 Subtype.val
⊢ (∃ x, x ∈ (span 𝕜 v)ᗮ ∧ x ≠ 0) → ∃ u, u ⊇ v ∧ Orthonormal 𝕜 Subtype.val ∧ u ≠ v
rintro ⟨x, hx', hx⟩
case mp.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1095350
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
v : Set E
hv : Orthonormal 𝕜 Subtype.val
x : E
hx' : x ∈ (span 𝕜 v)ᗮ
hx : x ≠ 0
e : E := (↑‖x‖)⁻¹ • x
⊢ ∃ u, u ⊇ v ∧ Orthonormal 𝕜 Subtype.val ∧ u ≠ v
case mp.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1095350
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
v : Set E
hv : Orthonormal 𝕜 Subtype.val
x : E
hx' : x ∈ (span 𝕜 v)ᗮ
hx : x ≠ 0
⊢ ∃ u, u ⊇ v ∧ Orthonormal 𝕜 Subtype.val ∧ u ≠ v
let e := (‖x‖⁻¹ : 𝕜) • x
case mp.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1095350
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
v : Set E
hv : Orthonormal 𝕜 Subtype.val
x : E
hx' : x ∈ (span 𝕜 v)ᗮ
hx : x ≠ 0
e : E := (↑‖x‖)⁻¹ • x
he : ‖e‖ = 1
⊢ ∃ u, u ⊇ v ∧ Orthonormal 𝕜 Subtype.val ∧ u ≠ v
case mp.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1095350
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
v : Set E
hv : Orthonormal 𝕜 Subtype.val
x : E
hx' : x ∈ (span 𝕜 v)ᗮ
hx : x ≠ 0
e : E := (↑‖x‖)⁻¹ • x
⊢ ∃ u, u ⊇ v ∧ Orthonormal 𝕜 Subtype.val ∧ u ≠ v
have he : ‖e‖ = 1 := by simp [norm_smul_inv_norm hx]
case mp.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1095350
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
v : Set E
hv : Orthonormal 𝕜 Subtype.val
x : E
hx' : x ∈ (span 𝕜 v)ᗮ
hx : x ≠ 0
e : E := (↑‖x‖)⁻¹ • x
he : ‖e‖ = 1
he' : e ∈ (span 𝕜 v)ᗮ
⊢ ∃ u, u ⊇ v ∧ Orthonormal 𝕜 Subtype.val ∧ u ≠ v
case mp.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1095350
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
v : Set E
hv : Orthonormal 𝕜 Subtype.val
x : E
hx' : x ∈ (span 𝕜 v)ᗮ
hx : x ≠ 0
e : E := (↑‖x‖)⁻¹ • x
he : ‖e‖ = 1
⊢ ∃ u, u ⊇ v ∧ Orthonormal 𝕜 Subtype.val ∧ u ≠ v
have he' : e ∈ (span 𝕜 v)ᗮ := smul_mem' _ _ hx'
case mp.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1095350
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
v : Set E
hv : Orthonormal 𝕜 Subtype.val
x : E
hx' : x ∈ (span 𝕜 v)ᗮ
hx : x ≠ 0
e : E := (↑‖x‖)⁻¹ • x
he : ‖e‖ = 1
he' : e ∈ (span 𝕜 v)ᗮ
he'' : ¬e ∈ v
⊢ ∃ u, u ⊇ v ∧ Orthonormal 𝕜 Subtype.val ∧ u ≠ v
case mp.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1095350
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
v : Set E
hv : Orthonormal 𝕜 Subtype.val
x : E
hx' : x ∈ (span 𝕜 v)ᗮ
hx : x ≠ 0
e : E := (↑‖x‖)⁻¹ • x
he : ‖e‖ = 1
he' : e ∈ (span 𝕜 v)ᗮ
⊢ ∃ u, u ⊇ v ∧ Orthonormal 𝕜 Subtype.val ∧ u ≠ v
have he'' : e ∉ v := by
  intro hev
  have : e = 0 := by
    have : e ∈ span 𝕜 v ⊓ (span 𝕜 v)ᗮ := ⟨subset_span hev, he'⟩
    simpa [(span 𝕜 v).inf_orthogonal_eq_bot] using this
  have : e ≠ 0 := hv.ne_zero ⟨e, hev⟩
  contradiction
case mp.intro.intro.refine'_1
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1095350
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
v : Set E
hv : Orthonormal 𝕜 Subtype.val
x : E
hx' : x ∈ (span 𝕜 v)ᗮ
hx : x ≠ 0
e : E := (↑‖x‖)⁻¹ • x
he : ‖e‖ = 1
he' : e ∈ (span 𝕜 v)ᗮ
he'' : ¬e ∈ v
⊢ ∀ (i : { x // x ∈ insert e v }), ‖↑i‖ = 1

case mp.intro.intro.refine'_2
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1095350
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
v : Set E
hv : Orthonormal 𝕜 Subtype.val
x : E
hx' : x ∈ (span 𝕜 v)ᗮ
hx : x ≠ 0
e : E := (↑‖x‖)⁻¹ • x
he : ‖e‖ = 1
he' : e ∈ (span 𝕜 v)ᗮ
he'' : ¬e ∈ v
⊢ ∀ {i j : { x // x ∈ insert e v }}, i ≠ j → inner ↑i ↑j = 0
case mp.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1095350
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
v : Set E
hv : Orthonormal 𝕜 Subtype.val
x : E
hx' : x ∈ (span 𝕜 v)ᗮ
hx : x ≠ 0
e : E := (↑‖x‖)⁻¹ • x
he : ‖e‖ = 1
he' : e ∈ (span 𝕜 v)ᗮ
he'' : ¬e ∈ v
⊢ ∃ u, u ⊇ v ∧ Orthonormal 𝕜 Subtype.val ∧ u ≠ v
refine' ⟨insert e v, v.subset_insert e, ⟨_, _⟩, (ne_insert_of_not_mem v he'').symm⟩
no goals
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1095350
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
v : Set E
hv : Orthonormal 𝕜 Subtype.val
x : E
hx' : x ∈ (span 𝕜 v)ᗮ
hx : x ≠ 0
e : E := (↑‖x‖)⁻¹ • x
⊢ ‖e‖ = 1
simp [norm_smul_inv_norm hx]
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1095350
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
v : Set E
hv : Orthonormal 𝕜 Subtype.val
x : E
hx' : x ∈ (span 𝕜 v)ᗮ
hx : x ≠ 0
e : E := (↑‖x‖)⁻¹ • x
he : ‖e‖ = 1
he' : e ∈ (span 𝕜 v)ᗮ
hev : e ∈ v
⊢ False
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1095350
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
v : Set E
hv : Orthonormal 𝕜 Subtype.val
x : E
hx' : x ∈ (span 𝕜 v)ᗮ
hx : x ≠ 0
e : E := (↑‖x‖)⁻¹ • x
he : ‖e‖ = 1
he' : e ∈ (span 𝕜 v)ᗮ
⊢ ¬e ∈ v
intro hev
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1095350
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
v : Set E
hv : Orthonormal 𝕜 Subtype.val
x : E
hx' : x ∈ (span 𝕜 v)ᗮ
hx : x ≠ 0
e : E := (↑‖x‖)⁻¹ • x
he : ‖e‖ = 1
he' : e ∈ (span 𝕜 v)ᗮ
hev : e ∈ v
this : e = 0
⊢ False
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1095350
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
v : Set E
hv : Orthonormal 𝕜 Subtype.val
x : E
hx' : x ∈ (span 𝕜 v)ᗮ
hx : x ≠ 0
e : E := (↑‖x‖)⁻¹ • x
he : ‖e‖ = 1
he' : e ∈ (span 𝕜 v)ᗮ
hev : e ∈ v
⊢ False
have : e = 0 := by
  have : e ∈ span 𝕜 v ⊓ (span 𝕜 v)ᗮ := ⟨subset_span hev, he'⟩
  simpa [(span 𝕜 v).inf_orthogonal_eq_bot] using this
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1095350
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
v : Set E
hv : Orthonormal 𝕜 Subtype.val
x : E
hx' : x ∈ (span 𝕜 v)ᗮ
hx : x ≠ 0
e : E := (↑‖x‖)⁻¹ • x
he : ‖e‖ = 1
he' : e ∈ (span 𝕜 v)ᗮ
hev : e ∈ v
this✝ : e = 0
this : e ≠ 0
⊢ False
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1095350
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
v : Set E
hv : Orthonormal 𝕜 Subtype.val
x : E
hx' : x ∈ (span 𝕜 v)ᗮ
hx : x ≠ 0
e : E := (↑‖x‖)⁻¹ • x
he : ‖e‖ = 1
he' : e ∈ (span 𝕜 v)ᗮ
hev : e ∈ v
this : e = 0
⊢ False
have : e ≠ 0 := hv.ne_zero ⟨e, hev⟩
no goals
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1095350
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
v : Set E
hv : Orthonormal 𝕜 Subtype.val
x : E
hx' : x ∈ (span 𝕜 v)ᗮ
hx : x ≠ 0
e : E := (↑‖x‖)⁻¹ • x
he : ‖e‖ = 1
he' : e ∈ (span 𝕜 v)ᗮ
hev : e ∈ v
this✝ : e = 0
this : e ≠ 0
⊢ False
contradiction
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1095350
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
v : Set E
hv : Orthonormal 𝕜 Subtype.val
x : E
hx' : x ∈ (span 𝕜 v)ᗮ
hx : x ≠ 0
e : E := (↑‖x‖)⁻¹ • x
he : ‖e‖ = 1
he' : e ∈ (span 𝕜 v)ᗮ
hev : e ∈ v
this : e ∈ span 𝕜 v ⊓ (span 𝕜 v)ᗮ
⊢ e = 0
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1095350
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
v : Set E
hv : Orthonormal 𝕜 Subtype.val
x : E
hx' : x ∈ (span 𝕜 v)ᗮ
hx : x ≠ 0
e : E := (↑‖x‖)⁻¹ • x
he : ‖e‖ = 1
he' : e ∈ (span 𝕜 v)ᗮ
hev : e ∈ v
⊢ e = 0
have : e ∈ span 𝕜 v ⊓ (span 𝕜 v)ᗮ := ⟨subset_span hev, he'⟩
no goals
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1095350
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
v : Set E
hv : Orthonormal 𝕜 Subtype.val
x : E
hx' : x ∈ (span 𝕜 v)ᗮ
hx : x ≠ 0
e : E := (↑‖x‖)⁻¹ • x
he : ‖e‖ = 1
he' : e ∈ (span 𝕜 v)ᗮ
hev : e ∈ v
this : e ∈ span 𝕜 v ⊓ (span 𝕜 v)ᗮ
⊢ e = 0
simpa [(span 𝕜 v).inf_orthogonal_eq_bot] using this
case mp.intro.intro.refine'_1.mk
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1095350
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
v : Set E
hv : Orthonormal 𝕜 Subtype.val
x : E
hx' : x ∈ (span 𝕜 v)ᗮ
hx : x ≠ 0
e : E := (↑‖x‖)⁻¹ • x
he : ‖e‖ = 1
he' : e ∈ (span 𝕜 v)ᗮ
he'' : ¬e ∈ v
a : E
ha' : a ∈ insert e v
⊢ ‖↑{ val := a, property := ha' }‖ = 1
case mp.intro.intro.refine'_1
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1095350
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
v : Set E
hv : Orthonormal 𝕜 Subtype.val
x : E
hx' : x ∈ (span 𝕜 v)ᗮ
hx : x ≠ 0
e : E := (↑‖x‖)⁻¹ • x
he : ‖e‖ = 1
he' : e ∈ (span 𝕜 v)ᗮ
he'' : ¬e ∈ v
⊢ ∀ (i : { x // x ∈ insert e v }), ‖↑i‖ = 1
rintro ⟨a, ha'⟩
case mp.intro.intro.refine'_1.mk.inl
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1095350
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
v : Set E
hv : Orthonormal 𝕜 Subtype.val
x : E
hx' : x ∈ (span 𝕜 v)ᗮ
hx : x ≠ 0
e : E := (↑‖x‖)⁻¹ • x
he : ‖e‖ = 1
he' : e ∈ (span 𝕜 v)ᗮ
he'' : ¬e ∈ v
a : E
ha' : a ∈ insert e v
ha : a = e
⊢ ‖↑{ val := a, property := ha' }‖ = 1

case mp.intro.intro.refine'_1.mk.inr
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1095350
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
v : Set E
hv : Orthonormal 𝕜 Subtype.val
x : E
hx' : x ∈ (span 𝕜 v)ᗮ
hx : x ≠ 0
e : E := (↑‖x‖)⁻¹ • x
he : ‖e‖ = 1
he' : e ∈ (span 𝕜 v)ᗮ
he'' : ¬e ∈ v
a : E
ha' : a ∈ insert e v
ha : a ∈ v
⊢ ‖↑{ val := a, property := ha' }‖ = 1
case mp.intro.intro.refine'_1.mk
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1095350
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
v : Set E
hv : Orthonormal 𝕜 Subtype.val
x : E
hx' : x ∈ (span 𝕜 v)ᗮ
hx : x ≠ 0
e : E := (↑‖x‖)⁻¹ • x
he : ‖e‖ = 1
he' : e ∈ (span 𝕜 v)ᗮ
he'' : ¬e ∈ v
a : E
ha' : a ∈ insert e v
⊢ ‖↑{ val := a, property := ha' }‖ = 1
cases' eq_or_mem_of_mem_insert ha' with ha ha
no goals
case mp.intro.intro.refine'_1.mk.inl
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1095350
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
v : Set E
hv : Orthonormal 𝕜 Subtype.val
x : E
hx' : x ∈ (span 𝕜 v)ᗮ
hx : x ≠ 0
e : E := (↑‖x‖)⁻¹ • x
he : ‖e‖ = 1
he' : e ∈ (span 𝕜 v)ᗮ
he'' : ¬e ∈ v
a : E
ha' : a ∈ insert e v
ha : a = e
⊢ ‖↑{ val := a, property := ha' }‖ = 1
simp [ha, he]
no goals
case mp.intro.intro.refine'_1.mk.inr
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1095350
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
v : Set E
hv : Orthonormal 𝕜 Subtype.val
x : E
hx' : x ∈ (span 𝕜 v)ᗮ
hx : x ≠ 0
e : E := (↑‖x‖)⁻¹ • x
he : ‖e‖ = 1
he' : e ∈ (span 𝕜 v)ᗮ
he'' : ¬e ∈ v
a : E
ha' : a ∈ insert e v
ha : a ∈ v
⊢ ‖↑{ val := a, property := ha' }‖ = 1
exact hv.1 ⟨a, ha⟩
case mp.intro.intro.refine'_2
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1095350
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
v : Set E
hv : Orthonormal 𝕜 Subtype.val
x : E
hx' : x ∈ (span 𝕜 v)ᗮ
hx : x ≠ 0
e : E := (↑‖x‖)⁻¹ • x
he : ‖e‖ = 1
he' : e ∈ (span 𝕜 v)ᗮ
he'' : ¬e ∈ v
h_end : ∀ (a : E), a ∈ v → inner a e = 0
⊢ ∀ {i j : { x // x ∈ insert e v }}, i ≠ j → inner ↑i ↑j = 0
case mp.intro.intro.refine'_2
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1095350
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
v : Set E
hv : Orthonormal 𝕜 Subtype.val
x : E
hx' : x ∈ (span 𝕜 v)ᗮ
hx : x ≠ 0
e : E := (↑‖x‖)⁻¹ • x
he : ‖e‖ = 1
he' : e ∈ (span 𝕜 v)ᗮ
he'' : ¬e ∈ v
⊢ ∀ {i j : { x // x ∈ insert e v }}, i ≠ j → inner ↑i ↑j = 0
have h_end : ∀ a ∈ v, ⟪a, e⟫ = 0 := by
  intro a ha
  exact he' a (Submodule.subset_span ha)
case mp.intro.intro.refine'_2.mk
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1095350
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
v : Set E
hv : Orthonormal 𝕜 Subtype.val
x : E
hx' : x ∈ (span 𝕜 v)ᗮ
hx : x ≠ 0
e : E := (↑‖x‖)⁻¹ • x
he : ‖e‖ = 1
he' : e ∈ (span 𝕜 v)ᗮ
he'' : ¬e ∈ v
h_end : ∀ (a : E), a ∈ v → inner a e = 0
a : E
ha' : a ∈ insert e v
⊢ ∀ {j : { x // x ∈ insert e v }}, { val := a, property := ha' } ≠ j → inner ↑{ val := a, property := ha' } ↑j = 0
case mp.intro.intro.refine'_2
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1095350
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
v : Set E
hv : Orthonormal 𝕜 Subtype.val
x : E
hx' : x ∈ (span 𝕜 v)ᗮ
hx : x ≠ 0
e : E := (↑‖x‖)⁻¹ • x
he : ‖e‖ = 1
he' : e ∈ (span 𝕜 v)ᗮ
he'' : ¬e ∈ v
h_end : ∀ (a : E), a ∈ v → inner a e = 0
⊢ ∀ {i j : { x // x ∈ insert e v }}, i ≠ j → inner ↑i ↑j = 0
rintro ⟨a, ha'⟩
case mp.intro.intro.refine'_2.mk.inl
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1095350
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
v : Set E
hv : Orthonormal 𝕜 Subtype.val
x : E
hx' : x ∈ (span 𝕜 v)ᗮ
hx : x ≠ 0
e : E := (↑‖x‖)⁻¹ • x
he : ‖e‖ = 1
he' : e ∈ (span 𝕜 v)ᗮ
he'' : ¬e ∈ v
h_end : ∀ (a : E), a ∈ v → inner a e = 0
a : E
ha' : a ∈ insert e v
ha : a = e
⊢ ∀ {j : { x // x ∈ insert e v }}, { val := a, property := ha' } ≠ j → inner ↑{ val := a, property := ha' } ↑j = 0

case mp.intro.intro.refine'_2.mk.inr
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1095350
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
v : Set E
hv : Orthonormal 𝕜 Subtype.val
x : E
hx' : x ∈ (span 𝕜 v)ᗮ
hx : x ≠ 0
e : E := (↑‖x‖)⁻¹ • x
he : ‖e‖ = 1
he' : e ∈ (span 𝕜 v)ᗮ
he'' : ¬e ∈ v
h_end : ∀ (a : E), a ∈ v → inner a e = 0
a : E
ha' : a ∈ insert e v
ha : a ∈ v
⊢ ∀ {j : { x // x ∈ insert e v }}, { val := a, property := ha' } ≠ j → inner ↑{ val := a, property := ha' } ↑j = 0
case mp.intro.intro.refine'_2.mk
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1095350
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
v : Set E
hv : Orthonormal 𝕜 Subtype.val
x : E
hx' : x ∈ (span 𝕜 v)ᗮ
hx : x ≠ 0
e : E := (↑‖x‖)⁻¹ • x
he : ‖e‖ = 1
he' : e ∈ (span 𝕜 v)ᗮ
he'' : ¬e ∈ v
h_end : ∀ (a : E), a ∈ v → inner a e = 0
a : E
ha' : a ∈ insert e v
⊢ ∀ {j : { x // x ∈ insert e v }}, { val := a, property := ha' } ≠ j → inner ↑{ val := a, property := ha' } ↑j = 0
cases' eq_or_mem_of_mem_insert ha' with ha ha
case mp.intro.intro.refine'_2.mk.inr.mk
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1095350
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
v : Set E
hv : Orthonormal 𝕜 Subtype.val
x : E
hx' : x ∈ (span 𝕜 v)ᗮ
hx : x ≠ 0
e : E := (↑‖x‖)⁻¹ • x
he : ‖e‖ = 1
he' : e ∈ (span 𝕜 v)ᗮ
he'' : ¬e ∈ v
h_end : ∀ (a : E), a ∈ v → inner a e = 0
a : E
ha' : a ∈ insert e v
ha : a ∈ v
b : E
hb' : b ∈ insert e v
hab' : { val := a, property := ha' } ≠ { val := b, property := hb' }
⊢ inner ↑{ val := a, property := ha' } ↑{ val := b, property := hb' } = 0
case mp.intro.intro.refine'_2.mk.inr
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1095350
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
v : Set E
hv : Orthonormal 𝕜 Subtype.val
x : E
hx' : x ∈ (span 𝕜 v)ᗮ
hx : x ≠ 0
e : E := (↑‖x‖)⁻¹ • x
he : ‖e‖ = 1
he' : e ∈ (span 𝕜 v)ᗮ
he'' : ¬e ∈ v
h_end : ∀ (a : E), a ∈ v → inner a e = 0
a : E
ha' : a ∈ insert e v
ha : a ∈ v
⊢ ∀ {j : { x // x ∈ insert e v }}, { val := a, property := ha' } ≠ j → inner ↑{ val := a, property := ha' } ↑j = 0
rintro ⟨b, hb'⟩ hab'
case mp.intro.intro.refine'_2.mk.inr.mk.inl
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1095350
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
v : Set E
hv : Orthonormal 𝕜 Subtype.val
x : E
hx' : x ∈ (span 𝕜 v)ᗮ
hx : x ≠ 0
e : E := (↑‖x‖)⁻¹ • x
he : ‖e‖ = 1
he' : e ∈ (span 𝕜 v)ᗮ
he'' : ¬e ∈ v
h_end : ∀ (a : E), a ∈ v → inner a e = 0
a : E
ha' : a ∈ insert e v
ha : a ∈ v
b : E
hb' : b ∈ insert e v
hab' : { val := a, property := ha' } ≠ { val := b, property := hb' }
hb : b = e
⊢ inner ↑{ val := a, property := ha' } ↑{ val := b, property := hb' } = 0

case mp.intro.intro.refine'_2.mk.inr.mk.inr
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1095350
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
v : Set E
hv : Orthonormal 𝕜 Subtype.val
x : E
hx' : x ∈ (span 𝕜 v)ᗮ
hx : x ≠ 0
e : E := (↑‖x‖)⁻¹ • x
he : ‖e‖ = 1
he' : e ∈ (span 𝕜 v)ᗮ
he'' : ¬e ∈ v
h_end : ∀ (a : E), a ∈ v → inner a e = 0
a : E
ha' : a ∈ insert e v
ha : a ∈ v
b : E
hb' : b ∈ insert e v
hab' : { val := a, property := ha' } ≠ { val := b, property := hb' }
hb : b ∈ v
⊢ inner ↑{ val := a, property := ha' } ↑{ val := b, property := hb' } = 0
case mp.intro.intro.refine'_2.mk.inr.mk
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1095350
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
v : Set E
hv : Orthonormal 𝕜 Subtype.val
x : E
hx' : x ∈ (span 𝕜 v)ᗮ
hx : x ≠ 0
e : E := (↑‖x‖)⁻¹ • x
he : ‖e‖ = 1
he' : e ∈ (span 𝕜 v)ᗮ
he'' : ¬e ∈ v
h_end : ∀ (a : E), a ∈ v → inner a e = 0
a : E
ha' : a ∈ insert e v
ha : a ∈ v
b : E
hb' : b ∈ insert e v
hab' : { val := a, property := ha' } ≠ { val := b, property := hb' }
⊢ inner ↑{ val := a, property := ha' } ↑{ val := b, property := hb' } = 0
cases' eq_or_mem_of_mem_insert hb' with hb hb
case mp.intro.intro.refine'_2.mk.inr.mk.inr
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1095350
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
v : Set E
hv : Orthonormal 𝕜 Subtype.val
x : E
hx' : x ∈ (span 𝕜 v)ᗮ
hx : x ≠ 0
e : E := (↑‖x‖)⁻¹ • x
he : ‖e‖ = 1
he' : e ∈ (span 𝕜 v)ᗮ
he'' : ¬e ∈ v
h_end : ∀ (a : E), a ∈ v → inner a e = 0
a : E
ha' : a ∈ insert e v
ha : a ∈ v
b : E
hb' : b ∈ insert e v
hab' : { val := a, property := ha' } ≠ { val := b, property := hb' }
hb : b ∈ v
this : { val := a, property := ha } ≠ { val := b, property := hb }
⊢ inner ↑{ val := a, property := ha' } ↑{ val := b, property := hb' } = 0
case mp.intro.intro.refine'_2.mk.inr.mk.inr
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1095350
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
v : Set E
hv : Orthonormal 𝕜 Subtype.val
x : E
hx' : x ∈ (span 𝕜 v)ᗮ
hx : x ≠ 0
e : E := (↑‖x‖)⁻¹ • x
he : ‖e‖ = 1
he' : e ∈ (span 𝕜 v)ᗮ
he'' : ¬e ∈ v
h_end : ∀ (a : E), a ∈ v → inner a e = 0
a : E
ha' : a ∈ insert e v
ha : a ∈ v
b : E
hb' : b ∈ insert e v
hab' : { val := a, property := ha' } ≠ { val := b, property := hb' }
hb : b ∈ v
⊢ inner ↑{ val := a, property := ha' } ↑{ val := b, property := hb' } = 0
have : (⟨a, ha⟩ : v) ≠ ⟨b, hb⟩ := by
  intro hab''
  apply hab'
  simpa using hab''
no goals
case mp.intro.intro.refine'_2.mk.inr.mk.inr
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1095350
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
v : Set E
hv : Orthonormal 𝕜 Subtype.val
x : E
hx' : x ∈ (span 𝕜 v)ᗮ
hx : x ≠ 0
e : E := (↑‖x‖)⁻¹ • x
he : ‖e‖ = 1
he' : e ∈ (span 𝕜 v)ᗮ
he'' : ¬e ∈ v
h_end : ∀ (a : E), a ∈ v → inner a e = 0
a : E
ha' : a ∈ insert e v
ha : a ∈ v
b : E
hb' : b ∈ insert e v
hab' : { val := a, property := ha' } ≠ { val := b, property := hb' }
hb : b ∈ v
this : { val := a, property := ha } ≠ { val := b, property := hb }
⊢ inner ↑{ val := a, property := ha' } ↑{ val := b, property := hb' } = 0
exact hv.2 this
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1095350
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
v : Set E
hv : Orthonormal 𝕜 Subtype.val
x : E
hx' : x ∈ (span 𝕜 v)ᗮ
hx : x ≠ 0
e : E := (↑‖x‖)⁻¹ • x
he : ‖e‖ = 1
he' : e ∈ (span 𝕜 v)ᗮ
he'' : ¬e ∈ v
a : E
ha : a ∈ v
⊢ inner a e = 0
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1095350
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
v : Set E
hv : Orthonormal 𝕜 Subtype.val
x : E
hx' : x ∈ (span 𝕜 v)ᗮ
hx : x ≠ 0
e : E := (↑‖x‖)⁻¹ • x
he : ‖e‖ = 1
he' : e ∈ (span 𝕜 v)ᗮ
he'' : ¬e ∈ v
⊢ ∀ (a : E), a ∈ v → inner a e = 0
intro a ha
no goals
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1095350
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
v : Set E
hv : Orthonormal 𝕜 Subtype.val
x : E
hx' : x ∈ (span 𝕜 v)ᗮ
hx : x ≠ 0
e : E := (↑‖x‖)⁻¹ • x
he : ‖e‖ = 1
he' : e ∈ (span 𝕜 v)ᗮ
he'' : ¬e ∈ v
a : E
ha : a ∈ v
⊢ inner a e = 0
exact he' a (Submodule.subset_span ha)
case mp.intro.intro.refine'_2.mk.inl.mk
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1095350
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
v : Set E
hv : Orthonormal 𝕜 Subtype.val
x : E
hx' : x ∈ (span 𝕜 v)ᗮ
hx : x ≠ 0
e : E := (↑‖x‖)⁻¹ • x
he : ‖e‖ = 1
he' : e ∈ (span 𝕜 v)ᗮ
he'' : ¬e ∈ v
h_end : ∀ (a : E), a ∈ v → inner a e = 0
a : E
ha' : a ∈ insert e v
ha : a = e
b : E
hb' : b ∈ insert e v
hab' : { val := a, property := ha' } ≠ { val := b, property := hb' }
⊢ inner ↑{ val := a, property := ha' } ↑{ val := b, property := hb' } = 0
case mp.intro.intro.refine'_2.mk.inl
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1095350
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
v : Set E
hv : Orthonormal 𝕜 Subtype.val
x : E
hx' : x ∈ (span 𝕜 v)ᗮ
hx : x ≠ 0
e : E := (↑‖x‖)⁻¹ • x
he : ‖e‖ = 1
he' : e ∈ (span 𝕜 v)ᗮ
he'' : ¬e ∈ v
h_end : ∀ (a : E), a ∈ v → inner a e = 0
a : E
ha' : a ∈ insert e v
ha : a = e
⊢ ∀ {j : { x // x ∈ insert e v }}, { val := a, property := ha' } ≠ j → inner ↑{ val := a, property := ha' } ↑j = 0
rintro ⟨b, hb'⟩ hab'
case mp.intro.intro.refine'_2.mk.inl.mk
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1095350
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
v : Set E
hv : Orthonormal 𝕜 Subtype.val
x : E
hx' : x ∈ (span 𝕜 v)ᗮ
hx : x ≠ 0
e : E := (↑‖x‖)⁻¹ • x
he : ‖e‖ = 1
he' : e ∈ (span 𝕜 v)ᗮ
he'' : ¬e ∈ v
h_end : ∀ (a : E), a ∈ v → inner a e = 0
a : E
ha' : a ∈ insert e v
ha : a = e
b : E
hb' : b ∈ insert e v
hab' : { val := a, property := ha' } ≠ { val := b, property := hb' }
hb : b ∈ v
⊢ inner ↑{ val := a, property := ha' } ↑{ val := b, property := hb' } = 0
case mp.intro.intro.refine'_2.mk.inl.mk
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1095350
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
v : Set E
hv : Orthonormal 𝕜 Subtype.val
x : E
hx' : x ∈ (span 𝕜 v)ᗮ
hx : x ≠ 0
e : E := (↑‖x‖)⁻¹ • x
he : ‖e‖ = 1
he' : e ∈ (span 𝕜 v)ᗮ
he'' : ¬e ∈ v
h_end : ∀ (a : E), a ∈ v → inner a e = 0
a : E
ha' : a ∈ insert e v
ha : a = e
b : E
hb' : b ∈ insert e v
hab' : { val := a, property := ha' } ≠ { val := b, property := hb' }
⊢ inner ↑{ val := a, property := ha' } ↑{ val := b, property := hb' } = 0
have hb : b ∈ v := by
  refine' mem_of_mem_insert_of_ne hb' _
  intro hbe'
  apply hab'
  simp [ha, hbe']
case mp.intro.intro.refine'_2.mk.inl.mk
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1095350
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
v : Set E
hv : Orthonormal 𝕜 Subtype.val
x : E
hx' : x ∈ (span 𝕜 v)ᗮ
hx : x ≠ 0
e : E := (↑‖x‖)⁻¹ • x
he : ‖e‖ = 1
he' : e ∈ (span 𝕜 v)ᗮ
he'' : ¬e ∈ v
h_end : ∀ (a : E), a ∈ v → inner a e = 0
a : E
ha' : a ∈ insert e v
ha : a = e
b : E
hb' : b ∈ insert e v
hab' : { val := a, property := ha' } ≠ { val := b, property := hb' }
hb : b ∈ v
⊢ inner ↑{ val := b, property := hb' } ↑{ val := a, property := ha' } = 0
case mp.intro.intro.refine'_2.mk.inl.mk
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1095350
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
v : Set E
hv : Orthonormal 𝕜 Subtype.val
x : E
hx' : x ∈ (span 𝕜 v)ᗮ
hx : x ≠ 0
e : E := (↑‖x‖)⁻¹ • x
he : ‖e‖ = 1
he' : e ∈ (span 𝕜 v)ᗮ
he'' : ¬e ∈ v
h_end : ∀ (a : E), a ∈ v → inner a e = 0
a : E
ha' : a ∈ insert e v
ha : a = e
b : E
hb' : b ∈ insert e v
hab' : { val := a, property := ha' } ≠ { val := b, property := hb' }
hb : b ∈ v
⊢ inner ↑{ val := a, property := ha' } ↑{ val := b, property := hb' } = 0
rw [inner_eq_zero_symm]
no goals
case mp.intro.intro.refine'_2.mk.inl.mk
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1095350
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
v : Set E
hv : Orthonormal 𝕜 Subtype.val
x : E
hx' : x ∈ (span 𝕜 v)ᗮ
hx : x ≠ 0
e : E := (↑‖x‖)⁻¹ • x
he : ‖e‖ = 1
he' : e ∈ (span 𝕜 v)ᗮ
he'' : ¬e ∈ v
h_end : ∀ (a : E), a ∈ v → inner a e = 0
a : E
ha' : a ∈ insert e v
ha : a = e
b : E
hb' : b ∈ insert e v
hab' : { val := a, property := ha' } ≠ { val := b, property := hb' }
hb : b ∈ v
⊢ inner ↑{ val := b, property := hb' } ↑{ val := a, property := ha' } = 0
simpa [ha] using h_end b hb
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1095350
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
v : Set E
hv : Orthonormal 𝕜 Subtype.val
x : E
hx' : x ∈ (span 𝕜 v)ᗮ
hx : x ≠ 0
e : E := (↑‖x‖)⁻¹ • x
he : ‖e‖ = 1
he' : e ∈ (span 𝕜 v)ᗮ
he'' : ¬e ∈ v
h_end : ∀ (a : E), a ∈ v → inner a e = 0
a : E
ha' : a ∈ insert e v
ha : a = e
b : E
hb' : b ∈ insert e v
hab' : { val := a, property := ha' } ≠ { val := b, property := hb' }
⊢ b ≠ e
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1095350
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
v : Set E
hv : Orthonormal 𝕜 Subtype.val
x : E
hx' : x ∈ (span 𝕜 v)ᗮ
hx : x ≠ 0
e : E := (↑‖x‖)⁻¹ • x
he : ‖e‖ = 1
he' : e ∈ (span 𝕜 v)ᗮ
he'' : ¬e ∈ v
h_end : ∀ (a : E), a ∈ v → inner a e = 0
a : E
ha' : a ∈ insert e v
ha : a = e
b : E
hb' : b ∈ insert e v
hab' : { val := a, property := ha' } ≠ { val := b, property := hb' }
⊢ b ∈ v
refine' mem_of_mem_insert_of_ne hb' _
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1095350
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
v : Set E
hv : Orthonormal 𝕜 Subtype.val
x : E
hx' : x ∈ (span 𝕜 v)ᗮ
hx : x ≠ 0
e : E := (↑‖x‖)⁻¹ • x
he : ‖e‖ = 1
he' : e ∈ (span 𝕜 v)ᗮ
he'' : ¬e ∈ v
h_end : ∀ (a : E), a ∈ v → inner a e = 0
a : E
ha' : a ∈ insert e v
ha : a = e
b : E
hb' : b ∈ insert e v
hab' : { val := a, property := ha' } ≠ { val := b, property := hb' }
hbe' : b = e
⊢ False
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1095350
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
v : Set E
hv : Orthonormal 𝕜 Subtype.val
x : E
hx' : x ∈ (span 𝕜 v)ᗮ
hx : x ≠ 0
e : E := (↑‖x‖)⁻¹ • x
he : ‖e‖ = 1
he' : e ∈ (span 𝕜 v)ᗮ
he'' : ¬e ∈ v
h_end : ∀ (a : E), a ∈ v → inner a e = 0
a : E
ha' : a ∈ insert e v
ha : a = e
b : E
hb' : b ∈ insert e v
hab' : { val := a, property := ha' } ≠ { val := b, property := hb' }
⊢ b ≠ e
intro hbe'
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1095350
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
v : Set E
hv : Orthonormal 𝕜 Subtype.val
x : E
hx' : x ∈ (span 𝕜 v)ᗮ
hx : x ≠ 0
e : E := (↑‖x‖)⁻¹ • x
he : ‖e‖ = 1
he' : e ∈ (span 𝕜 v)ᗮ
he'' : ¬e ∈ v
h_end : ∀ (a : E), a ∈ v → inner a e = 0
a : E
ha' : a ∈ insert e v
ha : a = e
b : E
hb' : b ∈ insert e v
hab' : { val := a, property := ha' } ≠ { val := b, property := hb' }
hbe' : b = e
⊢ { val := a, property := ha' } = { val := b, property := hb' }
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1095350
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
v : Set E
hv : Orthonormal 𝕜 Subtype.val
x : E
hx' : x ∈ (span 𝕜 v)ᗮ
hx : x ≠ 0
e : E := (↑‖x‖)⁻¹ • x
he : ‖e‖ = 1
he' : e ∈ (span 𝕜 v)ᗮ
he'' : ¬e ∈ v
h_end : ∀ (a : E), a ∈ v → inner a e = 0
a : E
ha' : a ∈ insert e v
ha : a = e
b : E
hb' : b ∈ insert e v
hab' : { val := a, property := ha' } ≠ { val := b, property := hb' }
hbe' : b = e
⊢ False
apply hab'
no goals
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1095350
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
v : Set E
hv : Orthonormal 𝕜 Subtype.val
x : E
hx' : x ∈ (span 𝕜 v)ᗮ
hx : x ≠ 0
e : E := (↑‖x‖)⁻¹ • x
he : ‖e‖ = 1
he' : e ∈ (span 𝕜 v)ᗮ
he'' : ¬e ∈ v
h_end : ∀ (a : E), a ∈ v → inner a e = 0
a : E
ha' : a ∈ insert e v
ha : a = e
b : E
hb' : b ∈ insert e v
hab' : { val := a, property := ha' } ≠ { val := b, property := hb' }
hbe' : b = e
⊢ { val := a, property := ha' } = { val := b, property := hb' }
simp [ha, hbe']
no goals
case mp.intro.intro.refine'_2.mk.inr.mk.inl
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1095350
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
v : Set E
hv : Orthonormal 𝕜 Subtype.val
x : E
hx' : x ∈ (span 𝕜 v)ᗮ
hx : x ≠ 0
e : E := (↑‖x‖)⁻¹ • x
he : ‖e‖ = 1
he' : e ∈ (span 𝕜 v)ᗮ
he'' : ¬e ∈ v
h_end : ∀ (a : E), a ∈ v → inner a e = 0
a : E
ha' : a ∈ insert e v
ha : a ∈ v
b : E
hb' : b ∈ insert e v
hab' : { val := a, property := ha' } ≠ { val := b, property := hb' }
hb : b = e
⊢ inner ↑{ val := a, property := ha' } ↑{ val := b, property := hb' } = 0
simpa [hb] using h_end a ha
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1095350
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
v : Set E
hv : Orthonormal 𝕜 Subtype.val
x : E
hx' : x ∈ (span 𝕜 v)ᗮ
hx : x ≠ 0
e : E := (↑‖x‖)⁻¹ • x
he : ‖e‖ = 1
he' : e ∈ (span 𝕜 v)ᗮ
he'' : ¬e ∈ v
h_end : ∀ (a : E), a ∈ v → inner a e = 0
a : E
ha' : a ∈ insert e v
ha : a ∈ v
b : E
hb' : b ∈ insert e v
hab' : { val := a, property := ha' } ≠ { val := b, property := hb' }
hb : b ∈ v
hab'' : { val := a, property := ha } = { val := b, property := hb }
⊢ False
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1095350
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
v : Set E
hv : Orthonormal 𝕜 Subtype.val
x : E
hx' : x ∈ (span 𝕜 v)ᗮ
hx : x ≠ 0
e : E := (↑‖x‖)⁻¹ • x
he : ‖e‖ = 1
he' : e ∈ (span 𝕜 v)ᗮ
he'' : ¬e ∈ v
h_end : ∀ (a : E), a ∈ v → inner a e = 0
a : E
ha' : a ∈ insert e v
ha : a ∈ v
b : E
hb' : b ∈ insert e v
hab' : { val := a, property := ha' } ≠ { val := b, property := hb' }
hb : b ∈ v
⊢ { val := a, property := ha } ≠ { val := b, property := hb }
intro hab''
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1095350
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
v : Set E
hv : Orthonormal 𝕜 Subtype.val
x : E
hx' : x ∈ (span 𝕜 v)ᗮ
hx : x ≠ 0
e : E := (↑‖x‖)⁻¹ • x
he : ‖e‖ = 1
he' : e ∈ (span 𝕜 v)ᗮ
he'' : ¬e ∈ v
h_end : ∀ (a : E), a ∈ v → inner a e = 0
a : E
ha' : a ∈ insert e v
ha : a ∈ v
b : E
hb' : b ∈ insert e v
hab' : { val := a, property := ha' } ≠ { val := b, property := hb' }
hb : b ∈ v
hab'' : { val := a, property := ha } = { val := b, property := hb }
⊢ { val := a, property := ha' } = { val := b, property := hb' }
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1095350
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
v : Set E
hv : Orthonormal 𝕜 Subtype.val
x : E
hx' : x ∈ (span 𝕜 v)ᗮ
hx : x ≠ 0
e : E := (↑‖x‖)⁻¹ • x
he : ‖e‖ = 1
he' : e ∈ (span 𝕜 v)ᗮ
he'' : ¬e ∈ v
h_end : ∀ (a : E), a ∈ v → inner a e = 0
a : E
ha' : a ∈ insert e v
ha : a ∈ v
b : E
hb' : b ∈ insert e v
hab' : { val := a, property := ha' } ≠ { val := b, property := hb' }
hb : b ∈ v
hab'' : { val := a, property := ha } = { val := b, property := hb }
⊢ False
apply hab'
no goals
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1095350
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
v : Set E
hv : Orthonormal 𝕜 Subtype.val
x : E
hx' : x ∈ (span 𝕜 v)ᗮ
hx : x ≠ 0
e : E := (↑‖x‖)⁻¹ • x
he : ‖e‖ = 1
he' : e ∈ (span 𝕜 v)ᗮ
he'' : ¬e ∈ v
h_end : ∀ (a : E), a ∈ v → inner a e = 0
a : E
ha' : a ∈ insert e v
ha : a ∈ v
b : E
hb' : b ∈ insert e v
hab' : { val := a, property := ha' } ≠ { val := b, property := hb' }
hb : b ∈ v
hab'' : { val := a, property := ha } = { val := b, property := hb }
⊢ { val := a, property := ha' } = { val := b, property := hb' }
simpa using hab''
case mpr
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1095350
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
v : Set E
hv : Orthonormal 𝕜 Subtype.val
⊢ (∀ (x : E), x ∈ (span 𝕜 v)ᗮ → x = 0) → ∀ (u : Set E), u ⊇ v → Orthonormal 𝕜 Subtype.val → u ⊆ v ∧ v ⊆ u
case mpr
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1095350
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
v : Set E
hv : Orthonormal 𝕜 Subtype.val
⊢ (∀ (x : E), x ∈ (span 𝕜 v)ᗮ → x = 0) → ∀ (u : Set E), u ⊇ v → Orthonormal 𝕜 Subtype.val → u = v
simp only [Subset.antisymm_iff]
case mpr
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1095350
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
v : Set E
hv : Orthonormal 𝕜 Subtype.val
h : ∀ (x : E), x ∈ (span 𝕜 v)ᗮ → x = 0
u : Set E
huv : v ⊆ u
hu : Orthonormal 𝕜 Subtype.val
⊢ u ⊆ v ∧ v ⊆ u
case mpr
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1095350
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
v : Set E
hv : Orthonormal 𝕜 Subtype.val
⊢ (∀ (x : E), x ∈ (span 𝕜 v)ᗮ → x = 0) → ∀ (u : Set E), u ⊇ v → Orthonormal 𝕜 Subtype.val → u ⊆ v ∧ v ⊆ u
rintro h u (huv : v ⊆ u) hu
case mpr
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1095350
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
v : Set E
hv : Orthonormal 𝕜 Subtype.val
h : ∀ (x : E), x ∈ (span 𝕜 v)ᗮ → x = 0
u : Set E
huv : v ⊆ u
hu : Orthonormal 𝕜 Subtype.val
⊢ u ⊆ v
case mpr
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1095350
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
v : Set E
hv : Orthonormal 𝕜 Subtype.val
h : ∀ (x : E), x ∈ (span 𝕜 v)ᗮ → x = 0
u : Set E
huv : v ⊆ u
hu : Orthonormal 𝕜 Subtype.val
⊢ u ⊆ v ∧ v ⊆ u
refine' ⟨_, huv⟩
case mpr
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1095350
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
v : Set E
hv : Orthonormal 𝕜 Subtype.val
h : ∀ (x : E), x ∈ (span 𝕜 v)ᗮ → x = 0
u : Set E
huv : v ⊆ u
hu : Orthonormal 𝕜 Subtype.val
x : E
hxu : x ∈ u
⊢ x ∈ v
case mpr
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1095350
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
v : Set E
hv : Orthonormal 𝕜 Subtype.val
h : ∀ (x : E), x ∈ (span 𝕜 v)ᗮ → x = 0
u : Set E
huv : v ⊆ u
hu : Orthonormal 𝕜 Subtype.val
⊢ u ⊆ v
intro x hxu
case mpr
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1095350
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
v : Set E
hv : Orthonormal 𝕜 Subtype.val
h : ∀ (x : E), x ∈ (span 𝕜 v)ᗮ → x = 0
u : Set E
huv : v ⊆ u
hu : Orthonormal 𝕜 Subtype.val
x : E
hxu : x ∈ u
⊢ ¬x ∈ v → x ∈ (span 𝕜 v)ᗮ
case mpr
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1095350
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
v : Set E
hv : Orthonormal 𝕜 Subtype.val
h : ∀ (x : E), x ∈ (span 𝕜 v)ᗮ → x = 0
u : Set E
huv : v ⊆ u
hu : Orthonormal 𝕜 Subtype.val
x : E
hxu : x ∈ u
⊢ x ∈ v
refine' ((mt (h x)) (hu.ne_zero ⟨x, hxu⟩)).imp_symm _
case mpr
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1095350
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
v : Set E
hv : Orthonormal 𝕜 Subtype.val
h : ∀ (x : E), x ∈ (span 𝕜 v)ᗮ → x = 0
u : Set E
huv : v ⊆ u
hu : Orthonormal 𝕜 Subtype.val
x : E
hxu : x ∈ u
hxv : ¬x ∈ v
y : E
hy : y ∈ span 𝕜 v
⊢ inner y x = 0
case mpr
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1095350
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
v : Set E
hv : Orthonormal 𝕜 Subtype.val
h : ∀ (x : E), x ∈ (span 𝕜 v)ᗮ → x = 0
u : Set E
huv : v ⊆ u
hu : Orthonormal 𝕜 Subtype.val
x : E
hxu : x ∈ u
⊢ ¬x ∈ v → x ∈ (span 𝕜 v)ᗮ
intro hxv y hy
case mpr
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1095350
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
v : Set E
hv : Orthonormal 𝕜 Subtype.val
h : ∀ (x : E), x ∈ (span 𝕜 v)ᗮ → x = 0
u : Set E
huv : v ⊆ u
hu : Orthonormal 𝕜 Subtype.val
x : E
hxu : x ∈ u
hxv : ¬x ∈ v
y : E
hy : y ∈ span 𝕜 v
hxv' : ¬{ val := x, property := hxu } ∈ Subtype.val ⁻¹' v
⊢ inner y x = 0
case mpr
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1095350
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
v : Set E
hv : Orthonormal 𝕜 Subtype.val
h : ∀ (x : E), x ∈ (span 𝕜 v)ᗮ → x = 0
u : Set E
huv : v ⊆ u
hu : Orthonormal 𝕜 Subtype.val
x : E
hxu : x ∈ u
hxv : ¬x ∈ v
y : E
hy : y ∈ span 𝕜 v
⊢ inner y x = 0
have hxv' : (⟨x, hxu⟩ : u) ∉ ((↑) ⁻¹' v : Set u) := by simp [huv, hxv]
case mpr.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1095350
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
v : Set E
hv : Orthonormal 𝕜 Subtype.val
h : ∀ (x : E), x ∈ (span 𝕜 v)ᗮ → x = 0
u : Set E
huv : v ⊆ u
hu : Orthonormal 𝕜 Subtype.val
x : E
hxu : x ∈ u
hxv : ¬x ∈ v
hxv' : ¬{ val := x, property := hxu } ∈ Subtype.val ⁻¹' v
l : ↑u →₀ 𝕜
hy : ↑(Finsupp.total (↑u) E 𝕜 Subtype.val) l ∈ span 𝕜 v
hl : l ∈ Finsupp.supported 𝕜 𝕜 (?m.1124382 (↑(Finsupp.total (↑u) E 𝕜 Subtype.val) l) hy l ⁻¹' v)
⊢ inner (↑(Finsupp.total (↑u) E 𝕜 Subtype.val) l) x = 0
case mpr
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1095350
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
v : Set E
hv : Orthonormal 𝕜 Subtype.val
h : ∀ (x : E), x ∈ (span 𝕜 v)ᗮ → x = 0
u : Set E
huv : v ⊆ u
hu : Orthonormal 𝕜 Subtype.val
x : E
hxu : x ∈ u
hxv : ¬x ∈ v
y : E
hy : y ∈ span 𝕜 v
hxv' : ¬{ val := x, property := hxu } ∈ Subtype.val ⁻¹' v
⊢ inner y x = 0
obtain ⟨l, hl, rfl⟩ :
  ∃ l ∈ Finsupp.supported 𝕜 𝕜 ((↑) ⁻¹' v : Set u), (Finsupp.total (↥u) E 𝕜 (↑)) l = y := by
  rw [← Finsupp.mem_span_image_iff_total]
  simp [huv, inter_eq_self_of_subset_left, hy]
no goals
case mpr.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1095350
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
v : Set E
hv : Orthonormal 𝕜 Subtype.val
h : ∀ (x : E), x ∈ (span 𝕜 v)ᗮ → x = 0
u : Set E
huv : v ⊆ u
hu : Orthonormal 𝕜 Subtype.val
x : E
hxu : x ∈ u
hxv : ¬x ∈ v
hxv' : ¬{ val := x, property := hxu } ∈ Subtype.val ⁻¹' v
l : ↑u →₀ 𝕜
hy : ↑(Finsupp.total (↑u) E 𝕜 Subtype.val) l ∈ span 𝕜 v
hl : l ∈ Finsupp.supported 𝕜 𝕜 (?m.1124382 (↑(Finsupp.total (↑u) E 𝕜 Subtype.val) l) hy l ⁻¹' v)
⊢ inner (↑(Finsupp.total (↑u) E 𝕜 Subtype.val) l) x = 0
exact hu.inner_finsupp_eq_zero hxv' hl
no goals
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1095350
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
v : Set E
hv : Orthonormal 𝕜 Subtype.val
h : ∀ (x : E), x ∈ (span 𝕜 v)ᗮ → x = 0
u : Set E
huv : v ⊆ u
hu : Orthonormal 𝕜 Subtype.val
x : E
hxu : x ∈ u
hxv : ¬x ∈ v
y : E
hy : y ∈ span 𝕜 v
⊢ ¬{ val := x, property := hxu } ∈ Subtype.val ⁻¹' v
simp [huv, hxv]
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1095350
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
v : Set E
hv : Orthonormal 𝕜 Subtype.val
h : ∀ (x : E), x ∈ (span 𝕜 v)ᗮ → x = 0
u : Set E
huv : v ⊆ u
hu : Orthonormal 𝕜 Subtype.val
x : E
hxu : x ∈ u
hxv : ¬x ∈ v
y : E
hy : y ∈ span 𝕜 v
hxv' : ¬{ val := x, property := hxu } ∈ Subtype.val ⁻¹' v
⊢ y ∈ span 𝕜 (Subtype.val '' (Subtype.val ⁻¹' v))
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1095350
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
v : Set E
hv : Orthonormal 𝕜 Subtype.val
h : ∀ (x : E), x ∈ (span 𝕜 v)ᗮ → x = 0
u : Set E
huv : v ⊆ u
hu : Orthonormal 𝕜 Subtype.val
x : E
hxu : x ∈ u
hxv : ¬x ∈ v
y : E
hy : y ∈ span 𝕜 v
hxv' : ¬{ val := x, property := hxu } ∈ Subtype.val ⁻¹' v
⊢ ∃ l, l ∈ Finsupp.supported 𝕜 𝕜 (Subtype.val ⁻¹' v) ∧ ↑(Finsupp.total (↑u) E 𝕜 Subtype.val) l = y
rw [← Finsupp.mem_span_image_iff_total]
no goals
𝕜 : Type u_1
E : Type u_2
F : Type ?u.1095350
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
v : Set E
hv : Orthonormal 𝕜 Subtype.val
h : ∀ (x : E), x ∈ (span 𝕜 v)ᗮ → x = 0
u : Set E
huv : v ⊆ u
hu : Orthonormal 𝕜 Subtype.val
x : E
hxu : x ∈ u
hxv : ¬x ∈ v
y : E
hy : y ∈ span 𝕜 v
hxv' : ¬{ val := x, property := hxu } ∈ Subtype.val ⁻¹' v
⊢ y ∈ span 𝕜 (Subtype.val '' (Subtype.val ⁻¹' v))
simp [huv, inter_eq_self_of_subset_left, hy]