awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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_1 :
  ∀ 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 : α
o : Option (List ℕ)
p : Option (List α)
IH : encode o = encode p
hi :
  ∀ (IH : encode (α := Option (List ℕ)) none = encode p),
    encode (Option.map (List.cons (encode a)) none) = encode (Option.map (List.cons a) p)
hi₁ :
  ∀ (val : List ℕ) (IH : encode (some val) = encode p),
    encode (Option.map (List.cons (encode a)) (some val)) = encode (Option.map (List.cons a) p)
⊢ encode (Option.map (List.cons (encode a)) o) = encode (Option.map (List.cons a) p)

Tactic:
cases o
-- 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_1 :
  ∀ 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 : α
p : Option (List α)
IH : encode (α := Option (List ℕ)) none = encode p
hi :
  ∀ (IH : encode (α := Option (List ℕ)) none = encode.{u_1} (α := Option (List α)) none),
    encode (Option.map (List.cons (encode a)) none) = encode (Option.map (List.cons a) none)
hi₁ :
  ∀ (val : List α) (IH : encode (α := Option (List ℕ)) none = encode (some val)),
    encode (Option.map (List.cons (encode a)) none) = encode (Option.map (List.cons a) (some val))
⊢ encode (Option.map (List.cons (encode a)) none) = encode (Option.map (List.cons a) p)

Tactic:
cases p
-- 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_1 :
  ∀ 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 : α
p : Option (List α)
val : List ℕ
IH : encode (some val) = encode p
hi :
  ∀ (IH : encode (some val) = encode.{u_1} (α := Option (List α)) none),
    encode (Option.map (List.cons (encode a)) (some val)) = encode (Option.map (List.cons a) none)
hi₁ :
  ∀ (val_1 : List α) (IH : encode (some val) = encode (some val_1)),
    encode (Option.map (List.cons (encode a)) (some val)) = encode (Option.map (List.cons a) (some val_1))
⊢ encode (Option.map (List.cons (encode a)) (some val)) = encode (Option.map (List.cons a) p)

Tactic:
cases p
-- 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_1 :
  ∀ 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 : α
IH : encode (α := Option (List ℕ)) none = encode.{u_1} (α := Option (List α)) none
⊢ encode (Option.map (List.cons (encode a)) none) = encode (Option.map (List.cons a) none)

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_1 :
  ∀ 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 : α
val : List α
IH : encode (α := Option (List ℕ)) none = encode (some val)
⊢ encode (Option.map (List.cons (encode a)) none) = encode (Option.map (List.cons a) (some val))

Tactic:
injection IH
-- 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_1 :
  ∀ 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 : α
val : List ℕ
IH : encode (some val) = encode.{u_1} (α := Option (List α)) none
⊢ encode (Option.map (List.cons (encode a)) (some val)) = encode (Option.map (List.cons a) none)

Tactic:
injection IH
-- 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_1 :
  ∀ 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 : α
val : List ℕ
val_1 : List α
IH : encode (some val) = encode (some val_1)
⊢ encode (Option.map (List.cons (encode a)) (some val)) = encode (Option.map (List.cons a) (some val_1))

Tactic:
congr_arg (fun k => (Nat.pair (encode a) k).succ.succ) (Nat.succ.inj IH)

Premises used: Nat.pair, congr_arg, Nat.succ.inj, Encodable.encodeList, Encodable.encode, Nat.succ
-- 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_1 :
  ∀ 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 : α
val : List ℕ
val_1 : List α
IH : encode (some val) = encode (some val_1)
⊢ encode (Option.map (List.cons (encode a)) (some val)) = encode (Option.map (List.cons a) (some val_1))

Tactic:
exact congr_arg (fun k => (Nat.pair (encode a) k).succ.succ) (Nat.succ.inj IH)

Premises used: Nat.pair, congr_arg, Nat.succ.inj, Encodable.encode, Nat.succ
-- Module: Mathlib.Computability.Primrec.List
Goal:
α : Type u_1
inst : Primcodable α
⊢ Primrec₂.{u_1, u_1, u_1} (α := α) List.cons

Tactic:
list_cons' (Primcodable.prim _)

Premises used: _private.0.list_cons'
-- Module: Mathlib.Computability.Primrec.List
Goal:
α : Type u_1
β : Type u_2
σ : Type u_4
inst : Primcodable α
inst_1 : Primcodable β
inst_2 : Primcodable σ
f : α → List β
g : α → σ
h : α → β × List β → σ
⊢ Primrec f →
    Primrec g →
      Primrec₂ h →
        Primrec.{u_1, u_4} (β := σ) fun (a : α) ↦
          List.casesOn (motive := fun (x : List β) ↦ σ) (f a) (g a) fun (b : β) (l : List β) ↦ h a (b, l)

Tactic:
list_casesOn' (Primcodable.prim _)

Premises used: _private.0.list_casesOn'
-- Module: Mathlib.Computability.Primrec.List
Goal:
α : Type u_1
β : Type u_2
σ : Type u_4
inst : Primcodable α
inst_1 : Primcodable β
inst_2 : Primcodable σ
f : α → List β
g : α → σ
h : α → σ × β → σ
⊢ Primrec f →
    Primrec g →
      Primrec₂ h → Primrec.{u_1, u_4} (β := σ) fun (a : α) ↦ List.foldl (fun (s : σ) (b : β) ↦ h a (s, b)) (g a) (f a)

Tactic:
list_foldl' (Primcodable.prim _)

Premises used: _private.0.list_foldl'
-- Module: Mathlib.Computability.Primrec.List
Goal:
α : Type u_1
inst : Primcodable α
⊢ Primrec.{u_1, u_1} (α := List α) List.reverse

Tactic:
list_reverse' (Primcodable.prim _)

Premises used: _private.0.list_reverse'
-- Module: Mathlib.Computability.Primrec.List
Goal:
α : Type u_1
β : Type u_2
σ : Type u_4
inst : Primcodable α
inst_1 : Primcodable β
inst_2 : Primcodable σ
f : α → List β
g : α → σ
h : α → β × σ → σ
hf : Primrec f
hg : Primrec g
hh : Primrec₂ h
a : α
⊢ List.foldl (fun (s : σ) (b : β) ↦ h (a, s, b).1 ((a, s, b).2.2, (a, s, b).2.1)) (g a) (f a).reverse =
    List.foldr (fun (b : β) (s : σ) ↦ h a (b, s)) (g a) (f a)

Tactic:
simp [List.foldl_reverse]

Premises used: List.foldl_reverse
-- Module: Mathlib.Computability.Primrec.List
Goal:
α : Type u_1
inst : Primcodable α
l : List α
nil :
  Eq.{u_1 + 1} (α := Option α)
    (List.casesOn (motive := fun (x : List α) ↦ Option α) (id []) none fun (b : α) (l : List α) ↦ some ([], b, l).2.1 :
      Option α)
    (List.head? [] : Option α)
cons :
  ∀ (head : α) (tail : List α),
    (List.casesOn (motive := fun (x : List α) ↦ Option α) (id (head :: tail)) none fun (b : α) (l : List α) ↦
        some (head :: tail, b, l).2.1) =
      (head :: tail).head?
⊢ (List.casesOn (motive := fun (x : List α) ↦ Option α) (id l) none fun (b : α) (l_1 : List α) ↦ some (l, b, l_1).2.1) =
    l.head?

Tactic:
cases l
-- Module: Mathlib.Computability.Primrec.List
Goal:
α : Type u_1
inst : Primcodable α
⊢ Eq.{u_1 + 1} (α := Option α)
    (List.casesOn (motive := fun (x : List α) ↦ Option α) (id []) none fun (b : α) (l : List α) ↦ some ([], b, l).2.1 :
      Option α)
    (List.head? [] : Option α)

Tactic:
rfl
-- Module: Mathlib.Computability.Primrec.List
Goal:
α : Type u_1
inst : Primcodable α
head : α
tail : List α
⊢ (List.casesOn (motive := fun (x : List α) ↦ Option α) (id (head :: tail)) none fun (b : α) (l : List α) ↦
      some (head :: tail, b, l).2.1) =
    (head :: tail).head?

Tactic:
rfl
-- Module: Mathlib.Computability.Primrec.List
Goal:
α : Type u_1
inst : Primcodable α
inst_1 : Inhabited α
⊢ Primrec.{u_1, u_1} (α := List α) List.headI

Tactic:
(option_getD_default.comp list_head?).of_eq fun l => l.head!_eq_head?_getD.symm

Premises used: Primrec.of_eq, Primrec.option_getD_default, List.head!_eq_head?_getD, Primrec.comp, Eq.symm, Primrec.list_head?
-- Module: Mathlib.Computability.Primrec.List
Goal:
α : Type u_1
inst : Primcodable α
l : List α
nil :
  Eq.{u_1 + 1} (α := List α)
    (List.casesOn (motive := fun (x : List α) ↦ List α) (id []) [] fun (b : α) (l : List α) ↦ ([], b, l).2.2 : List α)
    (List.tail [] : List α)
cons :
  ∀ (head : α) (tail : List α),
    (List.casesOn (motive := fun (x : List α) ↦ List α) (id (head :: tail)) [] fun (b : α) (l : List α) ↦
        (head :: tail, b, l).2.2) =
      (head :: tail).tail
⊢ (List.casesOn (motive := fun (x : List α) ↦ List α) (id l) [] fun (b : α) (l_1 : List α) ↦ (l, b, l_1).2.2) = l.tail

Tactic:
cases l
-- Module: Mathlib.Computability.Primrec.List
Goal:
α : Type u_1
inst : Primcodable α
⊢ Eq.{u_1 + 1} (α := List α)
    (List.casesOn (motive := fun (x : List α) ↦ List α) (id []) [] fun (b : α) (l : List α) ↦ ([], b, l).2.2 : List α)
    (List.tail [] : List α)

Tactic:
rfl
-- Module: Mathlib.Computability.Primrec.List
Goal:
α : Type u_1
inst : Primcodable α
head : α
tail : List α
⊢ (List.casesOn (motive := fun (x : List α) ↦ List α) (id (head :: tail)) [] fun (b : α) (l : List α) ↦
      (head :: tail, b, l).2.2) =
    (head :: tail).tail

Tactic:
rfl
-- Module: Mathlib.Computability.Primrec.List
Goal:
α : Type u_1
β : Type u_2
σ : Type u_4
inst : Primcodable α
inst_1 : Primcodable β
inst_2 : Primcodable σ
f : α → List β
g : α → σ
h : α → β × Prod.{u_2, u_4} (List β) σ → σ
hf : Primrec f
hg : Primrec g
hh : Primrec₂ h
F : (a : α) → Prod.{u_2, u_4} (List β) σ :=
  fun (a : α) ↦ List.foldr (fun (b : β) (s : Prod.{u_2, u_4} (List β) σ) ↦ (b :: s.1, h a (b, s))) ([], g a) (f a)
this_1 : Primrec F
a : α
this :
  F a =
    (f a, List.recOn (motive := fun (x : List β) ↦ σ) (f a) (g a) fun (b : β) (l : List β) (IH : σ) ↦ h a (b, l, IH))
rw rw₁ :
  Eq.{u_4 + 1} (α := σ)
    ((f a,
          List.recOn (motive := fun (x : List β) ↦ σ) (f a) (g a) fun (b : β) (l : List β) (IH : σ) ↦
            h a (b, l, IH)).2 :
      σ)
    (List.recOn (motive := fun (x : List β) ↦ σ) (f a) (g a) fun (b : β) (l : List β) (IH : σ) ↦ h a (b, l, IH) : σ)
⊢ (F a).2 = List.recOn (motive := fun (x : List β) ↦ σ) (f a) (g a) fun (b : β) (l : List β) (IH : σ) ↦ h a (b, l, IH)

Tactic:
rw [this]
-- Module: Mathlib.Computability.Primrec.List
Goal:
α : Type u_1
β : Type u_2
σ : Type u_4
inst : Primcodable α
inst_1 : Primcodable β
inst_2 : Primcodable σ
f : α → List β
g : α → σ
h : α → β × Prod.{u_2, u_4} (List β) σ → σ
hf : Primrec f
hg : Primrec g
hh : Primrec₂ h
F : (a : α) → Prod.{u_2, u_4} (List β) σ :=
  fun (a : α) ↦ List.foldr (fun (b : β) (s : Prod.{u_2, u_4} (List β) σ) ↦ (b :: s.1, h a (b, s))) ([], g a) (f a)
this : Primrec F
a : α
suffices :
  F a =
    (f a, List.recOn (motive := fun (x : List β) ↦ σ) (f a) (g a) fun (b : β) (l : List β) (IH : σ) ↦ h a (b, l, IH))
⊢ (F a).2 = List.recOn (motive := fun (x : List β) ↦ σ) (f a) (g a) fun (b : β) (l : List β) (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]
-- Module: Mathlib.Computability.Primrec.List
Goal:
α : Type u_1
β : Type u_2
σ : Type u_4
inst : Primcodable α
inst_1 : Primcodable β
inst_2 : Primcodable σ
f : α → List β
g : α → σ
h : α → β × Prod.{u_2, u_4} (List β) σ → σ
hf : Primrec f
hg : Primrec g
hh : Primrec₂ h
F : (a : α) → Prod.{u_2, u_4} (List β) σ :=
  fun (a : α) ↦ List.foldr (fun (b : β) (s : Prod.{u_2, u_4} (List β) σ) ↦ (b :: s.1, h a (b, s))) ([], g a) (f a)
this : Primrec F
a : α
dsimp :
  Eq (α := Prod.{u_2, u_4} (List β) σ)
    (List.foldr (fun (b : β) (s : Prod.{u_2, u_4} (List β) σ) ↦ (b :: s.1, h a (b, s))) ([], g a) (f a))
    (f a, List.rec (motive := fun (x : List β) ↦ σ) (g a) (fun (b : β) (l : List β) (IH : σ) ↦ h a (b, l, IH)) (f a))
⊢ F a =
    (f a, List.recOn (motive := fun (x : List β) ↦ σ) (f a) (g a) fun (b : β) (l : List β) (IH : σ) ↦ h a (b, l, IH))

Tactic:
dsimp [F]
-- Module: Mathlib.Computability.Primrec.List
Goal:
α : Type u_1
β : Type u_2
σ : Type u_4
inst : Primcodable α
inst_1 : Primcodable β
inst_2 : Primcodable σ
f : α → List β
g : α → σ
h : α → β × Prod.{u_2, u_4} (List β) σ → σ
hf : Primrec f
hg : Primrec g
hh : Primrec₂ h
F : (a : α) → Prod.{u_2, u_4} (List β) σ :=
  fun (a : α) ↦ List.foldr (fun (b : β) (s : Prod.{u_2, u_4} (List β) σ) ↦ (b :: s.1, h a (b, s))) ([], g a) (f a)
this : Primrec F
a : α
nil :
  Eq (α := Prod.{u_2, u_4} (List β) σ)
    (List.foldr (fun (b : β) (s : Prod.{u_2, u_4} (List β) σ) ↦ (b :: s.1, h a (b, s))) ([], g a) [])
    ([], List.rec (motive := fun (x : List β) ↦ σ) (g a) (fun (b : β) (l : List β) (IH : σ) ↦ h a (b, l, IH)) [])
cons :
  ∀ (head : β) (tail : List β),
    Eq (α := Prod.{u_2, u_4} (List β) σ)
        (List.foldr (fun (b : β) (s : Prod.{u_2, u_4} (List β) σ) ↦ (b :: s.1, h a (b, s))) ([], g a) tail)
        (tail,
          List.rec (motive := fun (x : List β) ↦ σ) (g a) (fun (b : β) (l : List β) (IH : σ) ↦ h a (b, l, IH)) tail) →
      Eq (α := Prod.{u_2, u_4} (List β) σ)
        (List.foldr (fun (b : β) (s : Prod.{u_2, u_4} (List β) σ) ↦ (b :: s.1, h a (b, s))) ([], g a) (head :: tail))
        (head :: tail,
          List.rec (motive := fun (x : List β) ↦ σ) (g a) (fun (b : β) (l : List β) (IH : σ) ↦ h a (b, l, IH))
            (head :: tail))
⊢ Eq (α := Prod.{u_2, u_4} (List β) σ)
    (List.foldr (fun (b : β) (s : Prod.{u_2, u_4} (List β) σ) ↦ (b :: s.1, h a (b, s))) ([], g a) (f a))
    (f a, List.rec (motive := fun (x : List β) ↦ σ) (g a) (fun (b : β) (l : List β) (IH : σ) ↦ h a (b, l, IH)) (f a))

Tactic:
induction f a
-- Module: Mathlib.Computability.Primrec.List
Goal:
α : Type u_1
β : Type u_2
σ : Type u_4
inst : Primcodable α
inst_1 : Primcodable β
inst_2 : Primcodable σ
f : α → List β
g : α → σ
h : α → β × Prod.{u_2, u_4} (List β) σ → σ
hf : Primrec f
hg : Primrec g
hh : Primrec₂ h
F : (a : α) → Prod.{u_2, u_4} (List β) σ :=
  fun (a : α) ↦ List.foldr (fun (b : β) (s : Prod.{u_2, u_4} (List β) σ) ↦ (b :: s.1, h a (b, s))) ([], g a) (f a)
this : Primrec F
a : α
⊢ Eq (α := Prod.{u_2, u_4} (List β) σ)
    (List.foldr (fun (b : β) (s : Prod.{u_2, u_4} (List β) σ) ↦ (b :: s.1, h a (b, s))) ([], g a) [])
    ([], List.rec (motive := fun (x : List β) ↦ σ) (g a) (fun (b : β) (l : List β) (IH : σ) ↦ h a (b, l, IH)) [])

Tactic:
simp [*]
-- Module: Mathlib.Computability.Primrec.List
Goal:
α : Type u_1
β : Type u_2
σ : Type u_4
inst : Primcodable α
inst_1 : Primcodable β
inst_2 : Primcodable σ
f : α → List β
g : α → σ
h : α → β × Prod.{u_2, u_4} (List β) σ → σ
hf : Primrec f
hg : Primrec g
hh : Primrec₂ h
F : (a : α) → Prod.{u_2, u_4} (List β) σ :=
  fun (a : α) ↦ List.foldr (fun (b : β) (s : Prod.{u_2, u_4} (List β) σ) ↦ (b :: s.1, h a (b, s))) ([], g a) (f a)
this : Primrec F
a : α
head : β
tail : List β
tail_ih :
  Eq (α := Prod.{u_2, u_4} (List β) σ)
    (List.foldr (fun (b : β) (s : Prod.{u_2, u_4} (List β) σ) ↦ (b :: s.1, h a (b, s))) ([], g a) tail)
    (tail, List.rec (motive := fun (x : List β) ↦ σ) (g a) (fun (b : β) (l : List β) (IH : σ) ↦ h a (b, l, IH)) tail)
⊢ Eq (α := Prod.{u_2, u_4} (List β) σ)
    (List.foldr (fun (b : β) (s : Prod.{u_2, u_4} (List β) σ) ↦ (b :: s.1, h a (b, s))) ([], g a) (head :: tail))
    (head :: tail,
      List.rec (motive := fun (x : List β) ↦ σ) (g a) (fun (b : β) (l : List β) (IH : σ) ↦ h a (b, l, IH))
        (head :: tail))

Tactic:
simp [*]
-- Module: Mathlib.Computability.Primrec.List
Goal:
α : Type u_1
inst : Primcodable α
F : (l : List α) → (n : ℕ) → ℕ ⊕ α :=
  fun (l : List α) (n : ℕ) ↦
    List.foldl
      (fun (s : ℕ ⊕ α) (a : α) ↦
        Sum.casesOn (motive := fun (x : ℕ ⊕ α) ↦ ℕ ⊕ α) s
          (fun (x : ℕ) ↦ Nat.casesOn (motive := fun (x : ℕ) ↦ ℕ ⊕ α) x (Sum.inr a) Sum.inl) Sum.inr)
      (Sum.inl n) l
hF : Primrec₂ F
this :
  Primrec (β := Option α) fun (p : List α × ℕ) ↦
    Sum.casesOn (motive := fun (x : ℕ ⊕ α) ↦ Option α) (F p.1 p.2) (fun (x : ℕ) ↦ none) some
l : List α
n : ℕ
dsimp :
  Sum.rec (motive := fun (x : ℕ ⊕ α) ↦ Option α) (fun (val : ℕ) ↦ none) (fun (val : α) ↦ some val) (F l n) =
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l n
⊢ Sum.casesOn (motive := fun (x : ℕ ⊕ α) ↦ Option α) (F (l, n).1 (l, n).2) (fun (x : ℕ) ↦ none) some =
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l n

Tactic:
dsimp
-- Module: Mathlib.Computability.Primrec.List
Goal:
α : Type u_1
inst : Primcodable α
F : (l : List α) → (n : ℕ) → ℕ ⊕ α :=
  fun (l : List α) (n : ℕ) ↦
    List.foldl
      (fun (s : ℕ ⊕ α) (a : α) ↦
        Sum.casesOn (motive := fun (x : ℕ ⊕ α) ↦ ℕ ⊕ α) s
          (fun (x : ℕ) ↦ Nat.casesOn (motive := fun (x : ℕ) ↦ ℕ ⊕ α) x (Sum.inr a) Sum.inl) Sum.inr)
      (Sum.inl n) l
hF : Primrec₂ F
this :
  Primrec (β := Option α) fun (p : List α × ℕ) ↦
    Sum.casesOn (motive := fun (x : ℕ ⊕ α) ↦ Option α) (F p.1 p.2) (fun (x : ℕ) ↦ none) some
l : List α
n : ℕ
symm :
  getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l n =
    Sum.rec (motive := fun (x : ℕ ⊕ α) ↦ Option α) (fun (val : ℕ) ↦ none) (fun (val : α) ↦ some val) (F l n)
⊢ Sum.rec (motive := fun (x : ℕ ⊕ α) ↦ Option α) (fun (val : ℕ) ↦ none) (fun (val : α) ↦ some val) (F l n) =
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l n

Tactic:
symm
-- Module: Mathlib.Computability.Primrec.List
Goal:
α : Type u_1
inst : Primcodable α
F : (l : List α) → (n : ℕ) → ℕ ⊕ α :=
  fun (l : List α) (n : ℕ) ↦
    List.foldl
      (fun (s : ℕ ⊕ α) (a : α) ↦
        Sum.casesOn (motive := fun (x : ℕ ⊕ α) ↦ ℕ ⊕ α) s
          (fun (x : ℕ) ↦ Nat.casesOn (motive := fun (x : ℕ) ↦ ℕ ⊕ α) x (Sum.inr a) Sum.inl) Sum.inr)
      (Sum.inl n) l
hF : Primrec₂ F
this :
  Primrec (β := Option α) fun (p : List α × ℕ) ↦
    Sum.casesOn (motive := fun (x : ℕ ⊕ α) ↦ Option α) (F p.1 p.2) (fun (x : ℕ) ↦ none) some
n : ℕ
⊢ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) [] n =
    Sum.rec (motive := fun (x : ℕ ⊕ α) ↦ Option α) (fun (val : ℕ) ↦ none) (fun (val : α) ↦ some val) (F [] n)

Tactic:
rfl