Theorem: exercise1_1 (LeanCourse/Assignments/Solutions/Solutions1.lean)

State before:
a b c d : ℝ
⊢ a + b + c + d = d + (b + a) + c
Tactic:
rw [add_comm a b, add_assoc d, add_comm d]
State after:
no goals