Theorem: IMOSL.IMO2011A3.step1_1 (IMOSLLean4/IMO2011/A3/A3.lean)

State before:
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
f g : R → R
h : good f g
x y : R
⊢ f x - x * g x - (f y - y * g y) = 2 • (y * g x - x * g y)
Tactic:
rw [nsmul_sub, sub_eq_sub_iff_add_eq_add, ← add_sub_right_comm, ← add_sub_assoc,
  sub_eq_sub_iff_add_eq_add, two_nsmul, ← add_mul, add_assoc, ← add_mul,
  ← two_nsmul, ← h, add_comm _ (f y), add_assoc, two_nsmul, ← add_mul,
  ← add_mul, ← two_nsmul, ← h, add_comm]
State after:
no goals