-- Mathlib/Computability/Partrec.lean
theorem nat_rec {f : α → ℕ} {g : α →. σ} {h : α → ℕ × σ →. σ} (hf : Computable f) (hg : Partrec g)
    (hh : Partrec₂ h) : Partrec fun a => (f a).rec (g a) fun y IH => IH.bind fun i => h a (y, i) :=
  (Nat.Partrec.prec' hf hg hh).of_eq fun n => by
    rcases e : decode (α := α) n with - | a <;> simp [e]
    induction' f a with m IH <;> simp
    rw [IH, Part.bind_map]
    congr; funext s
    simp [encodek]

Proof state:
case some.succ.e_g.h
α : Type u_1
σ : Type u_3
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f : α → ℕ
g : α →. σ
h : α → ℕ × σ →. σ
hf : Computable f
hg : Partrec g
hh : Partrec₂ h
n : ℕ
a : α
e : decode n = Option.some a
m : ℕ
IH :
  Nat.rec (Part.map encode (g a))
      (fun y IH =>
        IH.bind fun i => (↑(Option.map (Prod.mk a ∘ Prod.mk y) (decode i))).bind fun a => Part.map encode (h a.1 a.2))
      m =
    Part.map encode (Nat.rec (g a) (fun y IH => IH.bind fun i => h a (y, i)) m)
s : σ
⊢ ((↑(Option.map (Prod.mk a ∘ Prod.mk m) (decode (encode s)))).bind fun a => Part.map encode (h a.1 a.2)) =
    Part.map encode (h a (m, s))

Tactic:
simp [encodek]

Result:
no goals

Proof state:
case some
α : Type u_1
σ : Type u_3
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f : α → ℕ
g : α →. σ
h : α → ℕ × σ →. σ
hf : Computable f
hg : Partrec g
hh : Partrec₂ h
n : ℕ
a : α
e : decode n = Option.some a
⊢ Nat.rec (Part.map encode (g a))
      (fun y IH =>
        IH.bind fun i => (↑(Option.map (Prod.mk a ∘ Prod.mk y) (decode i))).bind fun a => Part.map encode (h a.1 a.2))
      (f a) =
    Part.map encode (Nat.rec (g a) (fun y IH => IH.bind fun i => h a (y, i)) (f a))

Tactic:
induction' f a with m IH <;> simp

Result:
case some.succ
α : Type u_1
σ : Type u_3
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f : α → ℕ
g : α →. σ
h : α → ℕ × σ →. σ
hf : Computable f
hg : Partrec g
hh : Partrec₂ h
n : ℕ
a : α
e : decode n = Option.some a
m : ℕ
IH :
  Nat.rec (Part.map encode (g a))
      (fun y IH =>
        IH.bind fun i => (↑(Option.map (Prod.mk a ∘ Prod.mk y) (decode i))).bind fun a => Part.map encode (h a.1 a.2))
      m =
    Part.map encode (Nat.rec (g a) (fun y IH => IH.bind fun i => h a (y, i)) m)
⊢ ((Nat.rec (Part.map encode (g a))
          (fun y IH =>
            IH.bind fun i =>
              (↑(Option.map (Prod.mk a ∘ Prod.mk y) (decode i))).bind fun a => Part.map encode (h a.1 a.2))
          m).bind
      fun i => (↑(Option.map (Prod.mk a ∘ Prod.mk m) (decode i))).bind fun a => Part.map encode (h a.1 a.2)) =
    (Nat.rec (g a) (fun y IH => IH.bind fun i => h a (y, i)) m).bind fun y => Part.map encode (h a (m, y))

Proof state:
case some.succ
α : Type u_1
σ : Type u_3
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f : α → ℕ
g : α →. σ
h : α → ℕ × σ →. σ
hf : Computable f
hg : Partrec g
hh : Partrec₂ h
n : ℕ
a : α
e : decode n = Option.some a
m : ℕ
IH :
  Nat.rec (Part.map encode (g a))
      (fun y IH =>
        IH.bind fun i => (↑(Option.map (Prod.mk a ∘ Prod.mk y) (decode i))).bind fun a => Part.map encode (h a.1 a.2))
      m =
    Part.map encode (Nat.rec (g a) (fun y IH => IH.bind fun i => h a (y, i)) m)
⊢ ((Nat.rec (Part.map encode (g a))
          (fun y IH =>
            IH.bind fun i =>
              (↑(Option.map (Prod.mk a ∘ Prod.mk y) (decode i))).bind fun a => Part.map encode (h a.1 a.2))
          m).bind
      fun i => (↑(Option.map (Prod.mk a ∘ Prod.mk m) (decode i))).bind fun a => Part.map encode (h a.1 a.2)) =
    (Nat.rec (g a) (fun y IH => IH.bind fun i => h a (y, i)) m).bind fun y => Part.map encode (h a (m, y))

Tactic:
rw [IH, Part.bind_map]

Result:
case some.succ
α : Type u_1
σ : Type u_3
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f : α → ℕ
g : α →. σ
h : α → ℕ × σ →. σ
hf : Computable f
hg : Partrec g
hh : Partrec₂ h
n : ℕ
a : α
e : decode n = Option.some a
m : ℕ
IH :
  Nat.rec (Part.map encode (g a))
      (fun y IH =>
        IH.bind fun i => (↑(Option.map (Prod.mk a ∘ Prod.mk y) (decode i))).bind fun a => Part.map encode (h a.1 a.2))
      m =
    Part.map encode (Nat.rec (g a) (fun y IH => IH.bind fun i => h a (y, i)) m)
⊢ ((Nat.rec (g a) (fun y IH => IH.bind fun i => h a (y, i)) m).bind fun y =>
      (↑(Option.map (Prod.mk a ∘ Prod.mk m) (decode (encode y)))).bind fun a => Part.map encode (h a.1 a.2)) =
    (Nat.rec (g a) (fun y IH => IH.bind fun i => h a (y, i)) m).bind fun y => Part.map encode (h a (m, y))

Proof state:
case some.succ.e_g
α : Type u_1
σ : Type u_3
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f : α → ℕ
g : α →. σ
h : α → ℕ × σ →. σ
hf : Computable f
hg : Partrec g
hh : Partrec₂ h
n : ℕ
a : α
e : decode n = Option.some a
m : ℕ
IH :
  Nat.rec (Part.map encode (g a))
      (fun y IH =>
        IH.bind fun i => (↑(Option.map (Prod.mk a ∘ Prod.mk y) (decode i))).bind fun a => Part.map encode (h a.1 a.2))
      m =
    Part.map encode (Nat.rec (g a) (fun y IH => IH.bind fun i => h a (y, i)) m)
⊢ (fun y => (↑(Option.map (Prod.mk a ∘ Prod.mk m) (decode (encode y)))).bind fun a => Part.map encode (h a.1 a.2)) =
    fun y => Part.map encode (h a (m, y))

Tactic:
funext s

Result:
case some.succ.e_g.h
α : Type u_1
σ : Type u_3
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f : α → ℕ
g : α →. σ
h : α → ℕ × σ →. σ
hf : Computable f
hg : Partrec g
hh : Partrec₂ h
n : ℕ
a : α
e : decode n = Option.some a
m : ℕ
IH :
  Nat.rec (Part.map encode (g a))
      (fun y IH =>
        IH.bind fun i => (↑(Option.map (Prod.mk a ∘ Prod.mk y) (decode i))).bind fun a => Part.map encode (h a.1 a.2))
      m =
    Part.map encode (Nat.rec (g a) (fun y IH => IH.bind fun i => h a (y, i)) m)
s : σ
⊢ ((↑(Option.map (Prod.mk a ∘ Prod.mk m) (decode (encode s)))).bind fun a => Part.map encode (h a.1 a.2)) =
    Part.map encode (h a (m, s))

Proof state:
α : Type u_1
σ : Type u_3
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f : α → ℕ
g : α →. σ
h : α → ℕ × σ →. σ
hf : Computable f
hg : Partrec g
hh : Partrec₂ h
n : ℕ
⊢ (((↑(decode n)).bind fun a => Part.map encode (↑f a)).bind fun n_1 =>
      Nat.rec ((↑(decode n)).bind fun a => Part.map encode (g a))
        (fun y IH => do
          let i ← IH
          (↑(decode (Nat.pair n (Nat.pair y i)))).bind fun a => Part.map encode ((fun p => h p.1 p.2) a))
        n_1) =
    (↑(decode n)).bind fun a =>
      Part.map encode ((fun a => Nat.rec (g a) (fun y IH => IH.bind fun i => h a (y, i)) (f a)) a)

Tactic:
rcases e : decode (α := α) n with - | a <;> simp [e]

Result:
case some
α : Type u_1
σ : Type u_3
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f : α → ℕ
g : α →. σ
h : α → ℕ × σ →. σ
hf : Computable f
hg : Partrec g
hh : Partrec₂ h
n : ℕ
a : α
e : decode n = Option.some a
⊢ Nat.rec (Part.map encode (g a))
      (fun y IH =>
        IH.bind fun i => (↑(Option.map (Prod.mk a ∘ Prod.mk y) (decode i))).bind fun a => Part.map encode (h a.1 a.2))
      (f a) =
    Part.map encode (Nat.rec (g a) (fun y IH => IH.bind fun i => h a (y, i)) (f a))