awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
m : PosNum
IH : ∀ (n : PosNum), (m.cmp n).swap = n.cmp m
n : PosNum
bit0 :
  Ordering.swap
      (Ordering.casesOn (motive := fun (x : Ordering) ↦ Ordering) Ordering.lt Ordering.lt Ordering.lt Ordering.gt) =
    Ordering.casesOn (motive := fun (x : Ordering) ↦ Ordering) Ordering.lt.swap Ordering.lt Ordering.gt Ordering.gt
bit0₁ :
  Ordering.swap
      (Ordering.casesOn (motive := fun (x : Ordering) ↦ Ordering) Ordering.eq Ordering.lt Ordering.lt Ordering.gt) =
    Ordering.casesOn (motive := fun (x : Ordering) ↦ Ordering) Ordering.eq.swap Ordering.lt Ordering.gt Ordering.gt
⊢ Ordering.swap
      (Ordering.casesOn (motive := fun (x : Ordering) ↦ Ordering) (m.cmp n) Ordering.lt Ordering.lt Ordering.gt) =
    Ordering.casesOn (motive := fun (x : Ordering) ↦ Ordering) (m.cmp n).swap Ordering.lt Ordering.gt Ordering.gt
have bit0₂ : Ordering.swap
    (Ordering.casesOn (motive := fun (x : Ordering) ↦ Ordering) Ordering.gt Ordering.lt Ordering.lt Ordering.gt) =
  Ordering.casesOn (motive := fun (x : Ordering) ↦ Ordering) Ordering.gt.swap Ordering.lt Ordering.gt Ordering.gt
Tactic: cases cmp m n
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
a b : PosNum
⊢ Ordering.casesOn (motive := fun (x : Ordering) ↦ Prop) (a.bit0.cmp b.bit0)
    (LT.lt (α := ℕ) (↑a.bit0 : ℕ) (↑b.bit0 : ℕ)) (a.bit0 = b.bit0) (LT.lt (α := ℕ) (↑b.bit0 : ℕ) (↑a.bit0 : ℕ))
have dsimp : Ordering.rec (motive := fun (x : Ordering) ↦ Prop)
  (HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑a : ℕ) < HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑b : ℕ)) (a.bit0 = b.bit0)
  (HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑b : ℕ) < HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑a : ℕ)) (a.cmp b)
Tactic: dsimp [cmp]
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
a b : PosNum
⊢ Ordering.rec (motive := fun (x : Ordering) ↦ Prop)
    (HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑a : ℕ) < HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑b : ℕ)) (a.bit0 = b.bit0)
    (HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑b : ℕ) < HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑a : ℕ)) (a.cmp b)
have have : ∀
  (this :
    Ordering.casesOn (motive := fun (x : Ordering) ↦ Prop) (a.cmp b) (LT.lt (α := ℕ) (↑a : ℕ) (↑b : ℕ)) (a = b)
      (LT.lt (α := ℕ) (↑b : ℕ) (↑a : ℕ))),
  Ordering.rec (motive := fun (x : Ordering) ↦ Prop)
    (HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑a : ℕ) < HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑b : ℕ)) (a.bit0 = b.bit0)
    (HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑b : ℕ) < HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑a : ℕ)) (a.cmp b)
Tactic: have := cmp_to_nat a b
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
a b : PosNum
this :
  Ordering.casesOn (motive := fun (x : Ordering) ↦ Prop) (a.cmp b) (LT.lt (α := ℕ) (↑a : ℕ) (↑b : ℕ)) (a = b)
    (LT.lt (α := ℕ) (↑b : ℕ) (↑a : ℕ))
⊢ Ordering.rec (motive := fun (x : Ordering) ↦ Prop)
    (HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑a : ℕ) < HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑b : ℕ)) (a.bit0 = b.bit0)
    (HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑b : ℕ) < HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑a : ℕ)) (a.cmp b)
have revert : ∀
  (this :
    Ordering.casesOn (motive := fun (x : Ordering) ↦ Prop) (a.cmp b) (LT.lt (α := ℕ) (↑a : ℕ) (↑b : ℕ)) (a = b)
      (LT.lt (α := ℕ) (↑b : ℕ) (↑a : ℕ))),
  Ordering.rec (motive := fun (x : Ordering) ↦ Prop)
    (HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑a : ℕ) < HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑b : ℕ)) (a.bit0 = b.bit0)
    (HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑b : ℕ) < HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑a : ℕ)) (a.cmp b)
Tactic: revert this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
a b : PosNum
⊢ ∀
    (this :
      Ordering.casesOn (motive := fun (x : Ordering) ↦ Prop) (a.cmp b) (LT.lt (α := ℕ) (↑a : ℕ) (↑b : ℕ)) (a = b)
        (LT.lt (α := ℕ) (↑b : ℕ) (↑a : ℕ))),
    Ordering.rec (motive := fun (x : Ordering) ↦ Prop)
      (HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑a : ℕ) < HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑b : ℕ)) (a.bit0 = b.bit0)
      (HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑b : ℕ) < HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑a : ℕ)) (a.cmp b)
have lt : ∀
  (this :
    Ordering.casesOn (motive := fun (x : Ordering) ↦ Prop) Ordering.lt (LT.lt (α := ℕ) (↑a : ℕ) (↑b : ℕ)) (a = b)
      (LT.lt (α := ℕ) (↑b : ℕ) (↑a : ℕ))),
  Ordering.rec (motive := fun (x : Ordering) ↦ Prop)
    (HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑a : ℕ) < HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑b : ℕ)) (a.bit0 = b.bit0)
    (HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑b : ℕ) < HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑a : ℕ)) Ordering.lt
Tactic: cases cmp a b
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
a b : PosNum
lt :
  ∀
    (this :
      Ordering.casesOn (motive := fun (x : Ordering) ↦ Prop) Ordering.lt (LT.lt (α := ℕ) (↑a : ℕ) (↑b : ℕ)) (a = b)
        (LT.lt (α := ℕ) (↑b : ℕ) (↑a : ℕ))),
    Ordering.rec (motive := fun (x : Ordering) ↦ Prop)
      (HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑a : ℕ) < HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑b : ℕ)) (a.bit0 = b.bit0)
      (HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑b : ℕ) < HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑a : ℕ)) Ordering.lt
⊢ ∀
    (this :
      Ordering.casesOn (motive := fun (x : Ordering) ↦ Prop) (a.cmp b) (LT.lt (α := ℕ) (↑a : ℕ) (↑b : ℕ)) (a = b)
        (LT.lt (α := ℕ) (↑b : ℕ) (↑a : ℕ))),
    Ordering.rec (motive := fun (x : Ordering) ↦ Prop)
      (HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑a : ℕ) < HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑b : ℕ)) (a.bit0 = b.bit0)
      (HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑b : ℕ) < HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑a : ℕ)) (a.cmp b)
have eq : ∀
  (this :
    Ordering.casesOn (motive := fun (x : Ordering) ↦ Prop) Ordering.eq (LT.lt (α := ℕ) (↑a : ℕ) (↑b : ℕ)) (a = b)
      (LT.lt (α := ℕ) (↑b : ℕ) (↑a : ℕ))),
  Ordering.rec (motive := fun (x : Ordering) ↦ Prop)
    (HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑a : ℕ) < HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑b : ℕ)) (a.bit0 = b.bit0)
    (HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑b : ℕ) < HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑a : ℕ)) Ordering.eq
Tactic: cases cmp a b
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
a b : PosNum
lt :
  ∀
    (this :
      Ordering.casesOn (motive := fun (x : Ordering) ↦ Prop) Ordering.lt (LT.lt (α := ℕ) (↑a : ℕ) (↑b : ℕ)) (a = b)
        (LT.lt (α := ℕ) (↑b : ℕ) (↑a : ℕ))),
    Ordering.rec (motive := fun (x : Ordering) ↦ Prop)
      (HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑a : ℕ) < HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑b : ℕ)) (a.bit0 = b.bit0)
      (HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑b : ℕ) < HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑a : ℕ)) Ordering.lt
eq :
  ∀
    (this :
      Ordering.casesOn (motive := fun (x : Ordering) ↦ Prop) Ordering.eq (LT.lt (α := ℕ) (↑a : ℕ) (↑b : ℕ)) (a = b)
        (LT.lt (α := ℕ) (↑b : ℕ) (↑a : ℕ))),
    Ordering.rec (motive := fun (x : Ordering) ↦ Prop)
      (HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑a : ℕ) < HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑b : ℕ)) (a.bit0 = b.bit0)
      (HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑b : ℕ) < HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑a : ℕ)) Ordering.eq
⊢ ∀
    (this :
      Ordering.casesOn (motive := fun (x : Ordering) ↦ Prop) (a.cmp b) (LT.lt (α := ℕ) (↑a : ℕ) (↑b : ℕ)) (a = b)
        (LT.lt (α := ℕ) (↑b : ℕ) (↑a : ℕ))),
    Ordering.rec (motive := fun (x : Ordering) ↦ Prop)
      (HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑a : ℕ) < HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑b : ℕ)) (a.bit0 = b.bit0)
      (HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑b : ℕ) < HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑a : ℕ)) (a.cmp b)
have gt : ∀
  (this :
    Ordering.casesOn (motive := fun (x : Ordering) ↦ Prop) Ordering.gt (LT.lt (α := ℕ) (↑a : ℕ) (↑b : ℕ)) (a = b)
      (LT.lt (α := ℕ) (↑b : ℕ) (↑a : ℕ))),
  Ordering.rec (motive := fun (x : Ordering) ↦ Prop)
    (HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑a : ℕ) < HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑b : ℕ)) (a.bit0 = b.bit0)
    (HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑b : ℕ) < HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑a : ℕ)) Ordering.gt
Tactic: cases cmp a b
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
a b : PosNum
this : a = b
⊢ a.bit0 = b.bit0
have eq : b.bit0 = b.bit0
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
a b : PosNum
⊢ Ordering.casesOn (motive := fun (x : Ordering) ↦ Prop) (a.bit0.cmp b.bit1)
    (LT.lt (α := ℕ) (↑a.bit0 : ℕ) (↑b.bit1 : ℕ)) (a.bit0 = b.bit1) (LT.lt (α := ℕ) (↑b.bit1 : ℕ) (↑a.bit0 : ℕ))
have dsimp : Ordering.rec (motive := fun (x : Ordering) ↦ Prop)
  (HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑a : ℕ) < HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑b : ℕ) + 1) (a.bit0 = b.bit1)
  (HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑b : ℕ) + 1 < HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑a : ℕ))
  (Ordering.rec (motive := fun (x : Ordering) ↦ Ordering) Ordering.lt Ordering.lt Ordering.gt (a.cmp b))
Tactic: dsimp [cmp]
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
a b : PosNum
⊢ Ordering.rec (motive := fun (x : Ordering) ↦ Prop)
    (HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑a : ℕ) < HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑b : ℕ) + 1) (a.bit0 = b.bit1)
    (HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑b : ℕ) + 1 < HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑a : ℕ))
    (Ordering.rec (motive := fun (x : Ordering) ↦ Ordering) Ordering.lt Ordering.lt Ordering.gt (a.cmp b))
have have : ∀
  (this :
    Ordering.casesOn (motive := fun (x : Ordering) ↦ Prop) (a.cmp b) (LT.lt (α := ℕ) (↑a : ℕ) (↑b : ℕ)) (a = b)
      (LT.lt (α := ℕ) (↑b : ℕ) (↑a : ℕ))),
  Ordering.rec (motive := fun (x : Ordering) ↦ Prop)
    (HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑a : ℕ) < HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑b : ℕ) + 1) (a.bit0 = b.bit1)
    (HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑b : ℕ) + 1 < HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑a : ℕ))
    (Ordering.rec (motive := fun (x : Ordering) ↦ Ordering) Ordering.lt Ordering.lt Ordering.gt (a.cmp b))
Tactic: have := cmp_to_nat a b
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
a b : PosNum
this :
  Ordering.casesOn (motive := fun (x : Ordering) ↦ Prop) (a.cmp b) (LT.lt (α := ℕ) (↑a : ℕ) (↑b : ℕ)) (a = b)
    (LT.lt (α := ℕ) (↑b : ℕ) (↑a : ℕ))
⊢ Ordering.rec (motive := fun (x : Ordering) ↦ Prop)
    (HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑a : ℕ) < HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑b : ℕ) + 1) (a.bit0 = b.bit1)
    (HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑b : ℕ) + 1 < HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑a : ℕ))
    (Ordering.rec (motive := fun (x : Ordering) ↦ Ordering) Ordering.lt Ordering.lt Ordering.gt (a.cmp b))
have revert : ∀
  (this :
    Ordering.casesOn (motive := fun (x : Ordering) ↦ Prop) (a.cmp b) (LT.lt (α := ℕ) (↑a : ℕ) (↑b : ℕ)) (a = b)
      (LT.lt (α := ℕ) (↑b : ℕ) (↑a : ℕ))),
  Ordering.rec (motive := fun (x : Ordering) ↦ Prop)
    (HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑a : ℕ) < HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑b : ℕ) + 1) (a.bit0 = b.bit1)
    (HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑b : ℕ) + 1 < HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑a : ℕ))
    (Ordering.rec (motive := fun (x : Ordering) ↦ Ordering) Ordering.lt Ordering.lt Ordering.gt (a.cmp b))
Tactic: revert this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
a b : PosNum
⊢ ∀
    (this :
      Ordering.casesOn (motive := fun (x : Ordering) ↦ Prop) (a.cmp b) (LT.lt (α := ℕ) (↑a : ℕ) (↑b : ℕ)) (a = b)
        (LT.lt (α := ℕ) (↑b : ℕ) (↑a : ℕ))),
    Ordering.rec (motive := fun (x : Ordering) ↦ Prop)
      (HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑a : ℕ) < HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑b : ℕ) + 1) (a.bit0 = b.bit1)
      (HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑b : ℕ) + 1 < HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑a : ℕ))
      (Ordering.rec (motive := fun (x : Ordering) ↦ Ordering) Ordering.lt Ordering.lt Ordering.gt (a.cmp b))
have lt : ∀
  (this :
    Ordering.casesOn (motive := fun (x : Ordering) ↦ Prop) Ordering.lt (LT.lt (α := ℕ) (↑a : ℕ) (↑b : ℕ)) (a = b)
      (LT.lt (α := ℕ) (↑b : ℕ) (↑a : ℕ))),
  Ordering.rec (motive := fun (x : Ordering) ↦ Prop)
    (HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑a : ℕ) < HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑b : ℕ) + 1) (a.bit0 = b.bit1)
    (HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑b : ℕ) + 1 < HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑a : ℕ))
    (Ordering.rec (motive := fun (x : Ordering) ↦ Ordering) Ordering.lt Ordering.lt Ordering.gt Ordering.lt)
Tactic: cases cmp a b
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
a b : PosNum
lt :
  ∀
    (this :
      Ordering.casesOn (motive := fun (x : Ordering) ↦ Prop) Ordering.lt (LT.lt (α := ℕ) (↑a : ℕ) (↑b : ℕ)) (a = b)
        (LT.lt (α := ℕ) (↑b : ℕ) (↑a : ℕ))),
    Ordering.rec (motive := fun (x : Ordering) ↦ Prop)
      (HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑a : ℕ) < HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑b : ℕ) + 1) (a.bit0 = b.bit1)
      (HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑b : ℕ) + 1 < HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑a : ℕ))
      (Ordering.rec (motive := fun (x : Ordering) ↦ Ordering) Ordering.lt Ordering.lt Ordering.gt Ordering.lt)
⊢ ∀
    (this :
      Ordering.casesOn (motive := fun (x : Ordering) ↦ Prop) (a.cmp b) (LT.lt (α := ℕ) (↑a : ℕ) (↑b : ℕ)) (a = b)
        (LT.lt (α := ℕ) (↑b : ℕ) (↑a : ℕ))),
    Ordering.rec (motive := fun (x : Ordering) ↦ Prop)
      (HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑a : ℕ) < HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑b : ℕ) + 1) (a.bit0 = b.bit1)
      (HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑b : ℕ) + 1 < HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑a : ℕ))
      (Ordering.rec (motive := fun (x : Ordering) ↦ Ordering) Ordering.lt Ordering.lt Ordering.gt (a.cmp b))
have eq : ∀
  (this :
    Ordering.casesOn (motive := fun (x : Ordering) ↦ Prop) Ordering.eq (LT.lt (α := ℕ) (↑a : ℕ) (↑b : ℕ)) (a = b)
      (LT.lt (α := ℕ) (↑b : ℕ) (↑a : ℕ))),
  Ordering.rec (motive := fun (x : Ordering) ↦ Prop)
    (HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑a : ℕ) < HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑b : ℕ) + 1) (a.bit0 = b.bit1)
    (HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑b : ℕ) + 1 < HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑a : ℕ))
    (Ordering.rec (motive := fun (x : Ordering) ↦ Ordering) Ordering.lt Ordering.lt Ordering.gt Ordering.eq)
Tactic: cases cmp a b
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
a b : PosNum
lt :
  ∀
    (this :
      Ordering.casesOn (motive := fun (x : Ordering) ↦ Prop) Ordering.lt (LT.lt (α := ℕ) (↑a : ℕ) (↑b : ℕ)) (a = b)
        (LT.lt (α := ℕ) (↑b : ℕ) (↑a : ℕ))),
    Ordering.rec (motive := fun (x : Ordering) ↦ Prop)
      (HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑a : ℕ) < HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑b : ℕ) + 1) (a.bit0 = b.bit1)
      (HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑b : ℕ) + 1 < HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑a : ℕ))
      (Ordering.rec (motive := fun (x : Ordering) ↦ Ordering) Ordering.lt Ordering.lt Ordering.gt Ordering.lt)
eq :
  ∀
    (this :
      Ordering.casesOn (motive := fun (x : Ordering) ↦ Prop) Ordering.eq (LT.lt (α := ℕ) (↑a : ℕ) (↑b : ℕ)) (a = b)
        (LT.lt (α := ℕ) (↑b : ℕ) (↑a : ℕ))),
    Ordering.rec (motive := fun (x : Ordering) ↦ Prop)
      (HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑a : ℕ) < HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑b : ℕ) + 1) (a.bit0 = b.bit1)
      (HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑b : ℕ) + 1 < HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑a : ℕ))
      (Ordering.rec (motive := fun (x : Ordering) ↦ Ordering) Ordering.lt Ordering.lt Ordering.gt Ordering.eq)
⊢ ∀
    (this :
      Ordering.casesOn (motive := fun (x : Ordering) ↦ Prop) (a.cmp b) (LT.lt (α := ℕ) (↑a : ℕ) (↑b : ℕ)) (a = b)
        (LT.lt (α := ℕ) (↑b : ℕ) (↑a : ℕ))),
    Ordering.rec (motive := fun (x : Ordering) ↦ Prop)
      (HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑a : ℕ) < HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑b : ℕ) + 1) (a.bit0 = b.bit1)
      (HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑b : ℕ) + 1 < HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑a : ℕ))
      (Ordering.rec (motive := fun (x : Ordering) ↦ Ordering) Ordering.lt Ordering.lt Ordering.gt (a.cmp b))
have gt : ∀
  (this :
    Ordering.casesOn (motive := fun (x : Ordering) ↦ Prop) Ordering.gt (LT.lt (α := ℕ) (↑a : ℕ) (↑b : ℕ)) (a = b)
      (LT.lt (α := ℕ) (↑b : ℕ) (↑a : ℕ))),
  Ordering.rec (motive := fun (x : Ordering) ↦ Prop)
    (HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑a : ℕ) < HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑b : ℕ) + 1) (a.bit0 = b.bit1)
    (HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑b : ℕ) + 1 < HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑a : ℕ))
    (Ordering.rec (motive := fun (x : Ordering) ↦ Ordering) Ordering.lt Ordering.lt Ordering.gt Ordering.gt)
Tactic: cases cmp a b
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
a b : PosNum
this : a = b
⊢ HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑a : ℕ) < HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑b : ℕ) + 1
have eq : HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑b : ℕ) < HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑b : ℕ) + 1
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
a b : PosNum
⊢ Ordering.casesOn (motive := fun (x : Ordering) ↦ Prop) (a.bit1.cmp b.bit0)
    (LT.lt (α := ℕ) (↑a.bit1 : ℕ) (↑b.bit0 : ℕ)) (a.bit1 = b.bit0) (LT.lt (α := ℕ) (↑b.bit0 : ℕ) (↑a.bit1 : ℕ))
have dsimp : Ordering.rec (motive := fun (x : Ordering) ↦ Prop)
  (HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑a : ℕ) + 1 < HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑b : ℕ)) (a.bit1 = b.bit0)
  (HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑b : ℕ) < HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑a : ℕ) + 1)
  (Ordering.rec (motive := fun (x : Ordering) ↦ Ordering) Ordering.lt Ordering.gt Ordering.gt (a.cmp b))
Tactic: dsimp [cmp]
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
a b : PosNum
⊢ Ordering.rec (motive := fun (x : Ordering) ↦ Prop)
    (HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑a : ℕ) + 1 < HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑b : ℕ)) (a.bit1 = b.bit0)
    (HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑b : ℕ) < HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑a : ℕ) + 1)
    (Ordering.rec (motive := fun (x : Ordering) ↦ Ordering) Ordering.lt Ordering.gt Ordering.gt (a.cmp b))
have have : ∀
  (this :
    Ordering.casesOn (motive := fun (x : Ordering) ↦ Prop) (a.cmp b) (LT.lt (α := ℕ) (↑a : ℕ) (↑b : ℕ)) (a = b)
      (LT.lt (α := ℕ) (↑b : ℕ) (↑a : ℕ))),
  Ordering.rec (motive := fun (x : Ordering) ↦ Prop)
    (HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑a : ℕ) + 1 < HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑b : ℕ)) (a.bit1 = b.bit0)
    (HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑b : ℕ) < HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑a : ℕ) + 1)
    (Ordering.rec (motive := fun (x : Ordering) ↦ Ordering) Ordering.lt Ordering.gt Ordering.gt (a.cmp b))
Tactic: have := cmp_to_nat a b
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
a b : PosNum
this :
  Ordering.casesOn (motive := fun (x : Ordering) ↦ Prop) (a.cmp b) (LT.lt (α := ℕ) (↑a : ℕ) (↑b : ℕ)) (a = b)
    (LT.lt (α := ℕ) (↑b : ℕ) (↑a : ℕ))
⊢ Ordering.rec (motive := fun (x : Ordering) ↦ Prop)
    (HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑a : ℕ) + 1 < HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑b : ℕ)) (a.bit1 = b.bit0)
    (HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑b : ℕ) < HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑a : ℕ) + 1)
    (Ordering.rec (motive := fun (x : Ordering) ↦ Ordering) Ordering.lt Ordering.gt Ordering.gt (a.cmp b))
have revert : ∀
  (this :
    Ordering.casesOn (motive := fun (x : Ordering) ↦ Prop) (a.cmp b) (LT.lt (α := ℕ) (↑a : ℕ) (↑b : ℕ)) (a = b)
      (LT.lt (α := ℕ) (↑b : ℕ) (↑a : ℕ))),
  Ordering.rec (motive := fun (x : Ordering) ↦ Prop)
    (HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑a : ℕ) + 1 < HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑b : ℕ)) (a.bit1 = b.bit0)
    (HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑b : ℕ) < HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑a : ℕ) + 1)
    (Ordering.rec (motive := fun (x : Ordering) ↦ Ordering) Ordering.lt Ordering.gt Ordering.gt (a.cmp b))
Tactic: revert this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
a b : PosNum
⊢ ∀
    (this :
      Ordering.casesOn (motive := fun (x : Ordering) ↦ Prop) (a.cmp b) (LT.lt (α := ℕ) (↑a : ℕ) (↑b : ℕ)) (a = b)
        (LT.lt (α := ℕ) (↑b : ℕ) (↑a : ℕ))),
    Ordering.rec (motive := fun (x : Ordering) ↦ Prop)
      (HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑a : ℕ) + 1 < HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑b : ℕ)) (a.bit1 = b.bit0)
      (HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑b : ℕ) < HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑a : ℕ) + 1)
      (Ordering.rec (motive := fun (x : Ordering) ↦ Ordering) Ordering.lt Ordering.gt Ordering.gt (a.cmp b))
have lt : ∀
  (this :
    Ordering.casesOn (motive := fun (x : Ordering) ↦ Prop) Ordering.lt (LT.lt (α := ℕ) (↑a : ℕ) (↑b : ℕ)) (a = b)
      (LT.lt (α := ℕ) (↑b : ℕ) (↑a : ℕ))),
  Ordering.rec (motive := fun (x : Ordering) ↦ Prop)
    (HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑a : ℕ) + 1 < HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑b : ℕ)) (a.bit1 = b.bit0)
    (HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑b : ℕ) < HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑a : ℕ) + 1)
    (Ordering.rec (motive := fun (x : Ordering) ↦ Ordering) Ordering.lt Ordering.gt Ordering.gt Ordering.lt)
Tactic: cases cmp a b
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
a b : PosNum
lt :
  ∀
    (this :
      Ordering.casesOn (motive := fun (x : Ordering) ↦ Prop) Ordering.lt (LT.lt (α := ℕ) (↑a : ℕ) (↑b : ℕ)) (a = b)
        (LT.lt (α := ℕ) (↑b : ℕ) (↑a : ℕ))),
    Ordering.rec (motive := fun (x : Ordering) ↦ Prop)
      (HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑a : ℕ) + 1 < HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑b : ℕ)) (a.bit1 = b.bit0)
      (HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑b : ℕ) < HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑a : ℕ) + 1)
      (Ordering.rec (motive := fun (x : Ordering) ↦ Ordering) Ordering.lt Ordering.gt Ordering.gt Ordering.lt)
⊢ ∀
    (this :
      Ordering.casesOn (motive := fun (x : Ordering) ↦ Prop) (a.cmp b) (LT.lt (α := ℕ) (↑a : ℕ) (↑b : ℕ)) (a = b)
        (LT.lt (α := ℕ) (↑b : ℕ) (↑a : ℕ))),
    Ordering.rec (motive := fun (x : Ordering) ↦ Prop)
      (HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑a : ℕ) + 1 < HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑b : ℕ)) (a.bit1 = b.bit0)
      (HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑b : ℕ) < HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑a : ℕ) + 1)
      (Ordering.rec (motive := fun (x : Ordering) ↦ Ordering) Ordering.lt Ordering.gt Ordering.gt (a.cmp b))
have eq : ∀
  (this :
    Ordering.casesOn (motive := fun (x : Ordering) ↦ Prop) Ordering.eq (LT.lt (α := ℕ) (↑a : ℕ) (↑b : ℕ)) (a = b)
      (LT.lt (α := ℕ) (↑b : ℕ) (↑a : ℕ))),
  Ordering.rec (motive := fun (x : Ordering) ↦ Prop)
    (HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑a : ℕ) + 1 < HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑b : ℕ)) (a.bit1 = b.bit0)
    (HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑b : ℕ) < HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑a : ℕ) + 1)
    (Ordering.rec (motive := fun (x : Ordering) ↦ Ordering) Ordering.lt Ordering.gt Ordering.gt Ordering.eq)
Tactic: cases cmp a b
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
a b : PosNum
lt :
  ∀
    (this :
      Ordering.casesOn (motive := fun (x : Ordering) ↦ Prop) Ordering.lt (LT.lt (α := ℕ) (↑a : ℕ) (↑b : ℕ)) (a = b)
        (LT.lt (α := ℕ) (↑b : ℕ) (↑a : ℕ))),
    Ordering.rec (motive := fun (x : Ordering) ↦ Prop)
      (HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑a : ℕ) + 1 < HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑b : ℕ)) (a.bit1 = b.bit0)
      (HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑b : ℕ) < HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑a : ℕ) + 1)
      (Ordering.rec (motive := fun (x : Ordering) ↦ Ordering) Ordering.lt Ordering.gt Ordering.gt Ordering.lt)
eq :
  ∀
    (this :
      Ordering.casesOn (motive := fun (x : Ordering) ↦ Prop) Ordering.eq (LT.lt (α := ℕ) (↑a : ℕ) (↑b : ℕ)) (a = b)
        (LT.lt (α := ℕ) (↑b : ℕ) (↑a : ℕ))),
    Ordering.rec (motive := fun (x : Ordering) ↦ Prop)
      (HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑a : ℕ) + 1 < HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑b : ℕ)) (a.bit1 = b.bit0)
      (HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑b : ℕ) < HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑a : ℕ) + 1)
      (Ordering.rec (motive := fun (x : Ordering) ↦ Ordering) Ordering.lt Ordering.gt Ordering.gt Ordering.eq)
⊢ ∀
    (this :
      Ordering.casesOn (motive := fun (x : Ordering) ↦ Prop) (a.cmp b) (LT.lt (α := ℕ) (↑a : ℕ) (↑b : ℕ)) (a = b)
        (LT.lt (α := ℕ) (↑b : ℕ) (↑a : ℕ))),
    Ordering.rec (motive := fun (x : Ordering) ↦ Prop)
      (HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑a : ℕ) + 1 < HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑b : ℕ)) (a.bit1 = b.bit0)
      (HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑b : ℕ) < HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑a : ℕ) + 1)
      (Ordering.rec (motive := fun (x : Ordering) ↦ Ordering) Ordering.lt Ordering.gt Ordering.gt (a.cmp b))
have gt : ∀
  (this :
    Ordering.casesOn (motive := fun (x : Ordering) ↦ Prop) Ordering.gt (LT.lt (α := ℕ) (↑a : ℕ) (↑b : ℕ)) (a = b)
      (LT.lt (α := ℕ) (↑b : ℕ) (↑a : ℕ))),
  Ordering.rec (motive := fun (x : Ordering) ↦ Prop)
    (HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑a : ℕ) + 1 < HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑b : ℕ)) (a.bit1 = b.bit0)
    (HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑b : ℕ) < HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑a : ℕ) + 1)
    (Ordering.rec (motive := fun (x : Ordering) ↦ Ordering) Ordering.lt Ordering.gt Ordering.gt Ordering.gt)
Tactic: cases cmp a b
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
a b : PosNum
this : a = b
⊢ HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑b : ℕ) < HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑a : ℕ) + 1
have eq : HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑b : ℕ) < HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑b : ℕ) + 1
Tactic: rw [this]