-- Mathlib/Computability/Primrec.lean
theorem nat_rec {f : α → β} {g : α → ℕ × β → β} (hf : Primrec f) (hg : Primrec₂ g) :
    Primrec₂ fun a (n : ℕ) => n.rec (motive := fun _ => β) (f a) fun n IH => g a (n, IH) :=
  Primrec₂.nat_iff.2 <|
    ((Nat.Primrec.casesOn' .zero <|
              (Nat.Primrec.prec hf <|
                    .comp hg <|
                      Nat.Primrec.left.pair <|
                        (Nat.Primrec.left.comp .right).pair <|
                          Nat.Primrec.pred.comp <| Nat.Primrec.right.comp .right).comp <|
                Nat.Primrec.right.pair <| Nat.Primrec.right.comp Nat.Primrec.left).comp <|
          Nat.Primrec.id.pair <| (@Primcodable.prim α).comp Nat.Primrec.left).of_eq
      fun n => by
      simp only [Nat.unpaired, id_eq, Nat.unpair_pair, decode_prod_val, decode_nat,
        Option.some_bind, Option.map_map, Option.map_some']
      rcases @decode α _ n.unpair.1 with - | a; · rfl
      simp only [Nat.pred_eq_sub_one, encode_some, Nat.succ_eq_add_one, encodek, Option.map_some',
        Option.some_bind, Option.map_map]
      induction' n.unpair.2 with m <;> simp [encodek]
      simp [*, encodek]

Proof state:
case some
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
f : α → β
g : α → ℕ × β → β
hf : Primrec f
hg : Primrec₂ g
n : ℕ
a : α
⊢ Nat.rec (encode (f a) + 1)
      (fun y IH => encode (Option.map ((fun p => g p.1 p.2) ∘ Prod.mk a ∘ Prod.mk y) (decode (IH - 1))))
      (Nat.unpair n).2 =
    encode (Nat.rec (f a) (fun n IH => g a (n, IH)) (Nat.unpair n).2) + 1

Tactic:
induction' n.unpair.2 with m <;> simp [encodek]

Result:
case some.succ
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
f : α → β
g : α → ℕ × β → β
hf : Primrec f
hg : Primrec₂ g
n : ℕ
a : α
m : ℕ
a✝ :
  Nat.rec (encode (f a) + 1)
      (fun y IH => encode (Option.map ((fun p => g p.1 p.2) ∘ Prod.mk a ∘ Prod.mk y) (decode (IH - 1)))) m =
    encode (Nat.rec (f a) (fun n IH => g a (n, IH)) m) + 1
⊢ encode
      (Option.map ((fun p => g p.1 p.2) ∘ Prod.mk a ∘ Prod.mk m)
        (decode
          (Nat.rec (encode (f a) + 1)
              (fun y IH => encode (Option.map ((fun p => g p.1 p.2) ∘ Prod.mk a ∘ Prod.mk y) (decode (IH - 1)))) m -
            1))) =
    encode (g a (m, Nat.rec (f a) (fun n IH => g a (n, IH)) m)) + 1

Proof state:
case some
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
f : α → β
g : α → ℕ × β → β
hf : Primrec f
hg : Primrec₂ g
n : ℕ
a : α
⊢ Nat.rec 0
      (fun n_1 n_ih =>
        Nat.rec (encode (Option.map f (decode n_1)))
          (fun y IH =>
            encode
              (Option.map (fun p => g p.1 p.2)
                ((decode n_1).bind fun a => Option.map (Prod.mk a ∘ Prod.mk y) (decode IH.pred))))
          (Nat.unpair n).2)
      (encode (some a)) =
    encode ((some a).bind fun a => some (Nat.rec (f a) (fun n IH => g a (n, IH)) (Nat.unpair n).2))

Tactic:
simp only [Nat.pred_eq_sub_one, encode_some, Nat.succ_eq_add_one, encodek, Option.map_some',
  Option.some_bind, Option.map_map]

Result:
case some
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
f : α → β
g : α → ℕ × β → β
hf : Primrec f
hg : Primrec₂ g
n : ℕ
a : α
⊢ Nat.rec (encode (f a) + 1)
      (fun y IH => encode (Option.map ((fun p => g p.1 p.2) ∘ Prod.mk a ∘ Prod.mk y) (decode (IH - 1))))
      (Nat.unpair n).2 =
    encode (Nat.rec (f a) (fun n IH => g a (n, IH)) (Nat.unpair n).2) + 1

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
f : α → β
g : α → ℕ × β → β
hf : Primrec f
hg : Primrec₂ g
n : ℕ
⊢ Nat.rec 0
      (fun n_1 n_ih =>
        Nat.rec (encode (Option.map f (decode n_1)))
          (fun y IH =>
            encode
              (Option.map (fun p => g p.1 p.2)
                ((decode n_1).bind fun a => Option.map (Prod.mk a ∘ Prod.mk y) (decode IH.pred))))
          (Nat.unpair n).2)
      (encode (decode (Nat.unpair n).1)) =
    encode ((decode (Nat.unpair n).1).bind fun a => some (Nat.rec (f a) (fun n IH => g a (n, IH)) (Nat.unpair n).2))

Tactic:
rcases @decode α _ n.unpair.1 with - | a

Result:
case none
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
f : α → β
g : α → ℕ × β → β
hf : Primrec f
hg : Primrec₂ g
n : ℕ
⊢ Nat.rec 0
      (fun n_1 n_ih =>
        Nat.rec (encode (Option.map f (decode n_1)))
          (fun y IH =>
            encode
              (Option.map (fun p => g p.1 p.2)
                ((decode n_1).bind fun a => Option.map (Prod.mk a ∘ Prod.mk y) (decode IH.pred))))
          (Nat.unpair n).2)
      (encode none) =
    encode (none.bind fun a => some (Nat.rec (f a) (fun n IH => g a (n, IH)) (Nat.unpair n).2))

case some
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
f : α → β
g : α → ℕ × β → β
hf : Primrec f
hg : Primrec₂ g
n : ℕ
a : α
⊢ Nat.rec 0
      (fun n_1 n_ih =>
        Nat.rec (encode (Option.map f (decode n_1)))
          (fun y IH =>
            encode
              (Option.map (fun p => g p.1 p.2)
                ((decode n_1).bind fun a => Option.map (Prod.mk a ∘ Prod.mk y) (decode IH.pred))))
          (Nat.unpair n).2)
      (encode (some a)) =
    encode ((some a).bind fun a => some (Nat.rec (f a) (fun n IH => g a (n, IH)) (Nat.unpair n).2))

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
f : α → β
g : α → ℕ × β → β
hf : Primrec f
hg : Primrec₂ g
n : ℕ
⊢ Nat.unpaired
      (fun z n =>
        Nat.casesOn n 0 fun y =>
          Nat.unpaired
            (fun z n =>
              Nat.rec (encode (Option.map f (decode z)))
                (fun y IH =>
                  encode
                    (Option.map (fun p => g p.1 p.2)
                      (decode
                        (Nat.pair (Nat.unpair (Nat.pair z (Nat.pair y IH))).1
                          (Nat.pair (Nat.unpair (Nat.unpair (Nat.pair z (Nat.pair y IH))).2).1
                            (Nat.unpair (Nat.unpair (Nat.pair z (Nat.pair y IH))).2).2.pred)))))
                n)
            (Nat.pair (Nat.unpair (Nat.pair z y)).2 (Nat.unpair (Nat.unpair (Nat.pair z y)).1).2))
      (Nat.pair (id n) (encode (decode (Nat.unpair n).1))) =
    Nat.unpaired
      (fun m n =>
        encode ((decode m).bind fun a => Option.map (fun n => Nat.rec (f a) (fun n IH => g a (n, IH)) n) (decode n)))
      n

Tactic:
simp only [Nat.unpaired, id_eq, Nat.unpair_pair, decode_prod_val, decode_nat,
  Option.some_bind, Option.map_map, Option.map_some']

Result:
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
f : α → β
g : α → ℕ × β → β
hf : Primrec f
hg : Primrec₂ g
n : ℕ
⊢ Nat.rec 0
      (fun n_1 n_ih =>
        Nat.rec (encode (Option.map f (decode n_1)))
          (fun y IH =>
            encode
              (Option.map (fun p => g p.1 p.2)
                ((decode n_1).bind fun a => Option.map (Prod.mk a ∘ Prod.mk y) (decode IH.pred))))
          (Nat.unpair n).2)
      (encode (decode (Nat.unpair n).1)) =
    encode ((decode (Nat.unpair n).1).bind fun a => some (Nat.rec (f a) (fun n IH => g a (n, IH)) (Nat.unpair n).2))

Proof state:
case some.succ
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
f : α → β
g : α → ℕ × β → β
hf : Primrec f
hg : Primrec₂ g
n : ℕ
a : α
m : ℕ
a✝ :
  Nat.rec (encode (f a) + 1)
      (fun y IH => encode (Option.map ((fun p => g p.1 p.2) ∘ Prod.mk a ∘ Prod.mk y) (decode (IH - 1)))) m =
    encode (Nat.rec (f a) (fun n IH => g a (n, IH)) m) + 1
⊢ encode
      (Option.map ((fun p => g p.1 p.2) ∘ Prod.mk a ∘ Prod.mk m)
        (decode
          (Nat.rec (encode (f a) + 1)
              (fun y IH => encode (Option.map ((fun p => g p.1 p.2) ∘ Prod.mk a ∘ Prod.mk y) (decode (IH - 1)))) m -
            1))) =
    encode (g a (m, Nat.rec (f a) (fun n IH => g a (n, IH)) m)) + 1

Tactic:
simp [*, encodek]

Result:
no goals