case inl
a b c q : ℚ
hq : q ≤ 0
⊢ abs q = ↑(Int.natAbs q.num) /. ↑q.den

case inr
a b c q : ℚ
hq : 0 ≤ q
⊢ abs q = ↑(Int.natAbs q.num) /. ↑q.den
a b c q : ℚ
⊢ abs q = ↑(Int.natAbs q.num) /. ↑q.den
cases' le_total q 0 with hq hq
case inl
a b c q : ℚ
hq : q ≤ 0
⊢ -q = ↑(Int.natAbs q.num) /. ↑q.den
case inl
a b c q : ℚ
hq : q ≤ 0
⊢ abs q = ↑(Int.natAbs q.num) /. ↑q.den
rw [abs_of_nonpos hq]
case inl
a b c q : ℚ
hq : q.num ≤ 0
⊢ -q = ↑(Int.natAbs q.num) /. ↑q.den
case inl
a b c q : ℚ
hq : q ≤ 0
⊢ -q = ↑(Int.natAbs q.num) /. ↑q.den
rw [← @num_den q, ← divInt_zero_one, Rat.le_def (Int.coe_nat_pos.2 q.pos) zero_lt_one, mul_one,
  zero_mul] at hq
no goals
case inl
a b c q : ℚ
hq : q.num ≤ 0
⊢ -q = ↑(Int.natAbs q.num) /. ↑q.den
rw [Int.ofNat_natAbs_of_nonpos hq, ← neg_def, num_den]
case inr
a b c q : ℚ
hq : 0 ≤ q
⊢ q = ↑(Int.natAbs q.num) /. ↑q.den
case inr
a b c q : ℚ
hq : 0 ≤ q
⊢ abs q = ↑(Int.natAbs q.num) /. ↑q.den
rw [abs_of_nonneg hq]
case inr
a b c q : ℚ
hq : 0 ≤ q.num
⊢ q = ↑(Int.natAbs q.num) /. ↑q.den
case inr
a b c q : ℚ
hq : 0 ≤ q
⊢ q = ↑(Int.natAbs q.num) /. ↑q.den
rw [← @num_den q, ← divInt_zero_one, Rat.le_def zero_lt_one (Int.coe_nat_pos.2 q.pos), mul_one,
  zero_mul] at hq
no goals
case inr
a b c q : ℚ
hq : 0 ≤ q.num
⊢ q = ↑(Int.natAbs q.num) /. ↑q.den
rw [Int.natAbs_of_nonneg hq, num_den]