awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
a b : Num
⊢ a ≤ b ∨ b ≤ a
have transfer_rw : LE.le (α := ℕ) (↑a : ℕ) (↑b : ℕ) ∨ LE.le (α := ℕ) (↑b : ℕ) (↑a : ℕ)
Tactic: transfer_rw
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
a : Num
ha : 0 < a
b c : Num
⊢ ∀ (hbc : b < c), a * b < a * c
have revert : ∀ (ha : 0 < a) (hbc : b < c), a * b < a * c
Tactic: revert ha
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
a b c : Num
⊢ ∀ (ha : 0 < a) (hbc : b < c), a * b < a * c
have transfer_rw : ∀ (ha : LT.lt (α := ℕ) 0 (↑a : ℕ)) (hbc : LT.lt (α := ℕ) (↑b : ℕ) (↑c : ℕ)),
  HMul.hMul (α := ℕ) (↑a : ℕ) (↑b : ℕ) < HMul.hMul (α := ℕ) (↑a : ℕ) (↑c : ℕ)
Tactic: transfer_rw
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
a : Num
ha : 0 < a
b c : Num
⊢ ∀ (hab : b < c), b * a < c * a
have revert : ∀ (ha : 0 < a) (hab : b < c), b * a < c * a
Tactic: revert ha
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
a b c : Num
⊢ ∀ (ha : 0 < a) (hab : b < c), b * a < c * a
have transfer_rw : ∀ (ha : LT.lt (α := ℕ) 0 (↑a : ℕ)) (hab : LT.lt (α := ℕ) (↑b : ℕ) (↑c : ℕ)),
  HMul.hMul (α := ℕ) (↑b : ℕ) (↑a : ℕ) < HMul.hMul (α := ℕ) (↑c : ℕ) (↑a : ℕ)
Tactic: transfer_rw
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
α : Type u_1
inst : AddGroupWithOne α
n : Num
⊢ Eq.{u_1 + 1} (α := α) (↑(↑n : ℤ) : α) (↑n : α)
have rw : Eq.{u_1 + 1} (α := α) (↑(↑(↑n : ℕ) : ℤ) : α) (↑n : α)
Tactic: rw [← to_nat_to_int, Int.cast_natCast, cast_to_nat]
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
α : Type u_1
inst : AddGroupWithOne α
n : Num
rw : Eq.{u_1 + 1} (α := α) (↑(↑(↑n : ℕ) : ℤ) : α) (↑n : α)
⊢ Eq.{u_1 + 1} (α := α) (↑(↑n : ℤ) : α) (↑n : α)
have rw₁ : Eq.{u_1 + 1} (α := α) (↑(↑n : ℕ) : α) (↑n : α)
Tactic: rw [← to_nat_to_int, Int.cast_natCast, cast_to_nat]
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
α : Type u_1
inst : AddGroupWithOne α
n : Num
rw : Eq.{u_1 + 1} (α := α) (↑(↑(↑n : ℕ) : ℤ) : α) (↑n : α)
rw₁ : Eq.{u_1 + 1} (α := α) (↑(↑n : ℕ) : α) (↑n : α)
⊢ Eq.{u_1 + 1} (α := α) (↑(↑n : ℤ) : α) (↑n : α)
have rw₂ : Eq.{u_1 + 1} (α := α) (↑n : α) (↑n : α)
Tactic: rw [← to_nat_to_int, Int.cast_natCast, cast_to_nat]
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
⊢ Eq (α := ℕ) (↑(↑0 : Num) : ℕ) 0
have rw : Eq (α := ℕ) (↑0 : ℕ) 0
Tactic: rw [Nat.cast_zero, cast_zero]
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
rw : Eq (α := ℕ) (↑0 : ℕ) 0
⊢ Eq (α := ℕ) (↑(↑0 : Num) : ℕ) 0
have rw₁ : Eq (α := ℕ) 0 0
Tactic: rw [Nat.cast_zero, cast_zero]
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
n : ℕ
⊢ (↑(↑(n + 1) : Num) : ℕ) = n + 1
have rw : (↑(HAdd.hAdd (α := Num) (↑n : Num) 1) : ℕ) = n + 1
Tactic: rw [Nat.cast_succ, add_one, succ_to_nat, to_of_nat n]
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
n : ℕ
rw : (↑(HAdd.hAdd (α := Num) (↑n : Num) 1) : ℕ) = n + 1
⊢ (↑(↑(n + 1) : Num) : ℕ) = n + 1
have rw₁ : (↑(succ (↑n : Num)) : ℕ) = n + 1
Tactic: rw [Nat.cast_succ, add_one, succ_to_nat, to_of_nat n]
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
n : ℕ
rw : (↑(HAdd.hAdd (α := Num) (↑n : Num) 1) : ℕ) = n + 1
rw₁ : (↑(succ (↑n : Num)) : ℕ) = n + 1
⊢ (↑(↑(n + 1) : Num) : ℕ) = n + 1
have rw₂ : HAdd.hAdd (α := ℕ) (↑(↑n : Num) : ℕ) 1 = n + 1
Tactic: rw [Nat.cast_succ, add_one, succ_to_nat, to_of_nat n]
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
n : ℕ
rw : (↑(HAdd.hAdd (α := Num) (↑n : Num) 1) : ℕ) = n + 1
rw₁ : (↑(succ (↑n : Num)) : ℕ) = n + 1
rw₂ : HAdd.hAdd (α := ℕ) (↑(↑n : Num) : ℕ) 1 = n + 1
⊢ (↑(↑(n + 1) : Num) : ℕ) = n + 1
have rw₃ : n + 1 = n + 1
Tactic: rw [Nat.cast_succ, add_one, succ_to_nat, to_of_nat n]
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
α : Type u_1
inst : AddMonoidWithOne α
n : ℕ
⊢ Eq.{u_1 + 1} (α := α) (↑(↑n : Num) : α) (↑n : α)
have rw : Eq.{u_1 + 1} (α := α) (↑(↑(↑n : Num) : ℕ) : α) (↑n : α)
Tactic: rw [← cast_to_nat, to_of_nat]
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
α : Type u_1
inst : AddMonoidWithOne α
n : ℕ
rw : Eq.{u_1 + 1} (α := α) (↑(↑(↑n : Num) : ℕ) : α) (↑n : α)
⊢ Eq.{u_1 + 1} (α := α) (↑(↑n : Num) : α) (↑n : α)
have rw₁ : Eq.{u_1 + 1} (α := α) (↑n : α) (↑n : α)
Tactic: rw [← cast_to_nat, to_of_nat]
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
m n : Num
h : Dvd.dvd (α := ℕ) (↑m : ℕ) (↑n : ℕ)
k : ℕ
e : (↑n : ℕ) = (↑m : ℕ) * k
⊢ n = m * (↑k : Num)
have rw : (↑((↑m : ℕ) * k) : Num) = m * (↑k : Num)
Tactic: rw [← of_to_nat n, e]
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
m n : PosNum
h : Eq (α := ℕ) (↑m : ℕ) (↑n : ℕ)
⊢ pos m = pos n
have rw : (↑(↑m : ℕ) : Num) = pos n
Tactic: rw [← PosNum.of_to_nat, ← PosNum.of_to_nat, h]
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
m n : PosNum
h : Eq (α := ℕ) (↑m : ℕ) (↑n : ℕ)
rw : (↑(↑m : ℕ) : Num) = pos n
⊢ pos m = pos n
have rw₁ : Eq (α := Num) (↑(↑m : ℕ) : Num) (↑(↑n : ℕ) : Num)
Tactic: rw [← PosNum.of_to_nat, ← PosNum.of_to_nat, h]
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
m n : PosNum
h : Eq (α := ℕ) (↑m : ℕ) (↑n : ℕ)
rw : (↑(↑m : ℕ) : Num) = pos n
rw₁ : Eq (α := Num) (↑(↑m : ℕ) : Num) (↑(↑n : ℕ) : Num)
⊢ pos m = pos n
have rw₂ : Eq (α := Num) (↑(↑n : ℕ) : Num) (↑(↑n : ℕ) : Num)
Tactic: rw [← PosNum.of_to_nat, ← PosNum.of_to_nat, h]
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
n : PosNum
⊢ Nat.succ (↑n.pred' : ℕ) = (↑n : ℕ)
have rw : (Nat.pred (↑n : ℕ)).succ = (↑n : ℕ)
Tactic: rw [pred'_to_nat n, Nat.succ_pred_eq_of_pos (to_nat_pos n)]
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
n : PosNum
rw : (Nat.pred (↑n : ℕ)).succ = (↑n : ℕ)
⊢ Nat.succ (↑n.pred' : ℕ) = (↑n : ℕ)
have rw₁ : Eq (α := ℕ) (↑n : ℕ) (↑n : ℕ)
Tactic: rw [pred'_to_nat n, Nat.succ_pred_eq_of_pos (to_nat_pos n)]
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
n : PosNum
this : Nat.succ (↑n.pred' : ℕ) = (↑n : ℕ)
h : Eq (α := ℕ) (↑1 : ℕ) (↑n : ℕ)
⊢ (↑(Num.casesOn (motive := fun (x : Num) ↦ PosNum) 0 1 bit1) : ℕ) = (HAdd.hAdd (α := ℕ) (↑n : ℕ) (↑n : ℕ)).pred
have rw : (↑(Num.casesOn (motive := fun (x : Num) ↦ PosNum) 0 1 bit1) : ℕ) = (HAdd.hAdd (α := ℕ) (↑1 : ℕ) (↑1 : ℕ)).pred
Tactic: rw [← to_nat_inj.1 h]
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
n : PosNum
this : Nat.succ (↑n.pred' : ℕ) = (↑n : ℕ)
p : PosNum
h : Nat.succ (↑p : ℕ) = (↑n : ℕ)
⊢ (↑(Num.casesOn (motive := fun (x : Num) ↦ PosNum) (pos p) 1 bit1) : ℕ) = (HAdd.hAdd (α := ℕ) (↑n : ℕ) (↑n : ℕ)).pred
have rw : (↑(Num.casesOn (motive := fun (x : Num) ↦ PosNum) (pos p) 1 bit1) : ℕ) = (Nat.succ (↑p : ℕ) + Nat.succ (↑p : ℕ)).pred
Tactic: rw [← h]
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
n : Num
⊢ Eq (α := ℕ) (↑n.succ'.pred' : ℕ) (↑n : ℕ)
have rw : Nat.pred (↑n.succ' : ℕ) = (↑n : ℕ)
Tactic: rw [pred'_to_nat, succ'_to_nat, Nat.add_one, Nat.pred_succ]
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
n : Num
rw : Nat.pred (↑n.succ' : ℕ) = (↑n : ℕ)
⊢ Eq (α := ℕ) (↑n.succ'.pred' : ℕ) (↑n : ℕ)
have rw₁ : (HAdd.hAdd (α := ℕ) (↑n : ℕ) 1).pred = (↑n : ℕ)
Tactic: rw [pred'_to_nat, succ'_to_nat, Nat.add_one, Nat.pred_succ]
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
n : Num
rw : Nat.pred (↑n.succ' : ℕ) = (↑n : ℕ)
rw₁ : (HAdd.hAdd (α := ℕ) (↑n : ℕ) 1).pred = (↑n : ℕ)
rw₂ : (Nat.succ (↑n : ℕ)).pred = (↑n : ℕ)
⊢ Eq (α := ℕ) (↑n.succ'.pred' : ℕ) (↑n : ℕ)
have rw₃ : Eq (α := ℕ) (↑n : ℕ) (↑n : ℕ)
Tactic: rw [pred'_to_nat, succ'_to_nat, Nat.add_one, Nat.pred_succ]
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
n : PosNum
⊢ Eq (α := ℕ) (↑n.pred'.succ' : ℕ) (↑n : ℕ)
have rw : HAdd.hAdd (α := ℕ) (↑n.pred' : ℕ) 1 = (↑n : ℕ)
Tactic: rw [succ'_to_nat, pred'_to_nat, Nat.add_one, Nat.succ_pred_eq_of_pos (to_nat_pos _)]
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
n : PosNum
rw : HAdd.hAdd (α := ℕ) (↑n.pred' : ℕ) 1 = (↑n : ℕ)
⊢ Eq (α := ℕ) (↑n.pred'.succ' : ℕ) (↑n : ℕ)
have rw₁ : Nat.pred (↑n : ℕ) + 1 = (↑n : ℕ)
Tactic: rw [succ'_to_nat, pred'_to_nat, Nat.add_one, Nat.succ_pred_eq_of_pos (to_nat_pos _)]
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
n : PosNum
rw : HAdd.hAdd (α := ℕ) (↑n.pred' : ℕ) 1 = (↑n : ℕ)
rw₁ : Nat.pred (↑n : ℕ) + 1 = (↑n : ℕ)
rw₂ : (Nat.pred (↑n : ℕ)).succ = (↑n : ℕ)
⊢ Eq (α := ℕ) (↑n.pred'.succ' : ℕ) (↑n : ℕ)
have rw₃ : Eq (α := ℕ) (↑n : ℕ) (↑n : ℕ)
Tactic: rw [succ'_to_nat, pred'_to_nat, Nat.add_one, Nat.succ_pred_eq_of_pos (to_nat_pos _)]
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
n : PosNum
⊢ (↑n.bit0.size : ℕ) = Nat.size (↑n.bit0 : ℕ)
have rw : Nat.bit false (↑n : ℕ) ≠ 0
Tactic: rw [size, succ_to_nat, size_to_nat n, cast_bit0, ← two_mul, ← Nat.bit_false_apply,
        Nat.size_bit]
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (hypothesis)
Goal:
n : PosNum
⊢ Nat.bit false (↑n : ℕ) ≠ 0
have this : LT.lt (α := ℕ) 0 (↑n : ℕ)
Tactic: have := to_nat_pos n
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
n : PosNum
⊢ (↑n.bit1.size : ℕ) = Nat.size (↑n.bit1 : ℕ)
have rw : Nat.bit true (↑n : ℕ) ≠ 0
Tactic: rw [size, succ_to_nat, size_to_nat n, cast_bit1, ← two_mul, ← Nat.bit_true_apply,
        Nat.size_bit]
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
n : PosNum
⊢ (↑n.bit0.size : ℕ) = n.bit0.natSize
have rw : (↑n.size.succ : ℕ) = n.bit0.natSize
Tactic: rw [size, succ_to_nat, natSize, size_eq_natSize n]
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
n : PosNum
rw : (↑n.size.succ : ℕ) = n.bit0.natSize
⊢ (↑n.bit0.size : ℕ) = n.bit0.natSize
have rw₁ : HAdd.hAdd (α := ℕ) (↑n.size : ℕ) 1 = n.bit0.natSize
Tactic: rw [size, succ_to_nat, natSize, size_eq_natSize n]
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
n : PosNum
rw : (↑n.size.succ : ℕ) = n.bit0.natSize
rw₁ : HAdd.hAdd (α := ℕ) (↑n.size : ℕ) 1 = n.bit0.natSize
⊢ (↑n.bit0.size : ℕ) = n.bit0.natSize
have rw₂ : HAdd.hAdd (α := ℕ) (↑n.size : ℕ) 1 = n.natSize.succ
Tactic: rw [size, succ_to_nat, natSize, size_eq_natSize n]
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
n : PosNum
rw : (↑n.size.succ : ℕ) = n.bit0.natSize
rw₁ : HAdd.hAdd (α := ℕ) (↑n.size : ℕ) 1 = n.bit0.natSize
rw₂ : HAdd.hAdd (α := ℕ) (↑n.size : ℕ) 1 = n.natSize.succ
⊢ (↑n.bit0.size : ℕ) = n.bit0.natSize
have rw₃ : n.natSize + 1 = n.natSize.succ
Tactic: rw [size, succ_to_nat, natSize, size_eq_natSize n]
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
n : PosNum
⊢ (↑n.bit1.size : ℕ) = n.bit1.natSize
have rw : (↑n.size.succ : ℕ) = n.bit1.natSize
Tactic: rw [size, succ_to_nat, natSize, size_eq_natSize n]
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
n : PosNum
rw : (↑n.size.succ : ℕ) = n.bit1.natSize
⊢ (↑n.bit1.size : ℕ) = n.bit1.natSize
have rw₁ : HAdd.hAdd (α := ℕ) (↑n.size : ℕ) 1 = n.bit1.natSize
Tactic: rw [size, succ_to_nat, natSize, size_eq_natSize n]
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
n : PosNum
rw : (↑n.size.succ : ℕ) = n.bit1.natSize
rw₁ : HAdd.hAdd (α := ℕ) (↑n.size : ℕ) 1 = n.bit1.natSize
⊢ (↑n.bit1.size : ℕ) = n.bit1.natSize
have rw₂ : HAdd.hAdd (α := ℕ) (↑n.size : ℕ) 1 = n.natSize.succ
Tactic: rw [size, succ_to_nat, natSize, size_eq_natSize n]
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
n : PosNum
rw : (↑n.size.succ : ℕ) = n.bit1.natSize
rw₁ : HAdd.hAdd (α := ℕ) (↑n.size : ℕ) 1 = n.bit1.natSize
rw₂ : HAdd.hAdd (α := ℕ) (↑n.size : ℕ) 1 = n.natSize.succ
⊢ (↑n.bit1.size : ℕ) = n.bit1.natSize
have rw₃ : n.natSize + 1 = n.natSize.succ
Tactic: rw [size, succ_to_nat, natSize, size_eq_natSize n]
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
n : PosNum
⊢ 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 : PosNum
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 : PosNum
⊢ 0 < n.natSize
have one : 0 < one.natSize
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
n : PosNum
one : 0 < PosNum.one.natSize
⊢ 0 < n.natSize
have bit1 : ∀ (a : PosNum), 0 < a.bit1.natSize
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
n : PosNum
one : 0 < PosNum.one.natSize
bit1 : ∀ (a : PosNum), 0 < a.bit1.natSize
⊢ 0 < n.natSize
have bit0 : ∀ (a : PosNum), 0 < a.bit0.natSize
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
α : Type u_1
transfer transfer₁ : ∀ (a b c : PosNum), a + b + c = a + (b + c)
⊢ ∀ (a b c : PosNum), a + b + c = a + (b + c)
have transfer₂ : ∀ (a b c : PosNum), HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑b : ℕ) + (↑c : ℕ) = (↑a : ℕ) + HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑c : ℕ)
Tactic: transfer
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
α : Type u_1
transfer transfer₁ : ∀ (a b : PosNum), a + b = b + a
⊢ ∀ (a b : PosNum), a + b = b + a
have transfer₂ : ∀ (a b : PosNum), HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑b : ℕ) = HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑a : ℕ)
Tactic: transfer
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
α : Type u_1
transfer transfer₁ : ∀ (a b c : PosNum), a * b * c = a * (b * c)
⊢ ∀ (a b c : PosNum), a * b * c = a * (b * c)
have transfer₂ : ∀ (a b c : PosNum), HMul.hMul (α := ℕ) (↑a : ℕ) (↑b : ℕ) * (↑c : ℕ) = (↑a : ℕ) * HMul.hMul (α := ℕ) (↑b : ℕ) (↑c : ℕ)
Tactic: transfer
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
α : Type u_1
transfer transfer₁ : ∀ (a : PosNum), 1 * a = a
⊢ ∀ (a : PosNum), 1 * a = a
have transfer₂ : ∀ (a : PosNum), HMul.hMul (α := ℕ) 1 (↑a : ℕ) = (↑a : ℕ)
Tactic: transfer
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
α : Type u_1
transfer transfer₁ : ∀ (a : PosNum), a * 1 = a
⊢ ∀ (a : PosNum), a * 1 = a
have transfer₂ : ∀ (a : PosNum), HMul.hMul (α := ℕ) (↑a : ℕ) 1 = (↑a : ℕ)
Tactic: transfer
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
α : Type u_1
transfer transfer₁ : ∀ (a b : PosNum), a * b = b * a
⊢ ∀ (a b : PosNum), a * b = b * a
have transfer₂ : ∀ (a b : PosNum), HMul.hMul (α := ℕ) (↑a : ℕ) (↑b : ℕ) = HMul.hMul (α := ℕ) (↑b : ℕ) (↑a : ℕ)
Tactic: transfer
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
α : Type u_1
⊢ ∀ (a b c : PosNum), a * (b + c) = a * b + a * c
have transfer : ∀ (a b c : PosNum),
  (↑a : ℕ) * HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑c : ℕ) =
    HMul.hMul (α := ℕ) (↑a : ℕ) (↑b : ℕ) + HMul.hMul (α := ℕ) (↑a : ℕ) (↑c : ℕ)
Tactic: transfer
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
α : Type u_1
⊢ ∀ (a b c : PosNum), (a + b) * c = a * c + b * c
have transfer : ∀ (a b c : PosNum),
  (↑c : ℕ) * HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑b : ℕ) =
    HMul.hMul (α := ℕ) (↑a : ℕ) (↑c : ℕ) + HMul.hMul (α := ℕ) (↑b : ℕ) (↑c : ℕ)
Tactic: transfer
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
α : Type u_1
a b c : PosNum
⊢ a ≤ b → b ≤ c → a ≤ c
have transfer_rw : LE.le (α := ℕ) (↑a : ℕ) (↑b : ℕ) → LE.le (α := ℕ) (↑b : ℕ) (↑c : ℕ) → LE.le (α := ℕ) (↑a : ℕ) (↑c : ℕ)
Tactic: transfer_rw
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
α : Type u_1
a b : PosNum
⊢ a < b ↔ a ≤ b ∧ ¬b ≤ a
have transfer_rw : LT.lt (α := ℕ) (↑a : ℕ) (↑b : ℕ) ↔ LE.le (α := ℕ) (↑a : ℕ) (↑b : ℕ) ∧ ¬LE.le (α := ℕ) (↑b : ℕ) (↑a : ℕ)
Tactic: transfer_rw
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
α : Type u_1
a b : PosNum
⊢ a ≤ b → b ≤ a → a = b
have transfer_rw : LE.le (α := ℕ) (↑a : ℕ) (↑b : ℕ) → LE.le (α := ℕ) (↑b : ℕ) (↑a : ℕ) → Eq (α := ℕ) (↑a : ℕ) (↑b : ℕ)
Tactic: transfer_rw
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
α : Type u_1
a b : PosNum
⊢ a ≤ b ∨ b ≤ a
have transfer_rw : LE.le (α := ℕ) (↑a : ℕ) (↑b : ℕ) ∨ LE.le (α := ℕ) (↑b : ℕ) (↑a : ℕ)
Tactic: transfer_rw
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
n : PosNum
⊢ (↑n : Num) = pos n
have rw : (↑(↑n : ℕ) : Num) = pos n
Tactic: rw [← cast_to_nat, ← of_to_nat n]
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
n : PosNum
rw : (↑(↑n : ℕ) : Num) = pos n
⊢ (↑n : Num) = pos n
have rw₁ : Eq (α := Num) (↑(↑n : ℕ) : Num) (↑(↑n : ℕ) : Num)
Tactic: rw [← cast_to_nat, ← of_to_nat n]
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
b : Bool
n : PosNum
⊢ (↑(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 : PosNum
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:
α : Type u_1
inst : AddMonoidWithOne α
m n : PosNum
⊢ (↑(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 : PosNum
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 : PosNum
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 : PosNum
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 : PosNum
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 : AddMonoidWithOne α
n : PosNum
⊢ (↑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.Lemmas (goal)
Goal:
α : Type u_1
inst : AddMonoidWithOne α
n : PosNum
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.Lemmas (goal)
Goal:
α : Type u_1
inst : AddMonoidWithOne α
n : PosNum
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.Lemmas (goal)
Goal:
α : Type u_1
inst : AddMonoidWithOne α
inst_1 : CharZero α
m n : PosNum
⊢ Eq.{u_1 + 1} (α := α) (↑m : α) (↑n : α) ↔ m = n
have rw : Eq.{u_1 + 1} (α := α) (↑(↑m : ℕ) : α) (↑n : α) ↔ m = n
Tactic: rw [← cast_to_nat m, ← cast_to_nat n, Nat.cast_inj, to_nat_inj]
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
α : Type u_1
inst : AddMonoidWithOne α
inst_1 : CharZero α
m n : PosNum
rw : Eq.{u_1 + 1} (α := α) (↑(↑m : ℕ) : α) (↑n : α) ↔ m = n
⊢ Eq.{u_1 + 1} (α := α) (↑m : α) (↑n : α) ↔ m = n
have rw₁ : Eq.{u_1 + 1} (α := α) (↑(↑m : ℕ) : α) (↑(↑n : ℕ) : α) ↔ m = n
Tactic: rw [← cast_to_nat m, ← cast_to_nat n, Nat.cast_inj, to_nat_inj]
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
α : Type u_1
inst : AddMonoidWithOne α
inst_1 : CharZero α
m n : PosNum
rw : Eq.{u_1 + 1} (α := α) (↑(↑m : ℕ) : α) (↑n : α) ↔ m = n
rw₁ : Eq.{u_1 + 1} (α := α) (↑(↑m : ℕ) : α) (↑(↑n : ℕ) : α) ↔ m = n
⊢ Eq.{u_1 + 1} (α := α) (↑m : α) (↑n : α) ↔ m = n
have rw₂ : Eq (α := ℕ) (↑m : ℕ) (↑n : ℕ) ↔ m = n
Tactic: rw [← cast_to_nat m, ← cast_to_nat n, Nat.cast_inj, to_nat_inj]
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
α : Type u_1
inst : AddMonoidWithOne α
inst_1 : CharZero α
m n : PosNum
rw : Eq.{u_1 + 1} (α := α) (↑(↑m : ℕ) : α) (↑n : α) ↔ m = n
rw₁ : Eq.{u_1 + 1} (α := α) (↑(↑m : ℕ) : α) (↑(↑n : ℕ) : α) ↔ m = n
rw₂ : Eq (α := ℕ) (↑m : ℕ) (↑n : ℕ) ↔ m = n
⊢ Eq.{u_1 + 1} (α := α) (↑m : α) (↑n : α) ↔ m = n
have rw₃ : m = n ↔ m = n
Tactic: rw [← cast_to_nat m, ← cast_to_nat n, Nat.cast_inj, to_nat_inj]
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
α : Type u_1
inst : Semiring α
inst_1 : PartialOrder α
inst_2 : IsStrictOrderedRing α
n : PosNum
⊢ LE.le.{u_1} (α := α) 1 (↑n : α)
have rw : LE.le (α := ℕ) 1 (↑n : ℕ)
Tactic: rw [← cast_to_nat, ← Nat.cast_one, Nat.cast_le (α := α)]
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
α : Type u_1
inst : NonAssocSemiring α
m n : PosNum
⊢ (↑(m * n) : α) = HMul.hMul (α := α) (↑m : α) (↑n : α)
have rw : (↑(↑(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 (goal)
Goal:
α : Type u_1
inst : NonAssocSemiring α
m n : PosNum
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_nat, mul_to_nat, Nat.cast_mul, cast_to_nat, cast_to_nat]
-- 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 : α)
⊢ (↑(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 (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 : α)
⊢ (↑(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]