-- Mathlib/Computability/Primrec.lean
theorem list_rec {f : α → List β} {g : α → σ} {h : α → β × List β × σ → σ} (hf : Primrec f)
    (hg : Primrec g) (hh : Primrec₂ h) :
    @Primrec _ σ _ _ fun a => List.recOn (f a) (g a) fun b l IH => h a (b, l, IH) :=
  let F (a : α) := (f a).foldr (fun (b : β) (s : List β × σ) => (b :: s.1, h a (b, s))) ([], g a)
  have : Primrec F :=
    list_foldr hf (pair (const []) hg) <|
      to₂ <| pair ((list_cons.comp fst (fst.comp snd)).comp snd) hh
  (snd.comp this).of_eq fun a => by
    suffices F a = (f a, List.recOn (f a) (g a) fun b l IH => h a (b, l, IH)) by rw [this]
    dsimp [F]
    induction' f a with b l IH <;> simp [*]

Proof state:
α : Type u_1
β : Type u_2
σ : Type u_4
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α → List β
g : α → σ
h : α → β × List β × σ → σ
hf : Primrec f
hg : Primrec g
hh : Primrec₂ h
F : α → List β × σ := fun a => List.foldr (fun b s => (b :: s.1, h a (b, s))) ([], g a) (f a)
this : Primrec F
a : α
⊢ F a = (f a, List.recOn (f a) (g a) fun b l IH => h a (b, l, IH))

Tactic:
dsimp [F]

Result:
α : Type u_1
β : Type u_2
σ : Type u_4
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α → List β
g : α → σ
h : α → β × List β × σ → σ
hf : Primrec f
hg : Primrec g
hh : Primrec₂ h
F : α → List β × σ := fun a => List.foldr (fun b s => (b :: s.1, h a (b, s))) ([], g a) (f a)
this : Primrec F
a : α
⊢ List.foldr (fun b s => (b :: s.1, h a (b, s))) ([], g a) (f a) =
    (f a, List.rec (g a) (fun b l IH => h a (b, l, IH)) (f a))

Proof state:
α : Type u_1
β : Type u_2
σ : Type u_4
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α → List β
g : α → σ
h : α → β × List β × σ → σ
hf : Primrec f
hg : Primrec g
hh : Primrec₂ h
F : α → List β × σ := fun a => List.foldr (fun b s => (b :: s.1, h a (b, s))) ([], g a) (f a)
this : Primrec F
a : α
⊢ List.foldr (fun b s => (b :: s.1, h a (b, s))) ([], g a) (f a) =
    (f a, List.rec (g a) (fun b l IH => h a (b, l, IH)) (f a))

Tactic:
induction' f a with b l IH <;> simp [*]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
σ : Type u_4
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α → List β
g : α → σ
h : α → β × List β × σ → σ
hf : Primrec f
hg : Primrec g
hh : Primrec₂ h
F : α → List β × σ := fun a => List.foldr (fun b s => (b :: s.1, h a (b, s))) ([], g a) (f a)
this✝ : Primrec F
a : α
this : F a = (f a, List.recOn (f a) (g a) fun b l IH => h a (b, l, IH))
⊢ (F a).2 = List.recOn (f a) (g a) fun b l IH => h a (b, l, IH)

Tactic:
rw [this]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
σ : Type u_4
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α → List β
g : α → σ
h : α → β × List β × σ → σ
hf : Primrec f
hg : Primrec g
hh : Primrec₂ h
F : α → List β × σ := fun a => List.foldr (fun b s => (b :: s.1, h a (b, s))) ([], g a) (f a)
this : Primrec F
a : α
⊢ (F a).2 = List.recOn (f a) (g a) fun b l IH => h a (b, l, IH)

Tactic:
suffices F a = (f a, List.recOn (f a) (g a) fun b l IH => h a (b, l, IH)) by rw [this]

Result:
α : Type u_1
β : Type u_2
σ : Type u_4
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α → List β
g : α → σ
h : α → β × List β × σ → σ
hf : Primrec f
hg : Primrec g
hh : Primrec₂ h
F : α → List β × σ := fun a => List.foldr (fun b s => (b :: s.1, h a (b, s))) ([], g a) (f a)
this : Primrec F
a : α
⊢ F a = (f a, List.recOn (f a) (g a) fun b l IH => h a (b, l, IH))