-- Mathlib/Data/Num/Lemmas.lean
theorem cmp_to_nat : ∀ m n, (Ordering.casesOn (cmp m n) ((m : ℕ) < n) (m = n) ((n : ℕ) < m) : Prop)
  | 1, 1 => rfl
  | bit0 a, 1 =>
    let h : (1 : ℕ) ≤ a := to_nat_pos a
    Nat.add_le_add h h
  | bit1 a, 1 => Nat.succ_lt_succ <| to_nat_pos <| bit0 a
  | 1, bit0 b =>
    let h : (1 : ℕ) ≤ b := to_nat_pos b
    Nat.add_le_add h h
  | 1, bit1 b => Nat.succ_lt_succ <| to_nat_pos <| bit0 b
  | bit0 a, bit0 b => by
    dsimp [cmp]
    have := cmp_to_nat a b; revert this; cases cmp a b <;> dsimp <;> intro this
    · exact Nat.add_lt_add this this
    · rw [this]
    · exact Nat.add_lt_add this this
  | bit0 a, bit1 b => by
    dsimp [cmp]
    have := cmp_to_nat a b; revert this; cases cmp a b <;> dsimp <;> intro this
    · exact Nat.le_succ_of_le (Nat.add_lt_add this this)
    · rw [this]
      apply Nat.lt_succ_self
    · exact cmp_to_nat_lemma this
  | bit1 a, bit0 b => by
    dsimp [cmp]
    have := cmp_to_nat a b; revert this; cases cmp a b <;> dsimp <;> intro this
    · exact cmp_to_nat_lemma this
    · rw [this]
      apply Nat.lt_succ_self
    · exact Nat.le_succ_of_le (Nat.add_lt_add this this)
  | bit1 a, bit1 b => by
    dsimp [cmp]
    have := cmp_to_nat a b; revert this; cases cmp a b <;> dsimp <;> intro this
    · exact Nat.succ_lt_succ (Nat.add_lt_add this this)
    · rw [this]
    · exact Nat.succ_lt_succ (Nat.add_lt_add this this)

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

Tactic:
dsimp [cmp]

Result:
a b : PosNum
⊢ Ordering.rec (↑a + ↑a < ↑b + ↑b) (a.bit0 = b.bit0) (↑b + ↑b < ↑a + ↑a) (a.cmp b)

Proof state:
case gt
a b : PosNum
this : ↑b < ↑a
⊢ ↑b + ↑b + 1 < ↑a + ↑a

Tactic:
exact cmp_to_nat_lemma this

Result:
no goals

Proof state:
case lt
a b : PosNum
this : ↑a < ↑b
⊢ ↑a + ↑a < ↑b + ↑b + 1

Tactic:
exact Nat.le_succ_of_le (Nat.add_lt_add this this)

Result:
no goals

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

Tactic:
dsimp [cmp]

Result:
a b : PosNum
⊢ Ordering.rec (↑a + ↑a + 1 < ↑b + ↑b) (a.bit1 = b.bit0) (↑b + ↑b < ↑a + ↑a + 1)
    (Ordering.rec Ordering.lt Ordering.gt Ordering.gt (a.cmp b))

Proof state:
a b : PosNum
⊢ Ordering.casesOn (a.cmp b) (↑a < ↑b) (a = b) (↑b < ↑a) →
    Ordering.rec (↑a + ↑a < ↑b + ↑b + 1) (a.bit0 = b.bit1) (↑b + ↑b + 1 < ↑a + ↑a)
      (Ordering.rec Ordering.lt Ordering.lt Ordering.gt (a.cmp b))

Tactic:
cases cmp a b <;> dsimp <;> intro this

Result:
case lt
a b : PosNum
this : ↑a < ↑b
⊢ ↑a + ↑a < ↑b + ↑b + 1

case eq
a b : PosNum
this : a = b
⊢ ↑a + ↑a < ↑b + ↑b + 1

case gt
a b : PosNum
this : ↑b < ↑a
⊢ ↑b + ↑b + 1 < ↑a + ↑a

Proof state:
case gt
a b : PosNum
this : ↑b < ↑a
⊢ ↑b + ↑b < ↑a + ↑a + 1

Tactic:
exact Nat.le_succ_of_le (Nat.add_lt_add this this)

Result:
no goals

Proof state:
case lt
a b : PosNum
this : ↑a < ↑b
⊢ ↑a + ↑a < ↑b + ↑b

Tactic:
exact Nat.add_lt_add this this

Result:
no goals

Proof state:
a b : PosNum
⊢ Ordering.casesOn (a.cmp b) (↑a < ↑b) (a = b) (↑b < ↑a) →
    Ordering.rec (↑a + ↑a + 1 < ↑b + ↑b) (a.bit1 = b.bit0) (↑b + ↑b < ↑a + ↑a + 1)
      (Ordering.rec Ordering.lt Ordering.gt Ordering.gt (a.cmp b))

Tactic:
cases cmp a b <;> dsimp <;> intro this

Result:
case lt
a b : PosNum
this : ↑a < ↑b
⊢ ↑a + ↑a + 1 < ↑b + ↑b

case eq
a b : PosNum
this : a = b
⊢ ↑b + ↑b < ↑a + ↑a + 1

case gt
a b : PosNum
this : ↑b < ↑a
⊢ ↑b + ↑b < ↑a + ↑a + 1

Proof state:
case gt
a b : PosNum
this : ↑b < ↑a
⊢ ↑b + ↑b < ↑a + ↑a

Tactic:
exact Nat.add_lt_add this this

Result:
no goals

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

Tactic:
dsimp [cmp]

Result:
a b : PosNum
⊢ Ordering.rec (↑a + ↑a < ↑b + ↑b + 1) (a.bit0 = b.bit1) (↑b + ↑b + 1 < ↑a + ↑a)
    (Ordering.rec Ordering.lt Ordering.lt Ordering.gt (a.cmp b))

Proof state:
a b : PosNum
⊢ Ordering.rec (↑a + ↑a + 1 < ↑b + ↑b) (a.bit1 = b.bit0) (↑b + ↑b < ↑a + ↑a + 1)
    (Ordering.rec Ordering.lt Ordering.gt Ordering.gt (a.cmp b))

Tactic:
have := cmp_to_nat a b

Result:
a b : PosNum
this : Ordering.casesOn (a.cmp b) (↑a < ↑b) (a = b) (↑b < ↑a)
⊢ Ordering.rec (↑a + ↑a + 1 < ↑b + ↑b) (a.bit1 = b.bit0) (↑b + ↑b < ↑a + ↑a + 1)
    (Ordering.rec Ordering.lt Ordering.gt Ordering.gt (a.cmp b))

Proof state:
case eq
a b : PosNum
this : a = b
⊢ ↑a + ↑a < ↑b + ↑b + 1

Tactic:
rw [this]

Result:
case eq
a b : PosNum
this : a = b
⊢ ↑b + ↑b < ↑b + ↑b + 1

Proof state:
case lt
a b : PosNum
this : ↑a < ↑b
⊢ ↑a + ↑a + 1 < ↑b + ↑b + 1

Tactic:
exact Nat.succ_lt_succ (Nat.add_lt_add this this)

Result:
no goals

Proof state:
a b : PosNum
⊢ Ordering.rec (↑a + ↑a < ↑b + ↑b + 1) (a.bit0 = b.bit1) (↑b + ↑b + 1 < ↑a + ↑a)
    (Ordering.rec Ordering.lt Ordering.lt Ordering.gt (a.cmp b))

Tactic:
have := cmp_to_nat a b

Result:
a b : PosNum
this : Ordering.casesOn (a.cmp b) (↑a < ↑b) (a = b) (↑b < ↑a)
⊢ Ordering.rec (↑a + ↑a < ↑b + ↑b + 1) (a.bit0 = b.bit1) (↑b + ↑b + 1 < ↑a + ↑a)
    (Ordering.rec Ordering.lt Ordering.lt Ordering.gt (a.cmp b))

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

Tactic:
revert this

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

Proof state:
case gt
a b : PosNum
this : ↑b < ↑a
⊢ ↑b + ↑b + 1 < ↑a + ↑a + 1

Tactic:
exact Nat.succ_lt_succ (Nat.add_lt_add this this)

Result:
no goals

Proof state:
a b : PosNum
⊢ Ordering.casesOn (a.cmp b) (↑a < ↑b) (a = b) (↑b < ↑a) →
    Ordering.rec (↑a + ↑a + 1 < ↑b + ↑b + 1) (a.bit1 = b.bit1) (↑b + ↑b + 1 < ↑a + ↑a + 1) (a.cmp b)

Tactic:
cases cmp a b <;> dsimp <;> intro this

Result:
case lt
a b : PosNum
this : ↑a < ↑b
⊢ ↑a + ↑a + 1 < ↑b + ↑b + 1

case eq
a b : PosNum
this : a = b
⊢ a.bit1 = b.bit1

case gt
a b : PosNum
this : ↑b < ↑a
⊢ ↑b + ↑b + 1 < ↑a + ↑a + 1

Proof state:
a b : PosNum
this : Ordering.casesOn (a.cmp b) (↑a < ↑b) (a = b) (↑b < ↑a)
⊢ Ordering.rec (↑a + ↑a + 1 < ↑b + ↑b) (a.bit1 = b.bit0) (↑b + ↑b < ↑a + ↑a + 1)
    (Ordering.rec Ordering.lt Ordering.gt Ordering.gt (a.cmp b))

Tactic:
revert this

Result:
a b : PosNum
⊢ Ordering.casesOn (a.cmp b) (↑a < ↑b) (a = b) (↑b < ↑a) →
    Ordering.rec (↑a + ↑a + 1 < ↑b + ↑b) (a.bit1 = b.bit0) (↑b + ↑b < ↑a + ↑a + 1)
      (Ordering.rec Ordering.lt Ordering.gt Ordering.gt (a.cmp b))

Proof state:
case eq
a b : PosNum
this : a = b
⊢ a.bit1 = b.bit1

Tactic:
rw [this]

Result:
no goals

Proof state:
a b : PosNum
this : Ordering.casesOn (a.cmp b) (↑a < ↑b) (a = b) (↑b < ↑a)
⊢ Ordering.rec (↑a + ↑a < ↑b + ↑b + 1) (a.bit0 = b.bit1) (↑b + ↑b + 1 < ↑a + ↑a)
    (Ordering.rec Ordering.lt Ordering.lt Ordering.gt (a.cmp b))

Tactic:
revert this

Result:
a b : PosNum
⊢ Ordering.casesOn (a.cmp b) (↑a < ↑b) (a = b) (↑b < ↑a) →
    Ordering.rec (↑a + ↑a < ↑b + ↑b + 1) (a.bit0 = b.bit1) (↑b + ↑b + 1 < ↑a + ↑a)
      (Ordering.rec Ordering.lt Ordering.lt Ordering.gt (a.cmp b))

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

Tactic:
have := cmp_to_nat a b

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

Proof state:
a b : PosNum
⊢ Ordering.rec (↑a + ↑a + 1 < ↑b + ↑b + 1) (a.bit1 = b.bit1) (↑b + ↑b + 1 < ↑a + ↑a + 1) (a.cmp b)

Tactic:
have := cmp_to_nat a b

Result:
a b : PosNum
this : Ordering.casesOn (a.cmp b) (↑a < ↑b) (a = b) (↑b < ↑a)
⊢ Ordering.rec (↑a + ↑a + 1 < ↑b + ↑b + 1) (a.bit1 = b.bit1) (↑b + ↑b + 1 < ↑a + ↑a + 1) (a.cmp b)