case inl
p q✝ q : ℚ
hq : q ≤ 0
⊢ toNNRat q⁻¹ = (toNNRat q)⁻¹

case inr
p q✝ q : ℚ
hq : 0 ≤ q
⊢ toNNRat q⁻¹ = (toNNRat q)⁻¹
p q✝ q : ℚ
⊢ toNNRat q⁻¹ = (toNNRat q)⁻¹
obtain hq | hq := le_total q 0
no goals
case inl
p q✝ q : ℚ
hq : q ≤ 0
⊢ toNNRat q⁻¹ = (toNNRat q)⁻¹
rw [toNNRat_eq_zero.mpr hq, inv_zero, toNNRat_eq_zero.mpr (inv_nonpos.mpr hq)]
case inr
p q✝ q : ℚ
hq : 0 ≤ q
⊢ toNNRat (↑(toNNRat q))⁻¹ = (toNNRat q)⁻¹
case inr
p q✝ q : ℚ
hq : 0 ≤ q
⊢ toNNRat q⁻¹ = (toNNRat q)⁻¹
nth_rw 1 [← Rat.coe_toNNRat q hq]
no goals
case inr
p q✝ q : ℚ
hq : 0 ≤ q
⊢ toNNRat (↑(toNNRat q))⁻¹ = (toNNRat q)⁻¹
rw [← coe_inv, toNNRat_coe]