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

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

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