Theorem: LoVe.Fraction.mul_num (LoVe/Lectures/LoVe14_RationalAndRealNumbers_Demo.lean)

State before:
a b : Fraction
⊢ (a * b).num = a.num * b.num
Tactic:
rfl
State after:
no goals