## Stream: maths

### Topic: real examples for ring?

#### Joseph Corneli (Mar 27 2019 at 16:24):

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 (Mar 27 2019 at 16:27):

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.

thanks

#### Chris Hughes (Mar 27 2019 at 16:28):

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 (Mar 27 2019 at 16:38):

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 (Mar 27 2019 at 16:44):

rintro rfl :rolling_eyes:

Last updated: May 14 2021 at 19:21 UTC