awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Computability.Primrec.List
Goal:
α : Type u_1
β : Type u_2
R : α → β → Prop
inst : Primcodable α
inst_1 : Primcodable β
hf : PrimrecRel R
have : ∀ (L : List α) (b : β), (filter (fun (x : α) ↦ decide (R x b)) L).length ≠ 0 ↔ ∃ a ∈ L, R a b
have₁ :
  ∀ (h : ∀ (L : List α) (b : β), (filter (fun (x : α) ↦ decide (R x b)) L).length ≠ 0 ↔ ∃ a ∈ L, R a b),
    PrimrecRel fun (L : List α) (b : β) ↦ ∃ a ∈ L, R a b
have₂ : ∀ (L : List α) (b : β), (filter (fun (x : α) ↦ decide (R x b)) L).length ≠ 0 ↔ ∃ a ∈ L, R a b
have₃ have₄ :
  ∀ (h : ∀ (L : List α) (b : β), (filter (fun (x : α) ↦ decide (R x b)) L).length ≠ 0 ↔ ∃ a ∈ L, R a b),
    PrimrecRel fun (L : List α) (b : β) ↦ ∃ a ∈ L, R a b
have₅ :
  ∀ (h : ∀ (L : List α) (b : β), (filter (fun (x : α) ↦ decide (R x b)) L).length ≠ 0 ↔ ∃ a ∈ L, R a b),
    PrimrecRel fun (a : List α) (b : β) ↦ (filter (fun (x : α) ↦ decide (R x b)) a).length = 0
⊢ PrimrecRel fun (L : List α) (b : β) ↦ ∃ a ∈ L, R a b

Tactic:
classical
  have h (L) (b) : (List.filter (R · b) L).length ≠ 0 ↔ ∃ a ∈ L, R a b := by simp
  refine .of_eq (.not ?_) h
  exact Primrec.eq.comp (list_length.comp hf.listFilter) (const 0)
-- Module: Mathlib.Computability.Primrec.List
Goal:
α : Type u_1
β : Type u_2
R : α → β → Prop
inst : Primcodable α
inst_1 : Primcodable β
hf : PrimrecRel R
L : List α
b : β
⊢ (filter (fun (x : α) ↦ decide (R x b)) L).length = L.length ↔ ∀ a ∈ L, R a b

Tactic:
simp
-- Module: Mathlib.Computability.Primrec.List
Goal:
α : Type u_1
β : Type u_2
R : α → β → Prop
inst : Primcodable α
inst_1 : Primcodable β
hf : PrimrecRel R
⊢ ∀ (L : List α) (b : β), (filter (fun (x : α) ↦ decide (R x b)) L).length = L.length ↔ ∀ a ∈ L, R a b

Tactic:
have h (L) (b) : (List.filter (R · b) L).length = L.length ↔ ∀ a ∈ L, R a b := by simp
-- Module: Mathlib.Computability.Primrec.List
Goal:
α : Type u_1
β : Type u_2
R : α → β → Prop
inst : Primcodable α
inst_1 : Primcodable β
hf : PrimrecRel R
h : ∀ (L : List α) (b : β), (filter (fun (x : α) ↦ decide (R x b)) L).length = L.length ↔ ∀ a ∈ L, R a b
apply : PrimrecRel fun (a : List α) (b : β) ↦ (filter (fun (x : α) ↦ decide (R x b)) a).length = a.length
⊢ PrimrecRel fun (L : List α) (b : β) ↦ ∀ a ∈ L, R a b

Tactic:
apply PrimrecRel.of_eq ?_ h

Premises used: PrimrecRel.of_eq
-- Module: Mathlib.Computability.Primrec.List
Goal:
α : Type u_1
β : Type u_2
R : α → β → Prop
inst : Primcodable α
inst_1 : Primcodable β
hf : PrimrecRel R
h : ∀ (L : List α) (b : β), (filter (fun (x : α) ↦ decide (R x b)) L).length = L.length ↔ ∀ a ∈ L, R a b
⊢ PrimrecRel fun (a : List α) (b : β) ↦ (filter (fun (x : α) ↦ decide (R x b)) a).length = a.length

Tactic:
(Primrec.eq.comp (list_length.comp <| PrimrecRel.listFilter hf) (.comp list_length fst))

Premises used: PrimrecRel, Primrec.list_length, PrimrecRel.listFilter, Primrec.fst, Primrec.eq, PrimrecRel.comp, Primrec.comp
-- Module: Mathlib.Computability.Primrec.List
Goal:
α : Type u_1
β : Type u_2
R : α → β → Prop
inst : Primcodable α
inst_1 : Primcodable β
hf : PrimrecRel R
h : ∀ (L : List α) (b : β), (filter (fun (x : α) ↦ decide (R x b)) L).length = L.length ↔ ∀ a ∈ L, R a b
⊢ PrimrecRel fun (a : List α) (b : β) ↦ (filter (fun (x : α) ↦ decide (R x b)) a).length = a.length

Tactic:
exact (Primrec.eq.comp (list_length.comp <| PrimrecRel.listFilter hf) (.comp list_length fst))

Premises used: Primrec.list_length, PrimrecRel.listFilter, Primrec.fst, Primrec.eq, PrimrecRel.comp, Primrec.comp
-- Module: Mathlib.Computability.Primrec.List
Goal:
α : Type u_1
β : Type u_2
R : α → β → Prop
inst : Primcodable α
inst_1 : Primcodable β
hf : PrimrecRel R
have : ∀ (L : List α) (b : β), (filter (fun (x : α) ↦ decide (R x b)) L).length = L.length ↔ ∀ a ∈ L, R a b
have₁ :
  ∀ (h : ∀ (L : List α) (b : β), (filter (fun (x : α) ↦ decide (R x b)) L).length = L.length ↔ ∀ a ∈ L, R a b),
    PrimrecRel fun (L : List α) (b : β) ↦ ∀ a ∈ L, R a b
have₂ : ∀ (L : List α) (b : β), (filter (fun (x : α) ↦ decide (R x b)) L).length = L.length ↔ ∀ a ∈ L, R a b
have₃ have₄ :
  ∀ (h : ∀ (L : List α) (b : β), (filter (fun (x : α) ↦ decide (R x b)) L).length = L.length ↔ ∀ a ∈ L, R a b),
    PrimrecRel fun (L : List α) (b : β) ↦ ∀ a ∈ L, R a b
have₅ :
  ∀ (h : ∀ (L : List α) (b : β), (filter (fun (x : α) ↦ decide (R x b)) L).length = L.length ↔ ∀ a ∈ L, R a b),
    PrimrecRel fun (a : List α) (b : β) ↦ (filter (fun (x : α) ↦ decide (R x b)) a).length = a.length
⊢ PrimrecRel fun (L : List α) (b : β) ↦ ∀ a ∈ L, R a b

Tactic:
classical
  have h (L) (b) : (List.filter (R · b) L).length = L.length ↔ ∀ a ∈ L, R a b := by simp
  apply PrimrecRel.of_eq ?_ h
  exact (Primrec.eq.comp (list_length.comp <| PrimrecRel.listFilter hf) (.comp list_length fst))
-- Module: Mathlib.Computability.Primrec.List
Goal:
R : ℕ → ℕ → Prop
hf : PrimrecRel R
⊢ ∀ (a : ℕ × ℕ), (∃ a_1 ∈ range a.1, R a_1 a.2) ↔ (fun (n y : ℕ) ↦ ∃ x < n, R x y) a.1 a.2

Tactic:
simp
-- Module: Mathlib.Computability.Primrec.List
Goal:
R : ℕ → ℕ → Prop
hf : PrimrecRel R
⊢ ∀ (a : ℕ × ℕ), (∀ a_1 ∈ range a.1, R a_1 a.2) ↔ (fun (n y : ℕ) ↦ ∀ x < n, R x y) a.1 a.2

Tactic:
simp
-- Module: Mathlib.Computability.Primrec.List
Goal:
α : Type u_1
inst : Primcodable α
n : ℕ
⊢ Primrec.{u_1, u_1} (α := List.Vector α n) List.Vector.toList

Tactic:
subtype_val (hp := (@Primrec.eq ℕ _).comp list_length (const _))

Premises used: List.Vector, Primrec.subtype_val, List.Vector.toList
-- Module: Mathlib.Computability.Primrec.List
Goal:
α : Type u_1
β : Type u_2
inst : Primcodable α
inst_1 : Primcodable β
n : ℕ
f : α → List.Vector β n
⊢ (Primrec.{u_1, u_2} (β := List β) fun (a : α) ↦ (f a).toList) ↔ Primrec f

Tactic:
subtype_val_iff (hp := (@Primrec.eq ℕ _).comp list_length (const _))

Premises used: Primrec.subtype_val_iff, List.Vector, List.Vector.toList
-- Module: Mathlib.Computability.Primrec.List
Goal:
α : Type u_1
inst : Primcodable α
n : ℕ
⊢ Primrec (β := List α) fun (a : α × List.Vector α n) ↦ (a.1 ::ᵥ a.2).toList

Tactic:
simpa using list_cons.comp fst (vector_toList_iff.2 snd)

Premises used: Iff.mpr, Primrec.vector_toList_iff, Primrec.snd, Primrec.fst, Primrec.list_cons, Primrec₂.comp
-- Module: Mathlib.Computability.Primrec.List
Goal:
α : Type u_1
inst : Primcodable α
n : ℕ
⊢ Primrec.{u_1, 0} (α := List.Vector α n) Vector.length

Tactic:
const _

Premises used: Primrec.const
-- Module: Mathlib.Computability.Primrec.List
Goal:
α : Type u_1
inst : Primcodable α
n : ℕ
⊢ Primrec.{u_1, u_1} (α := List.Vector α n.succ) List.Vector.head

Tactic:
option_some_iff.1 <| (list_head?.comp vector_toList).of_eq fun ⟨_ :: _, _⟩ => rfl

Premises used: List.head?, Primrec.of_eq, List.Vector.head, Option.some, _private.0.Primrec.vector_head.match_1, Primrec.vector_toList, Primrec.comp, Primrec.option_some_iff, Iff.mp, Primrec.list_head?, Eq, List.Vector.toList, rfl
-- Module: Mathlib.Computability.Primrec.List
Goal:
α : Type u_1
inst : Primcodable α
n : ℕ
x : List.Vector α n
l : List α
h : l.length = n
nil :
  ∀ (h : List.length.{u_1} (α := α) [] = n),
    Eq.{u_1 + 1} (α := List α)
      (List.tail (List.Vector.toList (n := n) (Subtype.mk (p := fun (l : List α) ↦ l.length = n) [] h)))
      (List.Vector.toList (n := n - 1) (List.Vector.tail (Subtype.mk (p := fun (l : List α) ↦ l.length = n) [] h)))
cons :
  ∀ (head : α) (tail : List α) (h : (head :: tail).length = n),
    (List.Vector.toList (n := n) (Subtype.mk (p := fun (l : List α) ↦ l.length = n) (head :: tail) h)).tail =
      List.Vector.toList (n := n - 1)
        (List.Vector.tail (Subtype.mk (p := fun (l : List α) ↦ l.length = n) (head :: tail) h))
⊢ (List.Vector.toList (n := n) (Subtype.mk (p := fun (l : List α) ↦ l.length = n) l h)).tail =
    List.Vector.toList (n := n - 1) (List.Vector.tail (Subtype.mk (p := fun (l : List α) ↦ l.length = n) l h))

Tactic:
cases l
-- Module: Mathlib.Computability.Primrec.List
Goal:
α : Type u_1
inst : Primcodable α
n : ℕ
x : List.Vector α n
h : List.length.{u_1} (α := α) [] = n
⊢ Eq.{u_1 + 1} (α := List α)
    (List.tail (List.Vector.toList (n := n) (Subtype.mk (p := fun (l : List α) ↦ l.length = n) [] h)))
    (List.Vector.toList (n := n - 1) (List.Vector.tail (Subtype.mk (p := fun (l : List α) ↦ l.length = n) [] h)))

Tactic:
rfl
-- Module: Mathlib.Computability.Primrec.List
Goal:
α : Type u_1
inst : Primcodable α
n : ℕ
x : List.Vector α n
head : α
tail : List α
h : (head :: tail).length = n
⊢ (List.Vector.toList (n := n) (Subtype.mk (p := fun (l : List α) ↦ l.length = n) (head :: tail) h)).tail =
    List.Vector.toList (n := n - 1)
      (List.Vector.tail (Subtype.mk (p := fun (l : List α) ↦ l.length = n) (head :: tail) h))

Tactic:
rfl
-- Module: Mathlib.Computability.Primrec.List
Goal:
α : Type u_1
inst : Primcodable α
n : ℕ
a : List.Vector α n × Fin n
⊢ getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) a.1.toList (↑a.2 : ℕ) = some (a.1.get a.2)

Tactic:
simp [Vector.get_eq_get_toList]

Premises used: List.Vector.get_eq_get_toList
-- Module: Mathlib.Computability.Primrec.List
Goal:
α : Type u_1
σ : Type u_3
inst : Primcodable α
inst_1 : Primcodable σ
x : Fin 0 → α → σ
h : ∀ (i : Fin 0), Primrec (x i)
⊢ Primrec.{u_1, u_3} (β := List σ) fun (a : α) ↦ []

Tactic:
const []

Premises used: Primrec.const, List.nil
-- Module: Mathlib.Computability.Primrec.List
Goal:
α : Type u_1
σ : Type u_3
inst : Primcodable α
inst_1 : Primcodable σ
x : Fin 0 → α → σ
h : ∀ (i : Fin 0), Primrec (x i)
⊢ Primrec.{u_1, u_3} (β := List σ) fun (a : α) ↦ []

Tactic:
exact const []

Premises used: Primrec.const, List.nil
-- Module: Mathlib.Computability.Primrec.List
Goal:
α : Type u_1
σ : Type u_3
inst : Primcodable α
inst_1 : Primcodable σ
n : ℕ
f : Fin (n + 1) → α → σ
hf : ∀ (i : Fin (n + 1)), Primrec (f i)
⊢ Primrec.{u_1, u_3} (β := List σ) fun (a : α) ↦ List.ofFn (n := n + 1) fun (i : Fin (n + 1)) ↦ f i a

Tactic:
simpa using list_cons.comp (hf 0) (list_ofFn fun i => hf i.succ)

Premises used: Fin.succ, Primrec.list_cons, Primrec₂.comp, OfNat.ofNat
-- Module: Mathlib.Computability.Primrec.List
Goal:
α : Type u_1
σ : Type u_3
inst : Primcodable α
inst_1 : Primcodable σ
n : ℕ
f : Fin n → α → σ
hf : ∀ (i : Fin n), Primrec (f i)
⊢ Primrec.{u_1, u_3} (β := List σ) fun (a : α) ↦ List.Vector.toList (n := n) (List.Vector.ofFn fun (i : Fin n) ↦ f i a)

Tactic:
simp [list_ofFn hf]

Premises used: Primrec.list_ofFn
-- Module: Mathlib.Computability.Primrec.List
Goal:
α : Type u_1
inst : Primcodable α
n : ℕ
⊢ Primrec.{u_1, u_1} (α := List.Vector α n) List.Vector.get

Tactic:
of_equiv_symm

Premises used: List.Vector.get, Primrec.of_equiv_symm
-- Module: Mathlib.Computability.Primrec.List
Goal:
α : Type u_1
inst : Primcodable α
n : ℕ
⊢ Primrec.{u_1, u_1} (α := Fin n → α) List.Vector.ofFn

Tactic:
of_equiv

Premises used: Primrec.of_equiv
-- Module: Mathlib.Computability.Primrec.List
Goal:
σ : Type u_3
inst : Primcodable σ
n : ℕ
x : (Fin n → σ) × Fin n
v : Fin n → σ
i : Fin n
⊢ (List.Vector.ofFn (v, i).1).get (v, i).2 = id (v, i).1 (v, i).2

Tactic:
simp
-- Module: Mathlib.Computability.Primrec.List
Goal:
α : Type u_1
σ : Type u_3
inst : Primcodable α
inst_1 : Primcodable σ
n : ℕ
f : Fin n → α → σ
h : ∀ (i : Fin n), Primrec (f i)
a : Fin n × α
⊢ List.Vector.get (List.Vector.ofFn fun (i : Fin n) ↦ f i a.2) a.1 = f a.1 a.2

Tactic:
simp
-- Module: Mathlib.Computability.Primrec.List
Goal:
α : Type u_1
σ : Type u_3
inst : Primcodable α
inst_1 : Primcodable σ
n : ℕ
f : α → Fin n → σ
h : Primrec₂ f
a : α
h₁ : ∀ (i : Fin n), List.Vector.get (List.Vector.ofFn fun (i : Fin n) ↦ f a i) i = f a i
⊢ List.Vector.get (List.Vector.ofFn fun (i : Fin n) ↦ f a i) = f a

Tactic:
funext i
-- Module: Mathlib.Computability.Primrec.List
Goal:
α : Type u_1
σ : Type u_3
inst : Primcodable α
inst_1 : Primcodable σ
n : ℕ
f : α → Fin n → σ
h : Primrec₂ f
a : α
i : Fin n
⊢ List.Vector.get (List.Vector.ofFn fun (i : Fin n) ↦ f a i) i = f a i

Tactic:
simp
-- Module: Mathlib.Computability.Primrec.List
Goal:
n : ℕ
f : List.Vector ℕ n → ℕ
⊢ Primrec (β := ℕ) fun (x : List.Vector ℕ 0) ↦ 0

Tactic:
.const 0

Premises used: Primrec.const, OfNat.ofNat
-- Module: Mathlib.Computability.Primrec.List
Goal:
n : ℕ
f : List.Vector ℕ n → ℕ
⊢ Primrec (β := ℕ) fun (x : List.Vector ℕ 0) ↦ 0

Tactic:
exact .const 0
-- Module: Mathlib.Computability.Primrec.List
Goal:
n : ℕ
f : List.Vector ℕ n → ℕ
⊢ Primrec (β := ℕ) fun (v : List.Vector ℕ 1) ↦ v.head.succ

Tactic:
_root_.Primrec.succ.comp .vector_head

Premises used: Primrec.succ, Primrec.comp, Primrec.vector_head
-- Module: Mathlib.Computability.Primrec.List
Goal:
n : ℕ
f : List.Vector ℕ n → ℕ
⊢ Primrec (β := ℕ) fun (v : List.Vector ℕ 1) ↦ v.head.succ

Tactic:
exact _root_.Primrec.succ.comp .vector_head

Premises used: Primrec.succ, Primrec.comp, Primrec.vector_head
-- Module: Mathlib.Computability.Primrec.List
Goal:
n : ℕ
f : List.Vector ℕ n → ℕ
n_1 : ℕ
i : Fin n_1
⊢ Primrec (β := ℕ) fun (v : List.Vector ℕ n_1) ↦ v.get i

Tactic:
Primrec.vector_get.comp .id (.const i)

Premises used: Primrec.const, Primrec.vector_get, Primrec₂.comp, Primrec.id
-- Module: Mathlib.Computability.Primrec.List
Goal:
n : ℕ
f : List.Vector ℕ n → ℕ
n_1 : ℕ
i : Fin n_1
⊢ Primrec (β := ℕ) fun (v : List.Vector ℕ n_1) ↦ v.get i

Tactic:
exact Primrec.vector_get.comp .id (.const i)

Premises used: Primrec.const, Primrec.vector_get, Primrec₂.comp, Primrec.id
-- Module: Mathlib.Computability.Primrec.List
Goal:
n : ℕ
f : List.Vector ℕ n → ℕ
m n_1 : ℕ
f_1 : List.Vector ℕ n_1 → ℕ
g : Fin n_1 → List.Vector ℕ m → ℕ
h : Primrec' f_1
h_1 : ∀ (i : Fin n_1), Primrec' (g i)
hf : Primrec f_1
hg : ∀ (i : Fin n_1), Primrec (g i)
⊢ Primrec (β := ℕ) fun (a : List.Vector ℕ m) ↦ f_1 (ofFn fun (i : Fin n_1) ↦ g i a)

Tactic:
hf.comp (.vector_ofFn fun i => hg i)

Premises used: Primrec.vector_ofFn, Primrec.comp
-- Module: Mathlib.Computability.Primrec.List
Goal:
n : ℕ
f : List.Vector ℕ n → ℕ
m n_1 : ℕ
f_1 : List.Vector ℕ n_1 → ℕ
g : Fin n_1 → List.Vector ℕ m → ℕ
h : Primrec' f_1
h_1 : ∀ (i : Fin n_1), Primrec' (g i)
hf : Primrec f_1
hg : ∀ (i : Fin n_1), Primrec (g i)
⊢ Primrec (β := ℕ) fun (a : List.Vector ℕ m) ↦ f_1 (ofFn fun (i : Fin n_1) ↦ g i a)

Tactic:
exact hf.comp (.vector_ofFn fun i => hg i)

Premises used: Primrec.vector_ofFn, Primrec.comp
-- Module: Mathlib.Computability.Primrec.List
Goal:
n_1 : ℕ
f_1 : List.Vector ℕ n_1 → ℕ
n : ℕ
f : List.Vector ℕ n → ℕ
g : List.Vector ℕ (n + 2) → ℕ
h : Primrec' f
h_1 : Primrec' g
hf : Primrec f
hg : Primrec g
⊢ Primrec (β := ℕ) fun (v : List.Vector ℕ (n + 1)) ↦
    Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (f v.tail) (fun (y IH : ℕ) ↦ g (y ::ᵥ IH ::ᵥ v.tail)) v.head

Tactic:
.nat_rec' .vector_head (hf.comp Primrec.vector_tail)
        (hg.comp <|
          Primrec.vector_cons.comp (Primrec.fst.comp .snd) <|
          Primrec.vector_cons.comp (Primrec.snd.comp .snd) <|
            (@Primrec.vector_tail _ _ (n + 1)).comp .fst).to₂

Premises used: Primrec.snd, Primrec.fst, Primrec.vector_tail, Primrec.nat_rec', Primrec.vector_cons, Primrec.comp, Primrec₂.comp, Primrec.to₂, Primrec.vector_head
-- Module: Mathlib.Computability.Primrec.List
Goal:
n_1 : ℕ
f_1 : List.Vector ℕ n_1 → ℕ
n : ℕ
f : List.Vector ℕ n → ℕ
g : List.Vector ℕ (n + 2) → ℕ
h : Primrec' f
h_1 : Primrec' g
hf : Primrec f
hg : Primrec g
⊢ Primrec (β := ℕ) fun (v : List.Vector ℕ (n + 1)) ↦
    Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (f v.tail) (fun (y IH : ℕ) ↦ g (y ::ᵥ IH ::ᵥ v.tail)) v.head

Tactic:
exact
      .nat_rec' .vector_head (hf.comp Primrec.vector_tail)
        (hg.comp <|
          Primrec.vector_cons.comp (Primrec.fst.comp .snd) <|
          Primrec.vector_cons.comp (Primrec.snd.comp .snd) <|
            (@Primrec.vector_tail _ _ (n + 1)).comp .fst).to₂
-- Module: Mathlib.Computability.Primrec.List
Goal:
n : ℕ
f : List.Vector ℕ n → ℕ
pf : Primrec' f
zero : Primrec (β := ℕ) fun (x : List.Vector ℕ 0) ↦ 0
succ : Primrec (β := ℕ) fun (v : List.Vector ℕ 1) ↦ v.head.succ
get : ∀ {n : ℕ} (i : Fin n), Primrec (β := ℕ) fun (v : List.Vector ℕ n) ↦ v.get i
comp :
  ∀ {m n : ℕ} {f : List.Vector ℕ n → ℕ} (g : Fin n → List.Vector ℕ m → ℕ),
    Primrec' f →
      (∀ (i : Fin n), Primrec' (g i)) →
        ∀ (hf : Primrec f) (hg : ∀ (i : Fin n), Primrec (g i)),
          Primrec (β := ℕ) fun (a : List.Vector ℕ m) ↦ f (ofFn fun (i : Fin n) ↦ g i a)
prec :
  ∀ {n : ℕ} {f : List.Vector ℕ n → ℕ} {g : List.Vector ℕ (n + 2) → ℕ},
    Primrec' f →
      Primrec' g →
        ∀ (hf : Primrec f) (hg : Primrec g),
          Primrec (β := ℕ) fun (v : List.Vector ℕ (n + 1)) ↦
            Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (f v.tail) (fun (y IH : ℕ) ↦ g (y ::ᵥ IH ::ᵥ v.tail)) v.head
⊢ Primrec f

Tactic:
induction pf with
  | zero => exact .const 0
  | succ => exact _root_.Primrec.succ.comp .vector_head
  | get i => exact Primrec.vector_get.comp .id (.const i)
  | comp _ _ _ hf hg => exact hf.comp (.vector_ofFn fun i => hg i)
  | @prec n f g _ _ hf hg =>
    exact
      .nat_rec' .vector_head (hf.comp Primrec.vector_tail)
        (hg.comp <|
          Primrec.vector_cons.comp (Primrec.fst.comp .snd) <|
          Primrec.vector_cons.comp (Primrec.snd.comp .snd) <|
            (@Primrec.vector_tail _ _ (n + 1)).comp .fst).to₂

Premises used: Nat.Primrec'.succ, Nat.Primrec'.get, Nat.Primrec'.prec, Primrec.succ, Primrec.comp, Nat.Primrec'.zero, Nat.Primrec'.comp, Primrec.vector_head
-- Module: Mathlib.Computability.Primrec.List
Goal:
n : ℕ
f g : List.Vector ℕ n → ℕ
hf : Primrec' f
H : ∀ (i : List.Vector ℕ n), f i = g i
⊢ Primrec' g

Tactic:
(funext H : f = g) ▸ hf

Premises used: Eq.rec, funext
-- Module: Mathlib.Computability.Primrec.List
Goal:
n : ℕ
v : List.Vector ℕ n.succ
⊢ v.get 0 = v.head

Tactic:
simp [get_zero]

Premises used: List.Vector.get_zero
-- Module: Mathlib.Computability.Primrec.List
Goal:
n : ℕ
f : List.Vector ℕ n → ℕ
hf : Primrec' f
v : List.Vector ℕ (n + 1)
rw : f (ofFn fun (i : Fin n) ↦ v.get i.succ) = f (ofFn v.tail.get)
⊢ f (ofFn fun (i : Fin n) ↦ v.get i.succ) = f v.tail

Tactic:
rw [← ofFn_get v.tail]

Premises used: List.Vector.ofFn_get, List.Vector.tail
-- Module: Mathlib.Computability.Primrec.List
Goal:
n : ℕ
f : List.Vector ℕ n → ℕ
hf : Primrec' f
v : List.Vector ℕ (n + 1)
e_a : (fun (i : Fin n) ↦ v.get i.succ) = v.tail.get
⊢ f (ofFn fun (i : Fin n) ↦ v.get i.succ) = f (ofFn v.tail.get)

Tactic:
congr
-- Module: Mathlib.Computability.Primrec.List
Goal:
n : ℕ
f : List.Vector ℕ n → ℕ
hf : Primrec' f
v : List.Vector ℕ (n + 1)
e_a : ∀ (i : Fin n), v.get i.succ = v.tail.get i
⊢ (fun (i : Fin n) ↦ v.get i.succ) = v.tail.get

Tactic:
funext i
-- Module: Mathlib.Computability.Primrec.List
Goal:
n : ℕ
f : List.Vector ℕ n → ℕ
hf : Primrec' f
v : List.Vector ℕ (n + 1)
i : Fin n
⊢ v.get i.succ = v.tail.get i

Tactic:
simp
-- Module: Mathlib.Computability.Primrec.List
Goal:
n : ℕ
⊢ Vec (n := n) (m := 0) fun (x : List.Vector ℕ n) ↦ nil

Tactic:
fun i => i.elim0

Premises used: Nat.Primrec'.Vec, Fin.elim0
-- Module: Mathlib.Computability.Primrec.List
Goal:
n m : ℕ
f : List.Vector ℕ n → ℕ
g : List.Vector ℕ n → List.Vector ℕ m
hf : Primrec' f
hg : Vec g
i : Fin m.succ
⊢ Primrec' (n := n) fun (v : List.Vector ℕ n) ↦
    List.Vector.get (n := m.succ) ((fun (v : List.Vector ℕ n) ↦ f v ::ᵥ g v) v) 0

Tactic:
simp [*]
-- Module: Mathlib.Computability.Primrec.List
Goal:
n m : ℕ
f : List.Vector ℕ n → ℕ
g : List.Vector ℕ n → List.Vector ℕ m
hf : Primrec' f
hg : Vec g
i_1 : Fin m.succ
i : Fin m
⊢ Primrec' (n := n) fun (v : List.Vector ℕ n) ↦ List.Vector.get ((fun (v : List.Vector ℕ n) ↦ f v ::ᵥ g v) v) i.succ

Tactic:
simp [hg i]
-- Module: Mathlib.Computability.Primrec.List
Goal:
n : ℕ
⊢ Vec (n := n) id

Tactic:
get

Premises used: Nat.Primrec'.Vec, Nat.Primrec'.get
-- Module: Mathlib.Computability.Primrec.List
Goal:
n m : ℕ
f : List.Vector ℕ m → ℕ
g : List.Vector ℕ n → List.Vector ℕ m
hf : Primrec' f
hg : Vec g
v : List.Vector ℕ n
⊢ f (ofFn fun (i : Fin m) ↦ (g v).get i) = f (g v)

Tactic:
simp
-- Module: Mathlib.Computability.Primrec.List
Goal:
f : ℕ → ℕ
hf : Primrec' (n := 1) fun (v : List.Vector ℕ 1) ↦ f v.head
n : ℕ
g : List.Vector ℕ n → ℕ
hg : Primrec' g
⊢ Primrec' (n := n) fun (v : List.Vector ℕ n) ↦ f (g v)

Tactic:
hf.comp _ fun _ => hg

Premises used: List.Vector.head, Nat.Primrec'.comp
-- Module: Mathlib.Computability.Primrec.List
Goal:
f : ℕ → ℕ → ℕ
hf : Primrec' (n := 2) fun (v : List.Vector ℕ 2) ↦ f v.head v.tail.head
n : ℕ
g h : List.Vector ℕ n → ℕ
hg : Primrec' g
hh : Primrec' h
⊢ Primrec' (n := n) fun (v : List.Vector ℕ n) ↦ f (g v) (h v)

Tactic:
simpa using hf.comp' (hg.cons <| hh.cons Primrec'.nil)

Premises used: Nat.Primrec'.comp', Nat.Primrec'.cons, Nat.Primrec'.nil
-- Module: Mathlib.Computability.Primrec.List
Goal:
n : ℕ
f g : List.Vector ℕ n → ℕ
h : List.Vector ℕ (n + 2) → ℕ
hf : Primrec' f
hg : Primrec' g
hh : Primrec' h
⊢ Primrec' (n := n) fun (v : List.Vector ℕ n) ↦
    Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (g v) (fun (y IH : ℕ) ↦ h (y ::ᵥ IH ::ᵥ v)) (f v)

Tactic:
simpa using comp' (prec hg hh) (hf.cons idv)

Premises used: Nat.Primrec'.comp', Nat.Primrec'.idv, Nat.Primrec'.cons, Nat.Primrec'.prec
-- Module: Mathlib.Computability.Primrec.List
Goal:
v : List.Vector ℕ (Nat.succ 0)
simp : Nat.rec (motive := fun (x : ℕ) ↦ ℕ) 0 (fun (y IH : ℕ) ↦ y) v.head = v.head - 1
⊢ Nat.rec (motive := fun (x : ℕ) ↦ ℕ) 0 (fun (y IH : ℕ) ↦ (y ::ᵥ IH ::ᵥ v).head) v.head = v.head.pred

Tactic:
simp
-- Module: Mathlib.Computability.Primrec.List
Goal:
v : List.Vector ℕ (Nat.succ 0)
zero : Nat.rec (motive := fun (x : ℕ) ↦ ℕ) 0 (fun (y IH : ℕ) ↦ y) 0 = HSub.hSub (α := ℕ) 0 1
succ : ∀ (n : ℕ), Nat.rec (motive := fun (x : ℕ) ↦ ℕ) 0 (fun (y IH : ℕ) ↦ y) (n + 1) = n + 1 - 1
⊢ Nat.rec (motive := fun (x : ℕ) ↦ ℕ) 0 (fun (y IH : ℕ) ↦ y) v.head = v.head - 1

Tactic:
cases v.head

Premises used: List.Vector.head
-- Module: Mathlib.Computability.Primrec.List
Goal:
v : List.Vector ℕ (Nat.succ 0)
⊢ Nat.rec (motive := fun (x : ℕ) ↦ ℕ) 0 (fun (y IH : ℕ) ↦ y) 0 = HSub.hSub (α := ℕ) 0 1

Tactic:
rfl
-- Module: Mathlib.Computability.Primrec.List
Goal:
v : List.Vector ℕ (Nat.succ 0)
n : ℕ
⊢ Nat.rec (motive := fun (x : ℕ) ↦ ℕ) 0 (fun (y IH : ℕ) ↦ y) (n + 1) = n + 1 - 1

Tactic:
rfl
-- Module: Mathlib.Computability.Primrec.List
Goal:
v : List.Vector ℕ (Nat.succ 0 + 1)
simp : Nat.rec (motive := fun (x : ℕ) ↦ ℕ) v.tail.head (fun (y IH : ℕ) ↦ IH + 1) v.head = v.head + v.tail.head
⊢ Nat.rec (motive := fun (x : ℕ) ↦ ℕ) v.tail.head (fun (y IH : ℕ) ↦ (y ::ᵥ IH ::ᵥ v.tail).tail.head.succ) v.head =
    v.head + v.tail.head

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

Tactic:
induction v.head

Premises used: List.Vector.head
-- Module: Mathlib.Computability.Primrec.List
Goal:
v : List.Vector ℕ (Nat.succ 0 + 1)
⊢ Nat.rec (motive := fun (x : ℕ) ↦ ℕ) v.tail.head (fun (y IH : ℕ) ↦ IH + 1) 0 = 0 + v.tail.head

Tactic:
simp [*, Nat.succ_add]

Premises used: Nat.succ_add
-- Module: Mathlib.Computability.Primrec.List
Goal:
v : List.Vector ℕ (Nat.succ 0 + 1)
n : ℕ
h : Nat.rec (motive := fun (x : ℕ) ↦ ℕ) v.tail.head (fun (y IH : ℕ) ↦ IH + 1) n = n + v.tail.head
⊢ Nat.rec (motive := fun (x : ℕ) ↦ ℕ) v.tail.head (fun (y IH : ℕ) ↦ IH + 1) (n + 1) = n + 1 + v.tail.head

Tactic:
simp [*, Nat.succ_add]

Premises used: Nat.succ_add
-- Module: Mathlib.Computability.Primrec.List
Goal:
⊢ Primrec' (n := 2) fun (v : List.Vector ℕ 2) ↦ (fun (a b : ℕ) ↦ b - a) v.head v.tail.head

Tactic:
(prec head (pred.comp₁ _ (tail head))).of_eq fun v => ?_

Premises used: Nat.Primrec'.comp₁, Nat.Primrec'.pred, Nat.Primrec'.head, Nat.Primrec'.prec, Nat.Primrec'.tail, Nat.Primrec'.of_eq
-- Module: Mathlib.Computability.Primrec.List
Goal:
refine :
  ∀ (v : List.Vector ℕ (Nat.succ 0 + 1)),
    Eq (α := ℕ)
      (Nat.rec (motive := fun (x : ℕ) ↦ ℕ) v.tail.head (fun (y IH : ℕ) ↦ (y ::ᵥ IH ::ᵥ v.tail).tail.head.pred) v.head :
        ℕ)
      ((fun (a b : ℕ) ↦ b - a) v.head v.tail.head : ℕ)
⊢ Primrec' (n := 2) fun (v : List.Vector ℕ 2) ↦ (fun (a b : ℕ) ↦ b - a) v.head v.tail.head

Tactic:
refine (prec head (pred.comp₁ _ (tail head))).of_eq fun v => ?_

Premises used: Nat.Primrec'.comp₁, Nat.Primrec'.pred, Nat.Primrec'.head, Nat.Primrec'.prec, Nat.Primrec'.tail, Nat.Primrec'.of_eq