Theorem: IMOSL.IMO2012A5.sq_sub_one_is_good (IMOSLLean4/IMO2012/A5/A5Answers/SqSubOneMap.lean)

State before:
R : Type u_1
inst✝ : CommRing R
x✝¹ x✝ : R
⊢ (fun x => x ^ 2 - 1) (x✝¹ * x✝ + 1) =
    (fun x => x ^ 2 - 1) x✝¹ * (fun x => x ^ 2 - 1) x✝ + (fun x => x ^ 2 - 1) (x✝¹ + x✝)
Tactic:
ring
State after:
no goals