Unwrapping definitions of functions using a simp set

Stream: general

[l1mey]

I have defined the simp set iN_to_bitvec, and I would like it to unwrap uses of iN.* functions and replace them with their implementations. How could I do that? I'm okay with defining a custom tactic, it just has to be explicit when you want to take the sledgehammer to an expression.

@[iN_to_bitvec]
protected def iN.shl_nsw {n} : iN n → iN n → iN n
  | poison, _ => poison
  | _, poison => poison
  | bitvec a, bitvec b =>
    let s := b.toNat
    if s >= n then
      poison
    else
      let res := a <<< s
      -- does the sign bit of the result differ from the sign bit of the original number?
      if a.msb != res.msb then
        poison
      else
        fromBitVec res

theorem t {n} (a : iN n): iN.shl_nsw a 0 = a := by
  cases a
  case poison => rfl
  case bitvec a =>
    simp only [iN_to_bitvec] at *
    -- simp made no progress