case mk
m : ℕ
b : Bool
xs : List Bool
P : List.length xs = m
⊢ Bitvec.toNat ({ val := xs, property := P }++ₜb ::ᵥ Vector.nil) =
    Bitvec.toNat { val := xs, property := P } * 2 + Bitvec.toNat (b ::ᵥ Vector.nil)
m : ℕ
xs : Bitvec m
b : Bool
⊢ Bitvec.toNat (xs++ₜb ::ᵥ Vector.nil) = Bitvec.toNat xs * 2 + Bitvec.toNat (b ::ᵥ Vector.nil)
cases' xs with xs P
case mk
m : ℕ
b : Bool
xs : List Bool
P : List.length xs = m
⊢ bitsToNat (xs ++ [b]) = bitsToNat [b] + bitsToNat xs * 2
case mk
m : ℕ
b : Bool
xs : List Bool
P : List.length xs = m
⊢ Bitvec.toNat ({ val := xs, property := P }++ₜb ::ᵥ Vector.nil) =
    Bitvec.toNat { val := xs, property := P } * 2 + Bitvec.toNat (b ::ᵥ Vector.nil)
simp [bitsToNat_toList]
case mk
m : ℕ
b : Bool
xs : List Bool
⊢ bitsToNat (xs ++ [b]) = bitsToNat [b] + bitsToNat xs * 2
case mk
m : ℕ
b : Bool
xs : List Bool
P : List.length xs = m
⊢ bitsToNat (xs ++ [b]) = bitsToNat [b] + bitsToNat xs * 2
clear P
case mk
m : ℕ
b : Bool
xs : List Bool
⊢ List.foldl addLsb 0 (xs ++ [b]) = List.foldl addLsb 0 [b] + List.foldl addLsb 0 xs * 2
case mk
m : ℕ
b : Bool
xs : List Bool
⊢ bitsToNat (xs ++ [b]) = bitsToNat [b] + bitsToNat xs * 2
unfold bitsToNat
case mk
m : ℕ
b : Bool
xs : List Bool
⊢ List.foldl addLsb 0 (xs ++ [b]) = addLsb 0 b + List.foldl addLsb 0 xs * 2
case mk
m : ℕ
b : Bool
xs : List Bool
⊢ List.foldl addLsb 0 (xs ++ [b]) = List.foldl addLsb 0 [b] + List.foldl addLsb 0 xs * 2
rw [List.foldl, List.foldl]
case mk
m : ℕ
b : Bool
xs : List Bool
x : ℕ
h : 0 = x
⊢ List.foldl addLsb x (xs ++ [b]) = addLsb x b + List.foldl addLsb x xs * 2
case mk
m : ℕ
b : Bool
xs : List Bool
⊢ List.foldl addLsb 0 (xs ++ [b]) = addLsb 0 b + List.foldl addLsb 0 xs * 2
generalize h : 0 = x
case mk
m : ℕ
b : Bool
xs : List Bool
x : ℕ
h : 0 = x
⊢ List.foldl addLsb x (xs ++ [b]) = addLsb 0 b + List.foldl addLsb x xs * 2
case mk
m : ℕ
b : Bool
xs : List Bool
x : ℕ
h : 0 = x
⊢ List.foldl addLsb x (xs ++ [b]) = addLsb x b + List.foldl addLsb x xs * 2
conv in addLsb x b =>
  rw [← h]
case mk
m : ℕ
b : Bool
xs : List Bool
x : ℕ
⊢ List.foldl addLsb x (xs ++ [b]) = addLsb 0 b + List.foldl addLsb x xs * 2
case mk
m : ℕ
b : Bool
xs : List Bool
x : ℕ
h : 0 = x
⊢ List.foldl addLsb x (xs ++ [b]) = addLsb 0 b + List.foldl addLsb x xs * 2
clear h
case mk
m : ℕ
b : Bool
xs : List Bool
x : ℕ
⊢ addLsb (List.foldl addLsb x xs) b = addLsb 0 b + List.foldl addLsb x xs * 2
case mk
m : ℕ
b : Bool
xs : List Bool
x : ℕ
⊢ List.foldl addLsb x (xs ++ [b]) = addLsb 0 b + List.foldl addLsb x xs * 2
simp
case mk.nil
m : ℕ
b : Bool
x✝ x : ℕ
⊢ addLsb (List.foldl addLsb x []) b = addLsb 0 b + List.foldl addLsb x [] * 2

case mk.cons
m : ℕ
b : Bool
x✝¹ : ℕ
x✝ : Bool
xs : List Bool
xs_ih : ∀ (x : ℕ), addLsb (List.foldl addLsb x xs) b = addLsb 0 b + List.foldl addLsb x xs * 2
x : ℕ
⊢ addLsb (List.foldl addLsb x (x✝ :: xs)) b = addLsb 0 b + List.foldl addLsb x (x✝ :: xs) * 2
case mk
m : ℕ
b : Bool
xs : List Bool
x : ℕ
⊢ addLsb (List.foldl addLsb x xs) b = addLsb 0 b + List.foldl addLsb x xs * 2
induction' xs with x xs xs_ih generalizing x
case mk.nil
m : ℕ
b : Bool
x✝ x : ℕ
⊢ addLsb x b = addLsb 0 b + x * 2
case mk.nil
m : ℕ
b : Bool
x✝ x : ℕ
⊢ addLsb (List.foldl addLsb x []) b = addLsb 0 b + List.foldl addLsb x [] * 2
simp
case mk.nil
m : ℕ
b : Bool
x✝ x : ℕ
⊢ (x + x + bif b then 1 else 0) = (0 + 0 + bif b then 1 else 0) + x * 2
case mk.nil
m : ℕ
b : Bool
x✝ x : ℕ
⊢ addLsb x b = addLsb 0 b + x * 2
unfold addLsb
no goals
case mk.nil
m : ℕ
b : Bool
x✝ x : ℕ
⊢ (x + x + bif b then 1 else 0) = (0 + 0 + bif b then 1 else 0) + x * 2
simp [Nat.mul_succ]
case mk.cons
m : ℕ
b : Bool
x✝¹ : ℕ
x✝ : Bool
xs : List Bool
xs_ih : ∀ (x : ℕ), addLsb (List.foldl addLsb x xs) b = addLsb 0 b + List.foldl addLsb x xs * 2
x : ℕ
⊢ addLsb (List.foldl addLsb (addLsb x x✝) xs) b = addLsb 0 b + List.foldl addLsb (addLsb x x✝) xs * 2
case mk.cons
m : ℕ
b : Bool
x✝¹ : ℕ
x✝ : Bool
xs : List Bool
xs_ih : ∀ (x : ℕ), addLsb (List.foldl addLsb x xs) b = addLsb 0 b + List.foldl addLsb x xs * 2
x : ℕ
⊢ addLsb (List.foldl addLsb x (x✝ :: xs)) b = addLsb 0 b + List.foldl addLsb x (x✝ :: xs) * 2
simp
no goals
case mk.cons
m : ℕ
b : Bool
x✝¹ : ℕ
x✝ : Bool
xs : List Bool
xs_ih : ∀ (x : ℕ), addLsb (List.foldl addLsb x xs) b = addLsb 0 b + List.foldl addLsb x xs * 2
x : ℕ
⊢ addLsb (List.foldl addLsb (addLsb x x✝) xs) b = addLsb 0 b + List.foldl addLsb (addLsb x x✝) xs * 2
apply xs_ih