From ff40b2c1a6da5c154363ef616ce098fbe18f1c7f Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Mon, 20 Jun 2022 09:15:55 +0000
Subject: [PATCH] chore(algebra/group/basic): lemmas about `bit0`, `bit1`, and
 addition (#14798)

---
 src/algebra/group/basic.lean | 22 ++++++++++++++++++++++
 src/data/nat/basic.lean      |  8 ++++++++
 2 files changed, 30 insertions(+)

diff --git a/src/algebra/group/basic.lean b/src/algebra/group/basic.lean
index 02851101b5d46..188264c85cf6e 100644
--- a/src/algebra/group/basic.lean
+++ b/src/algebra/group/basic.lean
@@ -116,6 +116,18 @@ by simp only [mul_left_comm, mul_comm]
 
 end comm_semigroup
 
+section add_comm_semigroup
+variables {M : Type u} [add_comm_semigroup M]
+
+lemma bit0_add (a b : M) : bit0 (a + b) = bit0 a + bit0 b :=
+add_add_add_comm _ _ _ _
+lemma bit1_add [has_one M] (a b : M) : bit1 (a + b) = bit0 a + bit1 b :=
+(congr_arg (+ (1 : M)) $ bit0_add a b : _).trans (add_assoc _ _ _)
+lemma bit1_add' [has_one M] (a b : M) : bit1 (a + b) = bit1 a + bit0 b :=
+by rw [add_comm, bit1_add, add_comm]
+
+end add_comm_semigroup
+
 local attribute [simp] mul_assoc sub_eq_add_neg
 
 section add_monoid
@@ -616,6 +628,16 @@ by rw [div_eq_iff_eq_mul, div_mul_eq_mul_div, div_eq_iff_eq_mul', mul_div_assoc]
 
 end comm_group
 
+section subtraction_comm_monoid
+variables {M : Type u} [subtraction_comm_monoid M]
+
+lemma bit0_sub (a b : M) : bit0 (a - b) = bit0 a - bit0 b :=
+sub_add_sub_comm _ _ _ _
+lemma bit1_sub [has_one M] (a b : M) : bit1 (a - b) = bit1 a - bit0 b :=
+(congr_arg (+ (1 : M)) $ bit0_sub a b : _).trans $ sub_add_eq_add_sub _ _ _
+
+end subtraction_comm_monoid
+
 section commutator
 
 /-- The commutator of two elements `g₁` and `g₂`. -/
diff --git a/src/data/nat/basic.lean b/src/data/nat/basic.lean
index cea19850364f7..ad0f43ba70096 100644
--- a/src/data/nat/basic.lean
+++ b/src/data/nat/basic.lean
@@ -1489,6 +1489,14 @@ by unfold bodd div2; cases bodd_div2 n; refl
 @[simp] lemma one_eq_bit1 {n : ℕ} : 1 = bit1 n ↔ n = 0 :=
 ⟨λ h, (@nat.bit1_inj 0 n h).symm, λ h, by subst h⟩
 
+theorem bit_add : ∀ (b : bool) (n m : ℕ), bit b (n + m) = bit ff n + bit b m
+| tt := bit1_add
+| ff := bit0_add
+
+theorem bit_add' : ∀ (b : bool) (n m : ℕ), bit b (n + m) = bit b n + bit ff m
+| tt := bit1_add'
+| ff := bit0_add
+
 protected theorem bit0_le {n m : ℕ} (h : n ≤ m) : bit0 n ≤ bit0 m :=
 add_le_add h h