Theorem: getBitRes_castSucc (Controlbits/BitResiduum.lean)

State before:
m : ℕ
i : Fin (m + 1)
⊢ getBitRes i.castSucc = getBitResCastSucc i
Tactic:
simp_rw [Equiv.ext_iff, getBitResCastSucc_apply,
  getBitRes_apply, getBitRes_symm_apply, Equiv.symm_apply_apply,
  Prod.mk.injEq, EmbeddingLike.apply_eq_iff_eq,
  Fin.eq_insertNth_iff, Fin.succAbove_last, Fin.castSucc_succAbove_last,
  Fin.castSucc_succAbove_castSucc, true_and, implies_true]
State after:
no goals