Implicit arguments in induction tactic

Stream: lean4

[Frédéric Dupuis]

I just ran into an annoying discrepancy between the two syntaxes of the induction tactic regarding the way in which implicit arguments are handled:

-- Let's define a new induction principle with an implicit argument in one of the cases:
theorem my_induction {P : α → Prop} (main : ∀ {x}, P x) (x : α) : P x := main

-- In this example, I can't name the argument to `main`:
example (h : ∀ x, x = 0) (y : Nat) : y = 0 := by
  induction y using my_induction with
  | main => sorry   -- how do I get `x` here?

-- Whereas it works fine if I use this syntax instead:
example (h : ∀ x, x = 0) (y : Nat) : y = 0 := by
  induction y using my_induction
  case main x => exact h x

Is this a known issue? (Note that there are some instances of induction principles like this in mathlib, such as docs#MeasureTheory.StronglyMeasurable.induction)

[Kyle Miller]

Use | @main x =>