Theorem: getBitRes_zero (Controlbits/BitResiduum.lean)

State before:
m : ℕ
⊢ getBitRes 0 = getBitResZero
Tactic:
ext q : 1
State after:
case H
m : ℕ
q : BV (m + 1)
⊢ (getBitRes 0) q = getBitResZero q

State before:
case H
m : ℕ
q : BV (m + 1)
⊢ (getBitRes 0) q = getBitResZero q
Tactic:
simp_rw [getBitRes_apply, getBitResZero_apply, Fin.zero_succAbove, finFunctionFinEquiv,
  Equiv.ofRightInverseOfCardLE_symm_apply, Fin.val_zero, pow_zero, Nat.div_one,
  finTwoEquiv_apply, Fin.val_succ, Equiv.ofRightInverseOfCardLE_apply,
  Nat.pow_eq, Prod.mk.injEq, decide_eq_decide, Fin.ext_iff, Fin.val_one, Fin.coe_modNat,
  Finset.sum_fin_eq_sum_range, dite_eq_ite, Fin.coe_divNat, true_and]
State after:
case H
m : ℕ
q : BV (m + 1)
⊢ (∑ x ∈ Finset.range m, if x < m then ↑q / 2 ^ (x + 1) % 2 * 2 ^ x else 0) = ↑q / 2

State before:
case H
m : ℕ
q : BV (m + 1)
⊢ (∑ x ∈ Finset.range m, if x < m then ↑q / 2 ^ (x + 1) % 2 * 2 ^ x else 0) = ↑q / 2
Tactic:
rw [Finset.sum_ite_of_true (h := fun _ H => (Finset.mem_range.mp H))]
State after:
case H
m : ℕ
q : BV (m + 1)
⊢ ∑ x ∈ Finset.range m, ↑q / 2 ^ (x + 1) % 2 * 2 ^ x = ↑q / 2

State before:
case H
m : ℕ
q : BV (m + 1)
⊢ ∑ x ∈ Finset.range m, ↑q / 2 ^ (x + 1) % 2 * 2 ^ x = ↑q / 2
Tactic:
refine' Nat.eq_of_mul_eq_mul_left (zero_lt_two)
  (add_right_cancel (b := (q : ℕ) / 2 ^ 0 % 2 * 2 ^ 0) _)
State after:
case H
m : ℕ
q : BV (m + 1)
⊢ 2 * ∑ x ∈ Finset.range m, ↑q / 2 ^ (x + 1) % 2 * 2 ^ x + ↑q / 2 ^ 0 % 2 * 2 ^ 0 =
    2 * (↑q / 2) + ↑q / 2 ^ 0 % 2 * 2 ^ 0

State before:
case H
m : ℕ
q : BV (m + 1)
⊢ 2 * ∑ x ∈ Finset.range m, ↑q / 2 ^ (x + 1) % 2 * 2 ^ x + ↑q / 2 ^ 0 % 2 * 2 ^ 0 =
    2 * (↑q / 2) + ↑q / 2 ^ 0 % 2 * 2 ^ 0
Tactic:
simp_rw [Finset.mul_sum, mul_left_comm (2 : ℕ), ← Nat.pow_succ', Nat.succ_eq_add_one,
← Finset.sum_range_succ' (fun x => (q : ℕ) / 2 ^ x % 2 * 2 ^ x), pow_zero, Nat.div_one,
  mul_one, Nat.div_add_mod, Finset.sum_range, ← finFunctionFinEquiv_symm_apply_val,
  ← finFunctionFinEquiv_apply_val, Equiv.apply_symm_apply]
State after:
no goals