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

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

State before:
k : ℕ
⊢ x (2 * 2 * k + 2) = x k
Tactic:
rw [mul_assoc, ← mul_add_one, x_mul2, x_mul2_add1,
  ← Nat.bit1_val, Nat.bodd_bit1, Bool.true_xor, Bool.not_not]
State after:
no goals