Theorem: mergeBitRes_apply_true_eq_apply_false_add_apply_true_zero (Controlbits/BitResiduum.lean)

State before:
m : ℕ
p : BV m
i : Fin (m + 1)
⊢ mergeBitRes i true p = mergeBitRes i false p + mergeBitRes i true 0
Tactic:
unfold mergeBitRes getBitRes
State after:
m : ℕ
p : BV m
i : Fin (m + 1)
⊢ Function.curry
      (⇑(Trans.trans (Trans.trans finFunctionFinEquiv.symm (Equiv.piFinSuccAbove (fun a => Fin 2) i))
            (finTwoEquiv.prodCongr finFunctionFinEquiv)).symm)
      true p =
    Function.curry
        (⇑(Trans.trans (Trans.trans finFunctionFinEquiv.symm (Equiv.piFinSuccAbove (fun a => Fin 2) i))
              (finTwoEquiv.prodCongr finFunctionFinEquiv)).symm)
        false p +
      Function.curry
        (⇑(Trans.trans (Trans.trans finFunctionFinEquiv.symm (Equiv.piFinSuccAbove (fun a => Fin 2) i))
              (finTwoEquiv.prodCongr finFunctionFinEquiv)).symm)
        true 0

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

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

State before:
m : ℕ
p : BV m
i : Fin (m + 1)
⊢ ⟨∑ x : Fin (m + 1), ↑(i.insertNth 1 (fun b => ⟨↑p / 2 ^ ↑b % 2, ⋯⟩) x) * 2 ^ ↑x, ⋯⟩ =
    ⟨∑ x : Fin (m + 1), ↑(i.insertNth 0 (fun b => ⟨↑p / 2 ^ ↑b % 2, ⋯⟩) x) * 2 ^ ↑x, ⋯⟩ +
      ⟨∑ x : Fin (m + 1), ↑(i.insertNth 1 (fun b => 0) x) * 2 ^ ↑x, ⋯⟩
Tactic:
simp_rw [Fin.add_def]
State after:
m : ℕ
p : BV m
i : Fin (m + 1)
⊢ ⟨∑ x : Fin (m + 1), ↑(i.insertNth 1 (fun b => ⟨↑p / 2 ^ ↑b % 2, ⋯⟩) x) * 2 ^ ↑x, ⋯⟩ =
    ⟨(∑ x : Fin (m + 1), ↑(i.insertNth 0 (fun b => ⟨↑p / 2 ^ ↑b % 2, ⋯⟩) x) * 2 ^ ↑x +
          ∑ x : Fin (m + 1), ↑(i.insertNth 1 (fun b => 0) x) * 2 ^ ↑x) %
        2 ^ (m + 1),
      ⋯⟩

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

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

State before:
case h
m : ℕ
p : BV m
i : Fin (m + 1)
⊢ ∑ x : Fin (m + 1), ↑(i.insertNth 1 (fun b => ⟨↑p / 2 ^ ↑b % 2, ⋯⟩) x) * 2 ^ ↑x =
    (∑ x : Fin (m + 1), ↑(i.insertNth 0 (fun b => ⟨↑p / 2 ^ ↑b % 2, ⋯⟩) x) * 2 ^ ↑x +
        ∑ x : Fin (m + 1), ↑(i.insertNth 1 (fun b => 0) x) * 2 ^ ↑x) %
      2 ^ (m + 1)
Tactic:
rw [← Finset.sum_add_distrib, Finset.sum_nat_mod, Finset.sum_congr]
State after:
case h
m : ℕ
p : BV m
i : Fin (m + 1)
⊢ ?m.88623.sum ?m.88625 =
    (∑ i_1 : Fin (m + 1),
        (↑(i.insertNth 0 (fun b => ⟨↑p / 2 ^ ↑b % 2, ⋯⟩) i_1) * 2 ^ ↑i_1 +
            ↑(i.insertNth 1 (fun b => 0) i_1) * 2 ^ ↑i_1) %
          2 ^ (m + 1)) %
      2 ^ (m + 1)

case h.h
m : ℕ
p : BV m
i : Fin (m + 1)
⊢ Finset.univ = ?m.88623

case h.a
m : ℕ
p : BV m
i : Fin (m + 1)
⊢ ∀ x ∈ ?m.88623, ↑(i.insertNth 1 (fun b => ⟨↑p / 2 ^ ↑b % 2, ⋯⟩) x) * 2 ^ ↑x = ?m.88625 x

m : ℕ
p : BV m
i : Fin (m + 1)
⊢ Finset (Fin (m + 1))

m : ℕ
p : BV m
i : Fin (m + 1)
⊢ Fin (m + 1) → ℕ