case a.h
l : Type u_1
m : Type u_2
n : Type u_4
o : Type u_5
p : Type u_6
q : Type u_7
m' : o → Type ?u.37702
n' : o → Type ?u.37707
p' : o → Type ?u.37712
R : Type ?u.37715
S : Type ?u.37718
α : Type u_3
β : Type ?u.37724
inst✝² : Fintype l
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
A' : Matrix l p α
B' : Matrix l q α
C' : Matrix m p α
D' : Matrix m q α
i : n ⊕ o
j : p ⊕ q
⊢ (fromBlocks A B C D ⬝ fromBlocks A' B' C' D') i j =
    fromBlocks (A ⬝ A' + B ⬝ C') (A ⬝ B' + B ⬝ D') (C ⬝ A' + D ⬝ C') (C ⬝ B' + D ⬝ D') i j
l : Type u_1
m : Type u_2
n : Type u_4
o : Type u_5
p : Type u_6
q : Type u_7
m' : o → Type ?u.37702
n' : o → Type ?u.37707
p' : o → Type ?u.37712
R : Type ?u.37715
S : Type ?u.37718
α : Type u_3
β : Type ?u.37724
inst✝² : Fintype l
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
A' : Matrix l p α
B' : Matrix l q α
C' : Matrix m p α
D' : Matrix m q α
⊢ fromBlocks A B C D ⬝ fromBlocks A' B' C' D' =
    fromBlocks (A ⬝ A' + B ⬝ C') (A ⬝ B' + B ⬝ D') (C ⬝ A' + D ⬝ C') (C ⬝ B' + D ⬝ D')
ext i j
no goals
case a.h
l : Type u_1
m : Type u_2
n : Type u_4
o : Type u_5
p : Type u_6
q : Type u_7
m' : o → Type ?u.37702
n' : o → Type ?u.37707
p' : o → Type ?u.37712
R : Type ?u.37715
S : Type ?u.37718
α : Type u_3
β : Type ?u.37724
inst✝² : Fintype l
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
A' : Matrix l p α
B' : Matrix l q α
C' : Matrix m p α
D' : Matrix m q α
i : n ⊕ o
j : p ⊕ q
⊢ (fromBlocks A B C D ⬝ fromBlocks A' B' C' D') i j =
    fromBlocks (A ⬝ A' + B ⬝ C') (A ⬝ B' + B ⬝ D') (C ⬝ A' + D ⬝ C') (C ⬝ B' + D ⬝ D') i j
rcases i with ⟨⟩ <;> rcases j with ⟨⟩ <;> simp only [fromBlocks, mul_apply, of_apply,
    Sum.elim_inr, Fintype.sum_sum_type, Sum.elim_inl, add_apply]