rw does not work, but exact does

Stream: new members

[Bolton Bailey]

I recently encountered this problem while updating my mathlib dependency. How do I rewrite this h term?

import Mathlib

example (x : ℕ ) (h: ¬ x = 0) : 1 ≤ x := by
  -- exact Nat.one_le_iff_ne_zero.mpr h -- Works
  -- rw [← Ne.def] at h invalid field notation
  rw [← Nat.one_le_iff_ne_zero] at h -- Did not find ≠ 0

[Rida Hamadani]

have you tried rewriting ne_eq at h first?

[Bolton Bailey]

That solves it, thank you!

[Bolton Bailey]

Is Ne.def just deprecated then? Shouldn't there be a deprecation notice if so?

[Rida Hamadani]

@loogle "Ne.def"

[loogle]

:shrug: nothing found

[Rida Hamadani]

I think you can rewrite Ne instead

[Ruben Van de Velde]

Ne.def also works, probably

[Richard Copley]

Ruben Van de Velde said:

Ne.def also works, probably

It used to! But not any longer. It was removed from Mathlib.Logic and callers changed to Ne.eq_def in "chore: move to v4.8.0-rc1 (#12548)". Ne.eq_def is maybe autogenerated (an "unfolding lemma"?), I guess, because I can't seem to find its definition.

[Ruben Van de Velde]

Oh, I suppressed that memory. Thanks for the correction