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

State before:
n k : Nat
⊢ n <<< succ k = 2 * n <<< k
Tactic:
simp
State after:
n k : Nat
⊢ n * 2 ^ succ k = 2 * (n * 2 ^ k)

State before:
n k : Nat
⊢ n * 2 ^ succ k = 2 * (n * 2 ^ k)
Tactic:
rw [←Nat.mul_assoc, Nat.mul_comm 2, Nat.mul_assoc, Nat.mul_comm 2]
State after:
n k : Nat
⊢ n * 2 ^ succ k = n * (2 ^ k * 2)

State before:
n k : Nat
⊢ n * 2 ^ succ k = n * (2 ^ k * 2)
Tactic:
rfl
State after:
no goals