Similar story in Isabelle/HOL - no special tactics required for this example:
lemma
fixes a :: "'a::comm_ring"
shows "a + b + c + d = d + b + c + a"
by fastforce
Just for fun, I wrote up an equivalent but completely manual proof where every proof step consist of just one application of an existing fact - this is extremely verbose, but still quite short for this example:
lemma
fixes a :: "'a::comm_ring"
shows "a + b + c + d = d + b + c + a"
proof -
note assoc = ab_semigroup_add_class.add_ac(1)
have "a + b + c + d = a + (b + c + d)"
unfolding assoc[of a] by rule
also have "… = a + (d + (b + c))"
unfolding add.commute[of d "b + c"] by rule
also have "… = d + (b + c) + a"
unfolding add.commute[of a "d + (b + c)"] by rule
also have "… = d + b + c + a"
unfolding assoc by rule
finally show ?thesis .
qed
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.)
