case a.h
l : Type ?u.1222192
m : Type u_1
n : Type u_2
o : Type ?u.1222201
m' : o → Type ?u.1222206
n' : o → Type ?u.1222211
R : Type u_3
S : Type ?u.1222217
α : Type v
β : Type w
γ : Type ?u.1222224
M : Matrix m n α
i✝ : m
j : n
b✝ : n → α
c : m → α
inst✝ : Subsingleton m
A : Matrix m n R
i : m
b : n → R
x : m
y : n
⊢ updateRow A i b x y = submatrix (row b) (Function.const m ()) id x y
l : Type ?u.1222192
m : Type u_1
n : Type u_2
o : Type ?u.1222201
m' : o → Type ?u.1222206
n' : o → Type ?u.1222211
R : Type u_3
S : Type ?u.1222217
α : Type v
β : Type w
γ : Type ?u.1222224
M : Matrix m n α
i✝ : m
j : n
b✝ : n → α
c : m → α
inst✝ : Subsingleton m
A : Matrix m n R
i : m
b : n → R
⊢ updateRow A i b = submatrix (row b) (Function.const m ()) id
ext x y
no goals
case a.h
l : Type ?u.1222192
m : Type u_1
n : Type u_2
o : Type ?u.1222201
m' : o → Type ?u.1222206
n' : o → Type ?u.1222211
R : Type u_3
S : Type ?u.1222217
α : Type v
β : Type w
γ : Type ?u.1222224
M : Matrix m n α
i✝ : m
j : n
b✝ : n → α
c : m → α
inst✝ : Subsingleton m
A : Matrix m n R
i : m
b : n → R
x : m
y : n
⊢ updateRow A i b x y = submatrix (row b) (Function.const m ()) id x y
simp [updateColumn_apply, Subsingleton.elim i x]