awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
bit1₄ : 2 * ((↑r : ℕ) + 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₅ : HMul.hMul (α := ℕ) 2 (↑n : ℕ) + 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
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 : ℕ)
have 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 : ℕ)
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₁.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 : ℕ)
have 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 : ℕ)
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₁.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 : ℕ)
have 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 : ℕ)
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.bit0).2 : ℕ) + HMul.hMul (α := ℕ) (↑d : ℕ) (↑(d.divModAux q r.bit0).1 : ℕ) = (↑n.bit0 : ℕ) ∧
    LT.lt (α := ℕ) (↑(d.divModAux q r.bit0).2 : ℕ) (↑d : ℕ)
have bit0 : (↑r.bit0 : ℕ) + (↑d : ℕ) * HAdd.hAdd (α := ℕ) (↑q : ℕ) (↑q : ℕ) = (↑n.bit0 : ℕ)
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 : ℕ)
bit0 : (↑r.bit0 : ℕ) + (↑d : ℕ) * HAdd.hAdd (α := ℕ) (↑q : ℕ) (↑q : ℕ) = (↑n.bit0 : ℕ)
⊢ (↑(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 : ℕ)
have bit0₁ : (↑r.bit0 : ℕ) < 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.bit0 : ℕ) + (↑d : ℕ) * HAdd.hAdd (α := ℕ) (↑q : ℕ) (↑q : ℕ) = (↑n.bit0 : ℕ)
have bit0 : HMul.hMul (α := ℕ) 2 (↑r : ℕ) + (↑d : ℕ) * HAdd.hAdd (α := ℕ) (↑q : ℕ) (↑q : ℕ) = HAdd.hAdd (α := ℕ) (↑n : ℕ) (↑n : ℕ)
Tactic: simp only [Num.cast_bit0, cast_bit0]
-- 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 : ℕ) + (↑d : ℕ) * HAdd.hAdd (α := ℕ) (↑q : ℕ) (↑q : ℕ) = HAdd.hAdd (α := ℕ) (↑n : ℕ) (↑n : ℕ)
have bit0 : HMul.hMul (α := ℕ) 2 (↑r : ℕ) + (↑d : ℕ) * HMul.hMul (α := ℕ) 2 (↑q : ℕ) = HAdd.hAdd (α := ℕ) (↑n : ℕ) (↑n : ℕ)
Tactic: rw [← two_mul, ← two_mul, 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 : ℕ)
bit0 : HMul.hMul (α := ℕ) 2 (↑r : ℕ) + (↑d : ℕ) * HMul.hMul (α := ℕ) 2 (↑q : ℕ) = HAdd.hAdd (α := ℕ) (↑n : ℕ) (↑n : ℕ)
⊢ HMul.hMul (α := ℕ) 2 (↑r : ℕ) + (↑d : ℕ) * HAdd.hAdd (α := ℕ) (↑q : ℕ) (↑q : ℕ) = HAdd.hAdd (α := ℕ) (↑n : ℕ) (↑n : ℕ)
have bit0₁ : HMul.hMul (α := ℕ) 2 (↑r : ℕ) + (↑d : ℕ) * HMul.hMul (α := ℕ) 2 (↑q : ℕ) = HMul.hMul (α := ℕ) 2 (↑n : ℕ)
Tactic: rw [← two_mul, ← two_mul, 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 : ℕ)
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 : ℕ)
⊢ HMul.hMul (α := ℕ) 2 (↑r : ℕ) + (↑d : ℕ) * HAdd.hAdd (α := ℕ) (↑q : ℕ) (↑q : ℕ) = HAdd.hAdd (α := ℕ) (↑n : ℕ) (↑n : ℕ)
have bit0₂ : HMul.hMul (α := ℕ) 2 (↑r : ℕ) + 2 * HMul.hMul (α := ℕ) (↑d : ℕ) (↑q : ℕ) = HMul.hMul (α := ℕ) 2 (↑n : ℕ)
Tactic: rw [← two_mul, ← two_mul, 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 : ℕ)
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 : ℕ)
⊢ HMul.hMul (α := ℕ) 2 (↑r : ℕ) + (↑d : ℕ) * HAdd.hAdd (α := ℕ) (↑q : ℕ) (↑q : ℕ) = HAdd.hAdd (α := ℕ) (↑n : ℕ) (↑n : ℕ)
have bit0₃ : 2 * ((↑r : ℕ) + HMul.hMul (α := ℕ) (↑d : ℕ) (↑q : ℕ)) = HMul.hMul (α := ℕ) 2 (↑n : ℕ)
Tactic: rw [← two_mul, ← two_mul, 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 : ℕ)
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 : ℕ)
⊢ HMul.hMul (α := ℕ) 2 (↑r : ℕ) + (↑d : ℕ) * HAdd.hAdd (α := ℕ) (↑q : ℕ) (↑q : ℕ) = HAdd.hAdd (α := ℕ) (↑n : ℕ) (↑n : ℕ)
have bit0₄ : 2 * ((↑r : ℕ) + HMul.hMul (α := ℕ) (↑d : ℕ) (↑q : ℕ)) = 2 * ((↑r : ℕ) + HMul.hMul (α := ℕ) (↑d : ℕ) (↑q : ℕ))
Tactic: rw [← two_mul, ← two_mul, mul_left_comm, ← mul_add, ← IH.1]
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
d n : PosNum
⊢ (↑(d.divMod n).2 : ℕ) + HMul.hMul (α := ℕ) (↑d : ℕ) (↑(d.divMod n).1 : ℕ) = (↑n : ℕ) ∧
    LT.lt (α := ℕ) (↑(d.divMod n).2 : ℕ) (↑d : ℕ)
have one : (↑(d.divMod one).2 : ℕ) + HMul.hMul (α := ℕ) (↑d : ℕ) (↑(d.divMod one).1 : ℕ) = (↑one : ℕ) ∧
  LT.lt (α := ℕ) (↑(d.divMod one).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
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
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 : ℕ)
⊢ (↑(d.divMod n).2 : ℕ) + HMul.hMul (α := ℕ) (↑d : ℕ) (↑(d.divMod n).1 : ℕ) = (↑n : ℕ) ∧
    LT.lt (α := ℕ) (↑(d.divMod n).2 : ℕ) (↑d : ℕ)
have 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 : ℕ)
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
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
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 : ℕ)
⊢ (↑(d.divMod n).2 : ℕ) + HMul.hMul (α := ℕ) (↑d : ℕ) (↑(d.divMod n).1 : ℕ) = (↑n : ℕ) ∧
    LT.lt (α := ℕ) (↑(d.divMod n).2 : ℕ) (↑d : ℕ)
have 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 : ℕ)
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
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
n : Num
⊢ n.div 0 = 0
have zero : zero.div 0 = 0
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
n : Num
zero : Num.zero.div 0 = 0
⊢ n.div 0 = 0
have pos : ∀ (a : PosNum), (pos a).div 0 = 0
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
n : Num
⊢ n.mod 0 = n
have zero : zero.mod 0 = zero
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
n : Num
zero : Num.zero.mod 0 = Num.zero
⊢ n.mod 0 = n
have pos : ∀ (a : PosNum), (pos a).mod 0 = pos a
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
n : ℕ
a : PosNum
b : Num
ab : pos a ≤ b
h : (pos a * b).natSize ≤ n.succ
⊢ (↑(gcdAux n.succ (pos a) b) : ℕ) = Nat.gcd (↑(pos a) : ℕ) (↑b : ℕ)
have simp : (↑(gcdAux n (b % pos a) (pos a)) : ℕ) = Nat.gcd (↑a : ℕ) (↑b : ℕ)
Tactic: simp only [gcdAux, cast_pos]
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
n : ℕ
a : PosNum
b : Num
ab : pos a ≤ b
h : (pos a * b).natSize ≤ n.succ
⊢ (↑(gcdAux n (b % pos a) (pos a)) : ℕ) = Nat.gcd (↑a : ℕ) (↑b : ℕ)
have rw : (HMod.hMod (α := ℕ) (↑b : ℕ) (↑(pos a) : ℕ)).gcd (↑(pos a) : ℕ) = (HMod.hMod (α := ℕ) (↑b : ℕ) (↑a : ℕ)).gcd (↑a : ℕ)
Tactic: rw [Nat.gcd_rec, gcd_to_nat_aux, mod_to_nat]
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
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 : ℕ)
⊢ (↑(gcdAux n (b % pos a) (pos a)) : ℕ) = Nat.gcd (↑a : ℕ) (↑b : ℕ)
have a₁ : b % pos a ≤ pos a
Tactic: rw [Nat.gcd_rec, gcd_to_nat_aux, mod_to_nat]
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
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
⊢ (↑(gcdAux n (b % pos a) (pos a)) : ℕ) = Nat.gcd (↑a : ℕ) (↑b : ℕ)
have a₂ : (b % pos a * pos a).natSize ≤ n
Tactic: rw [Nat.gcd_rec, gcd_to_nat_aux, mod_to_nat]
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
n : ℕ
a : PosNum
b : Num
ab : pos a ≤ b
h : (pos a * b).natSize ≤ n.succ
⊢ b % pos a ≤ pos a
have a₁ : HMod.hMod (α := ℕ) (↑b : ℕ) (↑(pos a) : ℕ) ≤ (↑(pos a) : ℕ)
Tactic: rw [← le_to_nat, mod_to_nat]
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
n : ℕ
a : PosNum
b : Num
ab : pos a ≤ b
h : (pos a * b).natSize ≤ n.succ
⊢ (b % pos a * pos a).natSize ≤ n
have a₁ : ∀ (h : HMul.hMul (α := ℕ) (↑(pos a) : ℕ) (↑b : ℕ) < HPow.hPow (α := ℕ) 2 n.succ),
  HMul.hMul (α := ℕ) (↑(b % pos a) : ℕ) (↑(pos a) : ℕ) < HPow.hPow (α := ℕ) 2 n
Tactic: rw [natSize_to_nat, mul_to_nat, Nat.size_le] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
n : ℕ
a : PosNum
b : Num
ab : pos a ≤ b
h : HMul.hMul (α := ℕ) (↑(pos a) : ℕ) (↑b : ℕ) < HPow.hPow (α := ℕ) 2 n.succ
⊢ HMul.hMul (α := ℕ) (↑(b % pos a) : ℕ) (↑(pos a) : ℕ) < HPow.hPow (α := ℕ) 2 n
have a₁ : (↑(pos a) : ℕ) * HMod.hMod (α := ℕ) (↑b : ℕ) (↑(pos a) : ℕ) < HPow.hPow (α := ℕ) 2 n
Tactic: rw [mod_to_nat, mul_comm]
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (hypothesis)
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) : ℕ) < HPow.hPow (α := ℕ) 2 n
have h₁ : (↑(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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
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
have a₁ : (↑(pos a) : ℕ) * HMod.hMod (α := ℕ) (↑b : ℕ) (↑(pos a) : ℕ) * 2 ≤
  (↑(pos a) : ℕ) *
    (HMod.hMod (α := ℕ) (↑b : ℕ) (↑(pos a) : ℕ) + (↑(pos a) : ℕ) * HDiv.hDiv (α := ℕ) (↑b : ℕ) (↑(pos a) : ℕ))
Tactic: refine lt_of_mul_lt_mul_right (lt_of_le_of_lt ?_ h) (Nat.zero_le 2)
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
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) : ℕ) * 2 ≤
    (↑(pos a) : ℕ) *
      (HMod.hMod (α := ℕ) (↑b : ℕ) (↑(pos a) : ℕ) + (↑(pos a) : ℕ) * HDiv.hDiv (α := ℕ) (↑b : ℕ) (↑(pos a) : ℕ))
have 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: rw [mul_two, mul_add]
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
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) : ℕ) +
      (↑(pos a) : ℕ) * HMod.hMod (α := ℕ) (↑b : ℕ) (↑(pos a) : ℕ) ≤
    (↑(pos a) : ℕ) * HMod.hMod (α := ℕ) (↑b : ℕ) (↑(pos a) : ℕ) +
      (↑(pos a) : ℕ) * ((↑(pos a) : ℕ) * HDiv.hDiv (α := ℕ) (↑b : ℕ) (↑(pos a) : ℕ))
have a₁ : HMod.hMod (α := ℕ) (↑b : ℕ) (↑(pos a) : ℕ) ≤ (↑(pos a) : ℕ) * HDiv.hDiv (α := ℕ) (↑b : ℕ) (↑(pos a) : ℕ)
Tactic: gcongr _ + _ * ?_
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
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
⊢ HMod.hMod (α := ℕ) (↑b : ℕ) (↑(pos a) : ℕ) ≤ (↑(pos a) : ℕ) * HDiv.hDiv (α := ℕ) (↑b : ℕ) (↑(pos a) : ℕ)
have a₁ : (↑(pos a) : ℕ) ≤ (↑(pos a) : ℕ) * HDiv.hDiv (α := ℕ) (↑(pos a) : ℕ) (↑(pos a) : ℕ)
Tactic: grw [Nat.mod_lt, ← le_to_nat.2 ab]
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
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) : ℕ)
⊢ HMod.hMod (α := ℕ) (↑b : ℕ) (↑(pos a) : ℕ) ≤ (↑(pos a) : ℕ) * HDiv.hDiv (α := ℕ) (↑b : ℕ) (↑(pos a) : ℕ)
have a₂ : LT.lt (α := ℕ) 0 (↑(pos a) : ℕ)
Tactic: grw [Nat.mod_lt, ← le_to_nat.2 ab]
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
a b : Num
⊢ (a * b).natSize ≤ a.natSize + b.natSize
have simp : (HMul.hMul (α := ℕ) (↑a : ℕ) (↑b : ℕ)).size ≤ Nat.size (↑a : ℕ) + Nat.size (↑b : ℕ)
Tactic: simp only [natSize_to_nat, cast_mul]
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
a b : Num
⊢ (HMul.hMul (α := ℕ) (↑a : ℕ) (↑b : ℕ)).size ≤ Nat.size (↑a : ℕ) + Nat.size (↑b : ℕ)
have rw : HMul.hMul (α := ℕ) (↑a : ℕ) (↑b : ℕ) <
  HPow.hPow (α := ℕ) 2 (Nat.size (↑a : ℕ)) * HPow.hPow (α := ℕ) 2 (Nat.size (↑b : ℕ))
Tactic: rw [Nat.size_le, pow_add]
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (hypothesis)
Goal:
⊢ ∀ (a b : Num), (↑(a.gcd b) : ℕ) = Nat.gcd (↑a : ℕ) (↑b : ℕ)
have this : ∀ (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 _)
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
this : ∀ (a b : Num), (a * b).natSize ≤ a.natSize + b.natSize
a b : Num
⊢ (↑(if a ≤ b then gcdAux (a.natSize + b.natSize) a b else gcdAux (b.natSize + a.natSize) b a) : ℕ) =
    Nat.gcd (↑a : ℕ) (↑b : ℕ)
have pos : ∀ (h : a ≤ b), (↑(gcdAux (a.natSize + b.natSize) a b) : ℕ) = Nat.gcd (↑a : ℕ) (↑b : ℕ)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
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 : ℕ)
⊢ (↑(if a ≤ b then gcdAux (a.natSize + b.natSize) a b else gcdAux (b.natSize + a.natSize) b a) : ℕ) =
    Nat.gcd (↑a : ℕ) (↑b : ℕ)
have neg : ∀ (h : ¬a ≤ b), (↑(gcdAux (b.natSize + a.natSize) b a) : ℕ) = Nat.gcd (↑a : ℕ) (↑b : ℕ)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
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 (↑a : ℕ) (↑b : ℕ)
have neg : (↑(gcdAux (b.natSize + a.natSize) b a) : ℕ) = Nat.gcd (↑b : ℕ) (↑a : ℕ)
Tactic: rw [Nat.gcd_comm]
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
m n : Num
⊢ m ∣ n ↔ n % m = 0
have rw : HMod.hMod (α := ℕ) (↑n : ℕ) (↑m : ℕ) = 0 ↔ HMod.hMod (α := ℕ) (↑n : ℕ) (↑m : ℕ) = (↑0 : ℕ)
Tactic: rw [← dvd_to_nat, Nat.dvd_iff_mod_eq_zero, ← to_nat_inj, mod_to_nat]
-- Lean 4 proof step from Mathlib.Data.Num.ZNum (goal)
Goal:
n : ZNum
⊢ n.div 0 = 0
have zero : zero.div 0 = 0
Tactic: cases n
Cleared hypotheses: n