How to optimize this proof

Stream: new members

[Michael Bucko]

I used a couple of new techniques to prove this one. Again, that's a new proof from The Mechanics.., spoiler alert. Can I collapse the calc into a one-liner? Can I use some functional programming approach here to solve this in one line?

Proof

example {x y : ℝ} (h : x = 2 ∨ y = -2) : x * y + 2 * x = 2 * y + 4 := by
  rcases h with rfl | rfl
  · norm_num
  · calc
      x * -2 + 2 * x = -2 * x + 2 * x := by rw [mul_comm]
      _ = 0 := by ring
      _ = 2 * -2 + 4 := by norm_num

[Riccardo Brasca]

I guess ring does it immediately?

[Riccardo Brasca]

import Mathlib

example {x y : ℝ} (h : x = 2 ∨ y = -2) : x * y + 2 * x = 2 * y + 4 := by
  rcases h with rfl | rfl <;> ring

[Michael Bucko]

Much better than mine! Thank you :thank_you:

[Michael Bucko]

(deleted)

[Edward van de Meent]

Michael Bucko said:

Can I collapse the calc into a one-liner?

note that although you can have calc a = b := by foo as a single line, lean doesn't like to parse that, making the lines after very prone to parsing errors. Also, it generally can just be replaced with by foo.