Theorem: IMOSL.IMO2010A4.x_mul4 (IMOSLLean4/IMO2010/A4/A4.lean)

State before:
k : ℕ
⊢ x (4 * k) = xor k.bodd (x k)
Tactic:
change x (2 * 2 * k) = xor k.bodd (x k)
State after:
k : ℕ
⊢ x (2 * 2 * k) = xor k.bodd (x k)

State before:
k : ℕ
⊢ x (2 * 2 * k) = xor k.bodd (x k)
Tactic:
rw [mul_assoc, x_mul2, x_mul2, ← Nat.bit0_val, Nat.bodd_bit0, Bool.false_xor]
State after:
no goals