Theorem: Nat.add_eq_xor (Algdata/Data/Nat/Bits.lean)

State before:
m n : Nat
disjoint : m &&& n = 0
⊢ m + n = m ^^^ n
Tactic:
apply (Nat.eq_zero_or_pos m).elim
State after:
case left
m n : Nat
disjoint : m &&& n = 0
⊢ m = 0 → m + n = m ^^^ n

case right
m n : Nat
disjoint : m &&& n = 0
⊢ m > 0 → m + n = m ^^^ n

State before:
case left
m n : Nat
disjoint : m &&& n = 0
⊢ m = 0 → m + n = m ^^^ n

case right
m n : Nat
disjoint : m &&& n = 0
⊢ m > 0 → m + n = m ^^^ n
Tactic:
(intro hm; cases hm; simp)
State after:
case right
m n : Nat
disjoint : m &&& n = 0
⊢ m > 0 → m + n = m ^^^ n

State before:
case right
m n : Nat
disjoint : m &&& n = 0
⊢ m > 0 → m + n = m ^^^ n
Tactic:
intro hm
State after:
case right
m n : Nat
disjoint : m &&& n = 0
hm : m > 0
⊢ m + n = m ^^^ n

State before:
case right
m n : Nat
disjoint : m &&& n = 0
hm : m > 0
⊢ m + n = m ^^^ n
Tactic:
apply eq_of_div_mod_two_eq
State after:
case right.hdiv
m n : Nat
disjoint : m &&& n = 0
hm : m > 0
⊢ (m + n) / 2 = (m ^^^ n) / 2

case right.hmod
m n : Nat
disjoint : m &&& n = 0
hm : m > 0
⊢ (m + n) % 2 = (m ^^^ n) % 2

State before:
case right.hdiv
m n : Nat
disjoint : m &&& n = 0
hm : m > 0
⊢ (m + n) / 2 = (m ^^^ n) / 2

case right.hmod
m n : Nat
disjoint : m &&& n = 0
hm : m > 0
⊢ (m + n) % 2 = (m ^^^ n) % 2
Tactic:
. have : (m &&& n).getBit 0 = false := by simp [disjoint]
  conv => lhs; simp [add_div_two, this]; change (m >>> 1) + (n >>> 1)
  conv => rhs; change (m ^^^ n) >>> 1; rw [xor_shiftRight]
  have : m >>> 1 < m := Nat.div_lt_self hm (Nat.lt_succ_self 1)
  exact add_eq_xor (m:=m >>> 1) (n:=n >>> 1) (by rw [←land_shiftRight, disjoint]; rfl)
State after:
case right.hmod
m n : Nat
disjoint : m &&& n = 0
hm : m > 0
⊢ (m + n) % 2 = (m ^^^ n) % 2

State before:
case right.hmod
m n : Nat
disjoint : m &&& n = 0
hm : m > 0
⊢ (m + n) % 2 = (m ^^^ n) % 2
Tactic:
. exact eq_mod2_of_decide (add_getBit_zero m n)
State after:
no goals

State before:
case left
m n : Nat
disjoint : m &&& n = 0
⊢ m = 0 → m + n = m ^^^ n

case right
m n : Nat
disjoint : m &&& n = 0
⊢ m > 0 → m + n = m ^^^ n
Tactic:
intro hm
State after:
case left
m n : Nat
disjoint : m &&& n = 0
hm : m = 0
⊢ m + n = m ^^^ n

case right
m n : Nat
disjoint : m &&& n = 0
⊢ m > 0 → m + n = m ^^^ n

State before:
case left
m n : Nat
disjoint : m &&& n = 0
hm : m = 0
⊢ m + n = m ^^^ n

case right
m n : Nat
disjoint : m &&& n = 0
⊢ m > 0 → m + n = m ^^^ n
Tactic:
cases hm
State after:
case left.refl
n : Nat
disjoint : 0 &&& n = 0
⊢ 0 + n = 0 ^^^ n

case right
m n : Nat
disjoint : m &&& n = 0
⊢ m > 0 → m + n = m ^^^ n

State before:
case left.refl
n : Nat
disjoint : 0 &&& n = 0
⊢ 0 + n = 0 ^^^ n

case right
m n : Nat
disjoint : m &&& n = 0
⊢ m > 0 → m + n = m ^^^ n
Tactic:
simp
State after:
case right
m n : Nat
disjoint : m &&& n = 0
⊢ m > 0 → m + n = m ^^^ n

State before:
case right.hdiv
m n : Nat
disjoint : m &&& n = 0
hm : m > 0
⊢ (m + n) / 2 = (m ^^^ n) / 2
Tactic:
have : (m &&& n).getBit 0 = false := by simp [disjoint]
State after:
case right.hdiv
m n : Nat
disjoint : m &&& n = 0
hm : m > 0
this : getBit (m &&& n) 0 = false
⊢ (m + n) / 2 = (m ^^^ n) / 2

State before:
case right.hdiv
m n : Nat
disjoint : m &&& n = 0
hm : m > 0
this : getBit (m &&& n) 0 = false
⊢ (m + n) / 2 = (m ^^^ n) / 2
Tactic:
conv => lhs; simp [add_div_two, this]; change (m >>> 1) + (n >>> 1)
State after:
case right.hdiv
m n : Nat
disjoint : m &&& n = 0
hm : m > 0
this : getBit (m &&& n) 0 = false
⊢ m >>> 1 + n >>> 1 = (m ^^^ n) / 2

State before:
case right.hdiv
m n : Nat
disjoint : m &&& n = 0
hm : m > 0
this : getBit (m &&& n) 0 = false
⊢ m >>> 1 + n >>> 1 = (m ^^^ n) / 2
Tactic:
conv => rhs; change (m ^^^ n) >>> 1; rw [xor_shiftRight]
State after:
case right.hdiv
m n : Nat
disjoint : m &&& n = 0
hm : m > 0
this : getBit (m &&& n) 0 = false
⊢ m >>> 1 + n >>> 1 = m >>> 1 ^^^ n >>> 1

State before:
case right.hdiv
m n : Nat
disjoint : m &&& n = 0
hm : m > 0
this : getBit (m &&& n) 0 = false
⊢ m >>> 1 + n >>> 1 = m >>> 1 ^^^ n >>> 1
Tactic:
have : m >>> 1 < m := Nat.div_lt_self hm (Nat.lt_succ_self 1)
State after:
case right.hdiv
m n : Nat
disjoint : m &&& n = 0
hm : m > 0
this✝ : getBit (m &&& n) 0 = false
this : m >>> 1 < m
⊢ m >>> 1 + n >>> 1 = m >>> 1 ^^^ n >>> 1

State before:
case right.hdiv
m n : Nat
disjoint : m &&& n = 0
hm : m > 0
this✝ : getBit (m &&& n) 0 = false
this : m >>> 1 < m
⊢ m >>> 1 + n >>> 1 = m >>> 1 ^^^ n >>> 1
Tactic:
exact add_eq_xor (m:=m >>> 1) (n:=n >>> 1) (by rw [←land_shiftRight, disjoint]; rfl)
State after:
no goals

State before:
m n : Nat
disjoint : m &&& n = 0
hm : m > 0
⊢ getBit (m &&& n) 0 = false
Tactic:
simp [disjoint]
State after:
no goals

State before:
m n : Nat
disjoint : m &&& n = 0
hm : m > 0
this✝ : getBit (m &&& n) 0 = false
this : m >>> 1 < m
⊢ m >>> 1 &&& n >>> 1 = 0
Tactic:
rw [←land_shiftRight, disjoint]
State after:
m n : Nat
disjoint : m &&& n = 0
hm : m > 0
this✝ : getBit (m &&& n) 0 = false
this : m >>> 1 < m
⊢ 0 >>> 1 = 0

State before:
m n : Nat
disjoint : m &&& n = 0
hm : m > 0
this✝ : getBit (m &&& n) 0 = false
this : m >>> 1 < m
⊢ 0 >>> 1 = 0
Tactic:
rfl
State after:
no goals

State before:
case right.hmod
m n : Nat
disjoint : m &&& n = 0
hm : m > 0
⊢ (m + n) % 2 = (m ^^^ n) % 2
Tactic:
exact eq_mod2_of_decide (add_getBit_zero m n)
State after:
no goals