Shadowing in Lean 4

Stream: new members

[Martin C. Martin]

As an exercise, I'm redefining Complex. In Lean 3, import tactic didn't import Complex, but in Lean 4, import Mathlib.Tactic does. So I just put my new Complex in a namespace. However, notation "ℂ" => Complex doesn't seem to follow the same shadowing rules, as now when I try z : ℂ I get an error that ℂ is ambiguous. Here's an #mwe:

import Mathlib.Data.Real.Basic
import Mathlib.Tactic

namespace LADR

structure Complex : Type where
  re : ℝ
  im : ℝ

notation "ℂ" => Complex


namespace Complex

@[ext]
theorem ext : ∀ {z w : ℂ}, z.re = w.re → z.im = w.im → z = w
  | ⟨_, _⟩, ⟨_, _⟩, rfl, rfl => rfl

end Complex
end LADR

How can I hide or shadow the existing ℂ, or otherwise get ℂ to refer to my Complex class?

[Eric Wieser]

This seems to work:

notation (priority := 2000) "ℂ" => Complex

[Alex J. Best]

Not exactly answering your question but maybe you can just import Mathlib.Tactic.Common instead