Trouble with "with" command

Stream: lean4

[Teddy Baker]

I am having issues with the "with" command in two cases. First I tried this tactic for an inequality
cases lt_or_gt_of_ne ineqj with ilj igj
The tactic is recognized with the with part, but without it gives an "unknown tactic" error.
I also am having the same issue with
induction i with j hj
which is a standard tactic that should not have an issue. I have tried restarting the lean server, closing vs code, rebuilding with lake build, using a different version of the code on a different codespace. All to no avail! Any help would be appreciated.

[Marcus Rossel]

Can you post a #mwe?

[Eric Wieser]

cases lt_or_gt_of_ne ineqj with ilj igj is not valid Lean 4 syntax

[Ruben Van de Velde]

You appear to be trying to use lean 3 syntax

[Kyle Miller]

There's a cases' tactic that's like the Lean 3 cases. I forget if this is core, std, or mathlib.

[Kyle Miller]

Similarly there is induction'

[Scott Morrison]

These backwards-compatibility tactics are from import Std.Tactic.Cases.

[Kevin Buzzard]

I used to always default to cases' and induction' (because it was what I knew) until it was pointed out to me that we now have tool tips code actions to help me get the syntax for cases right.

[Patrick Massot]

and code actions too.

[Kevin Buzzard]

Oh, I'm not sure I know my tool tips from my code actions; I actually mean "click on that blue lightbulb and the correctly-formatted code magically appears".

[Eric Rodriguez]

I think that is a code action

[Teddy Baker]

Thanks everyone!