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

State before:
n k : Nat
⊢ n <<< k >>> k = n
Tactic:
induction k generalizing n
State after:
case zero
n : Nat
⊢ n <<< zero >>> zero = n

case succ
n✝ : Nat
n_ih✝ : ∀ (n : Nat), n <<< n✝ >>> n✝ = n
n : Nat
⊢ n <<< succ n✝ >>> succ n✝ = n

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

State before:
k : Nat
h_ind : ∀ (n : Nat), n <<< k >>> k = n
n : Nat
⊢ n <<< succ k >>> succ k = n
Tactic:
case succ k h_ind =>
  conv =>
    lhs; simp; change (n * (2^k*2)) >>> k / 2
    rw [Nat.mul_comm (2^k) 2, ←Nat.mul_assoc]
    rw [←Nat.shiftLeft_eq (n*2) k, h_ind (n*2), Nat.mul_div_cancel n (n:=2) (by decide)]
State after:
no goals

State before:
n : Nat
⊢ n <<< zero >>> zero = n
Tactic:
rfl
State after:
no goals

State before:
k : Nat
h_ind : ∀ (n : Nat), n <<< k >>> k = n
n : Nat
⊢ n <<< succ k >>> succ k = n
Tactic:
conv =>
  lhs; simp; change (n * (2^k*2)) >>> k / 2
  rw [Nat.mul_comm (2^k) 2, ←Nat.mul_assoc]
  rw [←Nat.shiftLeft_eq (n*2) k, h_ind (n*2), Nat.mul_div_cancel n (n:=2) (by decide)]
State after:
no goals

State before:
k : Nat
h_ind : ∀ (n : Nat), n <<< k >>> k = n
n : Nat
⊢ 0 < 2
Tactic:
decide
State after:
no goals