tactics after `induction ... with`, but before goals

Stream: lean4

[Jireh Loreaux]

Is it possible to run tactics after an induction ... with, but before any of the cases in the induction? I couldn't find any syntax which seemed to make this work.

[Ruben Van de Velde]

Allegedly this works:

lemma toDigitsCore_lens_eq_aux (b f : Nat) :
    ∀ (n : Nat) (l1 l2 : List Char), l1.length = l2.length →
    (Nat.toDigitsCore b f n l1).length = (Nat.toDigitsCore b f n l2).length := by
  induction f with (simp only [Nat.toDigitsCore, List.length]; intro n l1 l2 hlen)
  | zero => assumption
  | succ f ih =>

[Jireh Loreaux]

hmmm... doesn't seem to work in my use case anyway. (but what I have is a bit hard to #mwe)

[Eric Wieser]

Isn't it <;> not ;?

[Ruben Van de Velde]

I copied that straight from mathlib