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

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

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