awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Num.Lemmas
Goal:
n : PosNum
rw : (n + n).succ = n.bit1
rw₁ : n.bit0.succ = n.bit1
rw₂ rw₃ : n.bit1 = n.bit1
⊢ n + n + 1 = n.bit1

Tactic:
rw [add_one, bit0_of_bit0, succ]

Premises used: PosNum.add_one, PosNum.bit0_of_bit0, PosNum.succ
-- Module: Mathlib.Data.Num.Lemmas
Goal:
m p : PosNum
rw :
  HMul.hMul (α := ℕ) (↑m : ℕ) (↑p : ℕ) + HMul.hMul (α := ℕ) (↑m : ℕ) (↑p : ℕ) =
    (↑m : ℕ) * HAdd.hAdd (α := ℕ) (↑p : ℕ) (↑p : ℕ)
rw₁ rw₂ :
  HMul.hMul (α := ℕ) (↑m : ℕ) (↑p : ℕ) + HMul.hMul (α := ℕ) (↑m : ℕ) (↑p : ℕ) =
    HMul.hMul (α := ℕ) (↑m : ℕ) (↑p : ℕ) + HMul.hMul (α := ℕ) (↑m : ℕ) (↑p : ℕ)
⊢ HAdd.hAdd (α := ℕ) (↑(m * p) : ℕ) (↑(m * p) : ℕ) = (↑m : ℕ) * HAdd.hAdd (α := ℕ) (↑p : ℕ) (↑p : ℕ)

Tactic:
rw [mul_to_nat m p, left_distrib]

Premises used: left_distrib
-- Module: Mathlib.Data.Num.Lemmas
Goal:
m p : PosNum
rw :
  HMul.hMul (α := ℕ) (↑m : ℕ) (↑p : ℕ) + HMul.hMul (α := ℕ) (↑m : ℕ) (↑p : ℕ) + (↑m : ℕ) =
    (↑m : ℕ) * HAdd.hAdd (α := ℕ) (↑p : ℕ) (↑p : ℕ) + (↑m : ℕ)
rw₁ rw₂ :
  HMul.hMul (α := ℕ) (↑m : ℕ) (↑p : ℕ) + HMul.hMul (α := ℕ) (↑m : ℕ) (↑p : ℕ) + (↑m : ℕ) =
    HMul.hMul (α := ℕ) (↑m : ℕ) (↑p : ℕ) + HMul.hMul (α := ℕ) (↑m : ℕ) (↑p : ℕ) + (↑m : ℕ)
⊢ HAdd.hAdd (α := ℕ) (↑(m * p) : ℕ) (↑(m * p) : ℕ) + (↑m : ℕ) =
    (↑m : ℕ) * HAdd.hAdd (α := ℕ) (↑p : ℕ) (↑p : ℕ) + (↑m : ℕ)

Tactic:
rw [mul_to_nat m p, left_distrib]

Premises used: left_distrib
-- Module: Mathlib.Data.Num.Lemmas
Goal:
m n : PosNum
h : LT.lt (α := ℕ) (↑m : ℕ) (↑n : ℕ)
rw : HAdd.hAdd (α := ℕ) (↑m : ℕ) 1 + HAdd.hAdd (α := ℕ) (↑m : ℕ) 1 ≤ HAdd.hAdd (α := ℕ) (↑n : ℕ) (↑n : ℕ)
⊢ HAdd.hAdd (α := ℕ) (↑m : ℕ) (↑m : ℕ) + 1 + 1 ≤ HAdd.hAdd (α := ℕ) (↑n : ℕ) (↑n : ℕ)

Tactic:
rw [Nat.add_right_comm m m 1, add_assoc]

Premises used: castPosNum, add_assoc, OfNat.ofNat, Nat.add_right_comm
-- Module: Mathlib.Data.Num.Lemmas
Goal:
m n : PosNum
h : LT.lt (α := ℕ) (↑m : ℕ) (↑n : ℕ)
⊢ HAdd.hAdd (α := ℕ) (↑m : ℕ) 1 + HAdd.hAdd (α := ℕ) (↑m : ℕ) 1 ≤ HAdd.hAdd (α := ℕ) (↑n : ℕ) (↑n : ℕ)

Tactic:
Nat.add_le_add h h

Premises used: Nat.add_le_add
-- Module: Mathlib.Data.Num.Lemmas
Goal:
m n : PosNum
h : LT.lt (α := ℕ) (↑m : ℕ) (↑n : ℕ)
⊢ HAdd.hAdd (α := ℕ) (↑m : ℕ) 1 + HAdd.hAdd (α := ℕ) (↑m : ℕ) 1 ≤ HAdd.hAdd (α := ℕ) (↑n : ℕ) (↑n : ℕ)

Tactic:
exact Nat.add_le_add h h

Premises used: Nat.add_le_add
-- Module: Mathlib.Data.Num.Lemmas
Goal:
⊢ ∀ (n : PosNum), (one.cmp n).swap = n.cmp one

Tactic:
?_
-- Module: Mathlib.Data.Num.Lemmas
Goal:
m : PosNum
IH : ∀ (n : PosNum), (m.cmp n).swap = n.cmp m
⊢ ∀ (n : PosNum), (m.bit1.cmp n).swap = n.cmp m.bit1

Tactic:
?_
-- Module: Mathlib.Data.Num.Lemmas
Goal:
m : PosNum
IH : ∀ (n : PosNum), (m.cmp n).swap = n.cmp m
⊢ ∀ (n : PosNum), (m.bit0.cmp n).swap = n.cmp m.bit0

Tactic:
?_
-- Module: Mathlib.Data.Num.Lemmas
Goal:
m : PosNum
one : ∀ (n : PosNum), (PosNum.one.cmp n).swap = n.cmp PosNum.one
bit1 : ∀ (m : PosNum) (IH : ∀ (n : PosNum), (m.cmp n).swap = n.cmp m) (n : PosNum), (m.bit1.cmp n).swap = n.cmp m.bit1
bit0 : ∀ (m : PosNum) (IH : ∀ (n : PosNum), (m.cmp n).swap = n.cmp m) (n : PosNum), (m.bit0.cmp n).swap = n.cmp m.bit0
⊢ ∀ (n : PosNum), (m.cmp n).swap = n.cmp m

Tactic:
induction m with | one => ?_ | bit1 m IH => ?_ | bit0 m IH => ?_

Premises used: PosNum.bit1, PosNum.bit0, PosNum.one
-- Module: Mathlib.Data.Num.Lemmas
Goal:
n : PosNum
one : (PosNum.one.cmp PosNum.one).swap = PosNum.one.cmp PosNum.one
one₁ : ∀ (n : PosNum), (PosNum.one.cmp n.bit1).swap = n.bit1.cmp PosNum.one
one₂ : ∀ (n : PosNum), (PosNum.one.cmp n.bit0).swap = n.bit0.cmp PosNum.one
⊢ (PosNum.one.cmp n).swap = n.cmp PosNum.one

Tactic:
obtain - | n | n := n
-- Module: Mathlib.Data.Num.Lemmas
Goal:
m : PosNum
IH : ∀ (n : PosNum), (m.cmp n).swap = n.cmp m
n : PosNum
bit1 : (m.bit1.cmp one).swap = one.cmp m.bit1
bit1₁ : ∀ (n : PosNum), (m.bit1.cmp n.bit1).swap = n.bit1.cmp m.bit1
bit1₂ : ∀ (n : PosNum), (m.bit1.cmp n.bit0).swap = n.bit0.cmp m.bit1
⊢ (m.bit1.cmp n).swap = n.cmp m.bit1

Tactic:
obtain - | n | n := n
-- Module: Mathlib.Data.Num.Lemmas
Goal:
m : PosNum
IH : ∀ (n : PosNum), (m.cmp n).swap = n.cmp m
n : PosNum
bit0 : (m.bit0.cmp one).swap = one.cmp m.bit0
bit0₁ : ∀ (n : PosNum), (m.bit0.cmp n.bit1).swap = n.bit1.cmp m.bit0
bit0₂ : ∀ (n : PosNum), (m.bit0.cmp n.bit0).swap = n.bit0.cmp m.bit0
⊢ (m.bit0.cmp n).swap = n.cmp m.bit0

Tactic:
obtain - | n | n := n
-- Module: Mathlib.Data.Num.Lemmas
Goal:
m : PosNum
IH : ∀ (n : PosNum), (m.cmp n).swap = n.cmp m
n : PosNum
bit1 : (m.cmp n).swap = n.cmp m
⊢ (m.bit1.cmp n.bit1).swap = n.bit1.cmp m.bit1

Tactic:
unfold cmp

Premises used: PosNum.cmp
-- Module: Mathlib.Data.Num.Lemmas
Goal:
m : PosNum
IH : ∀ (n : PosNum), (m.cmp n).swap = n.cmp m
n : PosNum
bit1 :
  Ordering.swap
      (Ordering.casesOn (motive := fun (x : Ordering) ↦ Ordering) (m.cmp n) Ordering.lt Ordering.gt Ordering.gt) =
    Ordering.casesOn (motive := fun (x : Ordering) ↦ Ordering) (n.cmp m) Ordering.lt Ordering.lt Ordering.gt
⊢ (m.bit1.cmp n.bit0).swap = n.bit0.cmp m.bit1

Tactic:
unfold cmp

Premises used: PosNum.cmp
-- Module: Mathlib.Data.Num.Lemmas
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) (m.cmp n) Ordering.lt Ordering.lt Ordering.gt) =
    Ordering.casesOn (motive := fun (x : Ordering) ↦ Ordering) (n.cmp m) Ordering.lt Ordering.gt Ordering.gt
⊢ (m.bit0.cmp n.bit1).swap = n.bit1.cmp m.bit0

Tactic:
unfold cmp

Premises used: PosNum.cmp
-- Module: Mathlib.Data.Num.Lemmas
Goal:
m : PosNum
IH : ∀ (n : PosNum), (m.cmp n).swap = n.cmp m
n : PosNum
bit0 : (m.cmp n).swap = n.cmp m
⊢ (m.bit0.cmp n.bit0).swap = n.bit0.cmp m.bit0

Tactic:
unfold cmp

Premises used: PosNum.cmp
-- Module: Mathlib.Data.Num.Lemmas
Goal:
⊢ Ordering.eq.swap = Ordering.eq

Tactic:
rfl
-- Module: Mathlib.Data.Num.Lemmas
Goal:
⊢ Ordering.eq.swap = Ordering.eq

Tactic:
{ rfl }
-- Module: Mathlib.Data.Num.Lemmas
Goal:
⊢ Ordering.eq.swap = Ordering.eq

Tactic:
try { rfl }
-- Module: Mathlib.Data.Num.Lemmas
Goal:
n : PosNum
⊢ Ordering.lt.swap = Ordering.gt

Tactic:
rfl
-- Module: Mathlib.Data.Num.Lemmas
Goal:
n : PosNum
⊢ Ordering.lt.swap = Ordering.gt

Tactic:
{ rfl }
-- Module: Mathlib.Data.Num.Lemmas
Goal:
n : PosNum
⊢ Ordering.lt.swap = Ordering.gt

Tactic:
try { rfl }
-- Module: Mathlib.Data.Num.Lemmas
Goal:
m : PosNum
IH : ∀ (n : PosNum), (m.cmp n).swap = n.cmp m
⊢ Ordering.gt.swap = Ordering.lt

Tactic:
rfl
-- Module: Mathlib.Data.Num.Lemmas
Goal:
m : PosNum
IH : ∀ (n : PosNum), (m.cmp n).swap = n.cmp m
⊢ Ordering.gt.swap = Ordering.lt

Tactic:
{ rfl }
-- Module: Mathlib.Data.Num.Lemmas
Goal:
m : PosNum
IH : ∀ (n : PosNum), (m.cmp n).swap = n.cmp m
⊢ Ordering.gt.swap = Ordering.lt

Tactic:
try { rfl }
-- Module: Mathlib.Data.Num.Lemmas
Goal:
m : PosNum
IH : ∀ (n : PosNum), (m.cmp n).swap = n.cmp m
n : PosNum
bit1 bit1₁ : (m.cmp n).swap = (m.cmp n).swap
⊢ (m.cmp n).swap = n.cmp m

Tactic:
rw [← IH]
-- Module: Mathlib.Data.Num.Lemmas
Goal:
m : PosNum
IH : ∀ (n : PosNum), (m.cmp n).swap = n.cmp m
n : PosNum
bit1 :
  Ordering.swap
      (Ordering.casesOn (motive := fun (x : Ordering) ↦ Ordering) (m.cmp n) Ordering.lt Ordering.gt Ordering.gt) =
    Ordering.casesOn (motive := fun (x : Ordering) ↦ Ordering) (m.cmp n).swap Ordering.lt Ordering.lt Ordering.gt
⊢ Ordering.swap
      (Ordering.casesOn (motive := fun (x : Ordering) ↦ Ordering) (m.cmp n) Ordering.lt Ordering.gt Ordering.gt) =
    Ordering.casesOn (motive := fun (x : Ordering) ↦ Ordering) (n.cmp m) Ordering.lt Ordering.lt Ordering.gt

Tactic:
rw [← IH]
-- Module: Mathlib.Data.Num.Lemmas
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) (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
⊢ 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) (n.cmp m) Ordering.lt Ordering.gt Ordering.gt

Tactic:
rw [← IH]
-- Module: Mathlib.Data.Num.Lemmas
Goal:
m : PosNum
IH : ∀ (n : PosNum), (m.cmp n).swap = n.cmp m
n : PosNum
bit0 bit0₁ : (m.cmp n).swap = (m.cmp n).swap
⊢ (m.cmp n).swap = n.cmp m

Tactic:
rw [← IH]
-- Module: Mathlib.Data.Num.Lemmas
Goal:
m : PosNum
IH : ∀ (n : PosNum), (m.cmp n).swap = n.cmp m
n : PosNum
bit1 :
  Ordering.swap
      (Ordering.casesOn (motive := fun (x : Ordering) ↦ Ordering) Ordering.lt Ordering.lt Ordering.gt Ordering.gt) =
    Ordering.casesOn (motive := fun (x : Ordering) ↦ Ordering) Ordering.lt.swap Ordering.lt Ordering.lt Ordering.gt
bit1₁ :
  Ordering.swap
      (Ordering.casesOn (motive := fun (x : Ordering) ↦ Ordering) Ordering.eq Ordering.lt Ordering.gt Ordering.gt) =
    Ordering.casesOn (motive := fun (x : Ordering) ↦ Ordering) Ordering.eq.swap Ordering.lt Ordering.lt Ordering.gt
bit1₂ :
  Ordering.swap
      (Ordering.casesOn (motive := fun (x : Ordering) ↦ Ordering) Ordering.gt Ordering.lt Ordering.gt Ordering.gt) =
    Ordering.casesOn (motive := fun (x : Ordering) ↦ Ordering) Ordering.gt.swap Ordering.lt Ordering.lt Ordering.gt
⊢ Ordering.swap
      (Ordering.casesOn (motive := fun (x : Ordering) ↦ Ordering) (m.cmp n) Ordering.lt Ordering.gt Ordering.gt) =
    Ordering.casesOn (motive := fun (x : Ordering) ↦ Ordering) (m.cmp n).swap Ordering.lt Ordering.lt Ordering.gt

Tactic:
cases cmp m n

Premises used: PosNum.cmp
-- Module: Mathlib.Data.Num.Lemmas
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
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
⊢ 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

Tactic:
cases cmp m n

Premises used: PosNum.cmp
-- Module: Mathlib.Data.Num.Lemmas
Goal:
m : PosNum
IH : ∀ (n : PosNum), (m.cmp n).swap = n.cmp m
n : PosNum
⊢ Ordering.swap
      (Ordering.casesOn (motive := fun (x : Ordering) ↦ Ordering) Ordering.lt Ordering.lt Ordering.gt Ordering.gt) =
    Ordering.casesOn (motive := fun (x : Ordering) ↦ Ordering) Ordering.lt.swap Ordering.lt Ordering.lt Ordering.gt

Tactic:
rfl
-- Module: Mathlib.Data.Num.Lemmas
Goal:
m : PosNum
IH : ∀ (n : PosNum), (m.cmp n).swap = n.cmp m
n : PosNum
⊢ Ordering.swap
      (Ordering.casesOn (motive := fun (x : Ordering) ↦ Ordering) Ordering.eq Ordering.lt Ordering.gt Ordering.gt) =
    Ordering.casesOn (motive := fun (x : Ordering) ↦ Ordering) Ordering.eq.swap Ordering.lt Ordering.lt Ordering.gt

Tactic:
rfl
-- Module: Mathlib.Data.Num.Lemmas
Goal:
m : PosNum
IH : ∀ (n : PosNum), (m.cmp n).swap = n.cmp m
n : PosNum
⊢ Ordering.swap
      (Ordering.casesOn (motive := fun (x : Ordering) ↦ Ordering) Ordering.gt Ordering.lt Ordering.gt Ordering.gt) =
    Ordering.casesOn (motive := fun (x : Ordering) ↦ Ordering) Ordering.gt.swap Ordering.lt Ordering.lt Ordering.gt

Tactic:
rfl
-- Module: Mathlib.Data.Num.Lemmas
Goal:
m : PosNum
IH : ∀ (n : PosNum), (m.cmp n).swap = n.cmp m
n : PosNum
⊢ 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

Tactic:
rfl
-- Module: Mathlib.Data.Num.Lemmas
Goal:
m : PosNum
IH : ∀ (n : PosNum), (m.cmp n).swap = n.cmp m
n : PosNum
⊢ 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

Tactic:
rfl
-- Module: Mathlib.Data.Num.Lemmas
Goal:
m : PosNum
IH : ∀ (n : PosNum), (m.cmp n).swap = n.cmp m
n : PosNum
⊢ 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:
rfl
-- Module: Mathlib.Data.Num.Lemmas
Goal:
a b : PosNum
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)
⊢ 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 : ℕ))

Tactic:
dsimp [cmp]

Premises used: PosNum.cmp
-- Module: Mathlib.Data.Num.Lemmas
Goal:
a b : PosNum
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)
⊢ 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
-- Module: Mathlib.Data.Num.Lemmas
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 : ℕ))
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)
⊢ 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
-- Module: Mathlib.Data.Num.Lemmas
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
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
⊢ ∀
    (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:
cases cmp a b

Premises used: PosNum.cmp
-- Module: Mathlib.Data.Num.Lemmas
Goal:
a b : PosNum
this : LT.lt (α := ℕ) (↑a : ℕ) (↑b : ℕ)
⊢ HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑a : ℕ) < HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑b : ℕ)

Tactic:
Nat.add_lt_add this this

Premises used: Nat.add_lt_add
-- Module: Mathlib.Data.Num.Lemmas
Goal:
a b : PosNum
this : LT.lt (α := ℕ) (↑a : ℕ) (↑b : ℕ)
⊢ HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑a : ℕ) < HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑b : ℕ)

Tactic:
exact Nat.add_lt_add this this

Premises used: Nat.add_lt_add
-- Module: Mathlib.Data.Num.Lemmas
Goal:
a b : PosNum
this : a = b
eq eq₁ : b.bit0 = b.bit0
⊢ a.bit0 = b.bit0

Tactic:
rw [this]
-- Module: Mathlib.Data.Num.Lemmas
Goal:
a b : PosNum
this : LT.lt (α := ℕ) (↑b : ℕ) (↑a : ℕ)
⊢ HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑b : ℕ) < HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑a : ℕ)

Tactic:
Nat.add_lt_add this this

Premises used: Nat.add_lt_add
-- Module: Mathlib.Data.Num.Lemmas
Goal:
a b : PosNum
this : LT.lt (α := ℕ) (↑b : ℕ) (↑a : ℕ)
⊢ HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑b : ℕ) < HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑a : ℕ)

Tactic:
exact Nat.add_lt_add this this

Premises used: Nat.add_lt_add
-- Module: Mathlib.Data.Num.Lemmas
Goal:
a b : PosNum
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))
⊢ 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 : ℕ))

Tactic:
dsimp [cmp]

Premises used: PosNum.cmp
-- Module: Mathlib.Data.Num.Lemmas
Goal:
a b : PosNum
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))
⊢ 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
-- Module: Mathlib.Data.Num.Lemmas
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 : ℕ))
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))
⊢ 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
-- Module: Mathlib.Data.Num.Lemmas
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)
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)
⊢ ∀
    (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:
cases cmp a b

Premises used: PosNum.cmp
-- Module: Mathlib.Data.Num.Lemmas
Goal:
a b : PosNum
this : LT.lt (α := ℕ) (↑a : ℕ) (↑b : ℕ)
⊢ HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑a : ℕ) < HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑b : ℕ) + 1

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

Premises used: Nat.add_lt_add, Nat.le_succ_of_le, Nat.lt
-- Module: Mathlib.Data.Num.Lemmas
Goal:
a b : PosNum
this : LT.lt (α := ℕ) (↑a : ℕ) (↑b : ℕ)
⊢ HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑a : ℕ) < HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑b : ℕ) + 1

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

Premises used: Nat.add_lt_add, Nat.le_succ_of_le
-- Module: Mathlib.Data.Num.Lemmas
Goal:
a b : PosNum
this : a = b
eq : HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑b : ℕ) < HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑b : ℕ) + 1
⊢ HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑a : ℕ) < HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑b : ℕ) + 1

Tactic:
rw [this]
-- Module: Mathlib.Data.Num.Lemmas
Goal:
a b : PosNum
this : a = b
⊢ HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑b : ℕ) < HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑b : ℕ) + 1

Tactic:
apply Nat.lt_succ_self

Premises used: Nat.lt_succ_self
-- Module: Mathlib.Data.Num.Lemmas
Goal:
a b : PosNum
this : LT.lt (α := ℕ) (↑b : ℕ) (↑a : ℕ)
⊢ HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑b : ℕ) + 1 < HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑a : ℕ)

Tactic:
cmp_to_nat_lemma this

Premises used: castPosNum, PosNum.cmp_to_nat_lemma