Activating Fin.CommRing instance

Stream: mathlib4

[thielema]

I have seen that Mathlib-4.21 got some changes to Fin.ofNat&Co. I understand the reasoning for the changes, and I was always worried about silent wrap-around in Fin. However, the change breaks a lot of proofs in my code. For instance:

lemma rev_zero_eq_minus_one [nezero : NeZero n]
  : Fin.rev 0 = (-1 : Fin n)
  := by
  have ⟨m,m_def⟩ := Nat.exists_eq_succ_of_ne_zero nezero.out
  subst m_def
  rw [Fin.rev_zero, ← Fin.neg_last, neg_neg]

lemma neg_eq_one_add_rev [nezero : NeZero n] (k : Fin n)
  : -k = 1+k.rev
  := open Fin.CommRing in by
  rw [add_comm, ← Fin.rev_sub, ← Fin.rev_eq_iff]
  rw [neg_eq_zero_sub, Fin.rev_sub, rev_zero_eq_minus_one]
  ring_nf

With Mathlib-4.20, ring_nf could complete the proof, but now it fails. I already added "open Fin.CommRing" as recommended in the Mathlib docs, but it does not help. I searched for Release Notes for Mathlib including a proposed migration but found only Release Notes for Lean4.21.

[Damiano Testa]

In the infoview, grind works in place of ring_nf (as does abel).

[Eric Wieser]

Works fine for me:

import Mathlib

open scoped Fin.CommRing

lemma rev_zero_eq_minus_one [nezero : NeZero n]
  : Fin.rev 0 = (-1 : Fin n)
  := by
  have ⟨m,m_def⟩ := Nat.exists_eq_succ_of_ne_zero nezero.out
  subst m_def
  rw [Fin.rev_zero, ← Fin.neg_last, neg_neg]

lemma neg_eq_one_add_rev [nezero : NeZero n] (k : Fin n)
  : -k = 1+k.rev
  := by
  rw [add_comm, ← Fin.rev_sub, ← Fin.rev_eq_iff]
  rw [neg_eq_zero_sub, Fin.rev_sub, rev_zero_eq_minus_one]
  ring_nf

[Eric Wieser]

open Fin.CommRing in ring_nf also works

[Eric Wieser]

It looks like open scoped Foo in by _ and by open scoped Foo in _ have different behaviors!

[thielema]

Both suggestions work here. Thanks a lot!