Theorem: Pos.add_left_comm (Extra/Pos/Lemmas.lean)

State before:
x y z : Pos
⊢ x + (y + z) = y + (x + z)
Tactic:
by_toNat
State after:
x y z : Pos
⊢ x.toNat + (y.toNat + z.toNat) = y.toNat + (x.toNat + z.toNat)

State before:
x y z : Pos
⊢ x.toNat + (y.toNat + z.toNat) = y.toNat + (x.toNat + z.toNat)
Tactic:
exact Nat.add_left_comm ..
State after:
no goals