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

State before:
n k l : Nat
⊢ n <<< k <<< l = n <<< (k + l)
Tactic:
induction l
State after:
case zero
n k : Nat
⊢ n <<< k <<< zero = n <<< (k + zero)

case succ
n k n✝ : Nat
n_ih✝ : n <<< k <<< n✝ = n <<< (k + n✝)
⊢ n <<< k <<< succ n✝ = n <<< (k + succ n✝)

State before:
n k : Nat
⊢ n <<< k <<< zero = n <<< (k + zero)
Tactic:
case zero => rfl
State after:
no goals

State before:
n k l : Nat
h_ind : n <<< k <<< l = n <<< (k + l)
⊢ n <<< k <<< succ l = n <<< (k + succ l)
Tactic:
case succ l h_ind =>
  conv =>
    rw [add_succ, shiftLeft_succ, shiftLeft_succ, h_ind]
State after:
no goals

State before:
n k : Nat
⊢ n <<< k <<< zero = n <<< (k + zero)
Tactic:
rfl
State after:
no goals

State before:
n k l : Nat
h_ind : n <<< k <<< l = n <<< (k + l)
⊢ n <<< k <<< succ l = n <<< (k + succ l)
Tactic:
conv =>
  rw [add_succ, shiftLeft_succ, shiftLeft_succ, h_ind]
State after:
no goals