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

State before:
a : Fraction
ha : a.num ≠ 0
⊢ a⁻¹.denom = a.num
Tactic:
rw [inv_def a ha]
State after:
no goals