feat(data/nat/bitwise): tweak lxor lemmas (#15409)

This PR does the following:
- add `lxor_cancel_right`, `lxor_cancel_left`, `lt_lxor_cases`.
- make `lxor_right_inj` and `lxor_left_inj` into iffs as per convention, prove the corresponding `lxor_right_injective` and `lxor_left_injective` separately.
- golf `lxor_eq_zero`, tag it as `simp`, add the corresponding `lxor_ne_zero` lemma.
- simplify the hypothesis of `lxor_trichotomy`.

src/data/nat/bitwise.lean

@@ -167,17 +167,32 @@ lemma lor_assoc (n m k : ℕ) : lor (lor n m) k = lor n (lor m k) := by bitwise_
 @[simp] lemma lxor_self (n : ℕ) : lxor n n = 0 :=
 zero_of_test_bit_eq_ff $ λ i, by simp
 
-lemma lxor_right_inj {n m m' : ℕ} (h : lxor n m = lxor n m') : m = m' :=
-calc m = lxor n (lxor n m') : by simp [←lxor_assoc, ←h]
-   ... = m' : by simp [←lxor_assoc]
+-- These lemmas match `mul_inv_cancel_right` and `mul_inv_cancel_left`.
 
-lemma lxor_left_inj {n n' m : ℕ} (h : lxor n m = lxor n' m) : n = n' :=
-by { rw [lxor_comm n m, lxor_comm n' m] at h, exact lxor_right_inj h }
+lemma lxor_cancel_right (n m : ℕ) : lxor (lxor m n) n = m :=
+by rw [lxor_assoc, lxor_self, lxor_zero]
 
-lemma lxor_eq_zero {n m : ℕ} : lxor n m = 0 ↔ n = m :=
-⟨by { rw ←lxor_self m, exact lxor_left_inj }, by { rintro rfl, exact lxor_self _ }⟩
+lemma lxor_cancel_left (n m : ℕ) : lxor n (lxor n m) = m :=
+by rw [←lxor_assoc, lxor_self, zero_lxor]
 
-lemma lxor_trichotomy {a b c : ℕ} (h : lxor a (lxor b c) ≠ 0) :
+lemma lxor_right_injective {n : ℕ} : function.injective (lxor n) :=
+λ m m' h, by rw [←lxor_cancel_left n m, ←lxor_cancel_left n m', h]
+
+lemma lxor_left_injective {n : ℕ} : function.injective (λ m, lxor m n) :=
+λ m m' (h : lxor m n = lxor m' n), by rw [←lxor_cancel_right n m, ←lxor_cancel_right n m', h]
+
+@[simp] lemma lxor_right_inj {n m m' : ℕ} : lxor n m = lxor n m' ↔ m = m' :=
+lxor_right_injective.eq_iff
+
+@[simp] lemma lxor_left_inj {n m m' : ℕ} : lxor m n = lxor m' n ↔ m = m' :=
+lxor_left_injective.eq_iff
+
+@[simp] lemma lxor_eq_zero {n m : ℕ} : lxor n m = 0 ↔ n = m :=
+by rw [←lxor_self n, lxor_right_inj, eq_comm]
+
+lemma lxor_ne_zero {n m : ℕ} : lxor n m ≠ 0 ↔ n ≠ m := lxor_eq_zero.not
+
+lemma lxor_trichotomy {a b c : ℕ} (h : a ≠ lxor b c) :
   lxor b c < a ∨ lxor a c < b ∨ lxor a b < c :=
 begin
   set v := lxor a (lxor b c) with hv,
@@ -194,7 +209,7 @@ begin
 
   -- If `i` is the position of the most significant bit of `v`, then at least one of `a`, `b`, `c`
   -- has a one bit at position `i`.
-  obtain ⟨i, ⟨hi, hi'⟩⟩ := exists_most_significant_bit h,
+  obtain ⟨i, ⟨hi, hi'⟩⟩ := exists_most_significant_bit (lxor_ne_zero.2 h),
   have : test_bit a i = tt ∨ test_bit b i = tt ∨ test_bit c i = tt,
   { contrapose! hi,
     simp only [eq_ff_eq_not_eq_tt, ne, test_bit_lxor] at ⊢ hi,
@@ -207,4 +222,7 @@ begin
   exact lt_of_test_bit i (by simp [h, hi]) h (λ j hj, by simp [hi' _ hj])
 end
 
+lemma lt_lxor_cases {a b c : ℕ} (h : a < lxor b c) : lxor a c < b ∨ lxor a b < c :=
+(or_iff_right $ λ h', (h.asymm h').elim).1 $ lxor_trichotomy h.ne
+
 end nat

src/set_theory/game/nim.lean

@@ -302,7 +302,7 @@ begin
       intro h,
       rw ordinal.nat_cast_inj at h,
       try { rw [nat.lxor_comm n k, nat.lxor_comm n m] at h },
-      exact hk.ne (nat.lxor_left_inj h) } },
+      exact hk.ne (nat.lxor_left_injective h) } },
 
   have h₁ : ∀ (u : ordinal), u < nat.lxor n m →
     u ∈ set.range (λ i, grundy_value ((nim n + nim m).move_left i)),
@@ -315,10 +315,7 @@ begin
     rw set.mem_range,
 
     -- By a lemma about xor, either `u xor m < n` or `u xor n < m`.
-    have : nat.lxor u (nat.lxor n m) ≠ 0,
-    { intro h, rw nat.lxor_eq_zero at h, linarith },
-    rcases nat.lxor_trichotomy this with h|h|h,
-    { linarith },
+    cases nat.lt_lxor_cases hu with h h,
 
     -- Therefore, we can play the corresponding move, and by the inductive hypothesis the new state
     -- is `(u xor m) xor m = u` or `n xor (u xor n) = u` as required.