awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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:
exacts [id, congr_arg pos, id]

Premises used: id, congr_arg, Num.pos
-- Module: Mathlib.Data.Num.Lemmas
Goal:
m n : Num
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 : Num
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 : Num
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 : Num
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 : Num
⊢ ¬LT.lt (α := ℕ) (↑n : ℕ) (↑m : ℕ) ↔ m ≤ n

Tactic:
not_congr lt_to_nat

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

Tactic:
exact not_congr lt_to_nat

Premises used: Num.lt_to_nat, not_congr
-- Module: Mathlib.Data.Num.Lemmas
Goal:
⊢ 1 = Num.pos 1

Tactic:
norm_cast
-- Module: Mathlib.Data.Num.Lemmas
Goal:
p : PosNum
⊢ Num.ofNat' (↑p.bit0 : ℕ) = Num.pos p.bit0

Tactic:
simpa only [Nat.bit_false, cond_false, two_mul, of_to_nat' p] using Num.ofNat'_bit false p

Premises used: castPosNum, two_mul, Num.ofNat'_bit, Nat.bit_false, Bool.false, cond_false
-- Module: Mathlib.Data.Num.Lemmas
Goal:
p : PosNum
⊢ Num.ofNat' (↑p.bit1 : ℕ) = Num.pos p.bit1

Tactic:
simpa only [Nat.bit_true, cond_true, two_mul, of_to_nat' p] using Num.ofNat'_bit true p

Premises used: castPosNum, Nat.bit_true, two_mul, cond_true, Num.ofNat'_bit, Bool.true
-- Module: Mathlib.Data.Num.Lemmas
Goal:
⊢ Function.Injective (β := ℕ) castNum

Tactic:
Function.LeftInverse.injective of_to_nat'

Premises used: Function.LeftInverse.injective, Num.of_to_nat'
-- Module: Mathlib.Data.Num.Lemmas
Goal:
m n : Num
⊢ Eq (α := ℕ) (↑m : ℕ) (↑n : ℕ) ↔ m = n

Tactic:
toNat_injective.eq_iff

Premises used: Num.toNat_injective, Function.Injective.eq_iff
-- Module: Mathlib.Data.Num.Lemmas
Goal:
transfer transfer₁ : ∀ (a b c : Num), a + b + c = a + (b + c)
transfer₂ transfer₃ :
  ∀ (a b c : Num), HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑b : ℕ) + (↑c : ℕ) = (↑a : ℕ) + HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑c : ℕ)
⊢ ∀ (a b c : Num), a + b + c = a + (b + c)

Tactic:
transfer
-- Module: Mathlib.Data.Num.Lemmas
Goal:
x x_1 : Num
simp_rw : Eq (α := ℕ) (↑(x + x_1) : ℕ) (↑(x_1 + x) : ℕ)
simp_rw₁ : HAdd.hAdd (α := ℕ) (↑x : ℕ) (↑x_1 : ℕ) = HAdd.hAdd (α := ℕ) (↑x_1 : ℕ) (↑x : ℕ)
⊢ x + x_1 = x_1 + x

Tactic:
simp_rw [← to_nat_inj, add_to_nat, add_comm]

Premises used: add_comm, Num.to_nat_inj, Num.add_to_nat
-- Module: Mathlib.Data.Num.Lemmas
Goal:
x x_1 x_2 : Num
simp_rw : Eq (α := ℕ) (↑(x * x_1 * x_2) : ℕ) (↑(x * (x_1 * x_2)) : ℕ)
simp_rw₁ : HMul.hMul (α := ℕ) (↑x : ℕ) (↑x_1 : ℕ) * (↑x_2 : ℕ) = (↑x : ℕ) * HMul.hMul (α := ℕ) (↑x_1 : ℕ) (↑x_2 : ℕ)
⊢ x * x_1 * x_2 = x * (x_1 * x_2)

Tactic:
simp_rw [← to_nat_inj, mul_to_nat, mul_assoc]

Premises used: mul_assoc, Num.to_nat_inj, Num.mul_to_nat
-- Module: Mathlib.Data.Num.Lemmas
Goal:
x : Num
rw : Eq (α := ℕ) (↑(1 * x) : ℕ) (↑x : ℕ)
rw₁ : HMul.hMul (α := ℕ) (↑1 : ℕ) (↑x : ℕ) = (↑x : ℕ)
rw₂ : HMul.hMul (α := ℕ) 1 (↑x : ℕ) = (↑x : ℕ)
rw₃ rw₄ : Eq (α := ℕ) (↑x : ℕ) (↑x : ℕ)
⊢ 1 * x = x

Tactic:
rw [← to_nat_inj, mul_to_nat, cast_one, one_mul]

Premises used: Num.cast_one, Num.to_nat_inj, Num.mul_to_nat, one_mul
-- Module: Mathlib.Data.Num.Lemmas
Goal:
x : Num
rw : Eq (α := ℕ) (↑(x * 1) : ℕ) (↑x : ℕ)
rw₁ : HMul.hMul (α := ℕ) (↑x : ℕ) (↑1 : ℕ) = (↑x : ℕ)
rw₂ : HMul.hMul (α := ℕ) (↑x : ℕ) 1 = (↑x : ℕ)
rw₃ rw₄ : Eq (α := ℕ) (↑x : ℕ) (↑x : ℕ)
⊢ x * 1 = x

Tactic:
rw [← to_nat_inj, mul_to_nat, cast_one, mul_one]

Premises used: Num.cast_one, mul_one, Num.to_nat_inj, Num.mul_to_nat
-- Module: Mathlib.Data.Num.Lemmas
Goal:
x : Num
rw : Eq (α := ℕ) (↑(0 * x) : ℕ) (↑0 : ℕ)
rw₁ : HMul.hMul (α := ℕ) (↑0 : ℕ) (↑x : ℕ) = (↑0 : ℕ)
rw₂ : HMul.hMul (α := ℕ) 0 (↑x : ℕ) = 0
rw₃ rw₄ : Eq (α := ℕ) 0 0
⊢ 0 * x = 0

Tactic:
rw [← to_nat_inj, mul_to_nat, cast_zero, zero_mul]

Premises used: Num.cast_zero, MulZeroClass.zero_mul, Num.to_nat_inj, Num.mul_to_nat
-- Module: Mathlib.Data.Num.Lemmas
Goal:
x : Num
rw : Eq (α := ℕ) (↑(x * 0) : ℕ) (↑0 : ℕ)
rw₁ : HMul.hMul (α := ℕ) (↑x : ℕ) (↑0 : ℕ) = (↑0 : ℕ)
rw₂ : HMul.hMul (α := ℕ) (↑x : ℕ) 0 = 0
rw₃ rw₄ : Eq (α := ℕ) 0 0
⊢ x * 0 = 0

Tactic:
rw [← to_nat_inj, mul_to_nat, cast_zero, mul_zero]

Premises used: Num.cast_zero, MulZeroClass.mul_zero, Num.to_nat_inj, Num.mul_to_nat
-- Module: Mathlib.Data.Num.Lemmas
Goal:
x x_1 x_2 : Num
⊢ x * (x_1 + x_2) = x * x_1 + x * x_2

Tactic:
simp only [← to_nat_inj, mul_to_nat, add_to_nat, mul_add]

Premises used: mul_add, Num.to_nat_inj, Num.mul_to_nat, Num.add_to_nat
-- Module: Mathlib.Data.Num.Lemmas
Goal:
x x_1 x_2 : Num
⊢ (x + x_1) * x_2 = x * x_2 + x_1 * x_2

Tactic:
simp only [← to_nat_inj, mul_to_nat, add_to_nat, add_mul]

Premises used: add_mul, Num.to_nat_inj, Num.mul_to_nat, Num.add_to_nat
-- Module: Mathlib.Data.Num.Lemmas
Goal:
x x_1 : Num
simp_rw : Eq (α := ℕ) (↑(x * x_1) : ℕ) (↑(x_1 * x) : ℕ)
simp_rw₁ : HMul.hMul (α := ℕ) (↑x : ℕ) (↑x_1 : ℕ) = HMul.hMul (α := ℕ) (↑x_1 : ℕ) (↑x : ℕ)
⊢ x * x_1 = x_1 * x

Tactic:
simp_rw [← to_nat_inj, mul_to_nat, mul_comm]

Premises used: mul_comm, Num.to_nat_inj, Num.mul_to_nat
-- Module: Mathlib.Data.Num.Lemmas
Goal:
transfer transfer₁ : ∀ (a : Num), a ≤ a
⊢ ∀ (a : Num), a ≤ a

Tactic:
transfer
-- Module: Mathlib.Data.Num.Lemmas
Goal:
a b c : Num
transfer_rw : LE.le (α := ℕ) (↑a : ℕ) (↑b : ℕ) → LE.le (α := ℕ) (↑b : ℕ) (↑c : ℕ) → LE.le (α := ℕ) (↑a : ℕ) (↑c : ℕ)
⊢ a ≤ b → b ≤ c → a ≤ c

Tactic:
transfer_rw
-- Module: Mathlib.Data.Num.Lemmas
Goal:
a b c : Num
⊢ LE.le (α := ℕ) (↑a : ℕ) (↑b : ℕ) → LE.le (α := ℕ) (↑b : ℕ) (↑c : ℕ) → LE.le (α := ℕ) (↑a : ℕ) (↑c : ℕ)

Tactic:
apply le_trans

Premises used: le_trans
-- Module: Mathlib.Data.Num.Lemmas
Goal:
a b : Num
⊢ a < b ↔ a ≤ b ∧ ¬b ≤ a

Tactic:
simp only [← lt_to_nat, ← le_to_nat, lt_iff_le_not_ge]

Premises used: lt_iff_le_not_ge, Num.lt_to_nat, Num.le_to_nat
-- Module: Mathlib.Data.Num.Lemmas
Goal:
a b : Num
transfer_rw : LE.le (α := ℕ) (↑a : ℕ) (↑b : ℕ) → LE.le (α := ℕ) (↑b : ℕ) (↑a : ℕ) → Eq (α := ℕ) (↑a : ℕ) (↑b : ℕ)
⊢ a ≤ b → b ≤ a → a = b

Tactic:
transfer_rw
-- Module: Mathlib.Data.Num.Lemmas
Goal:
a b : Num
⊢ LE.le (α := ℕ) (↑a : ℕ) (↑b : ℕ) → LE.le (α := ℕ) (↑b : ℕ) (↑a : ℕ) → Eq (α := ℕ) (↑a : ℕ) (↑b : ℕ)

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.Data.Num.Lemmas
Goal:
a b : Num
h : a ≤ b
c : Num
revert : ∀ (h : a ≤ b), a + c ≤ b + c
⊢ a + c ≤ b + c

Tactic:
revert h
-- Module: Mathlib.Data.Num.Lemmas
Goal:
a b c : Num
transfer_rw :
  ∀ (h : LE.le (α := ℕ) (↑a : ℕ) (↑b : ℕ)), HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑c : ℕ) ≤ HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑c : ℕ)
⊢ ∀ (h : a ≤ b), a + c ≤ b + c

Tactic:
transfer_rw
-- Module: Mathlib.Data.Num.Lemmas
Goal:
a b c : Num
⊢ ∀ (h : LE.le (α := ℕ) (↑a : ℕ) (↑b : ℕ)), HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑c : ℕ) ≤ HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑c : ℕ)

Tactic:
fun h => add_le_add_left h c

Premises used: add_le_add_left, castNum
-- Module: Mathlib.Data.Num.Lemmas
Goal:
a b c : Num
⊢ ∀ (h : LE.le (α := ℕ) (↑a : ℕ) (↑b : ℕ)), HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑c : ℕ) ≤ HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑c : ℕ)

Tactic:
exact fun h => add_le_add_left h c

Premises used: add_le_add_left
-- Module: Mathlib.Data.Num.Lemmas
Goal:
a b c : Num
transfer_rw :
  HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑b : ℕ) ≤ HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑c : ℕ) → LE.le (α := ℕ) (↑b : ℕ) (↑c : ℕ)
⊢ a + b ≤ a + c → b ≤ c

Tactic:
transfer_rw
-- Module: Mathlib.Data.Num.Lemmas
Goal:
a b c : Num
⊢ HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑b : ℕ) ≤ HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑c : ℕ) → LE.le (α := ℕ) (↑b : ℕ) (↑c : ℕ)

Tactic:
apply le_of_add_le_add_left

Premises used: le_of_add_le_add_left
-- Module: Mathlib.Data.Num.Lemmas
Goal:
a b : Num
transfer_rw : LE.le (α := ℕ) (↑a : ℕ) (↑b : ℕ) ∨ LE.le (α := ℕ) (↑b : ℕ) (↑a : ℕ)
⊢ a ≤ b ∨ b ≤ a

Tactic:
transfer_rw
-- Module: Mathlib.Data.Num.Lemmas
Goal:
a b : Num
⊢ LE.le (α := ℕ) (↑a : ℕ) (↑b : ℕ) ∨ LE.le (α := ℕ) (↑b : ℕ) (↑a : ℕ)

Tactic:
apply le_total

Premises used: le_total
-- Module: Mathlib.Data.Num.Lemmas
Goal:
⊢ LE.le (α := Num) 0 1

Tactic:
decide
-- Module: Mathlib.Data.Num.Lemmas
Goal:
⊢ Ne (α := Num) 0 1

Tactic:
decide
-- Module: Mathlib.Data.Num.Lemmas
Goal:
a : Num
ha : 0 < a
b c : Num
revert : ∀ (ha : 0 < a) (hbc : b < c), a * b < a * c
⊢ ∀ (hbc : b < c), a * b < a * c

Tactic:
revert ha
-- Module: Mathlib.Data.Num.Lemmas
Goal:
a b c : Num
transfer_rw :
  ∀ (ha : LT.lt (α := ℕ) 0 (↑a : ℕ)) (hbc : LT.lt (α := ℕ) (↑b : ℕ) (↑c : ℕ)),
    HMul.hMul (α := ℕ) (↑a : ℕ) (↑b : ℕ) < HMul.hMul (α := ℕ) (↑a : ℕ) (↑c : ℕ)
⊢ ∀ (ha : 0 < a) (hbc : b < c), a * b < a * c

Tactic:
transfer_rw
-- Module: Mathlib.Data.Num.Lemmas
Goal:
a b c : Num
⊢ ∀ (ha : LT.lt (α := ℕ) 0 (↑a : ℕ)) (hbc : LT.lt (α := ℕ) (↑b : ℕ) (↑c : ℕ)),
    HMul.hMul (α := ℕ) (↑a : ℕ) (↑b : ℕ) < HMul.hMul (α := ℕ) (↑a : ℕ) (↑c : ℕ)

Tactic:
apply flip mul_lt_mul_of_pos_left

Premises used: mul_lt_mul_of_pos_left, flip
-- Module: Mathlib.Data.Num.Lemmas
Goal:
a : Num
ha : 0 < a
b c : Num
revert : ∀ (ha : 0 < a) (hab : b < c), b * a < c * a
⊢ ∀ (hab : b < c), b * a < c * a

Tactic:
revert ha
-- Module: Mathlib.Data.Num.Lemmas
Goal:
a b c : Num
transfer_rw :
  ∀ (ha : LT.lt (α := ℕ) 0 (↑a : ℕ)) (hab : LT.lt (α := ℕ) (↑b : ℕ) (↑c : ℕ)),
    HMul.hMul (α := ℕ) (↑b : ℕ) (↑a : ℕ) < HMul.hMul (α := ℕ) (↑c : ℕ) (↑a : ℕ)
⊢ ∀ (ha : 0 < a) (hab : b < c), b * a < c * a

Tactic:
transfer_rw
-- Module: Mathlib.Data.Num.Lemmas
Goal:
a b c : Num
⊢ ∀ (ha : LT.lt (α := ℕ) 0 (↑a : ℕ)) (hab : LT.lt (α := ℕ) (↑b : ℕ) (↑c : ℕ)),
    HMul.hMul (α := ℕ) (↑b : ℕ) (↑a : ℕ) < HMul.hMul (α := ℕ) (↑c : ℕ) (↑a : ℕ)

Tactic:
apply flip mul_lt_mul_of_pos_right

Premises used: flip, mul_lt_mul_of_pos_right
-- Module: Mathlib.Data.Num.Lemmas
Goal:
m n : ℕ
⊢ (↑(m + n) : Num) = HAdd.hAdd (α := Num) (↑m : Num) (↑n : Num)

Tactic:
add_ofNat' _ _

Premises used: Num.add_ofNat'
-- Module: Mathlib.Data.Num.Lemmas
Goal:
n : Num
⊢ Eq (α := ℤ) (↑(↑n : ℕ) : ℤ) (↑n : ℤ)

Tactic:
cast_to_nat _

Premises used: Num.cast_to_nat
-- Module: Mathlib.Data.Num.Lemmas
Goal:
α : Type u_1
inst : AddGroupWithOne α
n : Num
rw : Eq.{u_1 + 1} (α := α) (↑(↑(↑n : ℕ) : ℤ) : α) (↑n : α)
rw₁ : Eq.{u_1 + 1} (α := α) (↑(↑n : ℕ) : α) (↑n : α)
rw₂ rw₃ : Eq.{u_1 + 1} (α := α) (↑n : α) (↑n : α)
⊢ Eq.{u_1 + 1} (α := α) (↑(↑n : ℤ) : α) (↑n : α)

Tactic:
rw [← to_nat_to_int, Int.cast_natCast, cast_to_nat]

Premises used: Int.cast_natCast, Num.cast_to_nat, Num.to_nat_to_int
-- Module: Mathlib.Data.Num.Lemmas
Goal:
rw : Eq (α := ℕ) (↑0 : ℕ) 0
rw₁ rw₂ : Eq (α := ℕ) 0 0
⊢ Eq (α := ℕ) (↑(↑0 : Num) : ℕ) 0

Tactic:
rw [Nat.cast_zero, cast_zero]

Premises used: Num.cast_zero, Nat.cast_zero
-- Module: Mathlib.Data.Num.Lemmas
Goal:
n : ℕ
rw : (↑(HAdd.hAdd (α := Num) (↑n : Num) 1) : ℕ) = n + 1
rw₁ : (↑(succ (↑n : Num)) : ℕ) = n + 1
rw₂ : HAdd.hAdd (α := ℕ) (↑(↑n : Num) : ℕ) 1 = n + 1
rw₃ rw₄ : n + 1 = n + 1
⊢ (↑(↑(n + 1) : Num) : ℕ) = n + 1

Tactic:
rw [Nat.cast_succ, add_one, succ_to_nat, to_of_nat n]

Premises used: Nat.cast_succ, Num.add_one, Num.succ_to_nat
-- Module: Mathlib.Data.Num.Lemmas
Goal:
α : Type u_1
inst : AddMonoidWithOne α
n : ℕ
rw : Eq.{u_1 + 1} (α := α) (↑(↑(↑n : Num) : ℕ) : α) (↑n : α)
rw₁ rw₂ : Eq.{u_1 + 1} (α := α) (↑n : α) (↑n : α)
⊢ Eq.{u_1 + 1} (α := α) (↑(↑n : Num) : α) (↑n : α)

Tactic:
rw [← cast_to_nat, to_of_nat]

Premises used: Num.to_of_nat, Num.cast_to_nat
-- Module: Mathlib.Data.Num.Lemmas
Goal:
m n : ℕ
⊢ Eq (α := Num) (↑m : Num) (↑n : Num) ↔ m = n

Tactic:
⟨fun h => Function.LeftInverse.injective to_of_nat h, congr_arg _⟩

Premises used: Function.LeftInverse.injective, Num.to_of_nat, congr_arg, Iff.intro
-- Module: Mathlib.Data.Num.Lemmas
Goal:
⊢ ∀ (n : Num), (↑(↑n : ℕ) : Num) = n

Tactic:
of_to_nat'

Premises used: Num.of_to_nat'
-- Module: Mathlib.Data.Num.Lemmas
Goal:
m n : Num
h : Dvd.dvd (α := ℕ) (↑m : ℕ) (↑n : ℕ)
k : ℕ
e : (↑n : ℕ) = (↑m : ℕ) * k
rw : (↑((↑m : ℕ) * k) : Num) = m * (↑k : Num)
⊢ n = m * (↑k : Num)

Tactic:
rw [← of_to_nat n, e]

Premises used: Num.of_to_nat
-- Module: Mathlib.Data.Num.Lemmas
Goal:
m n : Num
h : Dvd.dvd (α := ℕ) (↑m : ℕ) (↑n : ℕ)
k : ℕ
e : (↑n : ℕ) = (↑m : ℕ) * k
⊢ (↑((↑m : ℕ) * k) : Num) = m * (↑k : Num)

Tactic:
simp
-- Module: Mathlib.Data.Num.Lemmas
Goal:
m n : Num
h : m ∣ n
k : Num
e : n = m * k
⊢ (↑n : ℕ) = HMul.hMul (α := ℕ) (↑m : ℕ) (↑k : ℕ)

Tactic:
simp [e, mul_to_nat]

Premises used: Num.mul_to_nat
-- Module: Mathlib.Data.Num.Lemmas
Goal:
⊢ ∀ (n : PosNum), (↑(↑n : ℕ) : Num) = pos n

Tactic:
of_to_nat'

Premises used: PosNum.of_to_nat'
-- Module: Mathlib.Data.Num.Lemmas
Goal:
m n : PosNum
h : Eq (α := ℕ) (↑m : ℕ) (↑n : ℕ)
rw : (↑(↑m : ℕ) : Num) = pos n
rw₁ : Eq (α := Num) (↑(↑m : ℕ) : Num) (↑(↑n : ℕ) : Num)
rw₂ rw₃ : Eq (α := Num) (↑(↑n : ℕ) : Num) (↑(↑n : ℕ) : Num)
⊢ pos m = pos n

Tactic:
rw [← PosNum.of_to_nat, ← PosNum.of_to_nat, h]

Premises used: PosNum.of_to_nat
-- Module: Mathlib.Data.Num.Lemmas
Goal:
n : PosNum
rw : (Nat.pred (↑n : ℕ)).succ = (↑n : ℕ)
rw₁ rw₂ : Eq (α := ℕ) (↑n : ℕ) (↑n : ℕ)
⊢ Nat.succ (↑n.pred' : ℕ) = (↑n : ℕ)

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

Premises used: Nat.succ_pred_eq_of_pos, PosNum.to_nat_pos
-- Module: Mathlib.Data.Num.Lemmas
Goal:
n : PosNum
this : Nat.succ (↑n.pred' : ℕ) = (↑n : ℕ)
h : Eq (α := ℕ) (↑1 : ℕ) (↑n : ℕ)
rw : (↑(Num.casesOn (motive := fun (x : Num) ↦ PosNum) 0 1 bit1) : ℕ) = (HAdd.hAdd (α := ℕ) (↑1 : ℕ) (↑1 : ℕ)).pred
⊢ (↑(Num.casesOn (motive := fun (x : Num) ↦ PosNum) 0 1 bit1) : ℕ) = (HAdd.hAdd (α := ℕ) (↑n : ℕ) (↑n : ℕ)).pred

Tactic:
rw [← to_nat_inj.1 h]

Premises used: PosNum.to_nat_inj, Iff.mp
-- Module: Mathlib.Data.Num.Lemmas
Goal:
n : PosNum
this : Nat.succ (↑n.pred' : ℕ) = (↑n : ℕ)
h : Eq (α := ℕ) (↑1 : ℕ) (↑n : ℕ)
⊢ (↑(Num.casesOn (motive := fun (x : Num) ↦ PosNum) 0 1 bit1) : ℕ) = (HAdd.hAdd (α := ℕ) (↑1 : ℕ) (↑1 : ℕ)).pred

Tactic:
rfl
-- Module: Mathlib.Data.Num.Lemmas
Goal:
n : PosNum
this : Nat.succ (↑n.pred' : ℕ) = (↑n : ℕ)
p : PosNum
h : Nat.succ (↑p : ℕ) = (↑n : ℕ)
rw :
  (↑(Num.casesOn (motive := fun (x : Num) ↦ PosNum) (pos p) 1 bit1) : ℕ) = (Nat.succ (↑p : ℕ) + Nat.succ (↑p : ℕ)).pred
⊢ (↑(Num.casesOn (motive := fun (x : Num) ↦ PosNum) (pos p) 1 bit1) : ℕ) = (HAdd.hAdd (α := ℕ) (↑n : ℕ) (↑n : ℕ)).pred

Tactic:
rw [← h]
-- Module: Mathlib.Data.Num.Lemmas
Goal:
n : PosNum
this : Nat.succ (↑n.pred' : ℕ) = (↑n : ℕ)
p : PosNum
h : Nat.succ (↑p : ℕ) = (↑n : ℕ)
⊢ (↑(Num.casesOn (motive := fun (x : Num) ↦ PosNum) (pos p) 1 bit1) : ℕ) = (Nat.succ (↑p : ℕ) + Nat.succ (↑p : ℕ)).pred

Tactic:
(Nat.succ_add p p).symm

Premises used: castPosNum, Nat.succ_add, Eq.symm, Nat.pred
-- Module: Mathlib.Data.Num.Lemmas
Goal:
n : PosNum
this : Nat.succ (↑n.pred' : ℕ) = (↑n : ℕ)
p : PosNum
h : Nat.succ (↑p : ℕ) = (↑n : ℕ)
⊢ (↑(Num.casesOn (motive := fun (x : Num) ↦ PosNum) (pos p) 1 bit1) : ℕ) = (Nat.succ (↑p : ℕ) + Nat.succ (↑p : ℕ)).pred

Tactic:
exact (Nat.succ_add p p).symm

Premises used: castPosNum, Nat.succ_add, Eq.symm
-- Module: Mathlib.Data.Num.Lemmas
Goal:
n : Num
rw : Nat.pred (↑n.succ' : ℕ) = (↑n : ℕ)
rw₁ : (HAdd.hAdd (α := ℕ) (↑n : ℕ) 1).pred = (↑n : ℕ)
rw₂ : (Nat.succ (↑n : ℕ)).pred = (↑n : ℕ)
rw₃ rw₄ : Eq (α := ℕ) (↑n : ℕ) (↑n : ℕ)
⊢ Eq (α := ℕ) (↑n.succ'.pred' : ℕ) (↑n : ℕ)

Tactic:
rw [pred'_to_nat, succ'_to_nat, Nat.add_one, Nat.pred_succ]

Premises used: Num.succ'_to_nat, PosNum.pred'_to_nat, Nat.pred_succ, Nat.add_one
-- Module: Mathlib.Data.Num.Lemmas
Goal:
n : PosNum
rw : HAdd.hAdd (α := ℕ) (↑n.pred' : ℕ) 1 = (↑n : ℕ)
rw₁ : Nat.pred (↑n : ℕ) + 1 = (↑n : ℕ)
rw₂ : (Nat.pred (↑n : ℕ)).succ = (↑n : ℕ)
rw₃ rw₄ : Eq (α := ℕ) (↑n : ℕ) (↑n : ℕ)
⊢ Eq (α := ℕ) (↑n.pred'.succ' : ℕ) (↑n : ℕ)

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

Premises used: Num.succ'_to_nat, Nat.succ_pred_eq_of_pos, PosNum.to_nat_pos, PosNum.pred'_to_nat, Nat.add_one
-- Module: Mathlib.Data.Num.Lemmas
Goal:
m n : PosNum
⊢ Dvd.dvd (α := ℕ) (↑m : ℕ) (↑n : ℕ) ↔ m ∣ n

Tactic:
Num.dvd_to_nat (pos m) (pos n)

Premises used: castNum, Num.dvd_to_nat, Num.pos
-- Module: Mathlib.Data.Num.Lemmas
Goal:
n : PosNum
rw : Nat.bit false (↑n : ℕ) ≠ 0
⊢ (↑n.bit0.size : ℕ) = Nat.size (↑n.bit0 : ℕ)

Tactic:
rw [size, succ_to_nat, size_to_nat n, cast_bit0, ← two_mul, ← Nat.bit_false_apply,
        Nat.size_bit]

Premises used: two_mul, PosNum.size, Nat.size_bit, Nat.bit_false_apply, PosNum.cast_bit0, PosNum.succ_to_nat
-- Module: Mathlib.Data.Num.Lemmas
Goal:
n : PosNum
⊢ LT.lt (α := ℕ) 0 (↑n : ℕ)

Tactic:
have := to_nat_pos n
-- Module: Mathlib.Data.Num.Lemmas
Goal:
n : PosNum
this : LT.lt (α := ℕ) 0 (↑n : ℕ)
⊢ ¬HMul.hMul (α := ℕ) 2 (↑n : ℕ) = 0

Tactic:
lia
-- Module: Mathlib.Data.Num.Lemmas
Goal:
n : PosNum
rw : Nat.bit true (↑n : ℕ) ≠ 0
⊢ (↑n.bit1.size : ℕ) = Nat.size (↑n.bit1 : ℕ)

Tactic:
rw [size, succ_to_nat, size_to_nat n, cast_bit1, ← two_mul, ← Nat.bit_true_apply,
        Nat.size_bit]

Premises used: PosNum.cast_bit1, Nat.bit_true_apply, two_mul, PosNum.size, Nat.size_bit, PosNum.succ_to_nat
-- Module: Mathlib.Data.Num.Lemmas
Goal:
n : PosNum
⊢ ¬HMul.hMul (α := ℕ) 2 (↑n : ℕ) + 1 = 0

Tactic:
lia
-- Module: Mathlib.Data.Num.Lemmas
Goal:
n : PosNum
rw : (↑n.size.succ : ℕ) = n.bit0.natSize
rw₁ : HAdd.hAdd (α := ℕ) (↑n.size : ℕ) 1 = n.bit0.natSize
rw₂ : HAdd.hAdd (α := ℕ) (↑n.size : ℕ) 1 = n.natSize.succ
rw₃ rw₄ : n.natSize + 1 = n.natSize.succ
⊢ (↑n.bit0.size : ℕ) = n.bit0.natSize

Tactic:
rw [size, succ_to_nat, natSize, size_eq_natSize n]

Premises used: PosNum.natSize, PosNum.size, PosNum.succ_to_nat
-- Module: Mathlib.Data.Num.Lemmas
Goal:
n : PosNum
rw : (↑n.size.succ : ℕ) = n.bit1.natSize
rw₁ : HAdd.hAdd (α := ℕ) (↑n.size : ℕ) 1 = n.bit1.natSize
rw₂ : HAdd.hAdd (α := ℕ) (↑n.size : ℕ) 1 = n.natSize.succ
rw₃ rw₄ : n.natSize + 1 = n.natSize.succ
⊢ (↑n.bit1.size : ℕ) = n.bit1.natSize

Tactic:
rw [size, succ_to_nat, natSize, size_eq_natSize n]

Premises used: PosNum.natSize, PosNum.size, PosNum.succ_to_nat
-- Module: Mathlib.Data.Num.Lemmas
Goal:
n : PosNum
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: PosNum.size_to_nat, PosNum.size_eq_natSize
-- Module: Mathlib.Data.Num.Lemmas
Goal:
n : PosNum
one : 0 < PosNum.one.natSize
bit1 : ∀ (a : PosNum), 0 < a.bit1.natSize
bit0 : ∀ (a : PosNum), 0 < a.bit0.natSize
⊢ 0 < n.natSize

Tactic:
cases n
-- Module: Mathlib.Data.Num.Lemmas
Goal:
⊢ 0 < one.natSize

Tactic:
apply Nat.succ_pos

Premises used: Nat.succ_pos
-- Module: Mathlib.Data.Num.Lemmas
Goal:
a : PosNum
⊢ 0 < a.bit1.natSize

Tactic:
apply Nat.succ_pos

Premises used: Nat.succ_pos
-- Module: Mathlib.Data.Num.Lemmas
Goal:
a : PosNum
⊢ 0 < a.bit0.natSize

Tactic:
apply Nat.succ_pos

Premises used: Nat.succ_pos
-- Module: Mathlib.Data.Num.Lemmas
Goal:
α : Type u_1
transfer transfer₁ : ∀ (a b c : PosNum), a + b + c = a + (b + c)
transfer₂ transfer₃ :
  ∀ (a b c : PosNum), HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑b : ℕ) + (↑c : ℕ) = (↑a : ℕ) + HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑c : ℕ)
⊢ ∀ (a b c : PosNum), a + b + c = a + (b + c)

Tactic:
transfer
-- Module: Mathlib.Data.Num.Lemmas
Goal:
α : Type u_1
transfer transfer₁ : ∀ (a b : PosNum), a + b = b + a
transfer₂ transfer₃ : ∀ (a b : PosNum), HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑b : ℕ) = HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑a : ℕ)
⊢ ∀ (a b : PosNum), a + b = b + a

Tactic:
transfer
-- Module: Mathlib.Data.Num.Lemmas
Goal:
α : Type u_1
transfer transfer₁ : ∀ (a b c : PosNum), a * b * c = a * (b * c)
transfer₂ transfer₃ :
  ∀ (a b c : PosNum), HMul.hMul (α := ℕ) (↑a : ℕ) (↑b : ℕ) * (↑c : ℕ) = (↑a : ℕ) * HMul.hMul (α := ℕ) (↑b : ℕ) (↑c : ℕ)
⊢ ∀ (a b c : PosNum), a * b * c = a * (b * c)

Tactic:
transfer
-- Module: Mathlib.Data.Num.Lemmas
Goal:
α : Type u_1
transfer transfer₁ : ∀ (a : PosNum), 1 * a = a
transfer₂ transfer₃ : ∀ (a : PosNum), HMul.hMul (α := ℕ) 1 (↑a : ℕ) = (↑a : ℕ)
⊢ ∀ (a : PosNum), 1 * a = a

Tactic:
transfer
-- Module: Mathlib.Data.Num.Lemmas
Goal:
α : Type u_1
transfer transfer₁ : ∀ (a : PosNum), a * 1 = a
transfer₂ transfer₃ : ∀ (a : PosNum), HMul.hMul (α := ℕ) (↑a : ℕ) 1 = (↑a : ℕ)
⊢ ∀ (a : PosNum), a * 1 = a

Tactic:
transfer
-- Module: Mathlib.Data.Num.Lemmas
Goal:
α : Type u_1
transfer transfer₁ : ∀ (a b : PosNum), a * b = b * a
transfer₂ transfer₃ : ∀ (a b : PosNum), HMul.hMul (α := ℕ) (↑a : ℕ) (↑b : ℕ) = HMul.hMul (α := ℕ) (↑b : ℕ) (↑a : ℕ)
⊢ ∀ (a b : PosNum), a * b = b * a

Tactic:
transfer
-- Module: Mathlib.Data.Num.Lemmas
Goal:
α : Type u_1
transfer :
  ∀ (a b c : PosNum),
    (↑a : ℕ) * HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑c : ℕ) =
      HMul.hMul (α := ℕ) (↑a : ℕ) (↑b : ℕ) + HMul.hMul (α := ℕ) (↑a : ℕ) (↑c : ℕ)
⊢ ∀ (a b c : PosNum), a * (b + c) = a * b + a * c

Tactic:
transfer
-- Module: Mathlib.Data.Num.Lemmas
Goal:
α : Type u_1
a b c : PosNum
⊢ (↑a : ℕ) * HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑c : ℕ) =
    HMul.hMul (α := ℕ) (↑a : ℕ) (↑b : ℕ) + HMul.hMul (α := ℕ) (↑a : ℕ) (↑c : ℕ)

Tactic:
simp [mul_add]

Premises used: mul_add
-- Module: Mathlib.Data.Num.Lemmas
Goal:
α : Type u_1
transfer :
  ∀ (a b c : PosNum),
    (↑c : ℕ) * HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑b : ℕ) =
      HMul.hMul (α := ℕ) (↑a : ℕ) (↑c : ℕ) + HMul.hMul (α := ℕ) (↑b : ℕ) (↑c : ℕ)
⊢ ∀ (a b c : PosNum), (a + b) * c = a * c + b * c

Tactic:
transfer
-- Module: Mathlib.Data.Num.Lemmas
Goal:
α : Type u_1
a b c : PosNum
⊢ (↑c : ℕ) * HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑b : ℕ) =
    HMul.hMul (α := ℕ) (↑a : ℕ) (↑c : ℕ) + HMul.hMul (α := ℕ) (↑b : ℕ) (↑c : ℕ)

Tactic:
simp [mul_add, mul_comm]

Premises used: mul_comm, mul_add
-- Module: Mathlib.Data.Num.Lemmas
Goal:
α : Type u_1
transfer transfer₁ : ∀ (a : PosNum), a ≤ a
⊢ ∀ (a : PosNum), a ≤ a

Tactic:
transfer
-- Module: Mathlib.Data.Num.Lemmas
Goal:
α : Type u_1
a b c : PosNum
transfer_rw : LE.le (α := ℕ) (↑a : ℕ) (↑b : ℕ) → LE.le (α := ℕ) (↑b : ℕ) (↑c : ℕ) → LE.le (α := ℕ) (↑a : ℕ) (↑c : ℕ)
⊢ a ≤ b → b ≤ c → a ≤ c

Tactic:
transfer_rw
-- Module: Mathlib.Data.Num.Lemmas
Goal:
α : Type u_1
a b c : PosNum
⊢ LE.le (α := ℕ) (↑a : ℕ) (↑b : ℕ) → LE.le (α := ℕ) (↑b : ℕ) (↑c : ℕ) → LE.le (α := ℕ) (↑a : ℕ) (↑c : ℕ)

Tactic:
apply le_trans

Premises used: le_trans
-- Module: Mathlib.Data.Num.Lemmas
Goal:
α : Type u_1
a b : PosNum
transfer_rw : LT.lt (α := ℕ) (↑a : ℕ) (↑b : ℕ) ↔ LE.le (α := ℕ) (↑a : ℕ) (↑b : ℕ) ∧ ¬LE.le (α := ℕ) (↑b : ℕ) (↑a : ℕ)
⊢ a < b ↔ a ≤ b ∧ ¬b ≤ a

Tactic:
transfer_rw
-- Module: Mathlib.Data.Num.Lemmas
Goal:
α : Type u_1
a b : PosNum
⊢ LT.lt (α := ℕ) (↑a : ℕ) (↑b : ℕ) ↔ LE.le (α := ℕ) (↑a : ℕ) (↑b : ℕ) ∧ ¬LE.le (α := ℕ) (↑b : ℕ) (↑a : ℕ)

Tactic:
apply lt_iff_le_not_ge

Premises used: lt_iff_le_not_ge
-- Module: Mathlib.Data.Num.Lemmas
Goal:
α : Type u_1
a b : PosNum
transfer_rw : LE.le (α := ℕ) (↑a : ℕ) (↑b : ℕ) → LE.le (α := ℕ) (↑b : ℕ) (↑a : ℕ) → Eq (α := ℕ) (↑a : ℕ) (↑b : ℕ)
⊢ a ≤ b → b ≤ a → a = b

Tactic:
transfer_rw
-- Module: Mathlib.Data.Num.Lemmas
Goal:
α : Type u_1
a b : PosNum
⊢ LE.le (α := ℕ) (↑a : ℕ) (↑b : ℕ) → LE.le (α := ℕ) (↑b : ℕ) (↑a : ℕ) → Eq (α := ℕ) (↑a : ℕ) (↑b : ℕ)

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.Data.Num.Lemmas
Goal:
α : Type u_1
a b : PosNum
transfer_rw : LE.le (α := ℕ) (↑a : ℕ) (↑b : ℕ) ∨ LE.le (α := ℕ) (↑b : ℕ) (↑a : ℕ)
⊢ a ≤ b ∨ b ≤ a

Tactic:
transfer_rw
-- Module: Mathlib.Data.Num.Lemmas
Goal:
α : Type u_1
a b : PosNum
⊢ LE.le (α := ℕ) (↑a : ℕ) (↑b : ℕ) ∨ LE.le (α := ℕ) (↑b : ℕ) (↑a : ℕ)

Tactic:
apply le_total

Premises used: le_total