-- Mathlib/Computability/Partrec.lean
theorem nat_strong_rec (f : α → ℕ → σ) {g : α → List σ → Option σ} (hg : Computable₂ g)
    (H : ∀ a n, g a ((List.range n).map (f a)) = Option.some (f a n)) : Computable₂ f :=
  suffices Computable₂ fun a n => (List.range n).map (f a) from
    option_some_iff.1 <|
      (list_get?.comp (this.comp fst (succ.comp snd)) snd).to₂.of_eq fun a => by
        simp [List.getElem?_range (Nat.lt_succ_self a.2)]
  option_some_iff.1 <|
    (nat_rec snd (const (Option.some []))
          (to₂ <|
            option_bind (snd.comp snd) <|
              to₂ <|
                option_map (hg.comp (fst.comp <| fst.comp fst) snd)
                  (to₂ <| list_concat.comp (snd.comp fst) snd))).of_eq
      fun a => by
      induction' a.2 with n IH; · rfl
      simp [IH, H, List.range_succ]

Proof state:
case zero
α : Type u_1
σ : Type u_4
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f : α → ℕ → σ
g : α → List σ → Option σ
hg : Computable₂ g
H : ∀ (a : α) (n : ℕ), g a (List.map (f a) (List.range n)) = Option.some (f a n)
a : α × ℕ
⊢ Nat.rec (Option.some [])
      (fun y IH =>
        (a, y, IH).2.2.bind fun b =>
          Option.map (fun b_1 => (((a, y, IH), b), b_1).1.2 ++ [(((a, y, IH), b), b_1).2])
            (g ((a, y, IH), b).1.1.1 ((a, y, IH), b).2))
      0 =
    Option.some ((fun a n => List.map (f a) (List.range n)) a.1 0)

Tactic:
rfl

Result:
no goals

Proof state:
case succ
α : Type u_1
σ : Type u_4
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f : α → ℕ → σ
g : α → List σ → Option σ
hg : Computable₂ g
H : ∀ (a : α) (n : ℕ), g a (List.map (f a) (List.range n)) = Option.some (f a n)
a : α × ℕ
n : ℕ
IH :
  Nat.rec (Option.some [])
      (fun y IH =>
        (a, y, IH).2.2.bind fun b =>
          Option.map (fun b_1 => (((a, y, IH), b), b_1).1.2 ++ [(((a, y, IH), b), b_1).2])
            (g ((a, y, IH), b).1.1.1 ((a, y, IH), b).2))
      n =
    Option.some ((fun a n => List.map (f a) (List.range n)) a.1 n)
⊢ Nat.rec (Option.some [])
      (fun y IH =>
        (a, y, IH).2.2.bind fun b =>
          Option.map (fun b_1 => (((a, y, IH), b), b_1).1.2 ++ [(((a, y, IH), b), b_1).2])
            (g ((a, y, IH), b).1.1.1 ((a, y, IH), b).2))
      (n + 1) =
    Option.some ((fun a n => List.map (f a) (List.range n)) a.1 (n + 1))

Tactic:
simp [IH, H, List.range_succ]

Result:
no goals

Proof state:
α : Type u_1
σ : Type u_4
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f : α → ℕ → σ
g : α → List σ → Option σ
hg : Computable₂ g
H : ∀ (a : α) (n : ℕ), g a (List.map (f a) (List.range n)) = Option.some (f a n)
this : Computable₂ fun a n => List.map (f a) (List.range n)
a : α × ℕ
⊢ (fun a b => (List.map (f (a, b).1) (List.range (a, b).2.succ)).get? (a, b).2) a.1 a.2 = Option.some (f a.1 a.2)

Tactic:
simp [List.getElem?_range (Nat.lt_succ_self a.2)]

Result:
no goals

Proof state:
α : Type u_1
σ : Type u_4
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f : α → ℕ → σ
g : α → List σ → Option σ
hg : Computable₂ g
H : ∀ (a : α) (n : ℕ), g a (List.map (f a) (List.range n)) = Option.some (f a n)
a : α × ℕ
⊢ Nat.rec (Option.some [])
      (fun y IH =>
        (a, y, IH).2.2.bind fun b =>
          Option.map (fun b_1 => (((a, y, IH), b), b_1).1.2 ++ [(((a, y, IH), b), b_1).2])
            (g ((a, y, IH), b).1.1.1 ((a, y, IH), b).2))
      a.2 =
    Option.some ((fun a n => List.map (f a) (List.range n)) a.1 a.2)

Tactic:
induction' a.2 with n IH

Result:
case zero
α : Type u_1
σ : Type u_4
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f : α → ℕ → σ
g : α → List σ → Option σ
hg : Computable₂ g
H : ∀ (a : α) (n : ℕ), g a (List.map (f a) (List.range n)) = Option.some (f a n)
a : α × ℕ
⊢ Nat.rec (Option.some [])
      (fun y IH =>
        (a, y, IH).2.2.bind fun b =>
          Option.map (fun b_1 => (((a, y, IH), b), b_1).1.2 ++ [(((a, y, IH), b), b_1).2])
            (g ((a, y, IH), b).1.1.1 ((a, y, IH), b).2))
      0 =
    Option.some ((fun a n => List.map (f a) (List.range n)) a.1 0)

case succ
α : Type u_1
σ : Type u_4
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f : α → ℕ → σ
g : α → List σ → Option σ
hg : Computable₂ g
H : ∀ (a : α) (n : ℕ), g a (List.map (f a) (List.range n)) = Option.some (f a n)
a : α × ℕ
n : ℕ
IH :
  Nat.rec (Option.some [])
      (fun y IH =>
        (a, y, IH).2.2.bind fun b =>
          Option.map (fun b_1 => (((a, y, IH), b), b_1).1.2 ++ [(((a, y, IH), b), b_1).2])
            (g ((a, y, IH), b).1.1.1 ((a, y, IH), b).2))
      n =
    Option.some ((fun a n => List.map (f a) (List.range n)) a.1 n)
⊢ Nat.rec (Option.some [])
      (fun y IH =>
        (a, y, IH).2.2.bind fun b =>
          Option.map (fun b_1 => (((a, y, IH), b), b_1).1.2 ++ [(((a, y, IH), b), b_1).2])
            (g ((a, y, IH), b).1.1.1 ((a, y, IH), b).2))
      (n + 1) =
    Option.some ((fun a n => List.map (f a) (List.range n)) a.1 (n + 1))