awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : ℕ) * 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
bit1₄ : 2 * ((↑r : ℕ) + HMul.hMul (α := ℕ) (↑d : ℕ) (↑q : ℕ)) + 1 = HMul.hMul (α := ℕ) 2 (↑n : ℕ) + 1
bit1₅ bit1₆ : HMul.hMul (α := ℕ) 2 (↑n : ℕ) + 1 = HMul.hMul (α := ℕ) 2 (↑n : ℕ) + 1
⊢ HMul.hMul (α := ℕ) 2 (↑r : ℕ) + 1 + (↑d : ℕ) * HAdd.hAdd (α := ℕ) (↑q : ℕ) (↑q : ℕ) =
    HAdd.hAdd (α := ℕ) (↑n : ℕ) (↑n : ℕ) + 1

Tactic:
rw [← two_mul, ← two_mul, add_right_comm, mul_left_comm, ← mul_add, IH.1]

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

Tactic:
lia
-- 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 : ℕ)
bit0 :
  (↑(match (motive := Num × Num → Num × Num) d.divMod n with
              | (q, r₁) => d.divModAux q r₁.bit0).2 :
          ℕ) +
        HMul.hMul (α := ℕ) (↑d : ℕ)
          (↑(match (motive := Num × Num → Num × Num) d.divMod n with
                | (q, r₁) => d.divModAux q r₁.bit0).1 :
            ℕ) =
      (↑n.bit0 : ℕ) ∧
    LT.lt (α := ℕ)
      (↑(match (motive := Num × Num → Num × Num) d.divMod n with
            | (q, r₁) => d.divModAux q r₁.bit0).2 :
        ℕ)
      (↑d : ℕ)
⊢ (↑(d.divMod n.bit0).2 : ℕ) + HMul.hMul (α := ℕ) (↑d : ℕ) (↑(d.divMod n.bit0).1 : ℕ) = (↑n.bit0 : ℕ) ∧
    LT.lt (α := ℕ) (↑(d.divMod n.bit0).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 : ℕ)
bit0 :
  ∀
    (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₁.bit0).2 :
            ℕ) +
          HMul.hMul (α := ℕ) (↑d : ℕ)
            (↑(match (motive := Num × Num → Num × Num) d.divMod n with
                  | (q, r₁) => d.divModAux q r₁.bit0).1 :
              ℕ) =
        (↑n.bit0 : ℕ) ∧
      LT.lt (α := ℕ)
        (↑(match (motive := Num × Num → Num × Num) d.divMod n with
              | (q, r₁) => d.divModAux q r₁.bit0).2 :
          ℕ)
        (↑d : ℕ)
⊢ (↑(match (motive := Num × Num → Num × Num) d.divMod n with
              | (q, r₁) => d.divModAux q r₁.bit0).2 :
          ℕ) +
        HMul.hMul (α := ℕ) (↑d : ℕ)
          (↑(match (motive := Num × Num → Num × Num) d.divMod n with
                | (q, r₁) => d.divModAux q r₁.bit0).1 :
            ℕ) =
      (↑n.bit0 : ℕ) ∧
    LT.lt (α := ℕ)
      (↑(match (motive := Num × Num → Num × Num) d.divMod n with
            | (q, r₁) => d.divModAux q r₁.bit0).2 :
        ℕ)
      (↑d : ℕ)

Tactic:
revert IH
-- Module: Mathlib.Data.Num.ZNum
Goal:
d n : PosNum
bit0 :
  ∀ (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₁.bit0).2 :
            ℕ) +
          HMul.hMul (α := ℕ) (↑d : ℕ)
            (↑(match (motive := Num × Num → Num × Num) (q, r) with
                  | (q, r₁) => d.divModAux q r₁.bit0).1 :
              ℕ) =
        (↑n.bit0 : ℕ) ∧
      LT.lt (α := ℕ)
        (↑(match (motive := Num × Num → Num × Num) (q, r) with
              | (q, r₁) => d.divModAux q r₁.bit0).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₁.bit0).2 :
            ℕ) +
          HMul.hMul (α := ℕ) (↑d : ℕ)
            (↑(match (motive := Num × Num → Num × Num) d.divMod n with
                  | (q, r₁) => d.divModAux q r₁.bit0).1 :
              ℕ) =
        (↑n.bit0 : ℕ) ∧
      LT.lt (α := ℕ)
        (↑(match (motive := Num × Num → Num × Num) d.divMod n with
              | (q, r₁) => d.divModAux q r₁.bit0).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 : ℕ)
bit0 : (↑r.bit0 : ℕ) + (↑d : ℕ) * HAdd.hAdd (α := ℕ) (↑q : ℕ) (↑q : ℕ) = (↑n.bit0 : ℕ)
bit0₁ : (↑r.bit0 : ℕ) < HMul.hMul (α := ℕ) 2 (↑d : ℕ)
⊢ (↑(d.divModAux q r.bit0).2 : ℕ) + HMul.hMul (α := ℕ) (↑d : ℕ) (↑(d.divModAux q r.bit0).1 : ℕ) = (↑n.bit0 : ℕ) ∧
    LT.lt (α := ℕ) (↑(d.divModAux q r.bit0).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 : ℕ)
bit0 :
  HMul.hMul (α := ℕ) 2 (↑r : ℕ) + (↑d : ℕ) * HAdd.hAdd (α := ℕ) (↑q : ℕ) (↑q : ℕ) = HAdd.hAdd (α := ℕ) (↑n : ℕ) (↑n : ℕ)
⊢ (↑r.bit0 : ℕ) + (↑d : ℕ) * HAdd.hAdd (α := ℕ) (↑q : ℕ) (↑q : ℕ) = (↑n.bit0 : ℕ)

Tactic:
simp only [Num.cast_bit0, cast_bit0]

Premises used: Num.cast_bit0, PosNum.cast_bit0
-- Module: Mathlib.Data.Num.ZNum
Goal:
d n : PosNum
q r : Num
IH : (↑r : ℕ) + HMul.hMul (α := ℕ) (↑d : ℕ) (↑q : ℕ) = (↑n : ℕ) ∧ LT.lt (α := ℕ) (↑r : ℕ) (↑d : ℕ)
bit0 : HMul.hMul (α := ℕ) 2 (↑r : ℕ) + (↑d : ℕ) * HMul.hMul (α := ℕ) 2 (↑q : ℕ) = HAdd.hAdd (α := ℕ) (↑n : ℕ) (↑n : ℕ)
bit0₁ : HMul.hMul (α := ℕ) 2 (↑r : ℕ) + (↑d : ℕ) * HMul.hMul (α := ℕ) 2 (↑q : ℕ) = HMul.hMul (α := ℕ) 2 (↑n : ℕ)
bit0₂ : HMul.hMul (α := ℕ) 2 (↑r : ℕ) + 2 * HMul.hMul (α := ℕ) (↑d : ℕ) (↑q : ℕ) = HMul.hMul (α := ℕ) 2 (↑n : ℕ)
bit0₃ : 2 * ((↑r : ℕ) + HMul.hMul (α := ℕ) (↑d : ℕ) (↑q : ℕ)) = HMul.hMul (α := ℕ) 2 (↑n : ℕ)
bit0₄ bit0₅ :
  2 * ((↑r : ℕ) + HMul.hMul (α := ℕ) (↑d : ℕ) (↑q : ℕ)) = 2 * ((↑r : ℕ) + HMul.hMul (α := ℕ) (↑d : ℕ) (↑q : ℕ))
⊢ HMul.hMul (α := ℕ) 2 (↑r : ℕ) + (↑d : ℕ) * HAdd.hAdd (α := ℕ) (↑q : ℕ) (↑q : ℕ) = HAdd.hAdd (α := ℕ) (↑n : ℕ) (↑n : ℕ)

Tactic:
rw [← two_mul, ← two_mul, mul_left_comm, ← mul_add, ← IH.1]

Premises used: two_mul, mul_left_comm, And.left, mul_add
-- Module: Mathlib.Data.Num.ZNum
Goal:
d n : PosNum
q r : Num
IH : (↑r : ℕ) + HMul.hMul (α := ℕ) (↑d : ℕ) (↑q : ℕ) = (↑n : ℕ) ∧ LT.lt (α := ℕ) (↑r : ℕ) (↑d : ℕ)
⊢ (↑r.bit0 : ℕ) < HMul.hMul (α := ℕ) 2 (↑d : ℕ)

Tactic:
simpa using IH.2

Premises used: And.right
-- Module: Mathlib.Data.Num.ZNum
Goal:
d n : PosNum
one :
  (↑(d.divMod PosNum.one).2 : ℕ) + HMul.hMul (α := ℕ) (↑d : ℕ) (↑(d.divMod PosNum.one).1 : ℕ) = (↑PosNum.one : ℕ) ∧
    LT.lt (α := ℕ) (↑(d.divMod PosNum.one).2 : ℕ) (↑d : ℕ)
bit1 :
  ∀ (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 : ℕ)
bit0 :
  ∀ (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.bit0).2 : ℕ) + HMul.hMul (α := ℕ) (↑d : ℕ) (↑(d.divMod n.bit0).1 : ℕ) = (↑n.bit0 : ℕ) ∧
      LT.lt (α := ℕ) (↑(d.divMod n.bit0).2 : ℕ) (↑d : ℕ)
⊢ (↑(d.divMod n).2 : ℕ) + HMul.hMul (α := ℕ) (↑d : ℕ) (↑(d.divMod n).1 : ℕ) = (↑n : ℕ) ∧
    LT.lt (α := ℕ) (↑(d.divMod n).2 : ℕ) (↑d : ℕ)

Tactic:
induction n with
  | one =>
    exact divMod_to_nat_aux (by simp) (Nat.mul_le_mul_left 2 (PosNum.cast_pos d : (0 : ℕ) < d))
  | bit1 n IH =>
    unfold divMod
    -- Porting note: `cases'` didn't rewrite at `this`, so `revert` & `intro` are required.
    revert IH; obtain ⟨q, r⟩ := divMod d n; intro IH
    simp only at IH ⊢
    apply divMod_to_nat_aux <;> simp only [Num.cast_bit1, cast_bit1]
    · rw [← two_mul, ← two_mul, add_right_comm, mul_left_comm, ← mul_add, IH.1]
    · lia
  | bit0 n IH =>
    unfold divMod
    -- Porting note: `cases'` didn't rewrite at `this`, so `revert` & `intro` are required.
    revert IH; obtain ⟨q, r⟩ := divMod d n; intro IH
    simp only at IH ⊢
    apply divMod_to_nat_aux
    · simp only [Num.cast_bit0, cast_bit0]
      rw [← two_mul, ← two_mul, mul_left_comm, ← mul_add, ← IH.1]
    · simpa using IH.2

Premises used: PosNum.cast_bit1, Num.cast_bit0, PosNum.bit1, two_mul, Num.cast_bit1, add_right_comm, mul_left_comm, PosNum.bit0, PosNum.divMod, PosNum.divMod_to_nat_aux, PosNum.cast_bit0, mul_add, PosNum.one
-- Module: Mathlib.Data.Num.ZNum
Goal:
n d : PosNum
⊢ (↑(n.div' d) : ℕ) = HDiv.hDiv (α := ℕ) (↑n : ℕ) (↑d : ℕ)

Tactic:
(divMod_to_nat _ _).1.symm

Premises used: PosNum.div', And.left, PosNum.divMod_to_nat, Eq.symm
-- Module: Mathlib.Data.Num.ZNum
Goal:
n d : PosNum
⊢ (↑(n.mod' d) : ℕ) = HMod.hMod (α := ℕ) (↑n : ℕ) (↑d : ℕ)

Tactic:
(divMod_to_nat _ _).2.symm

Premises used: PosNum.mod', And.right, PosNum.divMod_to_nat, Eq.symm
-- Module: Mathlib.Data.Num.ZNum
Goal:
n : Num
zero : Num.zero.div 0 = 0
pos : ∀ (a : PosNum), (Num.pos a).div 0 = 0
⊢ n.div 0 = 0

Tactic:
cases n
-- Module: Mathlib.Data.Num.ZNum
Goal:
⊢ zero.div 0 = 0

Tactic:
rfl
-- Module: Mathlib.Data.Num.ZNum
Goal:
a : PosNum
⊢ (pos a).div 0 = 0

Tactic:
simp [Num.div]

Premises used: Num.div
-- Module: Mathlib.Data.Num.ZNum
Goal:
⊢ (↑(0 / 0) : ℕ) = HDiv.hDiv (α := ℕ) (↑0 : ℕ) (↑0 : ℕ)

Tactic:
simp
-- Module: Mathlib.Data.Num.ZNum
Goal:
n : Num
zero : Num.zero.mod 0 = Num.zero
pos : ∀ (a : PosNum), (Num.pos a).mod 0 = Num.pos a
⊢ n.mod 0 = n

Tactic:
cases n
-- Module: Mathlib.Data.Num.ZNum
Goal:
⊢ zero.mod 0 = zero

Tactic:
rfl
-- Module: Mathlib.Data.Num.ZNum
Goal:
a : PosNum
⊢ (pos a).mod 0 = pos a

Tactic:
simp [Num.mod]

Premises used: Num.mod
-- Module: Mathlib.Data.Num.ZNum
Goal:
⊢ (↑(HMod.hMod (α := Num) 0 0) : ℕ) = HMod.hMod (α := ℕ) (↑0 : ℕ) (↑0 : ℕ)

Tactic:
simp
-- Module: Mathlib.Data.Num.ZNum
Goal:
n : ℕ
a : PosNum
b : Num
ab : pos a ≤ b
h : (pos a * b).natSize ≤ n.succ
simp : (↑(gcdAux n (b % pos a) (pos a)) : ℕ) = Nat.gcd (↑a : ℕ) (↑b : ℕ)
⊢ (↑(gcdAux n.succ (pos a) b) : ℕ) = Nat.gcd (↑(pos a) : ℕ) (↑b : ℕ)

Tactic:
simp only [gcdAux, cast_pos]

Premises used: Num.gcdAux, Num.cast_pos
-- Module: Mathlib.Data.Num.ZNum
Goal:
n : ℕ
a : PosNum
b : Num
ab : pos a ≤ b
h : (pos a * b).natSize ≤ n.succ
rw :
  (HMod.hMod (α := ℕ) (↑b : ℕ) (↑(pos a) : ℕ)).gcd (↑(pos a) : ℕ) = (HMod.hMod (α := ℕ) (↑b : ℕ) (↑a : ℕ)).gcd (↑a : ℕ)
a₁ : b % pos a ≤ pos a
a₂ : (b % pos a * pos a).natSize ≤ n
⊢ (↑(gcdAux n (b % pos a) (pos a)) : ℕ) = Nat.gcd (↑a : ℕ) (↑b : ℕ)

Tactic:
rw [Nat.gcd_rec, gcd_to_nat_aux, mod_to_nat]

Premises used: Nat.gcd_rec, Num.mod_to_nat
-- Module: Mathlib.Data.Num.ZNum
Goal:
n : ℕ
a : PosNum
b : Num
ab : pos a ≤ b
h : (pos a * b).natSize ≤ n.succ
⊢ (HMod.hMod (α := ℕ) (↑b : ℕ) (↑(pos a) : ℕ)).gcd (↑(pos a) : ℕ) = (HMod.hMod (α := ℕ) (↑b : ℕ) (↑a : ℕ)).gcd (↑a : ℕ)

Tactic:
rfl
-- Module: Mathlib.Data.Num.ZNum
Goal:
n : ℕ
a : PosNum
b : Num
ab : pos a ≤ b
h : (pos a * b).natSize ≤ n.succ
a₁ : HMod.hMod (α := ℕ) (↑b : ℕ) (↑(pos a) : ℕ) ≤ (↑(pos a) : ℕ)
⊢ b % pos a ≤ pos a

Tactic:
rw [← le_to_nat, mod_to_nat]

Premises used: Num.le_to_nat, Num.mod_to_nat
-- Module: Mathlib.Data.Num.ZNum
Goal:
n : ℕ
a : PosNum
b : Num
ab : pos a ≤ b
h : (pos a * b).natSize ≤ n.succ
⊢ HMod.hMod (α := ℕ) (↑b : ℕ) (↑(pos a) : ℕ) ≤ (↑(pos a) : ℕ)

Tactic:
le_of_lt (Nat.mod_lt _ (PosNum.cast_pos _))

Premises used: le_of_lt, Nat.mod_lt, PosNum.cast_pos
-- Module: Mathlib.Data.Num.ZNum
Goal:
n : ℕ
a : PosNum
b : Num
ab : pos a ≤ b
h : (pos a * b).natSize ≤ n.succ
⊢ HMod.hMod (α := ℕ) (↑b : ℕ) (↑(pos a) : ℕ) ≤ (↑(pos a) : ℕ)

Tactic:
exact le_of_lt (Nat.mod_lt _ (PosNum.cast_pos _))

Premises used: le_of_lt, Nat.mod_lt, PosNum.cast_pos
-- Module: Mathlib.Data.Num.ZNum
Goal:
n : ℕ
a : PosNum
b : Num
ab : pos a ≤ b
h : (pos a * b).natSize ≤ n.succ
a₁ :
  ∀ (h : HMul.hMul (α := ℕ) (↑(pos a) : ℕ) (↑b : ℕ) < HPow.hPow (α := ℕ) 2 n.succ),
    HMul.hMul (α := ℕ) (↑(b % pos a) : ℕ) (↑(pos a) : ℕ) < HPow.hPow (α := ℕ) 2 n
⊢ (b % pos a * pos a).natSize ≤ n

Tactic:
rw [natSize_to_nat, mul_to_nat, Nat.size_le] at h ⊢

Premises used: Num.natSize_to_nat, Num.mul_to_nat, Nat.size_le
-- Module: Mathlib.Data.Num.ZNum
Goal:
n : ℕ
a : PosNum
b : Num
ab : pos a ≤ b
h : HMul.hMul (α := ℕ) (↑(pos a) : ℕ) (↑b : ℕ) < HPow.hPow (α := ℕ) 2 n.succ
a₁ : (↑(pos a) : ℕ) * HMod.hMod (α := ℕ) (↑b : ℕ) (↑(pos a) : ℕ) < HPow.hPow (α := ℕ) 2 n
⊢ HMul.hMul (α := ℕ) (↑(b % pos a) : ℕ) (↑(pos a) : ℕ) < HPow.hPow (α := ℕ) 2 n

Tactic:
rw [mod_to_nat, mul_comm]

Premises used: mul_comm, Num.mod_to_nat
-- Module: Mathlib.Data.Num.ZNum
Goal:
n : ℕ
a : PosNum
b : Num
ab : pos a ≤ b
h : HMul.hMul (α := ℕ) (↑(pos a) : ℕ) (↑b : ℕ) < HPow.hPow (α := ℕ) 2 n.succ
⊢ (↑(pos a) : ℕ) *
      (HMod.hMod (α := ℕ) (↑b : ℕ) (↑(pos a) : ℕ) + (↑(pos a) : ℕ) * HDiv.hDiv (α := ℕ) (↑b : ℕ) (↑(pos a) : ℕ)) <
    HPow.hPow (α := ℕ) 2 n * 2

Tactic:
rw [pow_succ, ← Nat.mod_add_div b (pos a)] at h

Premises used: pow_succ, castNum, Nat.mod_add_div, Num.pos
-- Module: Mathlib.Data.Num.ZNum
Goal:
n : ℕ
a : PosNum
b : Num
ab : pos a ≤ b
h :
  (↑(pos a) : ℕ) *
      (HMod.hMod (α := ℕ) (↑b : ℕ) (↑(pos a) : ℕ) + (↑(pos a) : ℕ) * HDiv.hDiv (α := ℕ) (↑b : ℕ) (↑(pos a) : ℕ)) <
    HPow.hPow (α := ℕ) 2 n * 2
⊢ (↑(pos a) : ℕ) * HMod.hMod (α := ℕ) (↑b : ℕ) (↑(pos a) : ℕ) < HPow.hPow (α := ℕ) 2 n

Tactic:
lt_of_mul_lt_mul_right (lt_of_le_of_lt ?_ h) (Nat.zero_le 2)

Premises used: Nat.zero_le, lt_of_le_of_lt, lt_of_mul_lt_mul_right, OfNat.ofNat
-- Module: Mathlib.Data.Num.ZNum
Goal:
n : ℕ
a : PosNum
b : Num
ab : pos a ≤ b
h :
  (↑(pos a) : ℕ) *
      (HMod.hMod (α := ℕ) (↑b : ℕ) (↑(pos a) : ℕ) + (↑(pos a) : ℕ) * HDiv.hDiv (α := ℕ) (↑b : ℕ) (↑(pos a) : ℕ)) <
    HPow.hPow (α := ℕ) 2 n * 2
a₁ :
  (↑(pos a) : ℕ) * HMod.hMod (α := ℕ) (↑b : ℕ) (↑(pos a) : ℕ) * 2 ≤
    (↑(pos a) : ℕ) *
      (HMod.hMod (α := ℕ) (↑b : ℕ) (↑(pos a) : ℕ) + (↑(pos a) : ℕ) * HDiv.hDiv (α := ℕ) (↑b : ℕ) (↑(pos a) : ℕ))
⊢ (↑(pos a) : ℕ) * HMod.hMod (α := ℕ) (↑b : ℕ) (↑(pos a) : ℕ) < HPow.hPow (α := ℕ) 2 n

Tactic:
refine lt_of_mul_lt_mul_right (lt_of_le_of_lt ?_ h) (Nat.zero_le 2)

Premises used: Nat.zero_le, lt_of_le_of_lt, lt_of_mul_lt_mul_right, OfNat.ofNat
-- Module: Mathlib.Data.Num.ZNum
Goal:
n : ℕ
a : PosNum
b : Num
ab : pos a ≤ b
h :
  (↑(pos a) : ℕ) *
      (HMod.hMod (α := ℕ) (↑b : ℕ) (↑(pos a) : ℕ) + (↑(pos a) : ℕ) * HDiv.hDiv (α := ℕ) (↑b : ℕ) (↑(pos a) : ℕ)) <
    HPow.hPow (α := ℕ) 2 n * 2
a₁ :
  (↑(pos a) : ℕ) * HMod.hMod (α := ℕ) (↑b : ℕ) (↑(pos a) : ℕ) +
      (↑(pos a) : ℕ) * HMod.hMod (α := ℕ) (↑b : ℕ) (↑(pos a) : ℕ) ≤
    (↑(pos a) : ℕ) * HMod.hMod (α := ℕ) (↑b : ℕ) (↑(pos a) : ℕ) +
      (↑(pos a) : ℕ) * ((↑(pos a) : ℕ) * HDiv.hDiv (α := ℕ) (↑b : ℕ) (↑(pos a) : ℕ))
⊢ (↑(pos a) : ℕ) * HMod.hMod (α := ℕ) (↑b : ℕ) (↑(pos a) : ℕ) * 2 ≤
    (↑(pos a) : ℕ) *
      (HMod.hMod (α := ℕ) (↑b : ℕ) (↑(pos a) : ℕ) + (↑(pos a) : ℕ) * HDiv.hDiv (α := ℕ) (↑b : ℕ) (↑(pos a) : ℕ))

Tactic:
rw [mul_two, mul_add]

Premises used: mul_add, mul_two
-- Module: Mathlib.Data.Num.ZNum
Goal:
n : ℕ
a : PosNum
b : Num
ab : pos a ≤ b
h :
  (↑(pos a) : ℕ) *
      (HMod.hMod (α := ℕ) (↑b : ℕ) (↑(pos a) : ℕ) + (↑(pos a) : ℕ) * HDiv.hDiv (α := ℕ) (↑b : ℕ) (↑(pos a) : ℕ)) <
    HPow.hPow (α := ℕ) 2 n * 2
a₁ : HMod.hMod (α := ℕ) (↑b : ℕ) (↑(pos a) : ℕ) ≤ (↑(pos a) : ℕ) * HDiv.hDiv (α := ℕ) (↑b : ℕ) (↑(pos a) : ℕ)
⊢ (↑(pos a) : ℕ) * HMod.hMod (α := ℕ) (↑b : ℕ) (↑(pos a) : ℕ) +
      (↑(pos a) : ℕ) * HMod.hMod (α := ℕ) (↑b : ℕ) (↑(pos a) : ℕ) ≤
    (↑(pos a) : ℕ) * HMod.hMod (α := ℕ) (↑b : ℕ) (↑(pos a) : ℕ) +
      (↑(pos a) : ℕ) * ((↑(pos a) : ℕ) * HDiv.hDiv (α := ℕ) (↑b : ℕ) (↑(pos a) : ℕ))

Tactic:
gcongr _ + _ * ?_
-- Module: Mathlib.Data.Num.ZNum
Goal:
n : ℕ
a : PosNum
b : Num
ab : pos a ≤ b
h :
  (↑(pos a) : ℕ) *
      (HMod.hMod (α := ℕ) (↑b : ℕ) (↑(pos a) : ℕ) + (↑(pos a) : ℕ) * HDiv.hDiv (α := ℕ) (↑b : ℕ) (↑(pos a) : ℕ)) <
    HPow.hPow (α := ℕ) 2 n * 2
a₁ : (↑(pos a) : ℕ) ≤ (↑(pos a) : ℕ) * HDiv.hDiv (α := ℕ) (↑(pos a) : ℕ) (↑(pos a) : ℕ)
a₂ : LT.lt (α := ℕ) 0 (↑(pos a) : ℕ)
⊢ HMod.hMod (α := ℕ) (↑b : ℕ) (↑(pos a) : ℕ) ≤ (↑(pos a) : ℕ) * HDiv.hDiv (α := ℕ) (↑b : ℕ) (↑(pos a) : ℕ)

Tactic:
grw [Nat.mod_lt, ← le_to_nat.2 ab]

Premises used: Iff.mpr, Nat.mod_lt, Num.le_to_nat
-- Module: Mathlib.Data.Num.ZNum
Goal:
n : ℕ
a : PosNum
b : Num
ab : pos a ≤ b
h :
  (↑(pos a) : ℕ) *
      (HMod.hMod (α := ℕ) (↑b : ℕ) (↑(pos a) : ℕ) + (↑(pos a) : ℕ) * HDiv.hDiv (α := ℕ) (↑b : ℕ) (↑(pos a) : ℕ)) <
    HPow.hPow (α := ℕ) 2 n * 2
⊢ (↑(pos a) : ℕ) ≤ (↑(pos a) : ℕ) * HDiv.hDiv (α := ℕ) (↑(pos a) : ℕ) (↑(pos a) : ℕ)

Tactic:
simp
-- Module: Mathlib.Data.Num.ZNum
Goal:
n : ℕ
a : PosNum
b : Num
ab : pos a ≤ b
h :
  (↑(pos a) : ℕ) *
      (HMod.hMod (α := ℕ) (↑b : ℕ) (↑(pos a) : ℕ) + (↑(pos a) : ℕ) * HDiv.hDiv (α := ℕ) (↑b : ℕ) (↑(pos a) : ℕ)) <
    HPow.hPow (α := ℕ) 2 n * 2
⊢ LT.lt (α := ℕ) 0 (↑(pos a) : ℕ)

Tactic:
PosNum.cast_pos _

Premises used: castNum, PosNum.cast_pos
-- Module: Mathlib.Data.Num.ZNum
Goal:
n : ℕ
a : PosNum
b : Num
ab : pos a ≤ b
h :
  (↑(pos a) : ℕ) *
      (HMod.hMod (α := ℕ) (↑b : ℕ) (↑(pos a) : ℕ) + (↑(pos a) : ℕ) * HDiv.hDiv (α := ℕ) (↑b : ℕ) (↑(pos a) : ℕ)) <
    HPow.hPow (α := ℕ) 2 n * 2
⊢ LT.lt (α := ℕ) 0 (↑(pos a) : ℕ)

Tactic:
exact PosNum.cast_pos _

Premises used: PosNum.cast_pos
-- Module: Mathlib.Data.Num.ZNum
Goal:
a b : Num
simp : (HMul.hMul (α := ℕ) (↑a : ℕ) (↑b : ℕ)).size ≤ Nat.size (↑a : ℕ) + Nat.size (↑b : ℕ)
⊢ (a * b).natSize ≤ a.natSize + b.natSize

Tactic:
simp only [natSize_to_nat, cast_mul]

Premises used: Num.natSize_to_nat, Num.cast_mul
-- Module: Mathlib.Data.Num.ZNum
Goal:
a b : Num
rw :
  HMul.hMul (α := ℕ) (↑a : ℕ) (↑b : ℕ) <
    HPow.hPow (α := ℕ) 2 (Nat.size (↑a : ℕ)) * HPow.hPow (α := ℕ) 2 (Nat.size (↑b : ℕ))
⊢ (HMul.hMul (α := ℕ) (↑a : ℕ) (↑b : ℕ)).size ≤ Nat.size (↑a : ℕ) + Nat.size (↑b : ℕ)

Tactic:
rw [Nat.size_le, pow_add]

Premises used: pow_add, Nat.size_le
-- Module: Mathlib.Data.Num.ZNum
Goal:
a b : Num
⊢ HMul.hMul (α := ℕ) (↑a : ℕ) (↑b : ℕ) <
    HPow.hPow (α := ℕ) 2 (Nat.size (↑a : ℕ)) * HPow.hPow (α := ℕ) 2 (Nat.size (↑b : ℕ))

Tactic:
mul_lt_mul'' (Nat.lt_size_self _) (Nat.lt_size_self _) (Nat.zero_le _) (Nat.zero_le _)

Premises used: Nat.zero_le, Nat.lt_size_self, mul_lt_mul''
-- Module: Mathlib.Data.Num.ZNum
Goal:
a b : Num
⊢ HMul.hMul (α := ℕ) (↑a : ℕ) (↑b : ℕ) <
    HPow.hPow (α := ℕ) 2 (Nat.size (↑a : ℕ)) * HPow.hPow (α := ℕ) 2 (Nat.size (↑b : ℕ))

Tactic:
exact mul_lt_mul'' (Nat.lt_size_self _) (Nat.lt_size_self _) (Nat.zero_le _) (Nat.zero_le _)

Premises used: Nat.zero_le, Nat.lt_size_self, mul_lt_mul''
-- Module: Mathlib.Data.Num.ZNum
Goal:
⊢ ∀ (a b : Num), (a * b).natSize ≤ a.natSize + b.natSize

Tactic:
have : ∀ a b : Num, (a * b).natSize ≤ a.natSize + b.natSize := by
    intros
    simp only [natSize_to_nat, cast_mul]
    rw [Nat.size_le, pow_add]
    exact mul_lt_mul'' (Nat.lt_size_self _) (Nat.lt_size_self _) (Nat.zero_le _) (Nat.zero_le _)
-- Module: Mathlib.Data.Num.ZNum
Goal:
this : ∀ (a b : Num), (a * b).natSize ≤ a.natSize + b.natSize
a b : Num
pos : ∀ (h : a ≤ b), (↑(gcdAux (a.natSize + b.natSize) a b) : ℕ) = Nat.gcd (↑a : ℕ) (↑b : ℕ)
neg : ∀ (h : ¬a ≤ b), (↑(gcdAux (b.natSize + a.natSize) b a) : ℕ) = Nat.gcd (↑a : ℕ) (↑b : ℕ)
⊢ (↑(if a ≤ b then gcdAux (a.natSize + b.natSize) a b else gcdAux (b.natSize + a.natSize) b a) : ℕ) =
    Nat.gcd (↑a : ℕ) (↑b : ℕ)

Tactic:
split_ifs with h
-- Module: Mathlib.Data.Num.ZNum
Goal:
this : ∀ (a b : Num), (a * b).natSize ≤ a.natSize + b.natSize
a b : Num
h : a ≤ b
⊢ (↑(gcdAux (a.natSize + b.natSize) a b) : ℕ) = Nat.gcd (↑a : ℕ) (↑b : ℕ)

Tactic:
gcd_to_nat_aux h (this _ _)

Premises used: Num.gcd_to_nat_aux
-- Module: Mathlib.Data.Num.ZNum
Goal:
this : ∀ (a b : Num), (a * b).natSize ≤ a.natSize + b.natSize
a b : Num
h : a ≤ b
⊢ (↑(gcdAux (a.natSize + b.natSize) a b) : ℕ) = Nat.gcd (↑a : ℕ) (↑b : ℕ)

Tactic:
exact gcd_to_nat_aux h (this _ _)

Premises used: Num.gcd_to_nat_aux
-- Module: Mathlib.Data.Num.ZNum
Goal:
this : ∀ (a b : Num), (a * b).natSize ≤ a.natSize + b.natSize
a b : Num
h : ¬a ≤ b
neg : (↑(gcdAux (b.natSize + a.natSize) b a) : ℕ) = Nat.gcd (↑b : ℕ) (↑a : ℕ)
⊢ (↑(gcdAux (b.natSize + a.natSize) b a) : ℕ) = Nat.gcd (↑a : ℕ) (↑b : ℕ)

Tactic:
rw [Nat.gcd_comm]

Premises used: Nat.gcd_comm
-- Module: Mathlib.Data.Num.ZNum
Goal:
this : ∀ (a b : Num), (a * b).natSize ≤ a.natSize + b.natSize
a b : Num
h : ¬a ≤ b
⊢ (↑(gcdAux (b.natSize + a.natSize) b a) : ℕ) = Nat.gcd (↑b : ℕ) (↑a : ℕ)

Tactic:
gcd_to_nat_aux (le_of_not_ge h) (this _ _)

Premises used: Num.gcd_to_nat_aux, le_of_not_ge
-- Module: Mathlib.Data.Num.ZNum
Goal:
this : ∀ (a b : Num), (a * b).natSize ≤ a.natSize + b.natSize
a b : Num
h : ¬a ≤ b
⊢ (↑(gcdAux (b.natSize + a.natSize) b a) : ℕ) = Nat.gcd (↑b : ℕ) (↑a : ℕ)

Tactic:
exact gcd_to_nat_aux (le_of_not_ge h) (this _ _)

Premises used: Num.gcd_to_nat_aux, le_of_not_ge
-- Module: Mathlib.Data.Num.ZNum
Goal:
m n : Num
rw : HMod.hMod (α := ℕ) (↑n : ℕ) (↑m : ℕ) = 0 ↔ HMod.hMod (α := ℕ) (↑n : ℕ) (↑m : ℕ) = (↑0 : ℕ)
⊢ m ∣ n ↔ n % m = 0

Tactic:
rw [← dvd_to_nat, Nat.dvd_iff_mod_eq_zero, ← to_nat_inj, mod_to_nat]

Premises used: Nat.dvd_iff_mod_eq_zero, Num.dvd_to_nat, Num.mod_to_nat, Num.to_nat_inj
-- Module: Mathlib.Data.Num.ZNum
Goal:
m n : Num
⊢ HMod.hMod (α := ℕ) (↑n : ℕ) (↑m : ℕ) = 0 ↔ HMod.hMod (α := ℕ) (↑n : ℕ) (↑m : ℕ) = (↑0 : ℕ)

Tactic:
rfl
-- Module: Mathlib.Data.Num.ZNum
Goal:
n : ZNum
zero : ZNum.zero.div 0 = 0
pos : ∀ (a : PosNum), (ZNum.pos a).div 0 = 0
neg : ∀ (a : PosNum), (ZNum.neg a).div 0 = 0
⊢ n.div 0 = 0

Tactic:
cases n
-- Module: Mathlib.Data.Num.ZNum
Goal:
a : PosNum
⊢ (pos a).div 0 = 0

Tactic:
rfl
-- Module: Mathlib.Data.Num.ZNum
Goal:
a : PosNum
⊢ (neg a).div 0 = 0

Tactic:
rfl
-- Module: Mathlib.Data.Num.ZNum
Goal:
⊢ (↑(0 / 0) : ℤ) = HDiv.hDiv (α := ℤ) (↑0 : ℤ) (↑0 : ℤ)

Tactic:
simp [Int.ediv_zero]

Premises used: Int.ediv_zero
-- Module: Mathlib.Data.Num.ZNum
Goal:
n d : PosNum
rw : (↑(↑(n.div' d) : ℕ) : ℤ) = HDiv.hDiv (α := ℤ) (↑(pos n) : ℤ) (↑(pos d) : ℤ)
⊢ (↑(n.div' d) : ℤ) = HDiv.hDiv (α := ℤ) (↑(pos n) : ℤ) (↑(pos d) : ℤ)

Tactic:
rw [← Num.to_nat_to_int]

Premises used: Num.to_nat_to_int
-- Module: Mathlib.Data.Num.ZNum
Goal:
n d : PosNum
⊢ (↑(↑(n.div' d) : ℕ) : ℤ) = HDiv.hDiv (α := ℤ) (↑(pos n) : ℤ) (↑(pos d) : ℤ)

Tactic:
simp
-- Module: Mathlib.Data.Num.ZNum
Goal:
n d : PosNum
rw : -(↑(↑(n.div' d) : ℕ) : ℤ) = HDiv.hDiv (α := ℤ) (↑(pos n) : ℤ) (↑(neg d) : ℤ)
⊢ -(↑(n.div' d) : ℤ) = HDiv.hDiv (α := ℤ) (↑(pos n) : ℤ) (↑(neg d) : ℤ)

Tactic:
rw [← Num.to_nat_to_int]

Premises used: Num.to_nat_to_int
-- Module: Mathlib.Data.Num.ZNum
Goal:
n d : PosNum
⊢ -(↑(↑(n.div' d) : ℕ) : ℤ) = HDiv.hDiv (α := ℤ) (↑(pos n) : ℤ) (↑(neg d) : ℤ)

Tactic:
simp
-- Module: Mathlib.Data.Num.ZNum
Goal:
n d : PosNum
rw :
  -(↑(HDiv.hDiv (α := ℕ) (↑n.pred' : ℕ) (↑(Num.pos d) : ℕ) + 1) : ℤ) =
    -HAdd.hAdd (α := ℤ) (↑(↑n.pred' : ℕ) : ℤ) 1 / HAdd.hAdd (α := ℤ) (↑(↑d.pred' : ℕ) : ℤ) 1
⊢ -(↑(n.pred' / Num.pos d).succ' : ℤ) = HDiv.hDiv (α := ℤ) (-(↑n : ℤ)) (↑d : ℤ)

Tactic:
rw [n.to_int_eq_succ_pred, d.to_int_eq_succ_pred, ← PosNum.to_nat_to_int, Num.succ'_to_nat,
        Num.div_to_nat]

Premises used: Num.div_to_nat, Num.succ'_to_nat, PosNum.to_int_eq_succ_pred, PosNum.to_nat_to_int