case a.h
l : Type u_2
m : Type u_4
n : Type u_1
o : Type u_5
p : Type ?u.6743
q : Type ?u.6746
m' : o → Type ?u.6751
n' : o → Type ?u.6756
p' : o → Type ?u.6761
R : Type ?u.6764
S : Type ?u.6767
α : Type u_3
β : Type u_6
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
f : α → β
i : n ⊕ o
j : l ⊕ m
⊢ map (fromBlocks A B C D) f i j = fromBlocks (map A f) (map B f) (map C f) (map D f) i j
l : Type u_2
m : Type u_4
n : Type u_1
o : Type u_5
p : Type ?u.6743
q : Type ?u.6746
m' : o → Type ?u.6751
n' : o → Type ?u.6756
p' : o → Type ?u.6761
R : Type ?u.6764
S : Type ?u.6767
α : Type u_3
β : Type u_6
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
f : α → β
⊢ map (fromBlocks A B C D) f = fromBlocks (map A f) (map B f) (map C f) (map D 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.6743
q : Type ?u.6746
m' : o → Type ?u.6751
n' : o → Type ?u.6756
p' : o → Type ?u.6761
R : Type ?u.6764
S : Type ?u.6767
α : Type u_3
β : Type u_6
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
f : α → β
i : n ⊕ o
j : l ⊕ m
⊢ map (fromBlocks A B C D) f i j = fromBlocks (map A f) (map B f) (map C f) (map D f) i j
rcases i with ⟨⟩ <;> rcases j with ⟨⟩ <;> simp [fromBlocks]