awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Num.Lemmas
Goal:
α : Type u_1
⊢ DecidableLE PosNum

Tactic:
infer_instance
-- Module: Mathlib.Data.Num.Lemmas
Goal:
α : Type u_1
⊢ DecidableEq PosNum

Tactic:
infer_instance
-- Module: Mathlib.Data.Num.Lemmas
Goal:
α : Type u_1
⊢ DecidableLT PosNum

Tactic:
infer_instance
-- Module: Mathlib.Data.Num.Lemmas
Goal:
n : PosNum
rw : (↑(↑n : ℕ) : Num) = pos n
rw₁ rw₂ : Eq (α := Num) (↑(↑n : ℕ) : Num) (↑(↑n : ℕ) : Num)
⊢ (↑n : Num) = pos n

Tactic:
rw [← cast_to_nat, ← of_to_nat n]

Premises used: PosNum.of_to_nat, PosNum.cast_to_nat
-- Module: Mathlib.Data.Num.Lemmas
Goal:
b : Bool
n : PosNum
false : (↑(bit Bool.false n) : ℕ) = Nat.bit Bool.false (↑n : ℕ)
true : (↑(bit Bool.true n) : ℕ) = Nat.bit Bool.true (↑n : ℕ)
⊢ (↑(bit b n) : ℕ) = Nat.bit b (↑n : ℕ)

Tactic:
cases b
-- Module: Mathlib.Data.Num.Lemmas
Goal:
n : PosNum
⊢ (↑(bit false n) : ℕ) = Nat.bit false (↑n : ℕ)

Tactic:
simp [bit, two_mul]

Premises used: two_mul, PosNum.bit
-- Module: Mathlib.Data.Num.Lemmas
Goal:
n : PosNum
⊢ (↑(bit true n) : ℕ) = Nat.bit true (↑n : ℕ)

Tactic:
simp [bit, two_mul]

Premises used: two_mul, PosNum.bit
-- Module: Mathlib.Data.Num.Lemmas
Goal:
α : Type u_1
inst : AddMonoidWithOne α
m n : PosNum
rw : (↑(↑(m + n) : ℕ) : α) = HAdd.hAdd (α := α) (↑m : α) (↑n : α)
rw₁ : (↑(HAdd.hAdd (α := ℕ) (↑m : ℕ) (↑n : ℕ)) : α) = HAdd.hAdd (α := α) (↑m : α) (↑n : α)
rw₂ : HAdd.hAdd (α := α) (↑(↑m : ℕ) : α) (↑(↑n : ℕ) : α) = HAdd.hAdd (α := α) (↑m : α) (↑n : α)
rw₃ : HAdd.hAdd (α := α) (↑m : α) (↑(↑n : ℕ) : α) = HAdd.hAdd (α := α) (↑m : α) (↑n : α)
rw₄ rw₅ : HAdd.hAdd (α := α) (↑m : α) (↑n : α) = HAdd.hAdd (α := α) (↑m : α) (↑n : α)
⊢ (↑(m + n) : α) = HAdd.hAdd (α := α) (↑m : α) (↑n : α)

Tactic:
rw [← cast_to_nat, add_to_nat, Nat.cast_add, cast_to_nat, cast_to_nat]

Premises used: PosNum.cast_to_nat, Nat.cast_add, PosNum.add_to_nat
-- Module: Mathlib.Data.Num.Lemmas
Goal:
α : Type u_1
inst : AddMonoidWithOne α
n : PosNum
rw : (↑(n + 1) : α) = HAdd.hAdd (α := α) (↑n : α) 1
rw₁ : HAdd.hAdd (α := α) (↑n : α) (↑1 : α) = HAdd.hAdd (α := α) (↑n : α) 1
rw₂ rw₃ : HAdd.hAdd (α := α) (↑n : α) 1 = HAdd.hAdd (α := α) (↑n : α) 1
⊢ (↑n.succ : α) = HAdd.hAdd (α := α) (↑n : α) 1

Tactic:
rw [← add_one, cast_add, cast_one]

Premises used: PosNum.cast_one, PosNum.add_one, PosNum.cast_add
-- Module: Mathlib.Data.Num.Lemmas
Goal:
α : Type u_1
inst : AddMonoidWithOne α
inst_1 : CharZero α
m n : PosNum
rw : Eq.{u_1 + 1} (α := α) (↑(↑m : ℕ) : α) (↑n : α) ↔ m = n
rw₁ : Eq.{u_1 + 1} (α := α) (↑(↑m : ℕ) : α) (↑(↑n : ℕ) : α) ↔ m = n
rw₂ : Eq (α := ℕ) (↑m : ℕ) (↑n : ℕ) ↔ m = n
rw₃ rw₄ : m = n ↔ m = n
⊢ Eq.{u_1 + 1} (α := α) (↑m : α) (↑n : α) ↔ m = n

Tactic:
rw [← cast_to_nat m, ← cast_to_nat n, Nat.cast_inj, to_nat_inj]

Premises used: PosNum.to_nat_inj, Nat.cast_inj, PosNum.cast_to_nat
-- Module: Mathlib.Data.Num.Lemmas
Goal:
α : Type u_1
inst : Semiring α
inst_1 : PartialOrder α
inst_2 : IsStrictOrderedRing α
n : PosNum
rw : LE.le (α := ℕ) 1 (↑n : ℕ)
⊢ LE.le.{u_1} (α := α) 1 (↑n : α)

Tactic:
rw [← cast_to_nat, ← Nat.cast_one, Nat.cast_le (α := α)]

Premises used: PosNum.cast_to_nat, Nat.cast_le, Nat.cast_one
-- Module: Mathlib.Data.Num.Lemmas
Goal:
α : Type u_1
inst : Semiring α
inst_1 : PartialOrder α
inst_2 : IsStrictOrderedRing α
n : PosNum
⊢ LE.le (α := ℕ) 1 (↑n : ℕ)

Tactic:
apply to_nat_pos

Premises used: PosNum.to_nat_pos
-- Module: Mathlib.Data.Num.Lemmas
Goal:
α : Type u_1
inst : Semiring α
inst_1 : PartialOrder α
inst_2 : IsStrictOrderedRing α
n : PosNum
⊢ LT.lt.{u_1} (α := α) 0 (↑n : α)

Tactic:
lt_of_lt_of_le zero_lt_one (one_le_cast n)

Premises used: zero_lt_one, PosNum.one_le_cast, lt_of_lt_of_le
-- Module: Mathlib.Data.Num.Lemmas
Goal:
α : Type u_1
inst : NonAssocSemiring α
m n : PosNum
rw : (↑(↑(m * n) : ℕ) : α) = HMul.hMul (α := α) (↑m : α) (↑n : α)
rw₁ : (↑(HMul.hMul (α := ℕ) (↑m : ℕ) (↑n : ℕ)) : α) = HMul.hMul (α := α) (↑m : α) (↑n : α)
rw₂ : HMul.hMul (α := α) (↑(↑m : ℕ) : α) (↑(↑n : ℕ) : α) = HMul.hMul (α := α) (↑m : α) (↑n : α)
rw₃ : HMul.hMul (α := α) (↑m : α) (↑(↑n : ℕ) : α) = HMul.hMul (α := α) (↑m : α) (↑n : α)
rw₄ rw₅ : HMul.hMul (α := α) (↑m : α) (↑n : α) = HMul.hMul (α := α) (↑m : α) (↑n : α)
⊢ (↑(m * n) : α) = HMul.hMul (α := α) (↑m : α) (↑n : α)

Tactic:
rw [← cast_to_nat, mul_to_nat, Nat.cast_mul, cast_to_nat, cast_to_nat]

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

Tactic:
have := cmp_to_nat m n
-- Module: Mathlib.Data.Num.Lemmas
Goal:
m n : PosNum
this :
  Ordering.casesOn (motive := fun (x : Ordering) ↦ Prop) (m.cmp n) (LT.lt (α := ℕ) (↑m : ℕ) (↑n : ℕ)) (m = n)
    (LT.lt (α := ℕ) (↑n : ℕ) (↑m : ℕ))
⊢ Ordering.casesOn (motive := fun (x : Ordering) ↦ Prop) (m.cmp n) (m < n) (m = n) (n < m)

Tactic:
norm_cast at this
-- Module: Mathlib.Data.Num.Lemmas
Goal:
m n : PosNum
this : Ordering.casesOn (motive := fun (x : Ordering) ↦ Prop) (m.cmp n) (m < n) (m = n) (n < m)
revert :
  ∀ (this : Ordering.casesOn (motive := fun (x : Ordering) ↦ Prop) (m.cmp n) (m < n) (m = n) (n < m)),
    m.cmp n = Ordering.eq ↔ m = n
⊢ m.cmp n = Ordering.eq ↔ m = n

Tactic:
revert this
-- Module: Mathlib.Data.Num.Lemmas
Goal:
m n : PosNum
lt :
  ∀ (this : Ordering.casesOn (motive := fun (x : Ordering) ↦ Prop) Ordering.lt (m < n) (m = n) (n < m)),
    Ordering.lt = Ordering.eq ↔ m = n
eq :
  ∀ (this : Ordering.casesOn (motive := fun (x : Ordering) ↦ Prop) Ordering.eq (m < n) (m = n) (n < m)),
    Ordering.eq = Ordering.eq ↔ m = n
gt :
  ∀ (this : Ordering.casesOn (motive := fun (x : Ordering) ↦ Prop) Ordering.gt (m < n) (m = n) (n < m)),
    Ordering.gt = Ordering.eq ↔ m = n
⊢ ∀ (this : Ordering.casesOn (motive := fun (x : Ordering) ↦ Prop) (m.cmp n) (m < n) (m = n) (n < m)),
    m.cmp n = Ordering.eq ↔ m = n

Tactic:
cases cmp m n

Premises used: PosNum.cmp
-- Module: Mathlib.Data.Num.Lemmas
Goal:
m n : PosNum
⊢ ∀ (this : Ordering.casesOn (motive := fun (x : Ordering) ↦ Prop) Ordering.lt (m < n) (m = n) (n < m)),
    Ordering.lt = Ordering.eq ↔ m = n

Tactic:
simp_all [LT.lt.ne, LT.lt.ne']

Premises used: LT.lt.ne', LT.lt.ne
-- Module: Mathlib.Data.Num.Lemmas
Goal:
m n : PosNum
⊢ ∀ (this : Ordering.casesOn (motive := fun (x : Ordering) ↦ Prop) Ordering.eq (m < n) (m = n) (n < m)),
    Ordering.eq = Ordering.eq ↔ m = n

Tactic:
simp_all [LT.lt.ne, LT.lt.ne']

Premises used: LT.lt.ne', LT.lt.ne
-- Module: Mathlib.Data.Num.Lemmas
Goal:
m n : PosNum
⊢ ∀ (this : Ordering.casesOn (motive := fun (x : Ordering) ↦ Prop) Ordering.gt (m < n) (m = n) (n < m)),
    Ordering.gt = Ordering.eq ↔ m = n

Tactic:
simp_all [LT.lt.ne, LT.lt.ne']

Premises used: LT.lt.ne', LT.lt.ne
-- Module: Mathlib.Data.Num.Lemmas
Goal:
α : Type u_1
inst : Semiring α
inst_1 : PartialOrder α
inst_2 : IsStrictOrderedRing α
m n : PosNum
rw : LT.lt.{u_1} (α := α) (↑(↑m : ℕ) : α) (↑n : α) ↔ m < n
rw₁ : LT.lt.{u_1} (α := α) (↑(↑m : ℕ) : α) (↑(↑n : ℕ) : α) ↔ m < n
rw₂ : LT.lt (α := ℕ) (↑m : ℕ) (↑n : ℕ) ↔ m < n
rw₃ rw₄ : m < n ↔ m < n
⊢ LT.lt.{u_1} (α := α) (↑m : α) (↑n : α) ↔ m < n

Tactic:
rw [← cast_to_nat m, ← cast_to_nat n, Nat.cast_lt (α := α), lt_to_nat]

Premises used: PosNum.lt_to_nat, PosNum.cast_to_nat, Nat.cast_lt
-- Module: Mathlib.Data.Num.Lemmas
Goal:
α : Type u_1
inst : Semiring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
m n : PosNum
rw : ¬LT.lt.{u_1} (α := α) (↑n : α) (↑m : α) ↔ m ≤ n
⊢ LE.le.{u_1} (α := α) (↑m : α) (↑n : α) ↔ m ≤ n

Tactic:
rw [← not_lt]

Premises used: not_lt
-- Module: Mathlib.Data.Num.Lemmas
Goal:
α : Type u_1
inst : Semiring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
m n : PosNum
⊢ ¬LT.lt.{u_1} (α := α) (↑n : α) (↑m : α) ↔ m ≤ n

Tactic:
not_congr cast_lt

Premises used: not_congr, PosNum.cast_lt
-- Module: Mathlib.Data.Num.Lemmas
Goal:
α : Type u_1
inst : Semiring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
m n : PosNum
⊢ ¬LT.lt.{u_1} (α := α) (↑n : α) (↑m : α) ↔ m ≤ n

Tactic:
exact not_congr cast_lt

Premises used: not_congr, PosNum.cast_lt
-- Module: Mathlib.Data.Num.Lemmas
Goal:
b : Bool
n : Num
false : (↑(bit Bool.false n) : ℕ) = Nat.bit Bool.false (↑n : ℕ)
true : (↑(bit Bool.true n) : ℕ) = Nat.bit Bool.true (↑n : ℕ)
⊢ (↑(bit b n) : ℕ) = Nat.bit b (↑n : ℕ)

Tactic:
cases b
-- Module: Mathlib.Data.Num.Lemmas
Goal:
n : Num
false : (↑(bit Bool.false zero) : ℕ) = Nat.bit Bool.false (↑zero : ℕ)
false₁ : ∀ (a : PosNum), (↑(bit Bool.false (pos a)) : ℕ) = Nat.bit Bool.false (↑(pos a) : ℕ)
⊢ (↑(bit Bool.false n) : ℕ) = Nat.bit Bool.false (↑n : ℕ)

Tactic:
cases n
-- Module: Mathlib.Data.Num.Lemmas
Goal:
n : Num
true : (↑(bit Bool.true zero) : ℕ) = Nat.bit Bool.true (↑zero : ℕ)
true₁ : ∀ (a : PosNum), (↑(bit Bool.true (pos a)) : ℕ) = Nat.bit Bool.true (↑(pos a) : ℕ)
⊢ (↑(bit Bool.true n) : ℕ) = Nat.bit Bool.true (↑n : ℕ)

Tactic:
cases n
-- Module: Mathlib.Data.Num.Lemmas
Goal:
a : PosNum
false : (↑(pos a).bit0 : ℕ) = HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑a : ℕ)
⊢ (↑(bit Bool.false (pos a)) : ℕ) = Nat.bit Bool.false (↑(pos a) : ℕ)

Tactic:
simp [bit, two_mul]

Premises used: Num.bit, two_mul
-- Module: Mathlib.Data.Num.Lemmas
Goal:
a : PosNum
true : (↑(pos a).bit1 : ℕ) = (↑a : ℕ) + HAdd.hAdd (α := ℕ) (↑a : ℕ) 1
⊢ (↑(bit Bool.true (pos a)) : ℕ) = Nat.bit Bool.true (↑(pos a) : ℕ)

Tactic:
simp [bit, two_mul]

Premises used: Num.bit, two_mul
-- Module: Mathlib.Data.Num.Lemmas
Goal:
⊢ Eq (α := ℕ) (↑zero.bit0 : ℕ) 0

Tactic:
rfl
-- Module: Mathlib.Data.Num.Lemmas
Goal:
a : PosNum
⊢ (↑(pos a).bit0 : ℕ) = HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑a : ℕ)

Tactic:
rfl
-- Module: Mathlib.Data.Num.Lemmas
Goal:
⊢ Eq (α := ℕ) (↑zero.bit1 : ℕ) 1

Tactic:
rfl
-- Module: Mathlib.Data.Num.Lemmas
Goal:
a : PosNum
⊢ (↑(pos a).bit1 : ℕ) = (↑a : ℕ) + HAdd.hAdd (α := ℕ) (↑a : ℕ) 1

Tactic:
rfl
-- Module: Mathlib.Data.Num.Lemmas
Goal:
α : Type u_1
inst : AddMonoidWithOne α
n : Num
rw : (↑(↑n.succ' : ℕ) : α) = HAdd.hAdd (α := α) (↑n : α) 1
rw₁ : (↑(HAdd.hAdd (α := ℕ) (↑n : ℕ) 1) : α) = HAdd.hAdd (α := α) (↑n : α) 1
rw₂ : HAdd.hAdd (α := α) (↑(↑n : ℕ) : α) 1 = HAdd.hAdd (α := α) (↑n : α) 1
rw₃ rw₄ : HAdd.hAdd (α := α) (↑n : α) 1 = HAdd.hAdd (α := α) (↑n : α) 1
⊢ (↑n.succ' : α) = HAdd.hAdd (α := α) (↑n : α) 1

Tactic:
rw [← PosNum.cast_to_nat, succ'_to_nat, Nat.cast_add_one, cast_to_nat]

Premises used: Num.succ'_to_nat, Num.cast_to_nat, PosNum.cast_to_nat, Nat.cast_add_one
-- Module: Mathlib.Data.Num.Lemmas
Goal:
α : Type u_1
inst : AddMonoidWithOne α
n : Num
⊢ (↑n.succ : α) = HAdd.hAdd (α := α) (↑n : α) 1

Tactic:
cast_succ' n

Premises used: castNum, Num.cast_succ'
-- Module: Mathlib.Data.Num.Lemmas
Goal:
α : Type u_1
inst : AddMonoidWithOne α
m n : Num
rw : (↑(↑(m + n) : ℕ) : α) = HAdd.hAdd (α := α) (↑m : α) (↑n : α)
rw₁ : (↑(HAdd.hAdd (α := ℕ) (↑m : ℕ) (↑n : ℕ)) : α) = HAdd.hAdd (α := α) (↑m : α) (↑n : α)
rw₂ : HAdd.hAdd (α := α) (↑(↑m : ℕ) : α) (↑(↑n : ℕ) : α) = HAdd.hAdd (α := α) (↑m : α) (↑n : α)
rw₃ : HAdd.hAdd (α := α) (↑m : α) (↑(↑n : ℕ) : α) = HAdd.hAdd (α := α) (↑m : α) (↑n : α)
rw₄ rw₅ : HAdd.hAdd (α := α) (↑m : α) (↑n : α) = HAdd.hAdd (α := α) (↑m : α) (↑n : α)
⊢ (↑(m + n) : α) = HAdd.hAdd (α := α) (↑m : α) (↑n : α)

Tactic:
rw [← cast_to_nat, add_to_nat, Nat.cast_add, cast_to_nat, cast_to_nat]

Premises used: Num.cast_to_nat, Nat.cast_add, Num.add_to_nat
-- Module: Mathlib.Data.Num.Lemmas
Goal:
α : Type u_1
inst : NonAssocSemiring α
n : Num
rw : (↑(n + n) : α) = HMul.hMul (α := α) 2 (↑n : α)
rw₁ : (↑(n + n) : α) = HAdd.hAdd (α := α) (↑n : α) (↑n : α)
rw₂ rw₃ : HAdd.hAdd (α := α) (↑n : α) (↑n : α) = HAdd.hAdd (α := α) (↑n : α) (↑n : α)
⊢ (↑n.bit0 : α) = HMul.hMul (α := α) 2 (↑n : α)

Tactic:
rw [← bit0_of_bit0, two_mul, cast_add]

Premises used: two_mul, Num.bit0_of_bit0, Num.cast_add
-- Module: Mathlib.Data.Num.Lemmas
Goal:
α : Type u_1
inst : NonAssocSemiring α
n : Num
rw : HMul.hMul (α := α) 2 (↑n : α) + (↑1 : α) = HMul.hMul (α := α) 2 (↑n : α) + 1
⊢ (↑n.bit1 : α) = HMul.hMul (α := α) 2 (↑n : α) + 1

Tactic:
rw [← bit1_of_bit1, bit0_of_bit0, cast_add, cast_bit0]

Premises used: Num.bit1_of_bit1, Num.cast_bit0, Num.bit0_of_bit0, Num.cast_add
-- Module: Mathlib.Data.Num.Lemmas
Goal:
α : Type u_1
inst : NonAssocSemiring α
n : Num
⊢ HMul.hMul (α := α) 2 (↑n : α) + (↑1 : α) = HMul.hMul (α := α) 2 (↑n : α) + 1

Tactic:
rfl
-- Module: Mathlib.Data.Num.Lemmas
Goal:
n : Num
rw : (↑n.size : ℕ) = Nat.size (↑n : ℕ)
rw₁ rw₂ : Nat.size (↑n : ℕ) = Nat.size (↑n : ℕ)
⊢ n.natSize = Nat.size (↑n : ℕ)

Tactic:
rw [← size_eq_natSize, size_to_nat]

Premises used: Num.size_to_nat, Num.size_eq_natSize
-- Module: Mathlib.Data.Num.Lemmas
Goal:
⊢ ofNat' 0 = (↑0 : Num)

Tactic:
simp
-- Module: Mathlib.Data.Num.Lemmas
Goal:
b : Bool
n : ℕ
IH : ofNat' n = (↑n : Num)
⊢ ofNat' (Nat.bit b n) = (↑(Nat.bit b n) : Num)

Tactic:
tauto
-- Module: Mathlib.Data.Num.Lemmas
Goal:
n : Num
zero : -Num.zero.toZNum = Num.zero.toZNumNeg
pos : ∀ (a : PosNum), -(Num.pos a).toZNum = (Num.pos a).toZNumNeg
⊢ -n.toZNum = n.toZNumNeg

Tactic:
cases n
-- Module: Mathlib.Data.Num.Lemmas
Goal:
⊢ -zero.toZNum = zero.toZNumNeg

Tactic:
rfl
-- Module: Mathlib.Data.Num.Lemmas
Goal:
a : PosNum
⊢ -(pos a).toZNum = (pos a).toZNumNeg

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

Tactic:
cases n
-- Module: Mathlib.Data.Num.Lemmas
Goal:
⊢ -zero.toZNumNeg = zero.toZNum

Tactic:
rfl
-- Module: Mathlib.Data.Num.Lemmas
Goal:
a : PosNum
⊢ -(pos a).toZNumNeg = (pos a).toZNum

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

Tactic:
cases m
-- Module: Mathlib.Data.Num.Lemmas
Goal:
n : Num
h : Num.zero.toZNum = n.toZNum
zero : ∀ (h : Num.zero.toZNum = Num.zero.toZNum), Num.zero = Num.zero
zero₁ : ∀ (a : PosNum) (h : Num.zero.toZNum = (pos a).toZNum), Num.zero = pos a
⊢ Num.zero = n

Tactic:
cases n
-- Module: Mathlib.Data.Num.Lemmas
Goal:
n : Num
a : PosNum
h : (Num.pos a).toZNum = n.toZNum
pos : ∀ (h : (Num.pos a).toZNum = zero.toZNum), Num.pos a = zero
pos₁ : ∀ (a_1 : PosNum) (h : (Num.pos a).toZNum = (Num.pos a_1).toZNum), Num.pos a = Num.pos a_1
⊢ Num.pos a = n

Tactic:
cases n
-- Module: Mathlib.Data.Num.Lemmas
Goal:
a : PosNum
h : zero.toZNum = (pos a).toZNum
⊢ zero = pos a

Tactic:
cases h
-- Module: Mathlib.Data.Num.Lemmas
Goal:
a : PosNum
h : (pos a).toZNum = zero.toZNum
⊢ pos a = zero

Tactic:
cases h
-- Module: Mathlib.Data.Num.Lemmas
Goal:
a a_1 : PosNum
h : (Num.pos a).toZNum = (Num.pos a_1).toZNum
pos : Num.pos a = Num.pos a
⊢ Num.pos a = Num.pos a_1

Tactic:
cases h
-- Module: Mathlib.Data.Num.Lemmas
Goal:
⊢ zero = zero

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

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

Tactic:
cases m
-- Module: Mathlib.Data.Num.Lemmas
Goal:
n : Num
zero : (Num.zero + Num.zero).toZNum = Num.zero.toZNum + Num.zero.toZNum
zero₁ : ∀ (a : PosNum), (Num.zero + pos a).toZNum = Num.zero.toZNum + (pos a).toZNum
⊢ (Num.zero + n).toZNum = Num.zero.toZNum + n.toZNum

Tactic:
cases n
-- Module: Mathlib.Data.Num.Lemmas
Goal:
n : Num
a : PosNum
pos : (Num.pos a + zero).toZNum = (Num.pos a).toZNum + zero.toZNum
pos₁ : ∀ (a_1 : PosNum), (Num.pos a + Num.pos a_1).toZNum = (Num.pos a).toZNum + (Num.pos a_1).toZNum
⊢ (Num.pos a + n).toZNum = (Num.pos a).toZNum + n.toZNum

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

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

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

Tactic:
rfl
-- Module: Mathlib.Data.Num.Lemmas
Goal:
a a_1 : PosNum
⊢ (pos a + pos a_1).toZNum = (pos a).toZNum + (pos a_1).toZNum

Tactic:
rfl
-- Module: Mathlib.Data.Num.Lemmas
Goal:
n : PosNum
h : 1 < n
unfold : (↑(Num.casesOn (motive := fun (x : Num) ↦ PosNum) n.pred' 1 id) : ℕ) = Nat.pred (↑n : ℕ)
⊢ (↑n.pred : ℕ) = Nat.pred (↑n : ℕ)

Tactic:
unfold pred

Premises used: PosNum.pred
-- Module: Mathlib.Data.Num.Lemmas
Goal:
n : PosNum
h : 1 < n
zero :
  ∀ (e : n.pred' = Num.zero), (↑(Num.casesOn (motive := fun (x : Num) ↦ PosNum) Num.zero 1 id) : ℕ) = Nat.pred (↑n : ℕ)
pos :
  ∀ (a : PosNum) (e : n.pred' = Num.pos a),
    (↑(Num.casesOn (motive := fun (x : Num) ↦ PosNum) (Num.pos a) 1 id) : ℕ) = Nat.pred (↑n : ℕ)
⊢ (↑(Num.casesOn (motive := fun (x : Num) ↦ PosNum) n.pred' 1 id) : ℕ) = Nat.pred (↑n : ℕ)

Tactic:
cases e : pred' n

Premises used: PosNum.pred'
-- Module: Mathlib.Data.Num.Lemmas
Goal:
n : PosNum
h : 1 < n
e : n.pred' = zero
⊢ 1 ≤ Nat.pred (↑n : ℕ)

Tactic:
have : (1 : ℕ) ≤ Nat.pred n := Nat.pred_le_pred ((@cast_lt ℕ _ _ _).2 h)
-- Module: Mathlib.Data.Num.Lemmas
Goal:
n : PosNum
h : 1 < n
e : n.pred' = zero
this : 1 ≤ Nat.pred (↑n : ℕ)
⊢ LE.le (α := ℕ) 1 (↑zero : ℕ)

Tactic:
rw [← pred'_to_nat, e] at this

Premises used: PosNum.pred'_to_nat
-- Module: Mathlib.Data.Num.Lemmas
Goal:
n : PosNum
h : 1 < n
e : n.pred' = zero
this : LE.le (α := ℕ) 1 (↑zero : ℕ)
⊢ ¬LE.le (α := ℕ) 1 (↑zero : ℕ)

Tactic:
decide
-- Module: Mathlib.Data.Num.Lemmas
Goal:
n : PosNum
h : 1 < n
e : n.pred' = zero
this : LE.le (α := ℕ) 1 (↑zero : ℕ)
⊢ (↑(Num.casesOn (motive := fun (x : Num) ↦ PosNum) zero 1 id) : ℕ) = Nat.pred (↑n : ℕ)

Tactic:
exact absurd this (by decide)

Premises used: absurd
-- Module: Mathlib.Data.Num.Lemmas
Goal:
n : PosNum
h : 1 < n
a : PosNum
e : n.pred' = Num.pos a
pos : Eq (α := ℕ) (↑(Num.casesOn (motive := fun (x : Num) ↦ PosNum) (Num.pos a) 1 id) : ℕ) (↑(Num.pos a) : ℕ)
⊢ (↑(Num.casesOn (motive := fun (x : Num) ↦ PosNum) (Num.pos a) 1 id) : ℕ) = Nat.pred (↑n : ℕ)

Tactic:
rw [← pred'_to_nat, e]

Premises used: PosNum.pred'_to_nat
-- Module: Mathlib.Data.Num.Lemmas
Goal:
n : PosNum
h : 1 < n
a : PosNum
e : n.pred' = pos a
⊢ Eq (α := ℕ) (↑(Num.casesOn (motive := fun (x : Num) ↦ PosNum) (pos a) 1 id) : ℕ) (↑(pos a) : ℕ)

Tactic:
rfl
-- Module: Mathlib.Data.Num.Lemmas
Goal:
a : PosNum
one : PosNum.one.sub' 1 = PosNum.one.pred'.toZNum
bit1 : ∀ (a : PosNum), a.bit1.sub' 1 = a.bit1.pred'.toZNum
bit0 : ∀ (a : PosNum), a.bit0.sub' 1 = a.bit0.pred'.toZNum
⊢ a.sub' 1 = a.pred'.toZNum

Tactic:
cases a
-- Module: Mathlib.Data.Num.Lemmas
Goal:
⊢ one.sub' 1 = one.pred'.toZNum

Tactic:
rfl
-- Module: Mathlib.Data.Num.Lemmas
Goal:
a : PosNum
⊢ a.bit1.sub' 1 = a.bit1.pred'.toZNum

Tactic:
rfl
-- Module: Mathlib.Data.Num.Lemmas
Goal:
a : PosNum
⊢ a.bit0.sub' 1 = a.bit0.pred'.toZNum

Tactic:
rfl
-- Module: Mathlib.Data.Num.Lemmas
Goal:
a : PosNum
one : sub' 1 PosNum.one = PosNum.one.pred'.toZNumNeg
bit1 : ∀ (a : PosNum), sub' 1 a.bit1 = a.bit1.pred'.toZNumNeg
bit0 : ∀ (a : PosNum), sub' 1 a.bit0 = a.bit0.pred'.toZNumNeg
⊢ sub' 1 a = a.pred'.toZNumNeg

Tactic:
cases a
-- Module: Mathlib.Data.Num.Lemmas
Goal:
⊢ sub' 1 one = one.pred'.toZNumNeg

Tactic:
rfl
-- Module: Mathlib.Data.Num.Lemmas
Goal:
a : PosNum
⊢ sub' 1 a.bit1 = a.bit1.pred'.toZNumNeg

Tactic:
rfl
-- Module: Mathlib.Data.Num.Lemmas
Goal:
a : PosNum
⊢ sub' 1 a.bit0 = a.bit0.pred'.toZNumNeg

Tactic:
rfl
-- Module: Mathlib.Data.Num.Lemmas
Goal:
m n : PosNum
⊢ m < n ↔ m.cmp n = Ordering.lt

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Data.Num.Lemmas
Goal:
m n : PosNum
rw : (m.cmp n).swap = Ordering.lt ↔ m.cmp n = Ordering.gt
⊢ n.cmp m = Ordering.lt ↔ m.cmp n = Ordering.gt

Tactic:
rw [← cmp_swap]

Premises used: PosNum.cmp_swap
-- Module: Mathlib.Data.Num.Lemmas
Goal:
m n : PosNum
lt : Ordering.lt.swap = Ordering.lt ↔ Ordering.lt = Ordering.gt
eq : Ordering.eq.swap = Ordering.lt ↔ Ordering.eq = Ordering.gt
gt : Ordering.gt.swap = Ordering.lt ↔ Ordering.gt = Ordering.gt
⊢ (m.cmp n).swap = Ordering.lt ↔ m.cmp n = Ordering.gt

Tactic:
cases cmp m n

Premises used: PosNum.cmp
-- Module: Mathlib.Data.Num.Lemmas
Goal:
m n : PosNum
⊢ Ordering.lt.swap = Ordering.lt ↔ Ordering.lt = Ordering.gt

Tactic:
decide
-- Module: Mathlib.Data.Num.Lemmas
Goal:
m n : PosNum
⊢ Ordering.eq.swap = Ordering.lt ↔ Ordering.eq = Ordering.gt

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

Tactic:
decide
-- Module: Mathlib.Data.Num.Lemmas
Goal:
p : PosNum
rw : Nat.pred (↑p : ℕ) = Nat.pred (↑(pos p) : ℕ)
⊢ (↑(pos p).pred : ℕ) = Nat.pred (↑(pos p) : ℕ)

Tactic:
rw [pred, PosNum.pred'_to_nat]

Premises used: PosNum.pred'_to_nat, Num.pred
-- Module: Mathlib.Data.Num.Lemmas
Goal:
p : PosNum
⊢ Nat.pred (↑p : ℕ) = Nat.pred (↑(pos p) : ℕ)

Tactic:
rfl
-- Module: Mathlib.Data.Num.Lemmas
Goal:
p : PosNum
rw : Nat.succ (↑p.pred' : ℕ) = (↑(pos p) : ℕ)
⊢ castNum <$> (pos p).ppred = Nat.ppred (↑(pos p) : ℕ)

Tactic:
rw [ppred, Option.map_eq_map, Option.map_some, Nat.ppred_eq_some.2]

Premises used: Iff.mpr, Nat.ppred_eq_some, Option.map_some, Option.map_eq_map, Num.ppred
-- Module: Mathlib.Data.Num.Lemmas
Goal:
p : PosNum
rw : Eq (α := ℕ) (↑p : ℕ) (↑(pos p) : ℕ)
⊢ Nat.succ (↑p.pred' : ℕ) = (↑(pos p) : ℕ)

Tactic:
rw [PosNum.pred'_to_nat, Nat.succ_pred_eq_of_pos (PosNum.to_nat_pos _)]

Premises used: Nat.succ_pred_eq_of_pos, PosNum.to_nat_pos, PosNum.pred'_to_nat
-- Module: Mathlib.Data.Num.Lemmas
Goal:
p : PosNum
⊢ Eq (α := ℕ) (↑p : ℕ) (↑(pos p) : ℕ)

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

Tactic:
cases m
-- Module: Mathlib.Data.Num.Lemmas
Goal:
n : Num
zero : (Num.zero.cmp Num.zero).swap = Num.zero.cmp Num.zero
zero₁ : ∀ (a : PosNum), (Num.zero.cmp (pos a)).swap = (pos a).cmp Num.zero
⊢ (Num.zero.cmp n).swap = n.cmp Num.zero

Tactic:
cases n
-- Module: Mathlib.Data.Num.Lemmas
Goal:
n : Num
a : PosNum
pos : ((Num.pos a).cmp zero).swap = zero.cmp (Num.pos a)
pos₁ : ∀ (a_1 : PosNum), ((Num.pos a).cmp (Num.pos a_1)).swap = (Num.pos a_1).cmp (Num.pos a)
⊢ ((Num.pos a).cmp n).swap = n.cmp (Num.pos a)

Tactic:
cases n
-- Module: Mathlib.Data.Num.Lemmas
Goal:
⊢ (zero.cmp zero).swap = zero.cmp zero

Tactic:
rfl
-- Module: Mathlib.Data.Num.Lemmas
Goal:
⊢ (zero.cmp zero).swap = zero.cmp zero

Tactic:
{ rfl }
-- Module: Mathlib.Data.Num.Lemmas
Goal:
⊢ (zero.cmp zero).swap = zero.cmp zero

Tactic:
try { rfl }
-- Module: Mathlib.Data.Num.Lemmas
Goal:
a : PosNum
⊢ (zero.cmp (pos a)).swap = (pos a).cmp zero

Tactic:
rfl
-- Module: Mathlib.Data.Num.Lemmas
Goal:
a : PosNum
⊢ (zero.cmp (pos a)).swap = (pos a).cmp zero

Tactic:
{ rfl }
-- Module: Mathlib.Data.Num.Lemmas
Goal:
a : PosNum
⊢ (zero.cmp (pos a)).swap = (pos a).cmp zero

Tactic:
try { rfl }
-- Module: Mathlib.Data.Num.Lemmas
Goal:
a : PosNum
⊢ ((pos a).cmp zero).swap = zero.cmp (pos a)

Tactic:
rfl
-- Module: Mathlib.Data.Num.Lemmas
Goal:
a : PosNum
⊢ ((pos a).cmp zero).swap = zero.cmp (pos a)

Tactic:
{ rfl }
-- Module: Mathlib.Data.Num.Lemmas
Goal:
a : PosNum
⊢ ((pos a).cmp zero).swap = zero.cmp (pos a)

Tactic:
try { rfl }
-- Module: Mathlib.Data.Num.Lemmas
Goal:
a a_1 : PosNum
⊢ ((pos a).cmp (pos a_1)).swap = (pos a_1).cmp (pos a)

Tactic:
apply PosNum.cmp_swap

Premises used: PosNum.cmp_swap
-- Module: Mathlib.Data.Num.Lemmas
Goal:
m n : Num
⊢ Ordering.casesOn (motive := fun (x : Ordering) ↦ Prop) (m.cmp n) (LT.lt (α := ℕ) (↑m : ℕ) (↑n : ℕ)) (m = n)
    (LT.lt (α := ℕ) (↑n : ℕ) (↑m : ℕ))

Tactic:
have := cmp_to_nat m n
-- Module: Mathlib.Data.Num.Lemmas
Goal:
m n : Num
this :
  Ordering.casesOn (motive := fun (x : Ordering) ↦ Prop) (m.cmp n) (LT.lt (α := ℕ) (↑m : ℕ) (↑n : ℕ)) (m = n)
    (LT.lt (α := ℕ) (↑n : ℕ) (↑m : ℕ))
⊢ Ordering.casesOn (motive := fun (x : Ordering) ↦ Prop) (m.cmp n) (m < n) (m = n) (n < m)

Tactic:
norm_cast at this
-- Module: Mathlib.Data.Num.Lemmas
Goal:
m n : Num
this : Ordering.casesOn (motive := fun (x : Ordering) ↦ Prop) (m.cmp n) (m < n) (m = n) (n < m)
revert :
  ∀ (this : Ordering.casesOn (motive := fun (x : Ordering) ↦ Prop) (m.cmp n) (m < n) (m = n) (n < m)),
    m.cmp n = Ordering.eq ↔ m = n
⊢ m.cmp n = Ordering.eq ↔ m = n

Tactic:
revert this