Theorem: IMOSL.IMO2014A4.linear_good' (IMOSLLean4/IMO2014/A4/A4.lean)

State before:
k m x y : ℤ
⊢ (fun x => k * x + m) (y + (fun x => k * x + m) x) - (fun x => k * x + m) y =
    (fun x => k * x + m) ((k + 1) * x) - (fun x => k * x + m) x + k * m
Tactic:
rw [add_sub_add_right_eq_sub, mul_add, add_sub_cancel_left, add_one_mul (α := ℤ),
  add_sub_add_right_eq_sub, ← mul_sub, add_sub_cancel_right, ← mul_add]
State after:
no goals