awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
a : α
l : List α
IH :
  ∀ (n : ℕ),
    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)
n : ℕ
cons :
  getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (a :: l) 0 =
    Sum.rec (motive := fun (x : ℕ ⊕ α) ↦ Option α) (fun (val : ℕ) ↦ none) (fun (val : α) ↦ some val) (F (a :: l) 0)
cons₁ :
  ∀ (n : ℕ),
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (a :: l) (n + 1) =
      Sum.rec (motive := fun (x : ℕ ⊕ α) ↦ Option α) (fun (val : ℕ) ↦ none) (fun (val : α) ↦ some val)
        (F (a :: l) (n + 1))
⊢ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (a :: l) n =
    Sum.rec (motive := fun (x : ℕ ⊕ α) ↦ Option α) (fun (val : ℕ) ↦ none) (fun (val : α) ↦ some val) (F (a :: l) n)

Tactic:
rcases n with - | n
-- 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
a : α
l : List α
IH :
  ∀ (n : ℕ),
    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)
cons :
  getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (a :: l) 0 =
    Sum.rec (motive := fun (x : ℕ ⊕ α) ↦ Option α) (fun (val : ℕ) ↦ none) (fun (val : α) ↦ some val)
      (List.foldl
        (fun (s : ℕ ⊕ α) (a : α) ↦
          Sum.rec (motive := fun (x : ℕ ⊕ α) ↦ ℕ ⊕ α)
            (fun (val : ℕ) ↦
              Nat.rec (motive := fun (x : ℕ) ↦ ℕ ⊕ α) (Sum.inr a) (fun (n : ℕ) (n_ih : ℕ ⊕ α) ↦ Sum.inl n) val)
            (fun (val : α) ↦ Sum.inr val) s)
        (Sum.inr a) l)
⊢ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (a :: l) 0 =
    Sum.rec (motive := fun (x : ℕ ⊕ α) ↦ Option α) (fun (val : ℕ) ↦ none) (fun (val : α) ↦ some val) (F (a :: l) 0)

Tactic:
dsimp [F]
-- 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
a : α
l : List α
cons :
  getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) [a] 0 =
    Sum.rec (motive := fun (x : ℕ ⊕ α) ↦ Option α) (fun (val : ℕ) ↦ none) (fun (val : α) ↦ some val)
      (List.foldl
        (fun (s : ℕ ⊕ α) (a : α) ↦
          Sum.rec (motive := fun (x : ℕ ⊕ α) ↦ ℕ ⊕ α)
            (fun (val : ℕ) ↦
              Nat.rec (motive := fun (x : ℕ) ↦ ℕ ⊕ α) (Sum.inr a) (fun (n : ℕ) (n_ih : ℕ ⊕ α) ↦ Sum.inl n) val)
            (fun (val : α) ↦ Sum.inr val) s)
        (Sum.inr a) [])
cons₁ :
  ∀ (head : α) (tail : List α),
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (a :: tail) 0 =
        Sum.rec (motive := fun (x : ℕ ⊕ α) ↦ Option α) (fun (val : ℕ) ↦ none) (fun (val : α) ↦ some val)
          (List.foldl
            (fun (s : ℕ ⊕ α) (a : α) ↦
              Sum.rec (motive := fun (x : ℕ ⊕ α) ↦ ℕ ⊕ α)
                (fun (val : ℕ) ↦
                  Nat.rec (motive := fun (x : ℕ) ↦ ℕ ⊕ α) (Sum.inr a) (fun (n : ℕ) (n_ih : ℕ ⊕ α) ↦ Sum.inl n) val)
                (fun (val : α) ↦ Sum.inr val) s)
            (Sum.inr a) tail) →
      getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (a :: head :: tail) 0 =
        Sum.rec (motive := fun (x : ℕ ⊕ α) ↦ Option α) (fun (val : ℕ) ↦ none) (fun (val : α) ↦ some val)
          (List.foldl
            (fun (s : ℕ ⊕ α) (a : α) ↦
              Sum.rec (motive := fun (x : ℕ ⊕ α) ↦ ℕ ⊕ α)
                (fun (val : ℕ) ↦
                  Nat.rec (motive := fun (x : ℕ) ↦ ℕ ⊕ α) (Sum.inr a) (fun (n : ℕ) (n_ih : ℕ ⊕ α) ↦ Sum.inl n) val)
                (fun (val : α) ↦ Sum.inr val) s)
            (Sum.inr a) (head :: tail))
⊢ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (a :: l) 0 =
    Sum.rec (motive := fun (x : ℕ ⊕ α) ↦ Option α) (fun (val : ℕ) ↦ none) (fun (val : α) ↦ some val)
      (List.foldl
        (fun (s : ℕ ⊕ α) (a : α) ↦
          Sum.rec (motive := fun (x : ℕ ⊕ α) ↦ ℕ ⊕ α)
            (fun (val : ℕ) ↦
              Nat.rec (motive := fun (x : ℕ) ↦ ℕ ⊕ α) (Sum.inr a) (fun (n : ℕ) (n_ih : ℕ ⊕ α) ↦ Sum.inl n) val)
            (fun (val : α) ↦ Sum.inr val) s)
        (Sum.inr a) l)

Tactic:
induction l
-- 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
a : α
⊢ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) [a] 0 =
    Sum.rec (motive := fun (x : ℕ ⊕ α) ↦ Option α) (fun (val : ℕ) ↦ none) (fun (val : α) ↦ some val)
      (List.foldl
        (fun (s : ℕ ⊕ α) (a : α) ↦
          Sum.rec (motive := fun (x : ℕ ⊕ α) ↦ ℕ ⊕ α)
            (fun (val : ℕ) ↦
              Nat.rec (motive := fun (x : ℕ) ↦ ℕ ⊕ α) (Sum.inr a) (fun (n : ℕ) (n_ih : ℕ ⊕ α) ↦ Sum.inl n) val)
            (fun (val : α) ↦ Sum.inr val) s)
        (Sum.inr a) [])

Tactic:
simp_all
-- 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
a head : α
tail : List α
tail_ih :
  getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (a :: tail) 0 =
    Sum.rec (motive := fun (x : ℕ ⊕ α) ↦ Option α) (fun (val : ℕ) ↦ none) (fun (val : α) ↦ some val)
      (List.foldl
        (fun (s : ℕ ⊕ α) (a : α) ↦
          Sum.rec (motive := fun (x : ℕ ⊕ α) ↦ ℕ ⊕ α)
            (fun (val : ℕ) ↦
              Nat.rec (motive := fun (x : ℕ) ↦ ℕ ⊕ α) (Sum.inr a) (fun (n : ℕ) (n_ih : ℕ ⊕ α) ↦ Sum.inl n) val)
            (fun (val : α) ↦ Sum.inr val) s)
        (Sum.inr a) tail)
⊢ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (a :: head :: tail) 0 =
    Sum.rec (motive := fun (x : ℕ ⊕ α) ↦ Option α) (fun (val : ℕ) ↦ none) (fun (val : α) ↦ some val)
      (List.foldl
        (fun (s : ℕ ⊕ α) (a : α) ↦
          Sum.rec (motive := fun (x : ℕ ⊕ α) ↦ ℕ ⊕ α)
            (fun (val : ℕ) ↦
              Nat.rec (motive := fun (x : ℕ) ↦ ℕ ⊕ α) (Sum.inr a) (fun (n : ℕ) (n_ih : ℕ ⊕ α) ↦ Sum.inl n) val)
            (fun (val : α) ↦ Sum.inr val) s)
        (Sum.inr a) (head :: tail))

Tactic:
simp_all
-- 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
a : α
l : List α
IH :
  ∀ (n : ℕ),
    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)
n : ℕ
⊢ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (a :: l) (n + 1) =
    Sum.rec (motive := fun (x : ℕ ⊕ α) ↦ Option α) (fun (val : ℕ) ↦ none) (fun (val : α) ↦ some val)
      (F (a :: l) (n + 1))

Tactic:
simpa using IH ..
-- 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 : ℕ
nil :
  ∀ (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)
cons :
  ∀ (a : α) (l : List α)
    (IH :
      ∀ (n : ℕ),
        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))
    (n : ℕ),
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (a :: l) n =
      Sum.rec (motive := fun (x : ℕ ⊕ α) ↦ Option α) (fun (val : ℕ) ↦ none) (fun (val : α) ↦ some val) (F (a :: l) n)
⊢ 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)

Tactic:
induction l generalizing n with
    | nil => rfl
    | cons a l IH =>
      rcases n with - | n
      · dsimp [F]
        clear IH
        induction l <;> simp_all
      · simpa using IH ..
-- Module: Mathlib.Computability.Primrec.List
Goal:
α : Type u_1
inst : Primcodable α
d : α
⊢ Primrec₂ (σ := α) fun (l : List α) (n : ℕ) ↦
    (getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l n).getD d

Tactic:
option_getD.comp₂ list_getElem? (const _)

Premises used: Primrec.const, Primrec.option_getD, Primrec.list_getElem?, Primrec₂.comp₂
-- Module: Mathlib.Computability.Primrec.List
Goal:
α : Type u_1
inst : Primcodable α
d : α
⊢ Primrec₂ (σ := α) fun (l : List α) (n : ℕ) ↦
    (getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l n).getD d

Tactic:
exact option_getD.comp₂ list_getElem? (const _)
-- Module: Mathlib.Computability.Primrec.List
Goal:
α : Type u_1
inst : Primcodable α
inst_1 : Inhabited α
⊢ Primrec₂.{u_1, 0, u_1} (α := List α) List.getI

Tactic:
list_getD _

Premises used: Primrec.list_getD, List.getI
-- Module: Mathlib.Computability.Primrec.List
Goal:
α : Type u_1
inst : Primcodable α
l₁ l₂ : List α
nil :
  List.foldr (fun (b : α) (s : List α) ↦ (([], l₂), b, s).2.1 :: (([], l₂), b, s).2.2) ([], l₂).2 ([], l₂).1 = [] ++ l₂
cons :
  ∀ (head : α) (tail : List α),
    List.foldr (fun (b : α) (s : List α) ↦ ((tail, l₂), b, s).2.1 :: ((tail, l₂), b, s).2.2) (tail, l₂).2 (tail, l₂).1 =
        tail ++ l₂ →
      List.foldr (fun (b : α) (s : List α) ↦ ((head :: tail, l₂), b, s).2.1 :: ((head :: tail, l₂), b, s).2.2)
          (head :: tail, l₂).2 (head :: tail, l₂).1 =
        head :: tail ++ l₂
⊢ List.foldr (fun (b : α) (s : List α) ↦ ((l₁, l₂), b, s).2.1 :: ((l₁, l₂), b, s).2.2) (l₁, l₂).2 (l₁, l₂).1 = l₁ ++ l₂

Tactic:
induction l₁
-- Module: Mathlib.Computability.Primrec.List
Goal:
α : Type u_1
inst : Primcodable α
l₂ : List α
⊢ List.foldr (fun (b : α) (s : List α) ↦ (([], l₂), b, s).2.1 :: (([], l₂), b, s).2.2) ([], l₂).2 ([], l₂).1 = [] ++ l₂

Tactic:
simp [*]
-- Module: Mathlib.Computability.Primrec.List
Goal:
α : Type u_1
inst : Primcodable α
l₂ : List α
head : α
tail : List α
tail_ih :
  List.foldr (fun (b : α) (s : List α) ↦ ((tail, l₂), b, s).2.1 :: ((tail, l₂), b, s).2.2) (tail, l₂).2 (tail, l₂).1 =
    tail ++ l₂
⊢ List.foldr (fun (b : α) (s : List α) ↦ ((head :: tail, l₂), b, s).2.1 :: ((head :: tail, l₂), b, s).2.2)
      (head :: tail, l₂).2 (head :: tail, l₂).1 =
    head :: tail ++ l₂

Tactic:
simp [*]
-- Module: Mathlib.Computability.Primrec.List
Goal:
α : Type u_1
inst : Primcodable α
⊢ Primrec₂ (σ := List α) fun (l : List α) (a : α) ↦ l ++ [a]

Tactic:
list_append.comp fst (list_cons.comp snd (const []))

Premises used: Primrec.snd, Primrec.fst, Primrec.const, Primrec.list_cons, Primrec₂.comp, Primrec.list_append, Primrec₂, List.nil
-- 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 : α → β → σ
hf : Primrec f
hg : Primrec₂ g
a : α
nil : List.foldr (fun (b : β) (s : List σ) ↦ g (a, b, s).1 (a, b, s).2.1 :: (a, b, s).2.2) [] [] = List.map (g a) []
cons :
  ∀ (head : β) (tail : List β),
    List.foldr (fun (b : β) (s : List σ) ↦ g (a, b, s).1 (a, b, s).2.1 :: (a, b, s).2.2) [] tail = List.map (g a) tail →
      List.foldr (fun (b : β) (s : List σ) ↦ g (a, b, s).1 (a, b, s).2.1 :: (a, b, s).2.2) [] (head :: tail) =
        List.map (g a) (head :: tail)
⊢ List.foldr (fun (b : β) (s : List σ) ↦ g (a, b, s).1 (a, b, s).2.1 :: (a, b, s).2.2) [] (f a) = List.map (g a) (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 : α → β → σ
hf : Primrec f
hg : Primrec₂ g
a : α
⊢ List.foldr (fun (b : β) (s : List σ) ↦ g (a, b, s).1 (a, b, s).2.1 :: (a, b, s).2.2) [] [] = List.map (g a) []

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 : α → β → σ
hf : Primrec f
hg : Primrec₂ g
a : α
head : β
tail : List β
tail_ih :
  List.foldr (fun (b : β) (s : List σ) ↦ g (a, b, s).1 (a, b, s).2.1 :: (a, b, s).2.2) [] tail = List.map (g a) tail
⊢ List.foldr (fun (b : β) (s : List σ) ↦ g (a, b, s).1 (a, b, s).2.1 :: (a, b, s).2.2) [] (head :: tail) =
    List.map (g a) (head :: tail)

Tactic:
simp [*]
-- Module: Mathlib.Computability.Primrec.List
Goal:
n : ℕ
simp : Nat.rec (motive := fun (x : ℕ) ↦ List ℕ) [] (fun (n : ℕ) (IH : List ℕ) ↦ IH ++ [n]) n = List.range n
⊢ Nat.rec (motive := fun (x : ℕ) ↦ List ℕ) []
      (fun (n_1 : ℕ) (IH : (fun (x : ℕ) ↦ List ℕ) n_1) ↦ (n, n_1, IH).2.2 ++ [(n, n_1, IH).2.1]) (id n) =
    List.range n

Tactic:
simp
-- Module: Mathlib.Computability.Primrec.List
Goal:
n : ℕ
zero : Nat.rec (motive := fun (x : ℕ) ↦ List ℕ) [] (fun (n : ℕ) (IH : List ℕ) ↦ IH ++ [n]) 0 = List.range 0
succ :
  ∀ (n : ℕ),
    Nat.rec (motive := fun (x : ℕ) ↦ List ℕ) [] (fun (n : ℕ) (IH : List ℕ) ↦ IH ++ [n]) n = List.range n →
      Nat.rec (motive := fun (x : ℕ) ↦ List ℕ) [] (fun (n : ℕ) (IH : List ℕ) ↦ IH ++ [n]) (n + 1) = List.range (n + 1)
⊢ Nat.rec (motive := fun (x : ℕ) ↦ List ℕ) [] (fun (n : ℕ) (IH : List ℕ) ↦ IH ++ [n]) n = List.range n

Tactic:
induction n
-- Module: Mathlib.Computability.Primrec.List
Goal:
⊢ Nat.rec (motive := fun (x : ℕ) ↦ List ℕ) [] (fun (n : ℕ) (IH : List ℕ) ↦ IH ++ [n]) 0 = List.range 0

Tactic:
simp [*, List.range_succ]

Premises used: List.range_succ
-- Module: Mathlib.Computability.Primrec.List
Goal:
n : ℕ
h : Nat.rec (motive := fun (x : ℕ) ↦ List ℕ) [] (fun (n : ℕ) (IH : List ℕ) ↦ IH ++ [n]) n = List.range n
⊢ Nat.rec (motive := fun (x : ℕ) ↦ List ℕ) [] (fun (n : ℕ) (IH : List ℕ) ↦ IH ++ [n]) (n + 1) = List.range (n + 1)

Tactic:
simp [*, List.range_succ]

Premises used: List.range_succ
-- Module: Mathlib.Computability.Primrec.List
Goal:
α : Type u_1
inst : Primcodable α
l : List (List α)
dsimp : List.foldr (fun (b s : List α) ↦ b ++ s) [] l = l.flatten
⊢ List.foldr (fun (b s : List α) ↦ (fun (x1 x2 : List α) ↦ x1 ++ x2) (l, b, s).2.1 (l, b, s).2.2) [] (id l) = l.flatten

Tactic:
dsimp
-- Module: Mathlib.Computability.Primrec.List
Goal:
α : Type u_1
inst : Primcodable α
l : List (List α)
nil : Eq.{u_1 + 1} (α := List α) (List.foldr (fun (b s : List α) ↦ b ++ s) [] []) (List.flatten [])
cons :
  ∀ (head : List α) (tail : List (List α)),
    List.foldr (fun (b s : List α) ↦ b ++ s) [] tail = tail.flatten →
      List.foldr (fun (b s : List α) ↦ b ++ s) [] (head :: tail) = (head :: tail).flatten
⊢ List.foldr (fun (b s : List α) ↦ b ++ s) [] l = l.flatten

Tactic:
induction l
-- Module: Mathlib.Computability.Primrec.List
Goal:
α : Type u_1
inst : Primcodable α
⊢ Eq.{u_1 + 1} (α := List α) (List.foldr (fun (b s : List α) ↦ b ++ s) [] []) (List.flatten [])

Tactic:
simp [*]
-- Module: Mathlib.Computability.Primrec.List
Goal:
α : Type u_1
inst : Primcodable α
head : List α
tail : List (List α)
tail_ih : List.foldr (fun (b s : List α) ↦ b ++ s) [] tail = tail.flatten
⊢ List.foldr (fun (b s : List α) ↦ b ++ s) [] (head :: tail) = (head :: tail).flatten

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 : α → β → List σ
hf : Primrec f
hg : Primrec₂ g
⊢ Primrec.{u_1, u_4} (β := List σ) fun (a : α) ↦ List.flatMap (g a) (f a)

Tactic:
list_flatten.comp (list_map hf hg)

Premises used: Primrec.list_map, Primrec.list_flatten, Primrec.comp
-- Module: Mathlib.Computability.Primrec.List
Goal:
α : Type u_1
inst : Primcodable α
o : Option α
none :
  Eq.{u_1 + 1} (α := List α)
    (Option.casesOn (motive := fun (x : Option α) ↦ List α) (id Option.none) [] fun (b : α) ↦ [id b] : List α)
    (Option.toList Option.none : List α)
some :
  ∀ (val : α),
    (Option.casesOn (motive := fun (x : Option α) ↦ List α) (id (Option.some val)) [] fun (b : α) ↦ [id b]) =
      (Option.some val).toList
⊢ (Option.casesOn (motive := fun (x : Option α) ↦ List α) (id o) [] fun (b : α) ↦ [id b]) = o.toList

Tactic:
rcases o
-- Module: Mathlib.Computability.Primrec.List
Goal:
α : Type u_1
inst : Primcodable α
⊢ Eq.{u_1 + 1} (α := List α)
    (Option.casesOn (motive := fun (x : Option α) ↦ List α) (id none) [] fun (b : α) ↦ [id b] : List α)
    (Option.toList none : List α)

Tactic:
simp
-- Module: Mathlib.Computability.Primrec.List
Goal:
α : Type u_1
inst : Primcodable α
val : α
⊢ (Option.casesOn (motive := fun (x : Option α) ↦ List α) (id (some val)) [] fun (b : α) ↦ [id b]) = (some val).toList

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 : α → β → Option σ
hf : Primrec f
hg : Primrec₂ g
⊢ Primrec.{u_1, u_4} (β := List σ) fun (a : α) ↦ List.filterMap (g a) (f a)

Tactic:
(list_flatMap hf (comp₂ optionToList hg)).of_eq
    fun _ ↦ Eq.symm <| List.filterMap_eq_flatMap_toList _ _

Premises used: List.filterMap_eq_flatMap_toList, Primrec.of_eq, Primrec.comp₂, Primrec.list_flatMap, Primrec.optionToList, Eq.symm
-- Module: Mathlib.Computability.Primrec.List
Goal:
α : Type u_1
inst : Primcodable α
l : List α
dsimp : List.foldr (fun (b : α) (s : ℕ) ↦ s + 1) 0 l = l.length
⊢ List.foldr (fun (b : α) (s : ℕ) ↦ (fun (a : List α) (b : α × ℕ) ↦ (a, b).2.2.succ) (l, b, s).1 (l, b, s).2) 0 (id l) =
    l.length

Tactic:
dsimp
-- Module: Mathlib.Computability.Primrec.List
Goal:
α : Type u_1
inst : Primcodable α
l : List α
nil : List.foldr (fun (b : α) (s : ℕ) ↦ s + 1) 0 [] = List.length.{u_1} (α := α) []
cons :
  ∀ (head : α) (tail : List α),
    List.foldr (fun (b : α) (s : ℕ) ↦ s + 1) 0 tail = tail.length →
      List.foldr (fun (b : α) (s : ℕ) ↦ s + 1) 0 (head :: tail) = (head :: tail).length
⊢ List.foldr (fun (b : α) (s : ℕ) ↦ s + 1) 0 l = l.length

Tactic:
induction l
-- Module: Mathlib.Computability.Primrec.List
Goal:
α : Type u_1
inst : Primcodable α
⊢ List.foldr (fun (b : α) (s : ℕ) ↦ s + 1) 0 [] = List.length.{u_1} (α := α) []

Tactic:
simp [*]
-- Module: Mathlib.Computability.Primrec.List
Goal:
α : Type u_1
inst : Primcodable α
head : α
tail : List α
tail_ih : List.foldr (fun (b : α) (s : ℕ) ↦ s + 1) 0 tail = tail.length
⊢ List.foldr (fun (b : α) (s : ℕ) ↦ s + 1) 0 (head :: tail) = (head :: tail).length

Tactic:
simp [*]
-- Module: Mathlib.Computability.Primrec.List
Goal:
α : Type u_1
inst : Primcodable α
p : α → Prop
inst_1 : DecidablePred p
hf : PrimrecPred p
rw : Primrec (β := List α) fun (L : List α) ↦ List.filterMap (Option.guard fun (x : α) ↦ decide (p x)) L
⊢ Primrec (β := List α) fun (L : List α) ↦ List.filter (fun (x : α) ↦ decide (p x)) L

Tactic:
rw [← List.filterMap_eq_filter]

Premises used: List.filterMap_eq_filter
-- Module: Mathlib.Computability.Primrec.List
Goal:
α : Type u_1
inst : Primcodable α
p : α → Prop
inst_1 : DecidablePred p
hf : PrimrecPred p
apply : Primrec₂ (β := α) (σ := Option α) fun (a : List α) ↦ Option.guard fun (x : α) ↦ decide (p x)
⊢ Primrec (β := List α) fun (L : List α) ↦ List.filterMap (Option.guard fun (x : α) ↦ decide (p x)) L

Tactic:
apply listFilterMap .id

Premises used: Primrec.id, Primrec.listFilterMap
-- Module: Mathlib.Computability.Primrec.List
Goal:
α : Type u_1
inst : Primcodable α
p : α → Prop
inst_1 : DecidablePred p
hf : PrimrecPred p
simp : Primrec (β := Option α) fun (p_1 : List α × α) ↦ if p p_1.2 then some p_1.2 else none
⊢ Primrec₂ (β := α) (σ := Option α) fun (a : List α) ↦ Option.guard fun (x : α) ↦ decide (p x)

Tactic:
simp only [Primrec₂, Option.guard, decide_eq_true_eq]

Premises used: Option.guard, decide_eq_true_eq, Primrec₂
-- Module: Mathlib.Computability.Primrec.List
Goal:
α : Type u_1
inst : Primcodable α
p : α → Prop
inst_1 : DecidablePred p
hf : PrimrecPred p
⊢ Primrec (β := Option α) fun (p_1 : List α × α) ↦ if p p_1.2 then some p_1.2 else none

Tactic:
ite (hf.comp snd) (option_some_iff.mpr snd) (const none)

Premises used: Iff.mpr, Primrec.snd, PrimrecPred.comp, Primrec.const, Option.none, Primrec.option_some_iff, Primrec.ite
-- Module: Mathlib.Computability.Primrec.List
Goal:
α : Type u_1
inst : Primcodable α
p : α → Prop
inst_1 : DecidablePred p
hf : PrimrecPred p
⊢ Primrec (β := Option α) fun (p_1 : List α × α) ↦ if p p_1.2 then some p_1.2 else none

Tactic:
exact ite (hf.comp snd) (option_some_iff.mpr snd) (const none)

Premises used: Iff.mpr, Primrec.snd, PrimrecPred.comp, Primrec.const, Option.none, Primrec.option_some_iff, Primrec.ite
-- Module: Mathlib.Computability.Primrec.List
Goal:
α : Type u_1
β : Type u_2
inst : Primcodable α
inst_1 : Primcodable β
f : α → List β
p : α → β → Bool
hf : Primrec f
hp : Primrec₂ p
a : α
dsimp : List.foldr (fun (b : β) (s : ℕ) ↦ bif p a b then 0 else s + 1) 0 (f a) = List.findIdx (p a) (f a)
⊢ List.foldr (fun (b : β) (s : ℕ) ↦ bif p (a, b, s).1 (a, b, s).2.1 then 0 else (a, b, s).2.2.succ) 0 (f a) =
    List.findIdx (p a) (f a)

Tactic:
dsimp