a : Rat
⊢ (if h : a.num < 0 then mk' (-↑a.den) (Int.natAbs a.num)
    else if h : a.num > 0 then mk' (↑a.den) (Int.natAbs a.num) else a) =
    ↑a.den /. a.num
a : Rat
⊢ Rat.inv a = ↑a.den /. a.num
unfold Rat.inv
case inl
a : Rat
h✝ : a.num < 0
⊢ mk' (-↑a.den) (Int.natAbs a.num) = ↑a.den /. a.num

case inr
a : Rat
h✝ : ¬a.num < 0
⊢ (if h : a.num > 0 then mk' (↑a.den) (Int.natAbs a.num) else a) = ↑a.den /. a.num
a : Rat
⊢ (if h : a.num < 0 then mk' (-↑a.den) (Int.natAbs a.num)
    else if h : a.num > 0 then mk' (↑a.den) (Int.natAbs a.num) else a) =
    ↑a.den /. a.num
split
case inr.inl
a : Rat
h✝¹ : ¬a.num < 0
h✝ : a.num > 0
⊢ mk' (↑a.den) (Int.natAbs a.num) = ↑a.den /. a.num

case inr.inr
a : Rat
h✝¹ : ¬a.num < 0
h✝ : ¬a.num > 0
⊢ a = ↑a.den /. a.num
case inr
a : Rat
h✝ : ¬a.num < 0
⊢ (if h : a.num > 0 then mk' (↑a.den) (Int.natAbs a.num) else a) = ↑a.den /. a.num
split
no goals
case inl
a : Rat
h✝ : a.num < 0
⊢ mk' (-↑a.den) (Int.natAbs a.num) = ↑a.den /. a.num
next h => rw [mk_eq_divInt, ← Int.natAbs_neg,
  Int.natAbs_of_nonneg (Int.le_of_lt <| Int.neg_pos_of_neg h), neg_divInt_neg]
no goals
a : Rat
h : a.num < 0
⊢ mk' (-↑a.den) (Int.natAbs a.num) = ↑a.den /. a.num
rw [mk_eq_divInt, ← Int.natAbs_neg,
Int.natAbs_of_nonneg (Int.le_of_lt <| Int.neg_pos_of_neg h), neg_divInt_neg]
no goals
case inr.inl
a : Rat
h✝¹ : ¬a.num < 0
h✝ : a.num > 0
⊢ mk' (↑a.den) (Int.natAbs a.num) = ↑a.den /. a.num
next h => rw [mk_eq_divInt, Int.natAbs_of_nonneg (Int.le_of_lt h)]
no goals
a : Rat
h✝ : ¬a.num < 0
h : a.num > 0
⊢ mk' (↑a.den) (Int.natAbs a.num) = ↑a.den /. a.num
rw [mk_eq_divInt, Int.natAbs_of_nonneg (Int.le_of_lt h)]
no goals
case inr.inr
a : Rat
h✝¹ : ¬a.num < 0
h✝ : ¬a.num > 0
⊢ a = ↑a.den /. a.num
next h₁ h₂ =>
apply (divInt_self _).symm.trans
simp [Int.le_antisymm (Int.not_lt.1 h₂) (Int.not_lt.1 h₁)]
a : Rat
h₁ : ¬a.num < 0
h₂ : ¬a.num > 0
⊢ a.num /. ↑a.den = ↑a.den /. a.num
a : Rat
h₁ : ¬a.num < 0
h₂ : ¬a.num > 0
⊢ a = ↑a.den /. a.num
apply (divInt_self _).symm.trans
no goals
a : Rat
h₁ : ¬a.num < 0
h₂ : ¬a.num > 0
⊢ a.num /. ↑a.den = ↑a.den /. a.num
simp [Int.le_antisymm (Int.not_lt.1 h₂) (Int.not_lt.1 h₁)]