grind proof breaks when importing mathlib

Stream: mathlib4

[Bhavik Mehta]

This proof works with no imports, but breaks if I import a low-level file in mathlib, but if I disable the instances Int.instMonoid Int.instCommMonoid, then it works again

import Mathlib.Algebra.Group.Int.Defs

theorem square_mod_eight_eq (n : Nat) :
    n ^ 2 % 8 = 0 ∨ n ^ 2 % 8 = 1 ∨ n ^ 2 % 8 = 4 := by
  sorry

theorem test1 {n : Nat} (hn : n % 8 = 7) (a b c : Nat)
    (hl' : a ^ 2 + b ^ 2 + c ^ 2 = n) :
    False := by
  grind [square_mod_eight_eq] -- fails

attribute [-instance] Int.instMonoid Int.instCommMonoid in
theorem test2 {n : Nat} (hn : n % 8 = 7) (a b c : Nat)
    (hl' : a ^ 2 + b ^ 2 + c ^ 2 = n) :
    False := by
  grind [square_mod_eight_eq] -- works

importing more of mathlib makes it break again (and I haven't yet figured out which instances are the problem).

Note that the same thing happens with grind only [square_mod_eight_eq, cases Or], so it's not related to new grind tags in mathlib

[Bhavik Mehta]

One choice of incantation to make grind work with mathlib again is:

attribute [-instance] Lean.Grind.instCommRingInt
attribute [-instance] Int.instCommRing
attribute [-instance] Int.euclideanDomain
attribute [-instance] Int.instNormedCommRing
attribute [-instance] Int.instCommSemiring

But surely there's a better solution here!

[Kim Morrison]

Here's the Mathlib-free minimization:

theorem square_mod_eight_eq (n : Nat) :
    n ^ 2 % 8 = 0 ∨ n ^ 2 % 8 = 1 ∨ n ^ 2 % 8 = 4 := by
  sorry

theorem test0 {n : Nat} (hn : n % 8 = 7) (a b c : Nat)
    (hl' : a ^ 2 + b ^ 2 + c ^ 2 = n) :
    False := by
  grind [square_mod_eight_eq] -- works

class Monoid (M : Type u) extends Mul M, One M where
  protected npow : Nat → M → M

instance Monoid.toNatPow {M : Type u} [Monoid M] : Pow M Nat :=
  ⟨fun x n ↦ Monoid.npow n x⟩

instance Int.instCommMonoid : Monoid Int where
  npow n x := x ^ n

theorem test1 {n : Nat} (hn : n % 8 = 7) (a b c : Nat)
    (hl' : a ^ 2 + b ^ 2 + c ^ 2 = n) :
    False := by
  grind [square_mod_eight_eq] -- fails!

attribute [-instance] Lean.Grind.instCommRingInt in

theorem test2 {n : Nat} (hn : n % 8 = 7) (a b c : Nat)
    (hl' : a ^ 2 + b ^ 2 + c ^ 2 = n) :
    False := by
  grind [square_mod_eight_eq] -- works

We're taking a look.

[Bhavik Mehta]

Thank you!