a problem about lean4 code

Stream: new members

[Billlie Franch]

theorem neg_eq_of_add_eq_zero {a b : R} (h : a + b = 0) : -a = b := by
  have h₁: a - a = a + b := by
    sorry
  sorry

Can someone help me complete this code?

[Johan Commelin]

This is not a complete stand-alone example. See #mwe.

[Johan Commelin]

Once you've turned your code into a #mwe, please outline what the next mathematical step is that you would like to take. Then we can explain how to turn it into Lean.

[Billlie Franch]

Johan Commelin said:

Once you've turned your code into a #mwe, please outline what the next mathematical step is that you would like to take. Then we can explain how to turn it into Lean.

Sorry, the full code is like this:

import Mathlib.Algebra.Ring.Defs
import Mathlib.Data.Real.Basic
import Mathlib.Tactic

theorem neg_eq_of_add_eq_zero {a b : R} (h : a + b = 0) : -a = b := by
  have h₁: a - a = a + b := by
    sorry
  sorry

[Johan Commelin]

This code cannot type check. Without more assumptions on R you can not write things like a + b.

[Johan Commelin]

You probably want to assume that R is a group/ring/field or something.

[Johan Commelin]

Or maybe you want to use the real numbers, given your list of imports.