awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Num.ZNum
Goal:
n : ℤ
simp : ∀ (k : ℤ), k ≤ 0 → (↑(↑k : ZNum) : ℤ) = k → HSub.hSub (α := ℤ) (↑(↑k : ZNum) : ℤ) (↑1 : ℤ) = k - 1
⊢ ∀ (k : ℤ), k ≤ 0 → (↑(↑k : ZNum) : ℤ) = k → (↑(↑(k - 1) : ZNum) : ℤ) = k - 1

Tactic:
simp
-- Module: Mathlib.Data.Num.ZNum
Goal:
n : ℕ
rw : Num.toZNumNeg (↑n : Num) = -Num.toZNum (↑n : Num)
rw₁ rw₂ : Num.toZNumNeg (↑n : Num) = Num.toZNumNeg (↑n : Num)
⊢ Num.toZNumNeg (↑n : Num) = -(↑n : ZNum)

Tactic:
rw [← of_nat_toZNum, Num.zneg_toZNum]

Premises used: Num.zneg_toZNum, ZNum.of_nat_toZNum
-- Module: Mathlib.Data.Num.ZNum
Goal:
α : Type u_1
inst : AddGroupWithOne α
n : ℤ
rw : Eq.{u_1 + 1} (α := α) (↑(↑(↑n : ZNum) : ℤ) : α) (↑n : α)
rw₁ rw₂ : Eq.{u_1 + 1} (α := α) (↑n : α) (↑n : α)
⊢ Eq.{u_1 + 1} (α := α) (↑(↑n : ZNum) : α) (↑n : α)

Tactic:
rw [← cast_to_int, to_of_int]

Premises used: ZNum.to_of_int, ZNum.cast_to_int
-- Module: Mathlib.Data.Num.ZNum
Goal:
α : Type u_1
inst : AddGroupWithOne α
n : ℕ
rw : Eq.{u_1 + 1} (α := α) (↑(↑n : ZNum) : α) (↑(↑n : ℤ) : α)
⊢ Eq.{u_1 + 1} (α := α) (↑(↑n : ZNum) : α) (↑n : α)

Tactic:
rw [← Int.cast_natCast, of_intCast, Int.cast_natCast]

Premises used: Int.cast_natCast, ZNum.of_intCast
-- Module: Mathlib.Data.Num.ZNum
Goal:
m n : ZNum
h : Dvd.dvd (α := ℤ) (↑m : ℤ) (↑n : ℤ)
k : ℤ
e : (↑n : ℤ) = (↑m : ℤ) * k
rw : (↑((↑m : ℤ) * k) : ZNum) = m * (↑k : ZNum)
⊢ n = m * (↑k : ZNum)

Tactic:
rw [← of_to_int n, e]

Premises used: ZNum.of_to_int
-- Module: Mathlib.Data.Num.ZNum
Goal:
m n : ZNum
h : Dvd.dvd (α := ℤ) (↑m : ℤ) (↑n : ℤ)
k : ℤ
e : (↑n : ℤ) = (↑m : ℤ) * k
⊢ (↑((↑m : ℤ) * k) : ZNum) = m * (↑k : ZNum)

Tactic:
simp
-- Module: Mathlib.Data.Num.ZNum
Goal:
m n : ZNum
h : m ∣ n
k : ZNum
e : n = m * k
simp : (↑(m * k) : ℤ) = HMul.hMul (α := ℤ) (↑m : ℤ) (↑k : ℤ)
⊢ (↑n : ℤ) = HMul.hMul (α := ℤ) (↑m : ℤ) (↑k : ℤ)

Tactic:
simp [e]
-- Module: Mathlib.Data.Num.ZNum
Goal:
n d : PosNum
q r : Num
h₁ : (↑r : ℕ) + (↑d : ℕ) * HAdd.hAdd (α := ℕ) (↑q : ℕ) (↑q : ℕ) = (↑n : ℕ)
h₂ : (↑r : ℕ) < HMul.hMul (α := ℕ) 2 (↑d : ℕ)
unfold :
  (↑(match (motive := Option Num → Num × Num) Num.ofZNum' (r.sub' (Num.pos d)) with
              | some r' => (q.bit1, r')
              | none => (q.bit0, r)).2 :
          ℕ) +
        HMul.hMul (α := ℕ) (↑d : ℕ)
          (↑(match (motive := Option Num → Num × Num) Num.ofZNum' (r.sub' (Num.pos d)) with
                | some r' => (q.bit1, r')
                | none => (q.bit0, r)).1 :
            ℕ) =
      (↑n : ℕ) ∧
    LT.lt (α := ℕ)
      (↑(match (motive := Option Num → Num × Num) Num.ofZNum' (r.sub' (Num.pos d)) with
            | some r' => (q.bit1, r')
            | none => (q.bit0, r)).2 :
        ℕ)
      (↑d : ℕ)
⊢ (↑(d.divModAux q r).2 : ℕ) + HMul.hMul (α := ℕ) (↑d : ℕ) (↑(d.divModAux q r).1 : ℕ) = (↑n : ℕ) ∧
    LT.lt (α := ℕ) (↑(d.divModAux q r).2 : ℕ) (↑d : ℕ)

Tactic:
unfold divModAux

Premises used: PosNum.divModAux
-- Module: Mathlib.Data.Num.ZNum
Goal:
n d : PosNum
q r : Num
h₁ : (↑r : ℕ) + (↑d : ℕ) * HAdd.hAdd (α := ℕ) (↑q : ℕ) (↑q : ℕ) = (↑n : ℕ)
h₂ : (↑r : ℕ) < HMul.hMul (α := ℕ) 2 (↑d : ℕ)
r₂ : Num
apply : r.sub' (Num.pos d) = r₂.toZNum ↔ (↑r : ℕ) = HAdd.hAdd (α := ℕ) (↑r₂ : ℕ) (↑d : ℕ)
⊢ Num.ofZNum' (r.sub' (Num.pos d)) = some r₂ ↔ (↑r : ℕ) = HAdd.hAdd (α := ℕ) (↑r₂ : ℕ) (↑d : ℕ)

Tactic:
apply Num.mem_ofZNum'.trans

Premises used: Iff.trans, Num.mem_ofZNum'
-- Module: Mathlib.Data.Num.ZNum
Goal:
n d : PosNum
q r : Num
h₁ : (↑r : ℕ) + (↑d : ℕ) * HAdd.hAdd (α := ℕ) (↑q : ℕ) (↑q : ℕ) = (↑n : ℕ)
h₂ : (↑r : ℕ) < HMul.hMul (α := ℕ) 2 (↑d : ℕ)
r₂ : Num
rw :
  (↑r : ℤ) = HAdd.hAdd (α := ℤ) (↑r₂ : ℤ) (↑(Num.pos d) : ℤ) ↔
    Eq (α := ℤ) (↑(↑r : ℕ) : ℤ) (↑(HAdd.hAdd (α := ℕ) (↑r₂ : ℕ) (↑d : ℕ)) : ℤ)
⊢ r.sub' (Num.pos d) = r₂.toZNum ↔ (↑r : ℕ) = HAdd.hAdd (α := ℕ) (↑r₂ : ℕ) (↑d : ℕ)

Tactic:
rw [← ZNum.to_int_inj, Num.cast_toZNum, Num.cast_sub', sub_eq_iff_eq_add, ← Int.natCast_inj]

Premises used: Num.cast_sub', sub_eq_iff_eq_add, ZNum.to_int_inj, Num.cast_toZNum, Int.natCast_inj
-- Module: Mathlib.Data.Num.ZNum
Goal:
n d : PosNum
q r : Num
h₁ : (↑r : ℕ) + (↑d : ℕ) * HAdd.hAdd (α := ℕ) (↑q : ℕ) (↑q : ℕ) = (↑n : ℕ)
h₂ : (↑r : ℕ) < HMul.hMul (α := ℕ) 2 (↑d : ℕ)
r₂ : Num
⊢ (↑r : ℤ) = HAdd.hAdd (α := ℤ) (↑r₂ : ℤ) (↑(Num.pos d) : ℤ) ↔
    Eq (α := ℤ) (↑(↑r : ℕ) : ℤ) (↑(HAdd.hAdd (α := ℕ) (↑r₂ : ℕ) (↑d : ℕ)) : ℤ)

Tactic:
simp
-- Module: Mathlib.Data.Num.ZNum
Goal:
n d : PosNum
q r : Num
h₁ : (↑r : ℕ) + (↑d : ℕ) * HAdd.hAdd (α := ℕ) (↑q : ℕ) (↑q : ℕ) = (↑n : ℕ)
h₂ : (↑r : ℕ) < HMul.hMul (α := ℕ) 2 (↑d : ℕ)
⊢ ∀ {r₂ : Num}, Num.ofZNum' (r.sub' (Num.pos d)) = some r₂ ↔ (↑r : ℕ) = HAdd.hAdd (α := ℕ) (↑r₂ : ℕ) (↑d : ℕ)

Tactic:
have : ∀ {r₂}, Num.ofZNum' (Num.sub' r (Num.pos d)) = some r₂ ↔ (r : ℕ) = r₂ + d := by
    intro r₂
    apply Num.mem_ofZNum'.trans
    rw [← ZNum.to_int_inj, Num.cast_toZNum, Num.cast_sub', sub_eq_iff_eq_add, ← Int.natCast_inj]
    simp
-- Module: Mathlib.Data.Num.ZNum
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)) = Option.some r₂ ↔ (↑r : ℕ) = HAdd.hAdd (α := ℕ) (↑r₂ : ℕ) (↑d : ℕ)
none :
  ∀ (e : Num.ofZNum' (r.sub' (Num.pos d)) = Option.none),
    (↑(match (motive := Option Num → Num × Num) Option.none with
                | Option.some r' => (q.bit1, r')
                | Option.none => (q.bit0, r)).2 :
            ℕ) +
          HMul.hMul (α := ℕ) (↑d : ℕ)
            (↑(match (motive := Option Num → Num × Num) Option.none with
                  | Option.some r' => (q.bit1, r')
                  | Option.none => (q.bit0, r)).1 :
              ℕ) =
        (↑n : ℕ) ∧
      LT.lt (α := ℕ)
        (↑(match (motive := Option Num → Num × Num) Option.none with
              | Option.some r' => (q.bit1, r')
              | Option.none => (q.bit0, r)).2 :
          ℕ)
        (↑d : ℕ)
some :
  ∀ (r₂ : Num) (e : Num.ofZNum' (r.sub' (Num.pos d)) = Option.some r₂),
    (↑(match (motive := Option Num → Num × Num) Option.some r₂ with
                | Option.some r' => (q.bit1, r')
                | Option.none => (q.bit0, r)).2 :
            ℕ) +
          HMul.hMul (α := ℕ) (↑d : ℕ)
            (↑(match (motive := Option Num → Num × Num) Option.some r₂ with
                  | Option.some r' => (q.bit1, r')
                  | Option.none => (q.bit0, r)).1 :
              ℕ) =
        (↑n : ℕ) ∧
      LT.lt (α := ℕ)
        (↑(match (motive := Option Num → Num × Num) Option.some r₂ with
              | Option.some r' => (q.bit1, r')
              | Option.none => (q.bit0, r)).2 :
          ℕ)
        (↑d : ℕ)
⊢ (↑(match (motive := Option Num → Num × Num) Num.ofZNum' (r.sub' (Num.pos d)) with
              | Option.some r' => (q.bit1, r')
              | Option.none => (q.bit0, r)).2 :
          ℕ) +
        HMul.hMul (α := ℕ) (↑d : ℕ)
          (↑(match (motive := Option Num → Num × Num) Num.ofZNum' (r.sub' (Num.pos d)) with
                | Option.some r' => (q.bit1, r')
                | Option.none => (q.bit0, r)).1 :
            ℕ) =
      (↑n : ℕ) ∧
    LT.lt (α := ℕ)
      (↑(match (motive := Option Num → Num × Num) Num.ofZNum' (r.sub' (Num.pos d)) with
            | Option.some r' => (q.bit1, r')
            | Option.none => (q.bit0, r)).2 :
        ℕ)
      (↑d : ℕ)

Tactic:
rcases e : Num.ofZNum' (Num.sub' r (Num.pos d)) with - | r₂

Premises used: Num.ofZNum', Num.pos, Num.sub'
-- Module: Mathlib.Data.Num.ZNum
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)) = Option.none
none :
  (↑(match (motive := Option Num → Num × Num) Option.none with
              | some r' => (q.bit1, r')
              | Option.none => (q.bit0, r)).2 :
          ℕ) +
        (↑d : ℕ) * HAdd.hAdd (α := ℕ) (↑q : ℕ) (↑q : ℕ) =
      (↑n : ℕ) ∧
    LT.lt (α := ℕ)
      (↑(match (motive := Option Num → Num × Num) Option.none with
            | some r' => (q.bit1, r')
            | Option.none => (q.bit0, r)).2 :
        ℕ)
      (↑d : ℕ)
⊢ (↑(match (motive := Option Num → Num × Num) Option.none with
              | some r' => (q.bit1, r')
              | Option.none => (q.bit0, r)).2 :
          ℕ) +
        HMul.hMul (α := ℕ) (↑d : ℕ)
          (↑(match (motive := Option Num → Num × Num) Option.none with
                | some r' => (q.bit1, r')
                | Option.none => (q.bit0, r)).1 :
            ℕ) =
      (↑n : ℕ) ∧
    LT.lt (α := ℕ)
      (↑(match (motive := Option Num → Num × Num) Option.none with
            | some r' => (q.bit1, r')
            | Option.none => (q.bit0, r)).2 :
        ℕ)
      (↑d : ℕ)

Tactic:
rw [Num.cast_bit0, two_mul]

Premises used: Num.cast_bit0, two_mul
-- Module: Mathlib.Data.Num.ZNum
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 : ℕ)

Tactic:
⟨h₁, lt_of_not_ge fun h => ?_⟩

Premises used: lt_of_not_ge, And.intro
-- Module: Mathlib.Data.Num.ZNum
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)) = Option.none
none :
  ∀
    (h :
      LE.le (α := ℕ) (↑d : ℕ)
        (↑(match (motive := Option Num → Num × Num) Option.none with
              | some r' => (q.bit1, r')
              | Option.none => (q.bit0, r)).2 :
          ℕ)),
    False
⊢ (↑(match (motive := Option Num → Num × Num) Option.none with
              | some r' => (q.bit1, r')
              | Option.none => (q.bit0, r)).2 :
          ℕ) +
        (↑d : ℕ) * HAdd.hAdd (α := ℕ) (↑q : ℕ) (↑q : ℕ) =
      (↑n : ℕ) ∧
    LT.lt (α := ℕ)
      (↑(match (motive := Option Num → Num × Num) Option.none with
            | some r' => (q.bit1, r')
            | Option.none => (q.bit0, r)).2 :
        ℕ)
      (↑d : ℕ)

Tactic:
refine ⟨h₁, lt_of_not_ge fun h => ?_⟩
-- Module: Mathlib.Data.Num.ZNum
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)) = Option.none
h :
  LE.le (α := ℕ) (↑d : ℕ)
    (↑(match (motive := Option Num → Num × Num) Option.none with
          | some r' => (q.bit1, r')
          | Option.none => (q.bit0, r)).2 :
      ℕ)
none :
  ∀ (r₂ : ℕ)
    (e' :
      (↑d : ℕ) + r₂ =
        (↑(match (motive := Option Num → Num × Num) Option.none with
              | some r' => (q.bit1, r')
              | Option.none => (q.bit0, r)).2 :
          ℕ)),
    False
⊢ False

Tactic:
obtain ⟨r₂, e'⟩ := Nat.le.dest h

Premises used: Nat.le.dest
-- Module: Mathlib.Data.Num.ZNum
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 :
      ℕ)
⊢ 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'

Premises used: Num.to_of_nat, add_comm
-- Module: Mathlib.Data.Num.ZNum
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' :
  HAdd.hAdd (α := ℕ) (↑(↑r₂ : Num) : ℕ) (↑d : ℕ) =
    (↑(match (motive := Option Num → Num × Num) none with
          | some r' => (q.bit1, r')
          | none => (q.bit0, r)).2 :
      ℕ)
⊢ False

Tactic:
cases e.symm.trans (this.2 e'.symm)

Premises used: Iff.mpr, Eq.symm, Eq.trans
-- Module: Mathlib.Data.Num.ZNum
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₂
⊢ (↑r : ℕ) = HAdd.hAdd (α := ℕ) (↑r₂ : ℕ) (↑d : ℕ)

Tactic:
have := this.1 e
-- Module: Mathlib.Data.Num.ZNum
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 : ℕ) ∧ LT.lt (α := ℕ) (↑r₂ : ℕ) (↑d : ℕ)
⊢ (↑(match (motive := Option Num → Num × Num) Option.some r₂ with
              | Option.some r' => (q.bit1, r')
              | none => (q.bit0, r)).2 :
          ℕ) +
        HMul.hMul (α := ℕ) (↑d : ℕ)
          (↑(match (motive := Option Num → Num × Num) Option.some r₂ with
                | Option.some r' => (q.bit1, r')
                | none => (q.bit0, r)).1 :
            ℕ) =
      (↑n : ℕ) ∧
    LT.lt (α := ℕ)
      (↑(match (motive := Option Num → Num × Num) Option.some r₂ with
            | Option.some r' => (q.bit1, r')
            | none => (q.bit0, r)).2 :
        ℕ)
      (↑d : ℕ)

Tactic:
simp only [Num.cast_bit1]

Premises used: Num.cast_bit1
-- Module: Mathlib.Data.Num.ZNum
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 : ℕ)
some₁ : LT.lt (α := ℕ) (↑r₂ : ℕ) (↑d : ℕ)
⊢ (↑r₂ : ℕ) + (↑d : ℕ) * (HMul.hMul (α := ℕ) 2 (↑q : ℕ) + 1) = (↑n : ℕ) ∧ LT.lt (α := ℕ) (↑r₂ : ℕ) (↑d : ℕ)

Tactic:
constructor
-- Module: Mathlib.Data.Num.ZNum
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 : ℕ)
some₄ : HAdd.hAdd (α := ℕ) (↑r₂ : ℕ) (↑d : ℕ) + (↑d : ℕ) * HAdd.hAdd (α := ℕ) (↑q : ℕ) (↑q : ℕ) = (↑n : ℕ)
some₅ some₆ some₇ some₈ : (↑r : ℕ) + (↑d : ℕ) * HAdd.hAdd (α := ℕ) (↑q : ℕ) (↑q : ℕ) = (↑n : ℕ)
⊢ (↑r₂ : ℕ) + (↑d : ℕ) * (HMul.hMul (α := ℕ) 2 (↑q : ℕ) + 1) = (↑n : ℕ)

Tactic:
rwa [two_mul, add_comm _ 1, mul_add, mul_one, ← add_assoc, ← this]

Premises used: add_assoc, two_mul, add_comm, mul_add, mul_one, OfNat.ofNat
-- Module: Mathlib.Data.Num.ZNum
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 : ℕ)
some₂ some₃ some₄ 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 : ℕ)
⊢ LT.lt (α := ℕ) (↑r₂ : ℕ) (↑d : ℕ)

Tactic:
rwa [this, two_mul, add_lt_add_iff_right] at h₂

Premises used: two_mul, add_lt_add_iff_right
-- Module: Mathlib.Data.Num.ZNum
Goal:
d n : PosNum
rw :
  (↑(d.divMod n).2 : ℕ) + HMul.hMul (α := ℕ) (↑d : ℕ) (↑(d.divMod n).1 : ℕ) = (↑n : ℕ) ∧
    LT.lt (α := ℕ) (↑(d.divMod n).2 : ℕ) (↑d : ℕ)
⊢ HDiv.hDiv (α := ℕ) (↑n : ℕ) (↑d : ℕ) = (↑(d.divMod n).1 : ℕ) ∧
    HMod.hMod (α := ℕ) (↑n : ℕ) (↑d : ℕ) = (↑(d.divMod n).2 : ℕ)

Tactic:
rw [Nat.div_mod_unique (PosNum.cast_pos _)]

Premises used: Nat.div_mod_unique, PosNum.cast_pos
-- Module: Mathlib.Data.Num.ZNum
Goal:
d : PosNum
⊢ (↑1 : ℕ) + (↑d : ℕ) * HAdd.hAdd (α := ℕ) (↑0 : ℕ) (↑0 : ℕ) = (↑one : ℕ)

Tactic:
simp
-- Module: Mathlib.Data.Num.ZNum
Goal:
d : PosNum
⊢ (↑(d.divMod one).2 : ℕ) + HMul.hMul (α := ℕ) (↑d : ℕ) (↑(d.divMod one).1 : ℕ) = (↑one : ℕ) ∧
    LT.lt (α := ℕ) (↑(d.divMod one).2 : ℕ) (↑d : ℕ)

Tactic:
exact divMod_to_nat_aux (by simp) (Nat.mul_le_mul_left 2 (PosNum.cast_pos d : (0 : ℕ) < d))
-- Module: Mathlib.Data.Num.ZNum
Goal:
d n : PosNum
IH :
  (↑(d.divMod n).2 : ℕ) + HMul.hMul (α := ℕ) (↑d : ℕ) (↑(d.divMod n).1 : ℕ) = (↑n : ℕ) ∧
    LT.lt (α := ℕ) (↑(d.divMod n).2 : ℕ) (↑d : ℕ)
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 : ℕ)
⊢ (↑(d.divMod n.bit1).2 : ℕ) + HMul.hMul (α := ℕ) (↑d : ℕ) (↑(d.divMod n.bit1).1 : ℕ) = (↑n.bit1 : ℕ) ∧
    LT.lt (α := ℕ) (↑(d.divMod n.bit1).2 : ℕ) (↑d : ℕ)

Tactic:
unfold divMod

Premises used: PosNum.divMod
-- Module: Mathlib.Data.Num.ZNum
Goal:
d n : PosNum
IH :
  (↑(d.divMod n).2 : ℕ) + HMul.hMul (α := ℕ) (↑d : ℕ) (↑(d.divMod n).1 : ℕ) = (↑n : ℕ) ∧
    LT.lt (α := ℕ) (↑(d.divMod n).2 : ℕ) (↑d : ℕ)
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 : ℕ)
⊢ (↑(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
-- Module: Mathlib.Data.Num.ZNum
Goal:
d n : PosNum
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 : ℕ)
⊢ ∀
    (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:
obtain ⟨q, r⟩ := divMod d n

Premises used: PosNum.divMod
-- Module: Mathlib.Data.Num.ZNum
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 : ℕ)
bit1₁ : (↑r.bit1 : ℕ) < HMul.hMul (α := ℕ) 2 (↑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 : ℕ)

Tactic:
apply divMod_to_nat_aux

Premises used: PosNum.divMod_to_nat_aux
-- Module: Mathlib.Data.Num.ZNum
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 : ℕ) * HAdd.hAdd (α := ℕ) (↑q : ℕ) (↑q : ℕ) =
    HAdd.hAdd (α := ℕ) (↑n : ℕ) (↑n : ℕ) + 1
⊢ (↑r.bit1 : ℕ) + (↑d : ℕ) * HAdd.hAdd (α := ℕ) (↑q : ℕ) (↑q : ℕ) = (↑n.bit1 : ℕ)

Tactic:
simp only [Num.cast_bit1, cast_bit1]

Premises used: PosNum.cast_bit1, Num.cast_bit1
-- Module: Mathlib.Data.Num.ZNum
Goal:
d n : PosNum
q r : Num
IH : (↑r : ℕ) + HMul.hMul (α := ℕ) (↑d : ℕ) (↑q : ℕ) = (↑n : ℕ) ∧ LT.lt (α := ℕ) (↑r : ℕ) (↑d : ℕ)
bit1 : HMul.hMul (α := ℕ) 2 (↑r : ℕ) + 1 < HMul.hMul (α := ℕ) 2 (↑d : ℕ)
⊢ (↑r.bit1 : ℕ) < HMul.hMul (α := ℕ) 2 (↑d : ℕ)

Tactic:
simp only [Num.cast_bit1, cast_bit1]

Premises used: PosNum.cast_bit1, Num.cast_bit1