chore(tactic/linarith): remove unneeded code (#16791)

Removes some unneeded lemmas (and consequently unneeded imports) in `tactic/linarith/lemmas.lean`, in preparation for porting.



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

Author: kim-em

src/algebra/order/ring.lean

@@ -1490,7 +1490,7 @@ end
 
 end mul_zero_class
 
-/-- `nontrivial α` is needed here as otherwise we have `1 * ⊤ = ⊤` but also `= 0 * ⊤ = 0`. -/
+/-- `nontrivial α` is needed here as otherwise we have `1 * ⊤ = ⊤` but also `0 * ⊤ = 0`. -/
 instance [mul_zero_one_class α] [nontrivial α] : mul_zero_one_class (with_top α) :=
 { mul := (*),
   one := 1,

src/data/int/basic.lean

@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jeremy Avigad
 -/
 import data.nat.pow
-import order.min_max
 import data.nat.cast
 import algebra.ring.regular
 

src/tactic/linarith/lemmas.lean

@@ -5,8 +5,6 @@ Authors: Robert Y. Lewis
 -/
 
 import algebra.order.ring
-import data.int.basic
-import tactic.norm_num
 
 /-!
 # Lemmas for `linarith`
@@ -17,33 +15,6 @@ If you find yourself looking for a theorem here, you might be in the wrong place
 
 namespace linarith
 
-lemma int.coe_nat_bit0 (n : ℕ) : (↑(bit0 n : ℕ) : ℤ) = bit0 (↑n : ℤ) := by simp [bit0]
-lemma int.coe_nat_bit1 (n : ℕ) : (↑(bit1 n : ℕ) : ℤ) = bit1 (↑n : ℤ) := by simp [bit1, bit0]
-lemma int.coe_nat_bit0_mul (n : ℕ) (x : ℕ) : (↑(bit0 n * x) : ℤ) = (↑(bit0 n) : ℤ) * (↑x : ℤ) :=
-by simp
-lemma int.coe_nat_bit1_mul (n : ℕ) (x : ℕ) : (↑(bit1 n * x) : ℤ) = (↑(bit1 n) : ℤ) * (↑x : ℤ) :=
-by simp
-lemma int.coe_nat_one_mul (x : ℕ) : (↑(1 * x) : ℤ) = 1 * (↑x : ℤ) := by simp
-lemma int.coe_nat_zero_mul (x : ℕ) : (↑(0 * x) : ℤ) = 0 * (↑x : ℤ) := by simp
-lemma int.coe_nat_mul_bit0 (n : ℕ) (x : ℕ) : (↑(x * bit0 n) : ℤ) = (↑x : ℤ) * (↑(bit0 n) : ℤ) :=
-by simp
-lemma int.coe_nat_mul_bit1 (n : ℕ) (x : ℕ) : (↑(x * bit1 n) : ℤ) = (↑x : ℤ) * (↑(bit1 n) : ℤ) :=
-by simp
-lemma int.coe_nat_mul_one (x : ℕ) : (↑(x * 1) : ℤ) = (↑x : ℤ) * 1 := by simp
-lemma int.coe_nat_mul_zero (x : ℕ) : (↑(x * 0) : ℤ) = (↑x : ℤ) * 0 := by simp
-
-lemma nat_eq_subst {n1 n2 : ℕ} {z1 z2 : ℤ} (hn : n1 = n2) (h1 : ↑n1 = z1) (h2 : ↑n2 = z2) :
-  z1 = z2 :=
-by simpa [eq.symm h1, eq.symm h2, int.coe_nat_eq_coe_nat_iff]
-
-lemma nat_le_subst {n1 n2 : ℕ} {z1 z2 : ℤ} (hn : n1 ≤ n2) (h1 : ↑n1 = z1) (h2 : ↑n2 = z2) :
-  z1 ≤ z2 :=
-by simpa [eq.symm h1, eq.symm h2, int.coe_nat_le]
-
-lemma nat_lt_subst {n1 n2 : ℕ} {z1 z2 : ℤ} (hn : n1 < n2) (h1 : ↑n1 = z1) (h2 : ↑n2 = z2) :
-  z1 < z2 :=
-by simpa [eq.symm h1, eq.symm h2, int.coe_nat_lt]
-
 lemma eq_of_eq_of_eq {α} [ordered_semiring α] {a b : α} (ha : a = 0) (hb : b = 0) : a + b = 0 :=
 by simp *
 
@@ -75,7 +46,6 @@ by simp *
 lemma eq_of_not_lt_of_not_gt {α} [linear_order α] (a b : α) (h1 : ¬ a < b) (h2 : ¬ b < a) : a = b :=
 le_antisymm (le_of_not_gt h2) (le_of_not_gt h1)
 
-
 -- used in the `nlinarith` normalization steps. The `_` argument is for uniformity.
 @[nolint unused_arguments]
 lemma mul_zero_eq {α} {R : α → α → Prop} [semiring α] {a b : α} (_ : R a 0) (h : b = 0) :