Vector.getElem_take range proof not resolved by unification

Prerequisites

Please put an X between the brackets as you perform the following steps:

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

In #6324 a lemma Vector.getElem_take was added (see here), but there is a small typo in the type of the range hypothesis: hi : i < min n m instead of hi : i < min m n.

As a result, rather than get_elem_tactic inserting hi via assumption, it inserts a non-trivial proof to commute min n m = min m n. Importantly, this means hi is not resolved via unification when simp tries to apply it, and therefore simp fails to apply in most cases.

Context

https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/Vector.20refactor/near/500330457

Steps to Reproduce

import Mathlib

example (k₁ k₂ : Vector α n) (h : j₁ < n) :
  (k₁.take n)[j₁] = (k₂.take n)[j₁] := by
  simp only [Vector.getElem_take] -- no progress
  sorry

@[simp] theorem getElem_take' (a : Vector α n) (m : Nat) (hi : i < min m n) :
    (a.take m)[i] = a[i] := by
  cases a; simp

example (k₁ k₂ : Vector α n) (h : j₁ < n) :
  (k₁.take n)[j₁] = (k₂.take n)[j₁] := by
  simp only [getElem_take'] -- progress
  sorry

Expected behavior: simp successfully rewrites with Vector.getElem_take

Actual behavior: simp fails with no progress

Versions

Lean 4.17.0-rc1 on live.lean-lang.org

Additional Information

[Additional information, configuration or data that might be necessary to reproduce the issue]

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

Open src/Init/Data/Vector/Lemmas.lean at Vector.getElem_take and compare its range hypothesis with the minimal reproduction in the issue. Run the reproduction, then verify that the corrected lemma lets simp rewrite the vector access without the replacement theorem; done means the expected simp step makes progress.