-- Mathlib/Data/Num/Lemmas.lean
theorem divMod_to_nat (d n : PosNum) :
    (n / d : ℕ) = (divMod d n).1 ∧ (n % d : ℕ) = (divMod d n).2

Proof state:
case bit1.mk.h₁
d n : PosNum
q r : Num
IH : ↑r + ↑d * ↑q = ↑n ∧ ↑r < ↑d
⊢ 2 * ↑r + 1 + ↑d * (↑q + ↑q) = ↑n + ↑n + 1

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

Result:
no goals

Proof state:
case bit1
d n : PosNum
IH : ↑(d.divMod n).2 + ↑d * ↑(d.divMod n).1 = ↑n ∧ ↑(d.divMod n).2 < ↑d
⊢ ↑(d.divMod n.bit1).2 + ↑d * ↑(d.divMod n.bit1).1 = ↑n.bit1 ∧ ↑(d.divMod n.bit1).2 < ↑d

Tactic:
unfold divMod

Result:
case bit1
d n : PosNum
IH : ↑(d.divMod n).2 + ↑d * ↑(d.divMod n).1 = ↑n ∧ ↑(d.divMod n).2 < ↑d
⊢ ↑(match d.divMod n with
            | (q, r₁) => d.divModAux q r₁.bit1).2 +
        ↑d *
          ↑(match d.divMod n with
              | (q, r₁) => d.divModAux q r₁.bit1).1 =
      ↑n.bit1 ∧
    ↑(match d.divMod n with
          | (q, r₁) => d.divModAux q r₁.bit1).2 <
      ↑d

Proof state:
d n : PosNum
⊢ ↑(d.divMod n).2 + ↑d * ↑(d.divMod n).1 = ↑n ∧ ↑(d.divMod n).2 < ↑d

Tactic:
induction' n with n IH n IH

Result:
case one
d : PosNum
⊢ ↑(d.divMod one).2 + ↑d * ↑(d.divMod one).1 = ↑one ∧ ↑(d.divMod one).2 < ↑d

case bit1
d n : PosNum
IH : ↑(d.divMod n).2 + ↑d * ↑(d.divMod n).1 = ↑n ∧ ↑(d.divMod n).2 < ↑d
⊢ ↑(d.divMod n.bit1).2 + ↑d * ↑(d.divMod n.bit1).1 = ↑n.bit1 ∧ ↑(d.divMod n.bit1).2 < ↑d

case bit0
d n : PosNum
IH : ↑(d.divMod n).2 + ↑d * ↑(d.divMod n).1 = ↑n ∧ ↑(d.divMod n).2 < ↑d
⊢ ↑(d.divMod n.bit0).2 + ↑d * ↑(d.divMod n.bit0).1 = ↑n.bit0 ∧ ↑(d.divMod n.bit0).2 < ↑d

Proof state:
case bit0.mk.h₂
d n : PosNum
q r : Num
IH : ↑r + ↑d * ↑q = ↑n ∧ ↑r < ↑d
⊢ ↑r.bit0 < 2 * ↑d

Tactic:
simpa using IH.2

Result:
no goals

Proof state:
case one
d : PosNum
⊢ ↑(d.divMod one).2 + ↑d * ↑(d.divMod one).1 = ↑one ∧ ↑(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))

Result:
no goals

Proof state:
case bit1
d n : PosNum
IH : ↑(d.divMod n).2 + ↑d * ↑(d.divMod n).1 = ↑n ∧ ↑(d.divMod n).2 < ↑d
⊢ ↑(match d.divMod n with
            | (q, r₁) => d.divModAux q r₁.bit1).2 +
        ↑d *
          ↑(match d.divMod n with
              | (q, r₁) => d.divModAux q r₁.bit1).1 =
      ↑n.bit1 ∧
    ↑(match d.divMod n with
          | (q, r₁) => d.divModAux q r₁.bit1).2 <
      ↑d

Tactic:
revert IH

Result:
case bit1
d n : PosNum
⊢ ↑(d.divMod n).2 + ↑d * ↑(d.divMod n).1 = ↑n ∧ ↑(d.divMod n).2 < ↑d →
    ↑(match d.divMod n with
              | (q, r₁) => d.divModAux q r₁.bit1).2 +
          ↑d *
            ↑(match d.divMod n with
                | (q, r₁) => d.divModAux q r₁.bit1).1 =
        ↑n.bit1 ∧
      ↑(match d.divMod n with
            | (q, r₁) => d.divModAux q r₁.bit1).2 <
        ↑d

Proof state:
case bit0.mk
d n : PosNum
q r : Num
⊢ ↑(q, r).2 + ↑d * ↑(q, r).1 = ↑n ∧ ↑(q, r).2 < ↑d →
    ↑(match (q, r) with
              | (q, r₁) => d.divModAux q r₁.bit0).2 +
          ↑d *
            ↑(match (q, r) with
                | (q, r₁) => d.divModAux q r₁.bit0).1 =
        ↑n.bit0 ∧
      ↑(match (q, r) with
            | (q, r₁) => d.divModAux q r₁.bit0).2 <
        ↑d

Tactic:
intro IH

Result:
case bit0.mk
d n : PosNum
q r : Num
IH : ↑(q, r).2 + ↑d * ↑(q, r).1 = ↑n ∧ ↑(q, r).2 < ↑d
⊢ ↑(match (q, r) with
            | (q, r₁) => d.divModAux q r₁.bit0).2 +
        ↑d *
          ↑(match (q, r) with
              | (q, r₁) => d.divModAux q r₁.bit0).1 =
      ↑n.bit0 ∧
    ↑(match (q, r) with
          | (q, r₁) => d.divModAux q r₁.bit0).2 <
      ↑d

Proof state:
case bit1
d n : PosNum
⊢ ↑(d.divMod n).2 + ↑d * ↑(d.divMod n).1 = ↑n ∧ ↑(d.divMod n).2 < ↑d →
    ↑(match d.divMod n with
              | (q, r₁) => d.divModAux q r₁.bit1).2 +
          ↑d *
            ↑(match d.divMod n with
                | (q, r₁) => d.divModAux q r₁.bit1).1 =
        ↑n.bit1 ∧
      ↑(match d.divMod n with
            | (q, r₁) => d.divModAux q r₁.bit1).2 <
        ↑d

Tactic:
obtain ⟨q, r⟩ := divMod d n

Result:
case bit1.mk
d n : PosNum
q r : Num
⊢ ↑(q, r).2 + ↑d * ↑(q, r).1 = ↑n ∧ ↑(q, r).2 < ↑d →
    ↑(match (q, r) with
              | (q, r₁) => d.divModAux q r₁.bit1).2 +
          ↑d *
            ↑(match (q, r) with
                | (q, r₁) => d.divModAux q r₁.bit1).1 =
        ↑n.bit1 ∧
      ↑(match (q, r) with
            | (q, r₁) => d.divModAux q r₁.bit1).2 <
        ↑d

Proof state:
case bit1.mk.h₂
d n : PosNum
q r : Num
IH : ↑r + ↑d * ↑q = ↑n ∧ ↑r < ↑d
⊢ 2 * ↑r + 1 < 2 * ↑d

Tactic:
omega

Result:
no goals

Proof state:
d n : PosNum
⊢ ↑n / ↑d = ↑(d.divMod n).1 ∧ ↑n % ↑d = ↑(d.divMod n).2

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

Result:
d n : PosNum
⊢ ↑(d.divMod n).2 + ↑d * ↑(d.divMod n).1 = ↑n ∧ ↑(d.divMod n).2 < ↑d

Proof state:
case bit0.mk
d n : PosNum
q r : Num
IH : ↑r + ↑d * ↑q = ↑n ∧ ↑r < ↑d
⊢ ↑(d.divModAux q r.bit0).2 + ↑d * ↑(d.divModAux q r.bit0).1 = ↑n.bit0 ∧ ↑(d.divModAux q r.bit0).2 < ↑d

Tactic:
apply divMod_to_nat_aux

Result:
case bit0.mk.h₁
d n : PosNum
q r : Num
IH : ↑r + ↑d * ↑q = ↑n ∧ ↑r < ↑d
⊢ ↑r.bit0 + ↑d * (↑q + ↑q) = ↑n.bit0

case bit0.mk.h₂
d n : PosNum
q r : Num
IH : ↑r + ↑d * ↑q = ↑n ∧ ↑r < ↑d
⊢ ↑r.bit0 < 2 * ↑d

Proof state:
case bit0.mk.h₁
d n : PosNum
q r : Num
IH : ↑r + ↑d * ↑q = ↑n ∧ ↑r < ↑d
⊢ 2 * ↑r + ↑d * (↑q + ↑q) = ↑n + ↑n

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

Result:
no goals

Proof state:
case bit0
d n : PosNum
IH : ↑(d.divMod n).2 + ↑d * ↑(d.divMod n).1 = ↑n ∧ ↑(d.divMod n).2 < ↑d
⊢ ↑(match d.divMod n with
            | (q, r₁) => d.divModAux q r₁.bit0).2 +
        ↑d *
          ↑(match d.divMod n with
              | (q, r₁) => d.divModAux q r₁.bit0).1 =
      ↑n.bit0 ∧
    ↑(match d.divMod n with
          | (q, r₁) => d.divModAux q r₁.bit0).2 <
      ↑d

Tactic:
revert IH

Result:
case bit0
d n : PosNum
⊢ ↑(d.divMod n).2 + ↑d * ↑(d.divMod n).1 = ↑n ∧ ↑(d.divMod n).2 < ↑d →
    ↑(match d.divMod n with
              | (q, r₁) => d.divModAux q r₁.bit0).2 +
          ↑d *
            ↑(match d.divMod n with
                | (q, r₁) => d.divModAux q r₁.bit0).1 =
        ↑n.bit0 ∧
      ↑(match d.divMod n with
            | (q, r₁) => d.divModAux q r₁.bit0).2 <
        ↑d

Proof state:
case bit0
d n : PosNum
IH : ↑(d.divMod n).2 + ↑d * ↑(d.divMod n).1 = ↑n ∧ ↑(d.divMod n).2 < ↑d
⊢ ↑(d.divMod n.bit0).2 + ↑d * ↑(d.divMod n.bit0).1 = ↑n.bit0 ∧ ↑(d.divMod n.bit0).2 < ↑d

Tactic:
unfold divMod

Result:
case bit0
d n : PosNum
IH : ↑(d.divMod n).2 + ↑d * ↑(d.divMod n).1 = ↑n ∧ ↑(d.divMod n).2 < ↑d
⊢ ↑(match d.divMod n with
            | (q, r₁) => d.divModAux q r₁.bit0).2 +
        ↑d *
          ↑(match d.divMod n with
              | (q, r₁) => d.divModAux q r₁.bit0).1 =
      ↑n.bit0 ∧
    ↑(match d.divMod n with
          | (q, r₁) => d.divModAux q r₁.bit0).2 <
      ↑d

Proof state:
d : PosNum
⊢ ↑1 + ↑d * (↑0 + ↑0) = ↑one

Tactic:
simp

Result:
no goals

Proof state:
case bit0.mk
d n : PosNum
q r : Num
IH : ↑(q, r).2 + ↑d * ↑(q, r).1 = ↑n ∧ ↑(q, r).2 < ↑d
⊢ ↑(match (q, r) with
            | (q, r₁) => d.divModAux q r₁.bit0).2 +
        ↑d *
          ↑(match (q, r) with
              | (q, r₁) => d.divModAux q r₁.bit0).1 =
      ↑n.bit0 ∧
    ↑(match (q, r) with
          | (q, r₁) => d.divModAux q r₁.bit0).2 <
      ↑d

Tactic:
simp only [divMod] at IH ⊢

Result:
case bit0.mk
d n : PosNum
q r : Num
IH : ↑r + ↑d * ↑q = ↑n ∧ ↑r < ↑d
⊢ ↑(d.divModAux q r.bit0).2 + ↑d * ↑(d.divModAux q r.bit0).1 = ↑n.bit0 ∧ ↑(d.divModAux q r.bit0).2 < ↑d

Proof state:
case bit0.mk.h₁
d n : PosNum
q r : Num
IH : ↑r + ↑d * ↑q = ↑n ∧ ↑r < ↑d
⊢ ↑r.bit0 + ↑d * (↑q + ↑q) = ↑n.bit0

Tactic:
simp only [Num.cast_bit0, cast_bit0]

Result:
case bit0.mk.h₁
d n : PosNum
q r : Num
IH : ↑r + ↑d * ↑q = ↑n ∧ ↑r < ↑d
⊢ 2 * ↑r + ↑d * (↑q + ↑q) = ↑n + ↑n