mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Computability.Primrec.List

Goal state before:
pp: β : Type u_2
σ : Type u_4
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : β → σ
m : β → ℕ
l : β → List β
g : β → List σ → Option σ
hm : Primrec m
hl : Primrec l
hg : Primrec₂ g
Ord : ∀ (b b' : β), b' ∈ l b → m b' < m b
H : ∀ (b : β), g b (List.map f (l b)) = some (f b)
this✝ : DecidableEq β
mapGraph : List (β × σ) → List β → List σ := fun M bs ↦ List.flatMap (fun x ↦ (List.lookup x M).toList) bs
bindList : β → ℕ → List β := fun b n ↦ Nat.rec [b] (fun x bs ↦ List.flatMap l bs) n
graph : β → ℕ → List (β × σ) :=
  fun b i ↦
    Nat.rec []
      (fun i ih ↦
        List.filterMap (fun b' ↦ Option.map (fun x ↦ (b', x)) (g b' (mapGraph ih (l b')))) (bindList b (m b - i)))
      i
mapGraph_primrec : Primrec₂ mapGraph
bindList_primrec : Primrec₂ bindList
graph_primrec : Primrec₂ graph
this : Primrec fun b ↦ Option.map Prod.snd (graph b (m b + 1))[0]?
b : β
i : ℕ
hi : i ≤ m b + 1
⊢ graph b i = List.map (fun x ↦ (x, f x)) (bindList b (m b + 1 - i))

Tactic:
by

Goal state after:
Module: Mathlib.Computability.Partrec

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → β ⊕ γ
g : α → β → σ
h : α → γ → σ
hf : Computable f
hg : Computable₂ g
hh : Computable₂ h
a : α
⊢ (bif (encode (f a)).bodd then Option.map (h a) (decode (encode (f a)).div2)
    else Option.map (g a) (decode (encode (f a)).div2)) =
    Option.some (Sum.casesOn (f a) (g a) (h a))

Tactic:
by

Goal state after:
Module: Mathlib.Computability.Primrec.List

Goal state before:
pp: β : Type u_2
σ : Type u_4
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : β → σ
m : β → ℕ
l : β → List β
g : β → List σ → Option σ
hm : Primrec m
hl : Primrec l
hg : Primrec₂ g
Ord : ∀ (b b' : β), b' ∈ l b → m b' < m b
H : ∀ (b : β), g b (List.map f (l b)) = some (f b)
this✝ : DecidableEq β
mapGraph : List (β × σ) → List β → List σ := fun M bs ↦ List.flatMap (fun x ↦ (List.lookup x M).toList) bs
bindList : β → ℕ → List β := fun b n ↦ Nat.rec [b] (fun x bs ↦ List.flatMap l bs) n
graph : β → ℕ → List (β × σ) :=
  fun b i ↦
    Nat.rec []
      (fun i ih ↦
        List.filterMap (fun b' ↦ Option.map (fun x ↦ (b', x)) (g b' (mapGraph ih (l b')))) (bindList b (m b - i)))
      i
mapGraph_primrec : Primrec₂ mapGraph
bindList_primrec : Primrec₂ bindList
graph_primrec : Primrec₂ graph
this : Primrec fun b ↦ Option.map Prod.snd (graph b (m b + 1))[0]?
b : β
⊢ Option.map Prod.snd (graph b (m b + 1))[0]? = some (f b)

Tactic:
by

Goal state after:
Module: Mathlib.Computability.Primrec.List

Goal state before:
pp: β : Type u_2
σ : Type u_4
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : β → σ
m : β → ℕ
l : β → List β
g : β → List σ → Option σ
hm : Primrec m
hl : Primrec l
hg : Primrec₂ g
Ord : ∀ (b b' : β), b' ∈ l b → m b' < m b
H : ∀ (b : β), g b (List.map f (l b)) = some (f b)
⊢ Primrec f

Tactic:
by

Goal state after:
Module: Mathlib.Computability.Partrec

Goal state before:
pp: α : Type u_1
σ : Type u_4
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f : α → ℕ → σ
g : α → List σ → Option σ
hg : Computable₂ g
H : ∀ (a : α) (n : ℕ), g a (List.map (f a) (List.range n)) = Option.some (f a n)
a : α × ℕ
⊢ Nat.rec (Option.some [])
      (fun y IH ↦
        (a, y, IH).2.2.bind fun b ↦
          Option.map (fun b_1 ↦ (((a, y, IH), b), b_1).1.2 ++ [(((a, y, IH), b), b_1).2])
            (g ((a, y, IH), b).1.1.1 ((a, y, IH), b).2))
      a.2 =
    Option.some ((fun a n ↦ List.map (f a) (List.range n)) a.1 a.2)

Tactic:
by

Goal state after:
Module: Mathlib.Computability.Primrec.List

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_4
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α → β → σ
m : α → β → ℕ
l : α → β → List β
g : α → β × List σ → Option σ
hm : Primrec₂ m
hl : Primrec₂ l
hg : Primrec₂ g
Ord : ∀ (a : α) (b b' : β), b' ∈ l a b → m a b' < m a b
H : ∀ (a : α) (b : β), g a (b, List.map (f a) (l a b)) = some (f a b)
⊢ ∀ (b b' : α × β), b' ∈ List.map (fun b_1 ↦ (b.1, b_1)) (l b.1 b.2) → uncurry m b' < uncurry m b

Tactic:
by

Goal state after:
Module: Mathlib.Computability.Partrec

Goal state before:
pp: α : Type u_1
σ : Type u_4
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f : α → ℕ → σ
g : α → List σ → Option σ
hg : Computable₂ g
H : ∀ (a : α) (n : ℕ), g a (List.map (f a) (List.range n)) = Option.some (f a n)
this : Computable₂ fun a n ↦ List.map (f a) (List.range n)
a : α × ℕ
⊢ (fun a b ↦ (List.map (f (a, b).1) (List.range (a, b).2.succ))[(a, b).2]?) a.1 a.2 = Option.some (f a.1 a.2)

Tactic:
by

Goal state after:
Module: Mathlib.Computability.Partrec

Goal state before:
pp: α : Type u_1
σ : Type u_4
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
x✝¹ : Fin 0 → α → σ
x✝ : ∀ (i : Fin 0), Computable (x✝¹ i)
⊢ Computable fun a ↦ List.ofFn fun i ↦ x✝¹ i a

Tactic:
by

Goal state after:
Module: Mathlib.Computability.Partrec

Goal state before:
pp: α : Type u_1
σ : Type u_4
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
n : ℕ
f : Fin (n + 1) → α → σ
hf : ∀ (i : Fin (n + 1)), Computable (f i)
⊢ Computable fun a ↦ List.ofFn fun i ↦ f i a

Tactic:
by

Goal state after:
Module: Mathlib.Computability.Partrec

Goal state before:
pp: α : Type u_1
σ : Type u_4
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
n : ℕ
f : Fin n → α → σ
hf : ∀ (i : Fin n), Computable (f i)
a : α
⊢ (Vector.mOfFn fun i ↦ ↑(f i) a) = (↑fun a ↦ List.Vector.ofFn fun i ↦ f i a) a

Tactic:
by

Goal state after:
Module: Mathlib.Computability.Primrec.List

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_4
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α → β → σ
m : α → β → ℕ
l : α → β → List β
g : α → β × List σ → Option σ
hm : Primrec₂ m
hl : Primrec₂ l
hg : Primrec₂ g
Ord : ∀ (a : α) (b b' : β), b' ∈ l a b → m a b' < m a b
H : ∀ (a : α) (b : β), g a (b, List.map (f a) (l a b)) = some (f a b)
⊢ ∀ (b : α × β), g b.1 (b.2, List.map (uncurry f) (List.map (fun b_1 ↦ (b.1, b_1)) (l b.1 b.2))) = some (uncurry f b)

Tactic:
by

Goal state after:
Module: Mathlib.Computability.Partrec

Goal state before:
pp: α : Type u_1
σ : Type u_4
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f : α →. σ
h : Partrec fun a ↦ Part.map Option.some (f a)
n : ℕ
⊢ (do
      let n ← (↑(decode n)).bind fun a ↦ Part.map encode ((fun a ↦ Part.map Option.some (f a)) a)
      ↑n.ppred) =
    (↑(decode n)).bind fun a ↦ Part.map encode (f a)

Tactic:
by

Goal state after:
Module: Mathlib.Computability.Partrec

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_4
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
o : α → Option β
f : α → σ
g : α → β →. σ
ho : Computable o
hf : Computable f
hg : Partrec₂ g
this : Partrec fun a ↦ Nat.casesOn (encode (o a)) (Part.some (f a)) fun n ↦ (↑(decode n)).bind (g a)
a : α
⊢ (Nat.casesOn (encode (o a)) (Part.some (f a)) fun n ↦ (↑(decode n)).bind (g a)) =
    Option.casesOn (o a) (Part.some (f a)) (g a)

Tactic:
by

Goal state after:
Module: Mathlib.Computability.Primrec.List

Goal state before:
pp: α : Type u_1
inst✝ : Primcodable α
x✝ : ℕ × List α
n : ℕ
l : List α
⊢ (List.drop ((n, l).2.length - (n, l).1) (n, l).2.reverse).reverse = List.take (n, l).1 (n, l).2

Tactic:
by

Goal state after:
Module: Mathlib.Computability.Partrec

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → β ⊕ γ
g : α → β → σ
h : α → γ →. σ
hf : Computable f
hg : Computable₂ g
hh : Partrec₂ h
this :
  Partrec fun a ↦
    Option.casesOn (Sum.casesOn (f a) (fun x ↦ Option.none) Option.some)
      (Part.some (Sum.casesOn (f a) (fun b ↦ Option.some (g a b)) fun x ↦ Option.none)) fun c ↦
      Part.map Option.some (h a c)
a : α
⊢ (Option.casesOn (Sum.casesOn (f a) (fun x ↦ Option.none) Option.some)
      (Part.some (Sum.casesOn (f a) (fun b ↦ Option.some (g a b)) fun x ↦ Option.none)) fun c ↦
      Part.map Option.some (h a c)) =
    Part.map Option.some (Sum.casesOn (f a) (fun b ↦ Part.some (g a b)) (h a))

Tactic:
by

Goal state after:
Module: Mathlib.Computability.Primrec.List

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
g : β → α → α
hg : Primrec₂ g
l : List α
b : β
⊢ (List.casesOn (l, b).1 [] fun b_1 l_1 ↦ g ((l, b), b_1, l_1).1.2 ((l, b), b_1, l_1).2.1 :: ((l, b), b_1, l_1).2.2) =
    List.modifyHead (g b) l

Tactic:
by

Goal state after:
Module: Mathlib.Computability.Partrec

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → β ⊕ γ
g : α → β →. σ
h : α → γ → σ
hf : Computable f
hg : Partrec₂ g
hh : Computable₂ h
a : α
⊢ Sum.casesOn (Sum.casesOn (f a) (fun b ↦ Sum.inr (a, b).2) fun b ↦ Sum.inl (a, b).2) (fun b ↦ Part.some (h a b))
      (g a) =
    Sum.casesOn (f a) (g a) fun c ↦ Part.some (h a c)

Tactic:
by

Goal state after:
Module: Mathlib.Computability.Primrec.List

Goal state before:
pp: α : Type u_1
p : α → Prop
inst✝ : Primcodable α
w✝ : DecidablePred p
hf : Primrec fun a ↦ decide (p a)
⊢ ∀ (a : List α), ¬(filter (fun x ↦ decide (p x)) a).length = 0 ↔ ∃ a_1 ∈ a, p a_1

Tactic:
by

Goal state after:
Module: Mathlib.Computability.Primrec.List

Goal state before:
pp: α : Type u_1
p : α → Prop
inst✝ : Primcodable α
w✝ : DecidablePred p
hf : Primrec fun a ↦ decide (p a)
⊢ ∀ (a : List α), (filter (fun x ↦ decide (p x)) a).length = a.length ↔ ∀ a_1 ∈ a, p a_1

Tactic:
by

Goal state after:
Module: Mathlib.Computability.Primrec.List

Goal state before:
pp: p : ℕ → Prop
hf : PrimrecPred p
⊢ ∀ (a : ℕ), (∃ a_1 ∈ range a, p a_1) ↔ ∃ x < a, p x

Tactic:
by

Goal state after:
Module: Mathlib.Computability.Primrec.List

Goal state before:
pp: p : ℕ → Prop
hf : PrimrecPred p
⊢ ∀ (a : ℕ), (∀ a_1 ∈ range a, p a_1) ↔ ∀ x < a, p x

Tactic:
by

Goal state after:
Module: Mathlib.Computability.Primrec.List

Goal state before:
pp: R : ℕ → ℕ → Prop
s : ℕ
inst✝ : DecidableRel R
hf : PrimrecRel R
⊢ Primrec fun n ↦ filter (fun y ↦ decide (R y n)) (range s)

Tactic:
by

Goal state after:
Module: Mathlib.Computability.Primrec.List

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
R : α → β → Prop
inst✝² : Primcodable α
inst✝¹ : Primcodable β
hf : PrimrecRel R
inst✝ : DecidableRel R
⊢ Primrec fun p ↦ some p.2

Tactic:
· exact option_some.comp snd

Goal state after:
Module: Mathlib.Computability.Primrec.List

Goal state before:
pp: α : Type u_1
β : Type u_2
R : α → β → Prop
inst✝² : Primcodable α
inst✝¹ : Primcodable β
hf : PrimrecRel R
inst✝ : DecidableRel R
⊢ Primrec₂ fun L b ↦ filter (fun a ↦ decide (R a b)) L

Tactic:
by

Goal state after:
Module: Mathlib.Computability.Primrec.List

Goal state before:
pp: α : Type u_1
β : Type u_2
R : α → β → Prop
inst✝¹ : Primcodable α
inst✝ : Primcodable β
hf : PrimrecRel R
L : List α
b : β
⊢ (filter (fun x ↦ decide (R x b)) L).length ≠ 0 ↔ ∃ a ∈ L, R a b

Tactic:
by

Goal state after:
Module: Mathlib.Computability.Primrec.List

Goal state before:
pp: α : Type u_1
β : Type u_2
R : α → β → Prop
inst✝¹ : Primcodable α
inst✝ : Primcodable β
hf : PrimrecRel R
⊢ PrimrecRel fun L b ↦ ∃ a ∈ L, R a b

Tactic:
by

Goal state after:
Module: Mathlib.Computability.Primrec.List

Goal state before:
pp: α : Type u_1
β : Type u_2
R : α → β → Prop
inst✝¹ : Primcodable α
inst✝ : Primcodable β
hf : PrimrecRel R
L : List α
b : β
⊢ (filter (fun x ↦ decide (R x b)) L).length = L.length ↔ ∀ a ∈ L, R a b

Tactic:
by

Goal state after:
Module: Mathlib.Computability.Partrec

Goal state before:
pp: α : Type u_5
σ : Type u_6
f : α →. σ ⊕ α
a : α
b : σ
F : α → ℕ →. σ ⊕ α :=
  fun a n ↦ Nat.rec (Part.some (Sum.inr a)) (fun x IH ↦ IH.bind fun s ↦ Sum.casesOn s (fun x ↦ Part.some s) f) n
n : ℕ
h₂ : Sum.inl b ∈ F a n
_x : ∃ b', Sum.inl b' ∈ F a n
h₁ : ∀ {m : ℕ}, m < n → ∃ b, Sum.inr b ∈ F a m
⊢ ∀ (m : ℕ) (a' : α), Sum.inr a' ∈ F a m → b ∈ f.fix a' → b ∈ f.fix a

Tactic:
by

Goal state after:
Module: Mathlib.Computability.Primrec.List

Goal state before:
pp: α : Type u_1
β : Type u_2
R : α → β → Prop
inst✝¹ : Primcodable α
inst✝ : Primcodable β
hf : PrimrecRel R
⊢ PrimrecRel fun L b ↦ ∀ a ∈ L, R a b

Tactic:
by

Goal state after:
Module: Mathlib.Computability.Primrec.List

Goal state before:
pp: 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:
by

Goal state after:
Module: Mathlib.Computability.Primrec.List

Goal state before:
pp: 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:
by

Goal state after:
Module: Mathlib.Computability.Primrec.List

Goal state before:
pp: α : Type u_1
inst✝ : Primcodable α
n : ℕ
⊢ Primrec fun a ↦ (a.1 ::ᵥ a.2).toList

Tactic:
by

Goal state after:
Module: Mathlib.Computability.Primrec.List

Goal state before:
pp: α : Type u_1
inst✝ : Primcodable α
n : ℕ
x✝ : List.Vector α n
l : List α
h : l.length = n
⊢ (List.Vector.toList ⟨l, h⟩).tail = (List.Vector.tail ⟨l, h⟩).toList

Tactic:
by

Goal state after:
Module: Mathlib.Computability.Primrec.List

Goal state before:
pp: α : Type u_1
inst✝ : Primcodable α
n : ℕ
a : List.Vector α n × Fin n
⊢ a.1.toList[↑a.2]? = some (a.1.get a.2)

Tactic:
by

Goal state after:
Module: Mathlib.Computability.Primrec.List

Goal state before:
pp: α : Type u_1
σ : Type u_3
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
x✝¹ : Fin 0 → α → σ
x✝ : ∀ (i : Fin 0), Primrec (x✝¹ i)
⊢ Primrec fun a ↦ List.ofFn fun i ↦ x✝¹ i a

Tactic:
by

Goal state after:
Module: Mathlib.Computability.Primrec.List

Goal state before:
pp: α : Type u_1
σ : Type u_3
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
n : ℕ
f : Fin (n + 1) → α → σ
hf : ∀ (i : Fin (n + 1)), Primrec (f i)
⊢ Primrec fun a ↦ List.ofFn fun i ↦ f i a

Tactic:
by

Goal state after:
Module: Mathlib.Computability.Primrec.List

Goal state before:
pp: α : Type u_1
σ : Type u_3
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
n : ℕ
f : Fin n → α → σ
hf : ∀ (i : Fin n), Primrec (f i)
⊢ Primrec fun a ↦ (List.Vector.ofFn fun i ↦ f i a).toList

Tactic:
by

Goal state after:
Module: Mathlib.Computability.Primrec.List

Goal state before:
pp: σ : 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:
by

Goal state after:
Module: Mathlib.Computability.Primrec.List

Goal state before:
pp: α : Type u_1
σ : Type u_3
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
n : ℕ
f : Fin n → α → σ
h : ∀ (i : Fin n), Primrec (f i)
a : Fin n × α
⊢ (List.Vector.ofFn fun i ↦ f i a.2).get a.1 = f a.1 a.2

Tactic:
by

Goal state after:
Module: Mathlib.Computability.Primrec.List

Goal state before:
pp: α : Type u_1
σ : Type u_3
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
n : ℕ
f : α → Fin n → σ
h : Primrec₂ f
a : α
⊢ (List.Vector.ofFn fun i ↦ f a i).get = f a

Tactic:
by

Goal state after:
Module: Mathlib.Computability.Primrec.List

Goal state before:
pp: n : ℕ
f : List.Vector ℕ n → ℕ
pf : Primrec' f
⊢ Primrec f

Tactic:
by

Goal state after:
Module: Mathlib.Computability.Primrec.List

Goal state before:
pp: n : ℕ
v : List.Vector ℕ n.succ
⊢ v.get 0 = v.head

Tactic:
by

Goal state after:
Module: Mathlib.Computability.Primrec.List

Goal state before:
pp: n : ℕ
f : List.Vector ℕ n → ℕ
hf : Primrec' f
v : List.Vector ℕ (n + 1)
⊢ f (ofFn fun i ↦ v.get i.succ) = f v.tail

Tactic:
by

Goal state after:
Module: Mathlib.Computability.Primrec.List

Goal state before:
pp: n m : ℕ
f : List.Vector ℕ n → ℕ
g : List.Vector ℕ n → List.Vector ℕ m
hf : Primrec' f
hg : Vec g
i : Fin m.succ
⊢ Primrec' fun v ↦ ((fun v ↦ f v ::ᵥ g v) v).get 0

Tactic:
by

Goal state after:
Module: Mathlib.Computability.Primrec.List

Goal state before:
pp: n m : ℕ
f : List.Vector ℕ n → ℕ
g : List.Vector ℕ n → List.Vector ℕ m
hf : Primrec' f
hg : Vec g
i✝ : Fin m.succ
i : Fin m
⊢ Primrec' fun v ↦ ((fun v ↦ f v ::ᵥ g v) v).get i.succ

Tactic:
by

Goal state after:
Module: Mathlib.Computability.Primrec.List

Goal state before:
pp: 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 ↦ (g v).get i) = f (g v)

Tactic:
by

Goal state after:
Module: Mathlib.Computability.Primrec.List

Goal state before:
pp: f : ℕ → ℕ → ℕ
hf : Primrec' fun v ↦ f v.head v.tail.head
n : ℕ
g h : List.Vector ℕ n → ℕ
hg : Primrec' g
hh : Primrec' h
⊢ Primrec' fun v ↦ f (g v) (h v)

Tactic:
by

Goal state after:
Module: Mathlib.Computability.Primrec.List

Goal state before:
pp: n : ℕ
f g : List.Vector ℕ n → ℕ
h : List.Vector ℕ (n + 2) → ℕ
hf : Primrec' f
hg : Primrec' g
hh : Primrec' h
⊢ Primrec' fun v ↦ Nat.rec (g v) (fun y IH ↦ h (y ::ᵥ IH ::ᵥ v)) (f v)

Tactic:
by

Goal state after:
Module: Mathlib.Computability.Primrec.List

Goal state before:
pp: v : List.Vector ℕ (Nat.succ 0)
⊢ Nat.rec 0 (fun y IH ↦ (y ::ᵥ IH ::ᵥ v).head) v.head = v.head.pred

Tactic:
by

Goal state after:
Module: Mathlib.Computability.Partrec

Goal state before:
pp: α : Type u_5
σ : Type u_6
f : α →. σ ⊕ α
a : α
b : σ
F : α → ℕ →. σ ⊕ α :=
  fun a n ↦ Nat.rec (Part.some (Sum.inr a)) (fun x IH ↦ IH.bind fun s ↦ Sum.casesOn s (fun x ↦ Part.some s) f) n
h : b ∈ f.fix a
this :
  ∀ (a' : α),
    b ∈ f.fix a' → ∀ (k : ℕ), Sum.inr a' ∈ F a k → ∃ n, Sum.inl b ∈ F a n ∧ ∀ m < n, k ≤ m → ∃ a₂, Sum.inr a₂ ∈ F a m
⊢ Sum.inr a ∈ F a 0

Tactic:
by

Goal state after:
Module: Mathlib.Computability.Primrec.List

Goal state before:
pp: v : List.Vector ℕ (Nat.succ 0 + 1)
⊢ Nat.rec v.tail.head (fun y IH ↦ (y ::ᵥ IH ::ᵥ v.tail).tail.head.succ) v.head = v.head + v.tail.head

Tactic:
by

Goal state after:
Module: Mathlib.Computability.Primrec.List

Goal state before:
pp: ⊢ Primrec' fun v ↦ (fun a b ↦ b - a) v.head v.tail.head

Tactic:
by

Goal state after:
Module: Mathlib.Computability.Primrec.List

Goal state before:
pp: ⊢ Primrec' fun v ↦ v.head - v.tail.head

Tactic:
by

Goal state after:
Module: Mathlib.Computability.Partrec

Goal state before:
pp: α : Type u_5
σ : Type u_6
f : α →. σ ⊕ α
a : α
b : σ
F : α → ℕ →. σ ⊕ α :=
  fun a n ↦ Nat.rec (Part.some (Sum.inr a)) (fun x IH ↦ IH.bind fun s ↦ Sum.casesOn s (fun x ↦ Part.some s) f) n
h : b ∈ f.fix a
this :
  ∀ (a' : α),
    b ∈ f.fix a' → ∀ (k : ℕ), Sum.inr a' ∈ F a k → ∃ n, Sum.inl b ∈ F a n ∧ ∀ m < n, k ≤ m → ∃ a₂, Sum.inr a₂ ∈ F a m
⊢ ∃ n, ((∃ b', Sum.inl b' ∈ F a n) ∧ ∀ {m : ℕ}, m < n → ∃ b, Sum.inr b ∈ F a m) ∧ Sum.inl b ∈ F a n

Tactic:
by

Goal state after:
Module: Mathlib.Computability.Primrec.List

Goal state before:
pp: v : List.Vector ℕ (Nat.succ 0 + 1)
⊢ Nat.rec 0 (fun y IH ↦ (y ::ᵥ IH ::ᵥ v.tail).tail.tail.head + (y ::ᵥ IH ::ᵥ v.tail).tail.head) v.head =
    v.head * v.tail.head

Tactic:
by

Goal state after:
Module: Mathlib.Computability.Primrec.List

Goal state before:
pp: n : ℕ
a b f g : List.Vector ℕ n → ℕ
ha : Primrec' a
hb : Primrec' b
hf : Primrec' f
hg : Primrec' g
v : List.Vector ℕ n
⊢ Nat.rec (g v) (fun y IH ↦ f (y ::ᵥ IH ::ᵥ v).tail.tail) (b v - a v) = if a v < b v then f v else g v

Tactic:
by

Goal state after:
Module: Mathlib.Computability.Primrec.List

Goal state before:
pp: v : List.Vector ℕ 0
⊢ 0 = encode v

Tactic:
by

Goal state after:
Module: Mathlib.Computability.Primrec.List

Goal state before:
pp: H : ∀ (n : ℕ), n.sqrt = Nat.rec 0 (fun x y ↦ if x.succ < y.succ * y.succ then y else y.succ) n
v : List.Vector ℕ (1 + 2)
⊢ ℕ

Tactic:
by

Goal state after:
Module: Mathlib.Computability.Primrec.List

Goal state before:
pp: H : ∀ (n : ℕ), n.sqrt = Nat.rec 0 (fun x y ↦ if x.succ < y.succ * y.succ then y else y.succ) n
⊢ Primrec' fun v ↦ v.head.sqrt

Tactic:
by

Goal state after:
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: f : ℕ →. ℕ
hf : Nat.Partrec f
⊢ Partrec₂ fun a m ↦ Part.map (fun x ↦ x + m) (Nat.rfind fun n ↦ (fun m ↦ decide (m = 0)) <$> f (Nat.pair a (n + m)))

Tactic:
by

Goal state after:
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: x✝ : Code.const 0 = Code.const 0
⊢ 0 = 0

Tactic:
by

Goal state after:
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: n₁ n₂ : ℕ
h : Code.const (n₁ + 1) = Code.const (n₂ + 1)
⊢ n₁ + 1 = n₂ + 1

Tactic:
by

Goal state after:
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: n : ℕ
m : ℕ := n.div2.div2
⊢ m < n + 4

Tactic:
by

Goal state after:
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: ⊢ (ofNatCode 0).encodeCode = 0

Tactic:
by

Goal state after:
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: ⊢ (ofNatCode 1).encodeCode = 1

Tactic:
by

Goal state after:
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: ⊢ (ofNatCode 2).encodeCode = 2

Tactic:
by

Goal state after:
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: ⊢ (ofNatCode 3).encodeCode = 3

Tactic:
by

Goal state after:
Module: Mathlib.Computability.Primrec.List

Goal state before:
pp: ⊢ Primrec' fun v ↦ v.head.sqrt

Tactic:
by

Goal state after:
Module: Mathlib.Computability.Primrec.List

Goal state before:
pp: n : ℕ
f : List.Vector ℕ n → ℕ
hf : Primrec' f
⊢ Primrec' fun v ↦ (unpair (f v)).1

Tactic:
by

Goal state after:
Module: Mathlib.Computability.Primrec.List

Goal state before:
pp: n : ℕ
f : List.Vector ℕ n → ℕ
hf : Primrec' f
⊢ Primrec' fun v ↦ (unpair (f v)).2

Tactic:
by

Goal state after:
Module: Mathlib.Computability.Primrec.List

Goal state before:
pp: n : ℕ
f✝ : List.Vector ℕ n → ℕ
f : ℕ → ℕ
hf : Nat.Primrec f
⊢ Primrec' fun v ↦ f v.head

Tactic:
by

Goal state after:
Module: Mathlib.Computability.Primrec.List

Goal state before:
pp: n : ℕ
f : List.Vector ℕ n → ℕ
this : ∀ (f : ℕ → ℕ), Nat.Primrec f → Primrec' fun v ↦ f v.head
hf : Primrec f
i : List.Vector ℕ n
⊢ (encode (Option.map f (decode (encode i)))).pred = f i

Tactic:
by

Goal state after:
Module: Mathlib.Computability.Primrec.List

Goal state before:
pp: f : ℕ → ℕ
h : Primrec fun v ↦ f v.head
v : ℕ
⊢ f (ofFn fun i ↦ id v).head = f v

Tactic:
by

Goal state after:
Module: Mathlib.Computability.Primrec.List

Goal state before:
pp: f : ℕ → ℕ → ℕ
h : Primrec fun v ↦ f v.head v.tail.head
v : ℕ × ℕ
⊢ f (v.1 ::ᵥ v.2 ::ᵥ nil).head (v.1 ::ᵥ v.2 ::ᵥ nil).tail.head = f v.1 v.2

Tactic:
by

Goal state after:
Module: Mathlib.Computability.Primrec.List

Goal state before:
pp: m n : ℕ
f : List.Vector ℕ m → List.Vector ℕ n
h : Vec f
⊢ Primrec f

Tactic:
by

Goal state after:
Module: Mathlib.Computability.Ackermann

Goal state before:
pp: n : ℕ
⊢ ack 0 n = n + 1

Tactic:
by

Goal state after:
Module: Mathlib.Computability.Ackermann

Goal state before:
pp: m : ℕ
⊢ ack (m + 1) 0 = ack m 1

Tactic:
by

Goal state after:
Module: Mathlib.Computability.Ackermann

Goal state before:
pp: m n : ℕ
⊢ ack (m + 1) (n + 1) = ack m (ack (m + 1) n)

Tactic:
by

Goal state after:
Module: Mathlib.Computability.Ackermann

Goal state before:
pp: n : ℕ
⊢ ack 1 n = n + 2

Tactic:
by

Goal state after:
Module: Mathlib.Computability.Ackermann

Goal state before:
pp: n : ℕ
⊢ ack 2 n = 2 * n + 3

Tactic:
by

Goal state after:
Module: Mathlib.Computability.Ackermann

Goal state before:
pp: n : ℕ
IH : ack 3 n = 2 ^ (n + 3) - 3
⊢ 2 * 3 ≤ 2 * 2 ^ 3

Tactic:
by

Goal state after:
Module: Mathlib.Computability.Ackermann

Goal state before:
pp: n : ℕ
IH : ack 3 n = 2 ^ (n + 3) - 3
⊢ 2 * 2 ^ 3 ≤ 2 * 2 ^ (n + 3)

Tactic:
by

Goal state after:
Module: Mathlib.Computability.Ackermann

Goal state before:
pp: n : ℕ
⊢ ack 3 n = 2 ^ (n + 3) - 3

Tactic:
by

Goal state after:
Module: Mathlib.Computability.Ackermann

Goal state before:
pp: n : ℕ
⊢ 0 < ack 0 n

Tactic:
by

Goal state after:
Module: Mathlib.Computability.Partrec

Goal state before:
pp: α : Type u_5
σ : Type u_6
f : α →. σ ⊕ α
a : α
b : σ
F : α → ℕ →. σ ⊕ α :=
  fun a n ↦ Nat.rec (Part.some (Sum.inr a)) (fun x IH ↦ IH.bind fun s ↦ Sum.casesOn s (fun x ↦ Part.some s) f) n
h : b ∈ f.fix a
a₁ : α
h₁ : b ∈ f.fix a₁
a₂ : α
h₂ : b ∈ f.fix a₂
IH :
  ∀ (a'' : α),
    Sum.inr a'' ∈ f a₂ →
      ∀ (k : ℕ), Sum.inr a'' ∈ F a k → ∃ n, Sum.inl b ∈ F a n ∧ ∀ m < n, k ≤ m → ∃ a₂, Sum.inr a₂ ∈ F a m
k : ℕ
hk : Sum.inr a₂ ∈ F a k
a₃ : α
am₃ : Sum.inr a₃ ∈ f a₂
right✝ : b ∈ f.fix a₃
⊢ Sum.inr a₃ ∈ F a k.succ

Tactic:
by

Goal state after:
Module: Mathlib.Computability.Ackermann

Goal state before:
pp: m : ℕ
⊢ 0 < ack (m + 1) 0

Tactic:
by

Goal state after: