𝕜 : Type u_1
E : Type u_2
F : Type ?u.2164084
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_3
dec_ι : DecidableEq ι
v : ι → E
hv : Orthonormal 𝕜 v
i : ι
this : ‖v i‖ ≠ 0
⊢ v i ≠ 0
𝕜 : Type u_1
E : Type u_2
F : Type ?u.2164084
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_3
dec_ι : DecidableEq ι
v : ι → E
hv : Orthonormal 𝕜 v
i : ι
⊢ v i ≠ 0
have : ‖v i‖ ≠ 0 := by
  rw [hv.1 i]
  norm_num
no goals
𝕜 : Type u_1
E : Type u_2
F : Type ?u.2164084
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_3
dec_ι : DecidableEq ι
v : ι → E
hv : Orthonormal 𝕜 v
i : ι
this : ‖v i‖ ≠ 0
⊢ v i ≠ 0
simpa using this
𝕜 : Type u_1
E : Type u_2
F : Type ?u.2164084
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_3
dec_ι : DecidableEq ι
v : ι → E
hv : Orthonormal 𝕜 v
i : ι
⊢ 1 ≠ 0
𝕜 : Type u_1
E : Type u_2
F : Type ?u.2164084
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_3
dec_ι : DecidableEq ι
v : ι → E
hv : Orthonormal 𝕜 v
i : ι
⊢ ‖v i‖ ≠ 0
rw [hv.1 i]
no goals
𝕜 : Type u_1
E : Type u_2
F : Type ?u.2164084
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_3
dec_ι : DecidableEq ι
v : ι → E
hv : Orthonormal 𝕜 v
i : ι
⊢ 1 ≠ 0
norm_num