How to sharpen an off-by-one

Stream: mathlib4

[Scott Carnahan]

In PR #7333, I changed the following theorem:

theorem eventually_constant_prod {u : ℕ → β} {N : ℕ} (hu : ∀ n ≥ N, u n = 1) {n : ℕ} (hn : N ≤ n) :
    (∏ k in range (n + 1), u k) = ∏ k in range (N + 1), u k

to

theorem eventually_constant_prod {u : ℕ → β} {N : ℕ} (hu : ∀ n ≥ N, u n = 1) {n : ℕ} (hn : N ≤ n) :
    (∏ k in range n, u k) = ∏ k in range N, u k

That is, I removed the superfluous +1s in the conclusion. However, I am having second thoughts about this, because range (n+1) appears naturally a lot, and I could have instead weakened the hypothesis hu : ∀ n ≥ N, u n = 1 to hu : ∀ n > N, u n = 1.
Do people have a preference for how this sharpening should be done?

[Yaël Dillies]

I think your current change is better because it's syntactically more general.

[Scott Carnahan]

Thank you for thinking about this! I'll start the merge.