awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Computability.Primrec.List
Goal:
α : Type u_1
β : Type u_2
σ : Type u_3
inst : Primcodable α
inst_1 : Primcodable β
inst_2 : Primcodable σ
H : Nat.Primrec fun (n : ℕ) ↦ encode.{u_2} (α := Option (List β)) (decode n)
f : α → List β
g : α → σ
h : α → σ × β → σ
hf : Primrec f
hg : Primrec g
hh : Primrec₂ h
this : Primcodable (List β) := prim H
G : (a : α) → (IH : Prod.{u_3, u_2} σ (List β)) → Prod.{u_3, u_2} σ (List β) :=
  fun (a : α) (IH : Prod.{u_3, u_2} σ (List β)) ↦
    List.casesOn (motive := fun (x : List β) ↦ Prod.{u_3, u_2} σ (List β)) IH.2 IH fun (b : β) (l : List β) ↦
      (h a (IH.1, b), l)
hG : Primrec₂ G
F : (a : α) → (n : ℕ) → Prod.{u_3, u_2} σ (List β) := fun (a : α) (n : ℕ) ↦ (G a)^[n] (g a, f a)
hF : Primrec.{u_1, u_3} (β := σ) fun (a : α) ↦ (F a (encode (f a))).1
a : α
n : ℕ
dsimp :
  (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))
⊢ 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]
-- Module: Mathlib.Computability.Primrec.List
Goal:
α : Type u_1
β : Type u_2
σ : Type u_3
inst : Primcodable α
inst_1 : Primcodable β
inst_2 : Primcodable σ
H : Nat.Primrec fun (n : ℕ) ↦ encode.{u_2} (α := Option (List β)) (decode n)
f : α → List β
g : α → σ
h : α → σ × β → σ
hf : Primrec f
hg : Primrec g
hh : Primrec₂ h
this : Primcodable (List β) := prim H
G : (a : α) → (IH : Prod.{u_3, u_2} σ (List β)) → Prod.{u_3, u_2} σ (List β) :=
  fun (a : α) (IH : Prod.{u_3, u_2} σ (List β)) ↦
    List.casesOn (motive := fun (x : List β) ↦ Prod.{u_3, u_2} σ (List β)) IH.2 IH fun (b : β) (l : List β) ↦
      (h a (IH.1, b), l)
hG : Primrec₂ G
F : (a : α) → (n : ℕ) → Prod.{u_3, u_2} σ (List β) := fun (a : α) (n : ℕ) ↦ (G a)^[n] (g a, f a)
hF : Primrec.{u_1, u_3} (β := σ) fun (a : α) ↦ (F a (encode (f a))).1
a : α
n : ℕ
generalize :
  ∀ (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)
⊢ (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
-- Module: Mathlib.Computability.Primrec.List
Goal:
α : Type u_1
β : Type u_2
σ : Type u_3
inst : Primcodable α
inst_1 : Primcodable β
inst_2 : Primcodable σ
H : Nat.Primrec fun (n : ℕ) ↦ encode.{u_2} (α := Option (List β)) (decode n)
f : α → List β
g : α → σ
h : α → σ × β → σ
hf : Primrec f
hg : Primrec g
hh : Primrec₂ h
this : Primcodable (List β) := prim H
G : (a : α) → (IH : Prod.{u_3, u_2} σ (List β)) → Prod.{u_3, u_2} σ (List β) :=
  fun (a : α) (IH : Prod.{u_3, u_2} σ (List β)) ↦
    List.casesOn (motive := fun (x : List β) ↦ Prod.{u_3, u_2} σ (List β)) IH.2 IH fun (b : β) (l : List β) ↦
      (h a (IH.1, b), l)
hG : Primrec₂ G
F : (a : α) → (n : ℕ) → Prod.{u_3, u_2} σ (List β) := fun (a : α) (n : ℕ) ↦ (G a)^[n] (g a, f a)
hF : Primrec.{u_1, u_3} (β := σ) fun (a : α) ↦ (F a (encode (f a))).1
a : α
n : ℕ
l : List β
generalize :
  ∀ (x : σ), (G a)^[n] (x, l) = (List.foldl (fun (s : σ) (b : β) ↦ h a (s, b)) x (List.take n l), List.drop n l)
⊢ (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
-- Module: Mathlib.Computability.Primrec.List
Goal:
α : Type u_1
β : Type u_2
σ : Type u_3
inst : Primcodable α
inst_1 : Primcodable β
inst_2 : Primcodable σ
H : Nat.Primrec fun (n : ℕ) ↦ encode.{u_2} (α := Option (List β)) (decode n)
f : α → List β
g : α → σ
h : α → σ × β → σ
hf : Primrec f
hg : Primrec g
hh : Primrec₂ h
this : Primcodable (List β) := prim H
G : (a : α) → (IH : Prod.{u_3, u_2} σ (List β)) → Prod.{u_3, u_2} σ (List β) :=
  fun (a : α) (IH : Prod.{u_3, u_2} σ (List β)) ↦
    List.casesOn (motive := fun (x : List β) ↦ Prod.{u_3, u_2} σ (List β)) IH.2 IH fun (b : β) (l : List β) ↦
      (h a (IH.1, b), l)
hG : Primrec₂ G
F : (a : α) → (n : ℕ) → Prod.{u_3, u_2} σ (List β) := fun (a : α) (n : ℕ) ↦ (G a)^[n] (g a, f a)
hF : Primrec.{u_1, u_3} (β := σ) 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
-- Module: Mathlib.Computability.Primrec.List
Goal:
α : Type u_1
β : Type u_2
σ : Type u_3
inst : Primcodable α
inst_1 : Primcodable β
inst_2 : Primcodable σ
H : Nat.Primrec fun (n : ℕ) ↦ encode.{u_2} (α := Option (List β)) (decode n)
f : α → List β
g : α → σ
h : α → σ × β → σ
hf : Primrec f
hg : Primrec g
hh : Primrec₂ h
this : Primcodable (List β) := prim H
G : (a : α) → (IH : Prod.{u_3, u_2} σ (List β)) → Prod.{u_3, u_2} σ (List β) :=
  fun (a : α) (IH : Prod.{u_3, u_2} σ (List β)) ↦
    List.casesOn (motive := fun (x : List β) ↦ Prod.{u_3, u_2} σ (List β)) IH.2 IH fun (b : β) (l : List β) ↦
      (h a (IH.1, b), l)
hG : Primrec₂ G
F : (a : α) → (n : ℕ) → Prod.{u_3, u_2} σ (List β) := fun (a : α) (n : ℕ) ↦ (G a)^[n] (g a, f a)
hF : Primrec.{u_1, u_3} (β := σ) fun (a : α) ↦ (F a (encode (f a))).1
a : α
n : ℕ
IH :
  ∀ (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)
l : List β
x : σ
succ :
  (G a)^[n] (G a (x, l)) = (List.foldl (fun (s : σ) (b : β) ↦ h a (s, b)) x (List.take (n + 1) l), List.drop (n + 1) l)
⊢ (G a)^[n + 1] (x, l) = (List.foldl (fun (s : σ) (b : β) ↦ h a (s, b)) x (List.take (n + 1) l), List.drop (n + 1) l)

Tactic:
simp only [iterate_succ, comp_apply]

Premises used: Function.iterate_succ, Function.comp_apply
-- Module: Mathlib.Computability.Primrec.List
Goal:
α : Type u_1
β : Type u_2
σ : Type u_3
inst : Primcodable α
inst_1 : Primcodable β
inst_2 : Primcodable σ
H : Nat.Primrec fun (n : ℕ) ↦ encode.{u_2} (α := Option (List β)) (decode n)
f : α → List β
g : α → σ
h : α → σ × β → σ
hf : Primrec f
hg : Primrec g
hh : Primrec₂ h
this : Primcodable (List β) := prim H
G : (a : α) → (IH : Prod.{u_3, u_2} σ (List β)) → Prod.{u_3, u_2} σ (List β) :=
  fun (a : α) (IH : Prod.{u_3, u_2} σ (List β)) ↦
    List.casesOn (motive := fun (x : List β) ↦ Prod.{u_3, u_2} σ (List β)) IH.2 IH fun (b : β) (l : List β) ↦
      (h a (IH.1, b), l)
hG : Primrec₂ G
F : (a : α) → (n : ℕ) → Prod.{u_3, u_2} σ (List β) := fun (a : α) (n : ℕ) ↦ (G a)^[n] (g a, f a)
hF : Primrec.{u_1, u_3} (β := σ) fun (a : α) ↦ (F a (encode (f a))).1
a : α
n : ℕ
IH :
  ∀ (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)
l : List β
x : σ
succ :
  (G a)^[n] (G a (x, [])) =
    (List.foldl (fun (s : σ) (b : β) ↦ h a (s, b)) x (List.take (n + 1) []), List.drop (n + 1) [])
succ₁ :
  ∀ (b : β) (l : List β),
    (G a)^[n] (G a (x, b :: l)) =
      (List.foldl (fun (s : σ) (b : β) ↦ h a (s, b)) x (List.take (n + 1) (b :: l)), List.drop (n + 1) (b :: l))
⊢ (G a)^[n] (G a (x, l)) = (List.foldl (fun (s : σ) (b : β) ↦ h a (s, b)) x (List.take (n + 1) l), List.drop (n + 1) l)

Tactic:
rcases l with - | ⟨b, l⟩
-- Module: Mathlib.Computability.Primrec.List
Goal:
α : Type u_1
β : Type u_2
σ : Type u_3
inst : Primcodable α
inst_1 : Primcodable β
inst_2 : Primcodable σ
H : Nat.Primrec fun (n : ℕ) ↦ encode.{u_2} (α := Option (List β)) (decode n)
f : α → List β
g : α → σ
h : α → σ × β → σ
hf : Primrec f
hg : Primrec g
hh : Primrec₂ h
this : Primcodable (List β) := prim H
G : (a : α) → (IH : Prod.{u_3, u_2} σ (List β)) → Prod.{u_3, u_2} σ (List β) :=
  fun (a : α) (IH : Prod.{u_3, u_2} σ (List β)) ↦
    List.casesOn (motive := fun (x : List β) ↦ Prod.{u_3, u_2} σ (List β)) IH.2 IH fun (b : β) (l : List β) ↦
      (h a (IH.1, b), l)
hG : Primrec₂ G
F : (a : α) → (n : ℕ) → Prod.{u_3, u_2} σ (List β) := fun (a : α) (n : ℕ) ↦ (G a)^[n] (g a, f a)
hF : Primrec.{u_1, u_3} (β := σ) fun (a : α) ↦ (F a (encode (f a))).1
a : α
n : ℕ
IH :
  ∀ (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)
x : σ
⊢ (G a)^[n] (G a (x, [])) =
    (List.foldl (fun (s : σ) (b : β) ↦ h a (s, b)) x (List.take (n + 1) []), List.drop (n + 1) [])

Tactic:
simp [G, IH]
-- Module: Mathlib.Computability.Primrec.List
Goal:
α : Type u_1
β : Type u_2
σ : Type u_3
inst : Primcodable α
inst_1 : Primcodable β
inst_2 : Primcodable σ
H : Nat.Primrec fun (n : ℕ) ↦ encode.{u_2} (α := Option (List β)) (decode n)
f : α → List β
g : α → σ
h : α → σ × β → σ
hf : Primrec f
hg : Primrec g
hh : Primrec₂ h
this : Primcodable (List β) := prim H
G : (a : α) → (IH : Prod.{u_3, u_2} σ (List β)) → Prod.{u_3, u_2} σ (List β) :=
  fun (a : α) (IH : Prod.{u_3, u_2} σ (List β)) ↦
    List.casesOn (motive := fun (x : List β) ↦ Prod.{u_3, u_2} σ (List β)) IH.2 IH fun (b : β) (l : List β) ↦
      (h a (IH.1, b), l)
hG : Primrec₂ G
F : (a : α) → (n : ℕ) → Prod.{u_3, u_2} σ (List β) := fun (a : α) (n : ℕ) ↦ (G a)^[n] (g a, f a)
hF : Primrec.{u_1, u_3} (β := σ) fun (a : α) ↦ (F a (encode (f a))).1
a : α
n : ℕ
IH :
  ∀ (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)
x : σ
b : β
l : List β
⊢ (G a)^[n] (G a (x, b :: l)) =
    (List.foldl (fun (s : σ) (b : β) ↦ h a (s, b)) x (List.take (n + 1) (b :: l)), List.drop (n + 1) (b :: l))

Tactic:
simp [G, IH]
-- Module: Mathlib.Computability.Primrec.List
Goal:
α : Type u_1
β : Type u_2
σ : Type u_3
inst : Primcodable α
inst_1 : Primcodable β
inst_2 : Primcodable σ
H : Nat.Primrec fun (n : ℕ) ↦ encode.{u_2} (α := Option (List β)) (decode n)
f : α → List β
g : α → σ
h : α → σ × β → σ
hf : Primrec f
hg : Primrec g
hh : Primrec₂ h
this : Primcodable (List β) := prim H
G : (a : α) → (IH : Prod.{u_3, u_2} σ (List β)) → Prod.{u_3, u_2} σ (List β) :=
  fun (a : α) (IH : Prod.{u_3, u_2} σ (List β)) ↦
    List.casesOn (motive := fun (x : List β) ↦ Prod.{u_3, u_2} σ (List β)) IH.2 IH fun (b : β) (l : List β) ↦
      (h a (IH.1, b), l)
hG : Primrec₂ G
F : (a : α) → (n : ℕ) → Prod.{u_3, u_2} σ (List β) := fun (a : α) (n : ℕ) ↦ (G a)^[n] (g a, f a)
hF : Primrec.{u_1, u_3} (β := σ) fun (a : α) ↦ (F a (encode (f a))).1
a : α
n : ℕ
l : List β
x : σ
zero :
  ∀ (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)
succ :
  ∀ (n : ℕ)
    (IH :
      ∀ (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))
    (l : List β) (x : σ),
    (G a)^[n + 1] (x, l) = (List.foldl (fun (s : σ) (b : β) ↦ h a (s, b)) x (List.take (n + 1) l), List.drop (n + 1) l)
⊢ (G a)^[n] (x, l) = (List.foldl (fun (s : σ) (b : β) ↦ h a (s, b)) x (List.take n l), List.drop n l)

Tactic:
induction n generalizing l x with
  | zero => rfl
  | succ n IH =>
    simp only [iterate_succ, comp_apply]
    rcases l with - | ⟨b, l⟩ <;> simp [G, IH]

Premises used: Function.iterate_succ, Primrec.succ, Function.comp_apply
-- Module: Mathlib.Computability.Primrec.List
Goal:
β : Type u_2
inst : Primcodable β
H : Nat.Primrec fun (n : ℕ) ↦ encode.{u_2} (α := Option (List β)) (decode n)
⊢ Primrec₂.{u_2, u_2, u_2} (α := β) List.cons

Tactic:
letI := prim H
  encode_iff.1 (succ.comp <| Primrec₂.natPair.comp (encode_iff.2 fst) (encode_iff.2 snd))

Premises used: Iff.mpr, Primrec.snd, Primrec.fst, Primrec.encode_iff, Primrec.succ, Primrec.comp, Primrec₂.natPair, Iff.mp, Primrec₂.comp, Primrec₂
-- Module: Mathlib.Computability.Primrec.List
Goal:
β : Type u_2
inst : Primcodable β
H : Nat.Primrec fun (n : ℕ) ↦ encode.{u_2} (α := Option (List β)) (decode n)
this : Primcodable (List β) := prim H
l : List β
nil : ∀ (r : List β), List.foldl (fun (s : List β) (b : β) ↦ b :: s) r [] = List.reverseAux [] r
cons :
  ∀ (head : β) (tail : List β),
    (∀ (r : List β), List.foldl (fun (s : List β) (b : β) ↦ b :: s) r tail = tail.reverseAux r) →
      ∀ (r : List β), List.foldl (fun (s : List β) (b : β) ↦ b :: s) r (head :: tail) = (head :: tail).reverseAux r
⊢ ∀ (r : List β), List.foldl (fun (s : List β) (b : β) ↦ b :: s) r l = l.reverseAux r

Tactic:
induction l
-- Module: Mathlib.Computability.Primrec.List
Goal:
β : Type u_2
inst : Primcodable β
H : Nat.Primrec fun (n : ℕ) ↦ encode.{u_2} (α := Option (List β)) (decode n)
this : Primcodable (List β) := prim H
⊢ ∀ (r : List β), List.foldl (fun (s : List β) (b : β) ↦ b :: s) r [] = List.reverseAux [] r

Tactic:
simp [*, List.reverseAux]

Premises used: List.reverseAux
-- Module: Mathlib.Computability.Primrec.List
Goal:
β : Type u_2
inst : Primcodable β
H : Nat.Primrec fun (n : ℕ) ↦ encode.{u_2} (α := Option (List β)) (decode n)
this : Primcodable (List β) := prim H
head : β
tail : List β
tail_ih : ∀ (r : List β), List.foldl (fun (s : List β) (b : β) ↦ b :: s) r tail = tail.reverseAux r
⊢ ∀ (r : List β), List.foldl (fun (s : List β) (b : β) ↦ b :: s) r (head :: tail) = (head :: tail).reverseAux r

Tactic:
simp [*, List.reverseAux]

Premises used: List.reverseAux
-- Module: Mathlib.Computability.Primrec.List
Goal:
α : Type u_1
β : Type u_2
inst : Primcodable α
inst_1 : Primcodable β
H : Nat.Primrec fun (n : ℕ) ↦ encode (α := Option (List ℕ)) (decode n) := ⋯
this_1 : Primrec₂ (σ := Option (List ℕ)) fun (a : α) (o : Option (List ℕ)) ↦ Option.map (List.cons (encode a)) o
this :
  Primrec (β := Option (List ℕ)) fun (n : ℕ) ↦
    List.foldl
      (fun (o : Option (List ℕ)) (m : ℕ) ↦ Option.bind (decode m) fun (a : α) ↦ Option.map (List.cons (encode a)) o)
      (some []) (List.reverse (ofNat (List ℕ) n))
n : ℕ
rw :
  encode (α := Option (List ℕ))
      (List.foldr
        (fun (x : ℕ) (y : Option (List ℕ)) ↦ Option.bind (decode x) fun (a : α) ↦ Option.map (List.cons (encode a)) y)
        (some []) (ofNat (List ℕ) n)) =
    encode.{u_1} (α := Option (List α)) (decode n)
⊢ encode (α := Option (List ℕ))
      (List.foldl
        (fun (o : Option (List ℕ)) (m : ℕ) ↦ Option.bind (decode m) fun (a : α) ↦ Option.map (List.cons (encode a)) o)
        (some []) (List.reverse (ofNat (List ℕ) n))) =
    encode.{u_1} (α := Option (List α)) (decode n)

Tactic:
rw [List.foldl_reverse]

Premises used: List.foldl_reverse
-- Module: Mathlib.Computability.Primrec.List
Goal:
α : Type u_1
β : Type u_2
inst : Primcodable α
inst_1 : Primcodable β
H : Nat.Primrec fun (n : ℕ) ↦ encode (α := Option (List ℕ)) (decode n) := ⋯
this_1 : Primrec₂ (σ := Option (List ℕ)) fun (a : α) (o : Option (List ℕ)) ↦ Option.map (List.cons (encode a)) o
this :
  Primrec (β := Option (List ℕ)) fun (n : ℕ) ↦
    List.foldl
      (fun (o : Option (List ℕ)) (m : ℕ) ↦ Option.bind (decode m) fun (a : α) ↦ Option.map (List.cons (encode a)) o)
      (some []) (List.reverse (ofNat (List ℕ) n))
n : ℕ
hz :
  encode (α := Option (List ℕ))
      (List.foldr
        (fun (x : ℕ) (y : Option (List ℕ)) ↦ Option.bind (decode x) fun (a : α) ↦ Option.map (List.cons (encode a)) y)
        (some []) (ofNat (List ℕ) 0)) =
    encode.{u_1} (α := Option (List α)) (decode 0)
hi :
  ∀ (n : ℕ),
    (∀ m ≤ n,
        encode (α := Option (List ℕ))
            (List.foldr
              (fun (x : ℕ) (y : Option (List ℕ)) ↦
                Option.bind (decode x) fun (a : α) ↦ Option.map (List.cons (encode a)) y)
              (some []) (ofNat (List ℕ) m)) =
          encode.{u_1} (α := Option (List α)) (decode m)) →
      encode (α := Option (List ℕ))
          (List.foldr
            (fun (x : ℕ) (y : Option (List ℕ)) ↦
              Option.bind (decode x) fun (a : α) ↦ Option.map (List.cons (encode a)) y)
            (some []) (ofNat (List ℕ) (n + 1))) =
        encode.{u_1} (α := Option (List α)) (decode (n + 1))
⊢ encode (α := Option (List ℕ))
      (List.foldr
        (fun (x : ℕ) (y : Option (List ℕ)) ↦ Option.bind (decode x) fun (a : α) ↦ Option.map (List.cons (encode a)) y)
        (some []) (ofNat (List ℕ) n)) =
    encode.{u_1} (α := Option (List α)) (decode n)

Tactic:
apply Nat.case_strong_induction_on n

Premises used: Nat.case_strong_induction_on
-- Module: Mathlib.Computability.Primrec.List
Goal:
α : Type u_1
β : Type u_2
inst : Primcodable α
inst_1 : Primcodable β
H : Nat.Primrec fun (n : ℕ) ↦ encode (α := Option (List ℕ)) (decode n) := ⋯
this_1 : Primrec₂ (σ := Option (List ℕ)) fun (a : α) (o : Option (List ℕ)) ↦ Option.map (List.cons (encode a)) o
this :
  Primrec (β := Option (List ℕ)) fun (n : ℕ) ↦
    List.foldl
      (fun (o : Option (List ℕ)) (m : ℕ) ↦ Option.bind (decode m) fun (a : α) ↦ Option.map (List.cons (encode a)) o)
      (some []) (List.reverse (ofNat (List ℕ) n))
n : ℕ
⊢ encode (α := Option (List ℕ))
      (List.foldr
        (fun (x : ℕ) (y : Option (List ℕ)) ↦ Option.bind (decode x) fun (a : α) ↦ Option.map (List.cons (encode a)) y)
        (some []) (ofNat (List ℕ) 0)) =
    encode.{u_1} (α := Option (List α)) (decode 0)

Tactic:
simp
-- Module: Mathlib.Computability.Primrec.List
Goal:
α : Type u_1
β : Type u_2
inst : Primcodable α
inst_1 : Primcodable β
H : Nat.Primrec fun (n : ℕ) ↦ encode (α := Option (List ℕ)) (decode n) := ⋯
this_1 : Primrec₂ (σ := Option (List ℕ)) fun (a : α) (o : Option (List ℕ)) ↦ Option.map (List.cons (encode a)) o
this :
  Primrec (β := Option (List ℕ)) fun (n : ℕ) ↦
    List.foldl
      (fun (o : Option (List ℕ)) (m : ℕ) ↦ Option.bind (decode m) fun (a : α) ↦ Option.map (List.cons (encode a)) o)
      (some []) (List.reverse (ofNat (List ℕ) n))
n_1 n : ℕ
IH :
  ∀ m ≤ n,
    encode (α := Option (List ℕ))
        (List.foldr
          (fun (x : ℕ) (y : Option (List ℕ)) ↦ Option.bind (decode x) fun (a : α) ↦ Option.map (List.cons (encode a)) y)
          (some []) (ofNat (List ℕ) m)) =
      encode.{u_1} (α := Option (List α)) (decode m)
hi :
  encode (α := Option (List ℕ))
      (Option.bind (decode (Nat.unpair n).1) fun (a : α) ↦
        Option.map (List.cons (encode a))
          (List.foldr
            (fun (x : ℕ) (y : Option (List ℕ)) ↦
              Option.bind (decode x) fun (a : α) ↦ Option.map (List.cons (encode a)) y)
            (some []) (ofNat (List ℕ) (Nat.unpair n).2))) =
    encode.{u_1} (α := Option (List α))
      (Option.map (fun (x1 : α) (x2 : List α) ↦ x1 :: x2) (decode (Nat.unpair n).1) <*> decode (Nat.unpair n).2)
⊢ encode (α := Option (List ℕ))
      (List.foldr
        (fun (x : ℕ) (y : Option (List ℕ)) ↦ Option.bind (decode x) fun (a : α) ↦ Option.map (List.cons (encode a)) y)
        (some []) (ofNat (List ℕ) (n + 1))) =
    encode.{u_1} (α := Option (List α)) (decode (n + 1))

Tactic:
simp
-- Module: Mathlib.Computability.Primrec.List
Goal:
α : Type u_1
β : Type u_2
inst : Primcodable α
inst_1 : Primcodable β
H : Nat.Primrec fun (n : ℕ) ↦ encode (α := Option (List ℕ)) (decode n) := ⋯
this_1 : Primrec₂ (σ := Option (List ℕ)) fun (a : α) (o : Option (List ℕ)) ↦ Option.map (List.cons (encode a)) o
this :
  Primrec (β := Option (List ℕ)) fun (n : ℕ) ↦
    List.foldl
      (fun (o : Option (List ℕ)) (m : ℕ) ↦ Option.bind (decode m) fun (a : α) ↦ Option.map (List.cons (encode a)) o)
      (some []) (List.reverse (ofNat (List ℕ) n))
n_1 n : ℕ
IH :
  ∀ m ≤ n,
    encode (α := Option (List ℕ))
        (List.foldr
          (fun (x : ℕ) (y : Option (List ℕ)) ↦ Option.bind (decode x) fun (a : α) ↦ Option.map (List.cons (encode a)) y)
          (some []) (ofNat (List ℕ) m)) =
      encode.{u_1} (α := Option (List α)) (decode m)
hi :
  encode (α := Option (List ℕ))
      (Option.bind none fun (a : α) ↦
        Option.map (List.cons (encode a))
          (List.foldr
            (fun (x : ℕ) (y : Option (List ℕ)) ↦
              Option.bind (decode x) fun (a : α) ↦ Option.map (List.cons (encode a)) y)
            (some []) (ofNat (List ℕ) (Nat.unpair n).2))) =
    encode.{u_1} (α := Option (List α))
      (Option.map (fun (x1 : α) (x2 : List α) ↦ x1 :: x2) none <*> decode (Nat.unpair n).2)
hi₁ :
  ∀ (a : α),
    encode (α := Option (List ℕ))
        ((some a).bind fun (a : α) ↦
          Option.map (List.cons (encode a))
            (List.foldr
              (fun (x : ℕ) (y : Option (List ℕ)) ↦
                Option.bind (decode x) fun (a : α) ↦ Option.map (List.cons (encode a)) y)
              (some []) (ofNat (List ℕ) (Nat.unpair n).2))) =
      encode (α := Option (List α))
        (Option.map (fun (x1 : α) (x2 : List α) ↦ x1 :: x2) (some a) <*> decode (Nat.unpair n).2)
⊢ encode (α := Option (List ℕ))
      (Option.bind (decode (Nat.unpair n).1) fun (a : α) ↦
        Option.map (List.cons (encode a))
          (List.foldr
            (fun (x : ℕ) (y : Option (List ℕ)) ↦
              Option.bind (decode x) fun (a : α) ↦ Option.map (List.cons (encode a)) y)
            (some []) (ofNat (List ℕ) (Nat.unpair n).2))) =
    encode.{u_1} (α := Option (List α))
      (Option.map (fun (x1 : α) (x2 : List α) ↦ x1 :: x2) (decode (Nat.unpair n).1) <*> decode (Nat.unpair n).2)

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

Premises used: Nat.unpair, Prod.fst, Encodable.decode
-- Module: Mathlib.Computability.Primrec.List
Goal:
α : Type u_1
β : Type u_2
inst : Primcodable α
inst_1 : Primcodable β
H : Nat.Primrec fun (n : ℕ) ↦ encode (α := Option (List ℕ)) (decode n) := ⋯
this_1 : Primrec₂ (σ := Option (List ℕ)) fun (a : α) (o : Option (List ℕ)) ↦ Option.map (List.cons (encode a)) o
this :
  Primrec (β := Option (List ℕ)) fun (n : ℕ) ↦
    List.foldl
      (fun (o : Option (List ℕ)) (m : ℕ) ↦ Option.bind (decode m) fun (a : α) ↦ Option.map (List.cons (encode a)) o)
      (some []) (List.reverse (ofNat (List ℕ) n))
n_1 n : ℕ
IH :
  ∀ m ≤ n,
    encode (α := Option (List ℕ))
        (List.foldr
          (fun (x : ℕ) (y : Option (List ℕ)) ↦ Option.bind (decode x) fun (a : α) ↦ Option.map (List.cons (encode a)) y)
          (some []) (ofNat (List ℕ) m)) =
      encode.{u_1} (α := Option (List α)) (decode m)
⊢ encode (α := Option (List ℕ))
      (Option.bind none fun (a : α) ↦
        Option.map (List.cons (encode a))
          (List.foldr
            (fun (x : ℕ) (y : Option (List ℕ)) ↦
              Option.bind (decode x) fun (a : α) ↦ Option.map (List.cons (encode a)) y)
            (some []) (ofNat (List ℕ) (Nat.unpair n).2))) =
    encode.{u_1} (α := Option (List α))
      (Option.map (fun (x1 : α) (x2 : List α) ↦ x1 :: x2) none <*> decode (Nat.unpair n).2)

Tactic:
rfl
-- Module: Mathlib.Computability.Primrec.List
Goal:
α : Type u_1
β : Type u_2
inst : Primcodable α
inst_1 : Primcodable β
H : Nat.Primrec fun (n : ℕ) ↦ encode (α := Option (List ℕ)) (decode n) := ⋯
this_1 : Primrec₂ (σ := Option (List ℕ)) fun (a : α) (o : Option (List ℕ)) ↦ Option.map (List.cons (encode a)) o
this :
  Primrec (β := Option (List ℕ)) fun (n : ℕ) ↦
    List.foldl
      (fun (o : Option (List ℕ)) (m : ℕ) ↦ Option.bind (decode m) fun (a : α) ↦ Option.map (List.cons (encode a)) o)
      (some []) (List.reverse (ofNat (List ℕ) n))
n_1 n : ℕ
IH :
  ∀ m ≤ n,
    encode (α := Option (List ℕ))
        (List.foldr
          (fun (x : ℕ) (y : Option (List ℕ)) ↦ Option.bind (decode x) fun (a : α) ↦ Option.map (List.cons (encode a)) y)
          (some []) (ofNat (List ℕ) m)) =
      encode.{u_1} (α := Option (List α)) (decode m)
a : α
hi :
  ∀ (o : Option (List ℕ)) (p : Option (List α)),
    encode o = encode p → encode (Option.map (List.cons (encode a)) o) = encode (Option.map (List.cons a) p)
⊢ encode
      (Option.map (List.cons (encode a))
        (List.foldr
          (fun (x : ℕ) (y : Option (List ℕ)) ↦ Option.bind (decode x) fun (a : α) ↦ Option.map (List.cons (encode a)) y)
          (some []) (ofNat (List ℕ) (Nat.unpair n).2))) =
    encode.{u_1} (α := Option (List α)) ((some fun (x2 : List α) ↦ a :: x2) <*> decode (Nat.unpair n).2)

Tactic:
suffices ∀ (o : Option (List ℕ)) (p), encode o = encode p →
            encode (Option.map (List.cons (encode a)) o) = encode (Option.map (List.cons a) p) from
          this _ _ (IH _ (Nat.unpair_right_le n))