cases Classical.em (num a = 0) with
| inl ha0 =>
  cases Classical.em (num a' = 0) with
  | inl ha'0 =>
    simp [ha0, ha'0, inv_zero]
  | inr ha'0 =>
    simp [ha0, ha'0, Setoid_Iff, denom_Neq_zero] at ha
| inr ha0 =>
  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
a a' : Fraction
ha : a ≈ a'
⊢ a⁻¹ ≈ a'⁻¹
no goals