-- 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 a n => F a (ofNat Code n)) a) (List.range (0 + 1 + 1 + 1))).1
      (a, List.map ((fun a n => F a (ofNat Code n)) a) (List.range (0 + 1 + 1 + 1))).2 =
    some ((fun a n => F a (ofNat Code n)) a (0 + 1 + 1 + 1))

Tactic:
simp [ofNatCode_eq, ofNatCode]

Result:
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)

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)
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 : α
n : ℕ
m : ℕ := n.div2.div2
⊢ n / 2 / 2 < n + 4

Tactic:
exact lt_of_le_of_lt
  (le_trans (Nat.div_le_self ..) (Nat.div_le_self ..))
  (Nat.succ_le_succ (Nat.le_add_right ..))

Result:
no goals