awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Computability.PartrecCode
Goal:
cf cg : Code
simp :
  cf.encodeCode < 2 * (2 * Nat.pair cf.encodeCode cg.encodeCode) + 4 ∧
    cg.encodeCode < 2 * (2 * Nat.pair cf.encodeCode cg.encodeCode) + 4
⊢ encode cf < encode (cf.pair cg) ∧ encode cg < encode (cf.pair cg)

Tactic:
simp only [encodeCode_eq, encodeCode]

Premises used: Nat.Partrec.Code.encodeCode, Nat.Partrec.Code.encodeCode_eq
-- Module: Mathlib.Computability.PartrecCode
Goal:
cf cg : Code
⊢ 1 ≤ HMul.hMul (α := ℕ) 2 2

Tactic:
decide
-- Module: Mathlib.Computability.PartrecCode
Goal:
cf cg : Code
⊢ 1 * Nat.pair cf.encodeCode cg.encodeCode ≤ HMul.hMul (α := ℕ) 2 2 * Nat.pair cf.encodeCode cg.encodeCode

Tactic:
have := Nat.mul_le_mul_right (Nat.pair cf.encodeCode cg.encodeCode) (by decide : 1 ≤ 2 * 2)
-- Module: Mathlib.Computability.PartrecCode
Goal:
cf cg : Code
this : 1 * Nat.pair cf.encodeCode cg.encodeCode ≤ HMul.hMul (α := ℕ) 2 2 * Nat.pair cf.encodeCode cg.encodeCode
⊢ Nat.pair cf.encodeCode cg.encodeCode ≤ 2 * (2 * Nat.pair cf.encodeCode cg.encodeCode)

Tactic:
rw [one_mul, mul_assoc] at this

Premises used: mul_assoc, one_mul
-- Module: Mathlib.Computability.PartrecCode
Goal:
cf cg : Code
this : Nat.pair cf.encodeCode cg.encodeCode ≤ 2 * (2 * Nat.pair cf.encodeCode cg.encodeCode)
⊢ LT.lt (α := ℕ) 0 4

Tactic:
decide
-- Module: Mathlib.Computability.PartrecCode
Goal:
cf cg : Code
this : Nat.pair cf.encodeCode cg.encodeCode ≤ 2 * (2 * Nat.pair cf.encodeCode cg.encodeCode)
⊢ Nat.pair cf.encodeCode cg.encodeCode < 2 * (2 * Nat.pair cf.encodeCode cg.encodeCode) + 4

Tactic:
have := lt_of_le_of_lt this (lt_add_of_pos_right _ (by decide : 0 < 4))
-- Module: Mathlib.Computability.PartrecCode
Goal:
cf cg : Code
this_1 : Nat.pair cf.encodeCode cg.encodeCode ≤ 2 * (2 * Nat.pair cf.encodeCode cg.encodeCode)
this : Nat.pair cf.encodeCode cg.encodeCode < 2 * (2 * Nat.pair cf.encodeCode cg.encodeCode) + 4
⊢ cf.encodeCode < 2 * (2 * Nat.pair cf.encodeCode cg.encodeCode) + 4 ∧
    cg.encodeCode < 2 * (2 * Nat.pair cf.encodeCode cg.encodeCode) + 4

Tactic:
⟨lt_of_le_of_lt (Nat.left_le_pair _ _) this, lt_of_le_of_lt (Nat.right_le_pair _ _) this⟩

Premises used: lt_of_le_of_lt, Nat.left_le_pair, Nat.right_le_pair, And.intro
-- Module: Mathlib.Computability.PartrecCode
Goal:
cf cg : Code
this_1 : Nat.pair cf.encodeCode cg.encodeCode ≤ 2 * (2 * Nat.pair cf.encodeCode cg.encodeCode)
this : Nat.pair cf.encodeCode cg.encodeCode < 2 * (2 * Nat.pair cf.encodeCode cg.encodeCode) + 4
⊢ cf.encodeCode < 2 * (2 * Nat.pair cf.encodeCode cg.encodeCode) + 4 ∧
    cg.encodeCode < 2 * (2 * Nat.pair cf.encodeCode cg.encodeCode) + 4

Tactic:
exact ⟨lt_of_le_of_lt (Nat.left_le_pair _ _) this, lt_of_le_of_lt (Nat.right_le_pair _ _) this⟩
-- Module: Mathlib.Computability.PartrecCode
Goal:
cf cg : Code
⊢ encode (cf.pair cg) < encode (cf.comp cg)

Tactic:
simp [encodeCode_eq, encodeCode]

Premises used: Nat.Partrec.Code.encodeCode, Nat.Partrec.Code.encodeCode_eq
-- Module: Mathlib.Computability.PartrecCode
Goal:
cf cg : Code
⊢ encode (cf.pair cg) < encode (cf.comp cg)

Tactic:
have : encode (pair cf cg) < encode (comp cf cg) := by simp [encodeCode_eq, encodeCode]
-- Module: Mathlib.Computability.PartrecCode
Goal:
cf cg : Code
this : encode (cf.pair cg) < encode (cf.comp cg)
⊢ encode cf < encode (cf.comp cg) ∧ encode cg < encode (cf.comp cg)

Tactic:
(encode_lt_pair cf cg).imp (fun h => lt_trans h this) fun h => lt_trans h this

Premises used: And.imp, lt_trans, Nat.Partrec.Code.encode_lt_pair
-- Module: Mathlib.Computability.PartrecCode
Goal:
cf cg : Code
this : encode (cf.pair cg) < encode (cf.comp cg)
⊢ encode cf < encode (cf.comp cg) ∧ encode cg < encode (cf.comp cg)

Tactic:
exact (encode_lt_pair cf cg).imp (fun h => lt_trans h this) fun h => lt_trans h this

Premises used: And.imp, lt_trans, Nat.Partrec.Code.encode_lt_pair
-- Module: Mathlib.Computability.PartrecCode
Goal:
cf cg : Code
⊢ encode (cf.pair cg) < encode (cf.prec cg)

Tactic:
simp [encodeCode_eq, encodeCode]

Premises used: Nat.Partrec.Code.encodeCode, Nat.Partrec.Code.encodeCode_eq
-- Module: Mathlib.Computability.PartrecCode
Goal:
cf cg : Code
⊢ encode (cf.pair cg) < encode (cf.prec cg)

Tactic:
have : encode (pair cf cg) < encode (prec cf cg) := by simp [encodeCode_eq, encodeCode]
-- Module: Mathlib.Computability.PartrecCode
Goal:
cf cg : Code
this : encode (cf.pair cg) < encode (cf.prec cg)
⊢ encode cf < encode (cf.prec cg) ∧ encode cg < encode (cf.prec cg)

Tactic:
(encode_lt_pair cf cg).imp (fun h => lt_trans h this) fun h => lt_trans h this

Premises used: And.imp, lt_trans, Nat.Partrec.Code.encode_lt_pair
-- Module: Mathlib.Computability.PartrecCode
Goal:
cf cg : Code
this : encode (cf.pair cg) < encode (cf.prec cg)
⊢ encode cf < encode (cf.prec cg) ∧ encode cg < encode (cf.prec cg)

Tactic:
exact (encode_lt_pair cf cg).imp (fun h => lt_trans h this) fun h => lt_trans h this

Premises used: And.imp, lt_trans, Nat.Partrec.Code.encode_lt_pair
-- Module: Mathlib.Computability.PartrecCode
Goal:
cf : Code
simp : cf.encodeCode < 2 * (2 * cf.encodeCode + 1) + 1 + 4
⊢ encode cf < encode cf.rfind'

Tactic:
simp only [encodeCode_eq, encodeCode]

Premises used: Nat.Partrec.Code.encodeCode, Nat.Partrec.Code.encodeCode_eq
-- Module: Mathlib.Computability.PartrecCode
Goal:
cf : Code
⊢ cf.encodeCode < 2 * (2 * cf.encodeCode + 1) + 1 + 4

Tactic:
lia
-- Module: Mathlib.Computability.PartrecCode
Goal:
⊢ Primrec₂ pair

Tactic:
Primrec₂.ofNat_iff.2 <|
    Primrec₂.encode_iff.1 <|
      nat_add.comp
        (nat_double.comp <|
          nat_double.comp <|
            Primrec₂.natPair.comp (encode_iff.2 <| (Primrec.ofNat Code).comp fst)
              (encode_iff.2 <| (Primrec.ofNat Code).comp snd))
        (Primrec₂.const 4)

Premises used: Iff.mpr, Primrec.nat_double, Primrec.nat_add, Primrec.snd, Primrec₂.encode_iff, Nat.Partrec.Code, Primrec.fst, Primrec.encode_iff, Primrec₂.const, Primrec₂.ofNat_iff, Primrec.comp, Primrec₂.natPair, Iff.mp, Primrec₂.comp, OfNat.ofNat, Primrec.ofNat
-- Module: Mathlib.Computability.PartrecCode
Goal:
⊢ Primrec₂ comp

Tactic:
Primrec₂.ofNat_iff.2 <|
    Primrec₂.encode_iff.1 <|
      nat_add.comp
        (nat_double.comp <|
          nat_double_succ.comp <|
            Primrec₂.natPair.comp (encode_iff.2 <| (Primrec.ofNat Code).comp fst)
              (encode_iff.2 <| (Primrec.ofNat Code).comp snd))
        (Primrec₂.const 4)

Premises used: Iff.mpr, Primrec.nat_double, Primrec.nat_add, Primrec.snd, Primrec₂.encode_iff, Nat.Partrec.Code, Primrec.fst, Primrec.encode_iff, Primrec₂.const, Primrec₂.ofNat_iff, Primrec.nat_double_succ, Primrec.comp, Primrec₂.natPair, Iff.mp, Primrec₂.comp, OfNat.ofNat, Primrec.ofNat
-- Module: Mathlib.Computability.PartrecCode
Goal:
⊢ Primrec₂ prec

Tactic:
Primrec₂.ofNat_iff.2 <|
    Primrec₂.encode_iff.1 <|
      nat_add.comp
        (nat_double_succ.comp <|
          nat_double.comp <|
            Primrec₂.natPair.comp (encode_iff.2 <| (Primrec.ofNat Code).comp fst)
              (encode_iff.2 <| (Primrec.ofNat Code).comp snd))
        (Primrec₂.const 4)

Premises used: Iff.mpr, Primrec.nat_double, Primrec.nat_add, Primrec.snd, Primrec₂.encode_iff, Nat.Partrec.Code, Primrec.fst, Primrec.encode_iff, Primrec₂.const, Primrec₂.ofNat_iff, Primrec.nat_double_succ, Primrec.comp, Primrec₂.natPair, Iff.mp, Primrec₂.comp, OfNat.ofNat, Primrec.ofNat
-- Module: Mathlib.Computability.PartrecCode
Goal:
⊢ Primrec rfind'

Tactic:
ofNat_iff.2 <|
    encode_iff.1 <|
      nat_add.comp
        (nat_double_succ.comp <| nat_double_succ.comp <|
          encode_iff.2 <| Primrec.ofNat Code)
        (const 4)

Premises used: Iff.mpr, Primrec.nat_add, Nat.Partrec.Code, Primrec.const, Primrec.encode_iff, Primrec.nat_double_succ, Primrec.comp, Iff.mp, Primrec₂.comp, OfNat.ofNat, Primrec.ofNat_iff, Primrec.ofNat
-- Module: Mathlib.Computability.PartrecCode
Goal:
α : Type u_1
σ : Type u_2
inst : Primcodable α
inst_1 : Primcodable σ
c : α → Code
hc : Primrec c
z : α → σ
hz : Primrec z
s : α → σ
hs : Primrec s
l : α → σ
hl : Primrec l
r : α → σ
hr : Primrec r
pr : α → Code × Code × σ × σ → σ
hpr : Primrec₂ pr
co : α → Code × Code × σ × σ → σ
hco : Primrec₂ co
pc : α → Code × Code × σ × σ → σ
hpc : Primrec₂ pc
rf : α → Code × σ → σ
hrf : Primrec₂ rf
PR : (a : α) → (cf cg : Code) → (hf hg : σ) → σ := fun (a : α) (cf cg : Code) (hf hg : σ) ↦ pr a (cf, cg, hf, hg)
_ :
  let CO : (a : α) → (cf cg : Code) → (hf hg : σ) → σ := fun (a : α) (cf cg : Code) (hf hg : σ) ↦ co a (cf, cg, hf, hg);
  let PC : (a : α) → (cf cg : Code) → (hf hg : σ) → σ := fun (a : α) (cf cg : Code) (hf hg : σ) ↦ pc a (cf, cg, hf, hg);
  let RF : (a : α) → (cf : Code) → (hf : σ) → σ := fun (a : α) (cf : Code) (hf : σ) ↦ rf a (cf, hf);
  let 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);
  Primrec.{u_1, u_2} (β := σ) fun (a : α) ↦ F a (c a)
⊢ let CO : (a : α) → (cf cg : Code) → (hf hg : σ) → σ := fun (a : α) (cf cg : Code) (hf hg : σ) ↦ co a (cf, cg, hf, hg);
  let PC : (a : α) → (cf cg : Code) → (hf hg : σ) → σ := fun (a : α) (cf cg : Code) (hf hg : σ) ↦ pc a (cf, cg, hf, hg);
  let RF : (a : α) → (cf : Code) → (hf : σ) → σ := fun (a : α) (cf : Code) (hf : σ) ↦ rf a (cf, hf);
  let 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);
  Primrec.{u_1, u_2} (β := σ) fun (a : α) ↦ F a (c a)

Tactic:
_
-- Module: Mathlib.Computability.PartrecCode
Goal:
α : Type u_1
σ : Type u_2
inst : Primcodable α
inst_1 : Primcodable σ
c : α → Code
hc : Primrec c
z : α → σ
hz : Primrec z
s : α → σ
hs : Primrec s
l : α → σ
hl : Primrec l
r : α → σ
hr : Primrec r
pr : α → Code × Code × σ × σ → σ
hpr : Primrec₂ pr
co : α → Code × Code × σ × σ → σ
hco : Primrec₂ co
pc : α → Code × Code × σ × σ → σ
hpc : Primrec₂ pc
rf : α → Code × σ → σ
hrf : Primrec₂ 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)
_ :
  let PC : (a : α) → (cf cg : Code) → (hf hg : σ) → σ := fun (a : α) (cf cg : Code) (hf hg : σ) ↦ pc a (cf, cg, hf, hg);
  let RF : (a : α) → (cf : Code) → (hf : σ) → σ := fun (a : α) (cf : Code) (hf : σ) ↦ rf a (cf, hf);
  let 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);
  Primrec.{u_1, u_2} (β := σ) fun (a : α) ↦ F a (c a)
⊢ let PC : (a : α) → (cf cg : Code) → (hf hg : σ) → σ := fun (a : α) (cf cg : Code) (hf hg : σ) ↦ pc a (cf, cg, hf, hg);
  let RF : (a : α) → (cf : Code) → (hf : σ) → σ := fun (a : α) (cf : Code) (hf : σ) ↦ rf a (cf, hf);
  let 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);
  Primrec.{u_1, u_2} (β := σ) fun (a : α) ↦ F a (c a)

Tactic:
_
-- Module: Mathlib.Computability.PartrecCode
Goal:
α : Type u_1
σ : Type u_2
inst : Primcodable α
inst_1 : Primcodable σ
c : α → Code
hc : Primrec c
z : α → σ
hz : Primrec z
s : α → σ
hs : Primrec s
l : α → σ
hl : Primrec l
r : α → σ
hr : Primrec r
pr : α → Code × Code × σ × σ → σ
hpr : Primrec₂ pr
co : α → Code × Code × σ × σ → σ
hco : Primrec₂ co
pc : α → Code × Code × σ × σ → σ
hpc : Primrec₂ pc
rf : α → Code × σ → σ
hrf : Primrec₂ 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)
_ :
  let RF : (a : α) → (cf : Code) → (hf : σ) → σ := fun (a : α) (cf : Code) (hf : σ) ↦ rf a (cf, hf);
  let 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);
  Primrec.{u_1, u_2} (β := σ) fun (a : α) ↦ F a (c a)
⊢ let RF : (a : α) → (cf : Code) → (hf : σ) → σ := fun (a : α) (cf : Code) (hf : σ) ↦ rf a (cf, hf);
  let 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);
  Primrec.{u_1, u_2} (β := σ) fun (a : α) ↦ F a (c a)

Tactic:
_
-- Module: Mathlib.Computability.PartrecCode
Goal:
α : Type u_1
σ : Type u_2
inst : Primcodable α
inst_1 : Primcodable σ
c : α → Code
hc : Primrec c
z : α → σ
hz : Primrec z
s : α → σ
hs : Primrec s
l : α → σ
hl : Primrec l
r : α → σ
hr : Primrec r
pr : α → Code × Code × σ × σ → σ
hpr : Primrec₂ pr
co : α → Code × Code × σ × σ → σ
hco : Primrec₂ co
pc : α → Code × Code × σ × σ → σ
hpc : Primrec₂ pc
rf : α → Code × σ → σ
hrf : Primrec₂ 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 : Primrec 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)
⊢ Primrec₂ G

Tactic:
have : Primrec₂ G := .mk <|
    nat_casesOn (list_length.comp snd) (option_some_iff.2 (hz.comp fst)) <| .mk <|
    nat_casesOn snd (option_some_iff.2 (hs.comp (fst.comp fst))) <| .mk <|
    nat_casesOn snd (option_some_iff.2 (hl.comp (fst.comp <| fst.comp fst))) <| .mk <|
    nat_casesOn snd (option_some_iff.2 (hr.comp (fst.comp <| fst.comp <| fst.comp fst))) <| .mk <|
    this.comp <|
      ((fst.pair snd).comp <| fst.comp <| fst.comp <| fst.comp <| fst).pair <|
      snd.pair <| nat_div2.comp <| nat_div2.comp snd
-- Module: Mathlib.Computability.PartrecCode
Goal:
α : Type u_1
σ : Type u_2
inst : Primcodable α
inst_1 : Primcodable σ
c : α → Code
hc : Primrec c
z : α → σ
hz : Primrec z
s : α → σ
hs : Primrec s
l : α → σ
hl : Primrec l
r : α → σ
hr : Primrec r
pr : α → Code × Code × σ × σ → σ
hpr : Primrec₂ pr
co : α → Code × Code × σ × σ → σ
hco : Primrec₂ co
pc : α → Code × Code × σ × σ → σ
hpc : Primrec₂ pc
rf : α → Code × σ → σ
hrf : Primrec₂ 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 : Primrec 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 : Primrec₂ G
a : α
⊢ F (id a) (ofNat Code (encode (c a))) = F a (c a)

Tactic:
simp
-- Module: Mathlib.Computability.PartrecCode
Goal:
α : Type u_1
σ : Type u_2
inst : Primcodable α
inst_1 : Primcodable σ
c : α → Code
hc : Primrec c
z : α → σ
hz : Primrec z
s : α → σ
hs : Primrec s
l : α → σ
hl : Primrec l
r : α → σ
hr : Primrec r
pr : α → Code × Code × σ × σ → σ
hpr : Primrec₂ pr
co : α → Code × Code × σ × σ → σ
hco : Primrec₂ co
pc : α → Code × Code × σ × σ → σ
hpc : Primrec₂ pc
rf : α → Code × σ → σ
hrf : Primrec₂ 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 : Primrec 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 : Primrec₂ G
refine :
  ∀ (a : α) (n : ℕ),
    G (a, List.map ((fun (a : α) (n : ℕ) ↦ F a (ofNat Code n)) a) (List.range n)).1
        (a, List.map ((fun (a : α) (n : ℕ) ↦ F a (ofNat Code n)) a) (List.range n)).2 =
      some ((fun (a : α) (n : ℕ) ↦ F a (ofNat Code n)) a n)
⊢ Primrec.{u_1, u_2} (β := σ) fun (a : α) ↦ F a (c a)

Tactic:
refine (nat_strong_rec (fun a n => F a (ofNat Code n)) this.to₂ fun a n => ?_)
    |>.comp .id (encode_iff.2 hc) |>.of_eq fun a => by simp

Premises used: Iff.mpr, Primrec.of_eq, Nat.Partrec.Code, Primrec.encode_iff, Primrec.nat_strong_rec, Primrec₂.comp, Primrec.id, Primrec.to₂, Denumerable.ofNat
-- Module: Mathlib.Computability.PartrecCode
Goal:
α : Type u_1
σ : Type u_2
inst : Primcodable α
inst_1 : Primcodable σ
c : α → Code
hc : Primrec c
z : α → σ
hz : Primrec z
s : α → σ
hs : Primrec s
l : α → σ
hl : Primrec l
r : α → σ
hr : Primrec r
pr : α → Code × Code × σ × σ → σ
hpr : Primrec₂ pr
co : α → Code × Code × σ × σ → σ
hco : Primrec₂ co
pc : α → Code × Code × σ × σ → σ
hpc : Primrec₂ pc
rf : α → Code × σ → σ
hrf : Primrec₂ 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 : Primrec 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 : Primrec₂ G
a : α
n : ℕ
zero :
  G (a, List.map ((fun (a : α) (n : ℕ) ↦ F a (ofNat Code n)) a) (List.range 0)).1
      (a, List.map ((fun (a : α) (n : ℕ) ↦ F a (ofNat Code n)) a) (List.range 0)).2 =
    some ((fun (a : α) (n : ℕ) ↦ F a (ofNat Code n)) a 0)
succ :
  ∀ (n : ℕ),
    G (a, List.map ((fun (a : α) (n : ℕ) ↦ F a (ofNat Code n)) a) (List.range (n + 1))).1
        (a, List.map ((fun (a : α) (n : ℕ) ↦ F a (ofNat Code n)) a) (List.range (n + 1))).2 =
      some ((fun (a : α) (n : ℕ) ↦ F a (ofNat Code n)) a (n + 1))
⊢ G (a, List.map ((fun (a : α) (n : ℕ) ↦ F a (ofNat Code n)) a) (List.range n)).1
      (a, List.map ((fun (a : α) (n : ℕ) ↦ F a (ofNat Code n)) a) (List.range n)).2 =
    some ((fun (a : α) (n : ℕ) ↦ F a (ofNat Code n)) a n)

Tactic:
rcases n with - | n