Theorem: Matrix.rows_linearIndependent_union_of_lower_zero_block (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
hst : LinearIndependent (ι := ↑s) R (A.submatrix s.incl t.incl).rowFun
hstc : LinearIndependent (ι := ↑sᶜ) R (A.submatrix sᶜ.incl tᶜ.incl).rowFun
h0 : A.submatrix sᶜ.incl t.incl = 0
⊢ LinearIndependent R A.rowFun
Tactic:
rw [← compl_compl s, ← compl_compl t] at hst
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
hst : LinearIndependent (ι := ↑sᶜᶜ) R (A.submatrix sᶜᶜ.incl tᶜᶜ.incl).rowFun
hstc : LinearIndependent (ι := ↑sᶜ) R (A.submatrix sᶜ.incl tᶜ.incl).rowFun
h0 : A.submatrix sᶜ.incl t.incl = 0
⊢ LinearIndependent R A.rowFun

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
hst : LinearIndependent (ι := ↑sᶜᶜ) R (A.submatrix sᶜᶜ.incl tᶜᶜ.incl).rowFun
hstc : LinearIndependent (ι := ↑sᶜ) R (A.submatrix sᶜ.incl tᶜ.incl).rowFun
h0 : A.submatrix sᶜ.incl t.incl = 0
⊢ LinearIndependent R A.rowFun
Tactic:
apply rows_linearIndependent_union_of_upper_zero_block hstc hst
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
hst : LinearIndependent (ι := ↑sᶜᶜ) R (A.submatrix sᶜᶜ.incl tᶜᶜ.incl).rowFun
hstc : LinearIndependent (ι := ↑sᶜ) R (A.submatrix sᶜ.incl tᶜ.incl).rowFun
h0 : A.submatrix sᶜ.incl t.incl = 0
⊢ A.submatrix sᶜ.incl tᶜᶜ.incl = 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
hst : LinearIndependent (ι := ↑sᶜᶜ) R (A.submatrix sᶜᶜ.incl tᶜᶜ.incl).rowFun
hstc : LinearIndependent (ι := ↑sᶜ) R (A.submatrix sᶜ.incl tᶜ.incl).rowFun
h0 : A.submatrix sᶜ.incl t.incl = 0
⊢ A.submatrix sᶜ.incl tᶜᶜ.incl = 0
Tactic:
rw [compl_compl]
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
hst : LinearIndependent (ι := ↑sᶜᶜ) R (A.submatrix sᶜᶜ.incl tᶜᶜ.incl).rowFun
hstc : LinearIndependent (ι := ↑sᶜ) R (A.submatrix sᶜ.incl tᶜ.incl).rowFun
h0 : A.submatrix sᶜ.incl t.incl = 0
⊢ A.submatrix sᶜ.incl t.incl = 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
hst : LinearIndependent (ι := ↑sᶜᶜ) R (A.submatrix sᶜᶜ.incl tᶜᶜ.incl).rowFun
hstc : LinearIndependent (ι := ↑sᶜ) R (A.submatrix sᶜ.incl tᶜ.incl).rowFun
h0 : A.submatrix sᶜ.incl t.incl = 0
⊢ A.submatrix sᶜ.incl t.incl = 0
Tactic:
exact h0
State after:
no goals