prove `c=c` in ring

Stream: new members

[Hank]

I was doing the exercises in Mathematics in Lean, and I was trying to prove the following:

theorem add_left_cancel (a b c : R) (h : a + b = a + c) : b = c := by
  rw [←neg_add_cancel_left a b, h, ←add_assoc, add_left_neg, zero_add, rfl]

Everything worked except the rfl in the last. The error message was

tactic 'rewrite' failed, pattern is a metavariable
  ?m.3545
from equation
  ?m.3545 = ?m.3545
R : Type u_1
inst✝ : Ring R
a b c : R
h : a + b = a + c
⊢ c = c

Changing rfl to refl didn't work either.

[Ruben Van de Velde]

Try just removing it

[Richard Osborn]

It might help to look through the following example and try to understand what is happening. Note that rewrite is rw, but it does not try to close the goal with rfl after rewriting. Also, note that rfl is both a tactic and a term. In particular, the example can just be solved with the tactic rfl alone.

#check Eq.refl -- Eq.refl.{u_1} {α : Sort u_1} (a : α) : a = a
#check rfl     -- rfl.{u} {α : Sort u} {a : α} : a = a

example : c = c := by
  rewrite [Eq.refl c]
  rewrite [rfl (a := c)]
  exact rfl

[Kevin Buzzard]

I don't think rw [rfl] is ever correct (in the sense that it's never useful and very likely to fail)

[Colin Jones ⚛️]

You can just remove the rfl in the rw tactic as rw does it for you.

theorem add_left_cancel (a b c : ℝ) (h : a + b = a + c) : b = c := by
rw [←neg_add_cancel_left a b, h, ←add_assoc, add_left_neg, zero_add]

[Hank]

Thanks!