use "2" to denote 2 times the unit matrix

Stream: new members

[Z. X. Wang]

i want to prove that

2 i j = 2 * 1 i j

where the previous "2" denote two times the unit matrix, and the later "2" is just a Nat, and "1" is the unit matrix. But now i feel confused about the way that lean define the previous "2", so there is some trouble for me to prove the simple proposition.

[Z. X. Wang]

Here is the code

import Mathlib

open Matrix

example : 2 = 2 • (1 : Matrix (Fin n) (Fin n) ℝ) := by
  refine ext ?_
  intro i j
  simp only [smul_apply, nsmul_eq_mul, Nat.cast_ofNat]
  sorry

[Yuyang Zhao]

import Mathlib

open Matrix

example : 2 = 2 • (1 : Matrix (Fin n) (Fin n) ℝ) := by
  simp [nsmul_eq_mul]

edit: actually there is no need to write any lemma in simp...