-- Mathlib/Data/Num/Lemmas.lean
theorem divMod_to_nat_aux {n d : PosNum} {q r : Num} (h₁ : (r : ℕ) + d * ((q : ℕ) + q) = n)
    (h₂ : (r : ℕ) < 2 * d) :
    ((divModAux d q r).2 + d * (divModAux d q r).1 : ℕ) = ↑n ∧ ((divModAux d q r).2 : ℕ) < d

Proof state:
case some
n d : PosNum
q r : Num
h₁ : ↑r + ↑d * (↑q + ↑q) = ↑n
h₂ : ↑r < 2 * ↑d
this✝ : ∀ {r₂ : Num}, Num.ofZNum' (r.sub' (Num.pos d)) = some r₂ ↔ ↑r = ↑r₂ + ↑d
r₂ : Num
e : Num.ofZNum' (r.sub' (Num.pos d)) = some r₂
this : ↑r = ↑r₂ + ↑d
⊢ ↑r₂ + ↑d * (2 * ↑q + 1) = ↑n ∧ ↑r₂ < ↑d

Tactic:
constructor

Result:
case some.left
n d : PosNum
q r : Num
h₁ : ↑r + ↑d * (↑q + ↑q) = ↑n
h₂ : ↑r < 2 * ↑d
this✝ : ∀ {r₂ : Num}, Num.ofZNum' (r.sub' (Num.pos d)) = some r₂ ↔ ↑r = ↑r₂ + ↑d
r₂ : Num
e : Num.ofZNum' (r.sub' (Num.pos d)) = some r₂
this : ↑r = ↑r₂ + ↑d
⊢ ↑r₂ + ↑d * (2 * ↑q + 1) = ↑n

case some.right
n d : PosNum
q r : Num
h₁ : ↑r + ↑d * (↑q + ↑q) = ↑n
h₂ : ↑r < 2 * ↑d
this✝ : ∀ {r₂ : Num}, Num.ofZNum' (r.sub' (Num.pos d)) = some r₂ ↔ ↑r = ↑r₂ + ↑d
r₂ : Num
e : Num.ofZNum' (r.sub' (Num.pos d)) = some r₂
this : ↑r = ↑r₂ + ↑d
⊢ ↑r₂ < ↑d

Proof state:
case none.intro
n d : PosNum
q r : Num
h₁ : ↑r + ↑d * (↑q + ↑q) = ↑n
h₂ : ↑r < 2 * ↑d
this : ∀ {r₂ : Num}, Num.ofZNum' (r.sub' (Num.pos d)) = some r₂ ↔ ↑r = ↑r₂ + ↑d
e : Num.ofZNum' (r.sub' (Num.pos d)) = none
h :
  ↑(match none with
        | some r' => (q.bit1, r')
        | none => (q.bit0, r)).2 ≥
    ↑d
r₂ : ℕ
e' :
  ↑d + r₂ =
    ↑(match none with
        | some r' => (q.bit1, r')
        | none => (q.bit0, r)).2
⊢ False

Tactic:
rw [← Num.to_of_nat r₂, add_comm] at e'

Result:
case none.intro
n d : PosNum
q r : Num
h₁ : ↑r + ↑d * (↑q + ↑q) = ↑n
h₂ : ↑r < 2 * ↑d
this : ∀ {r₂ : Num}, Num.ofZNum' (r.sub' (Num.pos d)) = some r₂ ↔ ↑r = ↑r₂ + ↑d
e : Num.ofZNum' (r.sub' (Num.pos d)) = none
h :
  ↑(match none with
        | some r' => (q.bit1, r')
        | none => (q.bit0, r)).2 ≥
    ↑d
r₂ : ℕ
e' :
  ↑↑r₂ + ↑d =
    ↑(match none with
        | some r' => (q.bit1, r')
        | none => (q.bit0, r)).2
⊢ False

Proof state:
case none
n d : PosNum
q r : Num
h₁ : ↑r + ↑d * (↑q + ↑q) = ↑n
h₂ : ↑r < 2 * ↑d
this : ∀ {r₂ : Num}, Num.ofZNum' (r.sub' (Num.pos d)) = some r₂ ↔ ↑r = ↑r₂ + ↑d
e : Num.ofZNum' (r.sub' (Num.pos d)) = none
⊢ ↑(match none with
            | some r' => (q.bit1, r')
            | none => (q.bit0, r)).2 +
        ↑d *
          ↑(match none with
              | some r' => (q.bit1, r')
              | none => (q.bit0, r)).1 =
      ↑n ∧
    ↑(match none with
          | some r' => (q.bit1, r')
          | none => (q.bit0, r)).2 <
      ↑d

Tactic:
rw [Num.cast_bit0, two_mul]

Result:
case none
n d : PosNum
q r : Num
h₁ : ↑r + ↑d * (↑q + ↑q) = ↑n
h₂ : ↑r < 2 * ↑d
this : ∀ {r₂ : Num}, Num.ofZNum' (r.sub' (Num.pos d)) = some r₂ ↔ ↑r = ↑r₂ + ↑d
e : Num.ofZNum' (r.sub' (Num.pos d)) = none
⊢ ↑(match none with
            | some r' => (q.bit1, r')
            | none => (q.bit0, r)).2 +
        ↑d * (↑q + ↑q) =
      ↑n ∧
    ↑(match none with
          | some r' => (q.bit1, r')
          | none => (q.bit0, r)).2 <
      ↑d

Proof state:
n d : PosNum
q r : Num
h₁ : ↑r + ↑d * (↑q + ↑q) = ↑n
h₂ : ↑r < 2 * ↑d
r₂ : Num
⊢ ↑r = ↑r₂ + ↑(Num.pos d) ↔ ↑↑r = ↑(↑r₂ + ↑d)

Tactic:
simp

Result:
no goals

Proof state:
n d : PosNum
q r : Num
h₁ : ↑r + ↑d * (↑q + ↑q) = ↑n
h₂ : ↑r < 2 * ↑d
this : ∀ {r₂ : Num}, Num.ofZNum' (r.sub' (Num.pos d)) = some r₂ ↔ ↑r = ↑r₂ + ↑d
⊢ ↑(match Num.ofZNum' (r.sub' (Num.pos d)) with
            | some r' => (q.bit1, r')
            | none => (q.bit0, r)).2 +
        ↑d *
          ↑(match Num.ofZNum' (r.sub' (Num.pos d)) with
              | some r' => (q.bit1, r')
              | none => (q.bit0, r)).1 =
      ↑n ∧
    ↑(match Num.ofZNum' (r.sub' (Num.pos d)) with
          | some r' => (q.bit1, r')
          | none => (q.bit0, r)).2 <
      ↑d

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

Result:
case none
n d : PosNum
q r : Num
h₁ : ↑r + ↑d * (↑q + ↑q) = ↑n
h₂ : ↑r < 2 * ↑d
this : ∀ {r₂ : Num}, Num.ofZNum' (r.sub' (Num.pos d)) = some r₂ ↔ ↑r = ↑r₂ + ↑d
e : Num.ofZNum' (r.sub' (Num.pos d)) = none
⊢ ↑(match none with
            | some r' => (q.bit1, r')
            | none => (q.bit0, r)).2 +
        ↑d *
          ↑(match none with
              | some r' => (q.bit1, r')
              | none => (q.bit0, r)).1 =
      ↑n ∧
    ↑(match none with
          | some r' => (q.bit1, r')
          | none => (q.bit0, r)).2 <
      ↑d

case some
n d : PosNum
q r : Num
h₁ : ↑r + ↑d * (↑q + ↑q) = ↑n
h₂ : ↑r < 2 * ↑d
this : ∀ {r₂ : Num}, Num.ofZNum' (r.sub' (Num.pos d)) = some r₂ ↔ ↑r = ↑r₂ + ↑d
r₂ : Num
e : Num.ofZNum' (r.sub' (Num.pos d)) = some r₂
⊢ ↑(match some r₂ with
            | some r' => (q.bit1, r')
            | none => (q.bit0, r)).2 +
        ↑d *
          ↑(match some r₂ with
              | some r' => (q.bit1, r')
              | none => (q.bit0, r)).1 =
      ↑n ∧
    ↑(match some r₂ with
          | some r' => (q.bit1, r')
          | none => (q.bit0, r)).2 <
      ↑d

Proof state:
case some.right
n d : PosNum
q r : Num
h₁ : ↑r + ↑d * (↑q + ↑q) = ↑n
h₂ : ↑r < 2 * ↑d
this✝ : ∀ {r₂ : Num}, Num.ofZNum' (r.sub' (Num.pos d)) = some r₂ ↔ ↑r = ↑r₂ + ↑d
r₂ : Num
e : Num.ofZNum' (r.sub' (Num.pos d)) = some r₂
this : ↑r = ↑r₂ + ↑d
⊢ ↑r₂ < ↑d

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

Result:
no goals

Proof state:
n d : PosNum
q r : Num
h₁ : ↑r + ↑d * (↑q + ↑q) = ↑n
h₂ : ↑r < 2 * ↑d
⊢ ↑(d.divModAux q r).2 + ↑d * ↑(d.divModAux q r).1 = ↑n ∧ ↑(d.divModAux q r).2 < ↑d

Tactic:
unfold divModAux

Result:
n d : PosNum
q r : Num
h₁ : ↑r + ↑d * (↑q + ↑q) = ↑n
h₂ : ↑r < 2 * ↑d
⊢ ↑(match Num.ofZNum' (r.sub' (Num.pos d)) with
            | some r' => (q.bit1, r')
            | none => (q.bit0, r)).2 +
        ↑d *
          ↑(match Num.ofZNum' (r.sub' (Num.pos d)) with
              | some r' => (q.bit1, r')
              | none => (q.bit0, r)).1 =
      ↑n ∧
    ↑(match Num.ofZNum' (r.sub' (Num.pos d)) with
          | some r' => (q.bit1, r')
          | none => (q.bit0, r)).2 <
      ↑d

Proof state:
case some
n d : PosNum
q r : Num
h₁ : ↑r + ↑d * (↑q + ↑q) = ↑n
h₂ : ↑r < 2 * ↑d
this✝ : ∀ {r₂ : Num}, Num.ofZNum' (r.sub' (Num.pos d)) = some r₂ ↔ ↑r = ↑r₂ + ↑d
r₂ : Num
e : Num.ofZNum' (r.sub' (Num.pos d)) = some r₂
this : ↑r = ↑r₂ + ↑d
⊢ ↑(match some r₂ with
            | some r' => (q.bit1, r')
            | none => (q.bit0, r)).2 +
        ↑d *
          ↑(match some r₂ with
              | some r' => (q.bit1, r')
              | none => (q.bit0, r)).1 =
      ↑n ∧
    ↑(match some r₂ with
          | some r' => (q.bit1, r')
          | none => (q.bit0, r)).2 <
      ↑d

Tactic:
simp only [Num.cast_bit1]

Result:
case some
n d : PosNum
q r : Num
h₁ : ↑r + ↑d * (↑q + ↑q) = ↑n
h₂ : ↑r < 2 * ↑d
this✝ : ∀ {r₂ : Num}, Num.ofZNum' (r.sub' (Num.pos d)) = some r₂ ↔ ↑r = ↑r₂ + ↑d
r₂ : Num
e : Num.ofZNum' (r.sub' (Num.pos d)) = some r₂
this : ↑r = ↑r₂ + ↑d
⊢ ↑r₂ + ↑d * (2 * ↑q + 1) = ↑n ∧ ↑r₂ < ↑d

Proof state:
n d : PosNum
q r : Num
h₁ : ↑r + ↑d * (↑q + ↑q) = ↑n
h₂ : ↑r < 2 * ↑d
⊢ ∀ {r₂ : Num}, Num.ofZNum' (r.sub' (Num.pos d)) = some r₂ ↔ ↑r = ↑r₂ + ↑d

Tactic:
intro r₂

Result:
n d : PosNum
q r : Num
h₁ : ↑r + ↑d * (↑q + ↑q) = ↑n
h₂ : ↑r < 2 * ↑d
r₂ : Num
⊢ Num.ofZNum' (r.sub' (Num.pos d)) = some r₂ ↔ ↑r = ↑r₂ + ↑d

Proof state:
n d : PosNum
q r : Num
h₁ : ↑r + ↑d * (↑q + ↑q) = ↑n
h₂ : ↑r < 2 * ↑d
r₂ : Num
⊢ r.sub' (Num.pos d) = r₂.toZNum ↔ ↑r = ↑r₂ + ↑d

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

Result:
n d : PosNum
q r : Num
h₁ : ↑r + ↑d * (↑q + ↑q) = ↑n
h₂ : ↑r < 2 * ↑d
r₂ : Num
⊢ ↑r = ↑r₂ + ↑(Num.pos d) ↔ ↑↑r = ↑(↑r₂ + ↑d)