Theorem: mergeBitRes_apply' (Controlbits/BitResiduum.lean)

State before:
m : ℕ
i : Fin (m + 1)
b : Bool
p : BV m
⊢ mergeBitRes i b p =
    ∑ i' : Fin (m + 1), i.insertNth (bif b then 1 else 0) (fun b => Fin.castLE ⋯ p / 2 ^ ↑b % 2) i' * 2 ^ ↑i'
Tactic:
unfold mergeBitRes getBitRes
State after:
m : ℕ
i : Fin (m + 1)
b : Bool
p : BV m
⊢ Function.curry
      (⇑(Trans.trans (Trans.trans finFunctionFinEquiv.symm (Equiv.piFinSuccAbove (fun a => Fin 2) i))
            (finTwoEquiv.prodCongr finFunctionFinEquiv)).symm)
      b p =
    ∑ i' : Fin (m + 1), i.insertNth (bif b then 1 else 0) (fun b => Fin.castLE ⋯ p / 2 ^ ↑b % 2) i' * 2 ^ ↑i'

State before:
m : ℕ
i : Fin (m + 1)
b : Bool
p : BV m
⊢ Function.curry
      (⇑(Trans.trans (Trans.trans finFunctionFinEquiv.symm (Equiv.piFinSuccAbove (fun a => Fin 2) i))
            (finTwoEquiv.prodCongr finFunctionFinEquiv)).symm)
      b p =
    ∑ i' : Fin (m + 1), i.insertNth (bif b then 1 else 0) (fun b => Fin.castLE ⋯ p / 2 ^ ↑b % 2) i' * 2 ^ ↑i'
Tactic:
simp [finFunctionFinEquiv]
State after:
m : ℕ
i : Fin (m + 1)
b : Bool
p : BV m
⊢ ⟨∑ i_1 : Fin (m + 1), ↑(i.insertNth (bif b then 1 else 0) (fun b => ⟨↑p / 2 ^ ↑b % 2, ⋯⟩) i_1) * 2 ^ ↑i_1, ⋯⟩ =
    ∑ i' : Fin (m + 1), i.insertNth (bif b then 1 else 0) (fun b => Fin.castLE ⋯ p / 2 ^ ↑b % 2) i' * 2 ^ ↑i'

State before:
m : ℕ
i : Fin (m + 1)
b : Bool
p : BV m
⊢ ⟨∑ i_1 : Fin (m + 1), ↑(i.insertNth (bif b then 1 else 0) (fun b => ⟨↑p / 2 ^ ↑b % 2, ⋯⟩) i_1) * 2 ^ ↑i_1, ⋯⟩ =
    ∑ i' : Fin (m + 1), i.insertNth (bif b then 1 else 0) (fun b => Fin.castLE ⋯ p / 2 ^ ↑b % 2) i' * 2 ^ ↑i'
Tactic:
norm_cast
State after:
m : ℕ
i : Fin (m + 1)
b : Bool
p : BV m
⊢ ⟨∑ x : Fin (m + 1), ↑(i.insertNth (bif b then 1 else 0) (fun b => ⟨↑p / 2 ^ ↑b % 2, ⋯⟩) x) * 2 ^ ↑x, ⋯⟩ =
    ∑ x : Fin (m + 1), i.insertNth (bif b then 1 else 0) (fun b => Fin.castLE ⋯ p / ↑(2 ^ ↑b) % 2) x * ↑(2 ^ ↑x)

State before:
m : ℕ
i : Fin (m + 1)
b : Bool
p : BV m
⊢ ⟨∑ x : Fin (m + 1), ↑(i.insertNth (bif b then 1 else 0) (fun b => ⟨↑p / 2 ^ ↑b % 2, ⋯⟩) x) * 2 ^ ↑x, ⋯⟩ =
    ∑ x : Fin (m + 1), i.insertNth (bif b then 1 else 0) (fun b => Fin.castLE ⋯ p / ↑(2 ^ ↑b) % 2) x * ↑(2 ^ ↑x)
Tactic:
ext
State after:
case h
m : ℕ
i : Fin (m + 1)
b : Bool
p : BV m
⊢ ↑⟨∑ x : Fin (m + 1), ↑(i.insertNth (bif b then 1 else 0) (fun b => ⟨↑p / 2 ^ ↑b % 2, ⋯⟩) x) * 2 ^ ↑x, ⋯⟩ =
    ↑(∑ x : Fin (m + 1), i.insertNth (bif b then 1 else 0) (fun b => Fin.castLE ⋯ p / ↑(2 ^ ↑b) % 2) x * ↑(2 ^ ↑x))

State before:
case h
m : ℕ
i : Fin (m + 1)
b : Bool
p : BV m
⊢ ↑⟨∑ x : Fin (m + 1), ↑(i.insertNth (bif b then 1 else 0) (fun b => ⟨↑p / 2 ^ ↑b % 2, ⋯⟩) x) * 2 ^ ↑x, ⋯⟩ =
    ↑(∑ x : Fin (m + 1), i.insertNth (bif b then 1 else 0) (fun b => Fin.castLE ⋯ p / ↑(2 ^ ↑b) % 2) x * ↑(2 ^ ↑x))
Tactic:
simp
State after:
case h
m : ℕ
i : Fin (m + 1)
b : Bool
p : BV m
⊢ ∑ x : Fin (m + 1), ↑(i.insertNth (bif b then 1 else 0) (fun b => ⟨↑p / 2 ^ ↑b % 2, ⋯⟩) x) * 2 ^ ↑x =
    ↑(∑ x : Fin (m + 1), i.insertNth (bif b then 1 else 0) (fun b => Fin.castLE ⋯ p / 2 ^ ↑b % 2) x * 2 ^ ↑x)

State before:
case h
m : ℕ
i : Fin (m + 1)
b : Bool
p : BV m
⊢ ∑ x : Fin (m + 1), ↑(i.insertNth (bif b then 1 else 0) (fun b => ⟨↑p / 2 ^ ↑b % 2, ⋯⟩) x) * 2 ^ ↑x =
    ↑(∑ x : Fin (m + 1), i.insertNth (bif b then 1 else 0) (fun b => Fin.castLE ⋯ p / 2 ^ ↑b % 2) x * 2 ^ ↑x)
Tactic:
norm_cast
State after:
case h
m : ℕ
i : Fin (m + 1)
b : Bool
p : BV m
⊢ ∑ x : Fin (m + 1), ↑(i.insertNth (bif b then 1 else 0) (fun b => ⟨↑p / 2 ^ ↑b % 2, ⋯⟩) x) * 2 ^ ↑x =
    ↑(∑ x : Fin (m + 1), i.insertNth (bif b then 1 else 0) (fun b => Fin.castLE ⋯ p / ↑(2 ^ ↑b) % 2) x * ↑(2 ^ ↑x))