Theorem: MyNat.add_comm_right (TheoremProvingLean/inductive_types.lean)

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

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

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