awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
n d : PosNum
q r : Num
h₁ : (↑r : ℕ) + (↑d : ℕ) * HAdd.hAdd (α := ℕ) (↑q : ℕ) (↑q : ℕ) = (↑n : ℕ)
h₂ : (↑r : ℕ) < HMul.hMul (α := ℕ) 2 (↑d : ℕ)
this : ∀ {r₂ : Num}, Num.ofZNum' (r.sub' (Num.pos d)) = some r₂ ↔ (↑r : ℕ) = HAdd.hAdd (α := ℕ) (↑r₂ : ℕ) (↑d : ℕ)
e : Num.ofZNum' (r.sub' (Num.pos d)) = none
⊢ (↑(match (motive := Option Num → Num × Num) none with
              | some r' => (q.bit1, r')
              | none => (q.bit0, r)).2 :
          ℕ) +
        (↑d : ℕ) * HAdd.hAdd (α := ℕ) (↑q : ℕ) (↑q : ℕ) =
      (↑n : ℕ) ∧
    LT.lt (α := ℕ)
      (↑(match (motive := Option Num → Num × Num) none with
            | some r' => (q.bit1, r')
            | none => (q.bit0, r)).2 :
        ℕ)
      (↑d : ℕ)
have none : ∀
  (h :
    LE.le (α := ℕ) (↑d : ℕ)
      (↑(match (motive := Option Num → Num × Num) none with
            | some r' => (q.bit1, r')
            | none => (q.bit0, r)).2 :
        ℕ)),
  False
Tactic: refine ⟨h₁, lt_of_not_ge fun h => ?_⟩
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
n d : PosNum
q r : Num
h₁ : (↑r : ℕ) + (↑d : ℕ) * HAdd.hAdd (α := ℕ) (↑q : ℕ) (↑q : ℕ) = (↑n : ℕ)
h₂ : (↑r : ℕ) < HMul.hMul (α := ℕ) 2 (↑d : ℕ)
this : ∀ {r₂ : Num}, Num.ofZNum' (r.sub' (Num.pos d)) = some r₂ ↔ (↑r : ℕ) = HAdd.hAdd (α := ℕ) (↑r₂ : ℕ) (↑d : ℕ)
e : Num.ofZNum' (r.sub' (Num.pos d)) = none
h :
  LE.le (α := ℕ) (↑d : ℕ)
    (↑(match (motive := Option Num → Num × Num) none with
          | some r' => (q.bit1, r')
          | none => (q.bit0, r)).2 :
      ℕ)
⊢ False
have none : ∀ (r₂ : ℕ)
  (e' :
    (↑d : ℕ) + r₂ =
      (↑(match (motive := Option Num → Num × Num) none with
            | some r' => (q.bit1, r')
            | none => (q.bit0, r)).2 :
        ℕ)),
  False
Tactic: obtain ⟨r₂, e'⟩ := Nat.le.dest h
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (hypothesis)
Goal:
n d : PosNum
q r : Num
h₁ : (↑r : ℕ) + (↑d : ℕ) * HAdd.hAdd (α := ℕ) (↑q : ℕ) (↑q : ℕ) = (↑n : ℕ)
h₂ : (↑r : ℕ) < HMul.hMul (α := ℕ) 2 (↑d : ℕ)
this : ∀ {r₂ : Num}, Num.ofZNum' (r.sub' (Num.pos d)) = some r₂ ↔ (↑r : ℕ) = HAdd.hAdd (α := ℕ) (↑r₂ : ℕ) (↑d : ℕ)
e : Num.ofZNum' (r.sub' (Num.pos d)) = none
h :
  LE.le (α := ℕ) (↑d : ℕ)
    (↑(match (motive := Option Num → Num × Num) none with
          | some r' => (q.bit1, r')
          | none => (q.bit0, r)).2 :
      ℕ)
r₂ : ℕ
e' :
  (↑d : ℕ) + r₂ =
    (↑(match (motive := Option Num → Num × Num) none with
          | some r' => (q.bit1, r')
          | none => (q.bit0, r)).2 :
      ℕ)
⊢ False
have e'₁ : HAdd.hAdd (α := ℕ) (↑(↑r₂ : Num) : ℕ) (↑d : ℕ) =
  (↑(match (motive := Option Num → Num × Num) none with
        | some r' => (q.bit1, r')
        | none => (q.bit0, r)).2 :
    ℕ)
Tactic: rw [← Num.to_of_nat r₂, add_comm] at e'
Cleared hypotheses: e'
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (hypothesis)
Goal:
n d : PosNum
q r : Num
h₁ : (↑r : ℕ) + (↑d : ℕ) * HAdd.hAdd (α := ℕ) (↑q : ℕ) (↑q : ℕ) = (↑n : ℕ)
h₂ : (↑r : ℕ) < HMul.hMul (α := ℕ) 2 (↑d : ℕ)
this : ∀ {r₂ : Num}, Num.ofZNum' (r.sub' (Num.pos d)) = some r₂ ↔ (↑r : ℕ) = HAdd.hAdd (α := ℕ) (↑r₂ : ℕ) (↑d : ℕ)
r₂ : Num
e : Num.ofZNum' (r.sub' (Num.pos d)) = some r₂
⊢ (↑(match (motive := Option Num → Num × Num) some r₂ with
              | some r' => (q.bit1, r')
              | none => (q.bit0, r)).2 :
          ℕ) +
        HMul.hMul (α := ℕ) (↑d : ℕ)
          (↑(match (motive := Option Num → Num × Num) some r₂ with
                | some r' => (q.bit1, r')
                | none => (q.bit0, r)).1 :
            ℕ) =
      (↑n : ℕ) ∧
    LT.lt (α := ℕ)
      (↑(match (motive := Option Num → Num × Num) some r₂ with
            | some r' => (q.bit1, r')
            | none => (q.bit0, r)).2 :
        ℕ)
      (↑d : ℕ)
have this₁ : (↑r : ℕ) = HAdd.hAdd (α := ℕ) (↑r₂ : ℕ) (↑d : ℕ)
Tactic: have := this.1 e
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
n d : PosNum
q r : Num
h₁ : (↑r : ℕ) + (↑d : ℕ) * HAdd.hAdd (α := ℕ) (↑q : ℕ) (↑q : ℕ) = (↑n : ℕ)
h₂ : (↑r : ℕ) < HMul.hMul (α := ℕ) 2 (↑d : ℕ)
this_1 : ∀ {r₂ : Num}, Num.ofZNum' (r.sub' (Num.pos d)) = some r₂ ↔ (↑r : ℕ) = HAdd.hAdd (α := ℕ) (↑r₂ : ℕ) (↑d : ℕ)
r₂ : Num
e : Num.ofZNum' (r.sub' (Num.pos d)) = some r₂
this : (↑r : ℕ) = HAdd.hAdd (α := ℕ) (↑r₂ : ℕ) (↑d : ℕ)
⊢ (↑(match (motive := Option Num → Num × Num) some r₂ with
              | some r' => (q.bit1, r')
              | none => (q.bit0, r)).2 :
          ℕ) +
        HMul.hMul (α := ℕ) (↑d : ℕ)
          (↑(match (motive := Option Num → Num × Num) some r₂ with
                | some r' => (q.bit1, r')
                | none => (q.bit0, r)).1 :
            ℕ) =
      (↑n : ℕ) ∧
    LT.lt (α := ℕ)
      (↑(match (motive := Option Num → Num × Num) some r₂ with
            | some r' => (q.bit1, r')
            | none => (q.bit0, r)).2 :
        ℕ)
      (↑d : ℕ)
have some : (↑r₂ : ℕ) + (↑d : ℕ) * (HMul.hMul (α := ℕ) 2 (↑q : ℕ) + 1) = (↑n : ℕ) ∧ LT.lt (α := ℕ) (↑r₂ : ℕ) (↑d : ℕ)
Tactic: simp only [Num.cast_bit1]
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
n d : PosNum
q r : Num
h₁ : (↑r : ℕ) + (↑d : ℕ) * HAdd.hAdd (α := ℕ) (↑q : ℕ) (↑q : ℕ) = (↑n : ℕ)
h₂ : (↑r : ℕ) < HMul.hMul (α := ℕ) 2 (↑d : ℕ)
this_1 : ∀ {r₂ : Num}, Num.ofZNum' (r.sub' (Num.pos d)) = some r₂ ↔ (↑r : ℕ) = HAdd.hAdd (α := ℕ) (↑r₂ : ℕ) (↑d : ℕ)
r₂ : Num
e : Num.ofZNum' (r.sub' (Num.pos d)) = some r₂
this : (↑r : ℕ) = HAdd.hAdd (α := ℕ) (↑r₂ : ℕ) (↑d : ℕ)
⊢ (↑r₂ : ℕ) + (↑d : ℕ) * (HMul.hMul (α := ℕ) 2 (↑q : ℕ) + 1) = (↑n : ℕ) ∧ LT.lt (α := ℕ) (↑r₂ : ℕ) (↑d : ℕ)
have some : (↑r₂ : ℕ) + (↑d : ℕ) * (HMul.hMul (α := ℕ) 2 (↑q : ℕ) + 1) = (↑n : ℕ)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
n d : PosNum
q r : Num
h₁ : (↑r : ℕ) + (↑d : ℕ) * HAdd.hAdd (α := ℕ) (↑q : ℕ) (↑q : ℕ) = (↑n : ℕ)
h₂ : (↑r : ℕ) < HMul.hMul (α := ℕ) 2 (↑d : ℕ)
this_1 :
  ∀ {r₂ : Num}, Num.ofZNum' (r.sub' (Num.pos d)) = Option.some r₂ ↔ (↑r : ℕ) = HAdd.hAdd (α := ℕ) (↑r₂ : ℕ) (↑d : ℕ)
r₂ : Num
e : Num.ofZNum' (r.sub' (Num.pos d)) = Option.some r₂
this : (↑r : ℕ) = HAdd.hAdd (α := ℕ) (↑r₂ : ℕ) (↑d : ℕ)
some : (↑r₂ : ℕ) + (↑d : ℕ) * (HMul.hMul (α := ℕ) 2 (↑q : ℕ) + 1) = (↑n : ℕ)
⊢ (↑r₂ : ℕ) + (↑d : ℕ) * (HMul.hMul (α := ℕ) 2 (↑q : ℕ) + 1) = (↑n : ℕ) ∧ LT.lt (α := ℕ) (↑r₂ : ℕ) (↑d : ℕ)
have some₁ : LT.lt (α := ℕ) (↑r₂ : ℕ) (↑d : ℕ)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
n d : PosNum
q r : Num
h₁ : (↑r : ℕ) + (↑d : ℕ) * HAdd.hAdd (α := ℕ) (↑q : ℕ) (↑q : ℕ) = (↑n : ℕ)
h₂ : (↑r : ℕ) < HMul.hMul (α := ℕ) 2 (↑d : ℕ)
this_1 : ∀ {r₂ : Num}, Num.ofZNum' (r.sub' (Num.pos d)) = some r₂ ↔ (↑r : ℕ) = HAdd.hAdd (α := ℕ) (↑r₂ : ℕ) (↑d : ℕ)
r₂ : Num
e : Num.ofZNum' (r.sub' (Num.pos d)) = some r₂
this : (↑r : ℕ) = HAdd.hAdd (α := ℕ) (↑r₂ : ℕ) (↑d : ℕ)
⊢ (↑r₂ : ℕ) + (↑d : ℕ) * (HMul.hMul (α := ℕ) 2 (↑q : ℕ) + 1) = (↑n : ℕ)
have some : (↑r₂ : ℕ) + (↑d : ℕ) * (HAdd.hAdd (α := ℕ) (↑q : ℕ) (↑q : ℕ) + 1) = (↑n : ℕ)
Tactic: rwa [two_mul, add_comm _ 1, mul_add, mul_one, ← add_assoc, ← this]
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
n d : PosNum
q r : Num
h₁ : (↑r : ℕ) + (↑d : ℕ) * HAdd.hAdd (α := ℕ) (↑q : ℕ) (↑q : ℕ) = (↑n : ℕ)
h₂ : (↑r : ℕ) < HMul.hMul (α := ℕ) 2 (↑d : ℕ)
this_1 :
  ∀ {r₂ : Num}, Num.ofZNum' (r.sub' (Num.pos d)) = Option.some r₂ ↔ (↑r : ℕ) = HAdd.hAdd (α := ℕ) (↑r₂ : ℕ) (↑d : ℕ)
r₂ : Num
e : Num.ofZNum' (r.sub' (Num.pos d)) = Option.some r₂
this : (↑r : ℕ) = HAdd.hAdd (α := ℕ) (↑r₂ : ℕ) (↑d : ℕ)
some : (↑r₂ : ℕ) + (↑d : ℕ) * (HAdd.hAdd (α := ℕ) (↑q : ℕ) (↑q : ℕ) + 1) = (↑n : ℕ)
⊢ (↑r₂ : ℕ) + (↑d : ℕ) * (HMul.hMul (α := ℕ) 2 (↑q : ℕ) + 1) = (↑n : ℕ)
have some₁ : (↑r₂ : ℕ) + (↑d : ℕ) * (1 + HAdd.hAdd (α := ℕ) (↑q : ℕ) (↑q : ℕ)) = (↑n : ℕ)
Tactic: rwa [two_mul, add_comm _ 1, mul_add, mul_one, ← add_assoc, ← this]
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
n d : PosNum
q r : Num
h₁ : (↑r : ℕ) + (↑d : ℕ) * HAdd.hAdd (α := ℕ) (↑q : ℕ) (↑q : ℕ) = (↑n : ℕ)
h₂ : (↑r : ℕ) < HMul.hMul (α := ℕ) 2 (↑d : ℕ)
this_1 :
  ∀ {r₂ : Num}, Num.ofZNum' (r.sub' (Num.pos d)) = Option.some r₂ ↔ (↑r : ℕ) = HAdd.hAdd (α := ℕ) (↑r₂ : ℕ) (↑d : ℕ)
r₂ : Num
e : Num.ofZNum' (r.sub' (Num.pos d)) = Option.some r₂
this : (↑r : ℕ) = HAdd.hAdd (α := ℕ) (↑r₂ : ℕ) (↑d : ℕ)
some : (↑r₂ : ℕ) + (↑d : ℕ) * (HAdd.hAdd (α := ℕ) (↑q : ℕ) (↑q : ℕ) + 1) = (↑n : ℕ)
some₁ : (↑r₂ : ℕ) + (↑d : ℕ) * (1 + HAdd.hAdd (α := ℕ) (↑q : ℕ) (↑q : ℕ)) = (↑n : ℕ)
⊢ (↑r₂ : ℕ) + (↑d : ℕ) * (HMul.hMul (α := ℕ) 2 (↑q : ℕ) + 1) = (↑n : ℕ)
have some₂ : (↑r₂ : ℕ) + (HMul.hMul (α := ℕ) (↑d : ℕ) 1 + (↑d : ℕ) * HAdd.hAdd (α := ℕ) (↑q : ℕ) (↑q : ℕ)) = (↑n : ℕ)
Tactic: rwa [two_mul, add_comm _ 1, mul_add, mul_one, ← add_assoc, ← this]
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
n d : PosNum
q r : Num
h₁ : (↑r : ℕ) + (↑d : ℕ) * HAdd.hAdd (α := ℕ) (↑q : ℕ) (↑q : ℕ) = (↑n : ℕ)
h₂ : (↑r : ℕ) < HMul.hMul (α := ℕ) 2 (↑d : ℕ)
this_1 :
  ∀ {r₂ : Num}, Num.ofZNum' (r.sub' (Num.pos d)) = Option.some r₂ ↔ (↑r : ℕ) = HAdd.hAdd (α := ℕ) (↑r₂ : ℕ) (↑d : ℕ)
r₂ : Num
e : Num.ofZNum' (r.sub' (Num.pos d)) = Option.some r₂
this : (↑r : ℕ) = HAdd.hAdd (α := ℕ) (↑r₂ : ℕ) (↑d : ℕ)
some : (↑r₂ : ℕ) + (↑d : ℕ) * (HAdd.hAdd (α := ℕ) (↑q : ℕ) (↑q : ℕ) + 1) = (↑n : ℕ)
some₁ : (↑r₂ : ℕ) + (↑d : ℕ) * (1 + HAdd.hAdd (α := ℕ) (↑q : ℕ) (↑q : ℕ)) = (↑n : ℕ)
some₂ : (↑r₂ : ℕ) + (HMul.hMul (α := ℕ) (↑d : ℕ) 1 + (↑d : ℕ) * HAdd.hAdd (α := ℕ) (↑q : ℕ) (↑q : ℕ)) = (↑n : ℕ)
⊢ (↑r₂ : ℕ) + (↑d : ℕ) * (HMul.hMul (α := ℕ) 2 (↑q : ℕ) + 1) = (↑n : ℕ)
have some₃ : (↑r₂ : ℕ) + ((↑d : ℕ) + (↑d : ℕ) * HAdd.hAdd (α := ℕ) (↑q : ℕ) (↑q : ℕ)) = (↑n : ℕ)
Tactic: rwa [two_mul, add_comm _ 1, mul_add, mul_one, ← add_assoc, ← this]
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
n d : PosNum
q r : Num
h₁ : (↑r : ℕ) + (↑d : ℕ) * HAdd.hAdd (α := ℕ) (↑q : ℕ) (↑q : ℕ) = (↑n : ℕ)
h₂ : (↑r : ℕ) < HMul.hMul (α := ℕ) 2 (↑d : ℕ)
this_1 :
  ∀ {r₂ : Num}, Num.ofZNum' (r.sub' (Num.pos d)) = Option.some r₂ ↔ (↑r : ℕ) = HAdd.hAdd (α := ℕ) (↑r₂ : ℕ) (↑d : ℕ)
r₂ : Num
e : Num.ofZNum' (r.sub' (Num.pos d)) = Option.some r₂
this : (↑r : ℕ) = HAdd.hAdd (α := ℕ) (↑r₂ : ℕ) (↑d : ℕ)
some : (↑r₂ : ℕ) + (↑d : ℕ) * (HAdd.hAdd (α := ℕ) (↑q : ℕ) (↑q : ℕ) + 1) = (↑n : ℕ)
some₁ : (↑r₂ : ℕ) + (↑d : ℕ) * (1 + HAdd.hAdd (α := ℕ) (↑q : ℕ) (↑q : ℕ)) = (↑n : ℕ)
some₂ : (↑r₂ : ℕ) + (HMul.hMul (α := ℕ) (↑d : ℕ) 1 + (↑d : ℕ) * HAdd.hAdd (α := ℕ) (↑q : ℕ) (↑q : ℕ)) = (↑n : ℕ)
some₃ : (↑r₂ : ℕ) + ((↑d : ℕ) + (↑d : ℕ) * HAdd.hAdd (α := ℕ) (↑q : ℕ) (↑q : ℕ)) = (↑n : ℕ)
⊢ (↑r₂ : ℕ) + (↑d : ℕ) * (HMul.hMul (α := ℕ) 2 (↑q : ℕ) + 1) = (↑n : ℕ)
have some₄ : HAdd.hAdd (α := ℕ) (↑r₂ : ℕ) (↑d : ℕ) + (↑d : ℕ) * HAdd.hAdd (α := ℕ) (↑q : ℕ) (↑q : ℕ) = (↑n : ℕ)
Tactic: rwa [two_mul, add_comm _ 1, mul_add, mul_one, ← add_assoc, ← this]
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
n d : PosNum
q r : Num
h₁ : (↑r : ℕ) + (↑d : ℕ) * HAdd.hAdd (α := ℕ) (↑q : ℕ) (↑q : ℕ) = (↑n : ℕ)
h₂ : (↑r : ℕ) < HMul.hMul (α := ℕ) 2 (↑d : ℕ)
this_1 : ∀ {r₂ : Num}, Num.ofZNum' (r.sub' (Num.pos d)) = some r₂ ↔ (↑r : ℕ) = HAdd.hAdd (α := ℕ) (↑r₂ : ℕ) (↑d : ℕ)
r₂ : Num
e : Num.ofZNum' (r.sub' (Num.pos d)) = some r₂
this : (↑r : ℕ) = HAdd.hAdd (α := ℕ) (↑r₂ : ℕ) (↑d : ℕ)
⊢ LT.lt (α := ℕ) (↑r₂ : ℕ) (↑d : ℕ)
have some : ∀ (h₂ : HAdd.hAdd (α := ℕ) (↑r₂ : ℕ) (↑d : ℕ) < HMul.hMul (α := ℕ) 2 (↑d : ℕ))
  (e : Num.ofZNum' (r.sub' (Num.pos d)) = some r₂) (this : (↑r : ℕ) = HAdd.hAdd (α := ℕ) (↑r₂ : ℕ) (↑d : ℕ)),
  LT.lt (α := ℕ) (↑r₂ : ℕ) (↑d : ℕ)
Tactic: rwa [this, two_mul, add_lt_add_iff_right] at h₂
Cleared hypotheses: h₂, e, this
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
n d : PosNum
q r : Num
h₁ : (↑r : ℕ) + (↑d : ℕ) * HAdd.hAdd (α := ℕ) (↑q : ℕ) (↑q : ℕ) = (↑n : ℕ)
h₂ : (↑r : ℕ) < HMul.hMul (α := ℕ) 2 (↑d : ℕ)
this_1 :
  ∀ {r₂ : Num}, Num.ofZNum' (r.sub' (Num.pos d)) = Option.some r₂ ↔ (↑r : ℕ) = HAdd.hAdd (α := ℕ) (↑r₂ : ℕ) (↑d : ℕ)
r₂ : Num
e : Num.ofZNum' (r.sub' (Num.pos d)) = Option.some r₂
this : (↑r : ℕ) = HAdd.hAdd (α := ℕ) (↑r₂ : ℕ) (↑d : ℕ)
some :
  ∀ (h₂ : HAdd.hAdd (α := ℕ) (↑r₂ : ℕ) (↑d : ℕ) < HMul.hMul (α := ℕ) 2 (↑d : ℕ))
    (e : Num.ofZNum' (r.sub' (Num.pos d)) = Option.some r₂) (this : (↑r : ℕ) = HAdd.hAdd (α := ℕ) (↑r₂ : ℕ) (↑d : ℕ)),
    LT.lt (α := ℕ) (↑r₂ : ℕ) (↑d : ℕ)
⊢ LT.lt (α := ℕ) (↑r₂ : ℕ) (↑d : ℕ)
have some₁ : ∀ (h₂ : HAdd.hAdd (α := ℕ) (↑r₂ : ℕ) (↑d : ℕ) < HAdd.hAdd (α := ℕ) (↑d : ℕ) (↑d : ℕ))
  (e : Num.ofZNum' (r.sub' (Num.pos d)) = Option.some r₂) (this : (↑r : ℕ) = HAdd.hAdd (α := ℕ) (↑r₂ : ℕ) (↑d : ℕ)),
  LT.lt (α := ℕ) (↑r₂ : ℕ) (↑d : ℕ)
Tactic: rwa [this, two_mul, add_lt_add_iff_right] at h₂
Cleared hypotheses: h₂, e, this
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
n d : PosNum
q r : Num
h₁ : (↑r : ℕ) + (↑d : ℕ) * HAdd.hAdd (α := ℕ) (↑q : ℕ) (↑q : ℕ) = (↑n : ℕ)
h₂ : (↑r : ℕ) < HMul.hMul (α := ℕ) 2 (↑d : ℕ)
this_1 :
  ∀ {r₂ : Num}, Num.ofZNum' (r.sub' (Num.pos d)) = Option.some r₂ ↔ (↑r : ℕ) = HAdd.hAdd (α := ℕ) (↑r₂ : ℕ) (↑d : ℕ)
r₂ : Num
e : Num.ofZNum' (r.sub' (Num.pos d)) = Option.some r₂
this : (↑r : ℕ) = HAdd.hAdd (α := ℕ) (↑r₂ : ℕ) (↑d : ℕ)
some :
  ∀ (h₂ : HAdd.hAdd (α := ℕ) (↑r₂ : ℕ) (↑d : ℕ) < HMul.hMul (α := ℕ) 2 (↑d : ℕ))
    (e : Num.ofZNum' (r.sub' (Num.pos d)) = Option.some r₂) (this : (↑r : ℕ) = HAdd.hAdd (α := ℕ) (↑r₂ : ℕ) (↑d : ℕ)),
    LT.lt (α := ℕ) (↑r₂ : ℕ) (↑d : ℕ)
some₁ :
  ∀ (h₂ : HAdd.hAdd (α := ℕ) (↑r₂ : ℕ) (↑d : ℕ) < HAdd.hAdd (α := ℕ) (↑d : ℕ) (↑d : ℕ))
    (e : Num.ofZNum' (r.sub' (Num.pos d)) = Option.some r₂) (this : (↑r : ℕ) = HAdd.hAdd (α := ℕ) (↑r₂ : ℕ) (↑d : ℕ)),
    LT.lt (α := ℕ) (↑r₂ : ℕ) (↑d : ℕ)
⊢ LT.lt (α := ℕ) (↑r₂ : ℕ) (↑d : ℕ)
have some₂ : ∀ (h₂ : LT.lt (α := ℕ) (↑r₂ : ℕ) (↑d : ℕ)) (e : Num.ofZNum' (r.sub' (Num.pos d)) = Option.some r₂)
  (this : (↑r : ℕ) = HAdd.hAdd (α := ℕ) (↑r₂ : ℕ) (↑d : ℕ)), LT.lt (α := ℕ) (↑r₂ : ℕ) (↑d : ℕ)
Tactic: rwa [this, two_mul, add_lt_add_iff_right] at h₂
Cleared hypotheses: h₂, e, this
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
d n : PosNum
⊢ HDiv.hDiv (α := ℕ) (↑n : ℕ) (↑d : ℕ) = (↑(d.divMod n).1 : ℕ) ∧
    HMod.hMod (α := ℕ) (↑n : ℕ) (↑d : ℕ) = (↑(d.divMod n).2 : ℕ)
have rw : (↑(d.divMod n).2 : ℕ) + HMul.hMul (α := ℕ) (↑d : ℕ) (↑(d.divMod n).1 : ℕ) = (↑n : ℕ) ∧
  LT.lt (α := ℕ) (↑(d.divMod n).2 : ℕ) (↑d : ℕ)
Tactic: rw [Nat.div_mod_unique (PosNum.cast_pos _)]
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
d n : PosNum
IH :
  (↑(d.divMod n).2 : ℕ) + HMul.hMul (α := ℕ) (↑d : ℕ) (↑(d.divMod n).1 : ℕ) = (↑n : ℕ) ∧
    LT.lt (α := ℕ) (↑(d.divMod n).2 : ℕ) (↑d : ℕ)
⊢ (↑(d.divMod n.bit1).2 : ℕ) + HMul.hMul (α := ℕ) (↑d : ℕ) (↑(d.divMod n.bit1).1 : ℕ) = (↑n.bit1 : ℕ) ∧
    LT.lt (α := ℕ) (↑(d.divMod n.bit1).2 : ℕ) (↑d : ℕ)
have bit1 : (↑(match (motive := Num × Num → Num × Num) d.divMod n with
            | (q, r₁) => d.divModAux q r₁.bit1).2 :
        ℕ) +
      HMul.hMul (α := ℕ) (↑d : ℕ)
        (↑(match (motive := Num × Num → Num × Num) d.divMod n with
              | (q, r₁) => d.divModAux q r₁.bit1).1 :
          ℕ) =
    (↑n.bit1 : ℕ) ∧
  LT.lt (α := ℕ)
    (↑(match (motive := Num × Num → Num × Num) d.divMod n with
          | (q, r₁) => d.divModAux q r₁.bit1).2 :
      ℕ)
    (↑d : ℕ)
Tactic: unfold divMod
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
d n : PosNum
IH :
  (↑(d.divMod n).2 : ℕ) + HMul.hMul (α := ℕ) (↑d : ℕ) (↑(d.divMod n).1 : ℕ) = (↑n : ℕ) ∧
    LT.lt (α := ℕ) (↑(d.divMod n).2 : ℕ) (↑d : ℕ)
⊢ (↑(match (motive := Num × Num → Num × Num) d.divMod n with
              | (q, r₁) => d.divModAux q r₁.bit1).2 :
          ℕ) +
        HMul.hMul (α := ℕ) (↑d : ℕ)
          (↑(match (motive := Num × Num → Num × Num) d.divMod n with
                | (q, r₁) => d.divModAux q r₁.bit1).1 :
            ℕ) =
      (↑n.bit1 : ℕ) ∧
    LT.lt (α := ℕ)
      (↑(match (motive := Num × Num → Num × Num) d.divMod n with
            | (q, r₁) => d.divModAux q r₁.bit1).2 :
        ℕ)
      (↑d : ℕ)
have bit1 : ∀
  (IH :
    (↑(d.divMod n).2 : ℕ) + HMul.hMul (α := ℕ) (↑d : ℕ) (↑(d.divMod n).1 : ℕ) = (↑n : ℕ) ∧
      LT.lt (α := ℕ) (↑(d.divMod n).2 : ℕ) (↑d : ℕ)),
  (↑(match (motive := Num × Num → Num × Num) d.divMod n with
              | (q, r₁) => d.divModAux q r₁.bit1).2 :
          ℕ) +
        HMul.hMul (α := ℕ) (↑d : ℕ)
          (↑(match (motive := Num × Num → Num × Num) d.divMod n with
                | (q, r₁) => d.divModAux q r₁.bit1).1 :
            ℕ) =
      (↑n.bit1 : ℕ) ∧
    LT.lt (α := ℕ)
      (↑(match (motive := Num × Num → Num × Num) d.divMod n with
            | (q, r₁) => d.divModAux q r₁.bit1).2 :
        ℕ)
      (↑d : ℕ)
Tactic: revert IH
Cleared hypotheses: IH
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
d n : PosNum
⊢ ∀
    (IH :
      (↑(d.divMod n).2 : ℕ) + HMul.hMul (α := ℕ) (↑d : ℕ) (↑(d.divMod n).1 : ℕ) = (↑n : ℕ) ∧
        LT.lt (α := ℕ) (↑(d.divMod n).2 : ℕ) (↑d : ℕ)),
    (↑(match (motive := Num × Num → Num × Num) d.divMod n with
                | (q, r₁) => d.divModAux q r₁.bit1).2 :
            ℕ) +
          HMul.hMul (α := ℕ) (↑d : ℕ)
            (↑(match (motive := Num × Num → Num × Num) d.divMod n with
                  | (q, r₁) => d.divModAux q r₁.bit1).1 :
              ℕ) =
        (↑n.bit1 : ℕ) ∧
      LT.lt (α := ℕ)
        (↑(match (motive := Num × Num → Num × Num) d.divMod n with
              | (q, r₁) => d.divModAux q r₁.bit1).2 :
          ℕ)
        (↑d : ℕ)
have bit1 : ∀ (q r : Num)
  (IH :
    (↑(q, r).2 : ℕ) + HMul.hMul (α := ℕ) (↑d : ℕ) (↑(q, r).1 : ℕ) = (↑n : ℕ) ∧ LT.lt (α := ℕ) (↑(q, r).2 : ℕ) (↑d : ℕ)),
  (↑(match (motive := Num × Num → Num × Num) (q, r) with
              | (q, r₁) => d.divModAux q r₁.bit1).2 :
          ℕ) +
        HMul.hMul (α := ℕ) (↑d : ℕ)
          (↑(match (motive := Num × Num → Num × Num) (q, r) with
                | (q, r₁) => d.divModAux q r₁.bit1).1 :
            ℕ) =
      (↑n.bit1 : ℕ) ∧
    LT.lt (α := ℕ)
      (↑(match (motive := Num × Num → Num × Num) (q, r) with
            | (q, r₁) => d.divModAux q r₁.bit1).2 :
        ℕ)
      (↑d : ℕ)
Tactic: obtain ⟨q, r⟩ := divMod d n
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
d n : PosNum
q r : Num
IH : (↑r : ℕ) + HMul.hMul (α := ℕ) (↑d : ℕ) (↑q : ℕ) = (↑n : ℕ) ∧ LT.lt (α := ℕ) (↑r : ℕ) (↑d : ℕ)
⊢ (↑(d.divModAux q r.bit1).2 : ℕ) + HMul.hMul (α := ℕ) (↑d : ℕ) (↑(d.divModAux q r.bit1).1 : ℕ) = (↑n.bit1 : ℕ) ∧
    LT.lt (α := ℕ) (↑(d.divModAux q r.bit1).2 : ℕ) (↑d : ℕ)
have bit1 : (↑r.bit1 : ℕ) + (↑d : ℕ) * HAdd.hAdd (α := ℕ) (↑q : ℕ) (↑q : ℕ) = (↑n.bit1 : ℕ)
Tactic: apply divMod_to_nat_aux
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
d n : PosNum
q r : Num
IH : (↑r : ℕ) + HMul.hMul (α := ℕ) (↑d : ℕ) (↑q : ℕ) = (↑n : ℕ) ∧ LT.lt (α := ℕ) (↑r : ℕ) (↑d : ℕ)
bit1 : (↑r.bit1 : ℕ) + (↑d : ℕ) * HAdd.hAdd (α := ℕ) (↑q : ℕ) (↑q : ℕ) = (↑n.bit1 : ℕ)
⊢ (↑(d.divModAux q r.bit1).2 : ℕ) + HMul.hMul (α := ℕ) (↑d : ℕ) (↑(d.divModAux q r.bit1).1 : ℕ) = (↑n.bit1 : ℕ) ∧
    LT.lt (α := ℕ) (↑(d.divModAux q r.bit1).2 : ℕ) (↑d : ℕ)
have bit1₁ : (↑r.bit1 : ℕ) < HMul.hMul (α := ℕ) 2 (↑d : ℕ)
Tactic: apply divMod_to_nat_aux
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
d n : PosNum
q r : Num
IH : (↑r : ℕ) + HMul.hMul (α := ℕ) (↑d : ℕ) (↑q : ℕ) = (↑n : ℕ) ∧ LT.lt (α := ℕ) (↑r : ℕ) (↑d : ℕ)
⊢ (↑r.bit1 : ℕ) + (↑d : ℕ) * HAdd.hAdd (α := ℕ) (↑q : ℕ) (↑q : ℕ) = (↑n.bit1 : ℕ)
have bit1 : HMul.hMul (α := ℕ) 2 (↑r : ℕ) + 1 + (↑d : ℕ) * HAdd.hAdd (α := ℕ) (↑q : ℕ) (↑q : ℕ) =
  HAdd.hAdd (α := ℕ) (↑n : ℕ) (↑n : ℕ) + 1
Tactic: simp only [Num.cast_bit1, cast_bit1]
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
d n : PosNum
q r : Num
IH : (↑r : ℕ) + HMul.hMul (α := ℕ) (↑d : ℕ) (↑q : ℕ) = (↑n : ℕ) ∧ LT.lt (α := ℕ) (↑r : ℕ) (↑d : ℕ)
⊢ (↑r.bit1 : ℕ) < HMul.hMul (α := ℕ) 2 (↑d : ℕ)
have bit1 : HMul.hMul (α := ℕ) 2 (↑r : ℕ) + 1 < HMul.hMul (α := ℕ) 2 (↑d : ℕ)
Tactic: simp only [Num.cast_bit1, cast_bit1]
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
d n : PosNum
q r : Num
IH : (↑r : ℕ) + HMul.hMul (α := ℕ) (↑d : ℕ) (↑q : ℕ) = (↑n : ℕ) ∧ LT.lt (α := ℕ) (↑r : ℕ) (↑d : ℕ)
⊢ HMul.hMul (α := ℕ) 2 (↑r : ℕ) + 1 + (↑d : ℕ) * HAdd.hAdd (α := ℕ) (↑q : ℕ) (↑q : ℕ) =
    HAdd.hAdd (α := ℕ) (↑n : ℕ) (↑n : ℕ) + 1
have bit1 : HMul.hMul (α := ℕ) 2 (↑r : ℕ) + 1 + (↑d : ℕ) * HMul.hMul (α := ℕ) 2 (↑q : ℕ) = HAdd.hAdd (α := ℕ) (↑n : ℕ) (↑n : ℕ) + 1
Tactic: rw [← two_mul, ← two_mul, add_right_comm, mul_left_comm, ← mul_add, IH.1]
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
d n : PosNum
q r : Num
IH : (↑r : ℕ) + HMul.hMul (α := ℕ) (↑d : ℕ) (↑q : ℕ) = (↑n : ℕ) ∧ LT.lt (α := ℕ) (↑r : ℕ) (↑d : ℕ)
bit1 :
  HMul.hMul (α := ℕ) 2 (↑r : ℕ) + 1 + (↑d : ℕ) * HMul.hMul (α := ℕ) 2 (↑q : ℕ) =
    HAdd.hAdd (α := ℕ) (↑n : ℕ) (↑n : ℕ) + 1
⊢ HMul.hMul (α := ℕ) 2 (↑r : ℕ) + 1 + (↑d : ℕ) * HAdd.hAdd (α := ℕ) (↑q : ℕ) (↑q : ℕ) =
    HAdd.hAdd (α := ℕ) (↑n : ℕ) (↑n : ℕ) + 1
have bit1₁ : HMul.hMul (α := ℕ) 2 (↑r : ℕ) + 1 + (↑d : ℕ) * HMul.hMul (α := ℕ) 2 (↑q : ℕ) = HMul.hMul (α := ℕ) 2 (↑n : ℕ) + 1
Tactic: rw [← two_mul, ← two_mul, add_right_comm, mul_left_comm, ← mul_add, IH.1]
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
d n : PosNum
q r : Num
IH : (↑r : ℕ) + HMul.hMul (α := ℕ) (↑d : ℕ) (↑q : ℕ) = (↑n : ℕ) ∧ LT.lt (α := ℕ) (↑r : ℕ) (↑d : ℕ)
bit1 :
  HMul.hMul (α := ℕ) 2 (↑r : ℕ) + 1 + (↑d : ℕ) * HMul.hMul (α := ℕ) 2 (↑q : ℕ) =
    HAdd.hAdd (α := ℕ) (↑n : ℕ) (↑n : ℕ) + 1
bit1₁ : HMul.hMul (α := ℕ) 2 (↑r : ℕ) + 1 + (↑d : ℕ) * HMul.hMul (α := ℕ) 2 (↑q : ℕ) = HMul.hMul (α := ℕ) 2 (↑n : ℕ) + 1
⊢ HMul.hMul (α := ℕ) 2 (↑r : ℕ) + 1 + (↑d : ℕ) * HAdd.hAdd (α := ℕ) (↑q : ℕ) (↑q : ℕ) =
    HAdd.hAdd (α := ℕ) (↑n : ℕ) (↑n : ℕ) + 1
have bit1₂ : HMul.hMul (α := ℕ) 2 (↑r : ℕ) + (↑d : ℕ) * HMul.hMul (α := ℕ) 2 (↑q : ℕ) + 1 = HMul.hMul (α := ℕ) 2 (↑n : ℕ) + 1
Tactic: rw [← two_mul, ← two_mul, add_right_comm, mul_left_comm, ← mul_add, IH.1]
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
d n : PosNum
q r : Num
IH : (↑r : ℕ) + HMul.hMul (α := ℕ) (↑d : ℕ) (↑q : ℕ) = (↑n : ℕ) ∧ LT.lt (α := ℕ) (↑r : ℕ) (↑d : ℕ)
bit1 :
  HMul.hMul (α := ℕ) 2 (↑r : ℕ) + 1 + (↑d : ℕ) * HMul.hMul (α := ℕ) 2 (↑q : ℕ) =
    HAdd.hAdd (α := ℕ) (↑n : ℕ) (↑n : ℕ) + 1
bit1₁ : HMul.hMul (α := ℕ) 2 (↑r : ℕ) + 1 + (↑d : ℕ) * HMul.hMul (α := ℕ) 2 (↑q : ℕ) = HMul.hMul (α := ℕ) 2 (↑n : ℕ) + 1
bit1₂ : HMul.hMul (α := ℕ) 2 (↑r : ℕ) + (↑d : ℕ) * HMul.hMul (α := ℕ) 2 (↑q : ℕ) + 1 = HMul.hMul (α := ℕ) 2 (↑n : ℕ) + 1
⊢ HMul.hMul (α := ℕ) 2 (↑r : ℕ) + 1 + (↑d : ℕ) * HAdd.hAdd (α := ℕ) (↑q : ℕ) (↑q : ℕ) =
    HAdd.hAdd (α := ℕ) (↑n : ℕ) (↑n : ℕ) + 1
have bit1₃ : HMul.hMul (α := ℕ) 2 (↑r : ℕ) + 2 * HMul.hMul (α := ℕ) (↑d : ℕ) (↑q : ℕ) + 1 = HMul.hMul (α := ℕ) 2 (↑n : ℕ) + 1
Tactic: rw [← two_mul, ← two_mul, add_right_comm, mul_left_comm, ← mul_add, IH.1]
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
d n : PosNum
q r : Num
IH : (↑r : ℕ) + HMul.hMul (α := ℕ) (↑d : ℕ) (↑q : ℕ) = (↑n : ℕ) ∧ LT.lt (α := ℕ) (↑r : ℕ) (↑d : ℕ)
bit1 :
  HMul.hMul (α := ℕ) 2 (↑r : ℕ) + 1 + (↑d : ℕ) * HMul.hMul (α := ℕ) 2 (↑q : ℕ) =
    HAdd.hAdd (α := ℕ) (↑n : ℕ) (↑n : ℕ) + 1
bit1₁ : HMul.hMul (α := ℕ) 2 (↑r : ℕ) + 1 + (↑d : ℕ) * HMul.hMul (α := ℕ) 2 (↑q : ℕ) = HMul.hMul (α := ℕ) 2 (↑n : ℕ) + 1
bit1₂ : HMul.hMul (α := ℕ) 2 (↑r : ℕ) + (↑d : ℕ) * HMul.hMul (α := ℕ) 2 (↑q : ℕ) + 1 = HMul.hMul (α := ℕ) 2 (↑n : ℕ) + 1
bit1₃ : HMul.hMul (α := ℕ) 2 (↑r : ℕ) + 2 * HMul.hMul (α := ℕ) (↑d : ℕ) (↑q : ℕ) + 1 = HMul.hMul (α := ℕ) 2 (↑n : ℕ) + 1
⊢ HMul.hMul (α := ℕ) 2 (↑r : ℕ) + 1 + (↑d : ℕ) * HAdd.hAdd (α := ℕ) (↑q : ℕ) (↑q : ℕ) =
    HAdd.hAdd (α := ℕ) (↑n : ℕ) (↑n : ℕ) + 1
have bit1₄ : 2 * ((↑r : ℕ) + HMul.hMul (α := ℕ) (↑d : ℕ) (↑q : ℕ)) + 1 = HMul.hMul (α := ℕ) 2 (↑n : ℕ) + 1
Tactic: rw [← two_mul, ← two_mul, add_right_comm, mul_left_comm, ← mul_add, IH.1]