𝕜 : Type u_3
E : Type u_2
F : Type ?u.1881979
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_1
v : ι → E
hz : ∀ (i : ι), v i ≠ 0
ho : ∀ (i j : ι), i ≠ j → inner (v i) (v j) = 0
⊢ ∀ (s : Finset ι) (g : ι → 𝕜), ∑ i in s, g i • v i = 0 → ∀ (i : ι), i ∈ s → g i = 0
𝕜 : Type u_3
E : Type u_2
F : Type ?u.1881979
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_1
v : ι → E
hz : ∀ (i : ι), v i ≠ 0
ho : ∀ (i j : ι), i ≠ j → inner (v i) (v j) = 0
⊢ LinearIndependent 𝕜 v
rw [linearIndependent_iff']
𝕜 : Type u_3
E : Type u_2
F : Type ?u.1881979
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_1
v : ι → E
hz : ∀ (i : ι), v i ≠ 0
ho : ∀ (i j : ι), i ≠ j → inner (v i) (v j) = 0
s : Finset ι
g : ι → 𝕜
hg : ∑ i in s, g i • v i = 0
i : ι
hi : i ∈ s
⊢ g i = 0
𝕜 : Type u_3
E : Type u_2
F : Type ?u.1881979
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_1
v : ι → E
hz : ∀ (i : ι), v i ≠ 0
ho : ∀ (i j : ι), i ≠ j → inner (v i) (v j) = 0
⊢ ∀ (s : Finset ι) (g : ι → 𝕜), ∑ i in s, g i • v i = 0 → ∀ (i : ι), i ∈ s → g i = 0
intro s g hg i hi
no goals
𝕜 : Type u_3
E : Type u_2
F : Type ?u.1881979
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_1
v : ι → E
hz : ∀ (i : ι), v i ≠ 0
ho : ∀ (i j : ι), i ≠ j → inner (v i) (v j) = 0
s : Finset ι
g : ι → 𝕜
hg : ∑ i in s, g i • v i = 0
i : ι
hi : i ∈ s
h' : g i * inner (v i) (v i) = inner (v i) (∑ j in s, g j • v j)
⊢ g i = 0
simpa [hg, hz] using h'
𝕜 : Type u_3
E : Type u_2
F : Type ?u.1881979
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_1
v : ι → E
hz : ∀ (i : ι), v i ≠ 0
ho : ∀ (i j : ι), i ≠ j → inner (v i) (v j) = 0
s : Finset ι
g : ι → 𝕜
hg : ∑ i in s, g i • v i = 0
i : ι
hi : i ∈ s
⊢ g i * inner (v i) (v i) = ∑ i_1 in s, inner (v i) (g i_1 • v i_1)
𝕜 : Type u_3
E : Type u_2
F : Type ?u.1881979
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_1
v : ι → E
hz : ∀ (i : ι), v i ≠ 0
ho : ∀ (i j : ι), i ≠ j → inner (v i) (v j) = 0
s : Finset ι
g : ι → 𝕜
hg : ∑ i in s, g i • v i = 0
i : ι
hi : i ∈ s
⊢ g i * inner (v i) (v i) = inner (v i) (∑ j in s, g j • v j)
rw [inner_sum]
𝕜 : Type u_3
E : Type u_2
F : Type ?u.1881979
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_1
v : ι → E
hz : ∀ (i : ι), v i ≠ 0
ho : ∀ (i j : ι), i ≠ j → inner (v i) (v j) = 0
s : Finset ι
g : ι → 𝕜
hg : ∑ i in s, g i • v i = 0
i : ι
hi : i ∈ s
⊢ ∑ i_1 in s, inner (v i) (g i_1 • v i_1) = g i * inner (v i) (v i)
𝕜 : Type u_3
E : Type u_2
F : Type ?u.1881979
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_1
v : ι → E
hz : ∀ (i : ι), v i ≠ 0
ho : ∀ (i j : ι), i ≠ j → inner (v i) (v j) = 0
s : Finset ι
g : ι → 𝕜
hg : ∑ i in s, g i • v i = 0
i : ι
hi : i ∈ s
⊢ g i * inner (v i) (v i) = ∑ i_1 in s, inner (v i) (g i_1 • v i_1)
symm
case h.e'_3
𝕜 : Type u_3
E : Type u_2
F : Type ?u.1881979
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_1
v : ι → E
hz : ∀ (i : ι), v i ≠ 0
ho : ∀ (i j : ι), i ≠ j → inner (v i) (v j) = 0
s : Finset ι
g : ι → 𝕜
hg : ∑ i in s, g i • v i = 0
i : ι
hi : i ∈ s
⊢ g i * inner (v i) (v i) = inner (v i) (g i • v i)

case convert_3
𝕜 : Type u_3
E : Type u_2
F : Type ?u.1881979
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_1
v : ι → E
hz : ∀ (i : ι), v i ≠ 0
ho : ∀ (i j : ι), i ≠ j → inner (v i) (v j) = 0
s : Finset ι
g : ι → 𝕜
hg : ∑ i in s, g i • v i = 0
i : ι
hi : i ∈ s
⊢ ∀ (b : ι), b ∈ s → b ≠ i → inner (v i) (g b • v b) = 0

case convert_4
𝕜 : Type u_3
E : Type u_2
F : Type ?u.1881979
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_1
v : ι → E
hz : ∀ (i : ι), v i ≠ 0
ho : ∀ (i j : ι), i ≠ j → inner (v i) (v j) = 0
s : Finset ι
g : ι → 𝕜
hg : ∑ i in s, g i • v i = 0
i : ι
hi : i ∈ s
⊢ ¬i ∈ s → inner (v i) (g i • v i) = 0
𝕜 : Type u_3
E : Type u_2
F : Type ?u.1881979
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_1
v : ι → E
hz : ∀ (i : ι), v i ≠ 0
ho : ∀ (i j : ι), i ≠ j → inner (v i) (v j) = 0
s : Finset ι
g : ι → 𝕜
hg : ∑ i in s, g i • v i = 0
i : ι
hi : i ∈ s
⊢ ∑ i_1 in s, inner (v i) (g i_1 • v i_1) = g i * inner (v i) (v i)
convert Finset.sum_eq_single (β := 𝕜) i ?_ ?_
no goals
case h.e'_3
𝕜 : Type u_3
E : Type u_2
F : Type ?u.1881979
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_1
v : ι → E
hz : ∀ (i : ι), v i ≠ 0
ho : ∀ (i j : ι), i ≠ j → inner (v i) (v j) = 0
s : Finset ι
g : ι → 𝕜
hg : ∑ i in s, g i • v i = 0
i : ι
hi : i ∈ s
⊢ g i * inner (v i) (v i) = inner (v i) (g i • v i)
rw [inner_smul_right]
case convert_3
𝕜 : Type u_3
E : Type u_2
F : Type ?u.1881979
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_1
v : ι → E
hz : ∀ (i : ι), v i ≠ 0
ho : ∀ (i j : ι), i ≠ j → inner (v i) (v j) = 0
s : Finset ι
g : ι → 𝕜
hg : ∑ i in s, g i • v i = 0
i : ι
hi : i ∈ s
j : ι
_hj : j ∈ s
hji : j ≠ i
⊢ inner (v i) (g j • v j) = 0
case convert_3
𝕜 : Type u_3
E : Type u_2
F : Type ?u.1881979
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_1
v : ι → E
hz : ∀ (i : ι), v i ≠ 0
ho : ∀ (i j : ι), i ≠ j → inner (v i) (v j) = 0
s : Finset ι
g : ι → 𝕜
hg : ∑ i in s, g i • v i = 0
i : ι
hi : i ∈ s
⊢ ∀ (b : ι), b ∈ s → b ≠ i → inner (v i) (g b • v b) = 0
intro j _hj hji
no goals
case convert_3
𝕜 : Type u_3
E : Type u_2
F : Type ?u.1881979
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_1
v : ι → E
hz : ∀ (i : ι), v i ≠ 0
ho : ∀ (i j : ι), i ≠ j → inner (v i) (v j) = 0
s : Finset ι
g : ι → 𝕜
hg : ∑ i in s, g i • v i = 0
i : ι
hi : i ∈ s
j : ι
_hj : j ∈ s
hji : j ≠ i
⊢ inner (v i) (g j • v j) = 0
rw [inner_smul_right, ho i j hji.symm, MulZeroClass.mul_zero]
no goals
case convert_4
𝕜 : Type u_3
E : Type u_2
F : Type ?u.1881979
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι : Type u_1
v : ι → E
hz : ∀ (i : ι), v i ≠ 0
ho : ∀ (i j : ι), i ≠ j → inner (v i) (v j) = 0
s : Finset ι
g : ι → 𝕜
hg : ∑ i in s, g i • v i = 0
i : ι
hi : i ∈ s
⊢ ¬i ∈ s → inner (v i) (g i • v i) = 0
exact fun h => False.elim (h hi)