-- Mathlib/Analysis/InnerProductSpace/Basic.lean
theorem linearIndependent_of_ne_zero_of_inner_eq_zero {ι : Type*} {v : ι → E} (hz : ∀ i, v i ≠ 0)
    (ho : Pairwise fun i j => ⟪v i, v j⟫ = 0) : LinearIndependent 𝕜 v

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
v : ι → E
hz : ∀ (i : ι), v i ≠ 0
ho : Pairwise fun i j => inner (v i) (v j) = 0
s : Finset ι
g : ι → 𝕜
hg : ∑ i ∈ s, g i • v i = 0
i : ι
hi : i ∈ s
h' : g i * inner (v i) (v i) = inner (v i) (∑ j ∈ s, g j • v j)
⊢ g i = 0

Tactic:
simpa [hg, hz] using h'

Result:
no goals

Proof state:
case convert_3
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
v : ι → E
hz : ∀ (i : ι), v i ≠ 0
ho : Pairwise fun i j => inner (v i) (v j) = 0
s : Finset ι
g : ι → 𝕜
hg : ∑ i ∈ 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

Tactic:
rw [inner_smul_right, ho hji.symm, mul_zero]

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
v : ι → E
hz : ∀ (i : ι), v i ≠ 0
ho : Pairwise fun i j => inner (v i) (v j) = 0
⊢ ∀ (s : Finset ι) (g : ι → 𝕜), ∑ i ∈ s, g i • v i = 0 → ∀ i ∈ s, g i = 0

Tactic:
intro s g hg i hi

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
v : ι → E
hz : ∀ (i : ι), v i ≠ 0
ho : Pairwise fun i j => inner (v i) (v j) = 0
s : Finset ι
g : ι → 𝕜
hg : ∑ i ∈ s, g i • v i = 0
i : ι
hi : i ∈ s
⊢ g i = 0

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
v : ι → E
hz : ∀ (i : ι), v i ≠ 0
ho : Pairwise fun i j => inner (v i) (v j) = 0
⊢ LinearIndependent 𝕜 v

Tactic:
rw [linearIndependent_iff']

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
v : ι → E
hz : ∀ (i : ι), v i ≠ 0
ho : Pairwise fun i j => inner (v i) (v j) = 0
⊢ ∀ (s : Finset ι) (g : ι → 𝕜), ∑ i ∈ s, g i • v i = 0 → ∀ i ∈ s, g i = 0

Proof state:
case convert_4
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
v : ι → E
hz : ∀ (i : ι), v i ≠ 0
ho : Pairwise fun i j => inner (v i) (v j) = 0
s : Finset ι
g : ι → 𝕜
hg : ∑ i ∈ s, g i • v i = 0
i : ι
hi : i ∈ s
⊢ i ∉ s → inner (v i) (g i • v i) = 0

Tactic:
exact fun h => False.elim (h hi)

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
v : ι → E
hz : ∀ (i : ι), v i ≠ 0
ho : Pairwise fun i j => inner (v i) (v j) = 0
s : Finset ι
g : ι → 𝕜
hg : ∑ i ∈ s, g i • v i = 0
i : ι
hi : i ∈ s
⊢ g i * inner (v i) (v i) = inner (v i) (∑ j ∈ s, g j • v j)

Tactic:
rw [inner_sum]

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
v : ι → E
hz : ∀ (i : ι), v i ≠ 0
ho : Pairwise fun i j => inner (v i) (v j) = 0
s : Finset ι
g : ι → 𝕜
hg : ∑ i ∈ s, g i • v i = 0
i : ι
hi : i ∈ s
⊢ g i * inner (v i) (v i) = ∑ i_1 ∈ s, inner (v i) (g i_1 • v i_1)

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
v : ι → E
hz : ∀ (i : ι), v i ≠ 0
ho : Pairwise fun i j => inner (v i) (v j) = 0
s : Finset ι
g : ι → 𝕜
hg : ∑ i ∈ s, g i • v i = 0
i : ι
hi : i ∈ s
⊢ g i * inner (v i) (v i) = ∑ i_1 ∈ s, inner (v i) (g i_1 • v i_1)

Tactic:
symm

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
v : ι → E
hz : ∀ (i : ι), v i ≠ 0
ho : Pairwise fun i j => inner (v i) (v j) = 0
s : Finset ι
g : ι → 𝕜
hg : ∑ i ∈ s, g i • v i = 0
i : ι
hi : i ∈ s
⊢ ∑ i_1 ∈ s, inner (v i) (g i_1 • v i_1) = g i * inner (v i) (v i)

Proof state:
case h.e'_3
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
v : ι → E
hz : ∀ (i : ι), v i ≠ 0
ho : Pairwise fun i j => inner (v i) (v j) = 0
s : Finset ι
g : ι → 𝕜
hg : ∑ i ∈ s, g i • v i = 0
i : ι
hi : i ∈ s
⊢ g i * inner (v i) (v i) = inner (v i) (g i • v i)

Tactic:
rw [inner_smul_right]

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
v : ι → E
hz : ∀ (i : ι), v i ≠ 0
ho : Pairwise fun i j => inner (v i) (v j) = 0
s : Finset ι
g : ι → 𝕜
hg : ∑ i ∈ s, g i • v i = 0
i : ι
hi : i ∈ s
⊢ ∑ i_1 ∈ s, inner (v i) (g i_1 • v i_1) = g i * inner (v i) (v i)

Tactic:
convert Finset.sum_eq_single (β := 𝕜) i ?_ ?_

Result:
case h.e'_3
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
v : ι → E
hz : ∀ (i : ι), v i ≠ 0
ho : Pairwise fun i j => inner (v i) (v j) = 0
s : Finset ι
g : ι → 𝕜
hg : ∑ i ∈ 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_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
v : ι → E
hz : ∀ (i : ι), v i ≠ 0
ho : Pairwise fun i j => inner (v i) (v j) = 0
s : Finset ι
g : ι → 𝕜
hg : ∑ i ∈ s, g i • v i = 0
i : ι
hi : i ∈ s
⊢ ∀ b ∈ s, b ≠ i → inner (v i) (g b • v b) = 0

case convert_4
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
v : ι → E
hz : ∀ (i : ι), v i ≠ 0
ho : Pairwise fun i j => inner (v i) (v j) = 0
s : Finset ι
g : ι → 𝕜
hg : ∑ i ∈ s, g i • v i = 0
i : ι
hi : i ∈ s
⊢ i ∉ s → inner (v i) (g i • v i) = 0

Proof state:
case convert_3
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
v : ι → E
hz : ∀ (i : ι), v i ≠ 0
ho : Pairwise fun i j => inner (v i) (v j) = 0
s : Finset ι
g : ι → 𝕜
hg : ∑ i ∈ s, g i • v i = 0
i : ι
hi : i ∈ s
⊢ ∀ b ∈ s, b ≠ i → inner (v i) (g b • v b) = 0

Tactic:
intro j _hj hji

Result:
case convert_3
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
v : ι → E
hz : ∀ (i : ι), v i ≠ 0
ho : Pairwise fun i j => inner (v i) (v j) = 0
s : Finset ι
g : ι → 𝕜
hg : ∑ i ∈ 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