cases Classical.em (num a' = 0) with
| inl ha'0 =>
  simp [ha0, ha'0, Setoid_Iff, denom_Neq_zero] at ha
| inr ha'0 =>
  simp [Setoid_Iff, ha0, ha'0] at *
  linarith
case inr
a a' : Fraction
ha : a ≈ a'
ha0 : ¬a.num = 0
⊢ a⁻¹ ≈ a'⁻¹
no goals