awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (goal)
Goal:
cf : Code
hf : ∀ {n x : ℕ} (h : x ∈ cf.eval n), ∃ (k : ℕ), x ∈ evaln (k + 1) cf n
n y 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
rfind' :
  ∀ (m : ℕ) (hy₁ : 0 ∈ cf.eval (Nat.pair (unpair n).1 (0 + m)))
    (hy₂ : ∀ {m_1 : ℕ}, m_1 < 0 → ∃ a ∈ cf.eval (Nat.pair (unpair n).1 (m_1 + m)), ¬a = 0),
    ∃ (k : ℕ), 0 + m ∈ evaln (k + 1) cf.rfind' (Nat.pair (unpair n).1 m)
rfind'₁ :
  ∀ (m : ℕ) (hy₁ : 0 ∈ cf.eval (Nat.pair (unpair n).1 (0 + m)))
    (hy₂ : ∀ {m_1 : ℕ}, m_1 < 0 → ∃ a ∈ cf.eval (Nat.pair (unpair n).1 (m_1 + m)), ¬a = 0),
    ∃ (k : ℕ),
      Nat.pair (unpair n).1 m ≤ k ∧
        ∃ (a : ℕ),
          evaln (k + 1) cf (Nat.pair (unpair n).1 m) = some a ∧
            (¬a = 0 → evaln k cf.rfind' (Nat.pair (unpair n).1 (m + 1)) = some m)
rfind'₂ :
  ∀ (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),
    ∃ (k : ℕ), y + 1 + m ∈ evaln (k + 1) cf.rfind' (Nat.pair (unpair n).1 m)
⊢ ∃ (k : ℕ), y + m ∈ evaln (k + 1) cf.rfind' (Nat.pair (unpair n).1 m)
have rfind'₃ : ∀ (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),
  ∃ (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: induction y generalizing m with simp [evaln, Option.bind_eq_some_iff]
    | zero =>
      simp at hy₁
      rcases hf hy₁ with ⟨k, hk⟩
      exact ⟨_, Nat.le_of_lt_succ <| evaln_bound hk, _, hk, by simp⟩
    | succ y IH =>
      rcases hy₂ (Nat.succ_pos _) with ⟨a, ha, a0⟩
      rcases hf ha with ⟨k₁, hk₁⟩
      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₂⟩
      use (max k₁ k₂).succ
      rw [zero_add] at hk₁
      use Nat.le_succ_of_le <| le_max_of_le_left <| Nat.le_of_lt_succ <| evaln_bound hk₁
      use a
      use evaln_mono (Nat.succ_le_succ <| Nat.le_succ_of_le <| le_max_left _ _) hk₁
      simpa [a0, add_comm, add_left_comm] using
        evaln_mono (Nat.succ_le_succ <| le_max_right _ _) hk₂
Cleared hypotheses: y, m, hy₁, hy₂
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (goal)
Goal:
n x : ℕ
h : x ∈ zero.eval n
⊢ ∃ (k : ℕ), x ∈ evaln (k + 1) zero n
have zero : ∀ (h : x = 0), (∃ (x : ℕ), n ≤ x) ∧ 0 = x
Tactic: simp [eval, evaln, pure, PFun.pure, Seq.seq, Option.bind_eq_some_iff] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (goal)
Goal:
n x : ℕ
h : x ∈ succ.eval n
⊢ ∃ (k : ℕ), x ∈ evaln (k + 1) succ n
have succ : ∀ (h : x = n + 1), (∃ (x : ℕ), n ≤ x) ∧ n + 1 = x
Tactic: simp [eval, evaln, pure, PFun.pure, Seq.seq, Option.bind_eq_some_iff] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (goal)
Goal:
n x : ℕ
h : x ∈ left.eval n
⊢ ∃ (k : ℕ), x ∈ evaln (k + 1) left n
have left : ∀ (h : x = (unpair n).1), (∃ (x : ℕ), n ≤ x) ∧ (unpair n).1 = x
Tactic: simp [eval, evaln, pure, PFun.pure, Seq.seq, Option.bind_eq_some_iff] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (goal)
Goal:
n x : ℕ
h : x ∈ right.eval n
⊢ ∃ (k : ℕ), x ∈ evaln (k + 1) right n
have right : ∀ (h : x = (unpair n).2), (∃ (x : ℕ), n ≤ x) ∧ (unpair n).2 = x
Tactic: simp [eval, evaln, pure, PFun.pure, Seq.seq, Option.bind_eq_some_iff] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (hypothesis)
Goal:
⊢ Primrec G
have a : Primrec (β := ℕ × Code) fun (a : List (List (Option ℕ))) ↦ ofNat (ℕ × Code) a.length
Tactic: have a := (Primrec.ofNat (ℕ × Code)).comp (Primrec.list_length (α := List (Option ℕ)))
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (hypothesis)
Goal:
a : Primrec (β := ℕ × Code) fun (a : List (List (Option ℕ))) ↦ ofNat (ℕ × Code) a.length
⊢ Primrec G
have k : Primrec (β := ℕ) fun (a : List (List (Option ℕ))) ↦ (ofNat (ℕ × Code) a.length).1
Tactic: have k := Primrec.fst.comp a
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (goal)
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
have 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
Tactic: refine Primrec.option_some.comp (Primrec.list_map (Primrec.list_range.comp k) (?_ : Primrec _))
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (hypothesis)
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 (β := 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
have k₁ : Primrec (β := ℕ) fun (a : List (List (Option ℕ)) × ℕ) ↦ (ofNat (ℕ × Code) a.1.length).1
Tactic: replace k := k.comp (Primrec.fst (β := ℕ))
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (hypothesis)
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 (β := 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
have n : Primrec (α := List (List (Option ℕ)) × ℕ) Prod.snd
Tactic: have n := Primrec.snd (α := List (List (Option ℕ))) (β := ℕ)
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (hypothesis)
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 (p : List (List (Option ℕ)) × ℕ) (k' : ℕ) ↦
        (Code.recOn (motive := fun (x : Code) ↦ Option ℕ) (ofNat (ℕ × Code) p.1.length).2 (some 0) (some p.2.succ)
            (some (unpair p.2).1) (some (unpair p.2).2)
            (fun (cf cg : Code) (x x_1 : Option ℕ) ↦ do
              let x ← lup p.1 ((ofNat (ℕ × Code) p.1.length).1, cf) p.2
              let y ← lup p.1 ((ofNat (ℕ × Code) p.1.length).1, cg) p.2
              some (Nat.pair x y))
            (fun (cf cg : Code) (x x_1 : Option ℕ) ↦ do
              let x ← lup p.1 ((ofNat (ℕ × Code) p.1.length).1, cg) p.2
              lup p.1 ((ofNat (ℕ × Code) p.1.length).1, cf) x)
            (fun (cf cg : Code) (x x_1 : Option ℕ) ↦
              have z := (unpair p.2).1;
              Nat.casesOn (motive := fun (x : ℕ) ↦ Option ℕ) (unpair p.2).2
                (lup p.1 ((ofNat (ℕ × Code) p.1.length).1, cf) z) fun (y : ℕ) ↦ do
                let i ← lup p.1 (k', (ofNat (ℕ × Code) p.1.length).2) (Nat.pair z y)
                lup p.1 ((ofNat (ℕ × Code) p.1.length).1, cg) (Nat.pair z (Nat.pair y i)))
            fun (cf : Code) (x : Option ℕ) ↦
            have z := (unpair p.2).1;
            have m := (unpair p.2).2;
            do
            let x ← lup p.1 ((ofNat (ℕ × Code) p.1.length).1, cf) (Nat.pair z m)
            Nat.casesOn (motive := fun (x : ℕ) ↦ Option ℕ) x (some m) fun (x : ℕ) ↦
                lup p.1 (k', (ofNat (ℕ × Code) p.1.length).2) (Nat.pair z (m + 1)) :
          Option ℕ))
      p.1 p.2
have k₁ : Primrec (β := ℕ) fun (a : (List (List (Option ℕ)) × ℕ) × ℕ) ↦ (ofNat (ℕ × Code) a.1.1.length).1
Tactic: have k := k.comp (Primrec.fst (β := ℕ))
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (hypothesis)
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 (β := Option ℕ) fun (p : (List (List (Option ℕ)) × ℕ) × ℕ) ↦
    (fun (p : List (List (Option ℕ)) × ℕ) (k' : ℕ) ↦
        (Code.recOn (motive := fun (x : Code) ↦ Option ℕ) (ofNat (ℕ × Code) p.1.length).2 (some 0) (some p.2.succ)
            (some (unpair p.2).1) (some (unpair p.2).2)
            (fun (cf cg : Code) (x x_1 : Option ℕ) ↦ do
              let x ← lup p.1 ((ofNat (ℕ × Code) p.1.length).1, cf) p.2
              let y ← lup p.1 ((ofNat (ℕ × Code) p.1.length).1, cg) p.2
              some (Nat.pair x y))
            (fun (cf cg : Code) (x x_1 : Option ℕ) ↦ do
              let x ← lup p.1 ((ofNat (ℕ × Code) p.1.length).1, cg) p.2
              lup p.1 ((ofNat (ℕ × Code) p.1.length).1, cf) x)
            (fun (cf cg : Code) (x x_1 : Option ℕ) ↦
              have z := (unpair p.2).1;
              Nat.casesOn (motive := fun (x : ℕ) ↦ Option ℕ) (unpair p.2).2
                (lup p.1 ((ofNat (ℕ × Code) p.1.length).1, cf) z) fun (y : ℕ) ↦ do
                let i ← lup p.1 (k', (ofNat (ℕ × Code) p.1.length).2) (Nat.pair z y)
                lup p.1 ((ofNat (ℕ × Code) p.1.length).1, cg) (Nat.pair z (Nat.pair y i)))
            fun (cf : Code) (x : Option ℕ) ↦
            have z := (unpair p.2).1;
            have m := (unpair p.2).2;
            do
            let x ← lup p.1 ((ofNat (ℕ × Code) p.1.length).1, cf) (Nat.pair z m)
            Nat.casesOn (motive := fun (x : ℕ) ↦ Option ℕ) x (some m) fun (x : ℕ) ↦
                lup p.1 (k', (ofNat (ℕ × Code) p.1.length).2) (Nat.pair z (m + 1)) :
          Option ℕ))
      p.1 p.2
have n₁ : Primrec (β := ℕ) fun (a : (List (List (Option ℕ)) × ℕ) × ℕ) ↦ a.1.2
Tactic: have n := n.comp (Primrec.fst (β := ℕ))
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (hypothesis)
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 (β := Option ℕ) fun (p : (List (List (Option ℕ)) × ℕ) × ℕ) ↦
    (fun (p : List (List (Option ℕ)) × ℕ) (k' : ℕ) ↦
        (Code.recOn (motive := fun (x : Code) ↦ Option ℕ) (ofNat (ℕ × Code) p.1.length).2 (some 0) (some p.2.succ)
            (some (unpair p.2).1) (some (unpair p.2).2)
            (fun (cf cg : Code) (x x_1 : Option ℕ) ↦ do
              let x ← lup p.1 ((ofNat (ℕ × Code) p.1.length).1, cf) p.2
              let y ← lup p.1 ((ofNat (ℕ × Code) p.1.length).1, cg) p.2
              some (Nat.pair x y))
            (fun (cf cg : Code) (x x_1 : Option ℕ) ↦ do
              let x ← lup p.1 ((ofNat (ℕ × Code) p.1.length).1, cg) p.2
              lup p.1 ((ofNat (ℕ × Code) p.1.length).1, cf) x)
            (fun (cf cg : Code) (x x_1 : Option ℕ) ↦
              have z := (unpair p.2).1;
              Nat.casesOn (motive := fun (x : ℕ) ↦ Option ℕ) (unpair p.2).2
                (lup p.1 ((ofNat (ℕ × Code) p.1.length).1, cf) z) fun (y : ℕ) ↦ do
                let i ← lup p.1 (k', (ofNat (ℕ × Code) p.1.length).2) (Nat.pair z y)
                lup p.1 ((ofNat (ℕ × Code) p.1.length).1, cg) (Nat.pair z (Nat.pair y i)))
            fun (cf : Code) (x : Option ℕ) ↦
            have z := (unpair p.2).1;
            have m := (unpair p.2).2;
            do
            let x ← lup p.1 ((ofNat (ℕ × Code) p.1.length).1, cf) (Nat.pair z m)
            Nat.casesOn (motive := fun (x : ℕ) ↦ Option ℕ) x (some m) fun (x : ℕ) ↦
                lup p.1 (k', (ofNat (ℕ × Code) p.1.length).2) (Nat.pair z (m + 1)) :
          Option ℕ))
      p.1 p.2
have k' : Primrec (α := (List (List (Option ℕ)) × ℕ) × ℕ) Prod.snd
Tactic: have k' := Primrec.snd (α := List (List (Option ℕ)) × ℕ) (β := ℕ)
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (hypothesis)
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 (β := Option ℕ) fun (p : (List (List (Option ℕ)) × ℕ) × ℕ) ↦
    (fun (p : List (List (Option ℕ)) × ℕ) (k' : ℕ) ↦
        (Code.recOn (motive := fun (x : Code) ↦ Option ℕ) (ofNat (ℕ × Code) p.1.length).2 (some 0) (some p.2.succ)
            (some (unpair p.2).1) (some (unpair p.2).2)
            (fun (cf cg : Code) (x x_1 : Option ℕ) ↦ do
              let x ← lup p.1 ((ofNat (ℕ × Code) p.1.length).1, cf) p.2
              let y ← lup p.1 ((ofNat (ℕ × Code) p.1.length).1, cg) p.2
              some (Nat.pair x y))
            (fun (cf cg : Code) (x x_1 : Option ℕ) ↦ do
              let x ← lup p.1 ((ofNat (ℕ × Code) p.1.length).1, cg) p.2
              lup p.1 ((ofNat (ℕ × Code) p.1.length).1, cf) x)
            (fun (cf cg : Code) (x x_1 : Option ℕ) ↦
              have z := (unpair p.2).1;
              Nat.casesOn (motive := fun (x : ℕ) ↦ Option ℕ) (unpair p.2).2
                (lup p.1 ((ofNat (ℕ × Code) p.1.length).1, cf) z) fun (y : ℕ) ↦ do
                let i ← lup p.1 (k', (ofNat (ℕ × Code) p.1.length).2) (Nat.pair z y)
                lup p.1 ((ofNat (ℕ × Code) p.1.length).1, cg) (Nat.pair z (Nat.pair y i)))
            fun (cf : Code) (x : Option ℕ) ↦
            have z := (unpair p.2).1;
            have m := (unpair p.2).2;
            do
            let x ← lup p.1 ((ofNat (ℕ × Code) p.1.length).1, cf) (Nat.pair z m)
            Nat.casesOn (motive := fun (x : ℕ) ↦ Option ℕ) x (some m) fun (x : ℕ) ↦
                lup p.1 (k', (ofNat (ℕ × Code) p.1.length).2) (Nat.pair z (m + 1)) :
          Option ℕ))
      p.1 p.2
have c : 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 (β := ℕ)))
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (goal)
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 (β := Option ℕ) fun (p : (List (List (Option ℕ)) × ℕ) × ℕ) ↦
    (fun (p : List (List (Option ℕ)) × ℕ) (k' : ℕ) ↦
        (Code.recOn (motive := fun (x : Code) ↦ Option ℕ) (ofNat (ℕ × Code) p.1.length).2 (some 0) (some p.2.succ)
            (some (unpair p.2).1) (some (unpair p.2).2)
            (fun (cf cg : Code) (x x_1 : Option ℕ) ↦ do
              let x ← lup p.1 ((ofNat (ℕ × Code) p.1.length).1, cf) p.2
              let y ← lup p.1 ((ofNat (ℕ × Code) p.1.length).1, cg) p.2
              some (Nat.pair x y))
            (fun (cf cg : Code) (x x_1 : Option ℕ) ↦ do
              let x ← lup p.1 ((ofNat (ℕ × Code) p.1.length).1, cg) p.2
              lup p.1 ((ofNat (ℕ × Code) p.1.length).1, cf) x)
            (fun (cf cg : Code) (x x_1 : Option ℕ) ↦
              have z := (unpair p.2).1;
              Nat.casesOn (motive := fun (x : ℕ) ↦ Option ℕ) (unpair p.2).2
                (lup p.1 ((ofNat (ℕ × Code) p.1.length).1, cf) z) fun (y : ℕ) ↦ do
                let i ← lup p.1 (k', (ofNat (ℕ × Code) p.1.length).2) (Nat.pair z y)
                lup p.1 ((ofNat (ℕ × Code) p.1.length).1, cg) (Nat.pair z (Nat.pair y i)))
            fun (cf : Code) (x : Option ℕ) ↦
            have z := (unpair p.2).1;
            have m := (unpair p.2).2;
            do
            let x ← lup p.1 ((ofNat (ℕ × Code) p.1.length).1, cf) (Nat.pair z m)
            Nat.casesOn (motive := fun (x : ℕ) ↦ Option ℕ) x (some m) fun (x : ℕ) ↦
                lup p.1 (k', (ofNat (ℕ × Code) p.1.length).2) (Nat.pair z (m + 1)) :
          Option ℕ))
      p.1 p.2
have hpr : Primrec (β := Option ℕ) fun (a : ((List (List (Option ℕ)) × ℕ) × ℕ) × Code × Code × Option ℕ × Option ℕ) ↦ do
  let x ← lup a.1.1.1 ((ofNat (ℕ × Code) a.1.1.1.length).1, a.2.1) a.1.1.2
  let y ← lup a.1.1.1 ((ofNat (ℕ × Code) a.1.1.1.length).1, a.2.2.1) a.1.1.2
  some (Nat.pair x y)
Tactic: apply
    Nat.Partrec.Code.primrec_recOn c
      (_root_.Primrec.const (some 0))
      (Primrec.option_some.comp (_root_.Primrec.succ.comp n))
      (Primrec.option_some.comp (Primrec.fst.comp <| Primrec.unpair.comp n))
      (Primrec.option_some.comp (Primrec.snd.comp <| Primrec.unpair.comp n))