Mathlib: det of a linear map on ℍ via basisOneIJK; simp can't evaluate (basisOneIJK j).re

To compute LinearMap.det of a map on Quaternion ℝ (e.g. conjugation, det = -1), rewrite with ← LinearMap.det_toMatrix (QuaternionAlgebra.basisOneIJK (-1 : ℝ) 0 (-1)), then show toMatrix = Matrix.diagonal ![1,-1,-1,-1] via ext i j; fin_cases i <;> fin_cases j <;> simp [LinearMap.toMatrix_apply, ...]. simp gets stuck on goals like ((basisOneIJK (-1) 0 (-1)) 1).imI = 1, because there is no simp lemma for the basis vectors themselves (only coe_basisOneIJK_repr). Fix: local lemmas have h1 (j : Fin 4) : (b j).imI = Finsupp.single j (1:ℝ) 1 := by rw [← b.repr_self]; rfl, and the same for re/imJ/imK. The rfl works because coe_basisOneIJK_repr is itself rfl. Pass them to simp. Then Matrix.det_diagonal, Fin.prod_univ_four, norm_num.