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.19562
m' : o → Type ?u.19567
n' : o → Type ?u.19572
p' : o → Type ?u.19577
R : Type ?u.19580
S : Type ?u.19583
α : Type u_3
β : Type ?u.19589
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
f : p → n ⊕ o
i : p
j : m ⊕ l
⊢ submatrix (fromBlocks A B C D) f Sum.swap i j = submatrix (fromBlocks B A D C) f id 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.19562
m' : o → Type ?u.19567
n' : o → Type ?u.19572
p' : o → Type ?u.19577
R : Type ?u.19580
S : Type ?u.19583
α : Type u_3
β : Type ?u.19589
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
f : p → n ⊕ o
⊢ submatrix (fromBlocks A B C D) f Sum.swap = submatrix (fromBlocks B A D C) f id
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.19562
m' : o → Type ?u.19567
n' : o → Type ?u.19572
p' : o → Type ?u.19577
R : Type ?u.19580
S : Type ?u.19583
α : Type u_3
β : Type ?u.19589
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
f : p → n ⊕ o
i : p
j : m ⊕ l
⊢ submatrix (fromBlocks A B C D) f Sum.swap i j = submatrix (fromBlocks B A D C) f id i j
cases j <;> dsimp <;> cases f i <;> rfl