awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
a b : PosNum
⊢ Ordering.casesOn (motive := fun (x : Ordering) ↦ Prop) (a.bit1.cmp b.bit1)
    (LT.lt (α := ℕ) (↑a.bit1 : ℕ) (↑b.bit1 : ℕ)) (a.bit1 = b.bit1) (LT.lt (α := ℕ) (↑b.bit1 : ℕ) (↑a.bit1 : ℕ))
have dsimp : Ordering.rec (motive := fun (x : Ordering) ↦ Prop)
  (HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑a : ℕ) + 1 < HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑b : ℕ) + 1) (a.bit1 = b.bit1)
  (HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑b : ℕ) + 1 < HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑a : ℕ) + 1) (a.cmp b)
Tactic: dsimp [cmp]
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
a b : PosNum
⊢ Ordering.rec (motive := fun (x : Ordering) ↦ Prop)
    (HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑a : ℕ) + 1 < HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑b : ℕ) + 1) (a.bit1 = b.bit1)
    (HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑b : ℕ) + 1 < HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑a : ℕ) + 1) (a.cmp b)
have have : ∀
  (this :
    Ordering.casesOn (motive := fun (x : Ordering) ↦ Prop) (a.cmp b) (LT.lt (α := ℕ) (↑a : ℕ) (↑b : ℕ)) (a = b)
      (LT.lt (α := ℕ) (↑b : ℕ) (↑a : ℕ))),
  Ordering.rec (motive := fun (x : Ordering) ↦ Prop)
    (HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑a : ℕ) + 1 < HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑b : ℕ) + 1) (a.bit1 = b.bit1)
    (HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑b : ℕ) + 1 < HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑a : ℕ) + 1) (a.cmp b)
Tactic: have := cmp_to_nat a b
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
a b : PosNum
this :
  Ordering.casesOn (motive := fun (x : Ordering) ↦ Prop) (a.cmp b) (LT.lt (α := ℕ) (↑a : ℕ) (↑b : ℕ)) (a = b)
    (LT.lt (α := ℕ) (↑b : ℕ) (↑a : ℕ))
⊢ Ordering.rec (motive := fun (x : Ordering) ↦ Prop)
    (HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑a : ℕ) + 1 < HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑b : ℕ) + 1) (a.bit1 = b.bit1)
    (HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑b : ℕ) + 1 < HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑a : ℕ) + 1) (a.cmp b)
have revert : ∀
  (this :
    Ordering.casesOn (motive := fun (x : Ordering) ↦ Prop) (a.cmp b) (LT.lt (α := ℕ) (↑a : ℕ) (↑b : ℕ)) (a = b)
      (LT.lt (α := ℕ) (↑b : ℕ) (↑a : ℕ))),
  Ordering.rec (motive := fun (x : Ordering) ↦ Prop)
    (HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑a : ℕ) + 1 < HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑b : ℕ) + 1) (a.bit1 = b.bit1)
    (HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑b : ℕ) + 1 < HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑a : ℕ) + 1) (a.cmp b)
Tactic: revert this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
a b : PosNum
⊢ ∀
    (this :
      Ordering.casesOn (motive := fun (x : Ordering) ↦ Prop) (a.cmp b) (LT.lt (α := ℕ) (↑a : ℕ) (↑b : ℕ)) (a = b)
        (LT.lt (α := ℕ) (↑b : ℕ) (↑a : ℕ))),
    Ordering.rec (motive := fun (x : Ordering) ↦ Prop)
      (HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑a : ℕ) + 1 < HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑b : ℕ) + 1) (a.bit1 = b.bit1)
      (HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑b : ℕ) + 1 < HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑a : ℕ) + 1) (a.cmp b)
have lt : ∀
  (this :
    Ordering.casesOn (motive := fun (x : Ordering) ↦ Prop) Ordering.lt (LT.lt (α := ℕ) (↑a : ℕ) (↑b : ℕ)) (a = b)
      (LT.lt (α := ℕ) (↑b : ℕ) (↑a : ℕ))),
  Ordering.rec (motive := fun (x : Ordering) ↦ Prop)
    (HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑a : ℕ) + 1 < HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑b : ℕ) + 1) (a.bit1 = b.bit1)
    (HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑b : ℕ) + 1 < HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑a : ℕ) + 1) Ordering.lt
Tactic: cases cmp a b
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
a b : PosNum
lt :
  ∀
    (this :
      Ordering.casesOn (motive := fun (x : Ordering) ↦ Prop) Ordering.lt (LT.lt (α := ℕ) (↑a : ℕ) (↑b : ℕ)) (a = b)
        (LT.lt (α := ℕ) (↑b : ℕ) (↑a : ℕ))),
    Ordering.rec (motive := fun (x : Ordering) ↦ Prop)
      (HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑a : ℕ) + 1 < HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑b : ℕ) + 1) (a.bit1 = b.bit1)
      (HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑b : ℕ) + 1 < HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑a : ℕ) + 1) Ordering.lt
⊢ ∀
    (this :
      Ordering.casesOn (motive := fun (x : Ordering) ↦ Prop) (a.cmp b) (LT.lt (α := ℕ) (↑a : ℕ) (↑b : ℕ)) (a = b)
        (LT.lt (α := ℕ) (↑b : ℕ) (↑a : ℕ))),
    Ordering.rec (motive := fun (x : Ordering) ↦ Prop)
      (HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑a : ℕ) + 1 < HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑b : ℕ) + 1) (a.bit1 = b.bit1)
      (HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑b : ℕ) + 1 < HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑a : ℕ) + 1) (a.cmp b)
have eq : ∀
  (this :
    Ordering.casesOn (motive := fun (x : Ordering) ↦ Prop) Ordering.eq (LT.lt (α := ℕ) (↑a : ℕ) (↑b : ℕ)) (a = b)
      (LT.lt (α := ℕ) (↑b : ℕ) (↑a : ℕ))),
  Ordering.rec (motive := fun (x : Ordering) ↦ Prop)
    (HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑a : ℕ) + 1 < HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑b : ℕ) + 1) (a.bit1 = b.bit1)
    (HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑b : ℕ) + 1 < HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑a : ℕ) + 1) Ordering.eq
Tactic: cases cmp a b
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
a b : PosNum
lt :
  ∀
    (this :
      Ordering.casesOn (motive := fun (x : Ordering) ↦ Prop) Ordering.lt (LT.lt (α := ℕ) (↑a : ℕ) (↑b : ℕ)) (a = b)
        (LT.lt (α := ℕ) (↑b : ℕ) (↑a : ℕ))),
    Ordering.rec (motive := fun (x : Ordering) ↦ Prop)
      (HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑a : ℕ) + 1 < HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑b : ℕ) + 1) (a.bit1 = b.bit1)
      (HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑b : ℕ) + 1 < HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑a : ℕ) + 1) Ordering.lt
eq :
  ∀
    (this :
      Ordering.casesOn (motive := fun (x : Ordering) ↦ Prop) Ordering.eq (LT.lt (α := ℕ) (↑a : ℕ) (↑b : ℕ)) (a = b)
        (LT.lt (α := ℕ) (↑b : ℕ) (↑a : ℕ))),
    Ordering.rec (motive := fun (x : Ordering) ↦ Prop)
      (HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑a : ℕ) + 1 < HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑b : ℕ) + 1) (a.bit1 = b.bit1)
      (HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑b : ℕ) + 1 < HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑a : ℕ) + 1) Ordering.eq
⊢ ∀
    (this :
      Ordering.casesOn (motive := fun (x : Ordering) ↦ Prop) (a.cmp b) (LT.lt (α := ℕ) (↑a : ℕ) (↑b : ℕ)) (a = b)
        (LT.lt (α := ℕ) (↑b : ℕ) (↑a : ℕ))),
    Ordering.rec (motive := fun (x : Ordering) ↦ Prop)
      (HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑a : ℕ) + 1 < HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑b : ℕ) + 1) (a.bit1 = b.bit1)
      (HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑b : ℕ) + 1 < HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑a : ℕ) + 1) (a.cmp b)
have gt : ∀
  (this :
    Ordering.casesOn (motive := fun (x : Ordering) ↦ Prop) Ordering.gt (LT.lt (α := ℕ) (↑a : ℕ) (↑b : ℕ)) (a = b)
      (LT.lt (α := ℕ) (↑b : ℕ) (↑a : ℕ))),
  Ordering.rec (motive := fun (x : Ordering) ↦ Prop)
    (HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑a : ℕ) + 1 < HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑b : ℕ) + 1) (a.bit1 = b.bit1)
    (HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑b : ℕ) + 1 < HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑a : ℕ) + 1) Ordering.gt
Tactic: cases cmp a b
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
a b : PosNum
this : a = b
⊢ a.bit1 = b.bit1
have eq : b.bit1 = b.bit1
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
m n : PosNum
⊢ LE.le (α := ℕ) (↑m : ℕ) (↑n : ℕ) ↔ m ≤ n
have rw : ¬LT.lt (α := ℕ) (↑n : ℕ) (↑m : ℕ) ↔ m ≤ n
Tactic: rw [← not_lt]
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
n : Num
⊢ n + 0 = n
have zero : zero + 0 = zero
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
n : Num
zero : Num.zero + 0 = Num.zero
⊢ n + 0 = n
have pos : ∀ (a : PosNum), pos a + 0 = pos a
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
n : Num
⊢ 0 + n = n
have zero : 0 + zero = zero
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
n : Num
zero : 0 + Num.zero = Num.zero
⊢ 0 + n = n
have pos : ∀ (a : PosNum), 0 + pos a = pos a
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
p : PosNum
⊢ pos p + 1 = (pos p).succ
have one : pos one + 1 = (pos one).succ
Tactic: cases p
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
p : PosNum
one : pos PosNum.one + 1 = (pos PosNum.one).succ
⊢ pos p + 1 = (pos p).succ
have bit1 : ∀ (a : PosNum), pos a.bit1 + 1 = (pos a.bit1).succ
Tactic: cases p
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
p : PosNum
one : pos PosNum.one + 1 = (pos PosNum.one).succ
bit1 : ∀ (a : PosNum), pos a.bit1 + 1 = (pos a.bit1).succ
⊢ pos p + 1 = (pos p).succ
have bit0 : ∀ (a : PosNum), pos a.bit0 + 1 = (pos a.bit0).succ
Tactic: cases p
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
p : PosNum
⊢ pos (p + 1) = (pos p + 0).succ
have rw : pos p.succ = (pos p + 0).succ
Tactic: rw [PosNum.add_one, add_zero, succ, succ']
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
p : PosNum
rw : pos p.succ = (pos p + 0).succ
⊢ pos (p + 1) = (pos p + 0).succ
have rw₁ : pos p.succ = (pos p).succ
Tactic: rw [PosNum.add_one, add_zero, succ, succ']
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
p : PosNum
rw : pos p.succ = (pos p + 0).succ
rw₁ : pos p.succ = (pos p).succ
⊢ pos (p + 1) = (pos p + 0).succ
have rw₂ : pos p.succ = pos (pos p).succ'
Tactic: rw [PosNum.add_one, add_zero, succ, succ']
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
p : PosNum
rw : pos p.succ = (pos p + 0).succ
rw₁ : pos p.succ = (pos p).succ
rw₂ : pos p.succ = pos (pos p).succ'
⊢ pos (p + 1) = (pos p + 0).succ
have rw₃ : pos p.succ = pos p.succ
Tactic: rw [PosNum.add_one, add_zero, succ, succ']
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
b : Bool
n : ℕ
ih : ofNat' (n + 1) = ofNat' n + 1
⊢ ofNat' (Nat.bit b n + 1) = ofNat' (Nat.bit b n) + 1
have false : ofNat' (Nat.bit false n + 1) = ofNat' (Nat.bit false n) + 1
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
b : Bool
n : ℕ
ih : ofNat' (n + 1) = ofNat' n + 1
false : ofNat' (Nat.bit Bool.false n + 1) = ofNat' (Nat.bit Bool.false n) + 1
⊢ ofNat' (Nat.bit b n + 1) = ofNat' (Nat.bit b n) + 1
have true : ofNat' (Nat.bit true n + 1) = ofNat' (Nat.bit true n) + 1
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
n : ℕ
ih : ofNat' (n + 1) = ofNat' n + 1
⊢ ofNat' (Nat.bit false n + 1) = ofNat' (Nat.bit false n) + 1
have false : (bif true then Num.bit1 else Num.bit0) (ofNat' n) = (bif false then Num.bit1 else Num.bit0) (ofNat' n) + 1
Tactic: erw [ofNat'_bit true n, ofNat'_bit]
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
n : ℕ
ih : ofNat' (n + 1) = ofNat' n + 1
⊢ ofNat' (Nat.bit true n + 1) = ofNat' (Nat.bit true n) + 1
have true : (bif false then Num.bit1 else Num.bit0) (ofNat' n + 1) = (bif true then Num.bit1 else Num.bit0) (ofNat' n) + 1
Tactic: rw [show n.bit true + 1 = (n + 1).bit false by simp [Nat.bit, mul_add],
        ofNat'_bit, ofNat'_bit, ih]
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
m n : ℕ
⊢ ofNat' (m + n) = ofNat' m + ofNat' n
have zero : ofNat' (m + 0) = ofNat' m + ofNat' 0
Tactic: induction n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
m n : ℕ
zero : ofNat' (m + 0) = ofNat' m + ofNat' 0
⊢ ofNat' (m + n) = ofNat' m + ofNat' n
have succ : ∀ (n : ℕ), ofNat' (m + n) = ofNat' m + ofNat' n → ofNat' (m + (n + 1)) = ofNat' m + ofNat' (n + 1)
Tactic: induction n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
a b : PosNum
⊢ Ordering.casesOn (motive := fun (x : Ordering) ↦ Prop) ((pos a).cmp (pos b))
    (LT.lt (α := ℕ) (↑(pos a) : ℕ) (↑(pos b) : ℕ)) (pos a = pos b) (LT.lt (α := ℕ) (↑(pos b) : ℕ) (↑(pos a) : ℕ))
have have : ∀
  (this :
    Ordering.casesOn (motive := fun (x : Ordering) ↦ Prop) (a.cmp b) (LT.lt (α := ℕ) (↑a : ℕ) (↑b : ℕ)) (a = b)
      (LT.lt (α := ℕ) (↑b : ℕ) (↑a : ℕ))),
  Ordering.casesOn (motive := fun (x : Ordering) ↦ Prop) ((pos a).cmp (pos b))
    (LT.lt (α := ℕ) (↑(pos a) : ℕ) (↑(pos b) : ℕ)) (pos a = pos b) (LT.lt (α := ℕ) (↑(pos b) : ℕ) (↑(pos a) : ℕ))
Tactic: have := PosNum.cmp_to_nat a b
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
a b : PosNum
this :
  Ordering.casesOn (motive := fun (x : Ordering) ↦ Prop) (a.cmp b) (LT.lt (α := ℕ) (↑a : ℕ) (↑b : ℕ)) (a = b)
    (LT.lt (α := ℕ) (↑b : ℕ) (↑a : ℕ))
⊢ Ordering.casesOn (motive := fun (x : Ordering) ↦ Prop) ((pos a).cmp (pos b))
    (LT.lt (α := ℕ) (↑(pos a) : ℕ) (↑(pos b) : ℕ)) (pos a = pos b) (LT.lt (α := ℕ) (↑(pos b) : ℕ) (↑(pos a) : ℕ))
have revert : ∀
  (this :
    Ordering.casesOn (motive := fun (x : Ordering) ↦ Prop) (a.cmp b) (LT.lt (α := ℕ) (↑a : ℕ) (↑b : ℕ)) (a = b)
      (LT.lt (α := ℕ) (↑b : ℕ) (↑a : ℕ))),
  Ordering.casesOn (motive := fun (x : Ordering) ↦ Prop) ((pos a).cmp (pos b))
    (LT.lt (α := ℕ) (↑(pos a) : ℕ) (↑(pos b) : ℕ)) (pos a = pos b) (LT.lt (α := ℕ) (↑(pos b) : ℕ) (↑(pos a) : ℕ))
Tactic: revert this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
a b : PosNum
⊢ ∀
    (this :
      Ordering.casesOn (motive := fun (x : Ordering) ↦ Prop) (a.cmp b) (LT.lt (α := ℕ) (↑a : ℕ) (↑b : ℕ)) (a = b)
        (LT.lt (α := ℕ) (↑b : ℕ) (↑a : ℕ))),
    Ordering.casesOn (motive := fun (x : Ordering) ↦ Prop) ((pos a).cmp (pos b))
      (LT.lt (α := ℕ) (↑(pos a) : ℕ) (↑(pos b) : ℕ)) (pos a = pos b) (LT.lt (α := ℕ) (↑(pos b) : ℕ) (↑(pos a) : ℕ))
have dsimp : ∀
  (this :
    Ordering.rec (motive := fun (x : Ordering) ↦ Prop) (LT.lt (α := ℕ) (↑a : ℕ) (↑b : ℕ)) (a = b)
      (LT.lt (α := ℕ) (↑b : ℕ) (↑a : ℕ)) (a.cmp b)),
  Ordering.rec (motive := fun (x : Ordering) ↦ Prop) (LT.lt (α := ℕ) (↑a : ℕ) (↑b : ℕ)) (pos a = pos b)
    (LT.lt (α := ℕ) (↑b : ℕ) (↑a : ℕ)) (a.cmp b)
Tactic: dsimp [cmp]
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
a b : PosNum
⊢ ∀
    (this :
      Ordering.rec (motive := fun (x : Ordering) ↦ Prop) (LT.lt (α := ℕ) (↑a : ℕ) (↑b : ℕ)) (a = b)
        (LT.lt (α := ℕ) (↑b : ℕ) (↑a : ℕ)) (a.cmp b)),
    Ordering.rec (motive := fun (x : Ordering) ↦ Prop) (LT.lt (α := ℕ) (↑a : ℕ) (↑b : ℕ)) (pos a = pos b)
      (LT.lt (α := ℕ) (↑b : ℕ) (↑a : ℕ)) (a.cmp b)
have lt : ∀
  (this :
    Ordering.rec (motive := fun (x : Ordering) ↦ Prop) (LT.lt (α := ℕ) (↑a : ℕ) (↑b : ℕ)) (a = b)
      (LT.lt (α := ℕ) (↑b : ℕ) (↑a : ℕ)) Ordering.lt),
  Ordering.rec (motive := fun (x : Ordering) ↦ Prop) (LT.lt (α := ℕ) (↑a : ℕ) (↑b : ℕ)) (pos a = pos b)
    (LT.lt (α := ℕ) (↑b : ℕ) (↑a : ℕ)) Ordering.lt
Tactic: cases PosNum.cmp a b
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
a b : PosNum
lt :
  ∀
    (this :
      Ordering.rec (motive := fun (x : Ordering) ↦ Prop) (LT.lt (α := ℕ) (↑a : ℕ) (↑b : ℕ)) (a = b)
        (LT.lt (α := ℕ) (↑b : ℕ) (↑a : ℕ)) Ordering.lt),
    Ordering.rec (motive := fun (x : Ordering) ↦ Prop) (LT.lt (α := ℕ) (↑a : ℕ) (↑b : ℕ)) (pos a = pos b)
      (LT.lt (α := ℕ) (↑b : ℕ) (↑a : ℕ)) Ordering.lt
⊢ ∀
    (this :
      Ordering.rec (motive := fun (x : Ordering) ↦ Prop) (LT.lt (α := ℕ) (↑a : ℕ) (↑b : ℕ)) (a = b)
        (LT.lt (α := ℕ) (↑b : ℕ) (↑a : ℕ)) (a.cmp b)),
    Ordering.rec (motive := fun (x : Ordering) ↦ Prop) (LT.lt (α := ℕ) (↑a : ℕ) (↑b : ℕ)) (pos a = pos b)
      (LT.lt (α := ℕ) (↑b : ℕ) (↑a : ℕ)) (a.cmp b)
have eq : ∀
  (this :
    Ordering.rec (motive := fun (x : Ordering) ↦ Prop) (LT.lt (α := ℕ) (↑a : ℕ) (↑b : ℕ)) (a = b)
      (LT.lt (α := ℕ) (↑b : ℕ) (↑a : ℕ)) Ordering.eq),
  Ordering.rec (motive := fun (x : Ordering) ↦ Prop) (LT.lt (α := ℕ) (↑a : ℕ) (↑b : ℕ)) (pos a = pos b)
    (LT.lt (α := ℕ) (↑b : ℕ) (↑a : ℕ)) Ordering.eq
Tactic: cases PosNum.cmp a b
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
a b : PosNum
lt :
  ∀
    (this :
      Ordering.rec (motive := fun (x : Ordering) ↦ Prop) (LT.lt (α := ℕ) (↑a : ℕ) (↑b : ℕ)) (a = b)
        (LT.lt (α := ℕ) (↑b : ℕ) (↑a : ℕ)) Ordering.lt),
    Ordering.rec (motive := fun (x : Ordering) ↦ Prop) (LT.lt (α := ℕ) (↑a : ℕ) (↑b : ℕ)) (pos a = pos b)
      (LT.lt (α := ℕ) (↑b : ℕ) (↑a : ℕ)) Ordering.lt
eq :
  ∀
    (this :
      Ordering.rec (motive := fun (x : Ordering) ↦ Prop) (LT.lt (α := ℕ) (↑a : ℕ) (↑b : ℕ)) (a = b)
        (LT.lt (α := ℕ) (↑b : ℕ) (↑a : ℕ)) Ordering.eq),
    Ordering.rec (motive := fun (x : Ordering) ↦ Prop) (LT.lt (α := ℕ) (↑a : ℕ) (↑b : ℕ)) (pos a = pos b)
      (LT.lt (α := ℕ) (↑b : ℕ) (↑a : ℕ)) Ordering.eq
⊢ ∀
    (this :
      Ordering.rec (motive := fun (x : Ordering) ↦ Prop) (LT.lt (α := ℕ) (↑a : ℕ) (↑b : ℕ)) (a = b)
        (LT.lt (α := ℕ) (↑b : ℕ) (↑a : ℕ)) (a.cmp b)),
    Ordering.rec (motive := fun (x : Ordering) ↦ Prop) (LT.lt (α := ℕ) (↑a : ℕ) (↑b : ℕ)) (pos a = pos b)
      (LT.lt (α := ℕ) (↑b : ℕ) (↑a : ℕ)) (a.cmp b)
have gt : ∀
  (this :
    Ordering.rec (motive := fun (x : Ordering) ↦ Prop) (LT.lt (α := ℕ) (↑a : ℕ) (↑b : ℕ)) (a = b)
      (LT.lt (α := ℕ) (↑b : ℕ) (↑a : ℕ)) Ordering.gt),
  Ordering.rec (motive := fun (x : Ordering) ↦ Prop) (LT.lt (α := ℕ) (↑a : ℕ) (↑b : ℕ)) (pos a = pos b)
    (LT.lt (α := ℕ) (↑b : ℕ) (↑a : ℕ)) Ordering.gt
Tactic: cases PosNum.cmp a b
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
m n : Num
⊢ LE.le (α := ℕ) (↑m : ℕ) (↑n : ℕ) ↔ m ≤ n
have rw : ¬LT.lt (α := ℕ) (↑n : ℕ) (↑m : ℕ) ↔ m ≤ n
Tactic: rw [← not_lt]
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
transfer transfer₁ : ∀ (a b c : Num), a + b + c = a + (b + c)
⊢ ∀ (a b c : Num), a + b + c = a + (b + c)
have transfer₂ : ∀ (a b c : Num), HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑b : ℕ) + (↑c : ℕ) = (↑a : ℕ) + HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑c : ℕ)
Tactic: transfer
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
x x_1 : Num
⊢ x + x_1 = x_1 + x
have simp_rw : Eq (α := ℕ) (↑(x + x_1) : ℕ) (↑(x_1 + x) : ℕ)
Tactic: simp_rw [← to_nat_inj, add_to_nat, add_comm]
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
x x_1 : Num
simp_rw : Eq (α := ℕ) (↑(x + x_1) : ℕ) (↑(x_1 + x) : ℕ)
⊢ x + x_1 = x_1 + x
have simp_rw₁ : HAdd.hAdd (α := ℕ) (↑x : ℕ) (↑x_1 : ℕ) = HAdd.hAdd (α := ℕ) (↑x_1 : ℕ) (↑x : ℕ)
Tactic: simp_rw [← to_nat_inj, add_to_nat, add_comm]
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
x x_1 x_2 : Num
⊢ x * x_1 * x_2 = x * (x_1 * x_2)
have simp_rw : Eq (α := ℕ) (↑(x * x_1 * x_2) : ℕ) (↑(x * (x_1 * x_2)) : ℕ)
Tactic: simp_rw [← to_nat_inj, mul_to_nat, mul_assoc]
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
x x_1 x_2 : Num
simp_rw : Eq (α := ℕ) (↑(x * x_1 * x_2) : ℕ) (↑(x * (x_1 * x_2)) : ℕ)
⊢ x * x_1 * x_2 = x * (x_1 * x_2)
have simp_rw₁ : HMul.hMul (α := ℕ) (↑x : ℕ) (↑x_1 : ℕ) * (↑x_2 : ℕ) = (↑x : ℕ) * HMul.hMul (α := ℕ) (↑x_1 : ℕ) (↑x_2 : ℕ)
Tactic: simp_rw [← to_nat_inj, mul_to_nat, mul_assoc]
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
x : Num
⊢ 1 * x = x
have rw : Eq (α := ℕ) (↑(1 * x) : ℕ) (↑x : ℕ)
Tactic: rw [← to_nat_inj, mul_to_nat, cast_one, one_mul]
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
x : Num
rw : Eq (α := ℕ) (↑(1 * x) : ℕ) (↑x : ℕ)
⊢ 1 * x = x
have rw₁ : HMul.hMul (α := ℕ) (↑1 : ℕ) (↑x : ℕ) = (↑x : ℕ)
Tactic: rw [← to_nat_inj, mul_to_nat, cast_one, one_mul]
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
x : Num
rw : Eq (α := ℕ) (↑(1 * x) : ℕ) (↑x : ℕ)
rw₁ : HMul.hMul (α := ℕ) (↑1 : ℕ) (↑x : ℕ) = (↑x : ℕ)
⊢ 1 * x = x
have rw₂ : HMul.hMul (α := ℕ) 1 (↑x : ℕ) = (↑x : ℕ)
Tactic: rw [← to_nat_inj, mul_to_nat, cast_one, one_mul]
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
x : Num
rw : Eq (α := ℕ) (↑(1 * x) : ℕ) (↑x : ℕ)
rw₁ : HMul.hMul (α := ℕ) (↑1 : ℕ) (↑x : ℕ) = (↑x : ℕ)
rw₂ : HMul.hMul (α := ℕ) 1 (↑x : ℕ) = (↑x : ℕ)
⊢ 1 * x = x
have rw₃ : Eq (α := ℕ) (↑x : ℕ) (↑x : ℕ)
Tactic: rw [← to_nat_inj, mul_to_nat, cast_one, one_mul]
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
x : Num
⊢ x * 1 = x
have rw : Eq (α := ℕ) (↑(x * 1) : ℕ) (↑x : ℕ)
Tactic: rw [← to_nat_inj, mul_to_nat, cast_one, mul_one]
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
x : Num
rw : Eq (α := ℕ) (↑(x * 1) : ℕ) (↑x : ℕ)
⊢ x * 1 = x
have rw₁ : HMul.hMul (α := ℕ) (↑x : ℕ) (↑1 : ℕ) = (↑x : ℕ)
Tactic: rw [← to_nat_inj, mul_to_nat, cast_one, mul_one]
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
x : Num
rw : Eq (α := ℕ) (↑(x * 1) : ℕ) (↑x : ℕ)
rw₁ : HMul.hMul (α := ℕ) (↑x : ℕ) (↑1 : ℕ) = (↑x : ℕ)
⊢ x * 1 = x
have rw₂ : HMul.hMul (α := ℕ) (↑x : ℕ) 1 = (↑x : ℕ)
Tactic: rw [← to_nat_inj, mul_to_nat, cast_one, mul_one]
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
x : Num
rw : Eq (α := ℕ) (↑(x * 1) : ℕ) (↑x : ℕ)
rw₁ : HMul.hMul (α := ℕ) (↑x : ℕ) (↑1 : ℕ) = (↑x : ℕ)
rw₂ : HMul.hMul (α := ℕ) (↑x : ℕ) 1 = (↑x : ℕ)
⊢ x * 1 = x
have rw₃ : Eq (α := ℕ) (↑x : ℕ) (↑x : ℕ)
Tactic: rw [← to_nat_inj, mul_to_nat, cast_one, mul_one]
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
x : Num
⊢ 0 * x = 0
have rw : Eq (α := ℕ) (↑(0 * x) : ℕ) (↑0 : ℕ)
Tactic: rw [← to_nat_inj, mul_to_nat, cast_zero, zero_mul]
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
x : Num
rw : Eq (α := ℕ) (↑(0 * x) : ℕ) (↑0 : ℕ)
⊢ 0 * x = 0
have rw₁ : HMul.hMul (α := ℕ) (↑0 : ℕ) (↑x : ℕ) = (↑0 : ℕ)
Tactic: rw [← to_nat_inj, mul_to_nat, cast_zero, zero_mul]
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
x : Num
rw : Eq (α := ℕ) (↑(0 * x) : ℕ) (↑0 : ℕ)
rw₁ : HMul.hMul (α := ℕ) (↑0 : ℕ) (↑x : ℕ) = (↑0 : ℕ)
⊢ 0 * x = 0
have rw₂ : HMul.hMul (α := ℕ) 0 (↑x : ℕ) = 0
Tactic: rw [← to_nat_inj, mul_to_nat, cast_zero, zero_mul]
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
x : Num
rw : Eq (α := ℕ) (↑(0 * x) : ℕ) (↑0 : ℕ)
rw₁ : HMul.hMul (α := ℕ) (↑0 : ℕ) (↑x : ℕ) = (↑0 : ℕ)
rw₂ : HMul.hMul (α := ℕ) 0 (↑x : ℕ) = 0
⊢ 0 * x = 0
have rw₃ : Eq (α := ℕ) 0 0
Tactic: rw [← to_nat_inj, mul_to_nat, cast_zero, zero_mul]
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
x : Num
⊢ x * 0 = 0
have rw : Eq (α := ℕ) (↑(x * 0) : ℕ) (↑0 : ℕ)
Tactic: rw [← to_nat_inj, mul_to_nat, cast_zero, mul_zero]
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
x : Num
rw : Eq (α := ℕ) (↑(x * 0) : ℕ) (↑0 : ℕ)
⊢ x * 0 = 0
have rw₁ : HMul.hMul (α := ℕ) (↑x : ℕ) (↑0 : ℕ) = (↑0 : ℕ)
Tactic: rw [← to_nat_inj, mul_to_nat, cast_zero, mul_zero]
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
x : Num
rw : Eq (α := ℕ) (↑(x * 0) : ℕ) (↑0 : ℕ)
rw₁ : HMul.hMul (α := ℕ) (↑x : ℕ) (↑0 : ℕ) = (↑0 : ℕ)
⊢ x * 0 = 0
have rw₂ : HMul.hMul (α := ℕ) (↑x : ℕ) 0 = 0
Tactic: rw [← to_nat_inj, mul_to_nat, cast_zero, mul_zero]
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
x : Num
rw : Eq (α := ℕ) (↑(x * 0) : ℕ) (↑0 : ℕ)
rw₁ : HMul.hMul (α := ℕ) (↑x : ℕ) (↑0 : ℕ) = (↑0 : ℕ)
rw₂ : HMul.hMul (α := ℕ) (↑x : ℕ) 0 = 0
⊢ x * 0 = 0
have rw₃ : Eq (α := ℕ) 0 0
Tactic: rw [← to_nat_inj, mul_to_nat, cast_zero, mul_zero]
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
x x_1 : Num
⊢ x * x_1 = x_1 * x
have simp_rw : Eq (α := ℕ) (↑(x * x_1) : ℕ) (↑(x_1 * x) : ℕ)
Tactic: simp_rw [← to_nat_inj, mul_to_nat, mul_comm]
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
x x_1 : Num
simp_rw : Eq (α := ℕ) (↑(x * x_1) : ℕ) (↑(x_1 * x) : ℕ)
⊢ x * x_1 = x_1 * x
have simp_rw₁ : HMul.hMul (α := ℕ) (↑x : ℕ) (↑x_1 : ℕ) = HMul.hMul (α := ℕ) (↑x_1 : ℕ) (↑x : ℕ)
Tactic: simp_rw [← to_nat_inj, mul_to_nat, mul_comm]
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
a b c : Num
⊢ 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:
a b : Num
⊢ 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:
a b : Num
h : a ≤ b
c : Num
⊢ a + c ≤ b + c
have revert : ∀ (h : a ≤ b), a + c ≤ b + c
Tactic: revert h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
a b c : Num
⊢ ∀ (h : a ≤ b), a + c ≤ b + c
have transfer_rw : ∀ (h : LE.le (α := ℕ) (↑a : ℕ) (↑b : ℕ)), HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑c : ℕ) ≤ HAdd.hAdd (α := ℕ) (↑b : ℕ) (↑c : ℕ)
Tactic: transfer_rw
-- Lean 4 proof step from Mathlib.Data.Num.Lemmas (goal)
Goal:
a b c : Num
⊢ a + b ≤ a + c → b ≤ c
have transfer_rw : HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑b : ℕ) ≤ HAdd.hAdd (α := ℕ) (↑a : ℕ) (↑c : ℕ) → LE.le (α := ℕ) (↑b : ℕ) (↑c : ℕ)
Tactic: transfer_rw