patterns with coerced var

Stream: new members

[Ralf Stephan]

Can you please help? How to find out what is wrong?

import Mathlib

set_option autoImplicit false
open Finset PNat BigOperators Function

lemma prod_Icc_succ_div {n x : ℕ+} : ∀ n : ℕ+,
    (∏ x in Icc 1 n, ((1 + x) : ℝ) / (x : ℝ)) = n + 1 := by
  rw [prod_div_distrib (s := Icc 1 n)
    (f := fun x : ℕ+ ↦ ((1 + x) : ℝ))
    (g := fun x : ℕ+ ↦ (x : ℝ))]

tactic 'rewrite' failed, did not find instance of the pattern in the target expression
  ∏ x in Icc 1 n, (1 + ↑↑x) / ↑↑x
n x : ℕ+
⊢ ∀ (n : ℕ+), ∏ x in Icc 1 n, (1 + ↑↑x) / ↑↑x = ↑↑n + 1

The pattern seems identical, but it's not? Would it be possible to give information what doesn't match in the error message? This is so frustrating. Thanks for any hint.

[Ruben Van de Velde]

You're confusing yourself by having two ns

[Ralf Stephan]

But when I remove the second \N+ so that it reads ∀ n, I get

failed to synthesize instance
  LocallyFiniteOrder ℝ

[Ralf Stephan]

Ah, you mean competely without \forall. That works. Thanks!

[Ralf Stephan]

Can't different variables with same name be labelled on error output? Should I open an issue?