Theorem: Matrix.rows_linearIndependent_of_submatrix (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✝
m : Type u_11
n : Type u_12
R : Type u_13
s : Set m
t : Set n
A B : Matrix m n R
inst✝ : Ring R
m₀ : Type u_14
n₀ : Type u_15
e : m₀ ≃ m
f : n₀ → n
h : LinearIndependent R (A.submatrix (⇑e) f).rowFun
⊢ LinearIndependent R A.rowFun
Tactic:
rw [linearIndependent_iff'] at h ⊢
State after:
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✝
m : Type u_11
n : Type u_12
R : Type u_13
s : Set m
t : Set n
A B : Matrix m n R
inst✝ : Ring R
m₀ : Type u_14
n₀ : Type u_15
e : m₀ ≃ m
f : n₀ → n
h : ∀ (s : Finset m₀) (g : m₀ → R), ∑ i ∈ s, g i • (A.submatrix (⇑e) f).rowFun i = 0 → ∀ i ∈ s, g i = 0
⊢ ∀ (s : Finset m) (g : m → R), ∑ i ∈ s, g i • A.rowFun i = 0 → ∀ i ∈ s, g i = 0

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✝
m : Type u_11
n : Type u_12
R : Type u_13
s : Set m
t : Set n
A B : Matrix m n R
inst✝ : Ring R
m₀ : Type u_14
n₀ : Type u_15
e : m₀ ≃ m
f : n₀ → n
h : ∀ (s : Finset m₀) (g : m₀ → R), ∑ i ∈ s, g i • (A.submatrix (⇑e) f).rowFun i = 0 → ∀ i ∈ s, g i = 0
⊢ ∀ (s : Finset m) (g : m → R), ∑ i ∈ s, g i • A.rowFun i = 0 → ∀ i ∈ s, g i = 0
Tactic:
intro s c hc i his
State after:
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✝
m : Type u_11
n : Type u_12
R : Type u_13
s✝ : Set m
t : Set n
A B : Matrix m n R
inst✝ : Ring R
m₀ : Type u_14
n₀ : Type u_15
e : m₀ ≃ m
f : n₀ → n
h : ∀ (s : Finset m₀) (g : m₀ → R), ∑ i ∈ s, g i • (A.submatrix (⇑e) f).rowFun i = 0 → ∀ i ∈ s, g i = 0
s : Finset m
c : m → R
hc : ∑ i ∈ s, c i • A.rowFun i = 0
i : m
his : i ∈ s
⊢ c i = 0

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✝
m : Type u_11
n : Type u_12
R : Type u_13
s✝ : Set m
t : Set n
A B : Matrix m n R
inst✝ : Ring R
m₀ : Type u_14
n₀ : Type u_15
e : m₀ ≃ m
f : n₀ → n
h : ∀ (s : Finset m₀) (g : m₀ → R), ∑ i ∈ s, g i • (A.submatrix (⇑e) f).rowFun i = 0 → ∀ i ∈ s, g i = 0
s : Finset m
c : m → R
hc : ∑ i ∈ s, c i • A.rowFun i = 0
i : m
his : i ∈ s
⊢ c i = 0
Tactic:
rw [← h (s.image e.symm) (c ∘ e) _ (e.symm i) (by simpa)]
State after:
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✝
m : Type u_11
n : Type u_12
R : Type u_13
s✝ : Set m
t : Set n
A B : Matrix m n R
inst✝ : Ring R
m₀ : Type u_14
n₀ : Type u_15
e : m₀ ≃ m
f : n₀ → n
h : ∀ (s : Finset m₀) (g : m₀ → R), ∑ i ∈ s, g i • (A.submatrix (⇑e) f).rowFun i = 0 → ∀ i ∈ s, g i = 0
s : Finset m
c : m → R
hc : ∑ i ∈ s, c i • A.rowFun i = 0
i : m
his : i ∈ s
⊢ c i = (c ∘ ⇑e) (e.symm i)

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✝
m : Type u_11
n : Type u_12
R : Type u_13
s✝ : Set m
t : Set n
A B : Matrix m n R
inst✝ : Ring R
m₀ : Type u_14
n₀ : Type u_15
e : m₀ ≃ m
f : n₀ → n
h : ∀ (s : Finset m₀) (g : m₀ → R), ∑ i ∈ s, g i • (A.submatrix (⇑e) f).rowFun i = 0 → ∀ i ∈ s, g i = 0
s : Finset m
c : m → R
hc : ∑ i ∈ s, c i • A.rowFun i = 0
i : m
his : i ∈ s
⊢ ∑ i ∈ Finset.image (⇑e.symm) s, (c ∘ ⇑e) i • (A.submatrix (⇑e) f).rowFun i = 0

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✝
m : Type u_11
n : Type u_12
R : Type u_13
s✝ : Set m
t : Set n
A B : Matrix m n R
inst✝ : Ring R
m₀ : Type u_14
n₀ : Type u_15
e : m₀ ≃ m
f : n₀ → n
h : ∀ (s : Finset m₀) (g : m₀ → R), ∑ i ∈ s, g i • (A.submatrix (⇑e) f).rowFun i = 0 → ∀ i ∈ s, g i = 0
s : Finset m
c : m → R
hc : ∑ i ∈ s, c i • A.rowFun i = 0
i : m
his : i ∈ s
⊢ ∑ i ∈ Finset.image (⇑e.symm) s, (c ∘ ⇑e) i • (A.submatrix (⇑e) f).rowFun i = 0
Tactic:
ext j
State after:
case h
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✝
m : Type u_11
n : Type u_12
R : Type u_13
s✝ : Set m
t : Set n
A B : Matrix m n R
inst✝ : Ring R
m₀ : Type u_14
n₀ : Type u_15
e : m₀ ≃ m
f : n₀ → n
h : ∀ (s : Finset m₀) (g : m₀ → R), ∑ i ∈ s, g i • (A.submatrix (⇑e) f).rowFun i = 0 → ∀ i ∈ s, g i = 0
s : Finset m
c : m → R
hc : ∑ i ∈ s, c i • A.rowFun i = 0
i : m
his : i ∈ s
j : n₀
⊢ (∑ i ∈ Finset.image (⇑e.symm) s, (c ∘ ⇑e) i • (A.submatrix (⇑e) f).rowFun i) j = 0 j

State before:
case h
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✝
m : Type u_11
n : Type u_12
R : Type u_13
s✝ : Set m
t : Set n
A B : Matrix m n R
inst✝ : Ring R
m₀ : Type u_14
n₀ : Type u_15
e : m₀ ≃ m
f : n₀ → n
h : ∀ (s : Finset m₀) (g : m₀ → R), ∑ i ∈ s, g i • (A.submatrix (⇑e) f).rowFun i = 0 → ∀ i ∈ s, g i = 0
s : Finset m
c : m → R
hc : ∑ i ∈ s, c i • A.rowFun i = 0
i : m
his : i ∈ s
j : n₀
⊢ (∑ i ∈ Finset.image (⇑e.symm) s, (c ∘ ⇑e) i • (A.submatrix (⇑e) f).rowFun i) j = 0 j
Tactic:
convert congr_fun hc (f j)
State after:
case h.e'_2
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✝
m : Type u_11
n : Type u_12
R : Type u_13
s✝ : Set m
t : Set n
A B : Matrix m n R
inst✝ : Ring R
m₀ : Type u_14
n₀ : Type u_15
e : m₀ ≃ m
f : n₀ → n
h : ∀ (s : Finset m₀) (g : m₀ → R), ∑ i ∈ s, g i • (A.submatrix (⇑e) f).rowFun i = 0 → ∀ i ∈ s, g i = 0
s : Finset m
c : m → R
hc : ∑ i ∈ s, c i • A.rowFun i = 0
i : m
his : i ∈ s
j : n₀
⊢ (∑ i ∈ Finset.image (⇑e.symm) s, (c ∘ ⇑e) i • (A.submatrix (⇑e) f).rowFun i) j = (∑ i ∈ s, c i • A.rowFun i) (f j)

State before:
case h.e'_2
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✝
m : Type u_11
n : Type u_12
R : Type u_13
s✝ : Set m
t : Set n
A B : Matrix m n R
inst✝ : Ring R
m₀ : Type u_14
n₀ : Type u_15
e : m₀ ≃ m
f : n₀ → n
h : ∀ (s : Finset m₀) (g : m₀ → R), ∑ i ∈ s, g i • (A.submatrix (⇑e) f).rowFun i = 0 → ∀ i ∈ s, g i = 0
s : Finset m
c : m → R
hc : ∑ i ∈ s, c i • A.rowFun i = 0
i : m
his : i ∈ s
j : n₀
⊢ (∑ i ∈ Finset.image (⇑e.symm) s, (c ∘ ⇑e) i • (A.submatrix (⇑e) f).rowFun i) j = (∑ i ∈ s, c i • A.rowFun i) (f j)
Tactic:
simp
State after:
no goals

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✝
m : Type u_11
n : Type u_12
R : Type u_13
s✝ : Set m
t : Set n
A B : Matrix m n R
inst✝ : Ring R
m₀ : Type u_14
n₀ : Type u_15
e : m₀ ≃ m
f : n₀ → n
h : ∀ (s : Finset m₀) (g : m₀ → R), ∑ i ∈ s, g i • (A.submatrix (⇑e) f).rowFun i = 0 → ∀ i ∈ s, g i = 0
s : Finset m
c : m → R
hc : ∑ i ∈ s, c i • A.rowFun i = 0
i : m
his : i ∈ s
⊢ e.symm i ∈ Finset.image (⇑e.symm) s
Tactic:
simpa
State after:
no goals

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✝
m : Type u_11
n : Type u_12
R : Type u_13
s✝ : Set m
t : Set n
A B : Matrix m n R
inst✝ : Ring R
m₀ : Type u_14
n₀ : Type u_15
e : m₀ ≃ m
f : n₀ → n
h : ∀ (s : Finset m₀) (g : m₀ → R), ∑ i ∈ s, g i • (A.submatrix (⇑e) f).rowFun i = 0 → ∀ i ∈ s, g i = 0
s : Finset m
c : m → R
hc : ∑ i ∈ s, c i • A.rowFun i = 0
i : m
his : i ∈ s
⊢ c i = (c ∘ ⇑e) (e.symm i)
Tactic:
simp
State after:
no goals