awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Num.ZNum
Goal:
p : PosNum
this : ZNum.bit0 (↑p : ZNum) = (ZNum.pos p).bit0
rwa rwa₁ rwa₂ rwa₃ :
  ∀ (this : HAdd.hAdd (α := ZNum) (↑p : ZNum) (↑p : ZNum) = (ZNum.pos p).bit0), (↑p.bit0 : ZNum) = ZNum.pos p.bit0
⊢ (↑p.bit0 : ZNum) = ZNum.pos p.bit0

Tactic:
rwa [← ZNum.bit0_of_bit0] at this

Premises used: ZNum.bit0_of_bit0
-- Module: Mathlib.Data.Num.ZNum
Goal:
p : PosNum
⊢ ZNum.bit1 (↑p : ZNum) = (ZNum.pos p).bit1

Tactic:
have := congr_arg ZNum.bit1 (cast_to_znum p)
-- Module: Mathlib.Data.Num.ZNum
Goal:
p : PosNum
this : ZNum.bit1 (↑p : ZNum) = (ZNum.pos p).bit1
rwa rwa₁ rwa₂ rwa₃ :
  ∀ (this : HAdd.hAdd (α := ZNum) (↑p : ZNum) (↑p : ZNum) + 1 = (ZNum.pos p).bit1), (↑p.bit1 : ZNum) = ZNum.pos p.bit1
⊢ (↑p.bit1 : ZNum) = ZNum.pos p.bit1

Tactic:
rwa [← ZNum.bit1_of_bit1] at this

Premises used: ZNum.bit1_of_bit1
-- Module: Mathlib.Data.Num.ZNum
Goal:
α : Type u_1
inst : AddGroupWithOne α
a : PosNum
rw : (↑(HSub.hSub (α := ℕ) (↑a : ℕ) 1) : α) = HSub.hSub (α := α) (↑a : α) (↑1 : α)
⊢ (↑(a.sub' 1) : α) = HSub.hSub (α := α) (↑a : α) (↑1 : α)

Tactic:
rw [sub'_one, Num.cast_toZNum, ← Num.cast_to_nat, pred'_to_nat, ← Nat.sub_one]

Premises used: PosNum.pred'_to_nat, Num.cast_to_nat, Nat.sub_one, PosNum.sub'_one, Num.cast_toZNum
-- Module: Mathlib.Data.Num.ZNum
Goal:
α : Type u_1
inst : AddGroupWithOne α
a : PosNum
⊢ (↑(HSub.hSub (α := ℕ) (↑a : ℕ) 1) : α) = HSub.hSub (α := α) (↑a : α) (↑1 : α)

Tactic:
simp
-- Module: Mathlib.Data.Num.ZNum
Goal:
α : Type u_1
inst : AddGroupWithOne α
b : PosNum
rw : (↑(HSub.hSub (α := ℕ) (↑b : ℕ) 1) : α) = HSub.hSub (α := α) (↑b : α) (↑1 : α)
⊢ (↑(sub' 1 b) : α) = HSub.hSub (α := α) (↑1 : α) (↑b : α)

Tactic:
rw [one_sub', Num.cast_toZNumNeg, ← neg_sub, neg_inj, ← Num.cast_to_nat, pred'_to_nat,
        ← Nat.sub_one]

Premises used: neg_sub, PosNum.one_sub', PosNum.pred'_to_nat, Num.cast_to_nat, neg_inj, Nat.sub_one, Num.cast_toZNumNeg
-- Module: Mathlib.Data.Num.ZNum
Goal:
α : Type u_1
inst : AddGroupWithOne α
b : PosNum
⊢ (↑(HSub.hSub (α := ℕ) (↑b : ℕ) 1) : α) = HSub.hSub (α := α) (↑b : α) (↑1 : α)

Tactic:
simp
-- Module: Mathlib.Data.Num.ZNum
Goal:
α : Type u_1
inst : AddGroupWithOne α
a b : PosNum
rw :
  HSub.hSub (α := α) (↑a : α) (↑b : α) + HSub.hSub (α := α) (↑a : α) (↑b : α) =
    HSub.hSub (α := α) (↑a.bit0 : α) (↑b.bit0 : α)
⊢ (↑(a.bit0.sub' b.bit0) : α) = HSub.hSub (α := α) (↑a.bit0 : α) (↑b.bit0 : α)

Tactic:
rw [sub', ZNum.cast_bit0, cast_sub' a b]

Premises used: PosNum.sub', ZNum.cast_bit0
-- Module: Mathlib.Data.Num.ZNum
Goal:
α : Type u_1
inst : AddGroupWithOne α
a b : PosNum
⊢ (↑(HAdd.hAdd (α := ℤ) (↑a : ℤ) (-(↑b : ℤ)) + HAdd.hAdd (α := ℤ) (↑a : ℤ) (-(↑b : ℤ))) : α) =
    HAdd.hAdd (α := α) (↑a : α) (↑a : α) + HAdd.hAdd (α := α) (-(↑b : α)) (-(↑b : α))

Tactic:
simp [add_left_comm]

Premises used: add_left_comm
-- Module: Mathlib.Data.Num.ZNum
Goal:
α : Type u_1
inst : AddGroupWithOne α
a b : PosNum
⊢ (↑(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]
-- Module: Mathlib.Data.Num.ZNum
Goal:
α : Type u_1
inst : AddGroupWithOne α
a b : PosNum
this :
  (↑(HAdd.hAdd (α := ℤ) (↑a : ℤ) (-(↑b : ℤ)) + HAdd.hAdd (α := ℤ) (↑a : ℤ) (-(↑b : ℤ))) : α) =
    HAdd.hAdd (α := α) (↑a : α) (↑a : α) + HAdd.hAdd (α := α) (-(↑b : α)) (-(↑b : α))
⊢ HSub.hSub (α := α) (↑a : α) (↑b : α) + HSub.hSub (α := α) (↑a : α) (↑b : α) =
    HSub.hSub (α := α) (↑a.bit0 : α) (↑b.bit0 : α)

Tactic:
simpa [sub_eq_add_neg] using this

Premises used: sub_eq_add_neg
-- Module: Mathlib.Data.Num.ZNum
Goal:
α : Type u_1
inst : AddGroupWithOne α
a b : PosNum
rw :
  HSub.hSub (α := α) (↑a : α) (↑b : α) + HSub.hSub (α := α) (↑a : α) (↑b : α) - 1 =
    HSub.hSub (α := α) (↑a.bit0 : α) (↑b.bit1 : α)
⊢ (↑(a.bit0.sub' b.bit1) : α) = HSub.hSub (α := α) (↑a.bit0 : α) (↑b.bit1 : α)

Tactic:
rw [sub', ZNum.cast_bitm1, cast_sub' a b]

Premises used: PosNum.sub', ZNum.cast_bitm1
-- Module: Mathlib.Data.Num.ZNum
Goal:
α : Type u_1
inst : AddGroupWithOne α
a b : PosNum
⊢ Eq.{u_1 + 1} (α := α) (↑(-(↑b : ℤ) + ((↑a : ℤ) + HAdd.hAdd (α := ℤ) (-(↑b : ℤ)) (-1))) : α)
    (↑(HAdd.hAdd (α := ℤ) (↑a : ℤ) (-1) + HAdd.hAdd (α := ℤ) (-(↑b : ℤ)) (-(↑b : ℤ))) : α)

Tactic:
simp [add_comm, add_left_comm]

Premises used: add_left_comm, add_comm
-- Module: Mathlib.Data.Num.ZNum
Goal:
α : Type u_1
inst : AddGroupWithOne α
a b : PosNum
⊢ 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]
-- Module: Mathlib.Data.Num.ZNum
Goal:
α : Type u_1
inst : AddGroupWithOne α
a b : PosNum
this :
  Eq.{u_1 + 1} (α := α) (↑(-(↑b : ℤ) + ((↑a : ℤ) + HAdd.hAdd (α := ℤ) (-(↑b : ℤ)) (-1))) : α)
    (↑(HAdd.hAdd (α := ℤ) (↑a : ℤ) (-1) + HAdd.hAdd (α := ℤ) (-(↑b : ℤ)) (-(↑b : ℤ))) : α)
⊢ HSub.hSub (α := α) (↑a : α) (↑b : α) + HSub.hSub (α := α) (↑a : α) (↑b : α) - 1 =
    HSub.hSub (α := α) (↑a.bit0 : α) (↑b.bit1 : α)

Tactic:
simpa [sub_eq_add_neg] using this

Premises used: sub_eq_add_neg
-- Module: Mathlib.Data.Num.ZNum
Goal:
α : Type u_1
inst : AddGroupWithOne α
a b : PosNum
rw :
  HSub.hSub (α := α) (↑a : α) (↑b : α) + HSub.hSub (α := α) (↑a : α) (↑b : α) + 1 =
    HSub.hSub (α := α) (↑a.bit1 : α) (↑b.bit0 : α)
⊢ (↑(a.bit1.sub' b.bit0) : α) = HSub.hSub (α := α) (↑a.bit1 : α) (↑b.bit0 : α)

Tactic:
rw [sub', ZNum.cast_bit1, cast_sub' a b]

Premises used: PosNum.sub', ZNum.cast_bit1
-- Module: Mathlib.Data.Num.ZNum
Goal:
α : Type u_1
inst : AddGroupWithOne α
a b : PosNum
⊢ Eq.{u_1 + 1} (α := α) (↑(-(↑b : ℤ) + ((↑a : ℤ) + HAdd.hAdd (α := ℤ) (-(↑b : ℤ)) 1)) : α)
    (↑(HAdd.hAdd (α := ℤ) (↑a : ℤ) 1 + HAdd.hAdd (α := ℤ) (-(↑b : ℤ)) (-(↑b : ℤ))) : α)

Tactic:
simp [add_comm, add_left_comm]

Premises used: add_left_comm, add_comm
-- Module: Mathlib.Data.Num.ZNum
Goal:
α : Type u_1
inst : AddGroupWithOne α
a b : PosNum
⊢ 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]
-- Module: Mathlib.Data.Num.ZNum
Goal:
α : Type u_1
inst : AddGroupWithOne α
a b : PosNum
this :
  Eq.{u_1 + 1} (α := α) (↑(-(↑b : ℤ) + ((↑a : ℤ) + HAdd.hAdd (α := ℤ) (-(↑b : ℤ)) 1)) : α)
    (↑(HAdd.hAdd (α := ℤ) (↑a : ℤ) 1 + HAdd.hAdd (α := ℤ) (-(↑b : ℤ)) (-(↑b : ℤ))) : α)
⊢ HSub.hSub (α := α) (↑a : α) (↑b : α) + HSub.hSub (α := α) (↑a : α) (↑b : α) + 1 =
    HSub.hSub (α := α) (↑a.bit1 : α) (↑b.bit0 : α)

Tactic:
simpa [sub_eq_add_neg] using this

Premises used: sub_eq_add_neg
-- Module: Mathlib.Data.Num.ZNum
Goal:
α : Type u_1
inst : AddGroupWithOne α
a b : PosNum
rw :
  HSub.hSub (α := α) (↑a : α) (↑b : α) + HSub.hSub (α := α) (↑a : α) (↑b : α) =
    HSub.hSub (α := α) (↑a.bit1 : α) (↑b.bit1 : α)
⊢ (↑(a.bit1.sub' b.bit1) : α) = HSub.hSub (α := α) (↑a.bit1 : α) (↑b.bit1 : α)

Tactic:
rw [sub', ZNum.cast_bit0, cast_sub' a b]

Premises used: PosNum.sub', ZNum.cast_bit0
-- Module: Mathlib.Data.Num.ZNum
Goal:
α : Type u_1
inst : AddGroupWithOne α
a b : PosNum
⊢ (↑(-(↑b : ℤ) + HAdd.hAdd (α := ℤ) (↑a : ℤ) (-(↑b : ℤ))) : α) = (↑a : α) + HAdd.hAdd (α := α) (-(↑b : α)) (-(↑b : α))

Tactic:
simp [add_left_comm]

Premises used: add_left_comm
-- Module: Mathlib.Data.Num.ZNum
Goal:
α : Type u_1
inst : AddGroupWithOne α
a b : PosNum
⊢ (↑(-(↑b : ℤ) + HAdd.hAdd (α := ℤ) (↑a : ℤ) (-(↑b : ℤ))) : α) = (↑a : α) + HAdd.hAdd (α := α) (-(↑b : α)) (-(↑b : α))

Tactic:
have : ((-b + (a + -b) : ℤ) : α) = a + (-b + -b) := by simp [add_left_comm]
-- Module: Mathlib.Data.Num.ZNum
Goal:
α : Type u_1
inst : AddGroupWithOne α
a b : PosNum
this :
  (↑(-(↑b : ℤ) + HAdd.hAdd (α := ℤ) (↑a : ℤ) (-(↑b : ℤ))) : α) = (↑a : α) + HAdd.hAdd (α := α) (-(↑b : α)) (-(↑b : α))
⊢ HSub.hSub (α := α) (↑a : α) (↑b : α) + HSub.hSub (α := α) (↑a : α) (↑b : α) =
    HSub.hSub (α := α) (↑a.bit1 : α) (↑b.bit1 : α)

Tactic:
simpa [sub_eq_add_neg] using this

Premises used: sub_eq_add_neg
-- Module: Mathlib.Data.Num.ZNum
Goal:
n : PosNum
rw : Eq (α := ℕ) (↑n : ℕ) (↑n.pred'.succ' : ℕ)
rw₁ rw₂ : Eq (α := ℕ) (↑n : ℕ) (↑n : ℕ)
⊢ (↑n : ℕ) = HAdd.hAdd (α := ℕ) (↑n.pred' : ℕ) 1

Tactic:
rw [← Num.succ'_to_nat, n.succ'_pred']

Premises used: Num.succ'_to_nat, PosNum.succ'_pred'
-- Module: Mathlib.Data.Num.ZNum
Goal:
n : PosNum
rw : (↑(HAdd.hAdd (α := ℕ) (↑n.pred' : ℕ) 1) : ℤ) = HAdd.hAdd (α := ℤ) (↑(↑n.pred' : ℕ) : ℤ) 1
⊢ (↑n : ℤ) = HAdd.hAdd (α := ℤ) (↑(↑n.pred' : ℕ) : ℤ) 1

Tactic:
rw [← n.to_nat_to_int, to_nat_eq_succ_pred]

Premises used: PosNum.to_nat_to_int, PosNum.to_nat_eq_succ_pred
-- Module: Mathlib.Data.Num.ZNum
Goal:
n : PosNum
⊢ (↑(HAdd.hAdd (α := ℕ) (↑n.pred' : ℕ) 1) : ℤ) = HAdd.hAdd (α := ℤ) (↑(↑n.pred' : ℕ) : ℤ) 1

Tactic:
rfl
-- Module: Mathlib.Data.Num.ZNum
Goal:
p : PosNum
rw : (pos p).toZNumNeg = ZNum.neg p
⊢ (pos p).succ'.pred'.toZNumNeg = ZNum.neg p

Tactic:
rw [PosNum.pred'_succ']

Premises used: PosNum.pred'_succ'
-- Module: Mathlib.Data.Num.ZNum
Goal:
p : PosNum
⊢ (pos p).toZNumNeg = ZNum.neg p

Tactic:
rfl
-- Module: Mathlib.Data.Num.ZNum
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
rw₄ rw₅ : ZNum.pos p = ZNum.pos p
⊢ (ZNum.pos p).pred.succ = ZNum.pos p

Tactic:
rw [ZNum.pred, ← toZNum_succ, Num.succ, PosNum.succ'_pred', toZNum]

Premises used: ZNum.pred, PosNum.succ'_pred', Num.succ, Num.toZNum, Num.toZNum_succ
-- Module: Mathlib.Data.Num.ZNum
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
rw₃ rw₄ : (ofNat' n).toZNum.succ = (ofNat' n).toZNum.succ
⊢ (ofNat' (n + 1)).toZNum = (ofNat' n).toZNum + 1

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

Premises used: Num.add_one, Num.ofNat'_succ, Num.toZNum_succ, ZNum.add_one
-- Module: Mathlib.Data.Num.ZNum
Goal:
⊢ toZNum 0 = (HAdd.hAdd (α := Num) 0 1).toZNumNeg + 1

Tactic:
rfl
-- Module: Mathlib.Data.Num.ZNum
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
rw₆ rw₇ : (ofNat' n).succ.toZNumNeg = (ofNat' n).succ.toZNumNeg
⊢ (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]

Premises used: Num.toZNumNeg_succ, Num.add_one, Num.ofNat'_succ, Num.pred_succ, ZNum.add_one
-- Module: Mathlib.Data.Num.ZNum
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
rw₆ rw₇ : (ZNum.ofInt' (↑n : ℤ)).succ = (ZNum.ofInt' (↑n : ℤ)).succ
⊢ toZNum (↑(n + 1) : Num) = 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]

Premises used: Nat.cast_succ, Num.add_one, Num.succ_ofInt', Num.toZNum_succ, ZNum.add_one
-- Module: Mathlib.Data.Num.ZNum
Goal:
m : Num
p : PosNum
zero : Num.pos p = Num.zero ↔ ZNum.pos p = Num.zero.toZNum
pos : ∀ (a : PosNum), Num.pos p = Num.pos a ↔ ZNum.pos p = (Num.pos a).toZNum
⊢ Num.pos p = m ↔ ZNum.pos p = m.toZNum

Tactic:
cases m
-- Module: Mathlib.Data.Num.ZNum
Goal:
p : PosNum
zero : pos p = Num.zero → ZNum.pos p = Num.zero.toZNum
zero₁ : ZNum.pos p = Num.zero.toZNum → pos p = Num.zero
⊢ pos p = Num.zero ↔ ZNum.pos p = Num.zero.toZNum

Tactic:
constructor
-- Module: Mathlib.Data.Num.ZNum
Goal:
p a : PosNum
pos : Num.pos p = Num.pos a → ZNum.pos p = (Num.pos a).toZNum
pos₁ : ZNum.pos p = (Num.pos a).toZNum → Num.pos p = Num.pos a
⊢ Num.pos p = Num.pos a ↔ ZNum.pos p = (Num.pos a).toZNum

Tactic:
constructor
-- Module: Mathlib.Data.Num.ZNum
Goal:
p : PosNum
h : pos p = zero
⊢ ZNum.pos p = zero.toZNum

Tactic:
cases h
-- Module: Mathlib.Data.Num.ZNum
Goal:
p : PosNum
h : pos p = zero
⊢ ZNum.pos p = zero.toZNum

Tactic:
try cases h <;> rfl
-- Module: Mathlib.Data.Num.ZNum
Goal:
p : PosNum
h : ZNum.pos p = zero.toZNum
⊢ pos p = zero

Tactic:
cases h
-- Module: Mathlib.Data.Num.ZNum
Goal:
p : PosNum
h : ZNum.pos p = zero.toZNum
⊢ pos p = zero

Tactic:
try cases h <;> rfl
-- Module: Mathlib.Data.Num.ZNum
Goal:
p a : PosNum
h : Num.pos p = Num.pos a
pos : ZNum.pos p = (Num.pos p).toZNum
⊢ ZNum.pos p = (Num.pos a).toZNum

Tactic:
cases h
-- Module: Mathlib.Data.Num.ZNum
Goal:
p : PosNum
⊢ ZNum.pos p = (pos p).toZNum

Tactic:
rfl
-- Module: Mathlib.Data.Num.ZNum
Goal:
p a : PosNum
h : Num.pos p = Num.pos a
pos pos₁ pos₂ pos₃ : ZNum.pos p = (Num.pos p).toZNum
⊢ ZNum.pos p = (Num.pos a).toZNum

Tactic:
try cases h <;> rfl
-- Module: Mathlib.Data.Num.ZNum
Goal:
p a : PosNum
h : ZNum.pos p = (Num.pos a).toZNum
pos : Num.pos p = Num.pos p
⊢ Num.pos p = Num.pos a

Tactic:
cases h
-- Module: Mathlib.Data.Num.ZNum
Goal:
p : PosNum
⊢ pos p = pos p

Tactic:
rfl
-- Module: Mathlib.Data.Num.ZNum
Goal:
p a : PosNum
h : ZNum.pos p = (Num.pos a).toZNum
pos pos₁ pos₂ pos₃ : Num.pos p = Num.pos p
⊢ Num.pos p = Num.pos a

Tactic:
try cases h <;> rfl
-- Module: Mathlib.Data.Num.ZNum
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)
pos : ∀ (a : PosNum) (h : ZNum.neg p = (Num.pos a).toZNum), Num.pos a ∈ ofZNum' (ZNum.neg p)
⊢ m ∈ ofZNum' (ZNum.neg p)

Tactic:
cases m
-- Module: Mathlib.Data.Num.ZNum
Goal:
p : PosNum
h : ZNum.neg p = zero.toZNum
⊢ zero ∈ ofZNum' (ZNum.neg p)

Tactic:
cases h
-- Module: Mathlib.Data.Num.ZNum
Goal:
p a : PosNum
h : ZNum.neg p = (pos a).toZNum
⊢ pos a ∈ ofZNum' (ZNum.neg p)

Tactic:
cases h
-- Module: Mathlib.Data.Num.ZNum
Goal:
p : PosNum
rw : castNum <$> ofZNum' (ZNum.pos p) = toNat? (↑(↑p : ℕ) : ℤ)
⊢ castNum <$> ofZNum' (ZNum.pos p) = toNat? (↑p : ℤ)

Tactic:
rw [← PosNum.to_nat_to_int p]

Premises used: PosNum.to_nat_to_int
-- Module: Mathlib.Data.Num.ZNum
Goal:
p : PosNum
⊢ castNum <$> ofZNum' (ZNum.pos p) = toNat? (↑(↑p : ℕ) : ℤ)

Tactic:
rfl
-- Module: Mathlib.Data.Num.ZNum
Goal:
p : PosNum
rw : Eq (α := ℤ) (↑(↑p.pred'.succ' : ℕ) : ℤ) (↑p : ℤ)
⊢ Eq (α := ℤ) (↑(HAdd.hAdd (α := ℕ) (↑p.pred' : ℕ) 1) : ℤ) (↑p : ℤ)

Tactic:
rw [← succ'_to_nat]

Premises used: Num.succ'_to_nat
-- Module: Mathlib.Data.Num.ZNum
Goal:
p : PosNum
⊢ Eq (α := ℤ) (↑(↑p.pred'.succ' : ℕ) : ℤ) (↑p : ℤ)

Tactic:
simp
-- Module: Mathlib.Data.Num.ZNum
Goal:
p : PosNum
rw : (↑(ofZNum (ZNum.pos p)) : ℕ) = toNat (↑(↑p : ℕ) : ℤ)
⊢ (↑(ofZNum (ZNum.pos p)) : ℕ) = toNat (↑p : ℤ)

Tactic:
rw [← PosNum.to_nat_to_int p]

Premises used: PosNum.to_nat_to_int
-- Module: Mathlib.Data.Num.ZNum
Goal:
p : PosNum
⊢ (↑(ofZNum (ZNum.pos p)) : ℕ) = toNat (↑(↑p : ℕ) : ℤ)

Tactic:
rfl
-- Module: Mathlib.Data.Num.ZNum
Goal:
α : Type u_1
inst : AddMonoidWithOne α
n : ZNum
rw : Eq.{u_1 + 1} (α := α) (↑(↑(ofZNum n) : ℕ) : α) (↑(toNat (↑n : ℤ)) : α)
rw₁ rw₂ : Eq.{u_1 + 1} (α := α) (↑(toNat (↑n : ℤ)) : α) (↑(toNat (↑n : ℤ)) : α)
⊢ Eq.{u_1 + 1} (α := α) (↑(ofZNum n) : α) (↑(toNat (↑n : ℤ)) : α)

Tactic:
rw [← cast_to_nat, ofZNum_toNat]

Premises used: Num.cast_to_nat, Num.ofZNum_toNat
-- Module: Mathlib.Data.Num.ZNum
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 : ℕ)
rw₄ rw₅ : HSub.hSub (α := ℕ) (↑m : ℕ) (↑n : ℕ) = HSub.hSub (α := ℕ) (↑m : ℕ) (↑n : ℕ)
⊢ (↑(ofZNum (m.sub' n)) : ℕ) = HSub.hSub (α := ℕ) (↑m : ℕ) (↑n : ℕ)

Tactic:
rw [ofZNum_toNat, cast_sub', ← to_nat_to_int, ← to_nat_to_int, Int.toNat_sub]

Premises used: Num.cast_sub', Int.toNat_sub, Num.ofZNum_toNat, Num.to_nat_to_int
-- Module: Mathlib.Data.Num.ZNum
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) : α)
neg : ∀ (a : PosNum), (↑(0 + ZNum.neg a) : α) = HAdd.hAdd (α := α) (↑0 : α) (↑(ZNum.neg a) : α)
⊢ (↑(0 + a) : α) = HAdd.hAdd (α := α) (↑0 : α) (↑a : α)

Tactic:
cases a
-- Module: Mathlib.Data.Num.ZNum
Goal:
α : Type u_1
inst : AddGroupWithOne α
⊢ (↑(0 + zero) : α) = HAdd.hAdd (α := α) (↑0 : α) (↑zero : α)

Tactic:
(_root_.zero_add _).symm

Premises used: castZNum, ZNum.add, zero_add, Eq.symm
-- Module: Mathlib.Data.Num.ZNum
Goal:
α : Type u_1
inst : AddGroupWithOne α
⊢ (↑(0 + zero) : α) = HAdd.hAdd (α := α) (↑0 : α) (↑zero : α)

Tactic:
exact (_root_.zero_add _).symm

Premises used: zero_add, Eq.symm
-- Module: Mathlib.Data.Num.ZNum
Goal:
α : Type u_1
inst : AddGroupWithOne α
a : PosNum
⊢ (↑(0 + pos a) : α) = HAdd.hAdd (α := α) (↑0 : α) (↑(pos a) : α)

Tactic:
(_root_.zero_add _).symm

Premises used: castZNum, ZNum.add, zero_add, Eq.symm
-- Module: Mathlib.Data.Num.ZNum
Goal:
α : Type u_1
inst : AddGroupWithOne α
a : PosNum
⊢ (↑(0 + pos a) : α) = HAdd.hAdd (α := α) (↑0 : α) (↑(pos a) : α)

Tactic:
exact (_root_.zero_add _).symm

Premises used: zero_add, Eq.symm
-- Module: Mathlib.Data.Num.ZNum
Goal:
α : Type u_1
inst : AddGroupWithOne α
a : PosNum
⊢ (↑(0 + neg a) : α) = HAdd.hAdd (α := α) (↑0 : α) (↑(neg a) : α)

Tactic:
(_root_.zero_add _).symm

Premises used: castZNum, ZNum.add, zero_add, Eq.symm
-- Module: Mathlib.Data.Num.ZNum
Goal:
α : Type u_1
inst : AddGroupWithOne α
a : PosNum
⊢ (↑(0 + neg a) : α) = HAdd.hAdd (α := α) (↑0 : α) (↑(neg a) : α)

Tactic:
exact (_root_.zero_add _).symm

Premises used: zero_add, Eq.symm
-- Module: Mathlib.Data.Num.ZNum
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 : α)
neg : ∀ (a : PosNum), (↑(ZNum.neg a + 0) : α) = HAdd.hAdd (α := α) (↑(ZNum.neg a) : α) (↑0 : α)
⊢ (↑(b + 0) : α) = HAdd.hAdd (α := α) (↑b : α) (↑0 : α)

Tactic:
cases b
-- Module: Mathlib.Data.Num.ZNum
Goal:
α : Type u_1
inst : AddGroupWithOne α
⊢ (↑(zero + 0) : α) = HAdd.hAdd (α := α) (↑zero : α) (↑0 : α)

Tactic:
(_root_.add_zero _).symm

Premises used: castZNum, ZNum.add, add_zero, Eq.symm
-- Module: Mathlib.Data.Num.ZNum
Goal:
α : Type u_1
inst : AddGroupWithOne α
⊢ (↑(zero + 0) : α) = HAdd.hAdd (α := α) (↑zero : α) (↑0 : α)

Tactic:
exact (_root_.add_zero _).symm

Premises used: add_zero, Eq.symm
-- Module: Mathlib.Data.Num.ZNum
Goal:
α : Type u_1
inst : AddGroupWithOne α
a : PosNum
⊢ (↑(pos a + 0) : α) = HAdd.hAdd (α := α) (↑(pos a) : α) (↑0 : α)

Tactic:
(_root_.add_zero _).symm

Premises used: castZNum, ZNum.add, add_zero, Eq.symm
-- Module: Mathlib.Data.Num.ZNum
Goal:
α : Type u_1
inst : AddGroupWithOne α
a : PosNum
⊢ (↑(pos a + 0) : α) = HAdd.hAdd (α := α) (↑(pos a) : α) (↑0 : α)

Tactic:
exact (_root_.add_zero _).symm

Premises used: add_zero, Eq.symm
-- Module: Mathlib.Data.Num.ZNum
Goal:
α : Type u_1
inst : AddGroupWithOne α
a : PosNum
⊢ (↑(neg a + 0) : α) = HAdd.hAdd (α := α) (↑(neg a) : α) (↑0 : α)

Tactic:
(_root_.add_zero _).symm

Premises used: castZNum, ZNum.add, add_zero, Eq.symm
-- Module: Mathlib.Data.Num.ZNum
Goal:
α : Type u_1
inst : AddGroupWithOne α
a : PosNum
⊢ (↑(neg a + 0) : α) = HAdd.hAdd (α := α) (↑(neg a) : α) (↑0 : α)

Tactic:
exact (_root_.add_zero _).symm

Premises used: add_zero, Eq.symm
-- Module: Mathlib.Data.Num.ZNum
Goal:
α : Type u_1
inst : AddGroupWithOne α
a b : PosNum
⊢ (↑(pos a + neg b) : α) = HAdd.hAdd (α := α) (↑(pos a) : α) (↑(neg b) : α)

Tactic:
simpa only [sub_eq_add_neg] using PosNum.cast_sub' (α := α) _ _

Premises used: sub_eq_add_neg, PosNum.cast_sub'
-- Module: Mathlib.Data.Num.ZNum
Goal:
α : Type u_1
inst : AddGroupWithOne α
a b : PosNum
rw : HAdd.hAdd (α := α) (↑(↑b : ℤ) : α) (↑(-(↑a : ℤ)) : α) = (↑(HAdd.hAdd (α := ℤ) (-(↑a : ℤ)) (↑b : ℤ)) : α)
⊢ 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)]

Premises used: Int.cast_neg, castPosNum, Int.cast_add, PosNum.cast_to_int, Neg.neg
-- Module: Mathlib.Data.Num.ZNum
Goal:
α : Type u_1
inst : AddGroupWithOne α
a b : PosNum
⊢ HAdd.hAdd (α := α) (↑(↑b : ℤ) : α) (↑(-(↑a : ℤ)) : α) = (↑(HAdd.hAdd (α := ℤ) (-(↑a : ℤ)) (↑b : ℤ)) : α)

Tactic:
simp [add_comm]

Premises used: add_comm
-- Module: Mathlib.Data.Num.ZNum
Goal:
α : Type u_1
inst : AddGroupWithOne α
a b : PosNum
rw : -HAdd.hAdd (α := α) (↑a : α) (↑b : α) = HAdd.hAdd (α := α) (-(↑a : α)) (-(↑b : α))
rw₁ : HAdd.hAdd (α := α) (↑a : α) (↑b : α) = -HAdd.hAdd (α := α) (-(↑a : α)) (-(↑b : α))
rw₂ : HAdd.hAdd (α := α) (↑a : α) (↑b : α) = HAdd.hAdd (α := α) (- -(↑b : α)) (- -(↑a : α))
rw₃ : HAdd.hAdd (α := α) (↑a : α) (↑b : α) = HAdd.hAdd (α := α) (↑b : α) (- -(↑a : α))
rw₄ : HAdd.hAdd (α := α) (↑a : α) (↑b : α) = HAdd.hAdd (α := α) (↑b : α) (↑a : α)
rw₅ : HAdd.hAdd (α := α) (↑(↑a : ℤ) : α) (↑b : α) = HAdd.hAdd (α := α) (↑b : α) (↑(↑a : ℤ) : α)
rw₆ : HAdd.hAdd (α := α) (↑(↑a : ℤ) : α) (↑(↑b : ℤ) : α) = HAdd.hAdd (α := α) (↑(↑b : ℤ) : α) (↑(↑a : ℤ) : α)
rw₇ : (↑(HAdd.hAdd (α := ℤ) (↑a : ℤ) (↑b : ℤ)) : α) = HAdd.hAdd (α := α) (↑(↑b : ℤ) : α) (↑(↑a : ℤ) : α)
rw₈ : Eq.{u_1 + 1} (α := α) (↑(HAdd.hAdd (α := ℤ) (↑a : ℤ) (↑b : ℤ)) : α) (↑(HAdd.hAdd (α := ℤ) (↑b : ℤ) (↑a : ℤ)) : α)
rw₉ rw₁₀ :
  Eq.{u_1 + 1} (α := α) (↑(HAdd.hAdd (α := ℤ) (↑b : ℤ) (↑a : ℤ)) : α) (↑(HAdd.hAdd (α := ℤ) (↑b : ℤ) (↑a : ℤ)) : α)
⊢ -(↑(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]

Premises used: neg_add_rev, Int.cast_add, neg_neg, neg_eq_iff_eq_neg, PosNum.cast_to_int, PosNum.cast_add, add_comm
-- Module: Mathlib.Data.Num.ZNum
Goal:
α : Type u_1
inst : AddGroupWithOne α
n : ZNum
rw : (↑(n + 1) : α) = HAdd.hAdd (α := α) (↑n : α) 1
rw₁ : HAdd.hAdd (α := α) (↑n : α) (↑1 : α) = HAdd.hAdd (α := α) (↑n : α) 1
rw₂ rw₃ : HAdd.hAdd (α := α) (↑n : α) 1 = HAdd.hAdd (α := α) (↑n : α) 1
⊢ (↑n.succ : α) = HAdd.hAdd (α := α) (↑n : α) 1

Tactic:
rw [← add_one, cast_add, cast_one]

Premises used: ZNum.cast_add, ZNum.cast_one, ZNum.add_one
-- Module: Mathlib.Data.Num.ZNum
Goal:
a : ZNum
zero : (↑(0 * ZNum.zero) : ℤ) = HMul.hMul (α := ℤ) (↑0 : ℤ) (↑ZNum.zero : ℤ)
pos : ∀ (a : PosNum), (↑(0 * ZNum.pos a) : ℤ) = HMul.hMul (α := ℤ) (↑0 : ℤ) (↑(ZNum.pos a) : ℤ)
neg : ∀ (a : PosNum), (↑(0 * ZNum.neg a) : ℤ) = HMul.hMul (α := ℤ) (↑0 : ℤ) (↑(ZNum.neg a) : ℤ)
⊢ (↑(0 * a) : ℤ) = HMul.hMul (α := ℤ) (↑0 : ℤ) (↑a : ℤ)

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

Tactic:
(zero_mul _).symm

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

Tactic:
exact (zero_mul _).symm

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

Tactic:
(zero_mul _).symm

Premises used: castZNum, MulZeroClass.zero_mul, Eq.symm