Theorem: Matrix.rows_linearIndependent_union_of_upper_zero_block
Proof state before:
case h.e'_4.h.h.e'_4.h.a.inl.inr
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
e_1✝ : ({ a // a ∈ s } ⊕ { a // a ∉ s }) = (↑s ⊕ ↑sᶜ)
e_3✝ : ({ a // a ∈ t } ⊕ { a // a ∉ t } → R) = (↑t ⊕ ↑tᶜ → R)
e_2✝ : ({ a // a ∈ t } ⊕ { a // a ∉ t }) = (↑t ⊕ ↑tᶜ)
i : { a // a ∈ s }
j : { a // a ∉ t }
⊢ A.submatrix (⇑(Equiv.sumCompl fun x => x ∈ s)) (⇑(Equiv.sumCompl fun x => x ∈ t)) (Sum.inl i) (Sum.inr j) =
    (A.submatrix s.incl t.incl).fromBlocks 0 (A.submatrix sᶜ.incl t.incl) (A.submatrix sᶜ.incl tᶜ.incl) (Sum.inl i)
      (Sum.inr j)

case h.e'_4.h.h.e'_4.h.a.inr.inl
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
e_1✝ : ({ a // a ∈ s } ⊕ { a // a ∉ s }) = (↑s ⊕ ↑sᶜ)
e_3✝ : ({ a // a ∈ t } ⊕ { a // a ∉ t } → R) = (↑t ⊕ ↑tᶜ → R)
e_2✝ : ({ a // a ∈ t } ⊕ { a // a ∉ t }) = (↑t ⊕ ↑tᶜ)
i : { a // a ∉ s }
j : { a // a ∈ t }
⊢ A.submatrix (⇑(Equiv.sumCompl fun x => x ∈ s)) (⇑(Equiv.sumCompl fun x => x ∈ t)) (Sum.inr i) (Sum.inl j) =
    (A.submatrix s.incl t.incl).fromBlocks 0 (A.submatrix sᶜ.incl t.incl) (A.submatrix sᶜ.incl tᶜ.incl) (Sum.inr i)
      (Sum.inl j)

case h.e'_4.h.h.e'_4.h.a.inr.inr
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
e_1✝ : ({ a // a ∈ s } ⊕ { a // a ∉ s }) = (↑s ⊕ ↑sᶜ)
e_3✝ : ({ a // a ∈ t } ⊕ { a // a ∉ t } → R) = (↑t ⊕ ↑tᶜ → R)
e_2✝ : ({ a // a ∈ t } ⊕ { a // a ∉ t }) = (↑t ⊕ ↑tᶜ)
i : { a // a ∉ s }
j : { a // a ∉ t }
⊢ A.submatrix (⇑(Equiv.sumCompl fun x => x ∈ s)) (⇑(Equiv.sumCompl fun x => x ∈ t)) (Sum.inr i) (Sum.inr j) =
    (A.submatrix s.incl t.incl).fromBlocks 0 (A.submatrix sᶜ.incl t.incl) (A.submatrix sᶜ.incl tᶜ.incl) (Sum.inr i)
      (Sum.inr j)
Tactic:
exact congr_fun (congr_fun h0 i) j
Proof state after:
case h.e'_4.h.h.e'_4.h.a.inr.inl
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
e_1✝ : ({ a // a ∈ s } ⊕ { a // a ∉ s }) = (↑s ⊕ ↑sᶜ)
e_3✝ : ({ a // a ∈ t } ⊕ { a // a ∉ t } → R) = (↑t ⊕ ↑tᶜ → R)
e_2✝ : ({ a // a ∈ t } ⊕ { a // a ∉ t }) = (↑t ⊕ ↑tᶜ)
i : { a // a ∉ s }
j : { a // a ∈ t }
⊢ A.submatrix (⇑(Equiv.sumCompl fun x => x ∈ s)) (⇑(Equiv.sumCompl fun x => x ∈ t)) (Sum.inr i) (Sum.inl j) =
    (A.submatrix s.incl t.incl).fromBlocks 0 (A.submatrix sᶜ.incl t.incl) (A.submatrix sᶜ.incl tᶜ.incl) (Sum.inr i)
      (Sum.inl j)

case h.e'_4.h.h.e'_4.h.a.inr.inr
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
e_1✝ : ({ a // a ∈ s } ⊕ { a // a ∉ s }) = (↑s ⊕ ↑sᶜ)
e_3✝ : ({ a // a ∈ t } ⊕ { a // a ∉ t } → R) = (↑t ⊕ ↑tᶜ → R)
e_2✝ : ({ a // a ∈ t } ⊕ { a // a ∉ t }) = (↑t ⊕ ↑tᶜ)
i : { a // a ∉ s }
j : { a // a ∉ t }
⊢ A.submatrix (⇑(Equiv.sumCompl fun x => x ∈ s)) (⇑(Equiv.sumCompl fun x => x ∈ t)) (Sum.inr i) (Sum.inr j) =
    (A.submatrix s.incl t.incl).fromBlocks 0 (A.submatrix sᶜ.incl t.incl) (A.submatrix sᶜ.incl tᶜ.incl) (Sum.inr i)
      (Sum.inr j)