case a.h
l : Type ?u.1221200
m : Type u_2
n : Type u_1
o : Type ?u.1221209
m' : o → Type ?u.1221214
n' : o → Type ?u.1221219
R : Type u_3
S : Type ?u.1221225
α : Type v
β : Type w
γ : Type ?u.1221232
M : Matrix m n α
i✝ : m
j : n
b✝ : n → α
c : m → α
inst✝ : Subsingleton n
A : Matrix m n R
i : n
b : m → R
x : m
y : n
⊢ updateColumn A i b x y = submatrix (col b) id (Function.const n ()) x y
l : Type ?u.1221200
m : Type u_2
n : Type u_1
o : Type ?u.1221209
m' : o → Type ?u.1221214
n' : o → Type ?u.1221219
R : Type u_3
S : Type ?u.1221225
α : Type v
β : Type w
γ : Type ?u.1221232
M : Matrix m n α
i✝ : m
j : n
b✝ : n → α
c : m → α
inst✝ : Subsingleton n
A : Matrix m n R
i : n
b : m → R
⊢ updateColumn A i b = submatrix (col b) id (Function.const n ())
ext x y
no goals
case a.h
l : Type ?u.1221200
m : Type u_2
n : Type u_1
o : Type ?u.1221209
m' : o → Type ?u.1221214
n' : o → Type ?u.1221219
R : Type u_3
S : Type ?u.1221225
α : Type v
β : Type w
γ : Type ?u.1221232
M : Matrix m n α
i✝ : m
j : n
b✝ : n → α
c : m → α
inst✝ : Subsingleton n
A : Matrix m n R
i : n
b : m → R
x : m
y : n
⊢ updateColumn A i b x y = submatrix (col b) id (Function.const n ()) x y
simp [updateColumn_apply, Subsingleton.elim i y]