q : ℚ
⊢ (-(q.num /. ↑q.den))⁻¹ = -(q.num /. ↑q.den)⁻¹
q : ℚ
⊢ (-q)⁻¹ = -q⁻¹
rw [← @num_den q]
no goals
q : ℚ
⊢ (-(q.num /. ↑q.den))⁻¹ = -(q.num /. ↑q.den)⁻¹
simp only [Rat.neg_def, Rat.inv_def', eq_self_iff_true, Rat.divInt_neg_den]