How to prove ∀ {x : α}, p x without introducing x

Stream: lean4

[Chris Hughes]

What's the nicest way to prove ∀ {x : α}, p x when I don't want to start the proof by introducing x. In my particular use case (here) the elaborator doesn't like the method @fun x => old_proof x so I resorted to the following which is very ugly

have ∀ (x : α), p x := old_proof
this _

[Kevin Buzzard]

Does @old_proof work?

[Ruben Van de Velde]

fun {x} => ...?

[Kevin Buzzard]

example (p : α → Prop) (h : ∀ (x : α), p x) : ∀ {x : α}, p x := @h

[Sebastian Ullrich]

Can GCD.induction not be used with induction using? Then I would just move the variables to the left of the colon (or use auto-implicits) and have induction handle the reverts.

[Chris Hughes]

I can't figure out how to give the induction hypothesis a name when I use induction using

[Sebastian Ullrich]

It should just be an additional parameter in the "pattern". It behaves basically like case.