𝕜 : Type u_1
E : Type u_2
F : Type ?u.2146112
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_3
dec_ι : DecidableEq ι
v w : ι → E
hv : Orthonormal 𝕜 v
hw : ∀ (i : ι), w i = v i ∨ w i = -v i
em✝ : (a : Prop) → Decidable a
⊢ Orthonormal 𝕜 w
𝕜 : Type u_1
E : Type u_2
F : Type ?u.2146112
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_3
dec_ι : DecidableEq ι
v w : ι → E
hv : Orthonormal 𝕜 v
hw : ∀ (i : ι), w i = v i ∨ w i = -v i
⊢ Orthonormal 𝕜 w
classical!
𝕜 : Type u_1
E : Type u_2
F : Type ?u.2146112
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_3
dec_ι : DecidableEq ι
v w : ι → E
hw : ∀ (i : ι), w i = v i ∨ w i = -v i
em✝ : (a : Prop) → Decidable a
hv : ∀ (i j : ι), inner (v i) (v j) = if i = j then 1 else 0
⊢ ∀ (i j : ι), inner (w i) (w j) = if i = j then 1 else 0
𝕜 : Type u_1
E : Type u_2
F : Type ?u.2146112
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_3
dec_ι : DecidableEq ι
v w : ι → E
hv : Orthonormal 𝕜 v
hw : ∀ (i : ι), w i = v i ∨ w i = -v i
em✝ : (a : Prop) → Decidable a
⊢ Orthonormal 𝕜 w
rw [orthonormal_iff_ite] at *
𝕜 : Type u_1
E : Type u_2
F : Type ?u.2146112
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_3
dec_ι : DecidableEq ι
v w : ι → E
hw : ∀ (i : ι), w i = v i ∨ w i = -v i
em✝ : (a : Prop) → Decidable a
hv : ∀ (i j : ι), inner (v i) (v j) = if i = j then 1 else 0
i j : ι
⊢ inner (w i) (w j) = if i = j then 1 else 0
𝕜 : Type u_1
E : Type u_2
F : Type ?u.2146112
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_3
dec_ι : DecidableEq ι
v w : ι → E
hw : ∀ (i : ι), w i = v i ∨ w i = -v i
em✝ : (a : Prop) → Decidable a
hv : ∀ (i j : ι), inner (v i) (v j) = if i = j then 1 else 0
⊢ ∀ (i j : ι), inner (w i) (w j) = if i = j then 1 else 0
intro i j
no goals
𝕜 : Type u_1
E : Type u_2
F : Type ?u.2146112
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_3
dec_ι : DecidableEq ι
v w : ι → E
hw : ∀ (i : ι), w i = v i ∨ w i = -v i
em✝ : (a : Prop) → Decidable a
hv : ∀ (i j : ι), inner (v i) (v j) = if i = j then 1 else 0
i j : ι
⊢ inner (w i) (w j) = if i = j then 1 else 0
cases' hw i with hi hi <;> cases' hw j with hj hj <;>
  replace hv := hv i j <;> split_ifs at hv ⊢ with h <;>
  simpa only [hi, hj, h, inner_neg_right, inner_neg_left, neg_neg, eq_self_iff_true,
    neg_eq_zero] using hv