awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (hypothesis)
Goal:
α : Type u_1
σ : Type u_2
inst : Primcodable α
inst_1 : Primcodable σ
c : α → Code
hc : Computable c
z : α → σ
hz : Computable z
s : α → σ
hs : Computable s
l : α → σ
hl : Computable l
r : α → σ
hr : Computable r
pr : α → Code × Code × σ × σ → σ
hpr : Computable₂ pr
co : α → Code × Code × σ × σ → σ
hco : Computable₂ co
pc : α → Code × Code × σ × σ → σ
hpc : Computable₂ pc
rf : α → Code × σ → σ
hrf : Computable₂ rf
PR : (a : α) → (cf cg : Code) → (hf hg : σ) → σ := fun (a : α) (cf cg : Code) (hf hg : σ) ↦ pr a (cf, cg, hf, hg)
CO : (a : α) → (cf cg : Code) → (hf hg : σ) → σ := fun (a : α) (cf cg : Code) (hf hg : σ) ↦ co a (cf, cg, hf, hg)
PC : (a : α) → (cf cg : Code) → (hf hg : σ) → σ := fun (a : α) (cf cg : Code) (hf hg : σ) ↦ pc a (cf, cg, hf, hg)
RF : (a : α) → (cf : Code) → (hf : σ) → σ := fun (a : α) (cf : Code) (hf : σ) ↦ rf a (cf, hf)
F : (a : α) → (c : Code) → σ :=
  fun (a : α) (c : Code) ↦
    Code.recOn (motive := fun (x : Code) ↦ σ) c (z a) (s a) (l a) (r a) (PR a) (CO a) (PC a) (RF a)
G₁ : Prod.{u_1, u_2} α (List σ) × ℕ × ℕ → Option σ :=
  fun (p : Prod.{u_1, u_2} α (List σ) × ℕ × ℕ) ↦
    (getElem? (valid := fun (as : List σ) (i : ℕ) ↦ i < as.length) p.1.2 p.2.2).bind fun (s : σ) ↦
      (getElem? (valid := fun (as : List σ) (i : ℕ) ↦ i < as.length) p.1.2 (unpair p.2.2).1).bind fun (s₁ : σ) ↦
        Option.map
          (fun (s₂ : σ) ↦
            bif p.2.1.bodd then
              bif p.2.1.div2.bodd then rf p.1.1 (ofNat Code p.2.2, s)
              else pc p.1.1 (ofNat Code (unpair p.2.2).1, ofNat Code (unpair p.2.2).2, s₁, s₂)
            else
              bif p.2.1.div2.bodd then co p.1.1 (ofNat Code (unpair p.2.2).1, ofNat Code (unpair p.2.2).2, s₁, s₂)
              else pr p.1.1 (ofNat Code (unpair p.2.2).1, ofNat Code (unpair p.2.2).2, s₁, s₂))
          (getElem? (valid := fun (as : List σ) (i : ℕ) ↦ i < as.length) p.1.2 (unpair p.2.2).2)
this_1 : Computable G₁
G : α → List σ → Option σ :=
  fun (a : α) (IH : List σ) ↦
    Nat.casesOn (motive := fun (x : ℕ) ↦ Option σ) IH.length (some (z a)) fun (n : ℕ) ↦
      Nat.casesOn (motive := fun (x : ℕ) ↦ Option σ) n (some (s a)) fun (n : ℕ) ↦
        Nat.casesOn (motive := fun (x : ℕ) ↦ Option σ) n (some (l a)) fun (n : ℕ) ↦
          Nat.casesOn (motive := fun (x : ℕ) ↦ Option σ) n (some (r a)) fun (n : ℕ) ↦ G₁ ((a, IH), n, n.div2.div2)
this : Computable₂ G
a : α
n : ℕ
m : ℕ := n.div2.div2
hm : m < n + 4
⊢ G₁ ((a, List.map (fun (n : ℕ) ↦ F a (ofNat Code n)) (List.range (n + 4))), n, m) = some (F a (ofNat Code (n + 4)))
have m1 : (unpair m).1 < n + 4
Tactic: have m1 : m.unpair.1 < n + 4 := lt_of_le_of_lt m.unpair_left_le hm
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (hypothesis)
Goal:
α : Type u_1
σ : Type u_2
inst : Primcodable α
inst_1 : Primcodable σ
c : α → Code
hc : Computable c
z : α → σ
hz : Computable z
s : α → σ
hs : Computable s
l : α → σ
hl : Computable l
r : α → σ
hr : Computable r
pr : α → Code × Code × σ × σ → σ
hpr : Computable₂ pr
co : α → Code × Code × σ × σ → σ
hco : Computable₂ co
pc : α → Code × Code × σ × σ → σ
hpc : Computable₂ pc
rf : α → Code × σ → σ
hrf : Computable₂ rf
PR : (a : α) → (cf cg : Code) → (hf hg : σ) → σ := fun (a : α) (cf cg : Code) (hf hg : σ) ↦ pr a (cf, cg, hf, hg)
CO : (a : α) → (cf cg : Code) → (hf hg : σ) → σ := fun (a : α) (cf cg : Code) (hf hg : σ) ↦ co a (cf, cg, hf, hg)
PC : (a : α) → (cf cg : Code) → (hf hg : σ) → σ := fun (a : α) (cf cg : Code) (hf hg : σ) ↦ pc a (cf, cg, hf, hg)
RF : (a : α) → (cf : Code) → (hf : σ) → σ := fun (a : α) (cf : Code) (hf : σ) ↦ rf a (cf, hf)
F : (a : α) → (c : Code) → σ :=
  fun (a : α) (c : Code) ↦
    Code.recOn (motive := fun (x : Code) ↦ σ) c (z a) (s a) (l a) (r a) (PR a) (CO a) (PC a) (RF a)
G₁ : Prod.{u_1, u_2} α (List σ) × ℕ × ℕ → Option σ :=
  fun (p : Prod.{u_1, u_2} α (List σ) × ℕ × ℕ) ↦
    (getElem? (valid := fun (as : List σ) (i : ℕ) ↦ i < as.length) p.1.2 p.2.2).bind fun (s : σ) ↦
      (getElem? (valid := fun (as : List σ) (i : ℕ) ↦ i < as.length) p.1.2 (unpair p.2.2).1).bind fun (s₁ : σ) ↦
        Option.map
          (fun (s₂ : σ) ↦
            bif p.2.1.bodd then
              bif p.2.1.div2.bodd then rf p.1.1 (ofNat Code p.2.2, s)
              else pc p.1.1 (ofNat Code (unpair p.2.2).1, ofNat Code (unpair p.2.2).2, s₁, s₂)
            else
              bif p.2.1.div2.bodd then co p.1.1 (ofNat Code (unpair p.2.2).1, ofNat Code (unpair p.2.2).2, s₁, s₂)
              else pr p.1.1 (ofNat Code (unpair p.2.2).1, ofNat Code (unpair p.2.2).2, s₁, s₂))
          (getElem? (valid := fun (as : List σ) (i : ℕ) ↦ i < as.length) p.1.2 (unpair p.2.2).2)
this_1 : Computable G₁
G : α → List σ → Option σ :=
  fun (a : α) (IH : List σ) ↦
    Nat.casesOn (motive := fun (x : ℕ) ↦ Option σ) IH.length (some (z a)) fun (n : ℕ) ↦
      Nat.casesOn (motive := fun (x : ℕ) ↦ Option σ) n (some (s a)) fun (n : ℕ) ↦
        Nat.casesOn (motive := fun (x : ℕ) ↦ Option σ) n (some (l a)) fun (n : ℕ) ↦
          Nat.casesOn (motive := fun (x : ℕ) ↦ Option σ) n (some (r a)) fun (n : ℕ) ↦ G₁ ((a, IH), n, n.div2.div2)
this : Computable₂ G
a : α
n : ℕ
m : ℕ := n.div2.div2
hm : m < n + 4
m1 : (unpair m).1 < n + 4
⊢ G₁ ((a, List.map (fun (n : ℕ) ↦ F a (ofNat Code n)) (List.range (n + 4))), n, m) = some (F a (ofNat Code (n + 4)))
have m2 : (unpair m).2 < n + 4
Tactic: have m2 : m.unpair.2 < n + 4 := lt_of_le_of_lt m.unpair_right_le hm
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (goal)
Goal:
cf cg : Code
a : ℕ
⊢ (cf.prec cg).eval (Nat.pair a 0) = cf.eval a
have rw : Nat.rec (motive := fun (x : ℕ) ↦ Part ℕ) (cf.eval (a, 0).1)
    (fun (y : ℕ) (IH : Part ℕ) ↦ do
      let i ← IH
      cg.eval (Nat.pair (a, 0).1 (Nat.pair y i)))
    (a, 0).2 =
  cf.eval a
Tactic: rw [eval, Nat.unpaired, Nat.unpair_pair]
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (goal)
Goal:
cf cg : Code
a : ℕ
⊢ Nat.rec (motive := fun (x : ℕ) ↦ Part ℕ) (cf.eval (a, 0).1)
      (fun (y : ℕ) (IH : Part ℕ) ↦ do
        let i ← IH
        cg.eval (Nat.pair (a, 0).1 (Nat.pair y i)))
      (a, 0).2 =
    cf.eval a
have simp : Nat.rec (motive := fun (x : ℕ) ↦ Part ℕ) (cf.eval a)
    (fun (y : ℕ) (IH : Part ℕ) ↦ do
      let i ← IH
      cg.eval (Nat.pair a (Nat.pair y i)))
    0 =
  cf.eval a
Tactic: simp (config := { Lean.Meta.Simp.neutralConfig with proj := true }) only []
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (goal)
Goal:
cf cg : Code
a : ℕ
⊢ Nat.rec (motive := fun (x : ℕ) ↦ Part ℕ) (cf.eval a)
      (fun (y : ℕ) (IH : Part ℕ) ↦ do
        let i ← IH
        cg.eval (Nat.pair a (Nat.pair y i)))
      0 =
    cf.eval a
have rw : cf.eval a = cf.eval a
Tactic: rw [Nat.rec_zero]
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (goal)
Goal:
cf cg : Code
a k : ℕ
⊢ (cf.prec cg).eval (Nat.pair a k.succ) = do
    let ih ← (cf.prec cg).eval (Nat.pair a k)
    cg.eval (Nat.pair a (Nat.pair k ih))
have rw : Eq (α := Part ℕ)
  (Nat.rec (motive := fun (x : ℕ) ↦ Part ℕ) (cf.eval (a, k.succ).1)
      (fun (y : ℕ) (IH : Part ℕ) ↦ do
        let i ← IH
        cg.eval (Nat.pair (a, k.succ).1 (Nat.pair y i)))
      (a, k.succ).2 :
    Part ℕ)
  (Part.bind
      (unpaired
        (fun (a n : ℕ) ↦
          Nat.rec (motive := fun (x : ℕ) ↦ Part ℕ) (cf.eval a)
            (fun (y : ℕ) (IH : Part ℕ) ↦ do
              let i ← IH
              cg.eval (Nat.pair a (Nat.pair y i)))
            n)
        (Nat.pair a k))
      fun (ih : ℕ) ↦ cg.eval (Nat.pair a (Nat.pair k ih)) :
    Part ℕ)
Tactic: rw [eval, Nat.unpaired, Part.bind_eq_bind, Nat.unpair_pair]
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (goal)
Goal:
n : ℕ
⊢ (fun (b : Code) ↦ succ.comp (n, b).2)^[id n] zero = Code.const n
have simp : (fun (b : Code) ↦ succ.comp b)^[n] zero = Code.const n
Tactic: simp
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (goal)
Goal:
n : ℕ
⊢ (fun (b : Code) ↦ succ.comp b)^[n] zero = Code.const n
have zero : (fun (b : Code) ↦ succ.comp b)^[0] zero = Code.const 0
Tactic: induction n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (goal)
Goal:
n : ℕ
zero : (fun (b : Code) ↦ succ.comp b)^[0] Code.zero = Code.const 0
⊢ (fun (b : Code) ↦ succ.comp b)^[n] Code.zero = Code.const n
have succ : ∀ (n : ℕ),
  (fun (b : Code) ↦ succ.comp b)^[n] Code.zero = Code.const n →
    (fun (b : Code) ↦ succ.comp b)^[n + 1] Code.zero = Code.const (n + 1)
Tactic: induction n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (hypothesis)
Goal:
c₁ c₂ : Code
n₁ n₂ : ℕ
h : c₁.curry n₁ = c₂.curry n₂
⊢ n₁ = n₂
have h₁ : c₁ = c₂
Tactic: injection h with h₁ h₂
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (hypothesis)
Goal:
c₁ c₂ : Code
n₁ n₂ : ℕ
h : c₁.curry n₁ = c₂.curry n₂
h₁ : c₁ = c₂
⊢ n₁ = n₂
have h₂ : (Code.const n₁).pair Code.id = (Code.const n₂).pair Code.id
Tactic: injection h with h₁ h₂
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (hypothesis)
Goal:
c₁ c₂ : Code
n₁ n₂ : ℕ
h₁ : c₁ = c₂
h₂ : (Code.const n₁).pair Code.id = (Code.const n₂).pair Code.id
⊢ n₁ = n₂
have h₃ : Code.const n₁ = Code.const n₂
Tactic: injection h₂ with h₃ h₄
Cleared hypotheses: h₂
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (hypothesis)
Goal:
c₁ c₂ : Code
n₁ n₂ : ℕ
h₁ : c₁ = c₂
h₂ : (Code.const n₁).pair Code.id = (Code.const n₂).pair Code.id
h₃ : Code.const n₁ = Code.const n₂
⊢ n₁ = n₂
have h₄ : Code.id = Code.id
Tactic: injection h₂ with h₃ h₄
Cleared hypotheses: h₂
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (goal)
Goal:
f : ℕ →. ℕ
⊢ Nat.Partrec f ↔ ∃ (c : Code), c.eval = f
have refine_1 : ∀ (h : Nat.Partrec f), ∃ (c : Code), c.eval = f
Tactic: refine ⟨fun h => ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (goal)
Goal:
f : ℕ →. ℕ
refine_1 : ∀ (h : Nat.Partrec f), ∃ (c : Code), c.eval = f
⊢ Nat.Partrec f ↔ ∃ (c : Code), c.eval = f
have refine_2 : (∃ (c : Code), c.eval = f) → Nat.Partrec f
Tactic: refine ⟨fun h => ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (goal)
Goal:
f f_1 g : ℕ →. ℕ
pf : Nat.Partrec f_1
pg : Nat.Partrec g
hf : ∃ (c : Code), c.eval = f_1
hg : ∃ (c : Code), c.eval = g
⊢ ∃ (c : Code), c.eval = fun (n : ℕ) ↦ Nat.pair <$> f_1 n <*> g n
have refine_1 : ∀ (cf : Code) (pf : Nat.Partrec cf.eval), ∃ (c : Code), c.eval = fun (n : ℕ) ↦ Nat.pair <$> cf.eval n <*> g n
Tactic: rcases hf with ⟨cf, rfl⟩
Cleared hypotheses: f_1, pf, hf
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (goal)
Goal:
f g : ℕ →. ℕ
pg : Nat.Partrec g
hg : ∃ (c : Code), c.eval = g
cf : Code
pf : Nat.Partrec cf.eval
⊢ ∃ (c : Code), c.eval = fun (n : ℕ) ↦ Nat.pair <$> cf.eval n <*> g n
have refine_1 : ∀ (cg : Code) (pg : Nat.Partrec cg.eval), ∃ (c : Code), c.eval = fun (n : ℕ) ↦ Nat.pair <$> cf.eval n <*> cg.eval n
Tactic: rcases hg with ⟨cg, rfl⟩
Cleared hypotheses: g, pg, hg
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (goal)
Goal:
f f_1 g : ℕ →. ℕ
pf : Nat.Partrec f_1
pg : Nat.Partrec g
hf : ∃ (c : Code), c.eval = f_1
hg : ∃ (c : Code), c.eval = g
⊢ ∃ (c : Code), c.eval = fun (n : ℕ) ↦ g n >>= f_1
have refine_1 : ∀ (cf : Code) (pf : Nat.Partrec cf.eval), ∃ (c : Code), c.eval = fun (n : ℕ) ↦ g n >>= cf.eval
Tactic: rcases hf with ⟨cf, rfl⟩
Cleared hypotheses: f_1, pf, hf
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (goal)
Goal:
f g : ℕ →. ℕ
pg : Nat.Partrec g
hg : ∃ (c : Code), c.eval = g
cf : Code
pf : Nat.Partrec cf.eval
⊢ ∃ (c : Code), c.eval = fun (n : ℕ) ↦ g n >>= cf.eval
have refine_1 : ∀ (cg : Code) (pg : Nat.Partrec cg.eval), ∃ (c : Code), c.eval = fun (n : ℕ) ↦ cg.eval n >>= cf.eval
Tactic: rcases hg with ⟨cg, rfl⟩
Cleared hypotheses: g, pg, hg
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (goal)
Goal:
f f_1 g : ℕ →. ℕ
pf : Nat.Partrec f_1
pg : Nat.Partrec g
hf : ∃ (c : Code), c.eval = f_1
hg : ∃ (c : Code), c.eval = g
⊢ ∃ (c : Code),
    c.eval =
      unpaired fun (a n : ℕ) ↦
        Nat.rec (motive := fun (x : ℕ) ↦ Part ℕ) (f_1 a)
          (fun (y : ℕ) (IH : Part ℕ) ↦ do
            let i ← IH
            g (Nat.pair a (Nat.pair y i)))
          n
have refine_1 : ∀ (cf : Code) (pf : Nat.Partrec cf.eval),
  ∃ (c : Code),
    c.eval =
      unpaired fun (a n : ℕ) ↦
        Nat.rec (motive := fun (x : ℕ) ↦ Part ℕ) (cf.eval a)
          (fun (y : ℕ) (IH : Part ℕ) ↦ do
            let i ← IH
            g (Nat.pair a (Nat.pair y i)))
          n
Tactic: rcases hf with ⟨cf, rfl⟩
Cleared hypotheses: f_1, pf, hf
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (goal)
Goal:
f g : ℕ →. ℕ
pg : Nat.Partrec g
hg : ∃ (c : Code), c.eval = g
cf : Code
pf : Nat.Partrec cf.eval
⊢ ∃ (c : Code),
    c.eval =
      unpaired fun (a n : ℕ) ↦
        Nat.rec (motive := fun (x : ℕ) ↦ Part ℕ) (cf.eval a)
          (fun (y : ℕ) (IH : Part ℕ) ↦ do
            let i ← IH
            g (Nat.pair a (Nat.pair y i)))
          n
have refine_1 : ∀ (cg : Code) (pg : Nat.Partrec cg.eval),
  ∃ (c : Code),
    c.eval =
      unpaired fun (a n : ℕ) ↦
        Nat.rec (motive := fun (x : ℕ) ↦ Part ℕ) (cf.eval a)
          (fun (y : ℕ) (IH : Part ℕ) ↦ do
            let i ← IH
            cg.eval (Nat.pair a (Nat.pair y i)))
          n
Tactic: rcases hg with ⟨cg, rfl⟩
Cleared hypotheses: g, pg, hg
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (goal)
Goal:
f f_1 : ℕ →. ℕ
pf : Nat.Partrec f_1
hf : ∃ (c : Code), c.eval = f_1
⊢ ∃ (c : Code), c.eval = fun (a : ℕ) ↦ Nat.rfind fun (n : ℕ) ↦ (fun (m : ℕ) ↦ decide (m = 0)) <$> f_1 (Nat.pair a n)
have refine_1 : ∀ (cf : Code) (pf : Nat.Partrec cf.eval),
  ∃ (c : Code), c.eval = fun (a : ℕ) ↦ Nat.rfind fun (n : ℕ) ↦ (fun (m : ℕ) ↦ decide (m = 0)) <$> cf.eval (Nat.pair a n)
Tactic: rcases hf with ⟨cf, rfl⟩
Cleared hypotheses: f_1, pf, hf
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (goal)
Goal:
f : ℕ →. ℕ
cf : Code
pf : Nat.Partrec cf.eval
⊢ ∃ (c : Code), c.eval = fun (a : ℕ) ↦ Nat.rfind fun (n : ℕ) ↦ (fun (m : ℕ) ↦ decide (m = 0)) <$> cf.eval (Nat.pair a n)
have refine_1 : (cf.rfind'.comp (Code.id.pair zero)).eval = fun (a : ℕ) ↦
  Nat.rfind fun (n : ℕ) ↦ (fun (m : ℕ) ↦ decide (m = 0)) <$> cf.eval (Nat.pair a n)
Tactic: refine ⟨comp (rfind' cf) (pair Code.id zero), ?_⟩
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (goal)
Goal:
f : ℕ →. ℕ
h : Nat.Partrec f
⊢ ∃ (c : Code), c.eval = f
have refine_1 : ∃ (c : Code), c.eval = pure 0
Tactic: induction h with
    | zero => exact ⟨zero, rfl⟩
    | succ => exact ⟨succ, rfl⟩
    | left => exact ⟨left, rfl⟩
    | right => exact ⟨right, rfl⟩
    | pair pf pg hf hg =>
      rcases hf with ⟨cf, rfl⟩; rcases hg with ⟨cg, rfl⟩
      exact ⟨pair cf cg, rfl⟩
    | comp pf pg hf hg =>
      rcases hf with ⟨cf, rfl⟩; rcases hg with ⟨cg, rfl⟩
      exact ⟨comp cf cg, rfl⟩
    | prec pf pg hf hg =>
      rcases hf with ⟨cf, rfl⟩; rcases hg with ⟨cg, rfl⟩
      exact ⟨prec cf cg, rfl⟩
    | rfind pf hf =>
      rcases hf with ⟨cf, rfl⟩
      refine ⟨comp (rfind' cf) (pair Code.id zero), ?_⟩
      simp [eval, Seq.seq, pure, PFun.pure, Part.map_id']
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (goal)
Goal:
f : ℕ →. ℕ
h : Nat.Partrec f
refine_1 : ∃ (c : Code), c.eval = pure 0
⊢ ∃ (c : Code), c.eval = f
have refine_1₁ : ∃ (c : Code), c.eval = (↑Nat.succ : ℕ →. ℕ)
Tactic: induction h with
    | zero => exact ⟨zero, rfl⟩
    | succ => exact ⟨succ, rfl⟩
    | left => exact ⟨left, rfl⟩
    | right => exact ⟨right, rfl⟩
    | pair pf pg hf hg =>
      rcases hf with ⟨cf, rfl⟩; rcases hg with ⟨cg, rfl⟩
      exact ⟨pair cf cg, rfl⟩
    | comp pf pg hf hg =>
      rcases hf with ⟨cf, rfl⟩; rcases hg with ⟨cg, rfl⟩
      exact ⟨comp cf cg, rfl⟩
    | prec pf pg hf hg =>
      rcases hf with ⟨cf, rfl⟩; rcases hg with ⟨cg, rfl⟩
      exact ⟨prec cf cg, rfl⟩
    | rfind pf hf =>
      rcases hf with ⟨cf, rfl⟩
      refine ⟨comp (rfind' cf) (pair Code.id zero), ?_⟩
      simp [eval, Seq.seq, pure, PFun.pure, Part.map_id']
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (goal)
Goal:
f : ℕ →. ℕ
h : Nat.Partrec f
refine_1 : ∃ (c : Code), c.eval = pure 0
refine_1₁ : ∃ (c : Code), c.eval = (↑Nat.succ : ℕ →. ℕ)
⊢ ∃ (c : Code), c.eval = f
have refine_1₂ : ∃ (c : Code), c.eval = (↑fun (n : ℕ) ↦ (unpair n).1 : ℕ →. ℕ)
Tactic: induction h with
    | zero => exact ⟨zero, rfl⟩
    | succ => exact ⟨succ, rfl⟩
    | left => exact ⟨left, rfl⟩
    | right => exact ⟨right, rfl⟩
    | pair pf pg hf hg =>
      rcases hf with ⟨cf, rfl⟩; rcases hg with ⟨cg, rfl⟩
      exact ⟨pair cf cg, rfl⟩
    | comp pf pg hf hg =>
      rcases hf with ⟨cf, rfl⟩; rcases hg with ⟨cg, rfl⟩
      exact ⟨comp cf cg, rfl⟩
    | prec pf pg hf hg =>
      rcases hf with ⟨cf, rfl⟩; rcases hg with ⟨cg, rfl⟩
      exact ⟨prec cf cg, rfl⟩
    | rfind pf hf =>
      rcases hf with ⟨cf, rfl⟩
      refine ⟨comp (rfind' cf) (pair Code.id zero), ?_⟩
      simp [eval, Seq.seq, pure, PFun.pure, Part.map_id']
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (goal)
Goal:
f : ℕ →. ℕ
h : Nat.Partrec f
refine_1 : ∃ (c : Code), c.eval = pure 0
refine_1₁ : ∃ (c : Code), c.eval = (↑Nat.succ : ℕ →. ℕ)
refine_1₂ : ∃ (c : Code), c.eval = (↑fun (n : ℕ) ↦ (unpair n).1 : ℕ →. ℕ)
⊢ ∃ (c : Code), c.eval = f
have refine_1₃ : ∃ (c : Code), c.eval = (↑fun (n : ℕ) ↦ (unpair n).2 : ℕ →. ℕ)
Tactic: induction h with
    | zero => exact ⟨zero, rfl⟩
    | succ => exact ⟨succ, rfl⟩
    | left => exact ⟨left, rfl⟩
    | right => exact ⟨right, rfl⟩
    | pair pf pg hf hg =>
      rcases hf with ⟨cf, rfl⟩; rcases hg with ⟨cg, rfl⟩
      exact ⟨pair cf cg, rfl⟩
    | comp pf pg hf hg =>
      rcases hf with ⟨cf, rfl⟩; rcases hg with ⟨cg, rfl⟩
      exact ⟨comp cf cg, rfl⟩
    | prec pf pg hf hg =>
      rcases hf with ⟨cf, rfl⟩; rcases hg with ⟨cg, rfl⟩
      exact ⟨prec cf cg, rfl⟩
    | rfind pf hf =>
      rcases hf with ⟨cf, rfl⟩
      refine ⟨comp (rfind' cf) (pair Code.id zero), ?_⟩
      simp [eval, Seq.seq, pure, PFun.pure, Part.map_id']
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (goal)
Goal:
f : ℕ →. ℕ
h : Nat.Partrec f
refine_1 : ∃ (c : Code), c.eval = pure 0
refine_1₁ : ∃ (c : Code), c.eval = (↑Nat.succ : ℕ →. ℕ)
refine_1₂ : ∃ (c : Code), c.eval = (↑fun (n : ℕ) ↦ (unpair n).1 : ℕ →. ℕ)
refine_1₃ : ∃ (c : Code), c.eval = (↑fun (n : ℕ) ↦ (unpair n).2 : ℕ →. ℕ)
⊢ ∃ (c : Code), c.eval = f
have refine_1₄ : ∀ {f g : ℕ →. ℕ} (pf : Nat.Partrec f) (pg : Nat.Partrec g) (hf : ∃ (c : Code), c.eval = f)
  (hg : ∃ (c : Code), c.eval = g), ∃ (c : Code), c.eval = fun (n : ℕ) ↦ Nat.pair <$> f n <*> g n
Tactic: induction h with
    | zero => exact ⟨zero, rfl⟩
    | succ => exact ⟨succ, rfl⟩
    | left => exact ⟨left, rfl⟩
    | right => exact ⟨right, rfl⟩
    | pair pf pg hf hg =>
      rcases hf with ⟨cf, rfl⟩; rcases hg with ⟨cg, rfl⟩
      exact ⟨pair cf cg, rfl⟩
    | comp pf pg hf hg =>
      rcases hf with ⟨cf, rfl⟩; rcases hg with ⟨cg, rfl⟩
      exact ⟨comp cf cg, rfl⟩
    | prec pf pg hf hg =>
      rcases hf with ⟨cf, rfl⟩; rcases hg with ⟨cg, rfl⟩
      exact ⟨prec cf cg, rfl⟩
    | rfind pf hf =>
      rcases hf with ⟨cf, rfl⟩
      refine ⟨comp (rfind' cf) (pair Code.id zero), ?_⟩
      simp [eval, Seq.seq, pure, PFun.pure, Part.map_id']
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (goal)
Goal:
f : ℕ →. ℕ
h : Nat.Partrec f
refine_1 : ∃ (c : Code), c.eval = pure 0
refine_1₁ : ∃ (c : Code), c.eval = (↑Nat.succ : ℕ →. ℕ)
refine_1₂ : ∃ (c : Code), c.eval = (↑fun (n : ℕ) ↦ (unpair n).1 : ℕ →. ℕ)
refine_1₃ : ∃ (c : Code), c.eval = (↑fun (n : ℕ) ↦ (unpair n).2 : ℕ →. ℕ)
refine_1₄ :
  ∀ {f g : ℕ →. ℕ} (pf : Nat.Partrec f) (pg : Nat.Partrec g) (hf : ∃ (c : Code), c.eval = f)
    (hg : ∃ (c : Code), c.eval = g), ∃ (c : Code), c.eval = fun (n : ℕ) ↦ Nat.pair <$> f n <*> g n
⊢ ∃ (c : Code), c.eval = f
have refine_1₅ : ∀ {f g : ℕ →. ℕ} (pf : Nat.Partrec f) (pg : Nat.Partrec g) (hf : ∃ (c : Code), c.eval = f)
  (hg : ∃ (c : Code), c.eval = g), ∃ (c : Code), c.eval = fun (n : ℕ) ↦ g n >>= f
Tactic: induction h with
    | zero => exact ⟨zero, rfl⟩
    | succ => exact ⟨succ, rfl⟩
    | left => exact ⟨left, rfl⟩
    | right => exact ⟨right, rfl⟩
    | pair pf pg hf hg =>
      rcases hf with ⟨cf, rfl⟩; rcases hg with ⟨cg, rfl⟩
      exact ⟨pair cf cg, rfl⟩
    | comp pf pg hf hg =>
      rcases hf with ⟨cf, rfl⟩; rcases hg with ⟨cg, rfl⟩
      exact ⟨comp cf cg, rfl⟩
    | prec pf pg hf hg =>
      rcases hf with ⟨cf, rfl⟩; rcases hg with ⟨cg, rfl⟩
      exact ⟨prec cf cg, rfl⟩
    | rfind pf hf =>
      rcases hf with ⟨cf, rfl⟩
      refine ⟨comp (rfind' cf) (pair Code.id zero), ?_⟩
      simp [eval, Seq.seq, pure, PFun.pure, Part.map_id']
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Computability.PartrecCode (goal)
Goal:
f : ℕ →. ℕ
h : Nat.Partrec f
refine_1 : ∃ (c : Code), c.eval = pure 0
refine_1₁ : ∃ (c : Code), c.eval = (↑Nat.succ : ℕ →. ℕ)
refine_1₂ : ∃ (c : Code), c.eval = (↑fun (n : ℕ) ↦ (unpair n).1 : ℕ →. ℕ)
refine_1₃ : ∃ (c : Code), c.eval = (↑fun (n : ℕ) ↦ (unpair n).2 : ℕ →. ℕ)
refine_1₄ :
  ∀ {f g : ℕ →. ℕ} (pf : Nat.Partrec f) (pg : Nat.Partrec g) (hf : ∃ (c : Code), c.eval = f)
    (hg : ∃ (c : Code), c.eval = g), ∃ (c : Code), c.eval = fun (n : ℕ) ↦ Nat.pair <$> f n <*> g n
refine_1₅ :
  ∀ {f g : ℕ →. ℕ} (pf : Nat.Partrec f) (pg : Nat.Partrec g) (hf : ∃ (c : Code), c.eval = f)
    (hg : ∃ (c : Code), c.eval = g), ∃ (c : Code), c.eval = fun (n : ℕ) ↦ g n >>= f
⊢ ∃ (c : Code), c.eval = f
have refine_1₆ : ∀ {f g : ℕ →. ℕ} (pf : Nat.Partrec f) (pg : Nat.Partrec g) (hf : ∃ (c : Code), c.eval = f)
  (hg : ∃ (c : Code), c.eval = g),
  ∃ (c : Code),
    c.eval =
      unpaired fun (a n : ℕ) ↦
        Nat.rec (motive := fun (x : ℕ) ↦ Part ℕ) (f a)
          (fun (y : ℕ) (IH : Part ℕ) ↦ do
            let i ← IH
            g (Nat.pair a (Nat.pair y i)))
          n
Tactic: induction h with
    | zero => exact ⟨zero, rfl⟩
    | succ => exact ⟨succ, rfl⟩
    | left => exact ⟨left, rfl⟩
    | right => exact ⟨right, rfl⟩
    | pair pf pg hf hg =>
      rcases hf with ⟨cf, rfl⟩; rcases hg with ⟨cg, rfl⟩
      exact ⟨pair cf cg, rfl⟩
    | comp pf pg hf hg =>
      rcases hf with ⟨cf, rfl⟩; rcases hg with ⟨cg, rfl⟩
      exact ⟨comp cf cg, rfl⟩
    | prec pf pg hf hg =>
      rcases hf with ⟨cf, rfl⟩; rcases hg with ⟨cg, rfl⟩
      exact ⟨prec cf cg, rfl⟩
    | rfind pf hf =>
      rcases hf with ⟨cf, rfl⟩
      refine ⟨comp (rfind' cf) (pair Code.id zero), ?_⟩
      simp [eval, Seq.seq, pure, PFun.pure, Part.map_id']
Cleared hypotheses: h