Theorem: getBitRes_succ (Controlbits/BitResiduum.lean)

State before:
m : ℕ
i : Fin (m + 1)
⊢ getBitRes i.succ = getBitResSucc i
Tactic:
simp_rw [Equiv.ext_iff, getBitResSucc_apply,
  getBitRes_apply, getBitRes_symm_apply, Equiv.symm_apply_apply,
  Prod.mk.injEq, EmbeddingLike.apply_eq_iff_eq,
  Fin.eq_insertNth_iff, Fin.succAbove_zero, Fin.succ_succAbove_zero,
  Fin.succ_succAbove_succ, true_and, implies_true]
State after:
no goals