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
rw : -HAdd.hAdd (α := α) (↑a : α) (↑b : α) = HAdd.hAdd (α := α) (-(↑a : α)) (-(↑b : α))
⊢ -(↑(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]
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
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 : α))
⊢ -(↑(a + b) : α) = HAdd.hAdd (α := α) (-(↑a : α)) (-(↑b : α))
have rw₂ : HAdd.hAdd (α := α) (↑a : α) (↑b : α) = HAdd.hAdd (α := α) (- -(↑b : α)) (- -(↑a : α))
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]
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
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 : α))
⊢ -(↑(a + b) : α) = HAdd.hAdd (α := α) (-(↑a : α)) (-(↑b : α))
have rw₃ : HAdd.hAdd (α := α) (↑a : α) (↑b : α) = HAdd.hAdd (α := α) (↑b : α) (- -(↑a : α))
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]
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
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 : α))
⊢ -(↑(a + b) : α) = HAdd.hAdd (α := α) (-(↑a : α)) (-(↑b : α))
have rw₄ : HAdd.hAdd (α := α) (↑a : α) (↑b : α) = HAdd.hAdd (α := α) (↑b : α) (↑a : α)
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]
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
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 : α)
⊢ -(↑(a + b) : α) = HAdd.hAdd (α := α) (-(↑a : α)) (-(↑b : α))
have rw₅ : HAdd.hAdd (α := α) (↑(↑a : ℤ) : α) (↑b : α) = HAdd.hAdd (α := α) (↑b : α) (↑(↑a : ℤ) : α)
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]
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
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 : ℤ) : α)
⊢ -(↑(a + b) : α) = HAdd.hAdd (α := α) (-(↑a : α)) (-(↑b : α))
have rw₆ : HAdd.hAdd (α := α) (↑(↑a : ℤ) : α) (↑(↑b : ℤ) : α) = HAdd.hAdd (α := α) (↑(↑b : ℤ) : α) (↑(↑a : ℤ) : α)
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]
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
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 : ℤ) : α)
⊢ -(↑(a + b) : α) = HAdd.hAdd (α := α) (-(↑a : α)) (-(↑b : α))
have rw₇ : (↑(HAdd.hAdd (α := ℤ) (↑a : ℤ) (↑b : ℤ)) : α) = HAdd.hAdd (α := α) (↑(↑b : ℤ) : α) (↑(↑a : ℤ) : α)
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]
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
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 : ℤ) : α)
⊢ -(↑(a + b) : α) = HAdd.hAdd (α := α) (-(↑a : α)) (-(↑b : α))
have rw₈ : Eq.{u_1 + 1} (α := α) (↑(HAdd.hAdd (α := ℤ) (↑a : ℤ) (↑b : ℤ)) : α) (↑(HAdd.hAdd (α := ℤ) (↑b : ℤ) (↑a : ℤ)) : α)
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]
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
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 : ℤ)) : α)
⊢ -(↑(a + b) : α) = HAdd.hAdd (α := α) (-(↑a : α)) (-(↑b : α))
have rw₉ : Eq.{u_1 + 1} (α := α) (↑(HAdd.hAdd (α := ℤ) (↑b : ℤ) (↑a : ℤ)) : α) (↑(HAdd.hAdd (α := ℤ) (↑b : ℤ) (↑a : ℤ)) : α)
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]
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
α : Type u_1
inst : AddGroupWithOne α
n : ZNum
⊢ (↑n.succ : α) = HAdd.hAdd (α := α) (↑n : α) 1
have rw : (↑(n + 1) : α) = HAdd.hAdd (α := α) (↑n : α) 1
Tactic: rw [← add_one, cast_add, cast_one]
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
α : Type u_1
inst : AddGroupWithOne α
n : ZNum
rw : (↑(n + 1) : α) = HAdd.hAdd (α := α) (↑n : α) 1
⊢ (↑n.succ : α) = HAdd.hAdd (α := α) (↑n : α) 1
have rw₁ : HAdd.hAdd (α := α) (↑n : α) (↑1 : α) = HAdd.hAdd (α := α) (↑n : α) 1
Tactic: rw [← add_one, cast_add, cast_one]
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
α : Type u_1
inst : AddGroupWithOne α
n : ZNum
rw : (↑(n + 1) : α) = HAdd.hAdd (α := α) (↑n : α) 1
rw₁ : HAdd.hAdd (α := α) (↑n : α) (↑1 : α) = HAdd.hAdd (α := α) (↑n : α) 1
⊢ (↑n.succ : α) = HAdd.hAdd (α := α) (↑n : α) 1
have rw₂ : HAdd.hAdd (α := α) (↑n : α) 1 = HAdd.hAdd (α := α) (↑n : α) 1
Tactic: rw [← add_one, cast_add, cast_one]
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
a : ZNum
⊢ (↑(0 * a) : ℤ) = HMul.hMul (α := ℤ) (↑0 : ℤ) (↑a : ℤ)
have zero : (↑(0 * zero) : ℤ) = HMul.hMul (α := ℤ) (↑0 : ℤ) (↑zero : ℤ)
Tactic: cases a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
a : ZNum
zero : (↑(0 * ZNum.zero) : ℤ) = HMul.hMul (α := ℤ) (↑0 : ℤ) (↑ZNum.zero : ℤ)
⊢ (↑(0 * a) : ℤ) = HMul.hMul (α := ℤ) (↑0 : ℤ) (↑a : ℤ)
have pos : ∀ (a : PosNum), (↑(0 * pos a) : ℤ) = HMul.hMul (α := ℤ) (↑0 : ℤ) (↑(pos a) : ℤ)
Tactic: cases a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
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) : ℤ)
⊢ (↑(0 * a) : ℤ) = HMul.hMul (α := ℤ) (↑0 : ℤ) (↑a : ℤ)
have neg : ∀ (a : PosNum), (↑(0 * neg a) : ℤ) = HMul.hMul (α := ℤ) (↑0 : ℤ) (↑(neg a) : ℤ)
Tactic: cases a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
b : ZNum
⊢ (↑(b * 0) : ℤ) = HMul.hMul (α := ℤ) (↑b : ℤ) (↑0 : ℤ)
have zero : (↑(zero * 0) : ℤ) = HMul.hMul (α := ℤ) (↑zero : ℤ) (↑0 : ℤ)
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
b : ZNum
zero : (↑(ZNum.zero * 0) : ℤ) = HMul.hMul (α := ℤ) (↑ZNum.zero : ℤ) (↑0 : ℤ)
⊢ (↑(b * 0) : ℤ) = HMul.hMul (α := ℤ) (↑b : ℤ) (↑0 : ℤ)
have pos : ∀ (a : PosNum), (↑(pos a * 0) : ℤ) = HMul.hMul (α := ℤ) (↑(pos a) : ℤ) (↑0 : ℤ)
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
b : ZNum
zero : (↑(ZNum.zero * 0) : ℤ) = HMul.hMul (α := ℤ) (↑ZNum.zero : ℤ) (↑0 : ℤ)
pos : ∀ (a : PosNum), (↑(ZNum.pos a * 0) : ℤ) = HMul.hMul (α := ℤ) (↑(ZNum.pos a) : ℤ) (↑0 : ℤ)
⊢ (↑(b * 0) : ℤ) = HMul.hMul (α := ℤ) (↑b : ℤ) (↑0 : ℤ)
have neg : ∀ (a : PosNum), (↑(neg a * 0) : ℤ) = HMul.hMul (α := ℤ) (↑(neg a) : ℤ) (↑0 : ℤ)
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
a b : PosNum
⊢ -(↑(a * b) : ℤ) = HMul.hMul (α := ℤ) (↑a : ℤ) (-(↑b : ℤ))
have rw : -HMul.hMul (α := ℤ) (↑a : ℤ) (↑b : ℤ) = HMul.hMul (α := ℤ) (↑a : ℤ) (-(↑b : ℤ))
Tactic: rw [PosNum.cast_mul, neg_mul_eq_mul_neg]
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
a b : PosNum
rw : -HMul.hMul (α := ℤ) (↑a : ℤ) (↑b : ℤ) = HMul.hMul (α := ℤ) (↑a : ℤ) (-(↑b : ℤ))
⊢ -(↑(a * b) : ℤ) = HMul.hMul (α := ℤ) (↑a : ℤ) (-(↑b : ℤ))
have rw₁ : HMul.hMul (α := ℤ) (↑a : ℤ) (-(↑b : ℤ)) = HMul.hMul (α := ℤ) (↑a : ℤ) (-(↑b : ℤ))
Tactic: rw [PosNum.cast_mul, neg_mul_eq_mul_neg]
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
a b : PosNum
⊢ -(↑(a * b) : ℤ) = HMul.hMul (α := ℤ) (-(↑a : ℤ)) (↑b : ℤ)
have rw : -HMul.hMul (α := ℤ) (↑a : ℤ) (↑b : ℤ) = HMul.hMul (α := ℤ) (-(↑a : ℤ)) (↑b : ℤ)
Tactic: rw [PosNum.cast_mul, neg_mul_eq_neg_mul]
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
a b : PosNum
rw : -HMul.hMul (α := ℤ) (↑a : ℤ) (↑b : ℤ) = HMul.hMul (α := ℤ) (-(↑a : ℤ)) (↑b : ℤ)
⊢ -(↑(a * b) : ℤ) = HMul.hMul (α := ℤ) (-(↑a : ℤ)) (↑b : ℤ)
have rw₁ : HMul.hMul (α := ℤ) (-(↑a : ℤ)) (↑b : ℤ) = HMul.hMul (α := ℤ) (-(↑a : ℤ)) (↑b : ℤ)
Tactic: rw [PosNum.cast_mul, neg_mul_eq_neg_mul]
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
a b : PosNum
⊢ (↑(a * b) : ℤ) = HMul.hMul (α := ℤ) (-(↑a : ℤ)) (-(↑b : ℤ))
have rw : HMul.hMul (α := ℤ) (↑a : ℤ) (↑b : ℤ) = HMul.hMul (α := ℤ) (-(↑a : ℤ)) (-(↑b : ℤ))
Tactic: rw [PosNum.cast_mul, neg_mul_neg]
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
a b : PosNum
rw : HMul.hMul (α := ℤ) (↑a : ℤ) (↑b : ℤ) = HMul.hMul (α := ℤ) (-(↑a : ℤ)) (-(↑b : ℤ))
⊢ (↑(a * b) : ℤ) = HMul.hMul (α := ℤ) (-(↑a : ℤ)) (-(↑b : ℤ))
have rw₁ : HMul.hMul (α := ℤ) (↑a : ℤ) (↑b : ℤ) = HMul.hMul (α := ℤ) (↑a : ℤ) (↑b : ℤ)
Tactic: rw [PosNum.cast_mul, neg_mul_neg]
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
α : Type u_1
inst : NonAssocRing α
m n : ZNum
⊢ (↑(m * n) : α) = HMul.hMul (α := α) (↑m : α) (↑n : α)
have rw : (↑(↑(m * n) : ℤ) : α) = HMul.hMul (α := α) (↑m : α) (↑n : α)
Tactic: rw [← cast_to_int, mul_to_int, Int.cast_mul, cast_to_int, cast_to_int]
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
α : Type u_1
inst : NonAssocRing α
m n : ZNum
rw : (↑(↑(m * n) : ℤ) : α) = HMul.hMul (α := α) (↑m : α) (↑n : α)
⊢ (↑(m * n) : α) = HMul.hMul (α := α) (↑m : α) (↑n : α)
have rw₁ : (↑(HMul.hMul (α := ℤ) (↑m : ℤ) (↑n : ℤ)) : α) = HMul.hMul (α := α) (↑m : α) (↑n : α)
Tactic: rw [← cast_to_int, mul_to_int, Int.cast_mul, cast_to_int, cast_to_int]
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
α : Type u_1
inst : NonAssocRing α
m n : ZNum
rw : (↑(↑(m * n) : ℤ) : α) = HMul.hMul (α := α) (↑m : α) (↑n : α)
rw₁ : (↑(HMul.hMul (α := ℤ) (↑m : ℤ) (↑n : ℤ)) : α) = HMul.hMul (α := α) (↑m : α) (↑n : α)
⊢ (↑(m * n) : α) = HMul.hMul (α := α) (↑m : α) (↑n : α)
have rw₂ : HMul.hMul (α := α) (↑(↑m : ℤ) : α) (↑(↑n : ℤ) : α) = HMul.hMul (α := α) (↑m : α) (↑n : α)
Tactic: rw [← cast_to_int, mul_to_int, Int.cast_mul, cast_to_int, cast_to_int]
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
α : Type u_1
inst : NonAssocRing α
m n : ZNum
rw : (↑(↑(m * n) : ℤ) : α) = HMul.hMul (α := α) (↑m : α) (↑n : α)
rw₁ : (↑(HMul.hMul (α := ℤ) (↑m : ℤ) (↑n : ℤ)) : α) = HMul.hMul (α := α) (↑m : α) (↑n : α)
rw₂ : HMul.hMul (α := α) (↑(↑m : ℤ) : α) (↑(↑n : ℤ) : α) = HMul.hMul (α := α) (↑m : α) (↑n : α)
⊢ (↑(m * n) : α) = HMul.hMul (α := α) (↑m : α) (↑n : α)
have rw₃ : HMul.hMul (α := α) (↑m : α) (↑(↑n : ℤ) : α) = HMul.hMul (α := α) (↑m : α) (↑n : α)
Tactic: rw [← cast_to_int, mul_to_int, Int.cast_mul, cast_to_int, cast_to_int]
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
α : Type u_1
inst : NonAssocRing α
m n : ZNum
rw : (↑(↑(m * n) : ℤ) : α) = HMul.hMul (α := α) (↑m : α) (↑n : α)
rw₁ : (↑(HMul.hMul (α := ℤ) (↑m : ℤ) (↑n : ℤ)) : α) = HMul.hMul (α := α) (↑m : α) (↑n : α)
rw₂ : HMul.hMul (α := α) (↑(↑m : ℤ) : α) (↑(↑n : ℤ) : α) = HMul.hMul (α := α) (↑m : α) (↑n : α)
rw₃ : HMul.hMul (α := α) (↑m : α) (↑(↑n : ℤ) : α) = HMul.hMul (α := α) (↑m : α) (↑n : α)
⊢ (↑(m * n) : α) = HMul.hMul (α := α) (↑m : α) (↑n : α)
have rw₄ : HMul.hMul (α := α) (↑m : α) (↑n : α) = HMul.hMul (α := α) (↑m : α) (↑n : α)
Tactic: rw [← cast_to_int, mul_to_int, Int.cast_mul, cast_to_int, cast_to_int]
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
n : ℕ
⊢ (Num.ofNat' (n + 1)).toZNumNeg = -(Num.ofNat' (n + 1)).toZNum
have rw : (Num.ofNat' (n + 1)).toZNumNeg = (Num.ofNat' (n + 1)).toZNumNeg
Tactic: rw [Num.zneg_toZNum]
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
a : PosNum
⊢ ofInt' (↑(pos a) : ℤ) = pos a
have rw : (Num.pos a).toZNum = pos a
Tactic: rw [cast_pos, ← PosNum.cast_to_nat, ← Num.ofInt'_toZNum, PosNum.of_to_nat]
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
a : PosNum
⊢ ofInt' (↑(neg a) : ℤ) = neg a
have rw : -(Num.pos a).toZNum = neg a
Tactic: rw [cast_neg, ofInt'_neg, ← PosNum.cast_to_nat, ← Num.ofInt'_toZNum, PosNum.of_to_nat]
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
a b : PosNum
⊢ Ordering.casesOn (motive := fun (x : Ordering) ↦ Prop) ((neg a).cmp (neg b))
    (LT.lt (α := ℤ) (↑(neg a) : ℤ) (↑(neg b) : ℤ)) (neg a = neg b) (LT.lt (α := ℤ) (↑(neg b) : ℤ) (↑(neg a) : ℤ))
have have : ∀
  (this :
    Ordering.casesOn (motive := fun (x : Ordering) ↦ Prop) (b.cmp a) (LT.lt (α := ℕ) (↑b : ℕ) (↑a : ℕ)) (b = a)
      (LT.lt (α := ℕ) (↑a : ℕ) (↑b : ℕ))),
  Ordering.casesOn (motive := fun (x : Ordering) ↦ Prop) ((neg a).cmp (neg b))
    (LT.lt (α := ℤ) (↑(neg a) : ℤ) (↑(neg b) : ℤ)) (neg a = neg b) (LT.lt (α := ℤ) (↑(neg b) : ℤ) (↑(neg a) : ℤ))
Tactic: have := PosNum.cmp_to_nat b a
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
a b : PosNum
this :
  Ordering.casesOn (motive := fun (x : Ordering) ↦ Prop) (b.cmp a) (LT.lt (α := ℕ) (↑b : ℕ) (↑a : ℕ)) (b = a)
    (LT.lt (α := ℕ) (↑a : ℕ) (↑b : ℕ))
⊢ Ordering.casesOn (motive := fun (x : Ordering) ↦ Prop) ((neg a).cmp (neg b))
    (LT.lt (α := ℤ) (↑(neg a) : ℤ) (↑(neg b) : ℤ)) (neg a = neg b) (LT.lt (α := ℤ) (↑(neg b) : ℤ) (↑(neg a) : ℤ))
have revert : ∀
  (this :
    Ordering.casesOn (motive := fun (x : Ordering) ↦ Prop) (b.cmp a) (LT.lt (α := ℕ) (↑b : ℕ) (↑a : ℕ)) (b = a)
      (LT.lt (α := ℕ) (↑a : ℕ) (↑b : ℕ))),
  Ordering.casesOn (motive := fun (x : Ordering) ↦ Prop) ((neg a).cmp (neg b))
    (LT.lt (α := ℤ) (↑(neg a) : ℤ) (↑(neg b) : ℤ)) (neg a = neg b) (LT.lt (α := ℤ) (↑(neg b) : ℤ) (↑(neg a) : ℤ))
Tactic: revert this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
a b : PosNum
⊢ ∀
    (this :
      Ordering.casesOn (motive := fun (x : Ordering) ↦ Prop) (b.cmp a) (LT.lt (α := ℕ) (↑b : ℕ) (↑a : ℕ)) (b = a)
        (LT.lt (α := ℕ) (↑a : ℕ) (↑b : ℕ))),
    Ordering.casesOn (motive := fun (x : Ordering) ↦ Prop) ((neg a).cmp (neg b))
      (LT.lt (α := ℤ) (↑(neg a) : ℤ) (↑(neg b) : ℤ)) (neg a = neg b) (LT.lt (α := ℤ) (↑(neg b) : ℤ) (↑(neg a) : ℤ))
have dsimp : ∀
  (this :
    Ordering.rec (motive := fun (x : Ordering) ↦ Prop) (LT.lt (α := ℕ) (↑b : ℕ) (↑a : ℕ)) (b = a)
      (LT.lt (α := ℕ) (↑a : ℕ) (↑b : ℕ)) (b.cmp a)),
  Ordering.rec (motive := fun (x : Ordering) ↦ Prop) (LT.lt (α := ℤ) (-(↑a : ℤ)) (-(↑b : ℤ))) (neg a = neg b)
    (LT.lt (α := ℤ) (-(↑b : ℤ)) (-(↑a : ℤ))) (b.cmp a)
Tactic: dsimp [cmp]
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
a b : PosNum
⊢ ∀
    (this :
      Ordering.rec (motive := fun (x : Ordering) ↦ Prop) (LT.lt (α := ℕ) (↑b : ℕ) (↑a : ℕ)) (b = a)
        (LT.lt (α := ℕ) (↑a : ℕ) (↑b : ℕ)) (b.cmp a)),
    Ordering.rec (motive := fun (x : Ordering) ↦ Prop) (LT.lt (α := ℤ) (-(↑a : ℤ)) (-(↑b : ℤ))) (neg a = neg b)
      (LT.lt (α := ℤ) (-(↑b : ℤ)) (-(↑a : ℤ))) (b.cmp a)
have lt : ∀
  (this :
    Ordering.rec (motive := fun (x : Ordering) ↦ Prop) (LT.lt (α := ℕ) (↑b : ℕ) (↑a : ℕ)) (b = a)
      (LT.lt (α := ℕ) (↑a : ℕ) (↑b : ℕ)) Ordering.lt),
  Ordering.rec (motive := fun (x : Ordering) ↦ Prop) (LT.lt (α := ℤ) (-(↑a : ℤ)) (-(↑b : ℤ))) (neg a = neg b)
    (LT.lt (α := ℤ) (-(↑b : ℤ)) (-(↑a : ℤ))) Ordering.lt
Tactic: cases PosNum.cmp b a
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
a b : PosNum
lt :
  ∀
    (this :
      Ordering.rec (motive := fun (x : Ordering) ↦ Prop) (LT.lt (α := ℕ) (↑b : ℕ) (↑a : ℕ)) (b = a)
        (LT.lt (α := ℕ) (↑a : ℕ) (↑b : ℕ)) Ordering.lt),
    Ordering.rec (motive := fun (x : Ordering) ↦ Prop) (LT.lt (α := ℤ) (-(↑a : ℤ)) (-(↑b : ℤ))) (neg a = neg b)
      (LT.lt (α := ℤ) (-(↑b : ℤ)) (-(↑a : ℤ))) Ordering.lt
⊢ ∀
    (this :
      Ordering.rec (motive := fun (x : Ordering) ↦ Prop) (LT.lt (α := ℕ) (↑b : ℕ) (↑a : ℕ)) (b = a)
        (LT.lt (α := ℕ) (↑a : ℕ) (↑b : ℕ)) (b.cmp a)),
    Ordering.rec (motive := fun (x : Ordering) ↦ Prop) (LT.lt (α := ℤ) (-(↑a : ℤ)) (-(↑b : ℤ))) (neg a = neg b)
      (LT.lt (α := ℤ) (-(↑b : ℤ)) (-(↑a : ℤ))) (b.cmp a)
have eq : ∀
  (this :
    Ordering.rec (motive := fun (x : Ordering) ↦ Prop) (LT.lt (α := ℕ) (↑b : ℕ) (↑a : ℕ)) (b = a)
      (LT.lt (α := ℕ) (↑a : ℕ) (↑b : ℕ)) Ordering.eq),
  Ordering.rec (motive := fun (x : Ordering) ↦ Prop) (LT.lt (α := ℤ) (-(↑a : ℤ)) (-(↑b : ℤ))) (neg a = neg b)
    (LT.lt (α := ℤ) (-(↑b : ℤ)) (-(↑a : ℤ))) Ordering.eq
Tactic: cases PosNum.cmp b a
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
a b : PosNum
lt :
  ∀
    (this :
      Ordering.rec (motive := fun (x : Ordering) ↦ Prop) (LT.lt (α := ℕ) (↑b : ℕ) (↑a : ℕ)) (b = a)
        (LT.lt (α := ℕ) (↑a : ℕ) (↑b : ℕ)) Ordering.lt),
    Ordering.rec (motive := fun (x : Ordering) ↦ Prop) (LT.lt (α := ℤ) (-(↑a : ℤ)) (-(↑b : ℤ))) (neg a = neg b)
      (LT.lt (α := ℤ) (-(↑b : ℤ)) (-(↑a : ℤ))) Ordering.lt
eq :
  ∀
    (this :
      Ordering.rec (motive := fun (x : Ordering) ↦ Prop) (LT.lt (α := ℕ) (↑b : ℕ) (↑a : ℕ)) (b = a)
        (LT.lt (α := ℕ) (↑a : ℕ) (↑b : ℕ)) Ordering.eq),
    Ordering.rec (motive := fun (x : Ordering) ↦ Prop) (LT.lt (α := ℤ) (-(↑a : ℤ)) (-(↑b : ℤ))) (neg a = neg b)
      (LT.lt (α := ℤ) (-(↑b : ℤ)) (-(↑a : ℤ))) Ordering.eq
⊢ ∀
    (this :
      Ordering.rec (motive := fun (x : Ordering) ↦ Prop) (LT.lt (α := ℕ) (↑b : ℕ) (↑a : ℕ)) (b = a)
        (LT.lt (α := ℕ) (↑a : ℕ) (↑b : ℕ)) (b.cmp a)),
    Ordering.rec (motive := fun (x : Ordering) ↦ Prop) (LT.lt (α := ℤ) (-(↑a : ℤ)) (-(↑b : ℤ))) (neg a = neg b)
      (LT.lt (α := ℤ) (-(↑b : ℤ)) (-(↑a : ℤ))) (b.cmp a)
have gt : ∀
  (this :
    Ordering.rec (motive := fun (x : Ordering) ↦ Prop) (LT.lt (α := ℕ) (↑b : ℕ) (↑a : ℕ)) (b = a)
      (LT.lt (α := ℕ) (↑a : ℕ) (↑b : ℕ)) Ordering.gt),
  Ordering.rec (motive := fun (x : Ordering) ↦ Prop) (LT.lt (α := ℤ) (-(↑a : ℤ)) (-(↑b : ℤ))) (neg a = neg b)
    (LT.lt (α := ℤ) (-(↑b : ℤ)) (-(↑a : ℤ))) Ordering.gt
Tactic: cases PosNum.cmp b a
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
a b : PosNum
⊢ ∀
    (this :
      Ordering.rec (motive := fun (x : Ordering) ↦ Prop) (LT.lt (α := ℕ) (↑b : ℕ) (↑a : ℕ)) (b = a)
        (LT.lt (α := ℕ) (↑a : ℕ) (↑b : ℕ)) (b.cmp a)),
    Ordering.rec (motive := fun (x : Ordering) ↦ Prop) (LT.lt (α := ℤ) (-(↑a : ℤ)) (-(↑b : ℤ))) (neg a = neg b)
      (LT.lt (α := ℤ) (-(↑b : ℤ)) (-(↑a : ℤ))) (b.cmp a)
have lt : ∀
  (this :
    Ordering.rec (motive := fun (x : Ordering) ↦ Prop) (LT.lt (α := ℕ) (↑b : ℕ) (↑a : ℕ)) (b = a)
      (LT.lt (α := ℕ) (↑a : ℕ) (↑b : ℕ)) Ordering.lt),
  Ordering.rec (motive := fun (x : Ordering) ↦ Prop) (LT.lt (α := ℤ) (-(↑a : ℤ)) (-(↑b : ℤ))) (neg a = neg b)
    (LT.lt (α := ℤ) (-(↑b : ℤ)) (-(↑a : ℤ))) Ordering.lt
Tactic: cases PosNum.cmp b a <;> [simp; simp +contextual; simp]
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
a b : PosNum
lt :
  ∀
    (this :
      Ordering.rec (motive := fun (x : Ordering) ↦ Prop) (LT.lt (α := ℕ) (↑b : ℕ) (↑a : ℕ)) (b = a)
        (LT.lt (α := ℕ) (↑a : ℕ) (↑b : ℕ)) Ordering.lt),
    Ordering.rec (motive := fun (x : Ordering) ↦ Prop) (LT.lt (α := ℤ) (-(↑a : ℤ)) (-(↑b : ℤ))) (neg a = neg b)
      (LT.lt (α := ℤ) (-(↑b : ℤ)) (-(↑a : ℤ))) Ordering.lt
⊢ ∀
    (this :
      Ordering.rec (motive := fun (x : Ordering) ↦ Prop) (LT.lt (α := ℕ) (↑b : ℕ) (↑a : ℕ)) (b = a)
        (LT.lt (α := ℕ) (↑a : ℕ) (↑b : ℕ)) (b.cmp a)),
    Ordering.rec (motive := fun (x : Ordering) ↦ Prop) (LT.lt (α := ℤ) (-(↑a : ℤ)) (-(↑b : ℤ))) (neg a = neg b)
      (LT.lt (α := ℤ) (-(↑b : ℤ)) (-(↑a : ℤ))) (b.cmp a)
have eq : ∀
  (this :
    Ordering.rec (motive := fun (x : Ordering) ↦ Prop) (LT.lt (α := ℕ) (↑b : ℕ) (↑a : ℕ)) (b = a)
      (LT.lt (α := ℕ) (↑a : ℕ) (↑b : ℕ)) Ordering.eq),
  Ordering.rec (motive := fun (x : Ordering) ↦ Prop) (LT.lt (α := ℤ) (-(↑a : ℤ)) (-(↑b : ℤ))) (neg a = neg b)
    (LT.lt (α := ℤ) (-(↑b : ℤ)) (-(↑a : ℤ))) Ordering.eq
Tactic: cases PosNum.cmp b a <;> [simp; simp +contextual; simp]