awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Num.Prime (goal)
Goal:
n : PosNum
⊢ (HAdd.hAdd (α := ℕ) (↑n : ℕ) (↑n : ℕ) + 1).sqrt < (↑n : ℕ) + (HAdd.hAdd (α := ℕ) 1 1 + 1)
have bit1 : HAdd.hAdd (α := ℕ) (↑n : ℕ) (↑n : ℕ) + 1 <
  ((↑n : ℕ) + (HAdd.hAdd (α := ℕ) 1 1 + 1)) * ((↑n : ℕ) + (HAdd.hAdd (α := ℕ) 1 1 + 1))
Tactic: rw [Nat.sqrt_lt]
-- Lean 4 proof step from Mathlib.Data.Num.Prime (goal)
Goal:
n : PosNum
⊢ HAdd.hAdd (α := ℕ) (↑n : ℕ) (↑n : ℕ) + 1 <
    ((↑n : ℕ) + (HAdd.hAdd (α := ℕ) 1 1 + 1)) * ((↑n : ℕ) + (HAdd.hAdd (α := ℕ) 1 1 + 1))
have by : HAdd.hAdd (α := ℕ) (↑n : ℕ) (↑n : ℕ) + 1 ≤ HAdd.hAdd (α := ℕ) (↑n : ℕ) (↑n : ℕ) + (↑n : ℕ)
Tactic: calc
      (n : ℕ) + (n : ℕ) + 1 ≤ (n : ℕ) + (n : ℕ) + (n : ℕ) := by simp
      _ = (n : ℕ) * (1 + 1 + 1) := by simp only [mul_add, mul_one]
      _ < _ := by simp [mul_lt_mul]
-- Lean 4 proof step from Mathlib.Data.Num.Prime (goal)
Goal:
n : PosNum
by : HAdd.hAdd (α := ℕ) (↑n : ℕ) (↑n : ℕ) + 1 ≤ HAdd.hAdd (α := ℕ) (↑n : ℕ) (↑n : ℕ) + (↑n : ℕ)
⊢ HAdd.hAdd (α := ℕ) (↑n : ℕ) (↑n : ℕ) + 1 <
    ((↑n : ℕ) + (HAdd.hAdd (α := ℕ) 1 1 + 1)) * ((↑n : ℕ) + (HAdd.hAdd (α := ℕ) 1 1 + 1))
have by₁ : HAdd.hAdd (α := ℕ) (↑n : ℕ) (↑n : ℕ) + (↑n : ℕ) = (↑n : ℕ) * (HAdd.hAdd (α := ℕ) 1 1 + 1)
Tactic: calc
      (n : ℕ) + (n : ℕ) + 1 ≤ (n : ℕ) + (n : ℕ) + (n : ℕ) := by simp
      _ = (n : ℕ) * (1 + 1 + 1) := by simp only [mul_add, mul_one]
      _ < _ := by simp [mul_lt_mul]
-- Lean 4 proof step from Mathlib.Data.Num.Prime (goal)
Goal:
n : PosNum
by : HAdd.hAdd (α := ℕ) (↑n : ℕ) (↑n : ℕ) + 1 ≤ HAdd.hAdd (α := ℕ) (↑n : ℕ) (↑n : ℕ) + (↑n : ℕ)
by₁ : HAdd.hAdd (α := ℕ) (↑n : ℕ) (↑n : ℕ) + (↑n : ℕ) = (↑n : ℕ) * (HAdd.hAdd (α := ℕ) 1 1 + 1)
⊢ HAdd.hAdd (α := ℕ) (↑n : ℕ) (↑n : ℕ) + 1 <
    ((↑n : ℕ) + (HAdd.hAdd (α := ℕ) 1 1 + 1)) * ((↑n : ℕ) + (HAdd.hAdd (α := ℕ) 1 1 + 1))
have by₂ : (↑n : ℕ) * (HAdd.hAdd (α := ℕ) 1 1 + 1) <
  ((↑n : ℕ) + (HAdd.hAdd (α := ℕ) 1 1 + 1)) * ((↑n : ℕ) + (HAdd.hAdd (α := ℕ) 1 1 + 1))
Tactic: calc
      (n : ℕ) + (n : ℕ) + 1 ≤ (n : ℕ) + (n : ℕ) + (n : ℕ) := by simp
      _ = (n : ℕ) * (1 + 1 + 1) := by simp only [mul_add, mul_one]
      _ < _ := by simp [mul_lt_mul]
-- Lean 4 proof step from Mathlib.Data.Num.Prime (goal)
Goal:
a : PosNum
⊢ (↑a.bit0.minFac : ℕ) = Nat.minFac (↑a.bit0 : ℕ)
have bit0 : Eq (α := ℕ) (↑2 : ℕ) 2
Tactic: rw [minFac, Nat.minFac_eq, if_pos]
-- Lean 4 proof step from Mathlib.Data.Num.Prime (goal)
Goal:
a : PosNum
bit0 : Eq (α := ℕ) (↑2 : ℕ) 2
⊢ (↑a.bit0.minFac : ℕ) = Nat.minFac (↑a.bit0 : ℕ)
have bit0₁ : Dvd.dvd (α := ℕ) 2 (↑a.bit0 : ℕ)
Tactic: rw [minFac, Nat.minFac_eq, if_pos]
-- Lean 4 proof step from Mathlib.Data.Num.Prime (goal)
Goal:
n : PosNum
⊢ n.bit0.Prime ↔ n = 1
have refine_1 : LE.le (α := ℕ) 2 (↑n.bit0 : ℕ)
Tactic: refine Nat.prime_def_minFac.trans ((and_iff_right ?_).trans <| eq_comm.trans ?_)
-- Lean 4 proof step from Mathlib.Data.Num.Prime (goal)
Goal:
n : PosNum
refine_1 : LE.le (α := ℕ) 2 (↑n.bit0 : ℕ)
⊢ n.bit0.Prime ↔ n = 1
have refine_2 : (↑n.bit0 : ℕ) = Nat.minFac (↑n.bit0 : ℕ) ↔ n = 1
Tactic: refine Nat.prime_def_minFac.trans ((and_iff_right ?_).trans <| eq_comm.trans ?_)
-- Lean 4 proof step from Mathlib.Data.Num.Prime (goal)
Goal:
n : PosNum
⊢ (↑n.bit0 : ℕ) = Nat.minFac (↑n.bit0 : ℕ) ↔ n = 1
have refine_2 : n.bit0 = n.bit0.minFac ↔ n = 1
Tactic: rw [← minFac_to_nat, to_nat_inj]
-- Lean 4 proof step from Mathlib.Data.Num.Prime (goal)
Goal:
n : PosNum
⊢ n.bit1.Prime ↔ n.bit1.minFacAux (↑n : ℕ) 1 = n.bit1
have refine_1 : LE.le (α := ℕ) 2 (↑n.bit1 : ℕ)
Tactic: refine Nat.prime_def_minFac.trans ((and_iff_right ?_).trans ?_)
-- Lean 4 proof step from Mathlib.Data.Num.Prime (goal)
Goal:
n : PosNum
refine_1 : LE.le (α := ℕ) 2 (↑n.bit1 : ℕ)
⊢ n.bit1.Prime ↔ n.bit1.minFacAux (↑n : ℕ) 1 = n.bit1
have refine_2 : Nat.minFac (↑n.bit1 : ℕ) = (↑n.bit1 : ℕ) ↔ n.bit1.minFacAux (↑n : ℕ) 1 = n.bit1
Tactic: refine Nat.prime_def_minFac.trans ((and_iff_right ?_).trans ?_)
-- Lean 4 proof step from Mathlib.Data.Num.Prime (hypothesis)
Goal:
n : PosNum
⊢ 2 ≤ HAdd.hAdd (α := ℕ) (↑n : ℕ) (↑n : ℕ) + 1
have this : LT.lt (α := ℕ) 0 (↑n : ℕ)
Tactic: have := to_nat_pos n
-- Lean 4 proof step from Mathlib.Data.Num.Prime (goal)
Goal:
n : PosNum
⊢ Nat.minFac (↑n.bit1 : ℕ) = (↑n.bit1 : ℕ) ↔ n.bit1.minFacAux (↑n : ℕ) 1 = n.bit1
have refine_2 : n.bit1.minFac = n.bit1 ↔ n.bit1.minFacAux (↑n : ℕ) 1 = n.bit1
Tactic: rw [← minFac_to_nat, to_nat_inj]
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
n : ZNum
⊢ - -n = n
have zero : - -zero = zero
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
n : ZNum
zero : - -ZNum.zero = ZNum.zero
⊢ - -n = n
have pos : ∀ (a : PosNum), - -pos a = pos a
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
n : ZNum
zero : - -ZNum.zero = ZNum.zero
pos : ∀ (a : PosNum), - -ZNum.pos a = ZNum.pos a
⊢ - -n = n
have neg : ∀ (a : PosNum), - -neg a = neg a
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
n : ZNum
⊢ -n.bit1 = (-n).bitm1
have zero : -zero.bit1 = (-zero).bitm1
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
n : ZNum
zero : -ZNum.zero.bit1 = (-ZNum.zero).bitm1
⊢ -n.bit1 = (-n).bitm1
have pos : ∀ (a : PosNum), -(pos a).bit1 = (-pos a).bitm1
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
n : ZNum
zero : -ZNum.zero.bit1 = (-ZNum.zero).bitm1
pos : ∀ (a : PosNum), -(ZNum.pos a).bit1 = (-ZNum.pos a).bitm1
⊢ -n.bit1 = (-n).bitm1
have neg : ∀ (a : PosNum), -(neg a).bit1 = (-neg a).bitm1
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
n : ZNum
⊢ -n.bitm1 = (-n).bit1
have zero : -zero.bitm1 = (-zero).bit1
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
n : ZNum
zero : -ZNum.zero.bitm1 = (-ZNum.zero).bit1
⊢ -n.bitm1 = (-n).bit1
have pos : ∀ (a : PosNum), -(pos a).bitm1 = (-pos a).bit1
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
n : ZNum
zero : -ZNum.zero.bitm1 = (-ZNum.zero).bit1
pos : ∀ (a : PosNum), -(ZNum.pos a).bitm1 = (-ZNum.pos a).bit1
⊢ -n.bitm1 = (-n).bit1
have neg : ∀ (a : PosNum), -(neg a).bitm1 = (-neg a).bit1
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
n : ZNum
⊢ -n.succ = (-n).pred
have zero : -zero.succ = (-zero).pred
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
n : ZNum
zero : -ZNum.zero.succ = (-ZNum.zero).pred
⊢ -n.succ = (-n).pred
have pos : ∀ (a : PosNum), -(pos a).succ = (-pos a).pred
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
n : ZNum
zero : -ZNum.zero.succ = (-ZNum.zero).pred
pos : ∀ (a : PosNum), -(ZNum.pos a).succ = (-ZNum.pos a).pred
⊢ -n.succ = (-n).pred
have neg : ∀ (a : PosNum), -(neg a).succ = (-neg a).pred
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
a : PosNum
⊢ -(neg a).succ = (-neg a).pred
have neg : a.pred'.toZNum = (-neg a).pred
Tactic: rw [succ, Num.zneg_toZNumNeg]
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
n : ZNum
⊢ -n.pred = (-n).succ
have rw : -n.pred = - -(-n).succ
Tactic: rw [← zneg_zneg (succ (-n)), zneg_succ, zneg_zneg]
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
n : ZNum
rw : -n.pred = - -(-n).succ
⊢ -n.pred = (-n).succ
have rw₁ : -n.pred = -(- -n).pred
Tactic: rw [← zneg_zneg (succ (-n)), zneg_succ, zneg_zneg]
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
n : ZNum
rw : -n.pred = - -(-n).succ
rw₁ : -n.pred = -(- -n).pred
⊢ -n.pred = (-n).succ
have rw₂ : -n.pred = -n.pred
Tactic: rw [← zneg_zneg (succ (-n)), zneg_succ, zneg_zneg]
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
p : PosNum
⊢ natAbs (↑(↑p : ℕ) : ℤ) = natAbs (-(↑p : ℤ))
have rw : natAbs (↑p : ℤ) = natAbs (-(↑p : ℤ))
Tactic: rw [p.to_nat_to_int, Int.natAbs_neg]
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
p : PosNum
rw : natAbs (↑p : ℤ) = natAbs (-(↑p : ℤ))
⊢ natAbs (↑(↑p : ℕ) : ℤ) = natAbs (-(↑p : ℤ))
have rw₁ : natAbs (↑p : ℤ) = natAbs (↑p : ℤ)
Tactic: rw [p.to_nat_to_int, Int.natAbs_neg]
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
α : Type u_1
inst : AddGroupWithOne α
⊢ Eq.{u_1 + 1} (α := α) (↑(↑0 : ℤ) : α) (↑0 : α)
have rw : Eq.{u_1 + 1} (α := α) (↑0 : α) (↑0 : α)
Tactic: rw [cast_zero, cast_zero, Int.cast_zero]
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
α : Type u_1
inst : AddGroupWithOne α
rw : Eq.{u_1 + 1} (α := α) (↑0 : α) (↑0 : α)
⊢ Eq.{u_1 + 1} (α := α) (↑(↑0 : ℤ) : α) (↑0 : α)
have rw₁ : Eq.{u_1 + 1} (α := α) (↑0 : α) 0
Tactic: rw [cast_zero, cast_zero, Int.cast_zero]
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
α : Type u_1
inst : AddGroupWithOne α
rw : Eq.{u_1 + 1} (α := α) (↑0 : α) (↑0 : α)
rw₁ : Eq.{u_1 + 1} (α := α) (↑0 : α) 0
⊢ Eq.{u_1 + 1} (α := α) (↑(↑0 : ℤ) : α) (↑0 : α)
have rw₂ : Eq.{u_1 + 1} (α := α) 0 0
Tactic: rw [cast_zero, cast_zero, Int.cast_zero]
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
α : Type u_1
inst : AddGroupWithOne α
p : PosNum
⊢ Eq.{u_1 + 1} (α := α) (↑(↑(pos p) : ℤ) : α) (↑(pos p) : α)
have rw : Eq.{u_1 + 1} (α := α) (↑(↑p : ℤ) : α) (↑(pos p) : α)
Tactic: rw [cast_pos, cast_pos, PosNum.cast_to_int]
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
α : Type u_1
inst : AddGroupWithOne α
p : PosNum
rw : Eq.{u_1 + 1} (α := α) (↑(↑p : ℤ) : α) (↑(pos p) : α)
⊢ Eq.{u_1 + 1} (α := α) (↑(↑(pos p) : ℤ) : α) (↑(pos p) : α)
have rw₁ : Eq.{u_1 + 1} (α := α) (↑(↑p : ℤ) : α) (↑p : α)
Tactic: rw [cast_pos, cast_pos, PosNum.cast_to_int]
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
α : Type u_1
inst : AddGroupWithOne α
p : PosNum
rw : Eq.{u_1 + 1} (α := α) (↑(↑p : ℤ) : α) (↑(pos p) : α)
rw₁ : Eq.{u_1 + 1} (α := α) (↑(↑p : ℤ) : α) (↑p : α)
⊢ Eq.{u_1 + 1} (α := α) (↑(↑(pos p) : ℤ) : α) (↑(pos p) : α)
have rw₂ : Eq.{u_1 + 1} (α := α) (↑p : α) (↑p : α)
Tactic: rw [cast_pos, cast_pos, PosNum.cast_to_int]
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
α : Type u_1
inst : AddGroupWithOne α
p : PosNum
⊢ Eq.{u_1 + 1} (α := α) (↑(↑(neg p) : ℤ) : α) (↑(neg p) : α)
have rw : Eq.{u_1 + 1} (α := α) (↑(-(↑p : ℤ)) : α) (↑(neg p) : α)
Tactic: rw [cast_neg, cast_neg, Int.cast_neg, PosNum.cast_to_int]
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
α : Type u_1
inst : AddGroupWithOne α
p : PosNum
rw : Eq.{u_1 + 1} (α := α) (↑(-(↑p : ℤ)) : α) (↑(neg p) : α)
⊢ Eq.{u_1 + 1} (α := α) (↑(↑(neg p) : ℤ) : α) (↑(neg p) : α)
have rw₁ : Eq.{u_1 + 1} (α := α) (↑(-(↑p : ℤ)) : α) (-(↑p : α))
Tactic: rw [cast_neg, cast_neg, Int.cast_neg, PosNum.cast_to_int]
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
α : Type u_1
inst : AddGroupWithOne α
p : PosNum
rw : Eq.{u_1 + 1} (α := α) (↑(-(↑p : ℤ)) : α) (↑(neg p) : α)
rw₁ : Eq.{u_1 + 1} (α := α) (↑(-(↑p : ℤ)) : α) (-(↑p : α))
⊢ Eq.{u_1 + 1} (α := α) (↑(↑(neg p) : ℤ) : α) (↑(neg p) : α)
have rw₂ : Eq.{u_1 + 1} (α := α) (-(↑(↑p : ℤ) : α)) (-(↑p : α))
Tactic: rw [cast_neg, cast_neg, Int.cast_neg, PosNum.cast_to_int]
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
α : Type u_1
inst : AddGroupWithOne α
p : PosNum
rw : Eq.{u_1 + 1} (α := α) (↑(-(↑p : ℤ)) : α) (↑(neg p) : α)
rw₁ : Eq.{u_1 + 1} (α := α) (↑(-(↑p : ℤ)) : α) (-(↑p : α))
rw₂ : Eq.{u_1 + 1} (α := α) (-(↑(↑p : ℤ) : α)) (-(↑p : α))
⊢ Eq.{u_1 + 1} (α := α) (↑(↑(neg p) : ℤ) : α) (↑(neg p) : α)
have rw₃ : Eq.{u_1 + 1} (α := α) (-(↑p : α)) (-(↑p : α))
Tactic: rw [cast_neg, cast_neg, Int.cast_neg, PosNum.cast_to_int]
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
a : PosNum
⊢ sub' 1 (a + a) = (neg a).bit1
have rw : a.bit0.pred'.toZNumNeg = (neg a).bit1
Tactic: rw [PosNum.one_sub', a.bit0_of_bit0]
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
α : Type u_1
inst : AddGroupWithOne α
p : PosNum
⊢ (↑(pos p).bit0 : α) = HAdd.hAdd (α := α) (↑(pos p) : α) (↑(pos p) : α)
have rw : (↑p.bit0 : α) = HAdd.hAdd (α := α) (↑p : α) (↑p : α)
Tactic: rw [ZNum.bit0, cast_pos, cast_pos]
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
α : Type u_1
inst : AddGroupWithOne α
p : PosNum
⊢ (↑(neg p).bit0 : α) = HAdd.hAdd (α := α) (↑(neg p) : α) (↑(neg p) : α)
have rw : (↑(neg p.bit0) : α) = HAdd.hAdd (α := α) (↑(neg p) : α) (↑(neg p) : α)
Tactic: rw [ZNum.bit0, cast_neg, cast_neg, PosNum.cast_bit0, neg_add_rev]
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
α : Type u_1
inst : AddGroupWithOne α
p : PosNum
rw : (↑(neg p.bit0) : α) = HAdd.hAdd (α := α) (↑(neg p) : α) (↑(neg p) : α)
⊢ (↑(neg p).bit0 : α) = HAdd.hAdd (α := α) (↑(neg p) : α) (↑(neg p) : α)
have rw₁ : -(↑p.bit0 : α) = HAdd.hAdd (α := α) (↑(neg p) : α) (↑(neg p) : α)
Tactic: rw [ZNum.bit0, cast_neg, cast_neg, PosNum.cast_bit0, neg_add_rev]
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
α : Type u_1
inst : AddGroupWithOne α
p : PosNum
rw : (↑(neg p.bit0) : α) = HAdd.hAdd (α := α) (↑(neg p) : α) (↑(neg p) : α)
rw₁ : -(↑p.bit0 : α) = HAdd.hAdd (α := α) (↑(neg p) : α) (↑(neg p) : α)
⊢ (↑(neg p).bit0 : α) = HAdd.hAdd (α := α) (↑(neg p) : α) (↑(neg p) : α)
have rw₂ : -(↑p.bit0 : α) = HAdd.hAdd (α := α) (-(↑p : α)) (-(↑p : α))
Tactic: rw [ZNum.bit0, cast_neg, cast_neg, PosNum.cast_bit0, neg_add_rev]
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
α : Type u_1
inst : AddGroupWithOne α
p : PosNum
rw : (↑(neg p.bit0) : α) = HAdd.hAdd (α := α) (↑(neg p) : α) (↑(neg p) : α)
rw₁ : -(↑p.bit0 : α) = HAdd.hAdd (α := α) (↑(neg p) : α) (↑(neg p) : α)
rw₂ : -(↑p.bit0 : α) = HAdd.hAdd (α := α) (-(↑p : α)) (-(↑p : α))
⊢ (↑(neg p).bit0 : α) = HAdd.hAdd (α := α) (↑(neg p) : α) (↑(neg p) : α)
have rw₃ : -HAdd.hAdd (α := α) (↑p : α) (↑p : α) = HAdd.hAdd (α := α) (-(↑p : α)) (-(↑p : α))
Tactic: rw [ZNum.bit0, cast_neg, cast_neg, PosNum.cast_bit0, neg_add_rev]
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
α : Type u_1
inst : AddGroupWithOne α
p : PosNum
rw : (↑(neg p.bit0) : α) = HAdd.hAdd (α := α) (↑(neg p) : α) (↑(neg p) : α)
rw₁ : -(↑p.bit0 : α) = HAdd.hAdd (α := α) (↑(neg p) : α) (↑(neg p) : α)
rw₂ : -(↑p.bit0 : α) = HAdd.hAdd (α := α) (-(↑p : α)) (-(↑p : α))
rw₃ : -HAdd.hAdd (α := α) (↑p : α) (↑p : α) = HAdd.hAdd (α := α) (-(↑p : α)) (-(↑p : α))
⊢ (↑(neg p).bit0 : α) = HAdd.hAdd (α := α) (↑(neg p) : α) (↑(neg p) : α)
have rw₄ : HAdd.hAdd (α := α) (-(↑p : α)) (-(↑p : α)) = HAdd.hAdd (α := α) (-(↑p : α)) (-(↑p : α))
Tactic: rw [ZNum.bit0, cast_neg, cast_neg, PosNum.cast_bit0, neg_add_rev]
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
α : Type u_1
inst : AddGroupWithOne α
p : PosNum
⊢ (↑(pos p).bit1 : α) = HAdd.hAdd (α := α) (↑(pos p) : α) (↑(pos p) : α) + 1
have rw : (↑p.bit1 : α) = HAdd.hAdd (α := α) (↑p : α) (↑p : α) + 1
Tactic: rw [ZNum.bit1, cast_pos, cast_pos]
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
α : Type u_1
inst : AddGroupWithOne α
p : PosNum
⊢ (↑(neg p).bit1 : α) = HAdd.hAdd (α := α) (↑(neg p) : α) (↑(neg p) : α) + 1
have rw : -(↑(Num.casesOn (motive := fun (x : Num) ↦ PosNum) p.pred' 1 bit1) : α) = HAdd.hAdd (α := α) (-(↑p : α)) (-(↑p : α)) + 1
Tactic: rw [ZNum.bit1, cast_neg, cast_neg]
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
α : Type u_1
inst : AddGroupWithOne α
p : PosNum
⊢ -(↑(Num.casesOn (motive := fun (x : Num) ↦ PosNum) p.pred' 1 bit1) : α) =
    HAdd.hAdd (α := α) (-(↑p : α)) (-(↑p : α)) + 1
have zero : ∀ (e : p.pred' = Num.zero),
  -(↑(Num.casesOn (motive := fun (x : Num) ↦ PosNum) Num.zero 1 bit1) : α) =
    HAdd.hAdd (α := α) (-(↑p : α)) (-(↑p : α)) + 1
Tactic: rcases e : pred' p with - | a
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
α : Type u_1
inst : AddGroupWithOne α
p : PosNum
zero :
  ∀ (e : p.pred' = Num.zero),
    -(↑(Num.casesOn (motive := fun (x : Num) ↦ PosNum) Num.zero 1 bit1) : α) =
      HAdd.hAdd (α := α) (-(↑p : α)) (-(↑p : α)) + 1
⊢ -(↑(Num.casesOn (motive := fun (x : Num) ↦ PosNum) p.pred' 1 bit1) : α) =
    HAdd.hAdd (α := α) (-(↑p : α)) (-(↑p : α)) + 1
have pos : ∀ (a : PosNum) (e : p.pred' = Num.pos a),
  -(↑(Num.casesOn (motive := fun (x : Num) ↦ PosNum) (Num.pos a) 1 bit1) : α) =
    HAdd.hAdd (α := α) (-(↑p : α)) (-(↑p : α)) + 1
Tactic: rcases e : pred' p with - | a
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (hypothesis)
Goal:
α : Type u_1
inst : AddGroupWithOne α
p : PosNum
e : p.pred' = Num.zero
⊢ -(↑(Num.casesOn (motive := fun (x : Num) ↦ PosNum) Num.zero 1 bit1) : α) =
    HAdd.hAdd (α := α) (-(↑p : α)) (-(↑p : α)) + 1
have ep : p = Num.zero.succ'
Tactic: have ep : p = _ := (succ'_pred' p).symm.trans (congr_arg Num.succ' e)
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (hypothesis)
Goal:
α : Type u_1
inst : AddGroupWithOne α
p a : PosNum
e : p.pred' = Num.pos a
⊢ -(↑(Num.casesOn (motive := fun (x : Num) ↦ PosNum) (Num.pos a) 1 bit1) : α) =
    HAdd.hAdd (α := α) (-(↑p : α)) (-(↑p : α)) + 1
have ep : p = (Num.pos a).succ'
Tactic: have ep : p = _ := (succ'_pred' p).symm.trans (congr_arg Num.succ' e)
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (hypothesis)
Goal:
α : Type u_1
inst : AddGroupWithOne α
p : PosNum
e : p.pred' = Num.zero
ep : p = Num.zero.succ'
⊢ -(↑(Num.casesOn (motive := fun (x : Num) ↦ PosNum) Num.zero 1 bit1) : α) =
    HAdd.hAdd (α := α) (-(↑p : α)) (-(↑p : α)) + 1
have ep₁ : p = 1
Tactic: conv at ep => change p = 1
Cleared hypotheses: ep
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
α : Type u_1
inst : AddGroupWithOne α
p : PosNum
e : p.pred' = Num.zero
ep : p = 1
⊢ -(↑(Num.casesOn (motive := fun (x : Num) ↦ PosNum) Num.zero 1 bit1) : α) =
    HAdd.hAdd (α := α) (-(↑p : α)) (-(↑p : α)) + 1
have zero : ∀ (e : pred' 1 = Num.zero),
  -(↑(Num.casesOn (motive := fun (x : Num) ↦ PosNum) Num.zero 1 bit1) : α) =
    HAdd.hAdd (α := α) (-(↑1 : α)) (-(↑1 : α)) + 1
Tactic: subst p
Cleared hypotheses: p, e, ep
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
α : Type u_1
inst : AddGroupWithOne α
p a : PosNum
e : p.pred' = Num.pos a
ep : p = a.succ
⊢ -(↑(Num.casesOn (motive := fun (x : Num) ↦ PosNum) (Num.pos a) 1 bit1) : α) =
    HAdd.hAdd (α := α) (-(↑p : α)) (-(↑p : α)) + 1
have pos : ∀ (e : a.succ.pred' = Num.pos a),
  -(↑(Num.casesOn (motive := fun (x : Num) ↦ PosNum) (Num.pos a) 1 bit1) : α) =
    HAdd.hAdd (α := α) (-(↑a.succ : α)) (-(↑a.succ : α)) + 1
Tactic: subst p
Cleared hypotheses: p, e, ep
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (hypothesis)
Goal:
α : Type u_1
inst : AddGroupWithOne α
a : PosNum
e : a.succ.pred' = Num.pos a
⊢ -(↑(Num.casesOn (motive := fun (x : Num) ↦ PosNum) (Num.pos a) 1 bit1) : α) =
    HAdd.hAdd (α := α) (-(↑a.succ : α)) (-(↑a.succ : α)) + 1
have this : (↑(-(↑a : ℤ)) : α) = HAdd.hAdd (α := α) (-1) (↑(HAdd.hAdd (α := ℤ) (-(↑a : ℤ)) 1) : α)
Tactic: have : (↑(-↑a : ℤ) : α) = -1 + ↑(-↑a + 1 : ℤ) := by simp [add_comm (-↑a : ℤ) 1]
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
α : Type u_1
inst : AddGroupWithOne α
n : ZNum
| (↑n.bitm1 : α) = HAdd.hAdd (α := α) (↑n : α) (↑n : α) - 1
have lhs : (↑n.bitm1 : α)
Tactic: lhs
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
α : Type u_1
inst : AddGroupWithOne α
n : ZNum
| (↑n.bitm1 : α)
have rw : (↑(- -n).bitm1 : α)
Tactic: rw [← zneg_zneg n]
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
α : Type u_1
inst : AddGroupWithOne α
n : ZNum
| (↑n.bitm1 : α) = HAdd.hAdd (α := α) (↑n : α) (↑n : α) - 1
have rw : (↑(- -n).bitm1 : α)
Tactic: lhs
    rw [← zneg_zneg n]
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
α : Type u_1
inst : AddGroupWithOne α
n : ZNum
⊢ (↑n.bitm1 : α) = HAdd.hAdd (α := α) (↑n : α) (↑n : α) - 1
have conv : (↑(- -n).bitm1 : α) = HAdd.hAdd (α := α) (↑n : α) (↑n : α) - 1
Tactic: conv =>
    lhs
    rw [← zneg_zneg n]
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
α : Type u_1
inst : AddGroupWithOne α
n : ZNum
⊢ (↑(- -n).bitm1 : α) = HAdd.hAdd (α := α) (↑n : α) (↑n : α) - 1
have rw : -(HAdd.hAdd (α := α) (↑(-n) : α) (↑(-n) : α) + 1) = HAdd.hAdd (α := α) (↑n : α) (↑n : α) - 1
Tactic: rw [← zneg_bit1, cast_zneg, cast_bit1]
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (hypothesis)
Goal:
α : Type u_1
inst : AddGroupWithOne α
n : ZNum
⊢ -(HAdd.hAdd (α := α) (↑(-n) : α) (↑(-n) : α) + 1) = HAdd.hAdd (α := α) (↑n : α) (↑n : α) - 1
have this : Eq.{u_1 + 1} (α := α) (↑(HAdd.hAdd (α := ℤ) (-1) (↑n : ℤ) + (↑n : ℤ)) : α)
  (↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) (↑n : ℤ) + -1) : α)
Tactic: have : ((-1 + n + n : ℤ) : α) = (n + n + -1 : ℤ) := by simp [add_comm]
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
n : ZNum
⊢ n + 0 = n
have zero : zero + 0 = zero
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
n : ZNum
zero : ZNum.zero + 0 = ZNum.zero
⊢ n + 0 = n
have pos : ∀ (a : PosNum), pos a + 0 = pos a
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
n : ZNum
zero : ZNum.zero + 0 = ZNum.zero
pos : ∀ (a : PosNum), ZNum.pos a + 0 = ZNum.pos a
⊢ n + 0 = n
have neg : ∀ (a : PosNum), neg a + 0 = neg a
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
n : ZNum
⊢ 0 + n = n
have zero : 0 + zero = zero
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
n : ZNum
zero : 0 + ZNum.zero = ZNum.zero
⊢ 0 + n = n
have pos : ∀ (a : PosNum), 0 + pos a = pos a
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
n : ZNum
zero : 0 + ZNum.zero = ZNum.zero
pos : ∀ (a : PosNum), 0 + ZNum.pos a = ZNum.pos a
⊢ 0 + n = n
have neg : ∀ (a : PosNum), 0 + neg a = neg a
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
p : PosNum
⊢ neg p + 1 = (neg p).succ
have one : neg one + 1 = (neg one).succ
Tactic: cases p
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
p : PosNum
one : neg PosNum.one + 1 = (neg PosNum.one).succ
⊢ neg p + 1 = (neg p).succ
have bit1 : ∀ (a : PosNum), neg a.bit1 + 1 = (neg a.bit1).succ
Tactic: cases p
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
p : PosNum
one : neg PosNum.one + 1 = (neg PosNum.one).succ
bit1 : ∀ (a : PosNum), neg a.bit1 + 1 = (neg a.bit1).succ
⊢ neg p + 1 = (neg p).succ
have bit0 : ∀ (a : PosNum), neg a.bit0 + 1 = (neg a.bit0).succ
Tactic: cases p
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (hypothesis)
Goal:
p : PosNum
⊢ (↑p.bit0 : ZNum) = ZNum.pos p.bit0
have this : ZNum.bit0 (↑p : ZNum) = (ZNum.pos p).bit0
Tactic: have := congr_arg ZNum.bit0 (cast_to_znum p)
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
p : PosNum
this : ZNum.bit0 (↑p : ZNum) = (ZNum.pos p).bit0
⊢ (↑p.bit0 : ZNum) = ZNum.pos p.bit0
have rwa : ∀ (this : HAdd.hAdd (α := ZNum) (↑p : ZNum) (↑p : ZNum) = (ZNum.pos p).bit0), (↑p.bit0 : ZNum) = ZNum.pos p.bit0
Tactic: rwa [← ZNum.bit0_of_bit0] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (hypothesis)
Goal:
p : PosNum
⊢ (↑p.bit1 : ZNum) = ZNum.pos p.bit1
have this : ZNum.bit1 (↑p : ZNum) = (ZNum.pos p).bit1
Tactic: have := congr_arg ZNum.bit1 (cast_to_znum p)
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
p : PosNum
this : ZNum.bit1 (↑p : ZNum) = (ZNum.pos p).bit1
⊢ (↑p.bit1 : ZNum) = ZNum.pos p.bit1
have rwa : ∀ (this : HAdd.hAdd (α := ZNum) (↑p : ZNum) (↑p : ZNum) + 1 = (ZNum.pos p).bit1), (↑p.bit1 : ZNum) = ZNum.pos p.bit1
Tactic: rwa [← ZNum.bit1_of_bit1] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
α : Type u_1
inst : AddGroupWithOne α
a : PosNum
⊢ (↑(a.sub' 1) : α) = HSub.hSub (α := α) (↑a : α) (↑1 : α)
have rw : (↑(HSub.hSub (α := ℕ) (↑a : ℕ) 1) : α) = HSub.hSub (α := α) (↑a : α) (↑1 : α)
Tactic: rw [sub'_one, Num.cast_toZNum, ← Num.cast_to_nat, pred'_to_nat, ← Nat.sub_one]
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
α : Type u_1
inst : AddGroupWithOne α
b : PosNum
⊢ (↑(sub' 1 b) : α) = HSub.hSub (α := α) (↑1 : α) (↑b : α)
have rw : (↑(HSub.hSub (α := ℕ) (↑b : ℕ) 1) : α) = HSub.hSub (α := α) (↑b : α) (↑1 : α)
Tactic: rw [one_sub', Num.cast_toZNumNeg, ← neg_sub, neg_inj, ← Num.cast_to_nat, pred'_to_nat,
        ← Nat.sub_one]