Theorem: IMOSL.IMO2012A5.sub_one_is_good (IMOSLLean4/IMO2012/A5/A5Answers/SubOneMap.lean)

State before:
R : Type u_1
inst✝ : NonAssocRing R
x y : R
⊢ (fun x => x - 1) (x * y + 1) = (fun x => x - 1) x * (fun x => x - 1) y + (fun x => x - 1) (x + y)
Tactic:
rw [sub_one_mul, mul_sub_one, sub_sub, ← add_sub_assoc x, sub_add_cancel]
State after:
R : Type u_1
inst✝ : NonAssocRing R
x y : R
⊢ (fun x => x - 1) (x * y + 1) = x * y

State before:
R : Type u_1
inst✝ : NonAssocRing R
x y : R
⊢ (fun x => x - 1) (x * y + 1) = x * y
Tactic:
exact add_sub_cancel_right _ _
State after:
no goals