Theorem: Matrix.rows_linearIndependent_reindex (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
em : m' ≃ m
en : n' ≃ n
h : LinearIndependent R A.rowFun
⊢ LinearIndependent R (A.submatrix ⇑em ⇑en).rowFun
Tactic:
rw [show A = (A.submatrix em en).submatrix em.symm en.symm from by simp]  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
em : m' ≃ m
en : n' ≃ n
h : LinearIndependent R ((A.submatrix ⇑em ⇑en).submatrix ⇑em.symm ⇑en.symm).rowFun
⊢ LinearIndependent R (A.submatrix ⇑em ⇑en).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
em : m' ≃ m
en : n' ≃ n
h : LinearIndependent R ((A.submatrix ⇑em ⇑en).submatrix ⇑em.symm ⇑en.symm).rowFun
⊢ LinearIndependent R (A.submatrix ⇑em ⇑en).rowFun
Tactic:
exact rows_linearIndependent_of_submatrix _ _ h
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
em : m' ≃ m
en : n' ≃ n
h : LinearIndependent R A.rowFun
⊢ A = (A.submatrix ⇑em ⇑en).submatrix ⇑em.symm ⇑en.symm
Tactic:
simp
State after:
no goals