Here's a verbose Lean calc proof using single rewrites:

  import tactic
  
  example (R : Type*) [comm_ring R] (a b c d : R) :
    a + b + c + d = d + b + c + a :=
  calc a + b + c + d = a + b + (c + d)   : by rw add_assoc
                 ... = a + (b + (c + d)) : by rw add_assoc
                 ... = b + (c + d) + a   : by rw add_comm
                 ... = c + d + b + a     : by rw add_comm b
                 ... = d + c + b + a     : by rw add_comm c
                 ... = d + (c + b) + a   : by rw add_assoc d
                 ... = d + (b + c) + a   : by rw add_comm c
                 ... = d + b + c + a     : by rw ← add_assoc

(I didn't put any thought into trying to make it be efficient.)