awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
α : Type u_1
inst : AddGroupWithOne α
a b : PosNum
⊢ (↑(a.bit0.sub' b.bit0) : α) = HSub.hSub (α := α) (↑a.bit0 : α) (↑b.bit0 : α)
have rw : HSub.hSub (α := α) (↑a : α) (↑b : α) + HSub.hSub (α := α) (↑a : α) (↑b : α) =
  HSub.hSub (α := α) (↑a.bit0 : α) (↑b.bit0 : α)
Tactic: rw [sub', ZNum.cast_bit0, cast_sub' a b]
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (hypothesis)
Goal:
α : Type u_1
inst : AddGroupWithOne α
a b : PosNum
⊢ HSub.hSub (α := α) (↑a : α) (↑b : α) + HSub.hSub (α := α) (↑a : α) (↑b : α) =
    HSub.hSub (α := α) (↑a.bit0 : α) (↑b.bit0 : α)
have this : (↑(HAdd.hAdd (α := ℤ) (↑a : ℤ) (-(↑b : ℤ)) + HAdd.hAdd (α := ℤ) (↑a : ℤ) (-(↑b : ℤ))) : α) =
  HAdd.hAdd (α := α) (↑a : α) (↑a : α) + HAdd.hAdd (α := α) (-(↑b : α)) (-(↑b : α))
Tactic: have : ((a + -b + (a + -b) : ℤ) : α) = a + a + (-b + -b) := by simp [add_left_comm]
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
α : Type u_1
inst : AddGroupWithOne α
a b : PosNum
⊢ (↑(a.bit0.sub' b.bit1) : α) = HSub.hSub (α := α) (↑a.bit0 : α) (↑b.bit1 : α)
have rw : HSub.hSub (α := α) (↑a : α) (↑b : α) + HSub.hSub (α := α) (↑a : α) (↑b : α) - 1 =
  HSub.hSub (α := α) (↑a.bit0 : α) (↑b.bit1 : α)
Tactic: rw [sub', ZNum.cast_bitm1, cast_sub' a b]
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (hypothesis)
Goal:
α : Type u_1
inst : AddGroupWithOne α
a b : PosNum
⊢ HSub.hSub (α := α) (↑a : α) (↑b : α) + HSub.hSub (α := α) (↑a : α) (↑b : α) - 1 =
    HSub.hSub (α := α) (↑a.bit0 : α) (↑b.bit1 : α)
have this : Eq.{u_1 + 1} (α := α) (↑(-(↑b : ℤ) + ((↑a : ℤ) + HAdd.hAdd (α := ℤ) (-(↑b : ℤ)) (-1))) : α)
  (↑(HAdd.hAdd (α := ℤ) (↑a : ℤ) (-1) + HAdd.hAdd (α := ℤ) (-(↑b : ℤ)) (-(↑b : ℤ))) : α)
Tactic: have : ((-b + (a + (-b + -1)) : ℤ) : α) = (a + -1 + (-b + -b) : ℤ) := by
      simp [add_comm, add_left_comm]
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
α : Type u_1
inst : AddGroupWithOne α
a b : PosNum
⊢ (↑(a.bit1.sub' b.bit0) : α) = HSub.hSub (α := α) (↑a.bit1 : α) (↑b.bit0 : α)
have rw : HSub.hSub (α := α) (↑a : α) (↑b : α) + HSub.hSub (α := α) (↑a : α) (↑b : α) + 1 =
  HSub.hSub (α := α) (↑a.bit1 : α) (↑b.bit0 : α)
Tactic: rw [sub', ZNum.cast_bit1, cast_sub' a b]
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (hypothesis)
Goal:
α : Type u_1
inst : AddGroupWithOne α
a b : PosNum
⊢ HSub.hSub (α := α) (↑a : α) (↑b : α) + HSub.hSub (α := α) (↑a : α) (↑b : α) + 1 =
    HSub.hSub (α := α) (↑a.bit1 : α) (↑b.bit0 : α)
have this : Eq.{u_1 + 1} (α := α) (↑(-(↑b : ℤ) + ((↑a : ℤ) + HAdd.hAdd (α := ℤ) (-(↑b : ℤ)) 1)) : α)
  (↑(HAdd.hAdd (α := ℤ) (↑a : ℤ) 1 + HAdd.hAdd (α := ℤ) (-(↑b : ℤ)) (-(↑b : ℤ))) : α)
Tactic: have : ((-b + (a + (-b + 1)) : ℤ) : α) = (a + 1 + (-b + -b) : ℤ) := by
      simp [add_comm, add_left_comm]
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
α : Type u_1
inst : AddGroupWithOne α
a b : PosNum
⊢ (↑(a.bit1.sub' b.bit1) : α) = HSub.hSub (α := α) (↑a.bit1 : α) (↑b.bit1 : α)
have rw : HSub.hSub (α := α) (↑a : α) (↑b : α) + HSub.hSub (α := α) (↑a : α) (↑b : α) =
  HSub.hSub (α := α) (↑a.bit1 : α) (↑b.bit1 : α)
Tactic: rw [sub', ZNum.cast_bit0, cast_sub' a b]
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (hypothesis)
Goal:
α : Type u_1
inst : AddGroupWithOne α
a b : PosNum
⊢ HSub.hSub (α := α) (↑a : α) (↑b : α) + HSub.hSub (α := α) (↑a : α) (↑b : α) =
    HSub.hSub (α := α) (↑a.bit1 : α) (↑b.bit1 : α)
have this : (↑(-(↑b : ℤ) + HAdd.hAdd (α := ℤ) (↑a : ℤ) (-(↑b : ℤ))) : α) = (↑a : α) + HAdd.hAdd (α := α) (-(↑b : α)) (-(↑b : α))
Tactic: have : ((-b + (a + -b) : ℤ) : α) = a + (-b + -b) := by simp [add_left_comm]
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
n : PosNum
⊢ (↑n : ℕ) = HAdd.hAdd (α := ℕ) (↑n.pred' : ℕ) 1
have rw : Eq (α := ℕ) (↑n : ℕ) (↑n.pred'.succ' : ℕ)
Tactic: rw [← Num.succ'_to_nat, n.succ'_pred']
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
n : PosNum
rw : Eq (α := ℕ) (↑n : ℕ) (↑n.pred'.succ' : ℕ)
⊢ (↑n : ℕ) = HAdd.hAdd (α := ℕ) (↑n.pred' : ℕ) 1
have rw₁ : Eq (α := ℕ) (↑n : ℕ) (↑n : ℕ)
Tactic: rw [← Num.succ'_to_nat, n.succ'_pred']
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
n : PosNum
⊢ (↑n : ℤ) = HAdd.hAdd (α := ℤ) (↑(↑n.pred' : ℕ) : ℤ) 1
have rw : (↑(HAdd.hAdd (α := ℕ) (↑n.pred' : ℕ) 1) : ℤ) = HAdd.hAdd (α := ℤ) (↑(↑n.pred' : ℕ) : ℤ) 1
Tactic: rw [← n.to_nat_to_int, to_nat_eq_succ_pred]
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
p : PosNum
⊢ (pos p).succ'.pred'.toZNumNeg = ZNum.neg p
have rw : (pos p).toZNumNeg = ZNum.neg p
Tactic: rw [PosNum.pred'_succ']
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
p : PosNum
⊢ (ZNum.pos p).pred.succ = ZNum.pos p
have rw : p.pred'.toZNum.succ = ZNum.pos p
Tactic: rw [ZNum.pred, ← toZNum_succ, Num.succ, PosNum.succ'_pred', toZNum]
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
p : PosNum
rw : p.pred'.toZNum.succ = ZNum.pos p
⊢ (ZNum.pos p).pred.succ = ZNum.pos p
have rw₁ : p.pred'.succ.toZNum = ZNum.pos p
Tactic: rw [ZNum.pred, ← toZNum_succ, Num.succ, PosNum.succ'_pred', toZNum]
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
p : PosNum
rw : p.pred'.toZNum.succ = ZNum.pos p
rw₁ : p.pred'.succ.toZNum = ZNum.pos p
⊢ (ZNum.pos p).pred.succ = ZNum.pos p
have rw₂ : (pos p.pred'.succ').toZNum = ZNum.pos p
Tactic: rw [ZNum.pred, ← toZNum_succ, Num.succ, PosNum.succ'_pred', toZNum]
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
p : PosNum
rw : p.pred'.toZNum.succ = ZNum.pos p
rw₁ : p.pred'.succ.toZNum = ZNum.pos p
rw₂ : (pos p.pred'.succ').toZNum = ZNum.pos p
⊢ (ZNum.pos p).pred.succ = ZNum.pos p
have rw₃ : (pos p).toZNum = ZNum.pos p
Tactic: rw [ZNum.pred, ← toZNum_succ, Num.succ, PosNum.succ'_pred', toZNum]
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
p : PosNum
rw : p.pred'.toZNum.succ = ZNum.pos p
rw₁ : p.pred'.succ.toZNum = ZNum.pos p
rw₂ : (pos p.pred'.succ').toZNum = ZNum.pos p
rw₃ : (pos p).toZNum = ZNum.pos p
⊢ (ZNum.pos p).pred.succ = ZNum.pos p
have rw₄ : ZNum.pos p = ZNum.pos p
Tactic: rw [ZNum.pred, ← toZNum_succ, Num.succ, PosNum.succ'_pred', toZNum]
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
n : ℕ
⊢ (ofNat' (n + 1)).toZNum = (ofNat' n).toZNum + 1
have rw : (ofNat' n + 1).toZNum = (ofNat' n).toZNum + 1
Tactic: rw [Num.ofNat'_succ, Num.add_one, toZNum_succ, ZNum.add_one]
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
n : ℕ
rw : (ofNat' n + 1).toZNum = (ofNat' n).toZNum + 1
⊢ (ofNat' (n + 1)).toZNum = (ofNat' n).toZNum + 1
have rw₁ : (ofNat' n).succ.toZNum = (ofNat' n).toZNum + 1
Tactic: rw [Num.ofNat'_succ, Num.add_one, toZNum_succ, ZNum.add_one]
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
n : ℕ
rw : (ofNat' n + 1).toZNum = (ofNat' n).toZNum + 1
rw₁ : (ofNat' n).succ.toZNum = (ofNat' n).toZNum + 1
⊢ (ofNat' (n + 1)).toZNum = (ofNat' n).toZNum + 1
have rw₂ : (ofNat' n).toZNum.succ = (ofNat' n).toZNum + 1
Tactic: rw [Num.ofNat'_succ, Num.add_one, toZNum_succ, ZNum.add_one]
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
n : ℕ
rw : (ofNat' n + 1).toZNum = (ofNat' n).toZNum + 1
rw₁ : (ofNat' n).succ.toZNum = (ofNat' n).toZNum + 1
rw₂ : (ofNat' n).toZNum.succ = (ofNat' n).toZNum + 1
⊢ (ofNat' (n + 1)).toZNum = (ofNat' n).toZNum + 1
have rw₃ : (ofNat' n).toZNum.succ = (ofNat' n).toZNum.succ
Tactic: rw [Num.ofNat'_succ, Num.add_one, toZNum_succ, ZNum.add_one]
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
n : ℕ
⊢ (ofNat' (n + 1)).toZNumNeg = (ofNat' (n + 1 + 1)).toZNumNeg + 1
have rw : (ofNat' (n + 1)).toZNumNeg = (ofNat' (n + 1) + 1).toZNumNeg + 1
Tactic: rw [@Num.ofNat'_succ (n + 1), Num.add_one, toZNumNeg_succ,
      @ofNat'_succ n, Num.add_one, ZNum.add_one, pred_succ]
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
n : ℕ
rw : (ofNat' (n + 1)).toZNumNeg = (ofNat' (n + 1) + 1).toZNumNeg + 1
⊢ (ofNat' (n + 1)).toZNumNeg = (ofNat' (n + 1 + 1)).toZNumNeg + 1
have rw₁ : (ofNat' (n + 1)).toZNumNeg = (ofNat' (n + 1)).succ.toZNumNeg + 1
Tactic: rw [@Num.ofNat'_succ (n + 1), Num.add_one, toZNumNeg_succ,
      @ofNat'_succ n, Num.add_one, ZNum.add_one, pred_succ]
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
n : ℕ
rw : (ofNat' (n + 1)).toZNumNeg = (ofNat' (n + 1) + 1).toZNumNeg + 1
rw₁ : (ofNat' (n + 1)).toZNumNeg = (ofNat' (n + 1)).succ.toZNumNeg + 1
⊢ (ofNat' (n + 1)).toZNumNeg = (ofNat' (n + 1 + 1)).toZNumNeg + 1
have rw₂ : (ofNat' (n + 1)).toZNumNeg = (ofNat' (n + 1)).toZNumNeg.pred + 1
Tactic: rw [@Num.ofNat'_succ (n + 1), Num.add_one, toZNumNeg_succ,
      @ofNat'_succ n, Num.add_one, ZNum.add_one, pred_succ]
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
n : ℕ
rw : (ofNat' (n + 1)).toZNumNeg = (ofNat' (n + 1) + 1).toZNumNeg + 1
rw₁ : (ofNat' (n + 1)).toZNumNeg = (ofNat' (n + 1)).succ.toZNumNeg + 1
rw₂ : (ofNat' (n + 1)).toZNumNeg = (ofNat' (n + 1)).toZNumNeg.pred + 1
⊢ (ofNat' (n + 1)).toZNumNeg = (ofNat' (n + 1 + 1)).toZNumNeg + 1
have rw₃ : (ofNat' n + 1).toZNumNeg = (ofNat' n + 1).toZNumNeg.pred + 1
Tactic: rw [@Num.ofNat'_succ (n + 1), Num.add_one, toZNumNeg_succ,
      @ofNat'_succ n, Num.add_one, ZNum.add_one, pred_succ]
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
n : ℕ
rw : (ofNat' (n + 1)).toZNumNeg = (ofNat' (n + 1) + 1).toZNumNeg + 1
rw₁ : (ofNat' (n + 1)).toZNumNeg = (ofNat' (n + 1)).succ.toZNumNeg + 1
rw₂ : (ofNat' (n + 1)).toZNumNeg = (ofNat' (n + 1)).toZNumNeg.pred + 1
rw₃ : (ofNat' n + 1).toZNumNeg = (ofNat' n + 1).toZNumNeg.pred + 1
⊢ (ofNat' (n + 1)).toZNumNeg = (ofNat' (n + 1 + 1)).toZNumNeg + 1
have rw₄ : (ofNat' n).succ.toZNumNeg = (ofNat' n).succ.toZNumNeg.pred + 1
Tactic: rw [@Num.ofNat'_succ (n + 1), Num.add_one, toZNumNeg_succ,
      @ofNat'_succ n, Num.add_one, ZNum.add_one, pred_succ]
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
n : ℕ
rw : (ofNat' (n + 1)).toZNumNeg = (ofNat' (n + 1) + 1).toZNumNeg + 1
rw₁ : (ofNat' (n + 1)).toZNumNeg = (ofNat' (n + 1)).succ.toZNumNeg + 1
rw₂ : (ofNat' (n + 1)).toZNumNeg = (ofNat' (n + 1)).toZNumNeg.pred + 1
rw₃ : (ofNat' n + 1).toZNumNeg = (ofNat' n + 1).toZNumNeg.pred + 1
rw₄ : (ofNat' n).succ.toZNumNeg = (ofNat' n).succ.toZNumNeg.pred + 1
⊢ (ofNat' (n + 1)).toZNumNeg = (ofNat' (n + 1 + 1)).toZNumNeg + 1
have rw₅ : (ofNat' n).succ.toZNumNeg = (ofNat' n).succ.toZNumNeg.pred.succ
Tactic: rw [@Num.ofNat'_succ (n + 1), Num.add_one, toZNumNeg_succ,
      @ofNat'_succ n, Num.add_one, ZNum.add_one, pred_succ]
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
n : ℕ
rw : (ofNat' (n + 1)).toZNumNeg = (ofNat' (n + 1) + 1).toZNumNeg + 1
rw₁ : (ofNat' (n + 1)).toZNumNeg = (ofNat' (n + 1)).succ.toZNumNeg + 1
rw₂ : (ofNat' (n + 1)).toZNumNeg = (ofNat' (n + 1)).toZNumNeg.pred + 1
rw₃ : (ofNat' n + 1).toZNumNeg = (ofNat' n + 1).toZNumNeg.pred + 1
rw₄ : (ofNat' n).succ.toZNumNeg = (ofNat' n).succ.toZNumNeg.pred + 1
rw₅ : (ofNat' n).succ.toZNumNeg = (ofNat' n).succ.toZNumNeg.pred.succ
⊢ (ofNat' (n + 1)).toZNumNeg = (ofNat' (n + 1 + 1)).toZNumNeg + 1
have rw₆ : (ofNat' n).succ.toZNumNeg = (ofNat' n).succ.toZNumNeg
Tactic: rw [@Num.ofNat'_succ (n + 1), Num.add_one, toZNumNeg_succ,
      @ofNat'_succ n, Num.add_one, ZNum.add_one, pred_succ]
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
n : ℕ
⊢ toZNum (↑(n + 1) : Num) = ZNum.ofInt' (↑(n + 1) : ℤ)
have rw : (HAdd.hAdd (α := Num) (↑n : Num) 1).toZNum = ZNum.ofInt' (↑(n + 1) : ℤ)
Tactic: rw [Nat.cast_succ, Num.add_one, toZNum_succ, ofInt'_toZNum n, Nat.cast_succ, succ_ofInt',
      ZNum.add_one]
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
n : ℕ
rw : (HAdd.hAdd (α := Num) (↑n : Num) 1).toZNum = ZNum.ofInt' (↑(n + 1) : ℤ)
⊢ toZNum (↑(n + 1) : Num) = ZNum.ofInt' (↑(n + 1) : ℤ)
have rw₁ : (succ (↑n : Num)).toZNum = ZNum.ofInt' (↑(n + 1) : ℤ)
Tactic: rw [Nat.cast_succ, Num.add_one, toZNum_succ, ofInt'_toZNum n, Nat.cast_succ, succ_ofInt',
      ZNum.add_one]
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
n : ℕ
rw : (HAdd.hAdd (α := Num) (↑n : Num) 1).toZNum = ZNum.ofInt' (↑(n + 1) : ℤ)
rw₁ : (succ (↑n : Num)).toZNum = ZNum.ofInt' (↑(n + 1) : ℤ)
⊢ toZNum (↑(n + 1) : Num) = ZNum.ofInt' (↑(n + 1) : ℤ)
have rw₂ : (toZNum (↑n : Num)).succ = ZNum.ofInt' (↑(n + 1) : ℤ)
Tactic: rw [Nat.cast_succ, Num.add_one, toZNum_succ, ofInt'_toZNum n, Nat.cast_succ, succ_ofInt',
      ZNum.add_one]
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
n : ℕ
rw : (HAdd.hAdd (α := Num) (↑n : Num) 1).toZNum = ZNum.ofInt' (↑(n + 1) : ℤ)
rw₁ : (succ (↑n : Num)).toZNum = ZNum.ofInt' (↑(n + 1) : ℤ)
rw₂ : (toZNum (↑n : Num)).succ = ZNum.ofInt' (↑(n + 1) : ℤ)
⊢ toZNum (↑(n + 1) : Num) = ZNum.ofInt' (↑(n + 1) : ℤ)
have rw₃ : (ZNum.ofInt' (↑n : ℤ)).succ = ZNum.ofInt' (↑(n + 1) : ℤ)
Tactic: rw [Nat.cast_succ, Num.add_one, toZNum_succ, ofInt'_toZNum n, Nat.cast_succ, succ_ofInt',
      ZNum.add_one]
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
n : ℕ
rw : (HAdd.hAdd (α := Num) (↑n : Num) 1).toZNum = ZNum.ofInt' (↑(n + 1) : ℤ)
rw₁ : (succ (↑n : Num)).toZNum = ZNum.ofInt' (↑(n + 1) : ℤ)
rw₂ : (toZNum (↑n : Num)).succ = ZNum.ofInt' (↑(n + 1) : ℤ)
rw₃ : (ZNum.ofInt' (↑n : ℤ)).succ = ZNum.ofInt' (↑(n + 1) : ℤ)
⊢ toZNum (↑(n + 1) : Num) = ZNum.ofInt' (↑(n + 1) : ℤ)
have rw₄ : (ZNum.ofInt' (↑n : ℤ)).succ = ZNum.ofInt' (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)
Tactic: rw [Nat.cast_succ, Num.add_one, toZNum_succ, ofInt'_toZNum n, Nat.cast_succ, succ_ofInt',
      ZNum.add_one]
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
n : ℕ
rw : (HAdd.hAdd (α := Num) (↑n : Num) 1).toZNum = ZNum.ofInt' (↑(n + 1) : ℤ)
rw₁ : (succ (↑n : Num)).toZNum = ZNum.ofInt' (↑(n + 1) : ℤ)
rw₂ : (toZNum (↑n : Num)).succ = ZNum.ofInt' (↑(n + 1) : ℤ)
rw₃ : (ZNum.ofInt' (↑n : ℤ)).succ = ZNum.ofInt' (↑(n + 1) : ℤ)
rw₄ : (ZNum.ofInt' (↑n : ℤ)).succ = ZNum.ofInt' (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)
⊢ toZNum (↑(n + 1) : Num) = ZNum.ofInt' (↑(n + 1) : ℤ)
have rw₅ : (ZNum.ofInt' (↑n : ℤ)).succ = ZNum.ofInt' (↑n : ℤ) + 1
Tactic: rw [Nat.cast_succ, Num.add_one, toZNum_succ, ofInt'_toZNum n, Nat.cast_succ, succ_ofInt',
      ZNum.add_one]
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
n : ℕ
rw : (HAdd.hAdd (α := Num) (↑n : Num) 1).toZNum = ZNum.ofInt' (↑(n + 1) : ℤ)
rw₁ : (succ (↑n : Num)).toZNum = ZNum.ofInt' (↑(n + 1) : ℤ)
rw₂ : (toZNum (↑n : Num)).succ = ZNum.ofInt' (↑(n + 1) : ℤ)
rw₃ : (ZNum.ofInt' (↑n : ℤ)).succ = ZNum.ofInt' (↑(n + 1) : ℤ)
rw₄ : (ZNum.ofInt' (↑n : ℤ)).succ = ZNum.ofInt' (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)
rw₅ : (ZNum.ofInt' (↑n : ℤ)).succ = ZNum.ofInt' (↑n : ℤ) + 1
⊢ toZNum (↑(n + 1) : Num) = ZNum.ofInt' (↑(n + 1) : ℤ)
have rw₆ : (ZNum.ofInt' (↑n : ℤ)).succ = (ZNum.ofInt' (↑n : ℤ)).succ
Tactic: rw [Nat.cast_succ, Num.add_one, toZNum_succ, ofInt'_toZNum n, Nat.cast_succ, succ_ofInt',
      ZNum.add_one]
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
m : Num
p : PosNum
⊢ pos p = m ↔ ZNum.pos p = m.toZNum
have zero : pos p = zero ↔ ZNum.pos p = zero.toZNum
Tactic: cases m
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
m : Num
p : PosNum
zero : pos p = Num.zero ↔ ZNum.pos p = Num.zero.toZNum
⊢ pos p = m ↔ ZNum.pos p = m.toZNum
have pos : ∀ (a : PosNum), pos p = pos a ↔ ZNum.pos p = (pos a).toZNum
Tactic: cases m
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
p : PosNum
⊢ pos p = zero ↔ ZNum.pos p = zero.toZNum
have zero : pos p = zero → ZNum.pos p = zero.toZNum
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
p : PosNum
zero : pos p = Num.zero → ZNum.pos p = Num.zero.toZNum
⊢ pos p = Num.zero ↔ ZNum.pos p = Num.zero.toZNum
have zero₁ : ZNum.pos p = Num.zero.toZNum → pos p = Num.zero
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
p a : PosNum
⊢ pos p = pos a ↔ ZNum.pos p = (pos a).toZNum
have pos : pos p = pos a → ZNum.pos p = (pos a).toZNum
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
p a : PosNum
pos : Num.pos p = Num.pos a → ZNum.pos p = (Num.pos a).toZNum
⊢ Num.pos p = Num.pos a ↔ ZNum.pos p = (Num.pos a).toZNum
have pos₁ : ZNum.pos p = (Num.pos a).toZNum → Num.pos p = Num.pos a
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
p a : PosNum
h : pos p = pos a
⊢ ZNum.pos p = (pos a).toZNum
have pos : ZNum.pos p = (pos p).toZNum
Tactic: cases h
Cleared hypotheses: a, h
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
p a : PosNum
h : pos p = pos a
⊢ ZNum.pos p = (pos a).toZNum
have pos : ZNum.pos p = (pos p).toZNum
Tactic: try cases h <;> rfl
Cleared hypotheses: a, h
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
p a : PosNum
h : ZNum.pos p = (pos a).toZNum
⊢ pos p = pos a
have pos : pos p = pos p
Tactic: cases h
Cleared hypotheses: a, h
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
p a : PosNum
h : ZNum.pos p = (pos a).toZNum
⊢ pos p = pos a
have pos : pos p = pos p
Tactic: try cases h <;> rfl
Cleared hypotheses: a, h
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
m : Num
p : PosNum
h : ZNum.neg p = m.toZNum
⊢ m ∈ ofZNum' (ZNum.neg p)
have zero : ∀ (h : ZNum.neg p = zero.toZNum), zero ∈ ofZNum' (ZNum.neg p)
Tactic: cases m
Cleared hypotheses: m, h
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
m : Num
p : PosNum
h : ZNum.neg p = m.toZNum
zero : ∀ (h : ZNum.neg p = Num.zero.toZNum), Num.zero ∈ ofZNum' (ZNum.neg p)
⊢ m ∈ ofZNum' (ZNum.neg p)
have pos : ∀ (a : PosNum) (h : ZNum.neg p = (pos a).toZNum), pos a ∈ ofZNum' (ZNum.neg p)
Tactic: cases m
Cleared hypotheses: m, h
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
p : PosNum
⊢ castNum <$> ofZNum' (ZNum.pos p) = toNat? (↑p : ℤ)
have rw : castNum <$> ofZNum' (ZNum.pos p) = toNat? (↑(↑p : ℕ) : ℤ)
Tactic: rw [← PosNum.to_nat_to_int p]
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
p : PosNum
⊢ Eq (α := ℤ) (↑(HAdd.hAdd (α := ℕ) (↑p.pred' : ℕ) 1) : ℤ) (↑p : ℤ)
have rw : Eq (α := ℤ) (↑(↑p.pred'.succ' : ℕ) : ℤ) (↑p : ℤ)
Tactic: rw [← succ'_to_nat]
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
p : PosNum
⊢ (↑(ofZNum (ZNum.pos p)) : ℕ) = toNat (↑p : ℤ)
have rw : (↑(ofZNum (ZNum.pos p)) : ℕ) = toNat (↑(↑p : ℕ) : ℤ)
Tactic: rw [← PosNum.to_nat_to_int p]
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
α : Type u_1
inst : AddMonoidWithOne α
n : ZNum
⊢ Eq.{u_1 + 1} (α := α) (↑(ofZNum n) : α) (↑(toNat (↑n : ℤ)) : α)
have rw : Eq.{u_1 + 1} (α := α) (↑(↑(ofZNum n) : ℕ) : α) (↑(toNat (↑n : ℤ)) : α)
Tactic: rw [← cast_to_nat, ofZNum_toNat]
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
α : Type u_1
inst : AddMonoidWithOne α
n : ZNum
rw : Eq.{u_1 + 1} (α := α) (↑(↑(ofZNum n) : ℕ) : α) (↑(toNat (↑n : ℤ)) : α)
⊢ Eq.{u_1 + 1} (α := α) (↑(ofZNum n) : α) (↑(toNat (↑n : ℤ)) : α)
have rw₁ : Eq.{u_1 + 1} (α := α) (↑(toNat (↑n : ℤ)) : α) (↑(toNat (↑n : ℤ)) : α)
Tactic: rw [← cast_to_nat, ofZNum_toNat]
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
m n : Num
⊢ (↑(ofZNum (m.sub' n)) : ℕ) = HSub.hSub (α := ℕ) (↑m : ℕ) (↑n : ℕ)
have rw : toNat (↑(m.sub' n) : ℤ) = HSub.hSub (α := ℕ) (↑m : ℕ) (↑n : ℕ)
Tactic: rw [ofZNum_toNat, cast_sub', ← to_nat_to_int, ← to_nat_to_int, Int.toNat_sub]
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
m n : Num
rw : toNat (↑(m.sub' n) : ℤ) = HSub.hSub (α := ℕ) (↑m : ℕ) (↑n : ℕ)
⊢ (↑(ofZNum (m.sub' n)) : ℕ) = HSub.hSub (α := ℕ) (↑m : ℕ) (↑n : ℕ)
have rw₁ : (HSub.hSub (α := ℤ) (↑m : ℤ) (↑n : ℤ)).toNat = HSub.hSub (α := ℕ) (↑m : ℕ) (↑n : ℕ)
Tactic: rw [ofZNum_toNat, cast_sub', ← to_nat_to_int, ← to_nat_to_int, Int.toNat_sub]
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
m n : Num
rw : toNat (↑(m.sub' n) : ℤ) = HSub.hSub (α := ℕ) (↑m : ℕ) (↑n : ℕ)
rw₁ : (HSub.hSub (α := ℤ) (↑m : ℤ) (↑n : ℤ)).toNat = HSub.hSub (α := ℕ) (↑m : ℕ) (↑n : ℕ)
⊢ (↑(ofZNum (m.sub' n)) : ℕ) = HSub.hSub (α := ℕ) (↑m : ℕ) (↑n : ℕ)
have rw₂ : (HSub.hSub (α := ℤ) (↑(↑m : ℕ) : ℤ) (↑n : ℤ)).toNat = HSub.hSub (α := ℕ) (↑m : ℕ) (↑n : ℕ)
Tactic: rw [ofZNum_toNat, cast_sub', ← to_nat_to_int, ← to_nat_to_int, Int.toNat_sub]
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
m n : Num
rw : toNat (↑(m.sub' n) : ℤ) = HSub.hSub (α := ℕ) (↑m : ℕ) (↑n : ℕ)
rw₁ : (HSub.hSub (α := ℤ) (↑m : ℤ) (↑n : ℤ)).toNat = HSub.hSub (α := ℕ) (↑m : ℕ) (↑n : ℕ)
rw₂ : (HSub.hSub (α := ℤ) (↑(↑m : ℕ) : ℤ) (↑n : ℤ)).toNat = HSub.hSub (α := ℕ) (↑m : ℕ) (↑n : ℕ)
⊢ (↑(ofZNum (m.sub' n)) : ℕ) = HSub.hSub (α := ℕ) (↑m : ℕ) (↑n : ℕ)
have rw₃ : (HSub.hSub (α := ℤ) (↑(↑m : ℕ) : ℤ) (↑(↑n : ℕ) : ℤ)).toNat = HSub.hSub (α := ℕ) (↑m : ℕ) (↑n : ℕ)
Tactic: rw [ofZNum_toNat, cast_sub', ← to_nat_to_int, ← to_nat_to_int, Int.toNat_sub]
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
m n : Num
rw : toNat (↑(m.sub' n) : ℤ) = HSub.hSub (α := ℕ) (↑m : ℕ) (↑n : ℕ)
rw₁ : (HSub.hSub (α := ℤ) (↑m : ℤ) (↑n : ℤ)).toNat = HSub.hSub (α := ℕ) (↑m : ℕ) (↑n : ℕ)
rw₂ : (HSub.hSub (α := ℤ) (↑(↑m : ℕ) : ℤ) (↑n : ℤ)).toNat = HSub.hSub (α := ℕ) (↑m : ℕ) (↑n : ℕ)
rw₃ : (HSub.hSub (α := ℤ) (↑(↑m : ℕ) : ℤ) (↑(↑n : ℕ) : ℤ)).toNat = HSub.hSub (α := ℕ) (↑m : ℕ) (↑n : ℕ)
⊢ (↑(ofZNum (m.sub' n)) : ℕ) = HSub.hSub (α := ℕ) (↑m : ℕ) (↑n : ℕ)
have rw₄ : HSub.hSub (α := ℕ) (↑m : ℕ) (↑n : ℕ) = HSub.hSub (α := ℕ) (↑m : ℕ) (↑n : ℕ)
Tactic: rw [ofZNum_toNat, cast_sub', ← to_nat_to_int, ← to_nat_to_int, Int.toNat_sub]
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
α : Type u_1
inst : AddGroupWithOne α
a : ZNum
⊢ (↑(0 + a) : α) = HAdd.hAdd (α := α) (↑0 : α) (↑a : α)
have zero : (↑(0 + zero) : α) = HAdd.hAdd (α := α) (↑0 : α) (↑zero : α)
Tactic: cases a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
α : Type u_1
inst : AddGroupWithOne α
a : ZNum
zero : (↑(0 + ZNum.zero) : α) = HAdd.hAdd (α := α) (↑0 : α) (↑ZNum.zero : α)
⊢ (↑(0 + a) : α) = HAdd.hAdd (α := α) (↑0 : α) (↑a : α)
have pos : ∀ (a : PosNum), (↑(0 + pos a) : α) = HAdd.hAdd (α := α) (↑0 : α) (↑(pos a) : α)
Tactic: cases a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
α : Type u_1
inst : AddGroupWithOne α
a : ZNum
zero : (↑(0 + ZNum.zero) : α) = HAdd.hAdd (α := α) (↑0 : α) (↑ZNum.zero : α)
pos : ∀ (a : PosNum), (↑(0 + ZNum.pos a) : α) = HAdd.hAdd (α := α) (↑0 : α) (↑(ZNum.pos a) : α)
⊢ (↑(0 + a) : α) = HAdd.hAdd (α := α) (↑0 : α) (↑a : α)
have neg : ∀ (a : PosNum), (↑(0 + neg a) : α) = HAdd.hAdd (α := α) (↑0 : α) (↑(neg a) : α)
Tactic: cases a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
α : Type u_1
inst : AddGroupWithOne α
b : ZNum
⊢ (↑(b + 0) : α) = HAdd.hAdd (α := α) (↑b : α) (↑0 : α)
have zero : (↑(zero + 0) : α) = HAdd.hAdd (α := α) (↑zero : α) (↑0 : α)
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
α : Type u_1
inst : AddGroupWithOne α
b : ZNum
zero : (↑(ZNum.zero + 0) : α) = HAdd.hAdd (α := α) (↑ZNum.zero : α) (↑0 : α)
⊢ (↑(b + 0) : α) = HAdd.hAdd (α := α) (↑b : α) (↑0 : α)
have pos : ∀ (a : PosNum), (↑(pos a + 0) : α) = HAdd.hAdd (α := α) (↑(pos a) : α) (↑0 : α)
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
α : Type u_1
inst : AddGroupWithOne α
b : ZNum
zero : (↑(ZNum.zero + 0) : α) = HAdd.hAdd (α := α) (↑ZNum.zero : α) (↑0 : α)
pos : ∀ (a : PosNum), (↑(ZNum.pos a + 0) : α) = HAdd.hAdd (α := α) (↑(ZNum.pos a) : α) (↑0 : α)
⊢ (↑(b + 0) : α) = HAdd.hAdd (α := α) (↑b : α) (↑0 : α)
have neg : ∀ (a : PosNum), (↑(neg a + 0) : α) = HAdd.hAdd (α := α) (↑(neg a) : α) (↑0 : α)
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
α : Type u_1
inst : AddGroupWithOne α
a b : PosNum
⊢ HAdd.hAdd (α := α) (↑b : α) (-(↑a : α)) = HAdd.hAdd (α := α) (-(↑a : α)) (↑b : α)
have rw : HAdd.hAdd (α := α) (↑(↑b : ℤ) : α) (↑(-(↑a : ℤ)) : α) = (↑(HAdd.hAdd (α := ℤ) (-(↑a : ℤ)) (↑b : ℤ)) : α)
Tactic: rw [← PosNum.cast_to_int a, ← PosNum.cast_to_int b, ← Int.cast_neg, ← Int.cast_add (-a)]
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
α : Type u_1
inst : AddGroupWithOne α
a b : PosNum
⊢ -(↑(a + b) : α) = HAdd.hAdd (α := α) (-(↑a : α)) (-(↑b : α))
have rw : -HAdd.hAdd (α := α) (↑a : α) (↑b : α) = HAdd.hAdd (α := α) (-(↑a : α)) (-(↑b : α))
Tactic: rw [PosNum.cast_add, neg_eq_iff_eq_neg, neg_add_rev, neg_neg, neg_neg,
          ← PosNum.cast_to_int a, ← PosNum.cast_to_int b, ← Int.cast_add, ← Int.cast_add, add_comm]