Theorem: getBitRes_succAbove (Controlbits/BitResiduum.lean)

State before:
m : ℕ
j : Fin (m + 2)
i : Fin (m + 1)
⊢ getBitRes (j.succAbove i) = getBitResSuccAbove j i
Tactic:
simp_rw [Equiv.ext_iff, getBitResSuccAbove_apply,
  getBitRes_apply, getBitRes_symm_apply, Equiv.symm_apply_apply,
  Prod.mk.injEq, EmbeddingLike.apply_eq_iff_eq,
  Fin.eq_insertNth_iff, Fin.succAbove_succAbove_predAbove,
  Fin.succAbove_succAbove_predAbove_succAbove, true_and, implies_true]
State after:
no goals