real examples for ring?

Stream: maths

[Joseph Corneli]

The first two examples here are successful but not very interesting; the third fails. Could someone suggest a more interesting working example to illustrate ring?

example (x : ℝ) : x=2 → 2+x=x+2 := begin intro h, ring, end -- works
example (x : ℝ) : x=2 → 2*x=x*2 := begin intro h, ring, end -- works
example (x : ℝ) : x=2 → 2+x=x*2 := begin intro h, ring, end -- fails

[Johan Commelin]

ring is good at expanding parentheses. So take (x + y)*(3+x^2+y), and put the expanded version on the RHS. Then ring can prove you did it right.

[Joseph Corneli]

thanks

[Chris Hughes]

I think ring just doesn't use hypotheses.
A more interesting example is

example (x y : ℝ) : (x - y) ^ 3 = x^3 - 3 * x^2 * y + 3 * x * y^2 - y^3 := by ring

[Mario Carneiro]

Something less obvious using a combination of ring and substitution:

example (x y : ℝ) : x=2 → (x+y)^2=y*(y+x*x)+x*2 := by rintro rfl; ring

[Chris Hughes]

rintro rfl :rolling_eyes: