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

State before:
a b c : Nat
⊢ a * (b * c) = b * (a * c)
Tactic:
rw [← mul_assoc]
State after:
a b c : Nat
⊢ a * b * c = b * (a * c)

State before:
a b c : Nat
⊢ a * b * c = b * (a * c)
Tactic:
rw [mul_comm a b]
State after:
a b c : Nat
⊢ b * a * c = b * (a * c)

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