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

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

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