chore(data/nat/basic): add @[simp] to some lemmas about numerals (#6652)

Allows the simplifier to make more progress in equalities of numerals (both in nat, and in `[(semi)ring R] [no_zero_divisors R] [char_zero R]`). Also adds `@[simp]` to `nat.succ_ne_zero` and `nat.succ_ne_self`.



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: Mario Carneiro <di.gama@gmail.com>

Author: kim-em

src/algebra/char_zero.lean

@@ -108,10 +108,57 @@ end
 section
 variables {R : Type*} [semiring R] [no_zero_divisors R] [char_zero R]
 
+@[simp]
 lemma add_self_eq_zero {a : R} : a + a = 0 ↔ a = 0 :=
 by simp only [(two_mul a).symm, mul_eq_zero, two_ne_zero', false_or]
 
+@[simp]
 lemma bit0_eq_zero {a : R} : bit0 a = 0 ↔ a = 0 := add_self_eq_zero
+@[simp]
+lemma zero_eq_bit0 {a : R} : 0 = bit0 a ↔ a = 0 :=
+by { rw [eq_comm], exact bit0_eq_zero }
+end
+
+section
+variables {R : Type*} [ring R] [no_zero_divisors R] [char_zero R]
+
+lemma nat_mul_inj {n : ℕ} {a b : R} (h : (n : R) * a = (n : R) * b) : n = 0 ∨ a = b :=
+begin
+  rw [←sub_eq_zero, ←mul_sub, mul_eq_zero, sub_eq_zero] at h,
+  exact_mod_cast h,
+end
+
+lemma nat_mul_inj' {n : ℕ} {a b : R} (h : (n : R) * a = (n : R) * b) (w : n ≠ 0) : a = b :=
+by simpa [w] using nat_mul_inj h
+
+lemma bit0_injective : function.injective (bit0 : R → R) :=
+λ a b h, begin
+  dsimp [bit0] at h,
+  simp only [(two_mul a).symm, (two_mul b).symm] at h,
+  refine nat_mul_inj' _ two_ne_zero,
+  exact_mod_cast h,
+end
+
+lemma bit1_injective : function.injective (bit1 : R → R) :=
+λ a b h, begin
+  simp only [bit1, add_left_inj] at h,
+  exact bit0_injective h,
+end
+
+@[simp] lemma bit0_eq_bit0 {a b : R} : bit0 a = bit0 b ↔ a = b :=
+bit0_injective.eq_iff
+
+@[simp] lemma bit1_eq_bit1 {a b : R} : bit1 a = bit1 b ↔ a = b :=
+bit1_injective.eq_iff
+
+@[simp]
+lemma bit1_eq_one {a : R} : bit1 a = 1 ↔ a = 0 :=
+by rw [show (1 : R) = bit1 0, by simp, bit1_eq_bit1]
+
+@[simp]
+lemma one_eq_bit1 {a : R} : 1 = bit1 a ↔ a = 0 :=
+by { rw [eq_comm], exact bit1_eq_one }
+
 end
 
 section

src/analysis/normed_space/operator_norm.lean

@@ -126,7 +126,7 @@ begin
     { assume h,
       have : x₀ ∈ f.ker, by { rw h, exact (linear_map.ker f).zero_mem },
       exact x₀ker this },
-    have rx₀_ne_zero : r * ∥x₀∥ ≠ 0, by { simp [norm_eq_zero, this], norm_num },
+    have rx₀_ne_zero : r * ∥x₀∥ ≠ 0, by { simp [norm_eq_zero, this], },
     have : ∀x, ∥f x∥ ≤ (((r * ∥x₀∥)⁻¹) * ∥f x₀∥) * ∥x∥,
     { assume x,
       by_cases hx : f x = 0,

src/data/nat/basic.lean

@@ -115,7 +115,11 @@ instance nat.comm_cancel_monoid_with_zero : comm_cancel_monoid_with_zero ℕ :=
     λ _ _ _ h1 h2, nat.eq_of_mul_eq_mul_right (nat.pos_of_ne_zero h1) h2,
   .. (infer_instance : comm_monoid_with_zero ℕ) }
 
-attribute [simp] nat.not_lt_zero
+attribute [simp] nat.not_lt_zero nat.succ_ne_zero nat.succ_ne_self
+  nat.zero_ne_one nat.one_ne_zero
+  nat.zero_ne_bit1 nat.bit1_ne_zero
+  nat.bit0_ne_one nat.one_ne_bit0
+  nat.bit0_ne_bit1 nat.bit1_ne_bit0
 
 /-!
 Inject some simple facts into the type class system.
@@ -1434,6 +1438,23 @@ by unfold bodd div2; cases bodd_div2 n; refl
 
 /-! ### `bit0` and `bit1` -/
 
+-- There is no need to prove `bit0_eq_zero : bit0 n = 0 ↔ n = 0`
+-- as this is true for any `[semiring R] [no_zero_divisors R] [char_zero R]`
+
+-- However the lemmas `bit0_eq_bit0`, `bit1_eq_bit1`, `bit1_eq_one`, `one_eq_bit1`
+-- need `[ring R] [no_zero_divisors R] [char_zero R]` in general,
+-- so we prove `ℕ` specialized versions here.
+@[simp] lemma bit0_eq_bit0 {m n : ℕ} : bit0 m = bit0 n ↔ m = n :=
+⟨nat.bit0_inj, λ h, by subst h⟩
+
+@[simp] lemma bit1_eq_bit1 {m n : ℕ} : bit1 m = bit1 n ↔ m = n :=
+⟨nat.bit1_inj, λ h, by subst h⟩
+
+@[simp] lemma bit1_eq_one {n : ℕ} : bit1 n = 1 ↔ n = 0 :=
+⟨@nat.bit1_inj n 0, λ h, by subst h⟩
+@[simp] lemma one_eq_bit1 {n : ℕ} : 1 = bit1 n ↔ n = 0 :=
+⟨λ h, (@nat.bit1_inj 0 n h).symm, λ h, by subst h⟩
+
 protected theorem bit0_le {n m : ℕ} (h : n ≤ m) : bit0 n ≤ bit0 m :=
 add_le_add h h
 

src/data/sym2.lean

@@ -273,22 +273,22 @@ def sym2_equiv_sym' {α : Type*} : equiv (sym2 α) (sym' α 2) :=
     (by { rintros _ _ ⟨_⟩, { refl }, apply list.perm.swap', refl }),
   inv_fun := quotient.map from_vector (begin
     rintros ⟨x, hx⟩ ⟨y, hy⟩ h,
-    cases x with _ x, { simp at hx; tauto },
-    cases x with _ x, { simp at hx; norm_num at hx },
-    cases x with _ x, swap, { exfalso, simp at hx; linarith [hx] },
-    cases y with _ y, { simp at hy; tauto },
-    cases y with _ y, { simp at hy; norm_num at hy },
-    cases y with _ y, swap, { exfalso, simp at hy; linarith [hy] },
+    cases x with _ x, { simpa using hx, },
+    cases x with _ x, { simpa using hx, },
+    cases x with _ x, swap, { exfalso, simp at hx, linarith [hx] },
+    cases y with _ y, { simpa using hy, },
+    cases y with _ y, { simpa using hy, },
+    cases y with _ y, swap, { exfalso, simp at hy, linarith [hy] },
     rcases perm_card_two_iff.mp h with ⟨rfl,rfl⟩|⟨rfl,rfl⟩, { refl },
     apply sym2.rel.swap,
   end),
   left_inv := by tidy,
   right_inv := λ x, begin
     refine quotient.rec_on_subsingleton x (λ x, _),
     { cases x with x hx,
-      cases x with _ x, { simp at hx; tauto },
-      cases x with _ x, { simp at hx; norm_num at hx },
-      cases x with _ x, swap, { exfalso, simp at hx; linarith [hx] },
+      cases x with _ x, { simpa using hx, },
+      cases x with _ x, { simpa using hx, },
+      cases x with _ x, swap, { exfalso, simp at hx, linarith [hx] },
       refl },
   end }
 

src/ring_theory/polynomial/bernstein.lean

@@ -154,7 +154,7 @@ begin
     replace w := nat.lt_succ_iff.mp w,
     revert w,
     induction k with k ih generalizing n ν,
-    { simp [eval_at_0], rintro ⟨⟩, },
+    { simp [eval_at_0], },
     { simp only [derivative_succ, int.coe_nat_eq_zero, int.nat_cast_eq_coe_nat, mul_eq_zero,
         function.comp_app, function.iterate_succ,
         polynomial.iterate_derivative_sub, polynomial.iterate_derivative_cast_nat_mul,