awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
α : Type u_1
inst : NonAssocSemiring α
m n : PosNum
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_nat, mul_to_nat, Nat.cast_mul, cast_to_nat, cast_to_nat]
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (hypothesis)
Goal:
m n : PosNum
⊢ m.cmp n = Ordering.eq ↔ m = n
have this : Ordering.casesOn (motive := fun (x : Ordering) ↦ Prop) (m.cmp n) (LT.lt (α := ℕ) (↑m : ℕ) (↑n : ℕ)) (m = n)
  (LT.lt (α := ℕ) (↑n : ℕ) (↑m : ℕ))
Tactic: have := cmp_to_nat m n
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (hypothesis)
Goal:
m n : PosNum
this :
  Ordering.casesOn (motive := fun (x : Ordering) ↦ Prop) (m.cmp n) (LT.lt (α := ℕ) (↑m : ℕ) (↑n : ℕ)) (m = n)
    (LT.lt (α := ℕ) (↑n : ℕ) (↑m : ℕ))
⊢ m.cmp n = Ordering.eq ↔ m = n
have this₁ : Ordering.casesOn (motive := fun (x : Ordering) ↦ Prop) (m.cmp n) (m < n) (m = n) (n < m)
Tactic: norm_cast at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
m n : PosNum
this : Ordering.casesOn (motive := fun (x : Ordering) ↦ Prop) (m.cmp n) (m < n) (m = n) (n < m)
⊢ m.cmp n = Ordering.eq ↔ m = n
have revert : ∀ (this : Ordering.casesOn (motive := fun (x : Ordering) ↦ Prop) (m.cmp n) (m < n) (m = n) (n < m)),
  m.cmp n = Ordering.eq ↔ m = n
Tactic: revert this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
m n : PosNum
⊢ ∀ (this : Ordering.casesOn (motive := fun (x : Ordering) ↦ Prop) (m.cmp n) (m < n) (m = n) (n < m)),
    m.cmp n = Ordering.eq ↔ m = n
have lt : ∀ (this : Ordering.casesOn (motive := fun (x : Ordering) ↦ Prop) Ordering.lt (m < n) (m = n) (n < m)),
  Ordering.lt = Ordering.eq ↔ m = n
Tactic: cases cmp m n
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
m n : PosNum
lt :
  ∀ (this : Ordering.casesOn (motive := fun (x : Ordering) ↦ Prop) Ordering.lt (m < n) (m = n) (n < m)),
    Ordering.lt = Ordering.eq ↔ m = n
⊢ ∀ (this : Ordering.casesOn (motive := fun (x : Ordering) ↦ Prop) (m.cmp n) (m < n) (m = n) (n < m)),
    m.cmp n = Ordering.eq ↔ m = n
have eq : ∀ (this : Ordering.casesOn (motive := fun (x : Ordering) ↦ Prop) Ordering.eq (m < n) (m = n) (n < m)),
  Ordering.eq = Ordering.eq ↔ m = n
Tactic: cases cmp m n
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
m n : PosNum
lt :
  ∀ (this : Ordering.casesOn (motive := fun (x : Ordering) ↦ Prop) Ordering.lt (m < n) (m = n) (n < m)),
    Ordering.lt = Ordering.eq ↔ m = n
eq :
  ∀ (this : Ordering.casesOn (motive := fun (x : Ordering) ↦ Prop) Ordering.eq (m < n) (m = n) (n < m)),
    Ordering.eq = Ordering.eq ↔ m = n
⊢ ∀ (this : Ordering.casesOn (motive := fun (x : Ordering) ↦ Prop) (m.cmp n) (m < n) (m = n) (n < m)),
    m.cmp n = Ordering.eq ↔ m = n
have gt : ∀ (this : Ordering.casesOn (motive := fun (x : Ordering) ↦ Prop) Ordering.gt (m < n) (m = n) (n < m)),
  Ordering.gt = Ordering.eq ↔ m = n
Tactic: cases cmp m n
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
α : Type u_1
inst : Semiring α
inst_1 : PartialOrder α
inst_2 : IsStrictOrderedRing α
m n : PosNum
⊢ LT.lt.{u_1} (α := α) (↑m : α) (↑n : α) ↔ m < n
have rw : LT.lt.{u_1} (α := α) (↑(↑m : ℕ) : α) (↑n : α) ↔ m < n
Tactic: rw [← cast_to_nat m, ← cast_to_nat n, Nat.cast_lt (α := α), lt_to_nat]
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
α : Type u_1
inst : Semiring α
inst_1 : PartialOrder α
inst_2 : IsStrictOrderedRing α
m n : PosNum
rw : LT.lt.{u_1} (α := α) (↑(↑m : ℕ) : α) (↑n : α) ↔ m < n
⊢ LT.lt.{u_1} (α := α) (↑m : α) (↑n : α) ↔ m < n
have rw₁ : LT.lt.{u_1} (α := α) (↑(↑m : ℕ) : α) (↑(↑n : ℕ) : α) ↔ m < n
Tactic: rw [← cast_to_nat m, ← cast_to_nat n, Nat.cast_lt (α := α), lt_to_nat]
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
α : Type u_1
inst : Semiring α
inst_1 : PartialOrder α
inst_2 : IsStrictOrderedRing α
m n : PosNum
rw : LT.lt.{u_1} (α := α) (↑(↑m : ℕ) : α) (↑n : α) ↔ m < n
rw₁ : LT.lt.{u_1} (α := α) (↑(↑m : ℕ) : α) (↑(↑n : ℕ) : α) ↔ m < n
⊢ LT.lt.{u_1} (α := α) (↑m : α) (↑n : α) ↔ m < n
have rw₂ : LT.lt (α := ℕ) (↑m : ℕ) (↑n : ℕ) ↔ m < n
Tactic: rw [← cast_to_nat m, ← cast_to_nat n, Nat.cast_lt (α := α), lt_to_nat]
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
α : Type u_1
inst : Semiring α
inst_1 : PartialOrder α
inst_2 : IsStrictOrderedRing α
m n : PosNum
rw : LT.lt.{u_1} (α := α) (↑(↑m : ℕ) : α) (↑n : α) ↔ m < n
rw₁ : LT.lt.{u_1} (α := α) (↑(↑m : ℕ) : α) (↑(↑n : ℕ) : α) ↔ m < n
rw₂ : LT.lt (α := ℕ) (↑m : ℕ) (↑n : ℕ) ↔ m < n
⊢ LT.lt.{u_1} (α := α) (↑m : α) (↑n : α) ↔ m < n
have rw₃ : m < n ↔ m < n
Tactic: rw [← cast_to_nat m, ← cast_to_nat n, Nat.cast_lt (α := α), lt_to_nat]
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
α : Type u_1
inst : Semiring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
m n : PosNum
⊢ LE.le.{u_1} (α := α) (↑m : α) (↑n : α) ↔ m ≤ n
have rw : ¬LT.lt.{u_1} (α := α) (↑n : α) (↑m : α) ↔ m ≤ n
Tactic: rw [← not_lt]
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
b : Bool
n : Num
⊢ (↑(bit b n) : ℕ) = Nat.bit b (↑n : ℕ)
have false : (↑(bit false n) : ℕ) = Nat.bit false (↑n : ℕ)
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
b : Bool
n : Num
false : (↑(bit Bool.false n) : ℕ) = Nat.bit Bool.false (↑n : ℕ)
⊢ (↑(bit b n) : ℕ) = Nat.bit b (↑n : ℕ)
have true : (↑(bit true n) : ℕ) = Nat.bit true (↑n : ℕ)
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
n : Num
⊢ (↑(bit false n) : ℕ) = Nat.bit false (↑n : ℕ)
have false : (↑(bit false zero) : ℕ) = Nat.bit false (↑zero : ℕ)
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
n : Num
false : (↑(bit Bool.false zero) : ℕ) = Nat.bit Bool.false (↑zero : ℕ)
⊢ (↑(bit Bool.false n) : ℕ) = Nat.bit Bool.false (↑n : ℕ)
have false₁ : ∀ (a : PosNum), (↑(bit Bool.false (pos a)) : ℕ) = Nat.bit Bool.false (↑(pos a) : ℕ)
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
n : Num
⊢ (↑(bit true n) : ℕ) = Nat.bit true (↑n : ℕ)
have true : (↑(bit true zero) : ℕ) = Nat.bit true (↑zero : ℕ)
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
n : Num
true : (↑(bit Bool.true zero) : ℕ) = Nat.bit Bool.true (↑zero : ℕ)
⊢ (↑(bit Bool.true n) : ℕ) = Nat.bit Bool.true (↑n : ℕ)
have true₁ : ∀ (a : PosNum), (↑(bit Bool.true (pos a)) : ℕ) = Nat.bit Bool.true (↑(pos a) : ℕ)
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
a : PosNum
⊢ (↑(bit false (pos a)) : ℕ) = Nat.bit false (↑(pos a) : ℕ)
have false : (↑(pos a).bit0 : ℕ) = HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑a : ℕ)
Tactic: simp [bit, two_mul]
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
a : PosNum
⊢ (↑(bit true (pos a)) : ℕ) = Nat.bit true (↑(pos a) : ℕ)
have true : (↑(pos a).bit1 : ℕ) = (↑a : ℕ) + HAdd.hAdd (α := ℕ) (↑a : ℕ) 1
Tactic: simp [bit, two_mul]
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
α : Type u_1
inst : AddMonoidWithOne α
n : Num
⊢ (↑n.succ' : α) = HAdd.hAdd (α := α) (↑n : α) 1
have rw : (↑(↑n.succ' : ℕ) : α) = HAdd.hAdd (α := α) (↑n : α) 1
Tactic: rw [← PosNum.cast_to_nat, succ'_to_nat, Nat.cast_add_one, cast_to_nat]
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
α : Type u_1
inst : AddMonoidWithOne α
n : Num
rw : (↑(↑n.succ' : ℕ) : α) = HAdd.hAdd (α := α) (↑n : α) 1
⊢ (↑n.succ' : α) = HAdd.hAdd (α := α) (↑n : α) 1
have rw₁ : (↑(HAdd.hAdd (α := ℕ) (↑n : ℕ) 1) : α) = HAdd.hAdd (α := α) (↑n : α) 1
Tactic: rw [← PosNum.cast_to_nat, succ'_to_nat, Nat.cast_add_one, cast_to_nat]
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
α : Type u_1
inst : AddMonoidWithOne α
n : Num
rw : (↑(↑n.succ' : ℕ) : α) = 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 [← PosNum.cast_to_nat, succ'_to_nat, Nat.cast_add_one, cast_to_nat]
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
α : Type u_1
inst : AddMonoidWithOne α
n : Num
rw : (↑(↑n.succ' : ℕ) : α) = HAdd.hAdd (α := α) (↑n : α) 1
rw₁ : (↑(HAdd.hAdd (α := ℕ) (↑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 [← PosNum.cast_to_nat, succ'_to_nat, Nat.cast_add_one, cast_to_nat]
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
α : Type u_1
inst : AddMonoidWithOne α
m n : Num
⊢ (↑(m + n) : α) = HAdd.hAdd (α := α) (↑m : α) (↑n : α)
have rw : (↑(↑(m + n) : ℕ) : α) = HAdd.hAdd (α := α) (↑m : α) (↑n : α)
Tactic: rw [← cast_to_nat, add_to_nat, Nat.cast_add, cast_to_nat, cast_to_nat]
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
α : Type u_1
inst : AddMonoidWithOne α
m n : Num
rw : (↑(↑(m + n) : ℕ) : α) = HAdd.hAdd (α := α) (↑m : α) (↑n : α)
⊢ (↑(m + n) : α) = HAdd.hAdd (α := α) (↑m : α) (↑n : α)
have rw₁ : (↑(HAdd.hAdd (α := ℕ) (↑m : ℕ) (↑n : ℕ)) : α) = HAdd.hAdd (α := α) (↑m : α) (↑n : α)
Tactic: rw [← cast_to_nat, add_to_nat, Nat.cast_add, cast_to_nat, cast_to_nat]
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
α : Type u_1
inst : AddMonoidWithOne α
m n : Num
rw : (↑(↑(m + n) : ℕ) : α) = HAdd.hAdd (α := α) (↑m : α) (↑n : α)
rw₁ : (↑(HAdd.hAdd (α := ℕ) (↑m : ℕ) (↑n : ℕ)) : α) = HAdd.hAdd (α := α) (↑m : α) (↑n : α)
⊢ (↑(m + n) : α) = HAdd.hAdd (α := α) (↑m : α) (↑n : α)
have rw₂ : HAdd.hAdd (α := α) (↑(↑m : ℕ) : α) (↑(↑n : ℕ) : α) = HAdd.hAdd (α := α) (↑m : α) (↑n : α)
Tactic: rw [← cast_to_nat, add_to_nat, Nat.cast_add, cast_to_nat, cast_to_nat]
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
α : Type u_1
inst : AddMonoidWithOne α
m n : Num
rw : (↑(↑(m + n) : ℕ) : α) = HAdd.hAdd (α := α) (↑m : α) (↑n : α)
rw₁ : (↑(HAdd.hAdd (α := ℕ) (↑m : ℕ) (↑n : ℕ)) : α) = HAdd.hAdd (α := α) (↑m : α) (↑n : α)
rw₂ : HAdd.hAdd (α := α) (↑(↑m : ℕ) : α) (↑(↑n : ℕ) : α) = HAdd.hAdd (α := α) (↑m : α) (↑n : α)
⊢ (↑(m + n) : α) = HAdd.hAdd (α := α) (↑m : α) (↑n : α)
have rw₃ : HAdd.hAdd (α := α) (↑m : α) (↑(↑n : ℕ) : α) = HAdd.hAdd (α := α) (↑m : α) (↑n : α)
Tactic: rw [← cast_to_nat, add_to_nat, Nat.cast_add, cast_to_nat, cast_to_nat]
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
α : Type u_1
inst : AddMonoidWithOne α
m n : Num
rw : (↑(↑(m + n) : ℕ) : α) = HAdd.hAdd (α := α) (↑m : α) (↑n : α)
rw₁ : (↑(HAdd.hAdd (α := ℕ) (↑m : ℕ) (↑n : ℕ)) : α) = HAdd.hAdd (α := α) (↑m : α) (↑n : α)
rw₂ : HAdd.hAdd (α := α) (↑(↑m : ℕ) : α) (↑(↑n : ℕ) : α) = HAdd.hAdd (α := α) (↑m : α) (↑n : α)
rw₃ : HAdd.hAdd (α := α) (↑m : α) (↑(↑n : ℕ) : α) = HAdd.hAdd (α := α) (↑m : α) (↑n : α)
⊢ (↑(m + n) : α) = HAdd.hAdd (α := α) (↑m : α) (↑n : α)
have rw₄ : HAdd.hAdd (α := α) (↑m : α) (↑n : α) = HAdd.hAdd (α := α) (↑m : α) (↑n : α)
Tactic: rw [← cast_to_nat, add_to_nat, Nat.cast_add, cast_to_nat, cast_to_nat]
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
α : Type u_1
inst : NonAssocSemiring α
n : Num
⊢ (↑n.bit0 : α) = HMul.hMul (α := α) 2 (↑n : α)
have rw : (↑(n + n) : α) = HMul.hMul (α := α) 2 (↑n : α)
Tactic: rw [← bit0_of_bit0, two_mul, cast_add]
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
α : Type u_1
inst : NonAssocSemiring α
n : Num
rw : (↑(n + n) : α) = HMul.hMul (α := α) 2 (↑n : α)
⊢ (↑n.bit0 : α) = HMul.hMul (α := α) 2 (↑n : α)
have rw₁ : (↑(n + n) : α) = HAdd.hAdd (α := α) (↑n : α) (↑n : α)
Tactic: rw [← bit0_of_bit0, two_mul, cast_add]
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
α : Type u_1
inst : NonAssocSemiring α
n : Num
rw : (↑(n + n) : α) = HMul.hMul (α := α) 2 (↑n : α)
rw₁ : (↑(n + n) : α) = HAdd.hAdd (α := α) (↑n : α) (↑n : α)
⊢ (↑n.bit0 : α) = HMul.hMul (α := α) 2 (↑n : α)
have rw₂ : HAdd.hAdd (α := α) (↑n : α) (↑n : α) = HAdd.hAdd (α := α) (↑n : α) (↑n : α)
Tactic: rw [← bit0_of_bit0, two_mul, cast_add]
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
α : Type u_1
inst : NonAssocSemiring α
n : Num
⊢ (↑n.bit1 : α) = HMul.hMul (α := α) 2 (↑n : α) + 1
have rw : HMul.hMul (α := α) 2 (↑n : α) + (↑1 : α) = HMul.hMul (α := α) 2 (↑n : α) + 1
Tactic: rw [← bit1_of_bit1, bit0_of_bit0, cast_add, cast_bit0]
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
n : Num
⊢ n.natSize = Nat.size (↑n : ℕ)
have rw : (↑n.size : ℕ) = Nat.size (↑n : ℕ)
Tactic: rw [← size_eq_natSize, size_to_nat]
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
n : Num
rw : (↑n.size : ℕ) = Nat.size (↑n : ℕ)
⊢ n.natSize = Nat.size (↑n : ℕ)
have rw₁ : Nat.size (↑n : ℕ) = Nat.size (↑n : ℕ)
Tactic: rw [← size_eq_natSize, size_to_nat]
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
n : Num
⊢ -n.toZNum = n.toZNumNeg
have zero : -zero.toZNum = zero.toZNumNeg
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
n : Num
zero : -Num.zero.toZNum = Num.zero.toZNumNeg
⊢ -n.toZNum = n.toZNumNeg
have pos : ∀ (a : PosNum), -(pos a).toZNum = (pos a).toZNumNeg
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
n : Num
⊢ -n.toZNumNeg = n.toZNum
have zero : -zero.toZNumNeg = zero.toZNum
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
n : Num
zero : -Num.zero.toZNumNeg = Num.zero.toZNum
⊢ -n.toZNumNeg = n.toZNum
have pos : ∀ (a : PosNum), -(pos a).toZNumNeg = (pos a).toZNum
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
m n : Num
h : m.toZNum = n.toZNum
⊢ m = n
have zero : ∀ (h : zero.toZNum = n.toZNum), zero = n
Tactic: cases m
Cleared hypotheses: m, h
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
m n : Num
h : m.toZNum = n.toZNum
zero : ∀ (h : Num.zero.toZNum = n.toZNum), Num.zero = n
⊢ m = n
have pos : ∀ (a : PosNum) (h : (pos a).toZNum = n.toZNum), pos a = n
Tactic: cases m
Cleared hypotheses: m, h
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
n : Num
h : zero.toZNum = n.toZNum
⊢ zero = n
have zero : ∀ (h : zero.toZNum = zero.toZNum), zero = zero
Tactic: cases n
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
n : Num
h : Num.zero.toZNum = n.toZNum
zero : ∀ (h : Num.zero.toZNum = Num.zero.toZNum), Num.zero = Num.zero
⊢ Num.zero = n
have zero₁ : ∀ (a : PosNum) (h : Num.zero.toZNum = (pos a).toZNum), Num.zero = pos a
Tactic: cases n
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
n : Num
a : PosNum
h : (pos a).toZNum = n.toZNum
⊢ pos a = n
have pos : ∀ (h : (pos a).toZNum = zero.toZNum), pos a = zero
Tactic: cases n
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
n : Num
a : PosNum
h : (Num.pos a).toZNum = n.toZNum
pos : ∀ (h : (Num.pos a).toZNum = zero.toZNum), Num.pos a = zero
⊢ Num.pos a = n
have pos₁ : ∀ (a_1 : PosNum) (h : (Num.pos a).toZNum = (Num.pos a_1).toZNum), Num.pos a = Num.pos a_1
Tactic: cases n
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
a a_1 : PosNum
h : (pos a).toZNum = (pos a_1).toZNum
⊢ pos a = pos a_1
have pos : pos a = pos a
Tactic: cases h
Cleared hypotheses: a_1, h
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
m n : Num
⊢ (m + n).toZNum = m.toZNum + n.toZNum
have zero : (zero + n).toZNum = zero.toZNum + n.toZNum
Tactic: cases m
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
m n : Num
zero : (Num.zero + n).toZNum = Num.zero.toZNum + n.toZNum
⊢ (m + n).toZNum = m.toZNum + n.toZNum
have pos : ∀ (a : PosNum), (pos a + n).toZNum = (pos a).toZNum + n.toZNum
Tactic: cases m
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
n : Num
⊢ (zero + n).toZNum = zero.toZNum + n.toZNum
have zero : (zero + zero).toZNum = zero.toZNum + zero.toZNum
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
n : Num
zero : (Num.zero + Num.zero).toZNum = Num.zero.toZNum + Num.zero.toZNum
⊢ (Num.zero + n).toZNum = Num.zero.toZNum + n.toZNum
have zero₁ : ∀ (a : PosNum), (Num.zero + pos a).toZNum = Num.zero.toZNum + (pos a).toZNum
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
n : Num
a : PosNum
⊢ (pos a + n).toZNum = (pos a).toZNum + n.toZNum
have pos : (pos a + zero).toZNum = (pos a).toZNum + zero.toZNum
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
n : Num
a : PosNum
pos : (Num.pos a + zero).toZNum = (Num.pos a).toZNum + zero.toZNum
⊢ (Num.pos a + n).toZNum = (Num.pos a).toZNum + n.toZNum
have pos₁ : ∀ (a_1 : PosNum), (Num.pos a + Num.pos a_1).toZNum = (Num.pos a).toZNum + (Num.pos a_1).toZNum
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
n : PosNum
h : 1 < n
⊢ (↑n.pred : ℕ) = Nat.pred (↑n : ℕ)
have unfold : (↑(Num.casesOn (motive := fun (x : Num) ↦ PosNum) n.pred' 1 id) : ℕ) = Nat.pred (↑n : ℕ)
Tactic: unfold pred
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
n : PosNum
h : 1 < n
⊢ (↑(Num.casesOn (motive := fun (x : Num) ↦ PosNum) n.pred' 1 id) : ℕ) = Nat.pred (↑n : ℕ)
have zero : ∀ (e : n.pred' = zero), (↑(Num.casesOn (motive := fun (x : Num) ↦ PosNum) zero 1 id) : ℕ) = Nat.pred (↑n : ℕ)
Tactic: cases e : pred' n
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
n : PosNum
h : 1 < n
zero :
  ∀ (e : n.pred' = Num.zero), (↑(Num.casesOn (motive := fun (x : Num) ↦ PosNum) Num.zero 1 id) : ℕ) = Nat.pred (↑n : ℕ)
⊢ (↑(Num.casesOn (motive := fun (x : Num) ↦ PosNum) n.pred' 1 id) : ℕ) = Nat.pred (↑n : ℕ)
have pos : ∀ (a : PosNum) (e : n.pred' = pos a),
  (↑(Num.casesOn (motive := fun (x : Num) ↦ PosNum) (pos a) 1 id) : ℕ) = Nat.pred (↑n : ℕ)
Tactic: cases e : pred' n
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (hypothesis)
Goal:
n : PosNum
h : 1 < n
e : n.pred' = zero
⊢ (↑(Num.casesOn (motive := fun (x : Num) ↦ PosNum) zero 1 id) : ℕ) = Nat.pred (↑n : ℕ)
have this : 1 ≤ Nat.pred (↑n : ℕ)
Tactic: have : (1 : ℕ) ≤ Nat.pred n := Nat.pred_le_pred ((@cast_lt ℕ _ _ _).2 h)
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (hypothesis)
Goal:
n : PosNum
h : 1 < n
e : n.pred' = zero
this : 1 ≤ Nat.pred (↑n : ℕ)
⊢ (↑(Num.casesOn (motive := fun (x : Num) ↦ PosNum) zero 1 id) : ℕ) = Nat.pred (↑n : ℕ)
have this₁ : LE.le (α := ℕ) 1 (↑zero : ℕ)
Tactic: rw [← pred'_to_nat, e] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
n : PosNum
h : 1 < n
a : PosNum
e : n.pred' = pos a
⊢ (↑(Num.casesOn (motive := fun (x : Num) ↦ PosNum) (pos a) 1 id) : ℕ) = Nat.pred (↑n : ℕ)
have pos : Eq (α := ℕ) (↑(Num.casesOn (motive := fun (x : Num) ↦ PosNum) (pos a) 1 id) : ℕ) (↑(pos a) : ℕ)
Tactic: rw [← pred'_to_nat, e]
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
a : PosNum
⊢ a.sub' 1 = a.pred'.toZNum
have one : one.sub' 1 = one.pred'.toZNum
Tactic: cases a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
a : PosNum
one : PosNum.one.sub' 1 = PosNum.one.pred'.toZNum
⊢ a.sub' 1 = a.pred'.toZNum
have bit1 : ∀ (a : PosNum), a.bit1.sub' 1 = a.bit1.pred'.toZNum
Tactic: cases a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
a : PosNum
one : PosNum.one.sub' 1 = PosNum.one.pred'.toZNum
bit1 : ∀ (a : PosNum), a.bit1.sub' 1 = a.bit1.pred'.toZNum
⊢ a.sub' 1 = a.pred'.toZNum
have bit0 : ∀ (a : PosNum), a.bit0.sub' 1 = a.bit0.pred'.toZNum
Tactic: cases a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
a : PosNum
⊢ sub' 1 a = a.pred'.toZNumNeg
have one : sub' 1 one = one.pred'.toZNumNeg
Tactic: cases a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
a : PosNum
one : sub' 1 PosNum.one = PosNum.one.pred'.toZNumNeg
⊢ sub' 1 a = a.pred'.toZNumNeg
have bit1 : ∀ (a : PosNum), sub' 1 a.bit1 = a.bit1.pred'.toZNumNeg
Tactic: cases a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
a : PosNum
one : sub' 1 PosNum.one = PosNum.one.pred'.toZNumNeg
bit1 : ∀ (a : PosNum), sub' 1 a.bit1 = a.bit1.pred'.toZNumNeg
⊢ sub' 1 a = a.pred'.toZNumNeg
have bit0 : ∀ (a : PosNum), sub' 1 a.bit0 = a.bit0.pred'.toZNumNeg
Tactic: cases a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
m n : PosNum
⊢ n.cmp m = Ordering.lt ↔ m.cmp n = Ordering.gt
have rw : (m.cmp n).swap = Ordering.lt ↔ m.cmp n = Ordering.gt
Tactic: rw [← cmp_swap]
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
m n : PosNum
⊢ (m.cmp n).swap = Ordering.lt ↔ m.cmp n = Ordering.gt
have lt : Ordering.lt.swap = Ordering.lt ↔ Ordering.lt = Ordering.gt
Tactic: cases cmp m n
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
m n : PosNum
lt : Ordering.lt.swap = Ordering.lt ↔ Ordering.lt = Ordering.gt
⊢ (m.cmp n).swap = Ordering.lt ↔ m.cmp n = Ordering.gt
have eq : Ordering.eq.swap = Ordering.lt ↔ Ordering.eq = Ordering.gt
Tactic: cases cmp m n
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
m n : PosNum
lt : Ordering.lt.swap = Ordering.lt ↔ Ordering.lt = Ordering.gt
eq : Ordering.eq.swap = Ordering.lt ↔ Ordering.eq = Ordering.gt
⊢ (m.cmp n).swap = Ordering.lt ↔ m.cmp n = Ordering.gt
have gt : Ordering.gt.swap = Ordering.lt ↔ Ordering.gt = Ordering.gt
Tactic: cases cmp m n
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
p : PosNum
⊢ (↑(pos p).pred : ℕ) = Nat.pred (↑(pos p) : ℕ)
have rw : Nat.pred (↑p : ℕ) = Nat.pred (↑(pos p) : ℕ)
Tactic: rw [pred, PosNum.pred'_to_nat]
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
p : PosNum
⊢ castNum <$> (pos p).ppred = Nat.ppred (↑(pos p) : ℕ)
have rw : Nat.succ (↑p.pred' : ℕ) = (↑(pos p) : ℕ)
Tactic: rw [ppred, Option.map_eq_map, Option.map_some, Nat.ppred_eq_some.2]
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
p : PosNum
⊢ Nat.succ (↑p.pred' : ℕ) = (↑(pos p) : ℕ)
have rw : Eq (α := ℕ) (↑p : ℕ) (↑(pos p) : ℕ)
Tactic: rw [PosNum.pred'_to_nat, Nat.succ_pred_eq_of_pos (PosNum.to_nat_pos _)]
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
m n : Num
⊢ (m.cmp n).swap = n.cmp m
have zero : (zero.cmp n).swap = n.cmp zero
Tactic: cases m
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
m n : Num
zero : (Num.zero.cmp n).swap = n.cmp Num.zero
⊢ (m.cmp n).swap = n.cmp m
have pos : ∀ (a : PosNum), ((pos a).cmp n).swap = n.cmp (pos a)
Tactic: cases m
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
n : Num
⊢ (zero.cmp n).swap = n.cmp zero
have zero : (zero.cmp zero).swap = zero.cmp zero
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
n : Num
zero : (Num.zero.cmp Num.zero).swap = Num.zero.cmp Num.zero
⊢ (Num.zero.cmp n).swap = n.cmp Num.zero
have zero₁ : ∀ (a : PosNum), (Num.zero.cmp (pos a)).swap = (pos a).cmp Num.zero
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
n : Num
a : PosNum
⊢ ((pos a).cmp n).swap = n.cmp (pos a)
have pos : ((pos a).cmp zero).swap = zero.cmp (pos a)
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
n : Num
a : PosNum
pos : ((Num.pos a).cmp zero).swap = zero.cmp (Num.pos a)
⊢ ((Num.pos a).cmp n).swap = n.cmp (Num.pos a)
have pos₁ : ∀ (a_1 : PosNum), ((Num.pos a).cmp (Num.pos a_1)).swap = (Num.pos a_1).cmp (Num.pos a)
Tactic: cases n
Cleared hypotheses: n