Prerequisites

• Put an X between the brackets on this line if you have done all of the following:
  • Checked that your issue isn't already filed.
  • Reduced the issue to a self-contained, reproducible test case.

Description

simp_all will reorder hypotheses, even when it can't simplify.

Steps to Reproduce

example : ∀ {A : Prop} (_ : A) (_ : W), W := by
  intros
  rename_i w
  exact w       -- This works

example : ∀ {A : Prop} (_ : A) (_ : W), W := by
  intros
  simp_all
  rename_i w
  exact w     -- Fails, since `simp_all` reordered hypotheses, so we have `w : A`

Expected behaviour

simp_all should not reorder hypotheses unnecessarily.

Versions

Lean (version 4.0.0-nightly-2023-08-05, commit 254582c00040, Release)

Additional Information

This will be fixed incidentally as part of #2334, noting it here so I can link to it from tests.