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

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

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

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

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