-- Mathlib/Computability/PartrecCode.lean
theorem rec_computable {α σ} [Primcodable α] [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) :
    let PR (a) cf cg hf hg := pr a (cf, cg, hf, hg)
    let CO (a) cf cg hf hg := co a (cf, cg, hf, hg)
    let PC (a) cf cg hf hg := pc a (cf, cg, hf, hg)
    let RF (a) cf hf := rf a (cf, hf)
    let F (a : α) (c : Code) : σ :=
      Nat.Partrec.Code.recOn c (z a) (s a) (l a) (r a) (PR a) (CO a) (PC a) (RF a)
    Computable fun a => F a (c a)

Proof state:
case succ.succ.succ.zero
α : Type u_1
σ : Type u_2
inst✝¹ : Primcodable α
inst✝ : 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✝ : α → Code → Code → σ → σ → σ := fun a cf cg hf hg => pr a (cf, cg, hf, hg)
CO✝ : α → Code → Code → σ → σ → σ := fun a cf cg hf hg => co a (cf, cg, hf, hg)
PC✝ : α → Code → Code → σ → σ → σ := fun a cf cg hf hg => pc a (cf, cg, hf, hg)
RF✝ : α → Code → σ → σ := fun a cf hf => rf a (cf, hf)
F : α → Code → σ := fun a c => Code.recOn c (z a) (s a) (l a) (r a) (PR✝ a) (CO✝ a) (PC✝ a) (RF✝ a)
G₁ : (α × List σ) × ℕ × ℕ → Option σ :=
  fun p =>
    (p.1.2.get? p.2.2).bind fun s =>
      (p.1.2.get? (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₂))
          (p.1.2.get? (unpair p.2.2).2)
this✝ : Computable G₁
G : α → List σ → Option σ :=
  fun a IH =>
    Nat.casesOn IH.length (some (z a)) fun n =>
      Nat.casesOn n (some (s a)) fun n =>
        Nat.casesOn n (some (l a)) fun n => Nat.casesOn n (some (r a)) fun n => G₁ ((a, IH), n, n.div2.div2)
this : Computable₂ G
a : α
⊢ G a (List.map (fun n => F a (ofNatCode n)) (List.range 3)) = some (F a right)

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
σ : Type u_2
inst✝¹ : Primcodable α
inst✝ : 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✝ : α → Code → Code → σ → σ → σ := fun a cf cg hf hg => pr a (cf, cg, hf, hg)
CO✝ : α → Code → Code → σ → σ → σ := fun a cf cg hf hg => co a (cf, cg, hf, hg)
PC✝ : α → Code → Code → σ → σ → σ := fun a cf cg hf hg => pc a (cf, cg, hf, hg)
RF✝ : α → Code → σ → σ := fun a cf hf => rf a (cf, hf)
F : α → Code → σ := fun a c => Code.recOn c (z a) (s a) (l a) (r a) (PR✝ a) (CO✝ a) (PC✝ a) (RF✝ a)
⊢ Computable fun a => F a (c a)

Tactic:
let G₁ : (α × List σ) × ℕ × ℕ → Option σ := fun p =>
  letI a := p.1.1; letI IH := p.1.2; letI n := p.2.1; letI m := p.2.2
  (IH.get? m).bind fun s =>
  (IH.get? m.unpair.1).bind fun s₁ =>
  (IH.get? m.unpair.2).map fun s₂ =>
  cond n.bodd
    (cond n.div2.bodd (rf a (ofNat Code m, s))
      (pc a (ofNat Code m.unpair.1, ofNat Code m.unpair.2, s₁, s₂)))
    (cond n.div2.bodd (co a (ofNat Code m.unpair.1, ofNat Code m.unpair.2, s₁, s₂))
      (pr a (ofNat Code m.unpair.1, ofNat Code m.unpair.2, s₁, s₂)))

Result:
α : Type u_1
σ : Type u_2
inst✝¹ : Primcodable α
inst✝ : 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✝ : α → Code → Code → σ → σ → σ := fun a cf cg hf hg => pr a (cf, cg, hf, hg)
CO✝ : α → Code → Code → σ → σ → σ := fun a cf cg hf hg => co a (cf, cg, hf, hg)
PC✝ : α → Code → Code → σ → σ → σ := fun a cf cg hf hg => pc a (cf, cg, hf, hg)
RF✝ : α → Code → σ → σ := fun a cf hf => rf a (cf, hf)
F : α → Code → σ := fun a c => Code.recOn c (z a) (s a) (l a) (r a) (PR✝ a) (CO✝ a) (PC✝ a) (RF✝ a)
G₁ : (α × List σ) × ℕ × ℕ → Option σ :=
  fun p =>
    (p.1.2.get? p.2.2).bind fun s =>
      (p.1.2.get? (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₂))
          (p.1.2.get? (unpair p.2.2).2)
⊢ Computable fun a => F a (c a)