awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Num.Prime
Goal:
n : PosNum
fuel : ℕ
ih :
  ∀ {k : PosNum} (h : Nat.sqrt (↑n : ℕ) < fuel + (↑k.bit1 : ℕ)),
    (↑(n.minFacAux fuel k) : ℕ) = Nat.minFacAux (↑n : ℕ) (↑k.bit1 : ℕ)
k : PosNum
h : Nat.sqrt (↑n : ℕ) < fuel + 1 + (↑k.bit1 : ℕ)
h_1 : ¬n < k.bit1 * k.bit1
h_2 : ¬k.bit1 ∣ n
h₁ : fuel + (↑k.succ.bit1 : ℕ) = (fuel + 1 + (↑k.bit1 : ℕ)).succ
⊢ Nat.sqrt (↑n : ℕ) < fuel + (↑k.succ.bit1 : ℕ)

Tactic:
convert! Nat.lt_succ_of_lt h using 1

Premises used: Nat.lt_succ_of_lt
-- Module: Mathlib.Data.Num.Prime
Goal:
n : PosNum
fuel : ℕ
ih :
  ∀ {k : PosNum} (h : Nat.sqrt (↑n : ℕ) < fuel + (↑k.bit1 : ℕ)),
    (↑(n.minFacAux fuel k) : ℕ) = Nat.minFacAux (↑n : ℕ) (↑k.bit1 : ℕ)
k : PosNum
h : Nat.sqrt (↑n : ℕ) < fuel + 1 + (↑k.bit1 : ℕ)
h_1 : ¬n < k.bit1 * k.bit1
h_2 : ¬k.bit1 ∣ n
neg : (↑k.succ.bit1 : ℕ) = HAdd.hAdd (α := ℕ) (↑k.bit1 : ℕ) 2
h₁ : fuel + (↑k.succ.bit1 : ℕ) = (fuel + 1 + (↑k.bit1 : ℕ)).succ
⊢ (↑(n.minFacAux fuel k.succ) : ℕ) = Nat.minFacAux (↑n : ℕ) (HAdd.hAdd (α := ℕ) (↑k.bit1 : ℕ) 2)

Tactic:
rw [ih] <;> [congr; convert! Nat.lt_succ_of_lt h using 1]

Premises used: Nat.lt_succ_of_lt
-- Module: Mathlib.Data.Num.Prime
Goal:
n : PosNum
fuel : ℕ
ih :
  ∀ {k : PosNum} (h : Nat.sqrt (↑n : ℕ) < fuel + (↑k.bit1 : ℕ)),
    (↑(n.minFacAux fuel k) : ℕ) = Nat.minFacAux (↑n : ℕ) (↑k.bit1 : ℕ)
k : PosNum
h : Nat.sqrt (↑n : ℕ) < fuel + 1 + (↑k.bit1 : ℕ)
h_1 : ¬n < k.bit1 * k.bit1
h_2 : ¬k.bit1 ∣ n
⊢ (↑k.succ.bit1 : ℕ) = HAdd.hAdd (α := ℕ) (↑k.bit1 : ℕ) 2

Tactic:
simp only [cast_bit1, cast_succ, Nat.succ_eq_add_one, add_assoc,
        add_left_comm, ← one_add_one_eq_two]

Premises used: PosNum.cast_bit1, Nat.succ_eq_add_one, add_left_comm, add_assoc, PosNum.cast_succ, one_add_one_eq_two
-- Module: Mathlib.Data.Num.Prime
Goal:
n : PosNum
fuel : ℕ
ih :
  ∀ {k : PosNum} (h : Nat.sqrt (↑n : ℕ) < fuel + (↑k.bit1 : ℕ)),
    (↑(n.minFacAux fuel k) : ℕ) = Nat.minFacAux (↑n : ℕ) (↑k.bit1 : ℕ)
k : PosNum
h : Nat.sqrt (↑n : ℕ) < fuel + 1 + (↑k.bit1 : ℕ)
h_1 : ¬n < k.bit1 * k.bit1
h_2 : ¬k.bit1 ∣ n
⊢ fuel + (↑k.succ.bit1 : ℕ) = (fuel + 1 + (↑k.bit1 : ℕ)).succ

Tactic:
simp only [cast_bit1, cast_succ, Nat.succ_eq_add_one, add_assoc,
        add_left_comm, ← one_add_one_eq_two]

Premises used: PosNum.cast_bit1, Nat.succ_eq_add_one, add_left_comm, add_assoc, PosNum.cast_succ, one_add_one_eq_two
-- Module: Mathlib.Data.Num.Prime
Goal:
n : PosNum
one : (↑PosNum.one.minFac : ℕ) = Nat.minFac (↑PosNum.one : ℕ)
bit1 : ∀ (n : PosNum), (↑n.bit1.minFac : ℕ) = Nat.minFac (↑n.bit1 : ℕ)
bit0 : ∀ (a : PosNum), (↑a.bit0.minFac : ℕ) = Nat.minFac (↑a.bit0 : ℕ)
⊢ (↑n.minFac : ℕ) = Nat.minFac (↑n : ℕ)

Tactic:
obtain - | n := n
-- Module: Mathlib.Data.Num.Prime
Goal:
⊢ (↑one.minFac : ℕ) = Nat.minFac (↑one : ℕ)

Tactic:
simp [minFac]

Premises used: PosNum.minFac
-- Module: Mathlib.Data.Num.Prime
Goal:
n : PosNum
bit1 : (↑(n.bit1.minFacAux (↑n : ℕ) 1) : ℕ) = Nat.minFacAux (↑n.bit1 : ℕ) 3
bit1₁ : ¬Dvd.dvd (α := ℕ) 2 (↑n.bit1 : ℕ)
⊢ (↑n.bit1.minFac : ℕ) = Nat.minFac (↑n.bit1 : ℕ)

Tactic:
rw [minFac, Nat.minFac_eq, if_neg]

Premises used: Nat.minFac_eq, PosNum.minFac, if_neg
-- Module: Mathlib.Data.Num.Prime
Goal:
n : PosNum
⊢ ¬Dvd.dvd (α := ℕ) 2 (↑n.bit1 : ℕ)

Tactic:
simp [← two_mul]

Premises used: two_mul
-- Module: Mathlib.Data.Num.Prime
Goal:
n : PosNum
bit1 : Nat.minFacAux (↑n.bit1 : ℕ) (↑(PosNum.bit1 1) : ℕ) = Nat.minFacAux (↑n.bit1 : ℕ) 3
bit1₁ : Nat.sqrt (↑n.bit1 : ℕ) < HAdd.hAdd (α := ℕ) (↑n : ℕ) (↑(PosNum.bit1 1) : ℕ)
⊢ (↑(n.bit1.minFacAux (↑n : ℕ) 1) : ℕ) = Nat.minFacAux (↑n.bit1 : ℕ) 3

Tactic:
rw [minFacAux_to_nat]

Premises used: PosNum.minFacAux_to_nat
-- Module: Mathlib.Data.Num.Prime
Goal:
n : PosNum
⊢ Nat.minFacAux (↑n.bit1 : ℕ) (↑(bit1 1) : ℕ) = Nat.minFacAux (↑n.bit1 : ℕ) 3

Tactic:
rfl
-- Module: Mathlib.Data.Num.Prime
Goal:
n : PosNum
bit1 :
  HAdd.hAdd (α := ℕ) (↑n : ℕ) (↑n : ℕ) + 1 <
    ((↑n : ℕ) + (HAdd.hAdd (α := ℕ) 1 1 + 1)) * ((↑n : ℕ) + (HAdd.hAdd (α := ℕ) 1 1 + 1))
⊢ (HAdd.hAdd (α := ℕ) (↑n : ℕ) (↑n : ℕ) + 1).sqrt < (↑n : ℕ) + (HAdd.hAdd (α := ℕ) 1 1 + 1)

Tactic:
rw [Nat.sqrt_lt]

Premises used: Nat.sqrt_lt
-- Module: Mathlib.Data.Num.Prime
Goal:
n : PosNum
⊢ HAdd.hAdd (α := ℕ) (↑n : ℕ) (↑n : ℕ) + 1 ≤ HAdd.hAdd (α := ℕ) (↑n : ℕ) (↑n : ℕ) + (↑n : ℕ)

Tactic:
simp
-- Module: Mathlib.Data.Num.Prime
Goal:
n : PosNum
⊢ HAdd.hAdd (α := ℕ) (↑n : ℕ) (↑n : ℕ) + (↑n : ℕ) = (↑n : ℕ) * (HAdd.hAdd (α := ℕ) 1 1 + 1)

Tactic:
simp only [mul_add, mul_one]

Premises used: mul_add, mul_one
-- Module: Mathlib.Data.Num.Prime
Goal:
n : PosNum
⊢ (↑n : ℕ) * (HAdd.hAdd (α := ℕ) 1 1 + 1) <
    ((↑n : ℕ) + (HAdd.hAdd (α := ℕ) 1 1 + 1)) * ((↑n : ℕ) + (HAdd.hAdd (α := ℕ) 1 1 + 1))

Tactic:
simp [mul_lt_mul]

Premises used: mul_lt_mul
-- Module: Mathlib.Data.Num.Prime
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)
by₂ :
  (↑n : ℕ) * (HAdd.hAdd (α := ℕ) 1 1 + 1) <
    ((↑n : ℕ) + (HAdd.hAdd (α := ℕ) 1 1 + 1)) * ((↑n : ℕ) + (HAdd.hAdd (α := ℕ) 1 1 + 1))
⊢ HAdd.hAdd (α := ℕ) (↑n : ℕ) (↑n : ℕ) + 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]

Premises used: castPosNum, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Data.Num.Prime
Goal:
a : PosNum
bit0 : Eq (α := ℕ) (↑2 : ℕ) 2
bit0₁ : Dvd.dvd (α := ℕ) 2 (↑a.bit0 : ℕ)
⊢ (↑a.bit0.minFac : ℕ) = Nat.minFac (↑a.bit0 : ℕ)

Tactic:
rw [minFac, Nat.minFac_eq, if_pos]

Premises used: Nat.minFac_eq, PosNum.minFac, if_pos
-- Module: Mathlib.Data.Num.Prime
Goal:
a : PosNum
⊢ Eq (α := ℕ) (↑2 : ℕ) 2

Tactic:
rfl
-- Module: Mathlib.Data.Num.Prime
Goal:
a : PosNum
⊢ Dvd.dvd (α := ℕ) 2 (↑a.bit0 : ℕ)

Tactic:
simp [← two_mul]

Premises used: two_mul
-- Module: Mathlib.Data.Num.Prime
Goal:
n : PosNum
⊢ n.bit0.Prime ↔ n = 1

Tactic:
Nat.prime_def_minFac.trans ((and_iff_right ?_).trans <| eq_comm.trans ?_)

Premises used: and_iff_right, eq_comm, PosNum.Prime, Iff.trans, Nat.prime_def_minFac
-- Module: Mathlib.Data.Num.Prime
Goal:
n : PosNum
refine_1 : LE.le (α := ℕ) 2 (↑n.bit0 : ℕ)
refine_2 : (↑n.bit0 : ℕ) = Nat.minFac (↑n.bit0 : ℕ) ↔ n = 1
⊢ n.bit0.Prime ↔ n = 1

Tactic:
refine Nat.prime_def_minFac.trans ((and_iff_right ?_).trans <| eq_comm.trans ?_)

Premises used: and_iff_right, eq_comm, Iff.trans, Nat.prime_def_minFac
-- Module: Mathlib.Data.Num.Prime
Goal:
n : PosNum
⊢ LE.le (α := ℕ) 2 (↑n.bit0 : ℕ)

Tactic:
add_le_add (Nat.succ_le_of_lt (to_nat_pos _)) (Nat.succ_le_of_lt (to_nat_pos _))

Premises used: castPosNum, Nat.succ_le_of_lt, add_le_add, PosNum.to_nat_pos
-- Module: Mathlib.Data.Num.Prime
Goal:
n : PosNum
⊢ LE.le (α := ℕ) 2 (↑n.bit0 : ℕ)

Tactic:
exact add_le_add (Nat.succ_le_of_lt (to_nat_pos _)) (Nat.succ_le_of_lt (to_nat_pos _))

Premises used: Nat.succ_le_of_lt, add_le_add, PosNum.to_nat_pos
-- Module: Mathlib.Data.Num.Prime
Goal:
n : PosNum
refine_2 : n.bit0 = n.bit0.minFac ↔ n = 1
⊢ (↑n.bit0 : ℕ) = Nat.minFac (↑n.bit0 : ℕ) ↔ n = 1

Tactic:
rw [← minFac_to_nat, to_nat_inj]

Premises used: PosNum.to_nat_inj, PosNum.minFac_to_nat
-- Module: Mathlib.Data.Num.Prime
Goal:
n : PosNum
⊢ n.bit0 = n.bit0.minFac ↔ n = 1

Tactic:
⟨bit0.inj, congr_arg _⟩

Premises used: congr_arg, PosNum.bit0.inj, Iff.intro
-- Module: Mathlib.Data.Num.Prime
Goal:
n : PosNum
⊢ n.bit0 = n.bit0.minFac ↔ n = 1

Tactic:
exact ⟨bit0.inj, congr_arg _⟩
-- Module: Mathlib.Data.Num.Prime
Goal:
n : PosNum
⊢ n.bit1.Prime ↔ n.bit1.minFacAux (↑n : ℕ) 1 = n.bit1

Tactic:
Nat.prime_def_minFac.trans ((and_iff_right ?_).trans ?_)

Premises used: and_iff_right, PosNum.Prime, Iff.trans, Nat.prime_def_minFac
-- Module: Mathlib.Data.Num.Prime
Goal:
n : PosNum
refine_1 : LE.le (α := ℕ) 2 (↑n.bit1 : ℕ)
refine_2 : Nat.minFac (↑n.bit1 : ℕ) = (↑n.bit1 : ℕ) ↔ n.bit1.minFacAux (↑n : ℕ) 1 = n.bit1
⊢ n.bit1.Prime ↔ n.bit1.minFacAux (↑n : ℕ) 1 = n.bit1

Tactic:
refine Nat.prime_def_minFac.trans ((and_iff_right ?_).trans ?_)

Premises used: and_iff_right, Iff.trans, Nat.prime_def_minFac
-- Module: Mathlib.Data.Num.Prime
Goal:
n : PosNum
⊢ LT.lt (α := ℕ) 0 (↑n : ℕ)

Tactic:
have := to_nat_pos n
-- Module: Mathlib.Data.Num.Prime
Goal:
n : PosNum
this : LT.lt (α := ℕ) 0 (↑n : ℕ)
⊢ 2 ≤ HAdd.hAdd (α := ℕ) (↑n : ℕ) (↑n : ℕ) + 1

Tactic:
lia
-- Module: Mathlib.Data.Num.Prime
Goal:
n : PosNum
refine_2 : n.bit1.minFac = n.bit1 ↔ n.bit1.minFacAux (↑n : ℕ) 1 = n.bit1
⊢ Nat.minFac (↑n.bit1 : ℕ) = (↑n.bit1 : ℕ) ↔ n.bit1.minFacAux (↑n : ℕ) 1 = n.bit1

Tactic:
rw [← minFac_to_nat, to_nat_inj]

Premises used: PosNum.to_nat_inj, PosNum.minFac_to_nat
-- Module: Mathlib.Data.Num.Prime
Goal:
n : PosNum
⊢ n.bit1.minFac = n.bit1 ↔ n.bit1.minFacAux (↑n : ℕ) 1 = n.bit1

Tactic:
rfl
-- Module: Mathlib.Data.Num.ZNum
Goal:
α : Type u_1
inst : Zero α
inst_1 : One α
inst_2 : Add α
inst_3 : Neg α
⊢ Eq.{u_1 + 1} (α := α) (↑0 : α) 0

Tactic:
rfl

Premises used: castZNum, rfl
-- Module: Mathlib.Data.Num.ZNum
Goal:
α : Type u_1
inst : Zero α
inst_1 : One α
inst_2 : Add α
inst_3 : Neg α
⊢ Eq.{u_1 + 1} (α := α) (↑zero : α) 0

Tactic:
rfl

Premises used: castZNum, rfl
-- Module: Mathlib.Data.Num.ZNum
Goal:
α : Type u_1
inst : Zero α
inst_1 : One α
inst_2 : Add α
inst_3 : Neg α
⊢ Eq.{u_1 + 1} (α := α) (↑1 : α) 1

Tactic:
rfl

Premises used: castZNum, castPosNum, rfl
-- Module: Mathlib.Data.Num.ZNum
Goal:
α : Type u_1
inst : Zero α
inst_1 : One α
inst_2 : Add α
inst_3 : Neg α
n : PosNum
⊢ Eq.{u_1 + 1} (α := α) (↑(pos n) : α) (↑n : α)

Tactic:
rfl

Premises used: castZNum, rfl
-- Module: Mathlib.Data.Num.ZNum
Goal:
α : Type u_1
inst : Zero α
inst_1 : One α
inst_2 : Add α
inst_3 : Neg α
n : PosNum
⊢ Eq.{u_1 + 1} (α := α) (↑(neg n) : α) (-(↑n : α))

Tactic:
rfl

Premises used: castZNum, rfl
-- Module: Mathlib.Data.Num.ZNum
Goal:
⊢ Eq (α := ZNum) (-0) 0

Tactic:
rfl

Premises used: ZNum.zNeg, rfl
-- Module: Mathlib.Data.Num.ZNum
Goal:
n : PosNum
⊢ -pos n = neg n

Tactic:
rfl

Premises used: ZNum.zNeg, rfl
-- Module: Mathlib.Data.Num.ZNum
Goal:
n : PosNum
⊢ -neg n = pos n

Tactic:
rfl

Premises used: ZNum.zNeg, rfl
-- Module: Mathlib.Data.Num.ZNum
Goal:
n : ZNum
zero : - -ZNum.zero = ZNum.zero
pos : ∀ (a : PosNum), - -ZNum.pos a = ZNum.pos a
neg : ∀ (a : PosNum), - -ZNum.neg a = ZNum.neg a
⊢ - -n = n

Tactic:
cases n
-- Module: Mathlib.Data.Num.ZNum
Goal:
⊢ - -zero = zero

Tactic:
rfl
-- Module: Mathlib.Data.Num.ZNum
Goal:
a : PosNum
⊢ - -pos a = pos a

Tactic:
rfl
-- Module: Mathlib.Data.Num.ZNum
Goal:
a : PosNum
⊢ - -neg a = neg a

Tactic:
rfl
-- Module: Mathlib.Data.Num.ZNum
Goal:
n : ZNum
zero : -ZNum.zero.bit1 = (-ZNum.zero).bitm1
pos : ∀ (a : PosNum), -(ZNum.pos a).bit1 = (-ZNum.pos a).bitm1
neg : ∀ (a : PosNum), -(ZNum.neg a).bit1 = (-ZNum.neg a).bitm1
⊢ -n.bit1 = (-n).bitm1

Tactic:
cases n
-- Module: Mathlib.Data.Num.ZNum
Goal:
⊢ -zero.bit1 = (-zero).bitm1

Tactic:
rfl
-- Module: Mathlib.Data.Num.ZNum
Goal:
a : PosNum
⊢ -(pos a).bit1 = (-pos a).bitm1

Tactic:
rfl
-- Module: Mathlib.Data.Num.ZNum
Goal:
a : PosNum
⊢ -(neg a).bit1 = (-neg a).bitm1

Tactic:
rfl
-- Module: Mathlib.Data.Num.ZNum
Goal:
n : ZNum
zero : -ZNum.zero.bitm1 = (-ZNum.zero).bit1
pos : ∀ (a : PosNum), -(ZNum.pos a).bitm1 = (-ZNum.pos a).bit1
neg : ∀ (a : PosNum), -(ZNum.neg a).bitm1 = (-ZNum.neg a).bit1
⊢ -n.bitm1 = (-n).bit1

Tactic:
cases n
-- Module: Mathlib.Data.Num.ZNum
Goal:
⊢ -zero.bitm1 = (-zero).bit1

Tactic:
rfl
-- Module: Mathlib.Data.Num.ZNum
Goal:
a : PosNum
⊢ -(pos a).bitm1 = (-pos a).bit1

Tactic:
rfl
-- Module: Mathlib.Data.Num.ZNum
Goal:
a : PosNum
⊢ -(neg a).bitm1 = (-neg a).bit1

Tactic:
rfl
-- Module: Mathlib.Data.Num.ZNum
Goal:
n : ZNum
zero : -ZNum.zero.succ = (-ZNum.zero).pred
pos : ∀ (a : PosNum), -(ZNum.pos a).succ = (-ZNum.pos a).pred
neg : ∀ (a : PosNum), -(ZNum.neg a).succ = (-ZNum.neg a).pred
⊢ -n.succ = (-n).pred

Tactic:
cases n
-- Module: Mathlib.Data.Num.ZNum
Goal:
⊢ -zero.succ = (-zero).pred

Tactic:
rfl
-- Module: Mathlib.Data.Num.ZNum
Goal:
⊢ -zero.succ = (-zero).pred

Tactic:
{ rfl }
-- Module: Mathlib.Data.Num.ZNum
Goal:
⊢ -zero.succ = (-zero).pred

Tactic:
try { rfl }
-- Module: Mathlib.Data.Num.ZNum
Goal:
a : PosNum
⊢ -(pos a).succ = (-pos a).pred

Tactic:
rfl
-- Module: Mathlib.Data.Num.ZNum
Goal:
a : PosNum
⊢ -(pos a).succ = (-pos a).pred

Tactic:
{ rfl }
-- Module: Mathlib.Data.Num.ZNum
Goal:
a : PosNum
⊢ -(pos a).succ = (-pos a).pred

Tactic:
try { rfl }
-- Module: Mathlib.Data.Num.ZNum
Goal:
a : PosNum
neg : a.pred'.toZNum = (-ZNum.neg a).pred
⊢ -(ZNum.neg a).succ = (-ZNum.neg a).pred

Tactic:
rw [succ, Num.zneg_toZNumNeg]

Premises used: ZNum.succ, Num.zneg_toZNumNeg
-- Module: Mathlib.Data.Num.ZNum
Goal:
a : PosNum
⊢ a.pred'.toZNum = (-neg a).pred

Tactic:
rfl
-- Module: Mathlib.Data.Num.ZNum
Goal:
n : ZNum
rw : -n.pred = - -(-n).succ
rw₁ : -n.pred = -(- -n).pred
rw₂ rw₃ : -n.pred = -n.pred
⊢ -n.pred = (-n).succ

Tactic:
rw [← zneg_zneg (succ (-n)), zneg_succ, zneg_zneg]

Premises used: ZNum.zneg_succ, ZNum.succ, Neg.neg, ZNum.zneg_zneg
-- Module: Mathlib.Data.Num.ZNum
Goal:
p : PosNum
rw : natAbs (↑p : ℤ) = natAbs (-(↑p : ℤ))
rw₁ rw₂ : natAbs (↑p : ℤ) = natAbs (↑p : ℤ)
⊢ natAbs (↑(↑p : ℕ) : ℤ) = natAbs (-(↑p : ℤ))

Tactic:
rw [p.to_nat_to_int, Int.natAbs_neg]

Premises used: PosNum.to_nat_to_int, Int.natAbs_neg
-- Module: Mathlib.Data.Num.ZNum
Goal:
α : Type u_1
inst : AddGroupWithOne α
rw : Eq.{u_1 + 1} (α := α) (↑0 : α) (↑0 : α)
rw₁ : Eq.{u_1 + 1} (α := α) (↑0 : α) 0
rw₂ rw₃ : Eq.{u_1 + 1} (α := α) 0 0
⊢ Eq.{u_1 + 1} (α := α) (↑(↑0 : ℤ) : α) (↑0 : α)

Tactic:
rw [cast_zero, cast_zero, Int.cast_zero]

Premises used: Int.cast_zero, ZNum.cast_zero
-- Module: Mathlib.Data.Num.ZNum
Goal:
α : Type u_1
inst : AddGroupWithOne α
p : PosNum
rw : Eq.{u_1 + 1} (α := α) (↑(↑p : ℤ) : α) (↑(pos p) : α)
rw₁ : Eq.{u_1 + 1} (α := α) (↑(↑p : ℤ) : α) (↑p : α)
rw₂ rw₃ : Eq.{u_1 + 1} (α := α) (↑p : α) (↑p : α)
⊢ Eq.{u_1 + 1} (α := α) (↑(↑(pos p) : ℤ) : α) (↑(pos p) : α)

Tactic:
rw [cast_pos, cast_pos, PosNum.cast_to_int]

Premises used: PosNum.cast_to_int, ZNum.cast_pos
-- Module: Mathlib.Data.Num.ZNum
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 : α))
rw₃ rw₄ : Eq.{u_1 + 1} (α := α) (-(↑p : α)) (-(↑p : α))
⊢ Eq.{u_1 + 1} (α := α) (↑(↑(neg p) : ℤ) : α) (↑(neg p) : α)

Tactic:
rw [cast_neg, cast_neg, Int.cast_neg, PosNum.cast_to_int]

Premises used: Int.cast_neg, ZNum.cast_neg, PosNum.cast_to_int
-- Module: Mathlib.Data.Num.ZNum
Goal:
a : PosNum
rw : a.bit0.pred'.toZNumNeg = (neg a).bit1
⊢ sub' 1 (a + a) = (neg a).bit1

Tactic:
rw [PosNum.one_sub', a.bit0_of_bit0]

Premises used: PosNum.one_sub', PosNum.bit0_of_bit0
-- Module: Mathlib.Data.Num.ZNum
Goal:
a : PosNum
⊢ a.bit0.pred'.toZNumNeg = (neg a).bit1

Tactic:
rfl
-- Module: Mathlib.Data.Num.ZNum
Goal:
α : Type u_1
inst : AddGroupWithOne α
p : PosNum
rw : (↑p.bit0 : α) = HAdd.hAdd (α := α) (↑p : α) (↑p : α)
⊢ (↑(pos p).bit0 : α) = HAdd.hAdd (α := α) (↑(pos p) : α) (↑(pos p) : α)

Tactic:
rw [ZNum.bit0, cast_pos, cast_pos]

Premises used: ZNum.bit0, ZNum.cast_pos
-- Module: Mathlib.Data.Num.ZNum
Goal:
α : Type u_1
inst : AddGroupWithOne α
p : PosNum
⊢ (↑p.bit0 : α) = HAdd.hAdd (α := α) (↑p : α) (↑p : α)

Tactic:
rfl
-- Module: Mathlib.Data.Num.ZNum
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 : α))
rw₄ rw₅ : HAdd.hAdd (α := α) (-(↑p : α)) (-(↑p : α)) = HAdd.hAdd (α := α) (-(↑p : α)) (-(↑p : α))
⊢ (↑(neg p).bit0 : α) = HAdd.hAdd (α := α) (↑(neg p) : α) (↑(neg p) : α)

Tactic:
rw [ZNum.bit0, cast_neg, cast_neg, PosNum.cast_bit0, neg_add_rev]

Premises used: neg_add_rev, ZNum.cast_neg, ZNum.bit0, PosNum.cast_bit0
-- Module: Mathlib.Data.Num.ZNum
Goal:
α : Type u_1
inst : AddGroupWithOne α
⊢ (↑(ZNum.bit1 0) : α) = HAdd.hAdd (α := α) (↑0 : α) (↑0 : α) + 1

Tactic:
simp [ZNum.bit1]

Premises used: ZNum.bit1
-- Module: Mathlib.Data.Num.ZNum
Goal:
α : Type u_1
inst : AddGroupWithOne α
p : PosNum
rw : (↑p.bit1 : α) = HAdd.hAdd (α := α) (↑p : α) (↑p : α) + 1
⊢ (↑(pos p).bit1 : α) = HAdd.hAdd (α := α) (↑(pos p) : α) (↑(pos p) : α) + 1

Tactic:
rw [ZNum.bit1, cast_pos, cast_pos]

Premises used: ZNum.bit1, ZNum.cast_pos
-- Module: Mathlib.Data.Num.ZNum
Goal:
α : Type u_1
inst : AddGroupWithOne α
p : PosNum
⊢ (↑p.bit1 : α) = HAdd.hAdd (α := α) (↑p : α) (↑p : α) + 1

Tactic:
rfl
-- Module: Mathlib.Data.Num.ZNum
Goal:
α : Type u_1
inst : AddGroupWithOne α
p : PosNum
rw :
  -(↑(Num.casesOn (motive := fun (x : Num) ↦ PosNum) p.pred' 1 bit1) : α) =
    HAdd.hAdd (α := α) (-(↑p : α)) (-(↑p : α)) + 1
⊢ (↑(neg p).bit1 : α) = HAdd.hAdd (α := α) (↑(neg p) : α) (↑(neg p) : α) + 1

Tactic:
rw [ZNum.bit1, cast_neg, cast_neg]

Premises used: ZNum.bit1, ZNum.cast_neg
-- Module: Mathlib.Data.Num.ZNum
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
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
⊢ -(↑(Num.casesOn (motive := fun (x : Num) ↦ PosNum) p.pred' 1 bit1) : α) =
    HAdd.hAdd (α := α) (-(↑p : α)) (-(↑p : α)) + 1

Tactic:
rcases e : pred' p with - | a

Premises used: PosNum.pred'
-- Module: Mathlib.Data.Num.ZNum
Goal:
α : Type u_1
inst : AddGroupWithOne α
p : PosNum
e : p.pred' = Num.zero
⊢ p = Num.zero.succ'

Tactic:
have ep : p = _ := (succ'_pred' p).symm.trans (congr_arg Num.succ' e)
-- Module: Mathlib.Data.Num.ZNum
Goal:
α : Type u_1
inst : AddGroupWithOne α
p a : PosNum
e : p.pred' = Num.pos a
⊢ p = (Num.pos a).succ'

Tactic:
have ep : p = _ := (succ'_pred' p).symm.trans (congr_arg Num.succ' e)
-- Module: Mathlib.Data.Num.ZNum
Goal:
α : Type u_1
inst : AddGroupWithOne α
p : PosNum
e : p.pred' = Num.zero
ep : p = Num.zero.succ'
⊢ p = 1

Tactic:
conv at ep => change p = 1
-- Module: Mathlib.Data.Num.ZNum
Goal:
α : Type u_1
inst : AddGroupWithOne α
p : PosNum
e : p.pred' = Num.zero
ep : p = 1
zero :
  ∀ (e : pred' 1 = Num.zero),
    -(↑(Num.casesOn (motive := fun (x : Num) ↦ PosNum) Num.zero 1 bit1) : α) =
      HAdd.hAdd (α := α) (-(↑1 : α)) (-(↑1 : α)) + 1
⊢ -(↑(Num.casesOn (motive := fun (x : Num) ↦ PosNum) Num.zero 1 bit1) : α) =
    HAdd.hAdd (α := α) (-(↑p : α)) (-(↑p : α)) + 1

Tactic:
subst p
-- Module: Mathlib.Data.Num.ZNum
Goal:
α : Type u_1
inst : AddGroupWithOne α
e : pred' 1 = Num.zero
⊢ -(↑(Num.casesOn (motive := fun (x : Num) ↦ PosNum) Num.zero 1 bit1) : α) =
    HAdd.hAdd (α := α) (-(↑1 : α)) (-(↑1 : α)) + 1

Tactic:
simp
-- Module: Mathlib.Data.Num.ZNum
Goal:
α : Type u_1
inst : AddGroupWithOne α
p a : PosNum
e : p.pred' = Num.pos a
ep : p = a.succ
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
⊢ -(↑(Num.casesOn (motive := fun (x : Num) ↦ PosNum) (Num.pos a) 1 bit1) : α) =
    HAdd.hAdd (α := α) (-(↑p : α)) (-(↑p : α)) + 1

Tactic:
subst p
-- Module: Mathlib.Data.Num.ZNum
Goal:
α : Type u_1
inst : AddGroupWithOne α
a : PosNum
e : a.succ.pred' = Num.pos a
⊢ (↑(-(↑a : ℤ)) : α) = HAdd.hAdd (α := α) (-1) (↑(HAdd.hAdd (α := ℤ) (-(↑a : ℤ)) 1) : α)

Tactic:
simp [add_comm (-↑a : ℤ) 1]

Premises used: add_comm, OfNat.ofNat, Neg.neg
-- Module: Mathlib.Data.Num.ZNum
Goal:
α : Type u_1
inst : AddGroupWithOne α
a : PosNum
e : a.succ.pred' = Num.pos a
⊢ (↑(-(↑a : ℤ)) : α) = HAdd.hAdd (α := α) (-1) (↑(HAdd.hAdd (α := ℤ) (-(↑a : ℤ)) 1) : α)

Tactic:
have : (↑(-↑a : ℤ) : α) = -1 + ↑(-↑a + 1 : ℤ) := by simp [add_comm (-↑a : ℤ) 1]
-- Module: Mathlib.Data.Num.ZNum
Goal:
α : Type u_1
inst : AddGroupWithOne α
a : PosNum
e : a.succ.pred' = Num.pos a
this : (↑(-(↑a : ℤ)) : α) = HAdd.hAdd (α := α) (-1) (↑(HAdd.hAdd (α := ℤ) (-(↑a : ℤ)) 1) : α)
⊢ -(↑(Num.casesOn (motive := fun (x : Num) ↦ PosNum) (Num.pos a) 1 bit1) : α) =
    HAdd.hAdd (α := α) (-(↑a.succ : α)) (-(↑a.succ : α)) + 1

Tactic:
simpa using this
-- Module: Mathlib.Data.Num.ZNum
Goal:
α : Type u_1
inst : AddGroupWithOne α
n : ZNum
lhs : (↑n.bitm1 : α)
| (↑n.bitm1 : α) = HAdd.hAdd (α := α) (↑n : α) (↑n : α) - 1

Tactic:
lhs
-- Module: Mathlib.Data.Num.ZNum
Goal:
α : Type u_1
inst : AddGroupWithOne α
n : ZNum
rw : (↑(- -n).bitm1 : α)
| (↑n.bitm1 : α)

Tactic:
rw [← zneg_zneg n]

Premises used: ZNum.zneg_zneg
-- Module: Mathlib.Data.Num.ZNum
Goal:
α : Type u_1
inst : AddGroupWithOne α
n : ZNum
rw : (↑(- -n).bitm1 : α)
| (↑n.bitm1 : α) = HAdd.hAdd (α := α) (↑n : α) (↑n : α) - 1

Tactic:
lhs
    rw [← zneg_zneg n]

Premises used: ZNum.zneg_zneg
-- Module: Mathlib.Data.Num.ZNum
Goal:
α : Type u_1
inst : AddGroupWithOne α
n : ZNum
conv : (↑(- -n).bitm1 : α) = HAdd.hAdd (α := α) (↑n : α) (↑n : α) - 1
⊢ (↑n.bitm1 : α) = HAdd.hAdd (α := α) (↑n : α) (↑n : α) - 1

Tactic:
conv =>
    lhs
    rw [← zneg_zneg n]

Premises used: ZNum.zneg_zneg
-- Module: Mathlib.Data.Num.ZNum
Goal:
α : Type u_1
inst : AddGroupWithOne α
n : ZNum
rw : -(HAdd.hAdd (α := α) (↑(-n) : α) (↑(-n) : α) + 1) = HAdd.hAdd (α := α) (↑n : α) (↑n : α) - 1
⊢ (↑(- -n).bitm1 : α) = HAdd.hAdd (α := α) (↑n : α) (↑n : α) - 1

Tactic:
rw [← zneg_bit1, cast_zneg, cast_bit1]

Premises used: ZNum.cast_zneg, ZNum.zneg_bit1, ZNum.cast_bit1
-- Module: Mathlib.Data.Num.ZNum
Goal:
α : Type u_1
inst : AddGroupWithOne α
n : ZNum
⊢ Eq.{u_1 + 1} (α := α) (↑(HAdd.hAdd (α := ℤ) (-1) (↑n : ℤ) + (↑n : ℤ)) : α)
    (↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) (↑n : ℤ) + -1) : α)

Tactic:
simp [add_comm]

Premises used: add_comm
-- Module: Mathlib.Data.Num.ZNum
Goal:
α : Type u_1
inst : AddGroupWithOne α
n : ZNum
⊢ 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]
-- Module: Mathlib.Data.Num.ZNum
Goal:
α : Type u_1
inst : AddGroupWithOne α
n : ZNum
this :
  Eq.{u_1 + 1} (α := α) (↑(HAdd.hAdd (α := ℤ) (-1) (↑n : ℤ) + (↑n : ℤ)) : α)
    (↑(HAdd.hAdd (α := ℤ) (↑n : ℤ) (↑n : ℤ) + -1) : α)
⊢ -(HAdd.hAdd (α := α) (↑(-n) : α) (↑(-n) : α) + 1) = HAdd.hAdd (α := α) (↑n : α) (↑n : α) - 1

Tactic:
simpa [sub_eq_add_neg] using this

Premises used: sub_eq_add_neg
-- Module: Mathlib.Data.Num.ZNum
Goal:
n : ZNum
zero : ZNum.zero + 0 = ZNum.zero
pos : ∀ (a : PosNum), ZNum.pos a + 0 = ZNum.pos a
neg : ∀ (a : PosNum), ZNum.neg a + 0 = ZNum.neg a
⊢ n + 0 = n

Tactic:
cases n
-- Module: Mathlib.Data.Num.ZNum
Goal:
⊢ zero + 0 = zero

Tactic:
rfl
-- Module: Mathlib.Data.Num.ZNum
Goal:
a : PosNum
⊢ pos a + 0 = pos a

Tactic:
rfl
-- Module: Mathlib.Data.Num.ZNum
Goal:
a : PosNum
⊢ neg a + 0 = neg a

Tactic:
rfl
-- Module: Mathlib.Data.Num.ZNum
Goal:
n : ZNum
zero : 0 + ZNum.zero = ZNum.zero
pos : ∀ (a : PosNum), 0 + ZNum.pos a = ZNum.pos a
neg : ∀ (a : PosNum), 0 + ZNum.neg a = ZNum.neg a
⊢ 0 + n = n

Tactic:
cases n
-- Module: Mathlib.Data.Num.ZNum
Goal:
⊢ 0 + zero = zero

Tactic:
rfl
-- Module: Mathlib.Data.Num.ZNum
Goal:
a : PosNum
⊢ 0 + pos a = pos a

Tactic:
rfl
-- Module: Mathlib.Data.Num.ZNum
Goal:
a : PosNum
⊢ 0 + neg a = neg a

Tactic:
rfl
-- Module: Mathlib.Data.Num.ZNum
Goal:
p : PosNum
one : neg PosNum.one + 1 = (neg PosNum.one).succ
bit1 : ∀ (a : PosNum), neg a.bit1 + 1 = (neg a.bit1).succ
bit0 : ∀ (a : PosNum), neg a.bit0 + 1 = (neg a.bit0).succ
⊢ neg p + 1 = (neg p).succ

Tactic:
cases p
-- Module: Mathlib.Data.Num.ZNum
Goal:
⊢ neg one + 1 = (neg one).succ

Tactic:
rfl
-- Module: Mathlib.Data.Num.ZNum
Goal:
a : PosNum
⊢ neg a.bit1 + 1 = (neg a.bit1).succ

Tactic:
rfl
-- Module: Mathlib.Data.Num.ZNum
Goal:
a : PosNum
⊢ neg a.bit0 + 1 = (neg a.bit0).succ

Tactic:
rfl
-- Module: Mathlib.Data.Num.ZNum
Goal:
p : PosNum
⊢ ZNum.bit0 (↑p : ZNum) = (ZNum.pos p).bit0

Tactic:
have := congr_arg ZNum.bit0 (cast_to_znum p)