ambiguous rewrite when only one is valid

Stream: mathlib4

[Bhavik Mehta]

My understanding was that Lean 4 was smart enough to distinguish which lemma to use in an ambiguous situation when only one is valid. But it doesn't seem to work in this case:

import Mathlib.Data.Real.Basic

open Nat

local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y)

example (n : ℕ) : (4 : ℝ) ^ n ≤ 4 * (4 : ℝ) ^ (n + 1) := by
  rw [pow_succ]

example (n : ℕ) : (4 : ℝ) ^ n ≤ (4 : ℝ) ^ (n + 1) := by
  rw [Nat.pow_succ]

example (n : ℕ) : (4 : ℝ) ^ n ≤ 4 * (4 : ℝ) ^ (n + 1) := by
  rw [_root_.pow_succ]

Lean 3 is able to disambiguate in this case.

[Kyle Miller]

Here's a MWE

theorem Foo.add_succ : true = true := rfl

open Nat Foo

#check add_succ -- Nat.add_succ
#check (add_succ : true = true) -- Foo.add_succ

example (x y : Nat) : x + (y + 1) = (x + y) + 1 := by
  rw [add_succ]
  /-
  ambiguous, possible interpretations
  Foo.add_succ : true = true

  Nat.add_succ : ∀ (n m : Nat), n + succ m = succ (n + m)
  -/

[Kyle Miller]

I thought the #check would show an ambiguity error, so that's a bit interesting that it doesn't.

[Bhavik Mehta]

This doesn't even need Foo:

theorem add_succ : true = true := rfl

open Nat

#check add_succ -- Nat.add_succ
#check (add_succ : true = true) -- _root_.add_succ

example (x y : Nat) : x + (y + 1) = (x + y) + 1 := by
  rw [add_succ]

[Bhavik Mehta]

Reported: https://github.com/leanprover/lean4/issues/2849