case a.h
l : Type u_2
m : Type u_4
n : Type u_1
o : Type u_5
p : Type u_6
q : Type ?u.18703
m' : o → Type ?u.18708
n' : o → Type ?u.18713
p' : o → Type ?u.18718
R : Type ?u.18721
S : Type ?u.18724
α : Type u_3
β : Type ?u.18730
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
f : p → l ⊕ m
i : o ⊕ n
j : p
⊢ submatrix (fromBlocks A B C D) Sum.swap f i j = submatrix (fromBlocks C D A B) id f i j
l : Type u_2
m : Type u_4
n : Type u_1
o : Type u_5
p : Type u_6
q : Type ?u.18703
m' : o → Type ?u.18708
n' : o → Type ?u.18713
p' : o → Type ?u.18718
R : Type ?u.18721
S : Type ?u.18724
α : Type u_3
β : Type ?u.18730
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
f : p → l ⊕ m
⊢ submatrix (fromBlocks A B C D) Sum.swap f = submatrix (fromBlocks C D A B) id f
ext (i j)
no goals
case a.h
l : Type u_2
m : Type u_4
n : Type u_1
o : Type u_5
p : Type u_6
q : Type ?u.18703
m' : o → Type ?u.18708
n' : o → Type ?u.18713
p' : o → Type ?u.18718
R : Type ?u.18721
S : Type ?u.18724
α : Type u_3
β : Type ?u.18730
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
f : p → l ⊕ m
i : o ⊕ n
j : p
⊢ submatrix (fromBlocks A B C D) Sum.swap f i j = submatrix (fromBlocks C D A B) id f i j
cases i <;> dsimp <;> cases f j <;> rfl