case h
l : Type u_1
m : Type u_2
n : Type u_4
o : Type u_5
p : Type ?u.43962
q : Type ?u.43965
m' : o → Type ?u.43970
n' : o → Type ?u.43975
p' : o → Type ?u.43980
R : Type ?u.43983
S : Type ?u.43986
α : Type u_3
β : Type ?u.43992
inst✝² : Fintype l
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
x : l ⊕ m → α
i : n ⊕ o
⊢ mulVec (fromBlocks A B C D) x i =
    Sum.elim (mulVec A (x ∘ Sum.inl) + mulVec B (x ∘ Sum.inr)) (mulVec C (x ∘ Sum.inl) + mulVec D (x ∘ Sum.inr)) i
l : Type u_1
m : Type u_2
n : Type u_4
o : Type u_5
p : Type ?u.43962
q : Type ?u.43965
m' : o → Type ?u.43970
n' : o → Type ?u.43975
p' : o → Type ?u.43980
R : Type ?u.43983
S : Type ?u.43986
α : Type u_3
β : Type ?u.43992
inst✝² : Fintype l
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
x : l ⊕ m → α
⊢ mulVec (fromBlocks A B C D) x =
    Sum.elim (mulVec A (x ∘ Sum.inl) + mulVec B (x ∘ Sum.inr)) (mulVec C (x ∘ Sum.inl) + mulVec D (x ∘ Sum.inr))
ext i
no goals
case h
l : Type u_1
m : Type u_2
n : Type u_4
o : Type u_5
p : Type ?u.43962
q : Type ?u.43965
m' : o → Type ?u.43970
n' : o → Type ?u.43975
p' : o → Type ?u.43980
R : Type ?u.43983
S : Type ?u.43986
α : Type u_3
β : Type ?u.43992
inst✝² : Fintype l
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
x : l ⊕ m → α
i : n ⊕ o
⊢ mulVec (fromBlocks A B C D) x i =
    Sum.elim (mulVec A (x ∘ Sum.inl) + mulVec B (x ∘ Sum.inr)) (mulVec C (x ∘ Sum.inl) + mulVec D (x ∘ Sum.inr)) i
cases i <;> simp [mulVec, dotProduct]