How to apply a tactic to the LHS of an equation

Stream: new members

[RedPig]

I try to understand how to use LEAN in a human interpretable way. For example, here is a LEAN proof with linarith but what I really want is just applying a simplification on the LHS of h0 by ring, which will gives x=2. How can I explicitly apply ring to $x^3 - (x + 1) * (x - 1) * x$ instead of using linarith?

import Mathlib
example
  (x : ℝ)
  (h₀ : x^3 - (x + 1) * (x - 1) * x = 2) :
  x^3 = 8 := by
  have : x=2  := by linarith
  rw [this]
  norm_num

Another simple question, say I have the inverse of the problem, given $x^3 = 8$ proves that $x=2$. What would be a good way to prove it without tactics like linarith or nlinarith

import Mathlib
example
  (x : ℝ)
  (h₀ : x^3 = 8 ) : x=2
  := by sorry

[Ruben Van de Velde]

conv_lhs => rw [...]

[Kevin Buzzard]

import Mathlib.Tactic

example
    (x : ℝ)
    (h₀ : x^3 - (x + 1) * (x - 1) * x = 2) :
    x^3 = 8 := by
  ring_nf at h₀
  subst h₀
  norm_num

for using ring on hypotheses.