Print Trace for `ring_nf`

Stream: Is there code for X?

[Tanner Duve]

is there a way to print to the info view what a particular call to ring_nf (and other such decision procedures) would do, similarly to simp? or aesop?.

[Kevin Buzzard]

It will do some hideously complicated thing.

import Mathlib

theorem x (a b : ℝ) : (a + b) ^ 3 = a^3+3*a^2*b+3*a*b^2+b^3 := by
  ring

#print x -- over 250 lines of impenetrable code

[Vlad Tsyrklevich]

Another way to get it inline is show_term tactic. This term is often what you're looking for, though the term generated by grind is just an invocation of an intermediate lemma which is less useful.