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

State before:
k : ℕ
h : S (4 * k) = 2 * S k
⊢ S (4 * k.succ) = 2 * S k.succ
Tactic:
change S (4 * k + 4) = 2 * S k.succ
State after:
k : ℕ
h : S (4 * k) = 2 * S k
⊢ S (4 * k + 4) = 2 * S k.succ

State before:
k : ℕ
h : S (4 * k) = 2 * S k
⊢ S (4 * k + 4) = 2 * S k.succ
Tactic:
rw [S_succ, x_mul4_add3, S_succ, x_mul4_add2, S_mul4_add2,
  h, add_assoc, ← two_mul, ← mul_add, ← S_succ]
State after:
no goals