no goals
l✝ : Type ?u.20447
m✝ : Type ?u.20450
n✝ : Type ?u.20453
o✝ : Type ?u.20456
p : Type ?u.20459
q : Type ?u.20462
m' : o✝ → Type ?u.20467
n' : o✝ → Type ?u.20472
p' : o✝ → Type ?u.20477
R : Type ?u.20480
S : Type ?u.20483
α✝ : Type ?u.20486
β : Type ?u.20489
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_5
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
⊢ submatrix (fromBlocks A B C D) Sum.swap Sum.swap = fromBlocks D C B A
simp