Simp offset checking fails with non-canonical instances.

[joehendrix]

The logic for checking if a term is an offset seems to do a syntactic check that prevents simp rules from firing.

This appears to be a regression introduced by #3614. Prior to that, the example below succeeds, but after #3614 lean returns error: simp made no progress.

class AddCommMagma (G : Type u) extends Add G where
  /-- Addition is commutative in an commutative additive magma. -/
  protected add_comm : ∀ a b : G, a + b = b + a

instance : AddCommMagma Nat where
  add_comm := Nat.add_comm

example (n : Nat) (p : n = 3) : 1 + n = 1 + 3 := by
  rw [AddCommMagma.add_comm 1, AddCommMagma.add_comm 1]
  simp only [Nat.succ.injEq]
  exact p