How does tactic solve goals in specific cases

Stream: Is there code for X?

[Rafael Grenier]

If I am writing a tactic proof and 'simp' cleanly ties up all the loose threads, is there a way to determine what proof terms simp is appealing to?

[Ruben Van de Velde]

simp?

[Rafael Grenier]

is there an equivalent to 'simp?' for linarith?

[Ruben Van de Velde]

There's always show_term linarith, but I doubt it'll teach much