Module: Mathlib.LinearAlgebra.Matrix.SchurComplement

Goal state before:
pp: case inl.inl
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
inst✝ : Invertible D
val✝¹ val✝ : m
⊢ fromBlocks A B C D (Sum.inl val✝¹) (Sum.inl val✝) =
    (fromBlocks D C B A).submatrix (⇑(Equiv.sumComm m n)) (⇑(Equiv.sumComm m n)) (Sum.inl val✝¹) (Sum.inl val✝)

pp: case inl.inr
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
inst✝ : Invertible D
val✝¹ : m
val✝ : n
⊢ fromBlocks A B C D (Sum.inl val✝¹) (Sum.inr val✝) =
    (fromBlocks D C B A).submatrix (⇑(Equiv.sumComm m n)) (⇑(Equiv.sumComm m n)) (Sum.inl val✝¹) (Sum.inr val✝)

pp: case inr.inl
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
inst✝ : Invertible D
val✝¹ : n
val✝ : m
⊢ fromBlocks A B C D (Sum.inr val✝¹) (Sum.inl val✝) =
    (fromBlocks D C B A).submatrix (⇑(Equiv.sumComm m n)) (⇑(Equiv.sumComm m n)) (Sum.inr val✝¹) (Sum.inl val✝)

pp: case inr.inr
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
inst✝ : Invertible D
val✝¹ val✝ : n
⊢ fromBlocks A B C D (Sum.inr val✝¹) (Sum.inr val✝) =
    (fromBlocks D C B A).submatrix (⇑(Equiv.sumComm m n)) (⇑(Equiv.sumComm m n)) (Sum.inr val✝¹) (Sum.inr val✝)

Tactic:
<;>

Goal state after:
case inl.inl
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
inst✝ : Invertible D
val✝¹ val✝ : m
⊢ fromBlocks A B C D (Sum.inl val✝¹) (Sum.inl val✝) =
    (fromBlocks D C B A).submatrix (⇑(Equiv.sumComm m n)) (⇑(Equiv.sumComm m n)) (Sum.inl val✝¹) (Sum.inl val✝)

case inl.inr
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
inst✝ : Invertible D
val✝¹ : m
val✝ : n
⊢ fromBlocks A B C D (Sum.inl val✝¹) (Sum.inr val✝) =
    (fromBlocks D C B A).submatrix (⇑(Equiv.sumComm m n)) (⇑(Equiv.sumComm m n)) (Sum.inl val✝¹) (Sum.inr val✝)

case inr.inl
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
inst✝ : Invertible D
val✝¹ : n
val✝ : m
⊢ fromBlocks A B C D (Sum.inr val✝¹) (Sum.inl val✝) =
    (fromBlocks D C B A).submatrix (⇑(Equiv.sumComm m n)) (⇑(Equiv.sumComm m n)) (Sum.inr val✝¹) (Sum.inl val✝)

case inr.inr
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
inst✝ : Invertible D
val✝¹ val✝ : n
⊢ fromBlocks A B C D (Sum.inr val✝¹) (Sum.inr val✝) =
    (fromBlocks D C B A).submatrix (⇑(Equiv.sumComm m n)) (⇑(Equiv.sumComm m n)) (Sum.inr val✝¹) (Sum.inr val✝)