awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Num.ZNum
Goal:
a : PosNum
⊢ (↑(0 * pos a) : ℤ) = HMul.hMul (α := ℤ) (↑0 : ℤ) (↑(pos a) : ℤ)

Tactic:
exact (zero_mul _).symm

Premises used: MulZeroClass.zero_mul, Eq.symm
-- Module: Mathlib.Data.Num.ZNum
Goal:
a : PosNum
⊢ (↑(0 * neg a) : ℤ) = HMul.hMul (α := ℤ) (↑0 : ℤ) (↑(neg a) : ℤ)

Tactic:
(zero_mul _).symm

Premises used: castZNum, MulZeroClass.zero_mul, Eq.symm
-- Module: Mathlib.Data.Num.ZNum
Goal:
a : PosNum
⊢ (↑(0 * neg a) : ℤ) = HMul.hMul (α := ℤ) (↑0 : ℤ) (↑(neg a) : ℤ)

Tactic:
exact (zero_mul _).symm

Premises used: MulZeroClass.zero_mul, Eq.symm
-- Module: Mathlib.Data.Num.ZNum
Goal:
b : ZNum
zero : (↑(ZNum.zero * 0) : ℤ) = HMul.hMul (α := ℤ) (↑ZNum.zero : ℤ) (↑0 : ℤ)
pos : ∀ (a : PosNum), (↑(ZNum.pos a * 0) : ℤ) = HMul.hMul (α := ℤ) (↑(ZNum.pos a) : ℤ) (↑0 : ℤ)
neg : ∀ (a : PosNum), (↑(ZNum.neg a * 0) : ℤ) = HMul.hMul (α := ℤ) (↑(ZNum.neg a) : ℤ) (↑0 : ℤ)
⊢ (↑(b * 0) : ℤ) = HMul.hMul (α := ℤ) (↑b : ℤ) (↑0 : ℤ)

Tactic:
cases b
-- Module: Mathlib.Data.Num.ZNum
Goal:
⊢ (↑(zero * 0) : ℤ) = HMul.hMul (α := ℤ) (↑zero : ℤ) (↑0 : ℤ)

Tactic:
(mul_zero _).symm

Premises used: castZNum, MulZeroClass.mul_zero, Eq.symm
-- Module: Mathlib.Data.Num.ZNum
Goal:
⊢ (↑(zero * 0) : ℤ) = HMul.hMul (α := ℤ) (↑zero : ℤ) (↑0 : ℤ)

Tactic:
exact (mul_zero _).symm

Premises used: MulZeroClass.mul_zero, Eq.symm
-- Module: Mathlib.Data.Num.ZNum
Goal:
a : PosNum
⊢ (↑(pos a * 0) : ℤ) = HMul.hMul (α := ℤ) (↑(pos a) : ℤ) (↑0 : ℤ)

Tactic:
(mul_zero _).symm

Premises used: castZNum, MulZeroClass.mul_zero, Eq.symm
-- Module: Mathlib.Data.Num.ZNum
Goal:
a : PosNum
⊢ (↑(pos a * 0) : ℤ) = HMul.hMul (α := ℤ) (↑(pos a) : ℤ) (↑0 : ℤ)

Tactic:
exact (mul_zero _).symm

Premises used: MulZeroClass.mul_zero, Eq.symm
-- Module: Mathlib.Data.Num.ZNum
Goal:
a : PosNum
⊢ (↑(neg a * 0) : ℤ) = HMul.hMul (α := ℤ) (↑(neg a) : ℤ) (↑0 : ℤ)

Tactic:
(mul_zero _).symm

Premises used: castZNum, MulZeroClass.mul_zero, Eq.symm
-- Module: Mathlib.Data.Num.ZNum
Goal:
a : PosNum
⊢ (↑(neg a * 0) : ℤ) = HMul.hMul (α := ℤ) (↑(neg a) : ℤ) (↑0 : ℤ)

Tactic:
exact (mul_zero _).symm

Premises used: MulZeroClass.mul_zero, Eq.symm
-- Module: Mathlib.Data.Num.ZNum
Goal:
a b : PosNum
rw : -HMul.hMul (α := ℤ) (↑a : ℤ) (↑b : ℤ) = HMul.hMul (α := ℤ) (↑a : ℤ) (-(↑b : ℤ))
rw₁ rw₂ : HMul.hMul (α := ℤ) (↑a : ℤ) (-(↑b : ℤ)) = HMul.hMul (α := ℤ) (↑a : ℤ) (-(↑b : ℤ))
⊢ -(↑(a * b) : ℤ) = HMul.hMul (α := ℤ) (↑a : ℤ) (-(↑b : ℤ))

Tactic:
rw [PosNum.cast_mul, neg_mul_eq_mul_neg]

Premises used: PosNum.cast_mul, neg_mul_eq_mul_neg
-- Module: Mathlib.Data.Num.ZNum
Goal:
a b : PosNum
rw : -HMul.hMul (α := ℤ) (↑a : ℤ) (↑b : ℤ) = HMul.hMul (α := ℤ) (-(↑a : ℤ)) (↑b : ℤ)
rw₁ rw₂ : HMul.hMul (α := ℤ) (-(↑a : ℤ)) (↑b : ℤ) = HMul.hMul (α := ℤ) (-(↑a : ℤ)) (↑b : ℤ)
⊢ -(↑(a * b) : ℤ) = HMul.hMul (α := ℤ) (-(↑a : ℤ)) (↑b : ℤ)

Tactic:
rw [PosNum.cast_mul, neg_mul_eq_neg_mul]

Premises used: PosNum.cast_mul, neg_mul_eq_neg_mul
-- Module: Mathlib.Data.Num.ZNum
Goal:
a b : PosNum
rw : HMul.hMul (α := ℤ) (↑a : ℤ) (↑b : ℤ) = HMul.hMul (α := ℤ) (-(↑a : ℤ)) (-(↑b : ℤ))
rw₁ rw₂ : HMul.hMul (α := ℤ) (↑a : ℤ) (↑b : ℤ) = HMul.hMul (α := ℤ) (↑a : ℤ) (↑b : ℤ)
⊢ (↑(a * b) : ℤ) = HMul.hMul (α := ℤ) (-(↑a : ℤ)) (-(↑b : ℤ))

Tactic:
rw [PosNum.cast_mul, neg_mul_neg]

Premises used: PosNum.cast_mul, neg_mul_neg
-- Module: Mathlib.Data.Num.ZNum
Goal:
α : Type u_1
inst : NonAssocRing α
m n : ZNum
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_int, mul_to_int, Int.cast_mul, cast_to_int, cast_to_int]

Premises used: Int.cast_mul, ZNum.cast_to_int, ZNum.mul_to_int
-- Module: Mathlib.Data.Num.ZNum
Goal:
n : ℕ
⊢ ofInt' (↑(n + 1) : ℤ) = -ofInt' -[n+1]

Tactic:
simp only [ofInt', Num.zneg_toZNumNeg]

Premises used: ZNum.ofInt', Num.zneg_toZNumNeg
-- Module: Mathlib.Data.Num.ZNum
Goal:
⊢ Num.toZNum 0 = -Num.toZNum 0

Tactic:
rfl
-- Module: Mathlib.Data.Num.ZNum
Goal:
n : ℕ
rw rw₁ : (Num.ofNat' (n + 1)).toZNumNeg = (Num.ofNat' (n + 1)).toZNumNeg
⊢ (Num.ofNat' (n + 1)).toZNumNeg = -(Num.ofNat' (n + 1)).toZNum

Tactic:
rw [Num.zneg_toZNum]

Premises used: Num.zneg_toZNum
-- Module: Mathlib.Data.Num.ZNum
Goal:
⊢ (Num.ofNat' 0).toZNum = 0

Tactic:
simp only [Num.ofNat'_zero, Num.toZNum]

Premises used: Num.ofNat'_zero, Num.toZNum
-- Module: Mathlib.Data.Num.ZNum
Goal:
a : PosNum
rw : (Num.pos a).toZNum = pos a
⊢ ofInt' (↑(pos a) : ℤ) = pos a

Tactic:
rw [cast_pos, ← PosNum.cast_to_nat, ← Num.ofInt'_toZNum, PosNum.of_to_nat]

Premises used: PosNum.of_to_nat, PosNum.cast_to_nat, Num.ofInt'_toZNum, ZNum.cast_pos
-- Module: Mathlib.Data.Num.ZNum
Goal:
a : PosNum
⊢ (Num.pos a).toZNum = pos a

Tactic:
rfl
-- Module: Mathlib.Data.Num.ZNum
Goal:
a : PosNum
rw : -(Num.pos a).toZNum = neg a
⊢ ofInt' (↑(neg a) : ℤ) = neg a

Tactic:
rw [cast_neg, ofInt'_neg, ← PosNum.cast_to_nat, ← Num.ofInt'_toZNum, PosNum.of_to_nat]

Premises used: ZNum.cast_neg, PosNum.of_to_nat, PosNum.cast_to_nat, Num.ofInt'_toZNum, ZNum.ofInt'_neg
-- Module: Mathlib.Data.Num.ZNum
Goal:
a : PosNum
⊢ -(Num.pos a).toZNum = neg a

Tactic:
rfl
-- Module: Mathlib.Data.Num.ZNum
Goal:
m n : ZNum
⊢ Eq (α := ℤ) (↑m : ℤ) (↑n : ℤ) ↔ m = n

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

Premises used: Function.LeftInverse.injective, congr_arg, Iff.intro, ZNum.of_to_int'
-- Module: Mathlib.Data.Num.ZNum
Goal:
a b : PosNum
⊢ 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:
simpa using PosNum.cmp_to_nat a b

Premises used: PosNum.cmp_to_nat
-- Module: Mathlib.Data.Num.ZNum
Goal:
a b : PosNum
have :
  ∀
    (this :
      Ordering.casesOn (motive := fun (x : Ordering) ↦ Prop) (b.cmp a) (LT.lt (α := ℕ) (↑b : ℕ) (↑a : ℕ)) (b = a)
        (LT.lt (α := ℕ) (↑a : ℕ) (↑b : ℕ))),
    Ordering.casesOn (motive := fun (x : Ordering) ↦ Prop) ((neg a).cmp (neg b))
      (LT.lt (α := ℤ) (↑(neg a) : ℤ) (↑(neg b) : ℤ)) (neg a = neg b) (LT.lt (α := ℤ) (↑(neg b) : ℤ) (↑(neg a) : ℤ))
⊢ Ordering.casesOn (motive := fun (x : Ordering) ↦ Prop) ((neg a).cmp (neg b))
    (LT.lt (α := ℤ) (↑(neg a) : ℤ) (↑(neg b) : ℤ)) (neg a = neg b) (LT.lt (α := ℤ) (↑(neg b) : ℤ) (↑(neg a) : ℤ))

Tactic:
have := PosNum.cmp_to_nat b a
-- Module: Mathlib.Data.Num.ZNum
Goal:
a b : PosNum
this :
  Ordering.casesOn (motive := fun (x : Ordering) ↦ Prop) (b.cmp a) (LT.lt (α := ℕ) (↑b : ℕ) (↑a : ℕ)) (b = a)
    (LT.lt (α := ℕ) (↑a : ℕ) (↑b : ℕ))
revert :
  ∀
    (this :
      Ordering.casesOn (motive := fun (x : Ordering) ↦ Prop) (b.cmp a) (LT.lt (α := ℕ) (↑b : ℕ) (↑a : ℕ)) (b = a)
        (LT.lt (α := ℕ) (↑a : ℕ) (↑b : ℕ))),
    Ordering.casesOn (motive := fun (x : Ordering) ↦ Prop) ((neg a).cmp (neg b))
      (LT.lt (α := ℤ) (↑(neg a) : ℤ) (↑(neg b) : ℤ)) (neg a = neg b) (LT.lt (α := ℤ) (↑(neg b) : ℤ) (↑(neg a) : ℤ))
⊢ Ordering.casesOn (motive := fun (x : Ordering) ↦ Prop) ((neg a).cmp (neg b))
    (LT.lt (α := ℤ) (↑(neg a) : ℤ) (↑(neg b) : ℤ)) (neg a = neg b) (LT.lt (α := ℤ) (↑(neg b) : ℤ) (↑(neg a) : ℤ))

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

Tactic:
dsimp [cmp]

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

Tactic:
cases PosNum.cmp b a

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

Tactic:
simp
-- Module: Mathlib.Data.Num.ZNum
Goal:
a b : PosNum
⊢ ∀
    (this :
      Ordering.rec (motive := fun (x : Ordering) ↦ Prop) (LT.lt (α := ℕ) (↑b : ℕ) (↑a : ℕ)) (b = a)
        (LT.lt (α := ℕ) (↑a : ℕ) (↑b : ℕ)) Ordering.eq),
    Ordering.rec (motive := fun (x : Ordering) ↦ Prop) (LT.lt (α := ℤ) (-(↑a : ℤ)) (-(↑b : ℤ))) (neg a = neg b)
      (LT.lt (α := ℤ) (-(↑b : ℤ)) (-(↑a : ℤ))) Ordering.eq

Tactic:
simp +contextual
-- Module: Mathlib.Data.Num.ZNum
Goal:
a b : PosNum
⊢ ∀
    (this :
      Ordering.rec (motive := fun (x : Ordering) ↦ Prop) (LT.lt (α := ℕ) (↑b : ℕ) (↑a : ℕ)) (b = a)
        (LT.lt (α := ℕ) (↑a : ℕ) (↑b : ℕ)) Ordering.gt),
    Ordering.rec (motive := fun (x : Ordering) ↦ Prop) (LT.lt (α := ℤ) (-(↑a : ℤ)) (-(↑b : ℤ))) (neg a = neg b)
      (LT.lt (α := ℤ) (-(↑b : ℤ)) (-(↑a : ℤ))) Ordering.gt

Tactic:
simp
-- Module: Mathlib.Data.Num.ZNum
Goal:
a b : PosNum
lt :
  ∀
    (this :
      Ordering.rec (motive := fun (x : Ordering) ↦ Prop) (LT.lt (α := ℕ) (↑b : ℕ) (↑a : ℕ)) (b = a)
        (LT.lt (α := ℕ) (↑a : ℕ) (↑b : ℕ)) Ordering.lt),
    Ordering.rec (motive := fun (x : Ordering) ↦ Prop) (LT.lt (α := ℤ) (-(↑a : ℤ)) (-(↑b : ℤ))) (neg a = neg b)
      (LT.lt (α := ℤ) (-(↑b : ℤ)) (-(↑a : ℤ))) Ordering.lt
eq :
  ∀
    (this :
      Ordering.rec (motive := fun (x : Ordering) ↦ Prop) (LT.lt (α := ℕ) (↑b : ℕ) (↑a : ℕ)) (b = a)
        (LT.lt (α := ℕ) (↑a : ℕ) (↑b : ℕ)) Ordering.eq),
    Ordering.rec (motive := fun (x : Ordering) ↦ Prop) (LT.lt (α := ℤ) (-(↑a : ℤ)) (-(↑b : ℤ))) (neg a = neg b)
      (LT.lt (α := ℤ) (-(↑b : ℤ)) (-(↑a : ℤ))) Ordering.eq
gt :
  ∀
    (this :
      Ordering.rec (motive := fun (x : Ordering) ↦ Prop) (LT.lt (α := ℕ) (↑b : ℕ) (↑a : ℕ)) (b = a)
        (LT.lt (α := ℕ) (↑a : ℕ) (↑b : ℕ)) Ordering.gt),
    Ordering.rec (motive := fun (x : Ordering) ↦ Prop) (LT.lt (α := ℤ) (-(↑a : ℤ)) (-(↑b : ℤ))) (neg a = neg b)
      (LT.lt (α := ℤ) (-(↑b : ℤ)) (-(↑a : ℤ))) Ordering.gt
lt₁ :
  ∀
    (this :
      Ordering.rec (motive := fun (x : Ordering) ↦ Prop) (LT.lt (α := ℕ) (↑b : ℕ) (↑a : ℕ)) (b = a)
        (LT.lt (α := ℕ) (↑a : ℕ) (↑b : ℕ)) Ordering.lt),
    Ordering.rec (motive := fun (x : Ordering) ↦ Prop) (LT.lt (α := ℤ) (-(↑a : ℤ)) (-(↑b : ℤ))) (neg a = neg b)
      (LT.lt (α := ℤ) (-(↑b : ℤ)) (-(↑a : ℤ))) Ordering.lt
eq₁ :
  ∀
    (this :
      Ordering.rec (motive := fun (x : Ordering) ↦ Prop) (LT.lt (α := ℕ) (↑b : ℕ) (↑a : ℕ)) (b = a)
        (LT.lt (α := ℕ) (↑a : ℕ) (↑b : ℕ)) Ordering.eq),
    Ordering.rec (motive := fun (x : Ordering) ↦ Prop) (LT.lt (α := ℤ) (-(↑a : ℤ)) (-(↑b : ℤ))) (neg a = neg b)
      (LT.lt (α := ℤ) (-(↑b : ℤ)) (-(↑a : ℤ))) Ordering.eq
gt₁ :
  ∀
    (this :
      Ordering.rec (motive := fun (x : Ordering) ↦ Prop) (LT.lt (α := ℕ) (↑b : ℕ) (↑a : ℕ)) (b = a)
        (LT.lt (α := ℕ) (↑a : ℕ) (↑b : ℕ)) Ordering.gt),
    Ordering.rec (motive := fun (x : Ordering) ↦ Prop) (LT.lt (α := ℤ) (-(↑a : ℤ)) (-(↑b : ℤ))) (neg a = neg b)
      (LT.lt (α := ℤ) (-(↑b : ℤ)) (-(↑a : ℤ))) Ordering.gt
⊢ ∀
    (this :
      Ordering.rec (motive := fun (x : Ordering) ↦ Prop) (LT.lt (α := ℕ) (↑b : ℕ) (↑a : ℕ)) (b = a)
        (LT.lt (α := ℕ) (↑a : ℕ) (↑b : ℕ)) (b.cmp a)),
    Ordering.rec (motive := fun (x : Ordering) ↦ Prop) (LT.lt (α := ℤ) (-(↑a : ℤ)) (-(↑b : ℤ))) (neg a = neg b)
      (LT.lt (α := ℤ) (-(↑b : ℤ)) (-(↑a : ℤ))) (b.cmp a)

Tactic:
cases PosNum.cmp b a <;> [simp; simp +contextual; simp]

Premises used: PosNum.cmp
-- Module: Mathlib.Data.Num.ZNum
Goal:
m n : ZNum
h : LT.lt (α := ℤ) (↑m : ℤ) (↑n : ℤ)
⊢ LT.lt (α := ℤ) (↑m : ℤ) (↑n : ℤ) ↔ Ordering.lt = Ordering.lt

Tactic:
simp [h]
-- Module: Mathlib.Data.Num.ZNum
Goal:
m n : ZNum
h : m = n
⊢ LT.lt (α := ℤ) (↑m : ℤ) (↑n : ℤ) ↔ Ordering.eq = Ordering.lt

Tactic:
simp [h]
-- Module: Mathlib.Data.Num.ZNum
Goal:
m n : ZNum
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.ZNum
Goal:
m n : ZNum
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.ZNum
Goal:
m n : ZNum
⊢ ¬LT.lt (α := ℤ) (↑n : ℤ) (↑m : ℤ) ↔ m ≤ n

Tactic:
not_congr lt_to_int

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

Tactic:
exact not_congr lt_to_int

Premises used: ZNum.lt_to_int, not_congr
-- Module: Mathlib.Data.Num.ZNum
Goal:
α : Type u_1
inst : Ring α
inst_1 : PartialOrder α
inst_2 : IsStrictOrderedRing α
m n : ZNum
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_int m, ← cast_to_int n, Int.cast_lt, lt_to_int]

Premises used: Int.cast_lt, ZNum.lt_to_int, ZNum.cast_to_int
-- Module: Mathlib.Data.Num.ZNum
Goal:
α : Type u_1
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
m n : ZNum
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.ZNum
Goal:
α : Type u_1
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
m n : ZNum
⊢ ¬LT.lt.{u_1} (α := α) (↑n : α) (↑m : α) ↔ m ≤ n

Tactic:
not_congr cast_lt

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

Tactic:
exact not_congr cast_lt

Premises used: ZNum.cast_lt, not_congr
-- Module: Mathlib.Data.Num.ZNum
Goal:
α : Type u_1
inst : Ring α
inst_1 : PartialOrder α
inst_2 : IsStrictOrderedRing α
m n : ZNum
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_int m, ← cast_to_int n, Int.cast_inj (α := α), to_int_inj]

Premises used: Int.cast_inj, ZNum.cast_to_int, ZNum.to_int_inj
-- Module: Mathlib.Data.Num.ZNum
Goal:
α : Type u_1
transfer transfer₁ : ∀ (a : ZNum), a ≤ a
⊢ ∀ (a : ZNum), a ≤ a

Tactic:
transfer
-- Module: Mathlib.Data.Num.ZNum
Goal:
α : Type u_1
a b c : ZNum
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.ZNum
Goal:
α : Type u_1
a b c : ZNum
⊢ LE.le (α := ℤ) (↑a : ℤ) (↑b : ℤ) → LE.le (α := ℤ) (↑b : ℤ) (↑c : ℤ) → LE.le (α := ℤ) (↑a : ℤ) (↑c : ℤ)

Tactic:
apply le_trans

Premises used: le_trans
-- Module: Mathlib.Data.Num.ZNum
Goal:
α : Type u_1
a b : ZNum
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.ZNum
Goal:
α : Type u_1
a b : ZNum
⊢ 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.ZNum
Goal:
α : Type u_1
a b : ZNum
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.ZNum
Goal:
α : Type u_1
a b : ZNum
⊢ LE.le (α := ℤ) (↑a : ℤ) (↑b : ℤ) → LE.le (α := ℤ) (↑b : ℤ) (↑a : ℤ) → Eq (α := ℤ) (↑a : ℤ) (↑b : ℤ)

Tactic:
apply le_antisymm

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

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

Tactic:
apply le_total

Premises used: le_total
-- Module: Mathlib.Data.Num.ZNum
Goal:
α : Type u_1
transfer transfer₁ : ∀ (a b c : ZNum), a + b + c = a + (b + c)
transfer₂ transfer₃ :
  ∀ (a b c : ZNum), HAdd.hAdd (α := ℤ) (↑a : ℤ) (↑b : ℤ) + (↑c : ℤ) = (↑a : ℤ) + HAdd.hAdd (α := ℤ) (↑b : ℤ) (↑c : ℤ)
⊢ ∀ (a b c : ZNum), a + b + c = a + (b + c)

Tactic:
transfer
-- Module: Mathlib.Data.Num.ZNum
Goal:
α : Type u_1
transfer transfer₁ : ∀ (a : ZNum), -a + a = 0
transfer₂ transfer₃ : ∀ (a : ZNum), HAdd.hAdd (α := ℤ) (↑(-a) : ℤ) (↑a : ℤ) = 0
⊢ ∀ (a : ZNum), -a + a = 0

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

Tactic:
transfer
-- Module: Mathlib.Data.Num.ZNum
Goal:
α : Type u_1
⊢ Num.toZNum 0 = 0

Tactic:
rfl
-- Module: Mathlib.Data.Num.ZNum
Goal:
α : Type u_1
n : ℕ
rw : (Num.ofNat' n + 1).toZNum = (Num.ofNat' n).toZNum + 1
rw₁ : (Num.ofNat' n).succ.toZNum = (Num.ofNat' n).toZNum + 1
rw₂ : (Num.ofNat' n).toZNum.succ = (Num.ofNat' n).toZNum + 1
rw₃ rw₄ : (Num.ofNat' n).toZNum.succ = (Num.ofNat' n).toZNum.succ
⊢ (Num.ofNat' (n + 1)).toZNum = (Num.ofNat' n).toZNum + 1

Tactic:
rw [Num.ofNat'_succ, Num.add_one, Num.toZNum_succ, ZNum.add_one]

Premises used: Num.add_one, Num.ofNat'_succ, Num.toZNum_succ, ZNum.add_one
-- Module: Mathlib.Data.Num.ZNum
Goal:
transfer transfer₁ : ∀ (a b : ZNum), a * b = b * a
transfer₂ transfer₃ : ∀ (a b : ZNum), HMul.hMul (α := ℤ) (↑a : ℤ) (↑b : ℤ) = HMul.hMul (α := ℤ) (↑b : ℤ) (↑a : ℤ)
⊢ ∀ (a b : ZNum), a * b = b * a

Tactic:
transfer
-- Module: Mathlib.Data.Num.ZNum
Goal:
α : Type u_1
a b c : ZNum
transfer transfer₁ transfer₂ transfer₃ transfer₄ : Eq (α := ℤ) (↑(a * b * c) : ℤ) (↑(a * (b * c)) : ℤ)
transfer₅ transfer₆ : HMul.hMul (α := ℤ) (↑a : ℤ) (↑b : ℤ) * (↑c : ℤ) = (↑a : ℤ) * HMul.hMul (α := ℤ) (↑b : ℤ) (↑c : ℤ)
⊢ a * b * c = a * (b * c)

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

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

Tactic:
transfer
-- Module: Mathlib.Data.Num.ZNum
Goal:
α : Type u_1
transfer transfer₁ : ∀ (a : ZNum), 0 * a = 0
transfer₂ transfer₃ : ∀ (a : ZNum), HMul.hMul (α := ℤ) 0 (↑a : ℤ) = 0
⊢ ∀ (a : ZNum), 0 * a = 0

Tactic:
transfer
-- Module: Mathlib.Data.Num.ZNum
Goal:
α : Type u_1
transfer transfer₁ : ∀ (a : ZNum), a * 0 = 0
transfer₂ transfer₃ : ∀ (a : ZNum), HMul.hMul (α := ℤ) (↑a : ℤ) 0 = 0
⊢ ∀ (a : ZNum), a * 0 = 0

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

Tactic:
transfer
-- Module: Mathlib.Data.Num.ZNum
Goal:
α : Type u_1
a b c : ZNum
⊢ (↑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.ZNum
Goal:
α : Type u_1
transfer :
  ∀ (a b c : ZNum),
    (↑c : ℤ) * HAdd.hAdd (α := ℤ) (↑a : ℤ) (↑b : ℤ) =
      HMul.hMul (α := ℤ) (↑a : ℤ) (↑c : ℤ) + HMul.hMul (α := ℤ) (↑b : ℤ) (↑c : ℤ)
⊢ ∀ (a b c : ZNum), (a + b) * c = a * c + b * c

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

Tactic:
simp [mul_add, _root_.mul_comm]

Premises used: mul_comm, mul_add
-- Module: Mathlib.Data.Num.ZNum
Goal:
α : Type u_1
⊢ Ne (α := ZNum) 0 1

Tactic:
decide
-- Module: Mathlib.Data.Num.ZNum
Goal:
α : Type u_1
⊢ LE.le (α := ZNum) 0 1

Tactic:
decide
-- Module: Mathlib.Data.Num.ZNum
Goal:
α : Type u_1
a b : ZNum
h : a ≤ b
c : ZNum
revert : ∀ (h : a ≤ b), a + c ≤ b + c
⊢ a + c ≤ b + c

Tactic:
revert h
-- Module: Mathlib.Data.Num.ZNum
Goal:
α : Type u_1
a b c : ZNum
transfer_rw : ∀ (h : LE.le (α := ℤ) (↑a : ℤ) (↑b : ℤ)), LE.le (α := ℤ) (↑(a + c) : ℤ) (↑(b + c) : ℤ)
⊢ ∀ (h : a ≤ b), a + c ≤ b + c

Tactic:
transfer_rw
-- Module: Mathlib.Data.Num.ZNum
Goal:
α : Type u_1
a b : ZNum
transfer_rw :
  LT.lt (α := ℤ) (↑0 : ℤ) (↑a : ℤ) → LT.lt (α := ℤ) (↑0 : ℤ) (↑b : ℤ) → LT.lt (α := ℤ) (↑0 : ℤ) (↑(a * b) : ℤ)
⊢ 0 < a → 0 < b → 0 < a * b

Tactic:
transfer_rw
-- Module: Mathlib.Data.Num.ZNum
Goal:
α : Type u_1
inst : AddCommGroupWithOne α
m n : ZNum
simp : (↑(m - n) : α) = HAdd.hAdd (α := α) (-(↑n : α)) (↑m : α)
⊢ (↑(m - n) : α) = HSub.hSub (α := α) (↑m : α) (↑n : α)

Tactic:
simp [sub_eq_neg_add]

Premises used: sub_eq_neg_add
-- Module: Mathlib.Data.Num.ZNum
Goal:
rw : Eq (α := ZNum) (-(↑0 : ZNum)) (-(↑0 : ZNum))
⊢ Eq (α := ZNum) (↑(-0) : ZNum) (-(↑0 : ZNum))

Tactic:
rw [Int.cast_neg]

Premises used: Int.cast_neg
-- Module: Mathlib.Data.Num.ZNum
Goal:
n : ℕ
⊢ Num.toZNum (↑n : Num) = (↑n : ZNum)

Tactic:
rfl

Premises used: ZNum.ofInt', Num.toZNum, rfl
-- Module: Mathlib.Data.Num.ZNum
Goal:
n : ZNum
rw : ofInt' (↑n : ℤ) = n
rw₁ rw₂ : n = n
⊢ (↑(↑n : ℤ) : ZNum) = n

Tactic:
rw [← ofInt'_eq, of_to_int']

Premises used: ZNum.of_to_int', ZNum.ofInt'_eq
-- Module: Mathlib.Data.Num.ZNum
Goal:
n : ℤ
simp : Eq (α := ℤ) (↑0 : ℤ) 0
⊢ Eq (α := ℤ) (↑(↑0 : ZNum) : ℤ) 0

Tactic:
simp
-- Module: Mathlib.Data.Num.ZNum
Goal:
n : ℤ
simp : ∀ (k : ℤ), 0 ≤ k → (↑(↑k : ZNum) : ℤ) = k → (↑(HAdd.hAdd (α := ZNum) (↑k : ZNum) 1) : ℤ) = k + 1
⊢ ∀ (k : ℤ), 0 ≤ k → (↑(↑k : ZNum) : ℤ) = k → (↑(↑(k + 1) : ZNum) : ℤ) = k + 1

Tactic:
simp