`cases` can reorder equally named hypotheses

example (P : Nat → Prop) (a) (h : ∃ n, a = n + 1 ∧ P n) : ∃ n, P n := by
  let ⟨n', e, h⟩ := h
  cases e
  exact ⟨_, h⟩
  -- application type mismatch
  --   Exists.intro ?m.12045 h
  -- argument
  --   h
  -- has type
  --   ∃ n, n' + 1 = n + 1 ∧ P n : Prop
  -- but is expected to have type
  --   P ?m.12045 : Prop

Before the cases, the state is:

P: Nat → Prop
a: Nat
: ∃ n, a = n + 1 ∧ P n
n': Nat
e: a = n' + 1
h: P n'
⊢ ∃ n, P n

The first h: ∃ n, a = n + 1 ∧ P n argument (name elided in the display) is being shadowed by the h: P n' argument. After cases, the state is:

case refl
P: Nat → Prop
n': Nat
: P n'
h: ∃ n, n' + 1 = n + 1 ∧ P n
⊢ ∃ n, P n

Because h: P n' did not need to be rewritten but h: ∃ n, a = n + 1 ∧ P n did, h: ∃ n, a = n + 1 ∧ P n got moved to the end of the hypothesis list, meaning that now h refers to h: ∃ n, a = n + 1 ∧ P n instead of h: P n' and the exact fails.

Start with the minimal Lean example in the issue and inspect the cases tactic's hypothesis reordering and name handling. The fix is complete when equally named hypotheses retain the intended bindings after cases and the shown exact ⟨_, h⟩ succeeds.