Theorem: IMOSL.IMO2012A5.map_commute_of_commute (IMOSLLean4/IMO2012/A5/A5Defs.lean)

State before:
R : Type u_2
S : Type u_1
inst✝³ : NonAssocSemiring R
inst✝² : Add S
inst✝¹ : Mul S
x y : R
inst✝ : IsCancelAdd S
f : R → S
h : good f
h0 : x * y = y * x
⊢ f x * f y + f (x + y) = f y * f x + f (x + y)
Tactic:
rw [← h, h0, h, add_comm x]
State after:
no goals