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

State before:
⊢ ∀ (n k : Nat), Nat.lsb n <<< k = Nat.lsb (n <<< k)
Tactic:
suffices ∀ n, 2*n.lsb = (2*n).lsb by
  intro n k
  induction k generalizing n
  case zero => rfl
  case succ k h_ind =>
    simp only [Nat.succ_eq_add_one, ←Nat.shiftLeft_shiftLeft, h_ind]
    conv => change 2*(n <<< k).lsb = (2* (n <<< k)).lsb
    rw [this]
State after:
⊢ ∀ (n : Nat), 2 * Nat.lsb n = Nat.lsb (2 * n)

State before:
⊢ ∀ (n : Nat), 2 * Nat.lsb n = Nat.lsb (2 * n)
Tactic:
intro n
State after:
n : Nat
⊢ 2 * Nat.lsb n = Nat.lsb (2 * n)

State before:
n : Nat
⊢ 2 * Nat.lsb n = Nat.lsb (2 * n)
Tactic:
cases n
State after:
case zero

⊢ 2 * Nat.lsb zero = Nat.lsb (2 * zero)

case succ
n✝ : Nat
⊢ 2 * Nat.lsb (succ n✝) = Nat.lsb (2 * succ n✝)

State before:
⊢ 2 * Nat.lsb zero = Nat.lsb (2 * zero)
Tactic:
case zero => rfl
State after:
no goals

State before:
n : Nat
⊢ 2 * Nat.lsb (succ n) = Nat.lsb (2 * succ n)
Tactic:
case succ n =>
  unfold Nat.lsb
  have : 2 * n.succ - 1 = 2 * (n.succ - 1) + 1 := by
    simp only [Nat.mul_succ, Nat.succ_sub_one]
  have : ∀ (k l : Nat), (2*k) &&& (2*l + 1) = 2*k &&& 2*l := by
    intro k l
    have : ∀ m, 2*m &&& 1 = 0 := by intros; rw [Nat.land_one, Nat.mul_mod_right]
    have : 2*l + 1 = 2*l ^^^ 1 := Nat.add_eq_xor (this l)
    calc
      2*k &&& (2*l + 1)
        = 2*k &&& (2*l ^^^ 1) := by rw [‹2*l + 1 = 2*l ^^^ 1›]
      _ = (2*k &&& 2*l) ^^^ (2*k &&& 1) := Nat.and_xor ..
      _ = (2*k &&& 2*l) ^^^ 0 := by rw [‹∀ m, 2*m &&& 1 = 0›]
      _ = 2*k &&& 2 * l:= by rw [Nat.xor_zero]
  rw [‹2*n.succ - 1 = 2 * (n.succ - 1) + 1›, this]
  conv =>
    rhs; simp only [←Nat.shiftLeft_one]
    simp only [←Nat.land_shiftLeft, ←Nat.xor_shiftLeft]
State after:
no goals

State before:
this : ∀ (n : Nat), 2 * Nat.lsb n = Nat.lsb (2 * n)
⊢ ∀ (n k : Nat), Nat.lsb n <<< k = Nat.lsb (n <<< k)
Tactic:
intro n k
State after:
this : ∀ (n : Nat), 2 * Nat.lsb n = Nat.lsb (2 * n)
n k : Nat
⊢ Nat.lsb n <<< k = Nat.lsb (n <<< k)

State before:
this : ∀ (n : Nat), 2 * Nat.lsb n = Nat.lsb (2 * n)
n k : Nat
⊢ Nat.lsb n <<< k = Nat.lsb (n <<< k)
Tactic:
induction k generalizing n
State after:
case zero
this : ∀ (n : Nat), 2 * Nat.lsb n = Nat.lsb (2 * n)
n : Nat
⊢ Nat.lsb n <<< zero = Nat.lsb (n <<< zero)

case succ
this : ∀ (n : Nat), 2 * Nat.lsb n = Nat.lsb (2 * n)
n✝ : Nat
n_ih✝ : ∀ (n : Nat), Nat.lsb n <<< n✝ = Nat.lsb (n <<< n✝)
n : Nat
⊢ Nat.lsb n <<< succ n✝ = Nat.lsb (n <<< succ n✝)

State before:
this : ∀ (n : Nat), 2 * Nat.lsb n = Nat.lsb (2 * n)
n : Nat
⊢ Nat.lsb n <<< zero = Nat.lsb (n <<< zero)
Tactic:
case zero => rfl
State after:
no goals

State before:
this : ∀ (n : Nat), 2 * Nat.lsb n = Nat.lsb (2 * n)
k : Nat
h_ind : ∀ (n : Nat), Nat.lsb n <<< k = Nat.lsb (n <<< k)
n : Nat
⊢ Nat.lsb n <<< succ k = Nat.lsb (n <<< succ k)
Tactic:
case succ k h_ind =>
  simp only [Nat.succ_eq_add_one, ←Nat.shiftLeft_shiftLeft, h_ind]
  conv => change 2*(n <<< k).lsb = (2* (n <<< k)).lsb
  rw [this]
State after:
no goals

State before:
this : ∀ (n : Nat), 2 * Nat.lsb n = Nat.lsb (2 * n)
n : Nat
⊢ Nat.lsb n <<< zero = Nat.lsb (n <<< zero)
Tactic:
rfl
State after:
no goals

State before:
this : ∀ (n : Nat), 2 * Nat.lsb n = Nat.lsb (2 * n)
k : Nat
h_ind : ∀ (n : Nat), Nat.lsb n <<< k = Nat.lsb (n <<< k)
n : Nat
⊢ Nat.lsb n <<< succ k = Nat.lsb (n <<< succ k)
Tactic:
simp only [Nat.succ_eq_add_one, ←Nat.shiftLeft_shiftLeft, h_ind]
State after:
this : ∀ (n : Nat), 2 * Nat.lsb n = Nat.lsb (2 * n)
k : Nat
h_ind : ∀ (n : Nat), Nat.lsb n <<< k = Nat.lsb (n <<< k)
n : Nat
⊢ Nat.lsb (n <<< k) <<< 1 = Nat.lsb (n <<< k <<< 1)

State before:
this : ∀ (n : Nat), 2 * Nat.lsb n = Nat.lsb (2 * n)
k : Nat
h_ind : ∀ (n : Nat), Nat.lsb n <<< k = Nat.lsb (n <<< k)
n : Nat
⊢ Nat.lsb (n <<< k) <<< 1 = Nat.lsb (n <<< k <<< 1)
Tactic:
conv => change 2*(n <<< k).lsb = (2* (n <<< k)).lsb
State after:
this : ∀ (n : Nat), 2 * Nat.lsb n = Nat.lsb (2 * n)
k : Nat
h_ind : ∀ (n : Nat), Nat.lsb n <<< k = Nat.lsb (n <<< k)
n : Nat
⊢ 2 * Nat.lsb (n <<< k) = Nat.lsb (2 * n <<< k)

State before:
this : ∀ (n : Nat), 2 * Nat.lsb n = Nat.lsb (2 * n)
k : Nat
h_ind : ∀ (n : Nat), Nat.lsb n <<< k = Nat.lsb (n <<< k)
n : Nat
⊢ 2 * Nat.lsb (n <<< k) = Nat.lsb (2 * n <<< k)
Tactic:
rw [this]
State after:
no goals

State before:
⊢ 2 * Nat.lsb zero = Nat.lsb (2 * zero)
Tactic:
rfl
State after:
no goals

State before:
n : Nat
⊢ 2 * Nat.lsb (succ n) = Nat.lsb (2 * succ n)
Tactic:
unfold Nat.lsb
State after:
n : Nat
⊢ 2 * (succ n ^^^ succ n &&& succ n - 1) = 2 * succ n ^^^ 2 * succ n &&& 2 * succ n - 1

State before:
n : Nat
⊢ 2 * (succ n ^^^ succ n &&& succ n - 1) = 2 * succ n ^^^ 2 * succ n &&& 2 * succ n - 1
Tactic:
have : 2 * n.succ - 1 = 2 * (n.succ - 1) + 1 := by
  simp only [Nat.mul_succ, Nat.succ_sub_one]
State after:
n : Nat
this : 2 * succ n - 1 = 2 * (succ n - 1) + 1
⊢ 2 * (succ n ^^^ succ n &&& succ n - 1) = 2 * succ n ^^^ 2 * succ n &&& 2 * succ n - 1

State before:
n : Nat
this : 2 * succ n - 1 = 2 * (succ n - 1) + 1
⊢ 2 * (succ n ^^^ succ n &&& succ n - 1) = 2 * succ n ^^^ 2 * succ n &&& 2 * succ n - 1
Tactic:
have : ∀ (k l : Nat), (2*k) &&& (2*l + 1) = 2*k &&& 2*l := by
  intro k l
  have : ∀ m, 2*m &&& 1 = 0 := by intros; rw [Nat.land_one, Nat.mul_mod_right]
  have : 2*l + 1 = 2*l ^^^ 1 := Nat.add_eq_xor (this l)
  calc
    2*k &&& (2*l + 1)
      = 2*k &&& (2*l ^^^ 1) := by rw [‹2*l + 1 = 2*l ^^^ 1›]
    _ = (2*k &&& 2*l) ^^^ (2*k &&& 1) := Nat.and_xor ..
    _ = (2*k &&& 2*l) ^^^ 0 := by rw [‹∀ m, 2*m &&& 1 = 0›]
    _ = 2*k &&& 2 * l:= by rw [Nat.xor_zero]
State after:
n : Nat
this✝ : 2 * succ n - 1 = 2 * (succ n - 1) + 1
this : ∀ (k l : Nat), 2 * k &&& 2 * l + 1 = 2 * k &&& 2 * l
⊢ 2 * (succ n ^^^ succ n &&& succ n - 1) = 2 * succ n ^^^ 2 * succ n &&& 2 * succ n - 1

State before:
n : Nat
this✝ : 2 * succ n - 1 = 2 * (succ n - 1) + 1
this : ∀ (k l : Nat), 2 * k &&& 2 * l + 1 = 2 * k &&& 2 * l
⊢ 2 * (succ n ^^^ succ n &&& succ n - 1) = 2 * succ n ^^^ 2 * succ n &&& 2 * succ n - 1
Tactic:
rw [‹2*n.succ - 1 = 2 * (n.succ - 1) + 1›, this]
State after:
n : Nat
this✝ : 2 * succ n - 1 = 2 * (succ n - 1) + 1
this : ∀ (k l : Nat), 2 * k &&& 2 * l + 1 = 2 * k &&& 2 * l
⊢ 2 * (succ n ^^^ succ n &&& succ n - 1) = 2 * succ n ^^^ 2 * succ n &&& 2 * (succ n - 1)

State before:
n : Nat
this✝ : 2 * succ n - 1 = 2 * (succ n - 1) + 1
this : ∀ (k l : Nat), 2 * k &&& 2 * l + 1 = 2 * k &&& 2 * l
⊢ 2 * (succ n ^^^ succ n &&& succ n - 1) = 2 * succ n ^^^ 2 * succ n &&& 2 * (succ n - 1)
Tactic:
conv =>
  rhs; simp only [←Nat.shiftLeft_one]
  simp only [←Nat.land_shiftLeft, ←Nat.xor_shiftLeft]
State after:
no goals

State before:
n : Nat
⊢ 2 * succ n - 1 = 2 * (succ n - 1) + 1
Tactic:
simp only [Nat.mul_succ, Nat.succ_sub_one]
State after:
no goals

State before:
n : Nat
this : 2 * succ n - 1 = 2 * (succ n - 1) + 1
⊢ ∀ (k l : Nat), 2 * k &&& 2 * l + 1 = 2 * k &&& 2 * l
Tactic:
intro k l
State after:
n : Nat
this : 2 * succ n - 1 = 2 * (succ n - 1) + 1
k l : Nat
⊢ 2 * k &&& 2 * l + 1 = 2 * k &&& 2 * l

State before:
n : Nat
this : 2 * succ n - 1 = 2 * (succ n - 1) + 1
k l : Nat
⊢ 2 * k &&& 2 * l + 1 = 2 * k &&& 2 * l
Tactic:
have : ∀ m, 2*m &&& 1 = 0 := by intros; rw [Nat.land_one, Nat.mul_mod_right]
State after:
n : Nat
this✝ : 2 * succ n - 1 = 2 * (succ n - 1) + 1
k l : Nat
this : ∀ (m : Nat), 2 * m &&& 1 = 0
⊢ 2 * k &&& 2 * l + 1 = 2 * k &&& 2 * l

State before:
n : Nat
this✝ : 2 * succ n - 1 = 2 * (succ n - 1) + 1
k l : Nat
this : ∀ (m : Nat), 2 * m &&& 1 = 0
⊢ 2 * k &&& 2 * l + 1 = 2 * k &&& 2 * l
Tactic:
have : 2*l + 1 = 2*l ^^^ 1 := Nat.add_eq_xor (this l)
State after:
n : Nat
this✝¹ : 2 * succ n - 1 = 2 * (succ n - 1) + 1
k l : Nat
this✝ : ∀ (m : Nat), 2 * m &&& 1 = 0
this : 2 * l + 1 = 2 * l ^^^ 1
⊢ 2 * k &&& 2 * l + 1 = 2 * k &&& 2 * l

State before:
n : Nat
this✝¹ : 2 * succ n - 1 = 2 * (succ n - 1) + 1
k l : Nat
this✝ : ∀ (m : Nat), 2 * m &&& 1 = 0
this : 2 * l + 1 = 2 * l ^^^ 1
⊢ 2 * k &&& 2 * l + 1 = 2 * k &&& 2 * l
Tactic:
calc
  2*k &&& (2*l + 1)
    = 2*k &&& (2*l ^^^ 1) := by rw [‹2*l + 1 = 2*l ^^^ 1›]
  _ = (2*k &&& 2*l) ^^^ (2*k &&& 1) := Nat.and_xor ..
  _ = (2*k &&& 2*l) ^^^ 0 := by rw [‹∀ m, 2*m &&& 1 = 0›]
  _ = 2*k &&& 2 * l:= by rw [Nat.xor_zero]
State after:
no goals

State before:
n : Nat
this : 2 * succ n - 1 = 2 * (succ n - 1) + 1
k l : Nat
⊢ ∀ (m : Nat), 2 * m &&& 1 = 0
Tactic:
intros
State after:
n : Nat
this : 2 * succ n - 1 = 2 * (succ n - 1) + 1
k l m✝ : Nat
⊢ 2 * m✝ &&& 1 = 0

State before:
n : Nat
this : 2 * succ n - 1 = 2 * (succ n - 1) + 1
k l m✝ : Nat
⊢ 2 * m✝ &&& 1 = 0
Tactic:
rw [Nat.land_one, Nat.mul_mod_right]
State after:
no goals

State before:
n : Nat
this✝¹ : 2 * succ n - 1 = 2 * (succ n - 1) + 1
k l : Nat
this✝ : ∀ (m : Nat), 2 * m &&& 1 = 0
this : 2 * l + 1 = 2 * l ^^^ 1
⊢ 2 * k &&& 2 * l + 1 = 2 * k &&& (2 * l ^^^ 1)
Tactic:
rw [‹2*l + 1 = 2*l ^^^ 1›]
State after:
no goals

State before:
n : Nat
this✝¹ : 2 * succ n - 1 = 2 * (succ n - 1) + 1
k l : Nat
this✝ : ∀ (m : Nat), 2 * m &&& 1 = 0
this : 2 * l + 1 = 2 * l ^^^ 1
⊢ 2 * k &&& 2 * l ^^^ 2 * k &&& 1 = 2 * k &&& 2 * l ^^^ 0
Tactic:
rw [‹∀ m, 2*m &&& 1 = 0›]
State after:
no goals

State before:
n : Nat
this✝¹ : 2 * succ n - 1 = 2 * (succ n - 1) + 1
k l : Nat
this✝ : ∀ (m : Nat), 2 * m &&& 1 = 0
this : 2 * l + 1 = 2 * l ^^^ 1
⊢ 2 * k &&& 2 * l ^^^ 0 = 2 * k &&& 2 * l
Tactic:
rw [Nat.xor_zero]
State after:
no goals