-- Mathlib/Computability/Primrec.lean
theorem list_foldl' {f : α → List β} {g : α → σ} {h : α → σ × β → σ}
    (hf : haveI := prim H; Primrec f) (hg : Primrec g) (hh : haveI := prim H; Primrec₂ h) :
    Primrec fun a => (f a).foldl (fun s b => h a (s, b)) (g a)

Proof state:
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
H : Nat.Primrec fun n => encode (decode n)
f : α → List β
g : α → σ
h : α → σ × β → σ
hf : Primrec f
hg : Primrec g
hh : Primrec₂ h
this : Primcodable (List β) := prim H
G : α → σ × List β → σ × List β := fun a IH => List.casesOn IH.2 IH fun b l => (h a (IH.1, b), l)
hG : Primrec₂ G
F : α → ℕ → σ × List β := fun a n => (G a)^[n] (g a, f a)
hF : Primrec fun a => (F a (encode (f a))).1
⊢ Primrec fun a => List.foldl (fun s b => h a (s, b)) (g a) (f a)

Tactic:
suffices ∀ a n, F a n = (((f a).take n).foldl (fun s b => h a (s, b)) (g a), (f a).drop n) by
  refine hF.of_eq fun a => ?_
  rw [this, List.take_of_length_le (length_le_encode _)]

Result:
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
H : Nat.Primrec fun n => encode (decode n)
f : α → List β
g : α → σ
h : α → σ × β → σ
hf : Primrec f
hg : Primrec g
hh : Primrec₂ h
this : Primcodable (List β) := prim H
G : α → σ × List β → σ × List β := fun a IH => List.casesOn IH.2 IH fun b l => (h a (IH.1, b), l)
hG : Primrec₂ G
F : α → ℕ → σ × List β := fun a n => (G a)^[n] (g a, f a)
hF : Primrec fun a => (F a (encode (f a))).1
⊢ ∀ (a : α) (n : ℕ), F a n = (List.foldl (fun s b => h a (s, b)) (g a) (List.take n (f a)), List.drop n (f a))

Proof state:
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
H : Nat.Primrec fun n => encode (decode n)
f : α → List β
g : α → σ
h : α → σ × β → σ
hf : Primrec f
hg : Primrec g
hh : Primrec₂ h
this : Primcodable (List β) := prim H
G : α → σ × List β → σ × List β := fun a IH => List.casesOn IH.2 IH fun b l => (h a (IH.1, b), l)
hG : Primrec₂ G
F : α → ℕ → σ × List β := fun a n => (G a)^[n] (g a, f a)
hF : Primrec fun a => (F a (encode (f a))).1
⊢ ∀ (a : α) (n : ℕ), F a n = (List.foldl (fun s b => h a (s, b)) (g a) (List.take n (f a)), List.drop n (f a))

Tactic:
introv

Result:
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
H : Nat.Primrec fun n => encode (decode n)
f : α → List β
g : α → σ
h : α → σ × β → σ
hf : Primrec f
hg : Primrec g
hh : Primrec₂ h
this : Primcodable (List β) := prim H
G : α → σ × List β → σ × List β := fun a IH => List.casesOn IH.2 IH fun b l => (h a (IH.1, b), l)
hG : Primrec₂ G
F : α → ℕ → σ × List β := fun a n => (G a)^[n] (g a, f a)
hF : Primrec fun a => (F a (encode (f a))).1
a : α
n : ℕ
⊢ F a n = (List.foldl (fun s b => h a (s, b)) (g a) (List.take n (f a)), List.drop n (f a))

Proof state:
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
H : Nat.Primrec fun n => encode (decode n)
f : α → List β
g : α → σ
h : α → σ × β → σ
hf : Primrec f
hg : Primrec g
hh : Primrec₂ h
this : Primcodable (List β) := prim H
G : α → σ × List β → σ × List β := fun a IH => List.casesOn IH.2 IH fun b l => (h a (IH.1, b), l)
hG : Primrec₂ G
F : α → ℕ → σ × List β := fun a n => (G a)^[n] (g a, f a)
hF : Primrec fun a => (F a (encode (f a))).1
a : α
n : ℕ
⊢ (G a)^[n] (g a, f a) = (List.foldl (fun s b => h a (s, b)) (g a) (List.take n (f a)), List.drop n (f a))

Tactic:
generalize f a = l

Result:
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
H : Nat.Primrec fun n => encode (decode n)
f : α → List β
g : α → σ
h : α → σ × β → σ
hf : Primrec f
hg : Primrec g
hh : Primrec₂ h
this : Primcodable (List β) := prim H
G : α → σ × List β → σ × List β := fun a IH => List.casesOn IH.2 IH fun b l => (h a (IH.1, b), l)
hG : Primrec₂ G
F : α → ℕ → σ × List β := fun a n => (G a)^[n] (g a, f a)
hF : Primrec fun a => (F a (encode (f a))).1
a : α
n : ℕ
l : List β
⊢ (G a)^[n] (g a, l) = (List.foldl (fun s b => h a (s, b)) (g a) (List.take n l), List.drop n l)