add term on both sides

Stream: new members

[Winston Yin]

What's the simplest way to prove this?

example {N : Type*} [add_comm_monoid N] (x y z : N) : x = y → x + z = y + z := sorry

[Johan Commelin]

by rintro rfl; refl or by intro h; rw h

[Yury G. Kudryashov]

See also tactic#subst

[Eric Rodriguez]

if you want to change a term, you can also do apply_fun (+ z) at h

[Eric Rodriguez]

(you'll get a non-beta reduced term but they are defeq)

[Winston Yin]

Let me try apply_fun. I have these looooong terms x, y, z, with a current goal of x + z = y + z. I'd like to change the goal to x = y without writing out the whole term

[Yakov Pechersky]

example {N : Type*} [add_comm_monoid N] (x y z : N) : x = y → x + z = y + z :=
congr_arg _

[Yakov Pechersky]

Winston, try the congr and congr' 1 tactics

[Yakov Pechersky]

congr' 1 is basically apply congr_arg

[Yakov Pechersky]

congr is mathlib speak for "do this thing to both sides"

[Winston Yin]

congr worked. Thanks!

[Yakov Pechersky]

so there are a lot of lemmas and tactics that use that vocab

[Johan Commelin]

@Winston Yin now try to add z on the left, and see how you need to adept all the various proofs that were suggested.

[Yakov Pechersky]

In fact,

example {N : Type*} [has_add N] (x y z : N) : x = y → x + z = y + z :=
congr_arg _