Theorem: Matrix.dotProduct_eq_zero_of_mem_span (Matroid/ForMathlib/LinearAlgebra/Matrix/Rowspace.lean)

State before:
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 y : m → R
s : Set (m → R)
hy : y ∈ span R s
h : ∀ z ∈ s, x ⬝ᵥ z = 0
⊢ x ⬝ᵥ y = 0
Tactic:
obtain ⟨c, y,z, rfl⟩ := mem_span_set'.1 hy
State after:
case intro.intro.intro
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
⊢ x ⬝ᵥ ∑ i : Fin c, y i • ↑(z i) = 0

State before:
case intro.intro.intro
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
⊢ x ⬝ᵥ ∑ i : Fin c, y i • ↑(z i) = 0
Tactic:
simp only [dotProduct, Finset.sum_apply, Pi.smul_apply, smul_eq_mul, Finset.mul_sum]
State after:
case intro.intro.intro
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
⊢ ∑ x_1 : m, ∑ i : Fin c, x x_1 * (y i * ↑(z i) x_1) = 0

State before:
case intro.intro.intro
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
⊢ ∑ x_1 : m, ∑ i : Fin c, x x_1 * (y i * ↑(z i) x_1) = 0
Tactic:
rw [Finset.sum_comm, Finset.sum_eq_zero]
State after:
case intro.intro.intro
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
⊢ ∀ x_1 ∈ Finset.univ, ∑ x_2 : m, x x_2 * (y x_1 * ↑(z x_1) x_2) = 0

State before:
case intro.intro.intro
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
⊢ ∀ x_1 ∈ Finset.univ, ∑ x_2 : m, x x_2 * (y x_1 * ↑(z x_1) x_2) = 0
Tactic:
rintro w -
State after:
case intro.intro.intro
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
⊢ ∑ x_1 : m, x x_1 * (y w * ↑(z w) x_1) = 0

State before:
case intro.intro.intro
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
⊢ ∑ x_1 : m, x x_1 * (y w * ↑(z w) x_1) = 0
Tactic:
obtain ⟨i, hi⟩ := z w
State after:
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

State before:
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
Tactic:
simp_rw [mul_comm (y w), ← mul_assoc, ← Finset.sum_mul]
State after:
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

State before:
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
Tactic:
convert zero_mul _
State after:
case h.e'_2.h.e'_5
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 = 0

State before:
case h.e'_2.h.e'_5
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 = 0
Tactic:
rw [← h i hi, dotProduct]
State after:
no goals