proving algebraic facts

Stream: new members

[zera]

Hi,
I'm new to Lean and I'm trying to find what's the best way to have something like the following step by step proof proven in a more natural written way.
For example, In English I would write:
a - b = 0
and next I can derive the following assume a,b \in \R
a + c = b + c

but right now I need to do
calc
a + c = a - (a - b) + c := by rw [h];ring
= b + c := by ring
which is a bit unnatural to me

I guess I'm asking if there is something similar to ring but proving on P \iff Q instead of equality using the ring property. Apology if the question may be unclear!

[Kevin Buzzard]

There will be lemmas in the library saying $a-b=0\iff a=b$ and $a=b\iff a+c=b+c$ and you can rw those.

[Kevin Buzzard]

Alternatively if you have a hypothesis $a-b=0$ and want to prove $a+c=b+c$ you can use the polyrith tactic. I would encourage you to ask your question by posting code though, for example right now we don't even know the types of $a$ and $b$ (Lean has many 37s, the natural 37 and the integer 37 and the real 37 are all different objects in Lean and the difference matters).

[zera]

Thanks! Here is the code example

example (a b: ℝ) (h: a-b=0) : a+c=b+c:= by{
  calc
  a+c = (a-b)+b+c := by ring
  _ = b+c := by rw [h]; ring
}

The reason I asked is that I feel this is kind of unnatural to me that I need to explicitly rewrite a with (a -b) +b myself in order to prove this with ring tactic. Wonder if there is tactic that can implicit infer this kind of things.

(Haven't looked at polyrith in detailed, but might be the thing I'm looking for)

[Notification Bot]

4 messages were moved here from #new members > basic question by Heather Macbeth.

[Kevin Buzzard]

I would look at polyrith. Your code doesn't compile by the way -- read #mwe to learn about the best way to ask questions.