## Stream: general

### Topic: Avoiding repetition in calc mode

#### Eric Wieser (Nov 26 2020 at 22:16):

I just found out you can do this:

lemma ι_add_mul_swap (x y : M) : ι R x * ι R y + ι R y * ι R x = 0 :=
calc _ = ι R (x + y) * ι R (x + y) : by simp [mul_add, add_mul]
... = _ : ι_square_zero _


Which saves you from repeating both the LHS and RHS in the calc proof

#### Eric Wieser (Nov 26 2020 at 22:18):

Turns out you can avoid the repetition and even get things in the right order if you ignore the linter:

def ι_add_mul_swap (x y : M) :=  -- I am a def so that my type is inferred from my value
calc ι R x * ι R y + ι R y * ι R x = ι R (x + y) * ι R (x + y) : by simp [mul_add, add_mul]
... = 0 : ι_square_zero _


Last updated: May 13 2021 at 22:15 UTC