case a.h
R : Type u_1
inst✝² : CommSemiring R
k : Type ?u.523416
l : Type ?u.523419
m : Type ?u.523422
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
i✝ x✝ : n
⊢ ↑toMatrix' id i✝ x✝ = OfNat.ofNat 1 i✝ x✝
R : Type u_1
inst✝² : CommSemiring R
k : Type ?u.523416
l : Type ?u.523419
m : Type ?u.523422
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
⊢ ↑toMatrix' id = 1
ext
no goals
case a.h
R : Type u_1
inst✝² : CommSemiring R
k : Type ?u.523416
l : Type ?u.523419
m : Type ?u.523422
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
i✝ x✝ : n
⊢ ↑toMatrix' id i✝ x✝ = OfNat.ofNat 1 i✝ x✝
rw [Matrix.one_apply, LinearMap.toMatrix'_apply, id_apply]