-- Mathlib/Data/Num/Lemmas.lean
theorem cmp_to_int : ∀ m n, (Ordering.casesOn (cmp m n) ((m : ℤ) < n) (m = n) ((n : ℤ) < m) : Prop)
  | 0, 0 => rfl
  | pos a, pos b => by
    have := PosNum.cmp_to_nat a b; revert this; dsimp [cmp]
    cases PosNum.cmp a b <;> dsimp <;> [simp; exact congr_arg pos; simp [GT.gt]]
  | neg a, neg b => by
    have := PosNum.cmp_to_nat b a; revert this; dsimp [cmp]
    cases PosNum.cmp b a <;> dsimp <;> [simp; simp +contextual; simp [GT.gt]]
  | pos _, 0 => PosNum.cast_pos _
  | pos _, neg _ => lt_trans (neg_lt_zero.2 <| PosNum.cast_pos _) (PosNum.cast_pos _)
  | 0, neg _ => neg_lt_zero.2 <| PosNum.cast_pos _
  | neg _, 0 => neg_lt_zero.2 <| PosNum.cast_pos _
  | neg _, pos _ => lt_trans (neg_lt_zero.2 <| PosNum.cast_pos _) (PosNum.cast_pos _)
  | 0, pos _ => PosNum.cast_pos _

Proof state:
a b : PosNum
this : Ordering.casesOn (a.cmp b) (↑a < ↑b) (a = b) (↑b < ↑a)
⊢ Ordering.casesOn ((pos a).cmp (pos b)) (↑(pos a) < ↑(pos b)) (pos a = pos b) (↑(pos b) < ↑(pos a))

Tactic:
revert this

Result:
a b : PosNum
⊢ Ordering.casesOn (a.cmp b) (↑a < ↑b) (a = b) (↑b < ↑a) →
    Ordering.casesOn ((pos a).cmp (pos b)) (↑(pos a) < ↑(pos b)) (pos a = pos b) (↑(pos b) < ↑(pos a))

Proof state:
a b : PosNum
⊢ Ordering.casesOn (b.cmp a) (↑b < ↑a) (b = a) (↑a < ↑b) →
    Ordering.casesOn ((neg a).cmp (neg b)) (↑(neg a) < ↑(neg b)) (neg a = neg b) (↑(neg b) < ↑(neg a))

Tactic:
dsimp [cmp]

Result:
a b : PosNum
⊢ Ordering.rec (↑b < ↑a) (b = a) (↑a < ↑b) (b.cmp a) → Ordering.rec (-↑a < -↑b) (neg a = neg b) (-↑b < -↑a) (b.cmp a)

Proof state:
a b : PosNum
⊢ Ordering.casesOn ((neg a).cmp (neg b)) (↑(neg a) < ↑(neg b)) (neg a = neg b) (↑(neg b) < ↑(neg a))

Tactic:
have := PosNum.cmp_to_nat b a

Result:
a b : PosNum
this : Ordering.casesOn (b.cmp a) (↑b < ↑a) (b = a) (↑a < ↑b)
⊢ Ordering.casesOn ((neg a).cmp (neg b)) (↑(neg a) < ↑(neg b)) (neg a = neg b) (↑(neg b) < ↑(neg a))

Proof state:
a b : PosNum
⊢ Ordering.casesOn (a.cmp b) (↑a < ↑b) (a = b) (↑b < ↑a) →
    Ordering.casesOn ((pos a).cmp (pos b)) (↑(pos a) < ↑(pos b)) (pos a = pos b) (↑(pos b) < ↑(pos a))

Tactic:
dsimp [cmp]

Result:
a b : PosNum
⊢ Ordering.rec (↑a < ↑b) (a = b) (↑b < ↑a) (a.cmp b) → Ordering.rec (↑a < ↑b) (pos a = pos b) (↑b < ↑a) (a.cmp b)

Proof state:
a b : PosNum
⊢ Ordering.casesOn ((pos a).cmp (pos b)) (↑(pos a) < ↑(pos b)) (pos a = pos b) (↑(pos b) < ↑(pos a))

Tactic:
have := PosNum.cmp_to_nat a b

Result:
a b : PosNum
this : Ordering.casesOn (a.cmp b) (↑a < ↑b) (a = b) (↑b < ↑a)
⊢ Ordering.casesOn ((pos a).cmp (pos b)) (↑(pos a) < ↑(pos b)) (pos a = pos b) (↑(pos b) < ↑(pos a))

Proof state:
a b : PosNum
this : Ordering.casesOn (b.cmp a) (↑b < ↑a) (b = a) (↑a < ↑b)
⊢ Ordering.casesOn ((neg a).cmp (neg b)) (↑(neg a) < ↑(neg b)) (neg a = neg b) (↑(neg b) < ↑(neg a))

Tactic:
revert this

Result:
a b : PosNum
⊢ Ordering.casesOn (b.cmp a) (↑b < ↑a) (b = a) (↑a < ↑b) →
    Ordering.casesOn ((neg a).cmp (neg b)) (↑(neg a) < ↑(neg b)) (neg a = neg b) (↑(neg b) < ↑(neg a))

Proof state:
a b : PosNum
⊢ Ordering.rec (↑b < ↑a) (b = a) (↑a < ↑b) (b.cmp a) → Ordering.rec (-↑a < -↑b) (neg a = neg b) (-↑b < -↑a) (b.cmp a)

Tactic:
cases PosNum.cmp b a <;> dsimp <;> [simp; simp +contextual; simp [GT.gt]]

Result:
no goals

Proof state:
a b : PosNum
⊢ Ordering.rec (↑a < ↑b) (a = b) (↑b < ↑a) (a.cmp b) → Ordering.rec (↑a < ↑b) (pos a = pos b) (↑b < ↑a) (a.cmp b)

Tactic:
cases PosNum.cmp a b <;> dsimp <;> [simp; exact congr_arg pos; simp [GT.gt]]

Result:
no goals