priority of theorems

Stream: lean4

[Jon Eugster]

Consider the example below. Is there a way to give the theorem MyNat.add_comm higher priority than _root_.add_comm to avoid the error ambiguous, possible interpretations? In other cases, like notations, there is the (priority := 1000000) syntax, but I'm not aware of a similar thing for theorems.

import Mathlib

#check add_comm

variable (U :Type) [Add U]

theorem MyNat.add_comm (a b : U) : a + b = b + a := sorry

open MyNat

example (a b c : ℕ) : a + b + c = c + a + b := by
  rw [add_comm] -- ERROR:
  -- ambiguous, possible interpretations
  -- _root_.add_comm : ∀ (a b : ?m.216), a + b = b + a

  -- MyNat.add_comm : ∀ (U : Type) [inst : Add U] (a b : U), a + b = b + a
  simp