regression due to #10199

Stream: general

[Yakov Pechersky]

Consider:

import data.matrix.notation
import linear_algebra.matrix

example : (1 : matrix (fin 3) (fin 3) ℕ) = ![![1, 0, 0], ![0, 1, 0], ![0, 0, 1]] :=
begin
  ext i j,
  fin_cases i;
  fin_cases j;
  norm_num [matrix.one_apply],
end

Doesn't work on 7d240ce1, works on daac85454a. Does anyone know what changed precisely? As far as I can tell, lemma only got moved, not deleted.

[Eric Wieser]

(#10199)

[Yury G. Kudryashov]

Works:

import data.fin.vec_notation

example : ![![1, 0, 0], ![0, 1, 0], ![0, 0, 1]] 2 0 = 0 :=
by simp

Doesn't work:

import data.matrix.notation

example : ![![1, 0, 0], ![0, 1, 0], ![0, 0, 1]] 2 0 = 0 :=
by simp

[Yury G. Kudryashov]

With import data.matrix.notation, it applies matrix.cons_val', then gets stuck