case h.h.h
R : Type u_2
inst✝² : CommSemiring R
k : Type ?u.293203
l : Type ?u.293206
m : Type ?u.293209
n : Type u_1
inst✝¹ : Fintype n
inst✝ : DecidableEq n
i✝ x✝ : n
⊢ ↑(comp (mulVecLin 1) (single i✝)) 1 x✝ = ↑(comp LinearMap.id (single i✝)) 1 x✝
R : Type u_2
inst✝² : CommSemiring R
k : Type ?u.293203
l : Type ?u.293206
m : Type ?u.293209
n : Type u_1
inst✝¹ : Fintype n
inst✝ : DecidableEq n
⊢ mulVecLin 1 = LinearMap.id
ext
no goals
case h.h.h
R : Type u_2
inst✝² : CommSemiring R
k : Type ?u.293203
l : Type ?u.293206
m : Type ?u.293209
n : Type u_1
inst✝¹ : Fintype n
inst✝ : DecidableEq n
i✝ x✝ : n
⊢ ↑(comp (mulVecLin 1) (single i✝)) 1 x✝ = ↑(comp LinearMap.id (single i✝)) 1 x✝
simp [Matrix.one_apply, Pi.single_apply]