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

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

State before:
x y : Pos
⊢ (x.toNat + 1) * y.toNat = x.toNat * y.toNat + y.toNat
Tactic:
exact Nat.succ_mul ..
State after:
no goals