case a.h
l : Type u_3
m : Type u_4
n : Type u_2
o : Type u_5
p : Type ?u.36919
q : Type ?u.36922
m' : o → Type ?u.36927
n' : o → Type ?u.36932
p' : o → Type ?u.36937
R : Type ?u.36940
S : Type ?u.36943
α : Type u_1
β : Type ?u.36949
inst✝ : Add α
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
A' : Matrix n l α
B' : Matrix n m α
C' : Matrix o l α
D' : Matrix o m α
i : n ⊕ o
j : l ⊕ m
⊢ (fromBlocks A B C D + fromBlocks A' B' C' D') i j = fromBlocks (A + A') (B + B') (C + C') (D + D') i j
l : Type u_3
m : Type u_4
n : Type u_2
o : Type u_5
p : Type ?u.36919
q : Type ?u.36922
m' : o → Type ?u.36927
n' : o → Type ?u.36932
p' : o → Type ?u.36937
R : Type ?u.36940
S : Type ?u.36943
α : Type u_1
β : Type ?u.36949
inst✝ : Add α
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
A' : Matrix n l α
B' : Matrix n m α
C' : Matrix o l α
D' : Matrix o m α
⊢ fromBlocks A B C D + fromBlocks A' B' C' D' = fromBlocks (A + A') (B + B') (C + C') (D + D')
ext (i j)
no goals
case a.h
l : Type u_3
m : Type u_4
n : Type u_2
o : Type u_5
p : Type ?u.36919
q : Type ?u.36922
m' : o → Type ?u.36927
n' : o → Type ?u.36932
p' : o → Type ?u.36937
R : Type ?u.36940
S : Type ?u.36943
α : Type u_1
β : Type ?u.36949
inst✝ : Add α
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
A' : Matrix n l α
B' : Matrix n m α
C' : Matrix o l α
D' : Matrix o m α
i : n ⊕ o
j : l ⊕ m
⊢ (fromBlocks A B C D + fromBlocks A' B' C' D') i j = fromBlocks (A + A') (B + B') (C + C') (D + D') i j
rcases i with ⟨⟩ <;> rcases j with ⟨⟩ <;> rfl