awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
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
⊢ ∀
    (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)
have 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
Tactic: cases PosNum.cmp b a <;> [simp; simp +contextual; simp]
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
m n : ZNum
⊢ LE.le (α := ℤ) (↑m : ℤ) (↑n : ℤ) ↔ m ≤ n
have rw : ¬LT.lt (α := ℤ) (↑n : ℤ) (↑m : ℤ) ↔ m ≤ n
Tactic: rw [← not_lt]
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
α : Type u_1
inst : Ring α
inst_1 : PartialOrder α
inst_2 : IsStrictOrderedRing α
m n : ZNum
⊢ LT.lt.{u_1} (α := α) (↑m : α) (↑n : α) ↔ m < n
have rw : LT.lt.{u_1} (α := α) (↑(↑m : ℤ) : α) (↑n : α) ↔ m < n
Tactic: rw [← cast_to_int m, ← cast_to_int n, Int.cast_lt, lt_to_int]
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
α : Type u_1
inst : Ring α
inst_1 : PartialOrder α
inst_2 : IsStrictOrderedRing α
m n : ZNum
rw : LT.lt.{u_1} (α := α) (↑(↑m : ℤ) : α) (↑n : α) ↔ m < n
⊢ LT.lt.{u_1} (α := α) (↑m : α) (↑n : α) ↔ m < n
have rw₁ : LT.lt.{u_1} (α := α) (↑(↑m : ℤ) : α) (↑(↑n : ℤ) : α) ↔ m < n
Tactic: rw [← cast_to_int m, ← cast_to_int n, Int.cast_lt, lt_to_int]
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
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
⊢ LT.lt.{u_1} (α := α) (↑m : α) (↑n : α) ↔ m < n
have rw₂ : LT.lt (α := ℤ) (↑m : ℤ) (↑n : ℤ) ↔ m < n
Tactic: rw [← cast_to_int m, ← cast_to_int n, Int.cast_lt, lt_to_int]
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
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
⊢ LT.lt.{u_1} (α := α) (↑m : α) (↑n : α) ↔ m < n
have rw₃ : m < n ↔ m < n
Tactic: rw [← cast_to_int m, ← cast_to_int n, Int.cast_lt, lt_to_int]
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
α : Type u_1
inst : Ring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
m n : ZNum
⊢ LE.le.{u_1} (α := α) (↑m : α) (↑n : α) ↔ m ≤ n
have rw : ¬LT.lt.{u_1} (α := α) (↑n : α) (↑m : α) ↔ m ≤ n
Tactic: rw [← not_lt]
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
α : Type u_1
inst : Ring α
inst_1 : PartialOrder α
inst_2 : IsStrictOrderedRing α
m n : ZNum
⊢ Eq.{u_1 + 1} (α := α) (↑m : α) (↑n : α) ↔ m = n
have rw : Eq.{u_1 + 1} (α := α) (↑(↑m : ℤ) : α) (↑n : α) ↔ m = n
Tactic: rw [← cast_to_int m, ← cast_to_int n, Int.cast_inj (α := α), to_int_inj]
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
α : Type u_1
inst : Ring α
inst_1 : PartialOrder α
inst_2 : IsStrictOrderedRing α
m n : ZNum
rw : Eq.{u_1 + 1} (α := α) (↑(↑m : ℤ) : α) (↑n : α) ↔ m = n
⊢ Eq.{u_1 + 1} (α := α) (↑m : α) (↑n : α) ↔ m = n
have rw₁ : Eq.{u_1 + 1} (α := α) (↑(↑m : ℤ) : α) (↑(↑n : ℤ) : α) ↔ m = n
Tactic: rw [← cast_to_int m, ← cast_to_int n, Int.cast_inj (α := α), to_int_inj]
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
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
⊢ Eq.{u_1 + 1} (α := α) (↑m : α) (↑n : α) ↔ m = n
have rw₂ : Eq (α := ℤ) (↑m : ℤ) (↑n : ℤ) ↔ m = n
Tactic: rw [← cast_to_int m, ← cast_to_int n, Int.cast_inj (α := α), to_int_inj]
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
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
⊢ Eq.{u_1 + 1} (α := α) (↑m : α) (↑n : α) ↔ m = n
have rw₃ : m = n ↔ m = n
Tactic: rw [← cast_to_int m, ← cast_to_int n, Int.cast_inj (α := α), to_int_inj]
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
α : Type u_1
a b c : ZNum
⊢ a ≤ b → b ≤ c → a ≤ c
have transfer_rw : LE.le (α := ℤ) (↑a : ℤ) (↑b : ℤ) → LE.le (α := ℤ) (↑b : ℤ) (↑c : ℤ) → LE.le (α := ℤ) (↑a : ℤ) (↑c : ℤ)
Tactic: transfer_rw
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
α : Type u_1
a b : ZNum
⊢ a < b ↔ a ≤ b ∧ ¬b ≤ a
have transfer_rw : LT.lt (α := ℤ) (↑a : ℤ) (↑b : ℤ) ↔ LE.le (α := ℤ) (↑a : ℤ) (↑b : ℤ) ∧ ¬LE.le (α := ℤ) (↑b : ℤ) (↑a : ℤ)
Tactic: transfer_rw
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
α : Type u_1
a b : ZNum
⊢ a ≤ b → b ≤ a → a = b
have transfer_rw : LE.le (α := ℤ) (↑a : ℤ) (↑b : ℤ) → LE.le (α := ℤ) (↑b : ℤ) (↑a : ℤ) → Eq (α := ℤ) (↑a : ℤ) (↑b : ℤ)
Tactic: transfer_rw
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
α : Type u_1
a b : ZNum
⊢ a ≤ b ∨ b ≤ a
have transfer_rw : LE.le (α := ℤ) (↑a : ℤ) (↑b : ℤ) ∨ LE.le (α := ℤ) (↑b : ℤ) (↑a : ℤ)
Tactic: transfer_rw
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
α : Type u_1
transfer transfer₁ : ∀ (a b c : ZNum), a + b + c = a + (b + c)
⊢ ∀ (a b c : ZNum), a + b + c = a + (b + c)
have transfer₂ : ∀ (a b c : ZNum), HAdd.hAdd (α := ℤ) (↑a : ℤ) (↑b : ℤ) + (↑c : ℤ) = (↑a : ℤ) + HAdd.hAdd (α := ℤ) (↑b : ℤ) (↑c : ℤ)
Tactic: transfer
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
α : Type u_1
transfer transfer₁ : ∀ (a : ZNum), -a + a = 0
⊢ ∀ (a : ZNum), -a + a = 0
have transfer₂ : ∀ (a : ZNum), HAdd.hAdd (α := ℤ) (↑(-a) : ℤ) (↑a : ℤ) = 0
Tactic: transfer
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
α : Type u_1
transfer transfer₁ : ∀ (a b : ZNum), a + b = b + a
⊢ ∀ (a b : ZNum), a + b = b + a
have transfer₂ : ∀ (a b : ZNum), HAdd.hAdd (α := ℤ) (↑a : ℤ) (↑b : ℤ) = HAdd.hAdd (α := ℤ) (↑b : ℤ) (↑a : ℤ)
Tactic: transfer
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
α : Type u_1
n : ℕ
⊢ (Num.ofNat' (n + 1)).toZNum = (Num.ofNat' n).toZNum + 1
have rw : (Num.ofNat' n + 1).toZNum = (Num.ofNat' n).toZNum + 1
Tactic: rw [Num.ofNat'_succ, Num.add_one, Num.toZNum_succ, ZNum.add_one]
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
α : Type u_1
n : ℕ
rw : (Num.ofNat' n + 1).toZNum = (Num.ofNat' n).toZNum + 1
⊢ (Num.ofNat' (n + 1)).toZNum = (Num.ofNat' n).toZNum + 1
have rw₁ : (Num.ofNat' n).succ.toZNum = (Num.ofNat' n).toZNum + 1
Tactic: rw [Num.ofNat'_succ, Num.add_one, Num.toZNum_succ, ZNum.add_one]
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
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
⊢ (Num.ofNat' (n + 1)).toZNum = (Num.ofNat' n).toZNum + 1
have rw₂ : (Num.ofNat' n).toZNum.succ = (Num.ofNat' n).toZNum + 1
Tactic: rw [Num.ofNat'_succ, Num.add_one, Num.toZNum_succ, ZNum.add_one]
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
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
⊢ (Num.ofNat' (n + 1)).toZNum = (Num.ofNat' n).toZNum + 1
have rw₃ : (Num.ofNat' n).toZNum.succ = (Num.ofNat' n).toZNum.succ
Tactic: rw [Num.ofNat'_succ, Num.add_one, Num.toZNum_succ, ZNum.add_one]
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
transfer transfer₁ : ∀ (a b : ZNum), a * b = b * a
⊢ ∀ (a b : ZNum), a * b = b * a
have transfer₂ : ∀ (a b : ZNum), HMul.hMul (α := ℤ) (↑a : ℤ) (↑b : ℤ) = HMul.hMul (α := ℤ) (↑b : ℤ) (↑a : ℤ)
Tactic: transfer
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
α : Type u_1
a b c : ZNum
⊢ a * b * c = a * (b * c)
have transfer : Eq (α := ℤ) (↑(a * b * c) : ℤ) (↑(a * (b * c)) : ℤ)
Tactic: transfer
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
α : Type u_1
a b c : ZNum
transfer transfer₁ transfer₂ transfer₃ transfer₄ : Eq (α := ℤ) (↑(a * b * c) : ℤ) (↑(a * (b * c)) : ℤ)
⊢ a * b * c = a * (b * c)
have transfer₅ : HMul.hMul (α := ℤ) (↑a : ℤ) (↑b : ℤ) * (↑c : ℤ) = (↑a : ℤ) * HMul.hMul (α := ℤ) (↑b : ℤ) (↑c : ℤ)
Tactic: transfer
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
α : Type u_1
transfer transfer₁ : ∀ (a : ZNum), 1 * a = a
⊢ ∀ (a : ZNum), 1 * a = a
have transfer₂ : ∀ (a : ZNum), HMul.hMul (α := ℤ) 1 (↑a : ℤ) = (↑a : ℤ)
Tactic: transfer
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
α : Type u_1
transfer transfer₁ : ∀ (a : ZNum), a * 1 = a
⊢ ∀ (a : ZNum), a * 1 = a
have transfer₂ : ∀ (a : ZNum), HMul.hMul (α := ℤ) (↑a : ℤ) 1 = (↑a : ℤ)
Tactic: transfer
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
α : Type u_1
transfer transfer₁ : ∀ (a : ZNum), 0 * a = 0
⊢ ∀ (a : ZNum), 0 * a = 0
have transfer₂ : ∀ (a : ZNum), HMul.hMul (α := ℤ) 0 (↑a : ℤ) = 0
Tactic: transfer
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
α : Type u_1
transfer transfer₁ : ∀ (a : ZNum), a * 0 = 0
⊢ ∀ (a : ZNum), a * 0 = 0
have transfer₂ : ∀ (a : ZNum), HMul.hMul (α := ℤ) (↑a : ℤ) 0 = 0
Tactic: transfer
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
α : Type u_1
⊢ ∀ (a b c : ZNum), a * (b + c) = a * b + a * c
have transfer : ∀ (a b c : ZNum),
  (↑a : ℤ) * HAdd.hAdd (α := ℤ) (↑b : ℤ) (↑c : ℤ) =
    HMul.hMul (α := ℤ) (↑a : ℤ) (↑b : ℤ) + HMul.hMul (α := ℤ) (↑a : ℤ) (↑c : ℤ)
Tactic: transfer
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
α : Type u_1
⊢ ∀ (a b c : ZNum), (a + b) * c = a * c + b * c
have transfer : ∀ (a b c : ZNum),
  (↑c : ℤ) * HAdd.hAdd (α := ℤ) (↑a : ℤ) (↑b : ℤ) =
    HMul.hMul (α := ℤ) (↑a : ℤ) (↑c : ℤ) + HMul.hMul (α := ℤ) (↑b : ℤ) (↑c : ℤ)
Tactic: transfer
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
α : Type u_1
a b : ZNum
h : a ≤ b
c : ZNum
⊢ a + c ≤ b + c
have revert : ∀ (h : a ≤ b), a + c ≤ b + c
Tactic: revert h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
α : Type u_1
a b c : ZNum
⊢ ∀ (h : a ≤ b), a + c ≤ b + c
have transfer_rw : ∀ (h : LE.le (α := ℤ) (↑a : ℤ) (↑b : ℤ)), LE.le (α := ℤ) (↑(a + c) : ℤ) (↑(b + c) : ℤ)
Tactic: transfer_rw
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
α : Type u_1
a b : ZNum
⊢ 0 < a → 0 < b → 0 < a * b
have transfer_rw : LT.lt (α := ℤ) (↑0 : ℤ) (↑a : ℤ) → LT.lt (α := ℤ) (↑0 : ℤ) (↑b : ℤ) → LT.lt (α := ℤ) (↑0 : ℤ) (↑(a * b) : ℤ)
Tactic: transfer_rw
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
α : Type u_1
inst : AddCommGroupWithOne α
m n : ZNum
⊢ (↑(m - n) : α) = HSub.hSub (α := α) (↑m : α) (↑n : α)
have simp : (↑(m - n) : α) = HAdd.hAdd (α := α) (-(↑n : α)) (↑m : α)
Tactic: simp [sub_eq_neg_add]
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
⊢ Eq (α := ZNum) (↑(-0) : ZNum) (-(↑0 : ZNum))
have rw : Eq (α := ZNum) (-(↑0 : ZNum)) (-(↑0 : ZNum))
Tactic: rw [Int.cast_neg]
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
n : ZNum
⊢ (↑(↑n : ℤ) : ZNum) = n
have rw : ofInt' (↑n : ℤ) = n
Tactic: rw [← ofInt'_eq, of_to_int']
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
n : ZNum
rw : ofInt' (↑n : ℤ) = n
⊢ (↑(↑n : ℤ) : ZNum) = n
have rw₁ : n = n
Tactic: rw [← ofInt'_eq, of_to_int']
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
n : ℤ
⊢ Eq (α := ℤ) (↑(↑0 : ZNum) : ℤ) 0
have simp : Eq (α := ℤ) (↑0 : ℤ) 0
Tactic: simp
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
n : ℤ
⊢ ∀ (k : ℤ), 0 ≤ k → (↑(↑k : ZNum) : ℤ) = k → (↑(↑(k + 1) : ZNum) : ℤ) = k + 1
have simp : ∀ (k : ℤ), 0 ≤ k → (↑(↑k : ZNum) : ℤ) = k → (↑(HAdd.hAdd (α := ZNum) (↑k : ZNum) 1) : ℤ) = k + 1
Tactic: simp
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
n : ℤ
⊢ ∀ (k : ℤ), k ≤ 0 → (↑(↑k : ZNum) : ℤ) = k → (↑(↑(k - 1) : ZNum) : ℤ) = k - 1
have simp : ∀ (k : ℤ), k ≤ 0 → (↑(↑k : ZNum) : ℤ) = k → HSub.hSub (α := ℤ) (↑(↑k : ZNum) : ℤ) (↑1 : ℤ) = k - 1
Tactic: simp
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
n : ℕ
⊢ Num.toZNumNeg (↑n : Num) = -(↑n : ZNum)
have rw : Num.toZNumNeg (↑n : Num) = -Num.toZNum (↑n : Num)
Tactic: rw [← of_nat_toZNum, Num.zneg_toZNum]
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
n : ℕ
rw : Num.toZNumNeg (↑n : Num) = -Num.toZNum (↑n : Num)
⊢ Num.toZNumNeg (↑n : Num) = -(↑n : ZNum)
have rw₁ : Num.toZNumNeg (↑n : Num) = Num.toZNumNeg (↑n : Num)
Tactic: rw [← of_nat_toZNum, Num.zneg_toZNum]
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
α : Type u_1
inst : AddGroupWithOne α
n : ℤ
⊢ Eq.{u_1 + 1} (α := α) (↑(↑n : ZNum) : α) (↑n : α)
have rw : Eq.{u_1 + 1} (α := α) (↑(↑(↑n : ZNum) : ℤ) : α) (↑n : α)
Tactic: rw [← cast_to_int, to_of_int]
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
α : Type u_1
inst : AddGroupWithOne α
n : ℤ
rw : Eq.{u_1 + 1} (α := α) (↑(↑(↑n : ZNum) : ℤ) : α) (↑n : α)
⊢ Eq.{u_1 + 1} (α := α) (↑(↑n : ZNum) : α) (↑n : α)
have rw₁ : Eq.{u_1 + 1} (α := α) (↑n : α) (↑n : α)
Tactic: rw [← cast_to_int, to_of_int]
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
α : Type u_1
inst : AddGroupWithOne α
n : ℕ
⊢ Eq.{u_1 + 1} (α := α) (↑(↑n : ZNum) : α) (↑n : α)
have rw : Eq.{u_1 + 1} (α := α) (↑(↑n : ZNum) : α) (↑(↑n : ℤ) : α)
Tactic: rw [← Int.cast_natCast, of_intCast, Int.cast_natCast]
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
m n : ZNum
h : Dvd.dvd (α := ℤ) (↑m : ℤ) (↑n : ℤ)
k : ℤ
e : (↑n : ℤ) = (↑m : ℤ) * k
⊢ n = m * (↑k : ZNum)
have rw : (↑((↑m : ℤ) * k) : ZNum) = m * (↑k : ZNum)
Tactic: rw [← of_to_int n, e]
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
m n : ZNum
h : m ∣ n
k : ZNum
e : n = m * k
⊢ (↑n : ℤ) = HMul.hMul (α := ℤ) (↑m : ℤ) (↑k : ℤ)
have simp : (↑(m * k) : ℤ) = HMul.hMul (α := ℤ) (↑m : ℤ) (↑k : ℤ)
Tactic: simp [e]
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
n d : PosNum
q r : Num
h₁ : (↑r : ℕ) + (↑d : ℕ) * HAdd.hAdd (α := ℕ) (↑q : ℕ) (↑q : ℕ) = (↑n : ℕ)
h₂ : (↑r : ℕ) < HMul.hMul (α := ℕ) 2 (↑d : ℕ)
⊢ (↑(d.divModAux q r).2 : ℕ) + HMul.hMul (α := ℕ) (↑d : ℕ) (↑(d.divModAux q r).1 : ℕ) = (↑n : ℕ) ∧
    LT.lt (α := ℕ) (↑(d.divModAux q r).2 : ℕ) (↑d : ℕ)
have unfold : (↑(match (motive := Option Num → Num × Num) Num.ofZNum' (r.sub' (Num.pos d)) with
            | some r' => (q.bit1, r')
            | none => (q.bit0, r)).2 :
        ℕ) +
      HMul.hMul (α := ℕ) (↑d : ℕ)
        (↑(match (motive := Option Num → Num × Num) Num.ofZNum' (r.sub' (Num.pos d)) with
              | some r' => (q.bit1, r')
              | none => (q.bit0, r)).1 :
          ℕ) =
    (↑n : ℕ) ∧
  LT.lt (α := ℕ)
    (↑(match (motive := Option Num → Num × Num) Num.ofZNum' (r.sub' (Num.pos d)) with
          | some r' => (q.bit1, r')
          | none => (q.bit0, r)).2 :
      ℕ)
    (↑d : ℕ)
Tactic: unfold divModAux
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
n d : PosNum
q r : Num
h₁ : (↑r : ℕ) + (↑d : ℕ) * HAdd.hAdd (α := ℕ) (↑q : ℕ) (↑q : ℕ) = (↑n : ℕ)
h₂ : (↑r : ℕ) < HMul.hMul (α := ℕ) 2 (↑d : ℕ)
r₂ : Num
⊢ Num.ofZNum' (r.sub' (Num.pos d)) = some r₂ ↔ (↑r : ℕ) = HAdd.hAdd (α := ℕ) (↑r₂ : ℕ) (↑d : ℕ)
have apply : r.sub' (Num.pos d) = r₂.toZNum ↔ (↑r : ℕ) = HAdd.hAdd (α := ℕ) (↑r₂ : ℕ) (↑d : ℕ)
Tactic: apply Num.mem_ofZNum'.trans
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
n d : PosNum
q r : Num
h₁ : (↑r : ℕ) + (↑d : ℕ) * HAdd.hAdd (α := ℕ) (↑q : ℕ) (↑q : ℕ) = (↑n : ℕ)
h₂ : (↑r : ℕ) < HMul.hMul (α := ℕ) 2 (↑d : ℕ)
r₂ : Num
⊢ r.sub' (Num.pos d) = r₂.toZNum ↔ (↑r : ℕ) = HAdd.hAdd (α := ℕ) (↑r₂ : ℕ) (↑d : ℕ)
have rw : (↑r : ℤ) = HAdd.hAdd (α := ℤ) (↑r₂ : ℤ) (↑(Num.pos d) : ℤ) ↔
  Eq (α := ℤ) (↑(↑r : ℕ) : ℤ) (↑(HAdd.hAdd (α := ℕ) (↑r₂ : ℕ) (↑d : ℕ)) : ℤ)
Tactic: rw [← ZNum.to_int_inj, Num.cast_toZNum, Num.cast_sub', sub_eq_iff_eq_add, ← Int.natCast_inj]
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (hypothesis)
Goal:
n d : PosNum
q r : Num
h₁ : (↑r : ℕ) + (↑d : ℕ) * HAdd.hAdd (α := ℕ) (↑q : ℕ) (↑q : ℕ) = (↑n : ℕ)
h₂ : (↑r : ℕ) < HMul.hMul (α := ℕ) 2 (↑d : ℕ)
⊢ (↑(match (motive := Option Num → Num × Num) Num.ofZNum' (r.sub' (Num.pos d)) with
              | some r' => (q.bit1, r')
              | none => (q.bit0, r)).2 :
          ℕ) +
        HMul.hMul (α := ℕ) (↑d : ℕ)
          (↑(match (motive := Option Num → Num × Num) Num.ofZNum' (r.sub' (Num.pos d)) with
                | some r' => (q.bit1, r')
                | none => (q.bit0, r)).1 :
            ℕ) =
      (↑n : ℕ) ∧
    LT.lt (α := ℕ)
      (↑(match (motive := Option Num → Num × Num) Num.ofZNum' (r.sub' (Num.pos d)) with
            | some r' => (q.bit1, r')
            | none => (q.bit0, r)).2 :
        ℕ)
      (↑d : ℕ)
have this : ∀ {r₂ : Num}, Num.ofZNum' (r.sub' (Num.pos d)) = some r₂ ↔ (↑r : ℕ) = HAdd.hAdd (α := ℕ) (↑r₂ : ℕ) (↑d : ℕ)
Tactic: have : ∀ {r₂}, Num.ofZNum' (Num.sub' r (Num.pos d)) = some r₂ ↔ (r : ℕ) = r₂ + d := by
    intro r₂
    apply Num.mem_ofZNum'.trans
    rw [← ZNum.to_int_inj, Num.cast_toZNum, Num.cast_sub', sub_eq_iff_eq_add, ← Int.natCast_inj]
    simp
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
n d : PosNum
q r : Num
h₁ : (↑r : ℕ) + (↑d : ℕ) * HAdd.hAdd (α := ℕ) (↑q : ℕ) (↑q : ℕ) = (↑n : ℕ)
h₂ : (↑r : ℕ) < HMul.hMul (α := ℕ) 2 (↑d : ℕ)
this : ∀ {r₂ : Num}, Num.ofZNum' (r.sub' (Num.pos d)) = some r₂ ↔ (↑r : ℕ) = HAdd.hAdd (α := ℕ) (↑r₂ : ℕ) (↑d : ℕ)
⊢ (↑(match (motive := Option Num → Num × Num) Num.ofZNum' (r.sub' (Num.pos d)) with
              | some r' => (q.bit1, r')
              | none => (q.bit0, r)).2 :
          ℕ) +
        HMul.hMul (α := ℕ) (↑d : ℕ)
          (↑(match (motive := Option Num → Num × Num) Num.ofZNum' (r.sub' (Num.pos d)) with
                | some r' => (q.bit1, r')
                | none => (q.bit0, r)).1 :
            ℕ) =
      (↑n : ℕ) ∧
    LT.lt (α := ℕ)
      (↑(match (motive := Option Num → Num × Num) Num.ofZNum' (r.sub' (Num.pos d)) with
            | some r' => (q.bit1, r')
            | none => (q.bit0, r)).2 :
        ℕ)
      (↑d : ℕ)
have none : ∀ (e : Num.ofZNum' (r.sub' (Num.pos d)) = none),
  (↑(match (motive := Option Num → Num × Num) none with
              | some r' => (q.bit1, r')
              | none => (q.bit0, r)).2 :
          ℕ) +
        HMul.hMul (α := ℕ) (↑d : ℕ)
          (↑(match (motive := Option Num → Num × Num) none with
                | some r' => (q.bit1, r')
                | none => (q.bit0, r)).1 :
            ℕ) =
      (↑n : ℕ) ∧
    LT.lt (α := ℕ)
      (↑(match (motive := Option Num → Num × Num) none with
            | some r' => (q.bit1, r')
            | none => (q.bit0, r)).2 :
        ℕ)
      (↑d : ℕ)
Tactic: rcases e : Num.ofZNum' (Num.sub' r (Num.pos d)) with - | r₂
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
n d : PosNum
q r : Num
h₁ : (↑r : ℕ) + (↑d : ℕ) * HAdd.hAdd (α := ℕ) (↑q : ℕ) (↑q : ℕ) = (↑n : ℕ)
h₂ : (↑r : ℕ) < HMul.hMul (α := ℕ) 2 (↑d : ℕ)
this : ∀ {r₂ : Num}, Num.ofZNum' (r.sub' (Num.pos d)) = some r₂ ↔ (↑r : ℕ) = HAdd.hAdd (α := ℕ) (↑r₂ : ℕ) (↑d : ℕ)
none :
  ∀ (e : Num.ofZNum' (r.sub' (Num.pos d)) = Option.none),
    (↑(match (motive := Option Num → Num × Num) Option.none with
                | some r' => (q.bit1, r')
                | Option.none => (q.bit0, r)).2 :
            ℕ) +
          HMul.hMul (α := ℕ) (↑d : ℕ)
            (↑(match (motive := Option Num → Num × Num) Option.none with
                  | some r' => (q.bit1, r')
                  | Option.none => (q.bit0, r)).1 :
              ℕ) =
        (↑n : ℕ) ∧
      LT.lt (α := ℕ)
        (↑(match (motive := Option Num → Num × Num) Option.none with
              | some r' => (q.bit1, r')
              | Option.none => (q.bit0, r)).2 :
          ℕ)
        (↑d : ℕ)
⊢ (↑(match (motive := Option Num → Num × Num) Num.ofZNum' (r.sub' (Num.pos d)) with
              | some r' => (q.bit1, r')
              | Option.none => (q.bit0, r)).2 :
          ℕ) +
        HMul.hMul (α := ℕ) (↑d : ℕ)
          (↑(match (motive := Option Num → Num × Num) Num.ofZNum' (r.sub' (Num.pos d)) with
                | some r' => (q.bit1, r')
                | Option.none => (q.bit0, r)).1 :
            ℕ) =
      (↑n : ℕ) ∧
    LT.lt (α := ℕ)
      (↑(match (motive := Option Num → Num × Num) Num.ofZNum' (r.sub' (Num.pos d)) with
            | some r' => (q.bit1, r')
            | Option.none => (q.bit0, r)).2 :
        ℕ)
      (↑d : ℕ)
have some : ∀ (r₂ : Num) (e : Num.ofZNum' (r.sub' (Num.pos d)) = some r₂),
  (↑(match (motive := Option Num → Num × Num) some r₂ with
              | some r' => (q.bit1, r')
              | Option.none => (q.bit0, r)).2 :
          ℕ) +
        HMul.hMul (α := ℕ) (↑d : ℕ)
          (↑(match (motive := Option Num → Num × Num) some r₂ with
                | some r' => (q.bit1, r')
                | Option.none => (q.bit0, r)).1 :
            ℕ) =
      (↑n : ℕ) ∧
    LT.lt (α := ℕ)
      (↑(match (motive := Option Num → Num × Num) some r₂ with
            | some r' => (q.bit1, r')
            | Option.none => (q.bit0, r)).2 :
        ℕ)
      (↑d : ℕ)
Tactic: rcases e : Num.ofZNum' (Num.sub' r (Num.pos d)) with - | r₂
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
n d : PosNum
q r : Num
h₁ : (↑r : ℕ) + (↑d : ℕ) * HAdd.hAdd (α := ℕ) (↑q : ℕ) (↑q : ℕ) = (↑n : ℕ)
h₂ : (↑r : ℕ) < HMul.hMul (α := ℕ) 2 (↑d : ℕ)
this : ∀ {r₂ : Num}, Num.ofZNum' (r.sub' (Num.pos d)) = some r₂ ↔ (↑r : ℕ) = HAdd.hAdd (α := ℕ) (↑r₂ : ℕ) (↑d : ℕ)
e : Num.ofZNum' (r.sub' (Num.pos d)) = none
⊢ (↑(match (motive := Option Num → Num × Num) none with
              | some r' => (q.bit1, r')
              | none => (q.bit0, r)).2 :
          ℕ) +
        HMul.hMul (α := ℕ) (↑d : ℕ)
          (↑(match (motive := Option Num → Num × Num) none with
                | some r' => (q.bit1, r')
                | none => (q.bit0, r)).1 :
            ℕ) =
      (↑n : ℕ) ∧
    LT.lt (α := ℕ)
      (↑(match (motive := Option Num → Num × Num) none with
            | some r' => (q.bit1, r')
            | none => (q.bit0, r)).2 :
        ℕ)
      (↑d : ℕ)
have none : (↑(match (motive := Option Num → Num × Num) none with
            | some r' => (q.bit1, r')
            | none => (q.bit0, r)).2 :
        ℕ) +
      (↑d : ℕ) * HAdd.hAdd (α := ℕ) (↑q : ℕ) (↑q : ℕ) =
    (↑n : ℕ) ∧
  LT.lt (α := ℕ)
    (↑(match (motive := Option Num → Num × Num) none with
          | some r' => (q.bit1, r')
          | none => (q.bit0, r)).2 :
      ℕ)
    (↑d : ℕ)
Tactic: rw [Num.cast_bit0, two_mul]