chore: upstream (most of) Std.Data.Nat.Lemmas (#3391)

When updating Std, be careful that not every lemma has been upstreamed,
so we need to be careful to only delete things that have already been
declared.

src/Init/Data/Nat.lean

@@ -15,3 +15,4 @@ import Init.Data.Nat.Log2
 import Init.Data.Nat.Power2
 import Init.Data.Nat.Linear
 import Init.Data.Nat.SOM
+import Init.Data.Nat.Lemmas

tests/lean/matchMultAlt.lean

@@ -24,7 +24,7 @@ def h (x : Nat) : Nat :=
 example : h x > 0 := by
   match x with
   | 0 | 1 => decide
-  | x + 2 => simp [h, Nat.add_succ]; simp_arith
+  | x + 2 => simp [h, Nat.add_succ]
 
 inductive StrOrNum where
   | S (s : String)

tests/lean/run/1380.lean

@@ -1,5 +1,3 @@
-theorem Nat.lt_succ_iff {m n : Nat} : m < succ n ↔ m ≤ n := sorry
-
 variable (n v₁ v₂) (hv₁: v₁ < n + 1) (hv₂: v₂ < n + 1)
 theorem foo (_: ¬ Fin.mk v₂ hv₂ = Fin.mk v₁ hv₁ ): True := trivial
 set_option trace.Meta.Tactic.simp true in

tests/lean/run/ac_rfl.lean

@@ -42,10 +42,6 @@ theorem max_comm (n m : Nat) : max n m = max m n :=
 
 theorem max_idem (n : Nat) : max n n = n := le_ext (by simp)
 
-theorem Nat.zero_max (n : Nat) : max 0 n = n := by simp [Nat.max_def]
-
-theorem Nat.max_zero (n : Nat) : max n 0 = n := by rw [max_comm, Nat.zero_max]
-
 instance : Associative (α := Nat) max := ⟨max_assoc⟩
 instance : Commutative (α := Nat) max := ⟨max_comm⟩
 instance : IdempotentOp (α := Nat) max := ⟨max_idem⟩

tests/lean/run/concatElim.lean

@@ -43,7 +43,6 @@ theorem dropLastLen {α} (xs : List α) : (n : Nat) → xs.length = n+1 → (dro
     cases n with
     | zero   =>
       simp [lengthCons] at h
-      injection h
     | succ n =>
       have : (x₁ :: x₂ :: xs).length = xs.length + 2 := by simp [lengthCons]
       have : xs.length = n := by rw [this] at h; injection h with h; injection h

tests/lean/run/eqTheoremForVec.lean

@@ -2,8 +2,6 @@ inductive Vector (α : Type u): Nat → Type u where
 | nil : Vector α 0
 | cons (head : α) (tail : Vector α n) : Vector α (n+1)
 
-theorem Nat.lt_of_add_lt_add_right {a b c : Nat} (h : a + b < c + b) : a < c := sorry
-
 def Vector.nth : ∀{n}, Vector α n → Fin n → α
 | n+1, Vector.cons x xs, ⟨  0, _⟩ => x
 | n+1, Vector.cons x xs, ⟨k+1, h⟩ => xs.nth ⟨k, Nat.lt_of_add_lt_add_right h⟩

tests/lean/run/eqnsAtSimp.lean

@@ -3,15 +3,13 @@ mutual
     | 0 => true
     | n+1 => isOdd n
   decreasing_by
-    simp [measure, invImage, InvImage, Nat.lt_wfRel]
-    apply Nat.lt_succ_self
+    sorry
 
   def isOdd : Nat → Bool
     | 0 => false
     | n+1 => isEven n
   decreasing_by
-    simp [measure, invImage, InvImage, Nat.lt_wfRel]
-    apply Nat.lt_succ_self
+    sorry
 end
 
 theorem isEven_double (x : Nat) : isEven (2 * x) = true := by

tests/lean/run/simproc_panic.lean

@@ -1,12 +1,6 @@
 -- Extracted from Mathlib.Data.UnionFind.
 -- This file was failing in Mathlib during development of #3124.
 
-section Std.Data.Nat.Lemmas
-
-protected theorem Nat.lt_or_eq_of_le {n m : Nat} (h : n ≤ m) : n < m ∨ n = m := sorry
-
-end Std.Data.Nat.Lemmas
-
 section Mathlib.Data.UnionFind
 
 structure UFNode (α : Type _) where

tests/lean/run/splitIssue.lean

@@ -5,9 +5,6 @@ def splitList {α : Type _} : (l : List α) → ListSplit l
   | [] => ListSplit.split [] []
   | h :: t => ListSplit.split [h] t
 
-theorem Nat.lt_add_left {m n : Nat}  : m < n + m := sorry
-theorem Nat.lt_add_right {m n : Nat} : m < m + n := sorry
-
 def len : List α → Nat
   | [] => 0
   | a :: [] => 1
@@ -16,11 +13,7 @@ def len : List α → Nat
     | ListSplit.split fst snd => len fst + len snd
 termination_by l => l.length
 decreasing_by
-  all_goals
-  simp [measure, id, invImage, InvImage, Nat.lt_wfRel, WellFoundedRelation.rel, sizeOf] <;>
-  first
-    | apply Nat.lt_add_right
-    | apply Nat.lt_add_left
+  all_goals sorry
 
 theorem len_nil : len ([] : List α) = 0 := by
   simp [len]

tests/lean/run/wfEqns1.lean

@@ -10,15 +10,13 @@ mutual
     | 0 => true
     | n+1 => isOdd n
   decreasing_by
-    simp [measure, invImage, InvImage, Nat.lt_wfRel]
-    apply Nat.lt_succ_self
+    sorry
 
   def isOdd : Nat → Bool
     | 0 => false
     | n+1 => isEven n
   decreasing_by
-    simp [measure, invImage, InvImage, Nat.lt_wfRel]
-    apply Nat.lt_succ_self
+    sorry
 end
 
 #print isEven

tests/lean/simp_trace.lean

@@ -24,8 +24,6 @@ theorem ex3 : fact x > 0 := by
   | zero => decide
   | succ x ih =>
     simp [fact]
-    apply Nat.mul_pos
-    apply Nat.zero_lt_succ
     apply ih
 
 def head [Inhabited α] : List α → α

tests/lean/simp_trace.lean.expected.out

@@ -5,9 +5,11 @@ 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
 [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]
+Try this: simp only [fact, gt_iff_lt, Nat.zero_lt_succ, Nat.mul_pos_iff_of_pos_left]
 [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
+[Meta.Tactic.simp.rewrite] Nat.zero_lt_succ:1000, 0 < x + 1 ==> True
+[Meta.Tactic.simp.rewrite] @Nat.mul_pos_iff_of_pos_left:1000, 0 < (x + 1) * fact x ==> 0 < fact x
 Try this: simp only [head]
 [Meta.Tactic.simp.rewrite] unfold head, head (a :: as) ==> match a :: as with
     | [] => default
@@ -60,7 +62,7 @@ Try this: simp only [my_thm]
 [Meta.Tactic.simp.rewrite] @my_thm:1000, b ∧ b ==> b
 [Meta.Tactic.simp.rewrite] @eq_self:1000, (a ∧ b) = (a ∧ b) ==> True
 Try this: simp (discharger := sorry) only [Nat.sub_add_cancel]
-simp_trace.lean:85:0-85:7: warning: declaration uses 'sorry'
+simp_trace.lean:83:0-83:7: warning: declaration uses 'sorry'
 [Meta.Tactic.simp.rewrite] @Nat.sub_add_cancel:1000, x - 1 + 1 ==> x
 [Meta.Tactic.simp.rewrite] @eq_self:1000, x = x ==> True
 Try this: simp only [bla, h] at *
@@ -74,7 +76,7 @@ Try this: simp only [bla, h] at h'
     | Sum.inr val => 0
 [Meta.Tactic.simp.rewrite] unfold h, h x ==> Sum.inl (x, x)
 Try this: simp only [bla, h, List.length_append] at *
-simp_trace.lean:101:101-102:40: error: unsolved goals
+simp_trace.lean:99:101-100:40: error: unsolved goals
 x y : Nat
 α : Type
 xs ys : List α
@@ -87,7 +89,7 @@ h₂ : List.length xs + List.length ys = y
 [Meta.Tactic.simp.rewrite] unfold h, h x ==> Sum.inl (x, x)
 [Meta.Tactic.simp.rewrite] @List.length_append:1000, List.length (xs ++ ys) ==> List.length xs + List.length ys
 Try this: simp only [bla, h, List.length_append] at *
-simp_trace.lean:105:101-106:53: error: unsolved goals
+simp_trace.lean:103:101-104:53: error: unsolved goals
 x y : Nat
 α : Type
 xs ys : List α