-- 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
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)

Tactic:
generalize g a = x

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 β
x : σ
⊢ (G a)^[n] (x, l) = (List.foldl (fun s b => h a (s, b)) x (List.take n l), List.drop n l)

Proof state:
case zero
α : 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 : α
l : List β
x : σ
⊢ (G a)^[0] (x, l) = (List.foldl (fun s b => h a (s, b)) x (List.take 0 l), List.drop 0 l)

Tactic:
rfl

Result:
no goals

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
⊢ Primrec fun a => List.foldl (fun s b => h a (s, b)) (g a) (f a)

Tactic:
let F := fun (a : α) (n : ℕ) => (G a)^[n] (g a, f a)

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)
⊢ Primrec fun a => List.foldl (fun s b => h a (s, b)) (g a) (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:
dsimp only [F]

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 : ℕ
⊢ (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))

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
this : ∀ (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))
⊢ Primrec fun a => List.foldl (fun s b => h a (s, b)) (g a) (f a)

Tactic:
refine hF.of_eq fun a => ?_

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
this : ∀ (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))
a : α
⊢ (F a (encode (f a))).1 = List.foldl (fun s b => h a (s, b)) (g a) (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)
⊢ Primrec fun a => List.foldl (fun s b => h a (s, b)) (g a) (f a)

Tactic:
have hF : Primrec fun a => (F a (encode (f a))).1 :=
  (fst.comp <|
    nat_iterate (encode_iff.2 hf) (pair hg hf) <|
    hG)

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
⊢ Primrec fun a => List.foldl (fun s b => h a (s, b)) (g a) (f a)