What's the lean4 equivalent of 'cc'?

Stream: new members

[jim]

Hi all! I'm learning Lean this evening, by working through the Natural Numbers Game. However, I'm using Lean 4, and the game just seems to be for Lean 3. So I'm converting each challenge to Lean 4 as I go. I've hit my first stumbling block: https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_game/?world=6&level=9 This chapter recommends solving with the tactic cc, but I can't see this tactic in Lean 4, or any equivalent of it. Could someone suggest how I would concisely solve this one in Lean 4?

[jim]

I found https://leanprover.github.io/lean4/doc/lean3changes.html - which looks useful, but it only seems to cover "language-level" breaking changes, rather than breaking changes in libraries, tactics, macros etc

[jim]

I also found congr, but it seems to be something different, and only usable within a conv mode (not really sure what I'm talking about here)

[Reid Barton]

I think the Lean 4 equivalent of cc is called cc--it just hasn't been written yet.

[Reid Barton]

I also didn't realize that this "maze" was within the scope of cc.

[jim]

A very logician-style answer :)

[jim]

Thanks, no worries - I don't think I need it

[Kyle Miller]

solve_by_elim might work for the maze (docs4#Mathlib.Tactic.SolveByElim.solveByElim)

[jim]

Thanks @Kyle Miller - I'm just using prelude etc at the moment and haven't figured out how to install packages like mathlib - I'll give it a go

[Patrick Massot]

@jim have you seen https://lovettsoftware.com/NaturalNumbers/TutorialWorld.lean.html?