Theorem: Imo2017P2.good_one_sub (Compfiles/Imo2017P2.lean)

State before:
R : Type u_1
inst✝ : Ring 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:
noncomm_ring
State after:
no goals