-- Mathlib/Computability/Primrec.lean
theorem nat_div : Primrec₂ ((· / ·) : ℕ → ℕ → ℕ)

Proof state:
this : PrimrecRel fun a b => a.2 = 0 ∧ b = 0 ∨ 0 < a.2 ∧ b * a.2 ≤ a.1 ∧ a.1 < (b + 1) * a.2
a k q : ℕ
H : ¬k = 0
⊢ q * k ≤ a ∧ a < (q + 1) * k ↔ q = a / k

Tactic:
rw [le_antisymm_iff, ← (@Nat.lt_succ _ q), Nat.le_div_iff_mul_le (Nat.pos_of_ne_zero H),
    Nat.div_lt_iff_lt_mul (Nat.pos_of_ne_zero H)]

Result:
no goals

Proof state:
this : PrimrecRel fun a b => a.2 = 0 ∧ b = 0 ∨ 0 < a.2 ∧ b * a.2 ≤ a.1 ∧ a.1 < (b + 1) * a.2
a k q : ℕ
H : ¬k = 0
⊢ (a, k).2 = 0 ∧ q = 0 ∨ 0 < (a, k).2 ∧ q * (a, k).2 ≤ (a, k).1 ∧ (a, k).1 < (q + 1) * (a, k).2 ↔
    (fun x1 x2 => x1 / x2) (a, k).1 (a, k).2 = q

Tactic:
have : q * k ≤ a ∧ a < (q + 1) * k ↔ q = a / k := by
  rw [le_antisymm_iff, ← (@Nat.lt_succ _ q), Nat.le_div_iff_mul_le (Nat.pos_of_ne_zero H),
      Nat.div_lt_iff_lt_mul (Nat.pos_of_ne_zero H)]

Result:
this✝ : PrimrecRel fun a b => a.2 = 0 ∧ b = 0 ∨ 0 < a.2 ∧ b * a.2 ≤ a.1 ∧ a.1 < (b + 1) * a.2
a k q : ℕ
H : ¬k = 0
this : q * k ≤ a ∧ a < (q + 1) * k ↔ q = a / k
⊢ (a, k).2 = 0 ∧ q = 0 ∨ 0 < (a, k).2 ∧ q * (a, k).2 ≤ (a, k).1 ∧ (a, k).1 < (q + 1) * (a, k).2 ↔
    (fun x1 x2 => x1 / x2) (a, k).1 (a, k).2 = q

Proof state:
this : PrimrecRel fun a b => a.2 = 0 ∧ b = 0 ∨ 0 < a.2 ∧ b * a.2 ≤ a.1 ∧ a.1 < (b + 1) * a.2
⊢ ∀ (a : ℕ × ℕ) (b : ℕ),
    a.2 = 0 ∧ b = 0 ∨ 0 < a.2 ∧ b * a.2 ≤ a.1 ∧ a.1 < (b + 1) * a.2 ↔ (fun x1 x2 => x1 / x2) a.1 a.2 = b

Tactic:
rintro ⟨a, k⟩ q

Result:
case mk
this : PrimrecRel fun a b => a.2 = 0 ∧ b = 0 ∨ 0 < a.2 ∧ b * a.2 ≤ a.1 ∧ a.1 < (b + 1) * a.2
a k q : ℕ
⊢ (a, k).2 = 0 ∧ q = 0 ∨ 0 < (a, k).2 ∧ q * (a, k).2 ≤ (a, k).1 ∧ (a, k).1 < (q + 1) * (a, k).2 ↔
    (fun x1 x2 => x1 / x2) (a, k).1 (a, k).2 = q

Proof state:
this : PrimrecRel fun a b => a.2 = 0 ∧ b = 0 ∨ 0 < a.2 ∧ b * a.2 ≤ a.1 ∧ a.1 < (b + 1) * a.2
⊢ PrimrecRel fun a b => (fun x1 x2 => x1 / x2) a.1 a.2 = b

Tactic:
refine this.of_eq ?_

Result:
this : PrimrecRel fun a b => a.2 = 0 ∧ b = 0 ∨ 0 < a.2 ∧ b * a.2 ≤ a.1 ∧ a.1 < (b + 1) * a.2
⊢ ∀ (a : ℕ × ℕ) (b : ℕ),
    a.2 = 0 ∧ b = 0 ∨ 0 < a.2 ∧ b * a.2 ≤ a.1 ∧ a.1 < (b + 1) * a.2 ↔ (fun x1 x2 => x1 / x2) a.1 a.2 = b

Proof state:
case mk
this : PrimrecRel fun a b => a.2 = 0 ∧ b = 0 ∨ 0 < a.2 ∧ b * a.2 ≤ a.1 ∧ a.1 < (b + 1) * a.2
a k q : ℕ
⊢ (a, k).2 = 0 ∧ q = 0 ∨ 0 < (a, k).2 ∧ q * (a, k).2 ≤ (a, k).1 ∧ (a, k).1 < (q + 1) * (a, k).2 ↔
    (fun x1 x2 => x1 / x2) (a, k).1 (a, k).2 = q

Tactic:
if H : k = 0 then simp [H, eq_comm]
else
  have : q * k ≤ a ∧ a < (q + 1) * k ↔ q = a / k := by
    rw [le_antisymm_iff, ← (@Nat.lt_succ _ q), Nat.le_div_iff_mul_le (Nat.pos_of_ne_zero H),
        Nat.div_lt_iff_lt_mul (Nat.pos_of_ne_zero H)]
  simpa [H, zero_lt_iff, eq_comm (b := q)]

Result:
no goals

Proof state:
this : PrimrecRel fun a b => a.2 = 0 ∧ b = 0 ∨ 0 < a.2 ∧ b * a.2 ≤ a.1 ∧ a.1 < (b + 1) * a.2
a k q : ℕ
H : k = 0
⊢ (a, k).2 = 0 ∧ q = 0 ∨ 0 < (a, k).2 ∧ q * (a, k).2 ≤ (a, k).1 ∧ (a, k).1 < (q + 1) * (a, k).2 ↔
    (fun x1 x2 => x1 / x2) (a, k).1 (a, k).2 = q

Tactic:
simp [H, eq_comm]

Result:
no goals

Proof state:
this✝ : PrimrecRel fun a b => a.2 = 0 ∧ b = 0 ∨ 0 < a.2 ∧ b * a.2 ≤ a.1 ∧ a.1 < (b + 1) * a.2
a k q : ℕ
H : ¬k = 0
this : q * k ≤ a ∧ a < (q + 1) * k ↔ q = a / k
⊢ (a, k).2 = 0 ∧ q = 0 ∨ 0 < (a, k).2 ∧ q * (a, k).2 ≤ (a, k).1 ∧ (a, k).1 < (q + 1) * (a, k).2 ↔
    (fun x1 x2 => x1 / x2) (a, k).1 (a, k).2 = q

Tactic:
simpa [H, zero_lt_iff, eq_comm (b := q)]

Result:
no goals

Proof state:
⊢ Primrec₂ fun x1 x2 => x1 / x2

Tactic:
refine of_graph ⟨_, fst, fun p => Nat.div_le_self _ _⟩ ?_

Result:
⊢ PrimrecRel fun a b => (fun x1 x2 => x1 / x2) a.1 a.2 = b

Proof state:
⊢ PrimrecRel fun a b => (fun x1 x2 => x1 / x2) a.1 a.2 = b

Tactic:
have : PrimrecRel fun (a : ℕ × ℕ) (b : ℕ) => (a.2 = 0 ∧ b = 0) ∨
    (0 < a.2 ∧ b * a.2 ≤ a.1 ∧ a.1 < (b + 1) * a.2) :=
  PrimrecPred.or
    (.and (const 0 |> Primrec.eq.comp (fst |> snd.comp)) (const 0 |> Primrec.eq.comp snd))
    (.and (nat_lt.comp (const 0) (fst |> snd.comp)) <|
        .and (nat_le.comp (nat_mul.comp snd (fst |> snd.comp)) (fst |> fst.comp))
        (nat_lt.comp (fst.comp fst) (nat_mul.comp (Primrec.succ.comp snd) (snd.comp fst))))

Result:
this : PrimrecRel fun a b => a.2 = 0 ∧ b = 0 ∨ 0 < a.2 ∧ b * a.2 ≤ a.1 ∧ a.1 < (b + 1) * a.2
⊢ PrimrecRel fun a b => (fun x1 x2 => x1 / x2) a.1 a.2 = b