ac_rfl
a a' b b' : Fraction
ha : a.num * a'.denom = a'.num * a.denom
hb : b.num * b'.denom = b'.num * b.denom
⊢ a'.num * a.denom * b.denom * b'.denom + b'.num * b.denom * a.denom * a'.denom =
    a'.num * b'.denom * (a.denom * b.denom) + b'.num * a'.denom * (a.denom * b.denom)
no goals