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

State before:
R : Type u_1
inst✝ : NonUnitalCommRing R
C x y : R
⊢ id ((fun x => x * x + C) (x + y)) = (fun x => x * x + C) x + (2 • x + y) * id y
Tactic:
rw [id, id, add_right_comm, add_left_inj, two_nsmul, mul_add,
  add_mul, mul_comm y, add_assoc, ← add_mul, add_assoc]
State after:
no goals