chore: upstream basic statements about inequalities (#3366)

src/Init/Core.lean

@@ -1932,6 +1932,18 @@ axiom ofReduceNat (a b : Nat) (h : reduceNat a = b) : a = b
 
 end Lean
 
+@[simp] theorem ge_iff_le [LE α] {x y : α} : x ≥ y ↔ y ≤ x := Iff.rfl
+
+@[simp] theorem gt_iff_lt [LT α] {x y : α} : x > y ↔ y < x := Iff.rfl
+
+theorem le_of_eq_of_le {a b c : α} [LE α] (h₁ : a = b) (h₂ : b ≤ c) : a ≤ c := h₁ ▸ h₂
+
+theorem le_of_le_of_eq {a b c : α} [LE α] (h₁ : a ≤ b) (h₂ : b = c) : a ≤ c := h₂ ▸ h₁
+
+theorem lt_of_eq_of_lt {a b c : α} [LT α] (h₁ : a = b) (h₂ : b < c) : a < c := h₁ ▸ h₂
+
+theorem lt_of_lt_of_eq {a b c : α} [LT α] (h₁ : a < b) (h₂ : b = c) : a < c := h₂ ▸ h₁
+
 namespace Std
 variable {α : Sort u}
 

tests/lean/letFun.lean.expected.out

@@ -5,15 +5,15 @@ f (y + x) : Nat
 a b : Nat
 h1 : a = 0
 h2 : b = 0
-⊢ (let_fun x := 1;
-    x + x) >
-    b
+⊢ b <
+    let_fun x := 1;
+    x + x
 (let_fun this := id;
   this)
   1 : Nat
 a b : Nat
 h : a > b
-⊢ a > b
+⊢ b < a
 let_fun n := 5;
 { val := [], property := (⋯ : 0 ≤ n) } : { as // List.length as ≤ 5 }
 rfl : (let_fun n := 5;

tests/lean/simp_trace.lean.expected.out

@@ -1,11 +1,13 @@
 Try this: simp only [f]
 [Meta.Tactic.simp.rewrite] unfold f, f (a :: b = []) ==> a :: b = []
 [Meta.Tactic.simp.rewrite] @eq_self:1000, False = False ==> True
-Try this: simp only [length]
+Try this: simp only [length, gt_iff_lt]
 [Meta.Tactic.simp.rewrite] unfold length, length (a :: b :: as) ==> length (b :: as) + 1
 [Meta.Tactic.simp.rewrite] unfold length, length (b :: as) ==> length as + 1
-Try this: simp only [fact]
+[Meta.Tactic.simp.rewrite] @gt_iff_lt:1000, length as + 1 + 1 > length as ==> length as < length as + 1 + 1
+Try this: simp only [fact, gt_iff_lt]
 [Meta.Tactic.simp.rewrite] unfold fact, fact (Nat.succ x) ==> (x + 1) * fact x
+[Meta.Tactic.simp.rewrite] @gt_iff_lt:1000, (x + 1) * fact x > 0 ==> 0 < (x + 1) * fact x
 Try this: simp only [head]
 [Meta.Tactic.simp.rewrite] unfold head, head (a :: as) ==> match a :: as with
     | [] => default

tests/lean/simp_trace_backtrack.lean

@@ -7,9 +7,6 @@ universe u
 theorem tsub_eq_zero_of_le {α : Type u} [LE α] [Sub α] [OfNat α 0] {a b : α} :
     a ≤ b → a - b = 0 := by sorry
 
-@[simp]
-theorem ge_iff_le (x y : Nat) : x ≥ y ↔ y ≤ x := Iff.rfl
-
 set_option tactic.simp.trace true
 
 -- This used to report: `Try this: simp only [ge_iff_le, Nat.succ_sub_succ_eq_sub]`

tests/lean/simp_trace_backtrack.lean.expected.out

@@ -1,3 +1,3 @@
 simp_trace_backtrack.lean:7:8-7:26: warning: declaration uses 'sorry'
 Try this: simp only [Nat.succ_sub_succ_eq_sub]
-simp_trace_backtrack.lean:17:0-17:7: warning: declaration uses 'sorry'
+simp_trace_backtrack.lean:14:0-14:7: warning: declaration uses 'sorry'