Is adding auto expansion possible?

[Shark-with-Blue-Shoes]

trafficstars

I'm curious to the possibility of having a feature where the Lsp can fetch the tactics invoked by the auto/eauto tactic and replace the auto tactic with the tactics. Here is an example.

Theorem simpl : forall n : nat,  n + 0 = n.
Proof. info_auto. Qed.

info_auto outputs this to the messages

(* info auto: *)

intro.
simple apply eq_sym ; trivial (in core).

The Lsp is able to replace info_auto with

Theorem simpl : forall n : nat,  n + 0 = n.
Proof. intro. simpl. apply eq_sym. apply plus_n_O. Qed.

Is this possible?

[ejgallego]

Actually I have a branch with support for code actions which could do this, however I'm not sure if getting this info from Rocq is possible.

@SkySkimmer @ppedrot any idea? [I think even if that's approximate, it would be helpful]