simp_rw [mul_comm (y w), ← mul_assoc, ← Finset.sum_mul]
case intro.intro.intro.mk
l : Type u_1
m : Type u_2
m' : Type u_3
n : Type u_4
n' : Type u_5
n₁ : Type u_6
n₂ : Type u_7
o : Type u_8
α : Type u_9
R : Type u_10
A B : Matrix m n R
s✝ : Set m
t : Set n
inst✝¹ : Fintype m
inst✝ : CommSemiring R
x : m → R
s : Set (m → R)
h : ∀ z ∈ s, x ⬝ᵥ z = 0
c : ℕ
y : Fin c → R
z : Fin c → ↑s
hy : ∑ i : Fin c, y i • ↑(z i) ∈ span R s
w : Fin c
i : m → R
hi : i ∈ s
⊢ ∑ x_1 : m, x x_1 * (y w * ↑⟨i, hi⟩ x_1) = 0
case intro.intro.intro.mk
l : Type u_1
m : Type u_2
m' : Type u_3
n : Type u_4
n' : Type u_5
n₁ : Type u_6
n₂ : Type u_7
o : Type u_8
α : Type u_9
R : Type u_10
A B : Matrix m n R
s✝ : Set m
t : Set n
inst✝¹ : Fintype m
inst✝ : CommSemiring R
x : m → R
s : Set (m → R)
h : ∀ z ∈ s, x ⬝ᵥ z = 0
c : ℕ
y : Fin c → R
z : Fin c → ↑s
hy : ∑ i : Fin c, y i • ↑(z i) ∈ span R s
w : Fin c
i : m → R
hi : i ∈ s
⊢ (∑ i_1 : m, x i_1 * i i_1) * y w = 0