Stream: new members

Topic: add term on both sides

Winston Yin (Jun 21 2021 at 14:57):

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 (Jun 21 2021 at 14:58):

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

Eric Rodriguez (Jun 21 2021 at 15:00):

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

Eric Rodriguez (Jun 21 2021 at 15:01):

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

Winston Yin (Jun 21 2021 at 15:01):

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 (Jun 21 2021 at 15:01):

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


Yakov Pechersky (Jun 21 2021 at 15:02):

Winston, try the congr and congr' 1 tactics

Yakov Pechersky (Jun 21 2021 at 15:02):

congr' 1 is basically apply congr_arg

Yakov Pechersky (Jun 21 2021 at 15:03):

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

Winston Yin (Jun 21 2021 at 15:03):

congr worked. Thanks!

Yakov Pechersky (Jun 21 2021 at 15:03):

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

Johan Commelin (Jun 21 2021 at 15:08):

@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 (Jun 21 2021 at 15:09):

In fact,

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


Last updated: Dec 20 2023 at 11:08 UTC