Solver tactic and general-purpose problem descriptor

Stream: new members

[Michael Bucko]

I am just re-doing a bunch of proofs from different books. And I noticed that many of them can be solved using more robust tactics (1 one vs 10 or 20 lines, and so on).

1. Does there exist a tactic that first classifies the problem type, then estimates its chances of solving the problem, and tries to solve it?
2. Does there exist a tool that could view a problem in the context (think embedding space) of Lean tactics and mathlib theorems? It'd be good to run it, and then see an overview in Infoview or terminal. It'd feel like debugging and reverse engineering proof writing.

[Michael Bucko]

As for this kind of solver tactic, one could first classify the problem, and then simply develop like a proof strategy plan for a specific problem-- it could start from something like this from Formalising Mathematics

[Daniel Weber]

There's hint