Theorem: IMOSL.IMO2017A6.one_sub_is_good (IMOSLLean4/IMO2017/A6/A6.lean)

State before:
R : Type u_1
inst✝ : NonAssocRing R
x y : R
⊢ (fun x => 1 - x) ((fun x => 1 - x) x * (fun x => 1 - x) y) + (fun x => 1 - x) (x + y) = (fun x => 1 - x) (x * y)
Tactic:
rw [sub_add_sub_comm, mul_one_sub, one_sub_mul, sub_sub, sub_add, add_sub_sub_cancel,
  add_sub_add_left_eq_sub, sub_sub_cancel_left, ← sub_eq_add_neg]
State after:
no goals