Theorem: Matrix.linearIndependent_rows_of_lower_tri (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
m₁ : Type u_15
n₀ : Type u_16
n₁ : Type u_17
A : Matrix m₀ n₀ R
B : Matrix m₁ n₀ R
C : Matrix m₁ n₁ R
hA : LinearIndependent R A.rowFun
hC : LinearIndependent R C.rowFun
⊢ LinearIndependent R (A.fromBlocks 0 B C).rowFun
Tactic:
refine rows_linearIndependent_of_reindex (Equiv.sumComm _ _) (Equiv.sumComm _ _) ?_
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
m₁ : Type u_15
n₀ : Type u_16
n₁ : Type u_17
A : Matrix m₀ n₀ R
B : Matrix m₁ n₀ R
C : Matrix m₁ n₁ R
hA : LinearIndependent R A.rowFun
hC : LinearIndependent R C.rowFun
⊢ LinearIndependent R ((A.fromBlocks 0 B C).submatrix ⇑(Equiv.sumComm m₁ m₀) ⇑(Equiv.sumComm n₁ n₀)).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
m₀ : Type u_14
m₁ : Type u_15
n₀ : Type u_16
n₁ : Type u_17
A : Matrix m₀ n₀ R
B : Matrix m₁ n₀ R
C : Matrix m₁ n₁ R
hA : LinearIndependent R A.rowFun
hC : LinearIndependent R C.rowFun
⊢ LinearIndependent R ((A.fromBlocks 0 B C).submatrix ⇑(Equiv.sumComm m₁ m₀) ⇑(Equiv.sumComm n₁ n₀)).rowFun
Tactic:
convert linearIndependent_rows_of_upper_tri C B A hC hA
State after:
case h.e'_4.h.e'_4
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
m₁ : Type u_15
n₀ : Type u_16
n₁ : Type u_17
A : Matrix m₀ n₀ R
B : Matrix m₁ n₀ R
C : Matrix m₁ n₁ R
hA : LinearIndependent R A.rowFun
hC : LinearIndependent R C.rowFun
⊢ (A.fromBlocks 0 B C).submatrix ⇑(Equiv.sumComm m₁ m₀) ⇑(Equiv.sumComm n₁ n₀) = C.fromBlocks B 0 A

State before:
case h.e'_4.h.e'_4
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
m₁ : Type u_15
n₀ : Type u_16
n₁ : Type u_17
A : Matrix m₀ n₀ R
B : Matrix m₁ n₀ R
C : Matrix m₁ n₁ R
hA : LinearIndependent R A.rowFun
hC : LinearIndependent R C.rowFun
⊢ (A.fromBlocks 0 B C).submatrix ⇑(Equiv.sumComm m₁ m₀) ⇑(Equiv.sumComm n₁ n₀) = C.fromBlocks B 0 A
Tactic:
simp only [Equiv.sumComm_apply, fromBlocks_submatrix_sum_swap_right,
  fromBlocks_submatrix_sum_swap_left, submatrix_id_id]
State after:
no goals