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

State before:
l m n : Nat
⊢ (l ^^^ m) &&& n = l &&& n ^^^ m &&& n
Tactic:
apply bitext
State after:
case a
l m n : Nat
⊢ ∀ (i : Nat), getBit ((l ^^^ m) &&& n) i = getBit (l &&& n ^^^ m &&& n) i

State before:
case a
l m n : Nat
⊢ ∀ (i : Nat), getBit ((l ^^^ m) &&& n) i = getBit (l &&& n ^^^ m &&& n) i
Tactic:
intro i
State after:
case a
l m n i : Nat
⊢ getBit ((l ^^^ m) &&& n) i = getBit (l &&& n ^^^ m &&& n) i

State before:
case a
l m n i : Nat
⊢ getBit ((l ^^^ m) &&& n) i = getBit (l &&& n ^^^ m &&& n) i
Tactic:
conv => lhs; change (bitwise and (bitwise bne l m) n).getBit i
State after:
case a
l m n i : Nat
⊢ getBit (bitwise and (bitwise bne l m) n) i = getBit (l &&& n ^^^ m &&& n) i

State before:
case a
l m n i : Nat
⊢ getBit (bitwise and (bitwise bne l m) n) i = getBit (l &&& n ^^^ m &&& n) i
Tactic:
conv => rhs; change (bitwise bne (bitwise and l n) (bitwise and m n)).getBit i
State after:
case a
l m n i : Nat
⊢ getBit (bitwise and (bitwise bne l m) n) i = getBit (bitwise bne (bitwise and l n) (bitwise and m n)) i

State before:
case a
l m n i : Nat
⊢ getBit (bitwise and (bitwise bne l m) n) i = getBit (bitwise bne (bitwise and l n) (bitwise and m n)) i
Tactic:
simp [bitwise_getBit]
State after:
case a
l m n i : Nat
⊢ (getBit l i != getBit m i && getBit n i) = ((getBit l i && getBit n i) != (getBit m i && getBit n i))

State before:
case a
l m n i : Nat
⊢ (getBit l i != getBit m i && getBit n i) = ((getBit l i && getBit n i) != (getBit m i && getBit n i))
Tactic:
cases l.getBit i <;> cases m.getBit i <;> cases n.getBit i <;> decide
State after:
no goals