ring tactic error

Stream: new members

[Yakov Pechersky]

What's going on here? Shouldn't ring just no-op here and not break? It used to work:

import data.matrix.notation

open_locale big_operators

-- this used to work
example {R : Type*} [field R] : ∀ f : fin 2 → R, ∑ x : fin 2, f x = f 0 + f 1 :=
begin
  intro f,
  calc
  ∑ x : fin 2, f x = _ + _ : rfl
  ...              = f 0 + f 1 : by { simp, ring, refl }
end

-- this works now
example {R : Type*} [field R] : ∀ f : fin 2 → R, ∑ x : fin 2, f x = f 0 + f 1 :=
begin
  intro f,
  calc
  ∑ x : fin 2, f x = _ + _ : rfl
  ...              = f 0 + f 1 : by { simpa }
end

[Yakov Pechersky]

Specifically, I had code at https://github.com/pechersky/e222/blob/fa698275f1b4dc98a502866b5dfe2eb341ac8e79/src/test2.lean#L74, using mathlib commit 490a09b04288034ab4e12a5456ee09698bdff797 but I cannot locate that commit now...

[Rob Lewis]

You need import tactic.ring

[Rob Lewis]

There were prs recently refining the import hierarchy, it's probably not imported by data.matrix.notation anymore.