awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Computability.PartrecCode
Goal:
cf : Code
hf : ∀ {n x : ℕ} (h : x ∈ cf.eval n), ∃ (k : ℕ), x ∈ evaln (k + 1) cf n
n y : ℕ
IH :
  ∀ (m : ℕ) (hy₁ : 0 ∈ cf.eval (Nat.pair (unpair n).1 (y + m)))
    (hy₂ : ∀ {m_1 : ℕ}, m_1 < y → ∃ a ∈ cf.eval (Nat.pair (unpair n).1 (m_1 + m)), ¬a = 0),
    ∃ (k : ℕ), y + m ∈ evaln (k + 1) cf.rfind' (Nat.pair (unpair n).1 m)
m : ℕ
hy₁ : 0 ∈ cf.eval (Nat.pair (unpair n).1 (y + 1 + m))
hy₂ : ∀ {m_1 : ℕ}, m_1 < y + 1 → ∃ a ∈ cf.eval (Nat.pair (unpair n).1 (m_1 + m)), ¬a = 0
a : ℕ
ha : a ∈ cf.eval (Nat.pair (unpair n).1 (0 + m))
a0 : ¬a = 0
k₁ : ℕ
hk₁ : a ∈ evaln (k₁ + 1) cf (Nat.pair (unpair n).1 (0 + m))
rfind' :
  ∀ (k₂ : ℕ) (hk₂ : y + m.succ ∈ evaln (k₂ + 1) cf.rfind' (Nat.pair (unpair n).1 m.succ)),
    ∃ (k : ℕ),
      Nat.pair (unpair n).1 m ≤ k ∧
        ∃ (a : ℕ),
          evaln (k + 1) cf (Nat.pair (unpair n).1 m) = some a ∧
            (if a = 0 then some m else evaln k cf.rfind' (Nat.pair (unpair n).1 (m + 1))) = some (y + 1 + m)
⊢ ∃ (k : ℕ),
    Nat.pair (unpair n).1 m ≤ k ∧
      ∃ (a : ℕ),
        evaln (k + 1) cf (Nat.pair (unpair n).1 m) = some a ∧
          (if a = 0 then some m else evaln k cf.rfind' (Nat.pair (unpair n).1 (m + 1))) = some (y + 1 + m)

Tactic:
rcases IH m.succ (by simpa [Nat.succ_eq_add_one, add_comm, add_left_comm] using hy₁)
          fun {i} hi => by
          simpa [Nat.succ_eq_add_one, add_comm, add_left_comm] using
            hy₂ (Nat.succ_lt_succ hi) with
        ⟨k₂, hk₂⟩

Premises used: Nat.succ
-- Module: Mathlib.Computability.PartrecCode
Goal:
cf : Code
hf : ∀ {n x : ℕ} (h : x ∈ cf.eval n), ∃ (k : ℕ), x ∈ evaln (k + 1) cf n
n y : ℕ
IH :
  ∀ (m : ℕ) (hy₁ : 0 ∈ cf.eval (Nat.pair (unpair n).1 (y + m)))
    (hy₂ : ∀ {m_1 : ℕ}, m_1 < y → ∃ a ∈ cf.eval (Nat.pair (unpair n).1 (m_1 + m)), ¬a = 0),
    ∃ (k : ℕ), y + m ∈ evaln (k + 1) cf.rfind' (Nat.pair (unpair n).1 m)
m : ℕ
hy₁ : 0 ∈ cf.eval (Nat.pair (unpair n).1 (y + 1 + m))
hy₂ : ∀ {m_1 : ℕ}, m_1 < y + 1 → ∃ a ∈ cf.eval (Nat.pair (unpair n).1 (m_1 + m)), ¬a = 0
a : ℕ
ha : a ∈ cf.eval (Nat.pair (unpair n).1 (0 + m))
a0 : ¬a = 0
k₁ : ℕ
hk₁ : a ∈ evaln (k₁ + 1) cf (Nat.pair (unpair n).1 (0 + m))
k₂ : ℕ
hk₂ : y + m.succ ∈ evaln (k₂ + 1) cf.rfind' (Nat.pair (unpair n).1 m.succ)
h :
  Nat.pair (unpair n).1 m ≤ (max k₁ k₂).succ ∧
    ∃ (a : ℕ),
      evaln ((max k₁ k₂).succ + 1) cf (Nat.pair (unpair n).1 m) = some a ∧
        (if a = 0 then some m else evaln (max k₁ k₂).succ cf.rfind' (Nat.pair (unpair n).1 (m + 1))) = some (y + 1 + m)
⊢ ∃ (k : ℕ),
    Nat.pair (unpair n).1 m ≤ k ∧
      ∃ (a : ℕ),
        evaln (k + 1) cf (Nat.pair (unpair n).1 m) = some a ∧
          (if a = 0 then some m else evaln k cf.rfind' (Nat.pair (unpair n).1 (m + 1))) = some (y + 1 + m)

Tactic:
use (max k₁ k₂).succ

Premises used: Max.max, Nat.succ
-- Module: Mathlib.Computability.PartrecCode
Goal:
cf : Code
hf : ∀ {n x : ℕ} (h : x ∈ cf.eval n), ∃ (k : ℕ), x ∈ evaln (k + 1) cf n
n y : ℕ
IH :
  ∀ (m : ℕ) (hy₁ : 0 ∈ cf.eval (Nat.pair (unpair n).1 (y + m)))
    (hy₂ : ∀ {m_1 : ℕ}, m_1 < y → ∃ a ∈ cf.eval (Nat.pair (unpair n).1 (m_1 + m)), ¬a = 0),
    ∃ (k : ℕ), y + m ∈ evaln (k + 1) cf.rfind' (Nat.pair (unpair n).1 m)
m : ℕ
hy₁ : 0 ∈ cf.eval (Nat.pair (unpair n).1 (y + 1 + m))
hy₂ : ∀ {m_1 : ℕ}, m_1 < y + 1 → ∃ a ∈ cf.eval (Nat.pair (unpair n).1 (m_1 + m)), ¬a = 0
a : ℕ
ha : a ∈ cf.eval (Nat.pair (unpair n).1 (0 + m))
a0 : ¬a = 0
k₁ : ℕ
hk₁ : a ∈ evaln (k₁ + 1) cf (Nat.pair (unpair n).1 (0 + m))
k₂ : ℕ
hk₂ : y + m.succ ∈ evaln (k₂ + 1) cf.rfind' (Nat.pair (unpair n).1 m.succ)
h :
  ∀ (hk₁ : a ∈ evaln (k₁ + 1) cf (Nat.pair (unpair n).1 m)) (k₂ : ℕ)
    (hk₂ : y + m.succ ∈ evaln (k₂ + 1) cf.rfind' (Nat.pair (unpair n).1 m.succ)),
    Nat.pair (unpair n).1 m ≤ (max k₁ k₂).succ ∧
      ∃ (a : ℕ),
        evaln ((max k₁ k₂).succ + 1) cf (Nat.pair (unpair n).1 m) = some a ∧
          (if a = 0 then some m else evaln (max k₁ k₂).succ cf.rfind' (Nat.pair (unpair n).1 (m + 1))) =
            some (y + 1 + m)
⊢ Nat.pair (unpair n).1 m ≤ (max k₁ k₂).succ ∧
    ∃ (a : ℕ),
      evaln ((max k₁ k₂).succ + 1) cf (Nat.pair (unpair n).1 m) = some a ∧
        (if a = 0 then some m else evaln (max k₁ k₂).succ cf.rfind' (Nat.pair (unpair n).1 (m + 1))) = some (y + 1 + m)

Tactic:
rw [zero_add] at hk₁

Premises used: zero_add
-- Module: Mathlib.Computability.PartrecCode
Goal:
cf : Code
hf : ∀ {n x : ℕ} (h : x ∈ cf.eval n), ∃ (k : ℕ), x ∈ evaln (k + 1) cf n
n y : ℕ
IH :
  ∀ (m : ℕ) (hy₁ : 0 ∈ cf.eval (Nat.pair (unpair n).1 (y + m)))
    (hy₂ : ∀ {m_1 : ℕ}, m_1 < y → ∃ a ∈ cf.eval (Nat.pair (unpair n).1 (m_1 + m)), ¬a = 0),
    ∃ (k : ℕ), y + m ∈ evaln (k + 1) cf.rfind' (Nat.pair (unpair n).1 m)
m : ℕ
hy₁ : 0 ∈ cf.eval (Nat.pair (unpair n).1 (y + 1 + m))
hy₂ : ∀ {m_1 : ℕ}, m_1 < y + 1 → ∃ a ∈ cf.eval (Nat.pair (unpair n).1 (m_1 + m)), ¬a = 0
a : ℕ
ha : a ∈ cf.eval (Nat.pair (unpair n).1 (0 + m))
a0 : ¬a = 0
k₁ : ℕ
hk₁ : a ∈ evaln (k₁ + 1) cf (Nat.pair (unpair n).1 m)
k₂ : ℕ
hk₂ : y + m.succ ∈ evaln (k₂ + 1) cf.rfind' (Nat.pair (unpair n).1 m.succ)
right :
  ∃ (a : ℕ),
    evaln ((max k₁ k₂).succ + 1) cf (Nat.pair (unpair n).1 m) = some a ∧
      (if a = 0 then some m else evaln (max k₁ k₂).succ cf.rfind' (Nat.pair (unpair n).1 (m + 1))) = some (y + 1 + m)
⊢ Nat.pair (unpair n).1 m ≤ (max k₁ k₂).succ ∧
    ∃ (a : ℕ),
      evaln ((max k₁ k₂).succ + 1) cf (Nat.pair (unpair n).1 m) = some a ∧
        (if a = 0 then some m else evaln (max k₁ k₂).succ cf.rfind' (Nat.pair (unpair n).1 (m + 1))) = some (y + 1 + m)

Tactic:
use Nat.le_succ_of_le <| le_max_of_le_left <| Nat.le_of_lt_succ <| evaln_bound hk₁

Premises used: Nat.Partrec.Code.evaln_bound, Nat.le_of_lt_succ, le_max_of_le_left, Nat.le_succ_of_le
-- Module: Mathlib.Computability.PartrecCode
Goal:
cf : Code
hf : ∀ {n x : ℕ} (h : x ∈ cf.eval n), ∃ (k : ℕ), x ∈ evaln (k + 1) cf n
n y : ℕ
IH :
  ∀ (m : ℕ) (hy₁ : 0 ∈ cf.eval (Nat.pair (unpair n).1 (y + m)))
    (hy₂ : ∀ {m_1 : ℕ}, m_1 < y → ∃ a ∈ cf.eval (Nat.pair (unpair n).1 (m_1 + m)), ¬a = 0),
    ∃ (k : ℕ), y + m ∈ evaln (k + 1) cf.rfind' (Nat.pair (unpair n).1 m)
m : ℕ
hy₁ : 0 ∈ cf.eval (Nat.pair (unpair n).1 (y + 1 + m))
hy₂ : ∀ {m_1 : ℕ}, m_1 < y + 1 → ∃ a ∈ cf.eval (Nat.pair (unpair n).1 (m_1 + m)), ¬a = 0
a : ℕ
ha : a ∈ cf.eval (Nat.pair (unpair n).1 (0 + m))
a0 : ¬a = 0
k₁ : ℕ
hk₁ : a ∈ evaln (k₁ + 1) cf (Nat.pair (unpair n).1 m)
k₂ : ℕ
hk₂ : y + m.succ ∈ evaln (k₂ + 1) cf.rfind' (Nat.pair (unpair n).1 m.succ)
h :
  evaln ((max k₁ k₂).succ + 1) cf (Nat.pair (unpair n).1 m) = some a ∧
    (if a = 0 then some m else evaln (max k₁ k₂).succ cf.rfind' (Nat.pair (unpair n).1 (m + 1))) = some (y + 1 + m)
⊢ ∃ (a : ℕ),
    evaln ((max k₁ k₂).succ + 1) cf (Nat.pair (unpair n).1 m) = some a ∧
      (if a = 0 then some m else evaln (max k₁ k₂).succ cf.rfind' (Nat.pair (unpair n).1 (m + 1))) = some (y + 1 + m)

Tactic:
use a
-- Module: Mathlib.Computability.PartrecCode
Goal:
cf : Code
hf : ∀ {n x : ℕ} (h : x ∈ cf.eval n), ∃ (k : ℕ), x ∈ evaln (k + 1) cf n
n y : ℕ
IH :
  ∀ (m : ℕ) (hy₁ : 0 ∈ cf.eval (Nat.pair (unpair n).1 (y + m)))
    (hy₂ : ∀ {m_1 : ℕ}, m_1 < y → ∃ a ∈ cf.eval (Nat.pair (unpair n).1 (m_1 + m)), ¬a = 0),
    ∃ (k : ℕ), y + m ∈ evaln (k + 1) cf.rfind' (Nat.pair (unpair n).1 m)
m : ℕ
hy₁ : 0 ∈ cf.eval (Nat.pair (unpair n).1 (y + 1 + m))
hy₂ : ∀ {m_1 : ℕ}, m_1 < y + 1 → ∃ a ∈ cf.eval (Nat.pair (unpair n).1 (m_1 + m)), ¬a = 0
a : ℕ
ha : a ∈ cf.eval (Nat.pair (unpair n).1 (0 + m))
a0 : ¬a = 0
k₁ : ℕ
hk₁ : a ∈ evaln (k₁ + 1) cf (Nat.pair (unpair n).1 m)
k₂ : ℕ
hk₂ : y + m.succ ∈ evaln (k₂ + 1) cf.rfind' (Nat.pair (unpair n).1 m.succ)
right : (if a = 0 then some m else evaln (max k₁ k₂).succ cf.rfind' (Nat.pair (unpair n).1 (m + 1))) = some (y + 1 + m)
⊢ evaln ((max k₁ k₂).succ + 1) cf (Nat.pair (unpair n).1 m) = some a ∧
    (if a = 0 then some m else evaln (max k₁ k₂).succ cf.rfind' (Nat.pair (unpair n).1 (m + 1))) = some (y + 1 + m)

Tactic:
use evaln_mono (Nat.succ_le_succ <| Nat.le_succ_of_le <| le_max_left _ _) hk₁

Premises used: Nat.le_succ_of_le, le_max_left, Nat.Partrec.Code.evaln_mono, Nat.succ_le_succ
-- Module: Mathlib.Computability.PartrecCode
Goal:
cf : Code
hf : ∀ {n x : ℕ} (h : x ∈ cf.eval n), ∃ (k : ℕ), x ∈ evaln (k + 1) cf n
n y : ℕ
IH :
  ∀ (m : ℕ) (hy₁ : 0 ∈ cf.eval (Nat.pair (unpair n).1 (y + m)))
    (hy₂ : ∀ {m_1 : ℕ}, m_1 < y → ∃ a ∈ cf.eval (Nat.pair (unpair n).1 (m_1 + m)), ¬a = 0),
    ∃ (k : ℕ), y + m ∈ evaln (k + 1) cf.rfind' (Nat.pair (unpair n).1 m)
m : ℕ
hy₁ : 0 ∈ cf.eval (Nat.pair (unpair n).1 (y + 1 + m))
hy₂ : ∀ {m_1 : ℕ}, m_1 < y + 1 → ∃ a ∈ cf.eval (Nat.pair (unpair n).1 (m_1 + m)), ¬a = 0
a : ℕ
ha : a ∈ cf.eval (Nat.pair (unpair n).1 (0 + m))
a0 : ¬a = 0
k₁ : ℕ
hk₁ : a ∈ evaln (k₁ + 1) cf (Nat.pair (unpair n).1 m)
k₂ : ℕ
hk₂ : y + m.succ ∈ evaln (k₂ + 1) cf.rfind' (Nat.pair (unpair n).1 m.succ)
⊢ (if a = 0 then some m else evaln (max k₁ k₂).succ cf.rfind' (Nat.pair (unpair n).1 (m + 1))) = some (y + 1 + m)

Tactic:
simpa [a0, add_comm, add_left_comm] using
        evaln_mono (Nat.succ_le_succ <| le_max_right _ _) hk₂

Premises used: le_max_right, add_left_comm, add_comm, Nat.Partrec.Code.evaln_mono, Nat.succ_le_succ
-- Module: Mathlib.Computability.PartrecCode
Goal:
n x : ℕ
h : x ∈ Code.zero.eval n
zero : ∀ (h : x = 0), (∃ (x : ℕ), n ≤ x) ∧ 0 = x
⊢ ∃ (k : ℕ), x ∈ evaln (k + 1) Code.zero n

Tactic:
simp [eval, evaln, pure, PFun.pure, Seq.seq, Option.bind_eq_some_iff] at h ⊢

Premises used: Pure.pure, Nat.Partrec.Code.evaln, Seq.seq, PFun.pure, Nat.Partrec.Code.eval, Option.bind_eq_some_iff
-- Module: Mathlib.Computability.PartrecCode
Goal:
n x : ℕ
h : x = 0
⊢ (∃ (x : ℕ), n ≤ x) ∧ 0 = x

Tactic:
⟨⟨_, le_rfl⟩, h.symm⟩

Premises used: le_rfl, And.intro, Exists.intro, Eq.symm
-- Module: Mathlib.Computability.PartrecCode
Goal:
n x : ℕ
h : x = 0
⊢ (∃ (x : ℕ), n ≤ x) ∧ 0 = x

Tactic:
exact ⟨⟨_, le_rfl⟩, h.symm⟩
-- Module: Mathlib.Computability.PartrecCode
Goal:
n x : ℕ
h : x ∈ Code.succ.eval n
succ : ∀ (h : x = n + 1), (∃ (x : ℕ), n ≤ x) ∧ n + 1 = x
⊢ ∃ (k : ℕ), x ∈ evaln (k + 1) Code.succ n

Tactic:
simp [eval, evaln, pure, PFun.pure, Seq.seq, Option.bind_eq_some_iff] at h ⊢

Premises used: Pure.pure, Nat.Partrec.Code.evaln, Seq.seq, PFun.pure, Nat.Partrec.Code.eval, Option.bind_eq_some_iff
-- Module: Mathlib.Computability.PartrecCode
Goal:
n x : ℕ
h : x = n + 1
⊢ (∃ (x : ℕ), n ≤ x) ∧ n + 1 = x

Tactic:
⟨⟨_, le_rfl⟩, h.symm⟩

Premises used: le_rfl, And.intro, Exists.intro, Eq.symm
-- Module: Mathlib.Computability.PartrecCode
Goal:
n x : ℕ
h : x = n + 1
⊢ (∃ (x : ℕ), n ≤ x) ∧ n + 1 = x

Tactic:
exact ⟨⟨_, le_rfl⟩, h.symm⟩
-- Module: Mathlib.Computability.PartrecCode
Goal:
n x : ℕ
h : x ∈ Code.left.eval n
left : ∀ (h : x = (unpair n).1), (∃ (x : ℕ), n ≤ x) ∧ (unpair n).1 = x
⊢ ∃ (k : ℕ), x ∈ evaln (k + 1) Code.left n

Tactic:
simp [eval, evaln, pure, PFun.pure, Seq.seq, Option.bind_eq_some_iff] at h ⊢

Premises used: Pure.pure, Nat.Partrec.Code.evaln, Seq.seq, PFun.pure, Nat.Partrec.Code.eval, Option.bind_eq_some_iff
-- Module: Mathlib.Computability.PartrecCode
Goal:
n x : ℕ
h : x = (unpair n).1
⊢ (∃ (x : ℕ), n ≤ x) ∧ (unpair n).1 = x

Tactic:
⟨⟨_, le_rfl⟩, h.symm⟩

Premises used: le_rfl, And.intro, Exists.intro, Eq.symm
-- Module: Mathlib.Computability.PartrecCode
Goal:
n x : ℕ
h : x = (unpair n).1
⊢ (∃ (x : ℕ), n ≤ x) ∧ (unpair n).1 = x

Tactic:
exact ⟨⟨_, le_rfl⟩, h.symm⟩
-- Module: Mathlib.Computability.PartrecCode
Goal:
n x : ℕ
h : x ∈ Code.right.eval n
right : ∀ (h : x = (unpair n).2), (∃ (x : ℕ), n ≤ x) ∧ (unpair n).2 = x
⊢ ∃ (k : ℕ), x ∈ evaln (k + 1) Code.right n

Tactic:
simp [eval, evaln, pure, PFun.pure, Seq.seq, Option.bind_eq_some_iff] at h ⊢

Premises used: Pure.pure, Nat.Partrec.Code.evaln, Seq.seq, PFun.pure, Nat.Partrec.Code.eval, Option.bind_eq_some_iff
-- Module: Mathlib.Computability.PartrecCode
Goal:
n x : ℕ
h : x = (unpair n).2
⊢ (∃ (x : ℕ), n ≤ x) ∧ (unpair n).2 = x

Tactic:
⟨⟨_, le_rfl⟩, h.symm⟩

Premises used: le_rfl, And.intro, Exists.intro, Eq.symm
-- Module: Mathlib.Computability.PartrecCode
Goal:
n x : ℕ
h : x = (unpair n).2
⊢ (∃ (x : ℕ), n ≤ x) ∧ (unpair n).2 = x

Tactic:
exact ⟨⟨_, le_rfl⟩, h.symm⟩
-- Module: Mathlib.Computability.PartrecCode
Goal:
⊢ Primrec (β := Option ℕ) fun (p : List (List (Option ℕ)) × (ℕ × Code) × ℕ) ↦ lup p.1 p.2.1 p.2.2

Tactic:
Primrec.option_bind
    (Primrec.list_getElem?.comp Primrec.fst (Primrec.encode.comp <| Primrec.fst.comp Primrec.snd))
    (Primrec.option_bind (Primrec.list_getElem?.comp Primrec.snd <| Primrec.snd.comp <|
      Primrec.snd.comp Primrec.fst) Primrec.snd)

Premises used: Primrec.snd, Primrec.fst, _private.0.Nat.Partrec.Code.lup, Primrec.list_getElem?, Primrec.comp, Primrec.option_bind, Primrec₂.comp, Primrec.encode
-- Module: Mathlib.Computability.PartrecCode
Goal:
⊢ Primrec (β := ℕ × Code) fun (a : List (List (Option ℕ))) ↦ ofNat (ℕ × Code) a.length

Tactic:
have a := (Primrec.ofNat (ℕ × Code)).comp (Primrec.list_length (α := List (Option ℕ)))
-- Module: Mathlib.Computability.PartrecCode
Goal:
a : Primrec (β := ℕ × Code) fun (a : List (List (Option ℕ))) ↦ ofNat (ℕ × Code) a.length
⊢ Primrec (β := ℕ) fun (a : List (List (Option ℕ))) ↦ (ofNat (ℕ × Code) a.length).1

Tactic:
have k := Primrec.fst.comp a
-- Module: Mathlib.Computability.PartrecCode
Goal:
a : Primrec (β := ℕ × Code) fun (a : List (List (Option ℕ))) ↦ ofNat (ℕ × Code) a.length
k : Primrec (β := ℕ) fun (a : List (List (Option ℕ))) ↦ (ofNat (ℕ × Code) a.length).1
⊢ Primrec G

Tactic:
Primrec.option_some.comp (Primrec.list_map (Primrec.list_range.comp k) (?_ : Primrec _))

Premises used: _private.0.Nat.Partrec.Code.G, Primrec.list_range, Primrec.list_map, Primrec.option_some, Primrec.comp
-- Module: Mathlib.Computability.PartrecCode
Goal:
a : Primrec (β := ℕ × Code) fun (a : List (List (Option ℕ))) ↦ ofNat (ℕ × Code) a.length
k : Primrec (β := ℕ) fun (a : List (List (Option ℕ))) ↦ (ofNat (ℕ × Code) a.length).1
refine :
  Primrec (β := Option ℕ) fun (p : List (List (Option ℕ)) × ℕ) ↦
    (fun (a : List (List (Option ℕ))) (n : ℕ) ↦
        (Nat.casesOn (motive := fun (x : ℕ) ↦ Option ℕ) (ofNat (ℕ × Code) a.length).1 Option.none fun (k' : ℕ) ↦
            Code.recOn (motive := fun (x : Code) ↦ Option ℕ) (ofNat (ℕ × Code) a.length).2 (some 0) (some n.succ)
              (some (unpair n).1) (some (unpair n).2)
              (fun (cf cg : Code) (x x_1 : Option ℕ) ↦ do
                let x ← lup a ((ofNat (ℕ × Code) a.length).1, cf) n
                let y ← lup a ((ofNat (ℕ × Code) a.length).1, cg) n
                some (Nat.pair x y))
              (fun (cf cg : Code) (x x_1 : Option ℕ) ↦ do
                let x ← lup a ((ofNat (ℕ × Code) a.length).1, cg) n
                lup a ((ofNat (ℕ × Code) a.length).1, cf) x)
              (fun (cf cg : Code) (x x_1 : Option ℕ) ↦
                have z := (unpair n).1;
                Nat.casesOn (motive := fun (x : ℕ) ↦ Option ℕ) (unpair n).2
                  (lup a ((ofNat (ℕ × Code) a.length).1, cf) z) fun (y : ℕ) ↦ do
                  let i ← lup a (k', (ofNat (ℕ × Code) a.length).2) (Nat.pair z y)
                  lup a ((ofNat (ℕ × Code) a.length).1, cg) (Nat.pair z (Nat.pair y i)))
              fun (cf : Code) (x : Option ℕ) ↦
              have z := (unpair n).1;
              have m := (unpair n).2;
              do
              let x ← lup a ((ofNat (ℕ × Code) a.length).1, cf) (Nat.pair z m)
              Nat.casesOn (motive := fun (x : ℕ) ↦ Option ℕ) x (some m) fun (x : ℕ) ↦
                  lup a (k', (ofNat (ℕ × Code) a.length).2) (Nat.pair z (m + 1)) :
          Option ℕ))
      p.1 p.2
⊢ Primrec G

Tactic:
refine Primrec.option_some.comp (Primrec.list_map (Primrec.list_range.comp k) (?_ : Primrec _))

Premises used: Primrec.list_range, Primrec.list_map, Primrec.option_some, Primrec.comp
-- Module: Mathlib.Computability.PartrecCode
Goal:
a : Primrec (β := ℕ × Code) fun (a : List (List (Option ℕ))) ↦ ofNat (ℕ × Code) a.length
k : Primrec (β := ℕ) fun (a : List (List (Option ℕ))) ↦ (ofNat (ℕ × Code) a.length).1
⊢ Primrec (β := ℕ) fun (a : List (List (Option ℕ)) × ℕ) ↦ (ofNat (ℕ × Code) a.1.length).1

Tactic:
replace k := k.comp (Primrec.fst (β := ℕ))
-- Module: Mathlib.Computability.PartrecCode
Goal:
a : Primrec (β := ℕ × Code) fun (a : List (List (Option ℕ))) ↦ ofNat (ℕ × Code) a.length
k : Primrec (β := ℕ) fun (a : List (List (Option ℕ)) × ℕ) ↦ (ofNat (ℕ × Code) a.1.length).1
⊢ Primrec (α := List (List (Option ℕ)) × ℕ) Prod.snd

Tactic:
have n := Primrec.snd (α := List (List (Option ℕ))) (β := ℕ)
-- Module: Mathlib.Computability.PartrecCode
Goal:
a : Primrec (β := ℕ × Code) fun (a : List (List (Option ℕ))) ↦ ofNat (ℕ × Code) a.length
k : Primrec (β := ℕ) fun (a : List (List (Option ℕ)) × ℕ) ↦ (ofNat (ℕ × Code) a.1.length).1
n : Primrec (α := List (List (Option ℕ)) × ℕ) Prod.snd
⊢ Primrec (β := Option ℕ) fun (p : List (List (Option ℕ)) × ℕ) ↦
    (fun (a : List (List (Option ℕ))) (n : ℕ) ↦
        (Nat.casesOn (motive := fun (x : ℕ) ↦ Option ℕ) (ofNat (ℕ × Code) a.length).1 Option.none fun (k' : ℕ) ↦
            Code.recOn (motive := fun (x : Code) ↦ Option ℕ) (ofNat (ℕ × Code) a.length).2 (some 0) (some n.succ)
              (some (unpair n).1) (some (unpair n).2)
              (fun (cf cg : Code) (x x_1 : Option ℕ) ↦ do
                let x ← lup a ((ofNat (ℕ × Code) a.length).1, cf) n
                let y ← lup a ((ofNat (ℕ × Code) a.length).1, cg) n
                some (Nat.pair x y))
              (fun (cf cg : Code) (x x_1 : Option ℕ) ↦ do
                let x ← lup a ((ofNat (ℕ × Code) a.length).1, cg) n
                lup a ((ofNat (ℕ × Code) a.length).1, cf) x)
              (fun (cf cg : Code) (x x_1 : Option ℕ) ↦
                have z := (unpair n).1;
                Nat.casesOn (motive := fun (x : ℕ) ↦ Option ℕ) (unpair n).2
                  (lup a ((ofNat (ℕ × Code) a.length).1, cf) z) fun (y : ℕ) ↦ do
                  let i ← lup a (k', (ofNat (ℕ × Code) a.length).2) (Nat.pair z y)
                  lup a ((ofNat (ℕ × Code) a.length).1, cg) (Nat.pair z (Nat.pair y i)))
              fun (cf : Code) (x : Option ℕ) ↦
              have z := (unpair n).1;
              have m := (unpair n).2;
              do
              let x ← lup a ((ofNat (ℕ × Code) a.length).1, cf) (Nat.pair z m)
              Nat.casesOn (motive := fun (x : ℕ) ↦ Option ℕ) x (some m) fun (x : ℕ) ↦
                  lup a (k', (ofNat (ℕ × Code) a.length).2) (Nat.pair z (m + 1)) :
          Option ℕ))
      p.1 p.2

Tactic:
Primrec.nat_casesOn k (_root_.Primrec.const Option.none) (?_ : Primrec _)

Premises used: Primrec.const, Option.none, Primrec.nat_casesOn
-- Module: Mathlib.Computability.PartrecCode
Goal:
a : Primrec (β := ℕ × Code) fun (a : List (List (Option ℕ))) ↦ ofNat (ℕ × Code) a.length
k : Primrec (β := ℕ) fun (a : List (List (Option ℕ)) × ℕ) ↦ (ofNat (ℕ × Code) a.1.length).1
n : Primrec (α := List (List (Option ℕ)) × ℕ) Prod.snd
⊢ Primrec (β := ℕ) fun (a : (List (List (Option ℕ)) × ℕ) × ℕ) ↦ (ofNat (ℕ × Code) a.1.1.length).1

Tactic:
have k := k.comp (Primrec.fst (β := ℕ))
-- Module: Mathlib.Computability.PartrecCode
Goal:
a : Primrec (β := ℕ × Code) fun (a : List (List (Option ℕ))) ↦ ofNat (ℕ × Code) a.length
k_1 : Primrec (β := ℕ) fun (a : List (List (Option ℕ)) × ℕ) ↦ (ofNat (ℕ × Code) a.1.length).1
n : Primrec (α := List (List (Option ℕ)) × ℕ) Prod.snd
k : Primrec (β := ℕ) fun (a : (List (List (Option ℕ)) × ℕ) × ℕ) ↦ (ofNat (ℕ × Code) a.1.1.length).1
⊢ Primrec (β := ℕ) fun (a : (List (List (Option ℕ)) × ℕ) × ℕ) ↦ a.1.2

Tactic:
have n := n.comp (Primrec.fst (β := ℕ))
-- Module: Mathlib.Computability.PartrecCode
Goal:
a : Primrec (β := ℕ × Code) fun (a : List (List (Option ℕ))) ↦ ofNat (ℕ × Code) a.length
k_1 : Primrec (β := ℕ) fun (a : List (List (Option ℕ)) × ℕ) ↦ (ofNat (ℕ × Code) a.1.length).1
n_1 : Primrec (α := List (List (Option ℕ)) × ℕ) Prod.snd
k : Primrec (β := ℕ) fun (a : (List (List (Option ℕ)) × ℕ) × ℕ) ↦ (ofNat (ℕ × Code) a.1.1.length).1
n : Primrec (β := ℕ) fun (a : (List (List (Option ℕ)) × ℕ) × ℕ) ↦ a.1.2
⊢ Primrec (α := (List (List (Option ℕ)) × ℕ) × ℕ) Prod.snd

Tactic:
have k' := Primrec.snd (α := List (List (Option ℕ)) × ℕ) (β := ℕ)
-- Module: Mathlib.Computability.PartrecCode
Goal:
a : Primrec (β := ℕ × Code) fun (a : List (List (Option ℕ))) ↦ ofNat (ℕ × Code) a.length
k_1 : Primrec (β := ℕ) fun (a : List (List (Option ℕ)) × ℕ) ↦ (ofNat (ℕ × Code) a.1.length).1
n_1 : Primrec (α := List (List (Option ℕ)) × ℕ) Prod.snd
k : Primrec (β := ℕ) fun (a : (List (List (Option ℕ)) × ℕ) × ℕ) ↦ (ofNat (ℕ × Code) a.1.1.length).1
n : Primrec (β := ℕ) fun (a : (List (List (Option ℕ)) × ℕ) × ℕ) ↦ a.1.2
k' : Primrec (α := (List (List (Option ℕ)) × ℕ) × ℕ) Prod.snd
⊢ Primrec (β := Code) fun (a : (List (List (Option ℕ)) × ℕ) × ℕ) ↦ (ofNat (ℕ × Code) a.1.1.length).2

Tactic:
have c := Primrec.snd.comp (a.comp <| (Primrec.fst (β := ℕ)).comp (Primrec.fst (β := ℕ)))
-- Module: Mathlib.Computability.PartrecCode
Goal:
a : Primrec (β := ℕ × Code) fun (a : List (List (Option ℕ))) ↦ ofNat (ℕ × Code) a.length
k_1 : Primrec (β := ℕ) fun (a : List (List (Option ℕ)) × ℕ) ↦ (ofNat (ℕ × Code) a.1.length).1
n_1 : Primrec (α := List (List (Option ℕ)) × ℕ) Prod.snd
k : Primrec (β := ℕ) fun (a : (List (List (Option ℕ)) × ℕ) × ℕ) ↦ (ofNat (ℕ × Code) a.1.1.length).1
n : Primrec (β := ℕ) fun (a : (List (List (Option ℕ)) × ℕ) × ℕ) ↦ a.1.2
k' : Primrec (α := (List (List (Option ℕ)) × ℕ) × ℕ) Prod.snd
c : Primrec (β := Code) fun (a : (List (List (Option ℕ)) × ℕ) × ℕ) ↦ (ofNat (ℕ × Code) a.1.1.length).2
⊢ Primrec (β := List (List (Option ℕ)))
    fun (a : ((List (List (Option ℕ)) × ℕ) × ℕ) × Code × Code × Option ℕ × Option ℕ) ↦ a.1.1.1

Tactic:
have L := (Primrec.fst.comp Primrec.fst).comp
      (Primrec.fst (α := (List (List (Option ℕ)) × ℕ) × ℕ)
        (β := Code × Code × Option ℕ × Option ℕ))
-- Module: Mathlib.Computability.PartrecCode
Goal:
a : Primrec (β := ℕ × Code) fun (a : List (List (Option ℕ))) ↦ ofNat (ℕ × Code) a.length
k_1 : Primrec (β := ℕ) fun (a : List (List (Option ℕ)) × ℕ) ↦ (ofNat (ℕ × Code) a.1.length).1
n_1 : Primrec (α := List (List (Option ℕ)) × ℕ) Prod.snd
k : Primrec (β := ℕ) fun (a : (List (List (Option ℕ)) × ℕ) × ℕ) ↦ (ofNat (ℕ × Code) a.1.1.length).1
n : Primrec (β := ℕ) fun (a : (List (List (Option ℕ)) × ℕ) × ℕ) ↦ a.1.2
k' : Primrec (α := (List (List (Option ℕ)) × ℕ) × ℕ) Prod.snd
c : Primrec (β := Code) fun (a : (List (List (Option ℕ)) × ℕ) × ℕ) ↦ (ofNat (ℕ × Code) a.1.1.length).2
L :
  Primrec (β := List (List (Option ℕ)))
    fun (a : ((List (List (Option ℕ)) × ℕ) × ℕ) × Code × Code × Option ℕ × Option ℕ) ↦ a.1.1.1
⊢ Primrec (β := ℕ) fun (a : ((List (List (Option ℕ)) × ℕ) × ℕ) × Code × Code × Option ℕ × Option ℕ) ↦
    (ofNat (ℕ × Code) a.1.1.1.length).1

Tactic:
have k := k.comp (Primrec.fst (β := Code × Code × Option ℕ × Option ℕ))
-- Module: Mathlib.Computability.PartrecCode
Goal:
a : Primrec (β := ℕ × Code) fun (a : List (List (Option ℕ))) ↦ ofNat (ℕ × Code) a.length
k_1 : Primrec (β := ℕ) fun (a : List (List (Option ℕ)) × ℕ) ↦ (ofNat (ℕ × Code) a.1.length).1
n_1 : Primrec (α := List (List (Option ℕ)) × ℕ) Prod.snd
k_2 : Primrec (β := ℕ) fun (a : (List (List (Option ℕ)) × ℕ) × ℕ) ↦ (ofNat (ℕ × Code) a.1.1.length).1
n : Primrec (β := ℕ) fun (a : (List (List (Option ℕ)) × ℕ) × ℕ) ↦ a.1.2
k' : Primrec (α := (List (List (Option ℕ)) × ℕ) × ℕ) Prod.snd
c : Primrec (β := Code) fun (a : (List (List (Option ℕ)) × ℕ) × ℕ) ↦ (ofNat (ℕ × Code) a.1.1.length).2
L :
  Primrec (β := List (List (Option ℕ)))
    fun (a : ((List (List (Option ℕ)) × ℕ) × ℕ) × Code × Code × Option ℕ × Option ℕ) ↦ a.1.1.1
k :
  Primrec (β := ℕ) fun (a : ((List (List (Option ℕ)) × ℕ) × ℕ) × Code × Code × Option ℕ × Option ℕ) ↦
    (ofNat (ℕ × Code) a.1.1.1.length).1
⊢ Primrec (β := ℕ) fun (a : ((List (List (Option ℕ)) × ℕ) × ℕ) × Code × Code × Option ℕ × Option ℕ) ↦ a.1.1.2

Tactic:
have n := n.comp (Primrec.fst (β := Code × Code × Option ℕ × Option ℕ))