fix: bug in reduceLeDiff simproc proof term

leanprover · May 5, 2024 · 02753f6 · 02753f6
1 parent dcccfb7
commit 02753f6
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 1 deletion.
diff --git a/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Nat.lean b/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Nat.lean
@@ -275,7 +275,7 @@ def reduceLTLE (nm : Name) (arity : Nat) (isLT : Bool) (e : Expr) : SimpM Step :
       applySimprocConst (mkConst ``True) ``Nat.Simproc.le_add_le #[x, yb, yo, leProof]
     else
       let finExpr := mkLENat (toExpr (xn - yn)) yb
-      let geProof ← mkOfDecideEqTrue (mkGENat yo x)
+      let geProof ← mkOfDecideEqTrue (mkGENat x yo)
       applySimprocConst finExpr ``Nat.Simproc.le_add_ge #[x, yb, yo, geProof]
   | .offset xb xo xn, .offset yb yo yn => do
     if xn ≤ yn then

diff --git a/tests/lean/run/simproc1.lean b/tests/lean/run/simproc1.lean
@@ -32,3 +32,5 @@ example : x + foo 2 = 12 + x := by
   -- We can use `-` to disable `simproc`s
   fail_if_success simp [-reduce_foo]
   simp_arith
+
+example (x : Nat) (h : x < 86) : ¬100 ≤ x + 14 := by simp; exact h