awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Num.Lemmas
Goal:
a b : PosNum
this : LT.lt (α := ℕ) (↑b : ℕ) (↑a : ℕ)
⊢ HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑b : ℕ) + 1 < HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑a : ℕ)

Tactic:
exact cmp_to_nat_lemma this

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

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 : ℕ) + 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))
⊢ 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
-- 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 : ℕ) + 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))
⊢ 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
-- 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 : ℕ) + 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)
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)
⊢ ∀
    (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:
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 : ℕ) + 1 < HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑b : ℕ)

Tactic:
cmp_to_nat_lemma this

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

Tactic:
exact cmp_to_nat_lemma this

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

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 : ℕ) + 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 (α := ℕ) (↑b : ℕ) (↑a : ℕ)
⊢ HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑b : ℕ) < HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑a : ℕ) + 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
dsimp :
  Ordering.rec (motive := fun (x : Ordering) ↦ Prop)
    (HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑a : ℕ) + 1 < HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑b : ℕ) + 1) (a.bit1 = b.bit1)
    (HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑b : ℕ) + 1 < HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑a : ℕ) + 1) (a.cmp b)
⊢ Ordering.casesOn (motive := fun (x : Ordering) ↦ Prop) (a.bit1.cmp b.bit1)
    (LT.lt (α := ℕ) (↑a.bit1 : ℕ) (↑b.bit1 : ℕ)) (a.bit1 = b.bit1) (LT.lt (α := ℕ) (↑b.bit1 : ℕ) (↑a.bit1 : ℕ))

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 : ℕ) + 1 < HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑b : ℕ) + 1) (a.bit1 = b.bit1)
      (HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑b : ℕ) + 1 < HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑a : ℕ) + 1) (a.cmp b)
⊢ Ordering.rec (motive := fun (x : Ordering) ↦ Prop)
    (HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑a : ℕ) + 1 < HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑b : ℕ) + 1) (a.bit1 = b.bit1)
    (HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑b : ℕ) + 1 < HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑a : ℕ) + 1) (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 : ℕ) + 1 < HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑b : ℕ) + 1) (a.bit1 = b.bit1)
      (HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑b : ℕ) + 1 < HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑a : ℕ) + 1) (a.cmp b)
⊢ Ordering.rec (motive := fun (x : Ordering) ↦ Prop)
    (HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑a : ℕ) + 1 < HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑b : ℕ) + 1) (a.bit1 = b.bit1)
    (HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑b : ℕ) + 1 < HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑a : ℕ) + 1) (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 : ℕ) + 1 < HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑b : ℕ) + 1) (a.bit1 = b.bit1)
      (HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑b : ℕ) + 1 < HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑a : ℕ) + 1) 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 : ℕ) + 1) (a.bit1 = b.bit1)
      (HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑b : ℕ) + 1 < HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑a : ℕ) + 1) 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 : ℕ) + 1 < HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑b : ℕ) + 1) (a.bit1 = b.bit1)
      (HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑b : ℕ) + 1 < HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑a : ℕ) + 1) 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 : ℕ) + 1 < HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑b : ℕ) + 1) (a.bit1 = b.bit1)
      (HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑b : ℕ) + 1 < HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑a : ℕ) + 1) (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 : ℕ) + 1 < HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑b : ℕ) + 1

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

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

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

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

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

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

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

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

Premises used: Nat.succ_lt_succ, Nat.add_lt_add
-- Module: Mathlib.Data.Num.Lemmas
Goal:
m n : PosNum
h :
  Ordering.casesOn (motive := fun (x : Ordering) ↦ Prop) Ordering.lt (LT.lt (α := ℕ) (↑m : ℕ) (↑n : ℕ)) (m = n)
    (LT.lt (α := ℕ) (↑n : ℕ) (↑m : ℕ))
⊢ LT.lt (α := ℕ) (↑m : ℕ) (↑n : ℕ) ↔ Ordering.lt = Ordering.lt

Tactic:
simp [h]
-- Module: Mathlib.Data.Num.Lemmas
Goal:
m n : PosNum
h :
  Ordering.casesOn (motive := fun (x : Ordering) ↦ Prop) Ordering.eq (LT.lt (α := ℕ) (↑m : ℕ) (↑n : ℕ)) (m = n)
    (LT.lt (α := ℕ) (↑n : ℕ) (↑m : ℕ))
⊢ LT.lt (α := ℕ) (↑m : ℕ) (↑n : ℕ) ↔ Ordering.eq = Ordering.lt

Tactic:
simp [h]
-- Module: Mathlib.Data.Num.Lemmas
Goal:
m n : PosNum
h :
  Ordering.casesOn (motive := fun (x : Ordering) ↦ Prop) Ordering.gt (LT.lt (α := ℕ) (↑m : ℕ) (↑n : ℕ)) (m = n)
    (LT.lt (α := ℕ) (↑n : ℕ) (↑m : ℕ))
⊢ LT.lt (α := ℕ) (↑m : ℕ) (↑n : ℕ) ↔ Ordering.gt = Ordering.lt

Tactic:
simp [not_lt_of_gt h]

Premises used: not_lt_of_gt
-- Module: Mathlib.Data.Num.Lemmas
Goal:
m n : PosNum
rw : ¬LT.lt (α := ℕ) (↑n : ℕ) (↑m : ℕ) ↔ m ≤ n
⊢ LE.le (α := ℕ) (↑m : ℕ) (↑n : ℕ) ↔ m ≤ n

Tactic:
rw [← not_lt]

Premises used: not_lt
-- Module: Mathlib.Data.Num.Lemmas
Goal:
m n : PosNum
⊢ ¬LT.lt (α := ℕ) (↑n : ℕ) (↑m : ℕ) ↔ m ≤ n

Tactic:
not_congr lt_to_nat

Premises used: PosNum.lt_to_nat, not_congr
-- Module: Mathlib.Data.Num.Lemmas
Goal:
m n : PosNum
⊢ ¬LT.lt (α := ℕ) (↑n : ℕ) (↑m : ℕ) ↔ m ≤ n

Tactic:
exact not_congr lt_to_nat

Premises used: PosNum.lt_to_nat, not_congr
-- Module: Mathlib.Data.Num.Lemmas
Goal:
n : Num
zero : Num.zero + 0 = Num.zero
pos : ∀ (a : PosNum), Num.pos a + 0 = Num.pos a
⊢ n + 0 = n

Tactic:
cases n
-- Module: Mathlib.Data.Num.Lemmas
Goal:
⊢ zero + 0 = zero

Tactic:
rfl
-- Module: Mathlib.Data.Num.Lemmas
Goal:
a : PosNum
⊢ pos a + 0 = pos a

Tactic:
rfl
-- Module: Mathlib.Data.Num.Lemmas
Goal:
n : Num
zero : 0 + Num.zero = Num.zero
pos : ∀ (a : PosNum), 0 + Num.pos a = Num.pos a
⊢ 0 + n = n

Tactic:
cases n
-- Module: Mathlib.Data.Num.Lemmas
Goal:
⊢ 0 + zero = zero

Tactic:
rfl
-- Module: Mathlib.Data.Num.Lemmas
Goal:
a : PosNum
⊢ 0 + pos a = pos a

Tactic:
rfl
-- Module: Mathlib.Data.Num.Lemmas
Goal:
p : PosNum
one : pos PosNum.one + 1 = (pos PosNum.one).succ
bit1 : ∀ (a : PosNum), pos a.bit1 + 1 = (pos a.bit1).succ
bit0 : ∀ (a : PosNum), pos a.bit0 + 1 = (pos a.bit0).succ
⊢ pos p + 1 = (pos p).succ

Tactic:
cases p
-- Module: Mathlib.Data.Num.Lemmas
Goal:
⊢ pos one + 1 = (pos one).succ

Tactic:
rfl
-- Module: Mathlib.Data.Num.Lemmas
Goal:
a : PosNum
⊢ pos a.bit1 + 1 = (pos a.bit1).succ

Tactic:
rfl
-- Module: Mathlib.Data.Num.Lemmas
Goal:
a : PosNum
⊢ pos a.bit0 + 1 = (pos a.bit0).succ

Tactic:
rfl
-- Module: Mathlib.Data.Num.Lemmas
Goal:
n : Num
⊢ 0 + n.succ = (0 + n).succ

Tactic:
simp [zero_add]

Premises used: Num.zero_add
-- Module: Mathlib.Data.Num.Lemmas
Goal:
p : PosNum
rw : pos p.succ = (pos p + 0).succ
rw₁ : pos p.succ = (pos p).succ
rw₂ : pos p.succ = pos (pos p).succ'
rw₃ rw₄ : pos p.succ = pos p.succ
⊢ pos (p + 1) = (pos p + 0).succ

Tactic:
rw [PosNum.add_one, add_zero, succ, succ']

Premises used: Num.add_zero, PosNum.add_one, Num.succ, Num.succ'
-- Module: Mathlib.Data.Num.Lemmas
Goal:
⊢ ofNat' 0 = 0

Tactic:
simp [Num.ofNat']

Premises used: Num.ofNat'
-- Module: Mathlib.Data.Num.Lemmas
Goal:
b : Bool
n : ℕ
⊢ ofNat' (Nat.bit b n) = (bif b then Num.bit1 else Num.bit0) (ofNat' n)

Tactic:
Nat.binaryRec_eq _ _ (.inl rfl)

Premises used: Or.inl, Num.ofNat', rfl, Nat.binaryRec_eq
-- Module: Mathlib.Data.Num.Lemmas
Goal:
⊢ ofNat' 1 = 1

Tactic:
simp [Num.ofNat', Num.bit1]

Premises used: Num.bit1, Num.ofNat'
-- Module: Mathlib.Data.Num.Lemmas
Goal:
⊢ ofNat' (HAdd.hAdd (α := ℕ) 0 1) = ofNat' 0 + 1

Tactic:
simp [zero_add]

Premises used: Num.zero_add
-- Module: Mathlib.Data.Num.Lemmas
Goal:
b : Bool
n : ℕ
ih : ofNat' (n + 1) = ofNat' n + 1
false : ofNat' (Nat.bit Bool.false n + 1) = ofNat' (Nat.bit Bool.false n) + 1
true : ofNat' (Nat.bit Bool.true n + 1) = ofNat' (Nat.bit Bool.true n) + 1
⊢ ofNat' (Nat.bit b n + 1) = ofNat' (Nat.bit b n) + 1

Tactic:
cases b
-- Module: Mathlib.Data.Num.Lemmas
Goal:
n : ℕ
ih : ofNat' (n + 1) = ofNat' n + 1
false : (bif true then Num.bit1 else Num.bit0) (ofNat' n) = (bif Bool.false then Num.bit1 else Num.bit0) (ofNat' n) + 1
⊢ ofNat' (Nat.bit Bool.false n + 1) = ofNat' (Nat.bit Bool.false n) + 1

Tactic:
erw [ofNat'_bit true n, ofNat'_bit]

Premises used: Num.ofNat'_bit, Bool.true
-- Module: Mathlib.Data.Num.Lemmas
Goal:
n : ℕ
ih : ofNat' (n + 1) = ofNat' n + 1
⊢ (bif true then Num.bit1 else Num.bit0) (ofNat' n) = (bif false then Num.bit1 else Num.bit0) (ofNat' n) + 1

Tactic:
simp only [← bit1_of_bit1, ← bit0_of_bit0, cond]

Premises used: cond, Num.bit1_of_bit1, Num.bit0_of_bit0
-- Module: Mathlib.Data.Num.Lemmas
Goal:
n : ℕ
ih : ofNat' (n + 1) = ofNat' n + 1
⊢ Nat.bit true n + 1 = Nat.bit false (n + 1)

Tactic:
simp [Nat.bit, mul_add]

Premises used: Nat.bit, mul_add
-- Module: Mathlib.Data.Num.Lemmas
Goal:
n : ℕ
ih : ofNat' (n + 1) = ofNat' n + 1
true :
  (bif false then Num.bit1 else Num.bit0) (ofNat' n + 1) = (bif Bool.true then Num.bit1 else Num.bit0) (ofNat' n) + 1
⊢ ofNat' (Nat.bit Bool.true n + 1) = ofNat' (Nat.bit Bool.true n) + 1

Tactic:
rw [show n.bit true + 1 = (n + 1).bit false by simp [Nat.bit, mul_add],
        ofNat'_bit, ofNat'_bit, ih]

Premises used: Num.ofNat'_bit
-- Module: Mathlib.Data.Num.Lemmas
Goal:
n : ℕ
ih : ofNat' (n + 1) = ofNat' n + 1
⊢ (bif false then Num.bit1 else Num.bit0) (ofNat' n + 1) = (bif true then Num.bit1 else Num.bit0) (ofNat' n) + 1

Tactic:
simp only [cond, add_one, bit1_succ]

Premises used: cond, Num.add_one, Num.bit1_succ
-- Module: Mathlib.Data.Num.Lemmas
Goal:
m n : ℕ
zero : ofNat' (m + 0) = ofNat' m + ofNat' 0
succ : ∀ (n : ℕ), ofNat' (m + n) = ofNat' m + ofNat' n → ofNat' (m + (n + 1)) = ofNat' m + ofNat' (n + 1)
⊢ ofNat' (m + n) = ofNat' m + ofNat' n

Tactic:
induction n
-- Module: Mathlib.Data.Num.Lemmas
Goal:
m : ℕ
⊢ ofNat' (m + 0) = ofNat' m + ofNat' 0

Tactic:
simp only [Nat.add_zero, ofNat'_zero, add_zero]

Premises used: Num.add_zero, Num.ofNat'_zero, Nat.add_zero
-- Module: Mathlib.Data.Num.Lemmas
Goal:
m n : ℕ
h : ofNat' (m + n) = ofNat' m + ofNat' n
⊢ ofNat' (m + (n + 1)) = ofNat' m + ofNat' (n + 1)

Tactic:
simp only [Nat.add_succ, Nat.add_zero, ofNat'_succ, add_one, add_succ, *]

Premises used: Num.add_one, Num.ofNat'_succ, Nat.add_succ, Nat.add_zero, Num.add_succ
-- Module: Mathlib.Data.Num.Lemmas
Goal:
α : Type u_1
inst : Zero α
inst_1 : One α
inst_2 : Add α
⊢ Eq.{u_1 + 1} (α := α) (↑0 : α) 0

Tactic:
rfl

Premises used: castNum, rfl
-- Module: Mathlib.Data.Num.Lemmas
Goal:
α : Type u_1
inst : Zero α
inst_1 : One α
inst_2 : Add α
⊢ Eq.{u_1 + 1} (α := α) (↑zero : α) 0

Tactic:
rfl

Premises used: castNum, rfl
-- Module: Mathlib.Data.Num.Lemmas
Goal:
α : Type u_1
inst : Zero α
inst_1 : One α
inst_2 : Add α
⊢ Eq.{u_1 + 1} (α := α) (↑1 : α) 1

Tactic:
rfl

Premises used: castPosNum, castNum, rfl
-- Module: Mathlib.Data.Num.Lemmas
Goal:
α : Type u_1
inst : Zero α
inst_1 : One α
inst_2 : Add α
n : PosNum
⊢ Eq.{u_1 + 1} (α := α) (↑(pos n) : α) (↑n : α)

Tactic:
rfl

Premises used: castNum, rfl
-- Module: Mathlib.Data.Num.Lemmas
Goal:
n : Num
⊢ (↑n.succ : ℕ) = HAdd.hAdd (α := ℕ) (↑n : ℕ) 1

Tactic:
succ'_to_nat n

Premises used: Num.succ'_to_nat, castNum
-- 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.casesOn (motive := fun (x : Ordering) ↦ Prop) ((pos a).cmp (pos b))
      (LT.lt (α := ℕ) (↑(pos a) : ℕ) (↑(pos b) : ℕ)) (pos a = pos b) (LT.lt (α := ℕ) (↑(pos b) : ℕ) (↑(pos a) : ℕ))
⊢ Ordering.casesOn (motive := fun (x : Ordering) ↦ Prop) ((pos a).cmp (pos b))
    (LT.lt (α := ℕ) (↑(pos a) : ℕ) (↑(pos b) : ℕ)) (pos a = pos b) (LT.lt (α := ℕ) (↑(pos b) : ℕ) (↑(pos a) : ℕ))

Tactic:
have := PosNum.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.casesOn (motive := fun (x : Ordering) ↦ Prop) ((pos a).cmp (pos b))
      (LT.lt (α := ℕ) (↑(pos a) : ℕ) (↑(pos b) : ℕ)) (pos a = pos b) (LT.lt (α := ℕ) (↑(pos b) : ℕ) (↑(pos a) : ℕ))
⊢ Ordering.casesOn (motive := fun (x : Ordering) ↦ Prop) ((pos a).cmp (pos b))
    (LT.lt (α := ℕ) (↑(pos a) : ℕ) (↑(pos b) : ℕ)) (pos a = pos b) (LT.lt (α := ℕ) (↑(pos b) : ℕ) (↑(pos a) : ℕ))

Tactic:
revert this
-- Module: Mathlib.Data.Num.Lemmas
Goal:
a b : PosNum
dsimp :
  ∀
    (this :
      Ordering.rec (motive := fun (x : Ordering) ↦ Prop) (LT.lt (α := ℕ) (↑a : ℕ) (↑b : ℕ)) (a = b)
        (LT.lt (α := ℕ) (↑b : ℕ) (↑a : ℕ)) (a.cmp b)),
    Ordering.rec (motive := fun (x : Ordering) ↦ Prop) (LT.lt (α := ℕ) (↑a : ℕ) (↑b : ℕ)) (pos a = pos b)
      (LT.lt (α := ℕ) (↑b : ℕ) (↑a : ℕ)) (a.cmp b)
⊢ ∀
    (this :
      Ordering.casesOn (motive := fun (x : Ordering) ↦ Prop) (a.cmp b) (LT.lt (α := ℕ) (↑a : ℕ) (↑b : ℕ)) (a = b)
        (LT.lt (α := ℕ) (↑b : ℕ) (↑a : ℕ))),
    Ordering.casesOn (motive := fun (x : Ordering) ↦ Prop) ((pos a).cmp (pos b))
      (LT.lt (α := ℕ) (↑(pos a) : ℕ) (↑(pos b) : ℕ)) (pos a = pos b) (LT.lt (α := ℕ) (↑(pos b) : ℕ) (↑(pos a) : ℕ))

Tactic:
dsimp [cmp]

Premises used: Num.cmp
-- Module: Mathlib.Data.Num.Lemmas
Goal:
a b : PosNum
lt :
  ∀
    (this :
      Ordering.rec (motive := fun (x : Ordering) ↦ Prop) (LT.lt (α := ℕ) (↑a : ℕ) (↑b : ℕ)) (a = b)
        (LT.lt (α := ℕ) (↑b : ℕ) (↑a : ℕ)) Ordering.lt),
    Ordering.rec (motive := fun (x : Ordering) ↦ Prop) (LT.lt (α := ℕ) (↑a : ℕ) (↑b : ℕ)) (pos a = pos b)
      (LT.lt (α := ℕ) (↑b : ℕ) (↑a : ℕ)) Ordering.lt
eq :
  ∀
    (this :
      Ordering.rec (motive := fun (x : Ordering) ↦ Prop) (LT.lt (α := ℕ) (↑a : ℕ) (↑b : ℕ)) (a = b)
        (LT.lt (α := ℕ) (↑b : ℕ) (↑a : ℕ)) Ordering.eq),
    Ordering.rec (motive := fun (x : Ordering) ↦ Prop) (LT.lt (α := ℕ) (↑a : ℕ) (↑b : ℕ)) (pos a = pos b)
      (LT.lt (α := ℕ) (↑b : ℕ) (↑a : ℕ)) Ordering.eq
gt :
  ∀
    (this :
      Ordering.rec (motive := fun (x : Ordering) ↦ Prop) (LT.lt (α := ℕ) (↑a : ℕ) (↑b : ℕ)) (a = b)
        (LT.lt (α := ℕ) (↑b : ℕ) (↑a : ℕ)) Ordering.gt),
    Ordering.rec (motive := fun (x : Ordering) ↦ Prop) (LT.lt (α := ℕ) (↑a : ℕ) (↑b : ℕ)) (pos a = pos b)
      (LT.lt (α := ℕ) (↑b : ℕ) (↑a : ℕ)) Ordering.gt
⊢ ∀
    (this :
      Ordering.rec (motive := fun (x : Ordering) ↦ Prop) (LT.lt (α := ℕ) (↑a : ℕ) (↑b : ℕ)) (a = b)
        (LT.lt (α := ℕ) (↑b : ℕ) (↑a : ℕ)) (a.cmp b)),
    Ordering.rec (motive := fun (x : Ordering) ↦ Prop) (LT.lt (α := ℕ) (↑a : ℕ) (↑b : ℕ)) (pos a = pos b)
      (LT.lt (α := ℕ) (↑b : ℕ) (↑a : ℕ)) (a.cmp b)

Tactic:
cases PosNum.cmp a b

Premises used: PosNum.cmp
-- Module: Mathlib.Data.Num.Lemmas
Goal:
a b : PosNum
⊢ ∀
    (this :
      Ordering.rec (motive := fun (x : Ordering) ↦ Prop) (LT.lt (α := ℕ) (↑a : ℕ) (↑b : ℕ)) (a = b)
        (LT.lt (α := ℕ) (↑b : ℕ) (↑a : ℕ)) Ordering.lt),
    Ordering.rec (motive := fun (x : Ordering) ↦ Prop) (LT.lt (α := ℕ) (↑a : ℕ) (↑b : ℕ)) (pos a = pos b)
      (LT.lt (α := ℕ) (↑b : ℕ) (↑a : ℕ)) Ordering.lt

Tactic:
id

Premises used: id
-- Module: Mathlib.Data.Num.Lemmas
Goal:
a b : PosNum
⊢ ∀
    (this :
      Ordering.rec (motive := fun (x : Ordering) ↦ Prop) (LT.lt (α := ℕ) (↑a : ℕ) (↑b : ℕ)) (a = b)
        (LT.lt (α := ℕ) (↑b : ℕ) (↑a : ℕ)) Ordering.eq),
    Ordering.rec (motive := fun (x : Ordering) ↦ Prop) (LT.lt (α := ℕ) (↑a : ℕ) (↑b : ℕ)) (pos a = pos b)
      (LT.lt (α := ℕ) (↑b : ℕ) (↑a : ℕ)) Ordering.eq

Tactic:
congr_arg pos

Premises used: congr_arg, Num.pos
-- Module: Mathlib.Data.Num.Lemmas
Goal:
a b : PosNum
⊢ ∀
    (this :
      Ordering.rec (motive := fun (x : Ordering) ↦ Prop) (LT.lt (α := ℕ) (↑a : ℕ) (↑b : ℕ)) (a = b)
        (LT.lt (α := ℕ) (↑b : ℕ) (↑a : ℕ)) Ordering.gt),
    Ordering.rec (motive := fun (x : Ordering) ↦ Prop) (LT.lt (α := ℕ) (↑a : ℕ) (↑b : ℕ)) (pos a = pos b)
      (LT.lt (α := ℕ) (↑b : ℕ) (↑a : ℕ)) Ordering.gt

Tactic:
id

Premises used: id