definitional equality making my head spin

Stream: new members

[Eric Rodriguez]

Heya! I'm Eric, and I'm hoping to formalise some combinatorial statements for my undergrad thesis. I've been working through all the examples from the books, and I'm confused as to why this doesn't work:

theorem self_sub_error (a : R) : a - a = 0 :=
begin
  rw add_comm a (-a), exact add_left_neg _
end

complaining about no instance of a + -a but as far as I understood, a - a and a + -a are the same thing within Lean. it works just fine if I prepend it with suffices h: a + -a = 0, by exact h, , which makes sense, but I'm not sure why I have to do this at all.

[Yakov Pechersky]

What constraints to you have on R?

[Johan Commelin]

They are not the same. rw sub_eq_add_neg should help you

[Yakov Pechersky]

For example. add_left_neg wouldn't work unless [add_group R]

[Johan Commelin]

Until two months ago they were defeq, but mathlib was refactored to solve some hairy issues.

[Eric Rodriguez]

Yakov, this is just from 2.2 in Mathematics in Lean

[Eric Rodriguez]

Ahh I see, but then why does exact h solve it?

[Johan Commelin]

hmm, MiL is still using an old mathlib, I guess.

[Johan Commelin]

Anyway, the reason rw doesn't work is because it looks at syntax, not just up to defeq

[Eric Rodriguez]

makes sense, thanks!