Avoiding repetition in calc mode

Stream: general

[Eric Wieser]

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]

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 _