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

State before:
m n : Nat
incl : m &&& n = n
⊢ m - n = m ^^^ n
Tactic:
apply Nat.sub_eq_of_eq_add
State after:
case h
m n : Nat
incl : m &&& n = n
⊢ m = (m ^^^ n) + n

State before:
case h
m n : Nat
incl : m &&& n = n
⊢ m = (m ^^^ n) + n
Tactic:
have := calc
  (m ^^^ n) &&& n
    = (m &&& n) ^^^ (n &&& n) := Nat.xor_and m n n
  _ = n ^^^ n := by rw [incl, Nat.land_self n]
  _ = 0 := Nat.xor_self n
State after:
case h
m n : Nat
incl : m &&& n = n
this : (m ^^^ n) &&& n = 0
⊢ m = (m ^^^ n) + n

State before:
case h
m n : Nat
incl : m &&& n = n
this : (m ^^^ n) &&& n = 0
⊢ m = (m ^^^ n) + n
Tactic:
simp [add_eq_xor this, Nat.xor_assoc]
State after:
no goals

State before:
m n : Nat
incl : m &&& n = n
⊢ m &&& n ^^^ n &&& n = n ^^^ n
Tactic:
rw [incl, Nat.land_self n]
State after:
no goals