awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : α
nil : List.foldr (fun (b : β) (s : ℕ) ↦ bif p a b then 0 else s + 1) 0 [] = List.findIdx (p a) []
cons :
  ∀ (head : β) (tail : List β),
    List.foldr (fun (b : β) (s : ℕ) ↦ bif p a b then 0 else s + 1) 0 tail = List.findIdx (p a) tail →
      List.foldr (fun (b : β) (s : ℕ) ↦ bif p a b then 0 else s + 1) 0 (head :: tail) =
        List.findIdx (p a) (head :: tail)
⊢ List.foldr (fun (b : β) (s : ℕ) ↦ bif p a b then 0 else s + 1) 0 (f a) = List.findIdx (p a) (f a)

Tactic:
induction f a
-- 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 : α
⊢ List.foldr (fun (b : β) (s : ℕ) ↦ bif p a b then 0 else s + 1) 0 [] = List.findIdx (p a) []

Tactic:
simp [List.findIdx_cons, *]

Premises used: List.findIdx_cons
-- 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 : α
head : β
tail : List β
tail_ih : List.foldr (fun (b : β) (s : ℕ) ↦ bif p a b then 0 else s + 1) 0 tail = List.findIdx (p a) tail
⊢ List.foldr (fun (b : β) (s : ℕ) ↦ bif p a b then 0 else s + 1) 0 (head :: tail) = List.findIdx (p a) (head :: tail)

Tactic:
simp [List.findIdx_cons, *]

Premises used: List.findIdx_cons
-- Module: Mathlib.Computability.Primrec.List
Goal:
α : Type u_1
inst : Primcodable α
inst_1 : DecidableEq α
⊢ Primrec₂.{u_1, u_1, 0} (α := α) List.idxOf

Tactic:
to₂ <| list_findIdx snd <| Primrec.beq.comp₂ snd.to₂ (fst.comp fst).to₂

Premises used: Primrec.snd, Primrec.beq, Primrec.fst, Primrec.comp, Primrec₂.comp₂, List.idxOf, Primrec.to₂, Primrec.list_findIdx
-- Module: Mathlib.Computability.Primrec.List
Goal:
α : Type u_1
σ : Type u_4
inst : Primcodable α
inst_1 : Primcodable σ
f : α → ℕ → σ
g : α → List σ → Option σ
hg : Primrec₂ g
H : ∀ (a : α) (n : ℕ), g a (List.map (f a) (List.range n)) = some (f a n)
a : α
⊢ Nat.rec (motive := fun (x : ℕ) ↦ Option (List σ)) (some [])
      (fun (n : ℕ) (IH : (fun (x : ℕ) ↦ Option.{u_4} (List σ)) n) ↦
        (a, n, IH).2.2.bind fun (b : List σ) ↦
          Option.map (fun (b_1 : σ) ↦ (((a, n, IH), b), b_1).1.2 ++ [(((a, n, IH), b), b_1).2])
            (g ((a, n, IH), b).1.1 ((a, n, IH), b).2))
      0 =
    some (List.map (f a) (List.range 0))

Tactic:
rfl
-- Module: Mathlib.Computability.Primrec.List
Goal:
α : Type u_1
σ : Type u_4
inst : Primcodable α
inst_1 : Primcodable σ
f : α → ℕ → σ
g : α → List σ → Option σ
hg : Primrec₂ g
H : ∀ (a : α) (n : ℕ), g a (List.map (f a) (List.range n)) = some (f a n)
a : α
n : ℕ
IH :
  Nat.rec (motive := fun (x : ℕ) ↦ Option (List σ)) (some [])
      (fun (n : ℕ) (IH : (fun (x : ℕ) ↦ Option.{u_4} (List σ)) n) ↦
        (a, n, IH).2.2.bind fun (b : List σ) ↦
          Option.map (fun (b_1 : σ) ↦ (((a, n, IH), b), b_1).1.2 ++ [(((a, n, IH), b), b_1).2])
            (g ((a, n, IH), b).1.1 ((a, n, IH), b).2))
      n =
    some (List.map (f a) (List.range n))
⊢ Nat.rec (motive := fun (x : ℕ) ↦ Option (List σ)) (some [])
      (fun (n : ℕ) (IH : (fun (x : ℕ) ↦ Option.{u_4} (List σ)) n) ↦
        (a, n, IH).2.2.bind fun (b : List σ) ↦
          Option.map (fun (b_1 : σ) ↦ (((a, n, IH), b), b_1).1.2 ++ [(((a, n, IH), b), b_1).2])
            (g ((a, n, IH), b).1.1 ((a, n, IH), b).2))
      (n + 1) =
    some (List.map (f a) (List.range (n + 1)))

Tactic:
simp [IH, H, List.range_succ]

Premises used: List.range_succ
-- Module: Mathlib.Computability.Primrec.List
Goal:
α : Type u_1
σ : Type u_4
inst : Primcodable α
inst_1 : Primcodable σ
f : α → ℕ → σ
g : α → List σ → Option σ
hg : Primrec₂ g
H : ∀ (a : α) (n : ℕ), g a (List.map (f a) (List.range n)) = some (f a n)
a : α
n : ℕ
zero :
  Nat.rec (motive := fun (x : ℕ) ↦ Option (List σ)) (some [])
      (fun (n : ℕ) (IH : (fun (x : ℕ) ↦ Option.{u_4} (List σ)) n) ↦
        (a, n, IH).2.2.bind fun (b : List σ) ↦
          Option.map (fun (b_1 : σ) ↦ (((a, n, IH), b), b_1).1.2 ++ [(((a, n, IH), b), b_1).2])
            (g ((a, n, IH), b).1.1 ((a, n, IH), b).2))
      0 =
    some (List.map (f a) (List.range 0))
succ :
  ∀ (n : ℕ)
    (IH :
      Nat.rec (motive := fun (x : ℕ) ↦ Option (List σ)) (some [])
          (fun (n : ℕ) (IH : (fun (x : ℕ) ↦ Option.{u_4} (List σ)) n) ↦
            (a, n, IH).2.2.bind fun (b : List σ) ↦
              Option.map (fun (b_1 : σ) ↦ (((a, n, IH), b), b_1).1.2 ++ [(((a, n, IH), b), b_1).2])
                (g ((a, n, IH), b).1.1 ((a, n, IH), b).2))
          n =
        some (List.map (f a) (List.range n))),
    Nat.rec (motive := fun (x : ℕ) ↦ Option (List σ)) (some [])
        (fun (n : ℕ) (IH : (fun (x : ℕ) ↦ Option.{u_4} (List σ)) n) ↦
          (a, n, IH).2.2.bind fun (b : List σ) ↦
            Option.map (fun (b_1 : σ) ↦ (((a, n, IH), b), b_1).1.2 ++ [(((a, n, IH), b), b_1).2])
              (g ((a, n, IH), b).1.1 ((a, n, IH), b).2))
        (n + 1) =
      some (List.map (f a) (List.range (n + 1)))
⊢ Nat.rec (motive := fun (x : ℕ) ↦ Option (List σ)) (some [])
      (fun (n : ℕ) (IH : (fun (x : ℕ) ↦ Option.{u_4} (List σ)) n) ↦
        (a, n, IH).2.2.bind fun (b : List σ) ↦
          Option.map (fun (b_1 : σ) ↦ (((a, n, IH), b), b_1).1.2 ++ [(((a, n, IH), b), b_1).2])
            (g ((a, n, IH), b).1.1 ((a, n, IH), b).2))
      n =
    some (List.map (f a) (List.range n))

Tactic:
induction n with
      | zero => rfl
      | succ n IH => simp [IH, H, List.range_succ]

Premises used: Primrec.succ, List.range_succ
-- Module: Mathlib.Computability.Primrec.List
Goal:
α : Type u_1
σ : Type u_4
inst : Primcodable α
inst_1 : Primcodable σ
f : α → ℕ → σ
g : α → List σ → Option σ
hg : Primrec₂ g
H : ∀ (a : α) (n : ℕ), g a (List.map (f a) (List.range n)) = some (f a n)
this : Primrec₂.{u_1, 0, u_4} (σ := List σ) fun (a : α) (n : ℕ) ↦ List.map (f a) (List.range n)
a : α
n : ℕ
⊢ getElem? (valid := fun (as : List σ) (i : ℕ) ↦ i < as.length) (List.map (f (a, n).1) (List.range (a, n).2.succ))
      (a, n).2 =
    some (f a n)

Tactic:
simp
-- Module: Mathlib.Computability.Primrec.List
Goal:
α : Type u_1
β : Type u_2
inst : Primcodable α
inst_1 : Primcodable β
inst_2 : DecidableEq α
a : α
p : α × β
ps : List (α × β)
ih :
  (List.recOn (motive := fun (x : List (α × β)) ↦ Option β) (a, ps).2 none
      fun (b : α × β) (l : List (α × β)) (IH : Option β) ↦
      bif ((a, ps), b, l, IH).1.1 == ((a, ps), b, l, IH).2.1.1 then some ((a, ps), b, l, IH).2.1.2
      else ((a, ps), b, l, IH).2.2.2) =
    List.lookup a ps
cons :
  (bif a == p.1 then some p.2 else List.lookup a ps) =
    match (motive := Bool → Option β) a == p.1 with
    | true => some p.2
    | false => List.lookup a ps
⊢ (List.recOn (motive := fun (x : List (α × β)) ↦ Option β) (a, p :: ps).2 none
      fun (b : α × β) (l : List (α × β)) (IH : Option β) ↦
      bif ((a, p :: ps), b, l, IH).1.1 == ((a, p :: ps), b, l, IH).2.1.1 then some ((a, p :: ps), b, l, IH).2.1.2
      else ((a, p :: ps), b, l, IH).2.2.2) =
    List.lookup a (p :: ps)

Tactic:
simp [List.lookup, *]

Premises used: List.lookup
-- Module: Mathlib.Computability.Primrec.List
Goal:
α : Type u_1
β : Type u_2
inst : Primcodable α
inst_1 : Primcodable β
inst_2 : DecidableEq α
a : α
p : α × β
ps : List (α × β)
ih :
  (List.recOn (motive := fun (x : List (α × β)) ↦ Option β) (a, ps).2 none
      fun (b : α × β) (l : List (α × β)) (IH : Option β) ↦
      bif ((a, ps), b, l, IH).1.1 == ((a, ps), b, l, IH).2.1.1 then some ((a, ps), b, l, IH).2.1.2
      else ((a, ps), b, l, IH).2.2.2) =
    List.lookup a ps
cons :
  ∀ (ha : (a == p.1) = false),
    (bif false then some p.2 else List.lookup a ps) =
      match (motive := Bool → Option β) false with
      | true => some p.2
      | false => List.lookup a ps
cons₁ :
  ∀ (ha : (a == p.1) = true),
    (bif true then some p.2 else List.lookup a ps) =
      match (motive := Bool → Option β) true with
      | true => some p.2
      | false => List.lookup a ps
⊢ (bif a == p.1 then some p.2 else List.lookup a ps) =
    match (motive := Bool → Option β) a == p.1 with
    | true => some p.2
    | false => List.lookup a ps

Tactic:
cases ha : a == p.1

Premises used: Prod.fst
-- Module: Mathlib.Computability.Primrec.List
Goal:
α : Type u_1
β : Type u_2
inst : Primcodable α
inst_1 : Primcodable β
inst_2 : DecidableEq α
a : α
p : α × β
ps : List (α × β)
ih :
  (List.recOn (motive := fun (x : List (α × β)) ↦ Option β) (a, ps).2 none
      fun (b : α × β) (l : List (α × β)) (IH : Option β) ↦
      bif ((a, ps), b, l, IH).1.1 == ((a, ps), b, l, IH).2.1.1 then some ((a, ps), b, l, IH).2.1.2
      else ((a, ps), b, l, IH).2.2.2) =
    List.lookup a ps
ha : (a == p.1) = false
⊢ (bif false then some p.2 else List.lookup a ps) =
    match (motive := Bool → Option β) false with
    | true => some p.2
    | false => List.lookup a ps

Tactic:
simp
-- Module: Mathlib.Computability.Primrec.List
Goal:
α : Type u_1
β : Type u_2
inst : Primcodable α
inst_1 : Primcodable β
inst_2 : DecidableEq α
a : α
p : α × β
ps : List (α × β)
ih :
  (List.recOn (motive := fun (x : List (α × β)) ↦ Option β) (a, ps).2 none
      fun (b : α × β) (l : List (α × β)) (IH : Option β) ↦
      bif ((a, ps), b, l, IH).1.1 == ((a, ps), b, l, IH).2.1.1 then some ((a, ps), b, l, IH).2.1.2
      else ((a, ps), b, l, IH).2.2.2) =
    List.lookup a ps
ha : (a == p.1) = true
⊢ (bif true then some p.2 else List.lookup a ps) =
    match (motive := Bool → Option β) true with
    | true => some p.2
    | false => List.lookup a ps

Tactic:
simp
-- Module: Mathlib.Computability.Primrec.List
Goal:
α : Type u_1
β : Type u_2
inst : Primcodable α
inst_1 : Primcodable β
inst_2 : DecidableEq α
a : α
⊢ Eq.{u_2 + 1} (α := Option β)
    (List.recOn (motive := fun (x : List (α × β)) ↦ Option β) (a, []).2 none
        fun (b : α × β) (l : List (α × β)) (IH : Option β) ↦
        bif ((a, []), b, l, IH).1.1 == ((a, []), b, l, IH).2.1.1 then some ((a, []), b, l, IH).2.1.2
        else ((a, []), b, l, IH).2.2.2 :
      Option β)
    (List.lookup a [] : Option β)

Tactic:
simp [List.lookup, *]

Premises used: List.lookup
-- Module: Mathlib.Computability.Primrec.List
Goal:
α : Type u_1
β : Type u_2
inst : Primcodable α
inst_1 : Primcodable β
inst_2 : DecidableEq α
a : α
ps : List (α × β)
cons :
  ∀ (p : α × β) (ps : List (α × β))
    (ih :
      (List.recOn (motive := fun (x : List (α × β)) ↦ Option β) (a, ps).2 none
          fun (b : α × β) (l : List (α × β)) (IH : Option β) ↦
          bif ((a, ps), b, l, IH).1.1 == ((a, ps), b, l, IH).2.1.1 then some ((a, ps), b, l, IH).2.1.2
          else ((a, ps), b, l, IH).2.2.2) =
        List.lookup a ps),
    (List.recOn (motive := fun (x : List (α × β)) ↦ Option β) (a, p :: ps).2 none
        fun (b : α × β) (l : List (α × β)) (IH : Option β) ↦
        bif ((a, p :: ps), b, l, IH).1.1 == ((a, p :: ps), b, l, IH).2.1.1 then some ((a, p :: ps), b, l, IH).2.1.2
        else ((a, p :: ps), b, l, IH).2.2.2) =
      List.lookup a (p :: ps)
cons₁ :
  ∀ (p : α × β) (ps : List (α × β))
    (ih :
      (List.recOn (motive := fun (x : List (α × β)) ↦ Option β) (a, ps).2 none
          fun (b : α × β) (l : List (α × β)) (IH : Option β) ↦
          bif ((a, ps), b, l, IH).1.1 == ((a, ps), b, l, IH).2.1.1 then some ((a, ps), b, l, IH).2.1.2
          else ((a, ps), b, l, IH).2.2.2) =
        List.lookup a ps),
    (bif a == p.1 then some p.2 else List.lookup a ps) =
      match (motive := Bool → Option β) a == p.1 with
      | true => some p.2
      | false => List.lookup a ps
nil :
  Eq.{u_2 + 1} (α := Option β)
    (List.recOn (motive := fun (x : List (α × β)) ↦ Option β) (a, []).2 none
        fun (b : α × β) (l : List (α × β)) (IH : Option β) ↦
        bif ((a, []), b, l, IH).1.1 == ((a, []), b, l, IH).2.1.1 then some ((a, []), b, l, IH).2.1.2
        else ((a, []), b, l, IH).2.2.2 :
      Option β)
    (List.lookup a [] : Option β)
⊢ (List.recOn (motive := fun (x : List (α × β)) ↦ Option β) (a, ps).2 none
      fun (b : α × β) (l : List (α × β)) (IH : Option β) ↦
      bif ((a, ps), b, l, IH).1.1 == ((a, ps), b, l, IH).2.1.1 then some ((a, ps), b, l, IH).2.1.2
      else ((a, ps), b, l, IH).2.2.2) =
    List.lookup a ps

Tactic:
induction ps with simp [List.lookup, *]
  | cons p ps ih => cases ha : a == p.1 <;> simp

Premises used: List.lookup
-- Module: Mathlib.Computability.Primrec.List
Goal:
β : Type u_2
σ : Type u_4
inst : Primcodable β
inst_1 : 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)
haveI : ∀ (this : DecidableEq β), Primrec f
⊢ Primrec f

Tactic:
haveI : DecidableEq β := Encodable.decidableEqOfEncodable β
-- Module: Mathlib.Computability.Primrec.List
Goal:
β : Type u_2
σ : Type u_4
inst : Primcodable β
inst_1 : 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 : (M : List (β × σ)) → (bs : List β) → List σ :=
  fun (M : List (β × σ)) (bs : List β) ↦ List.flatMap (fun (x : β) ↦ (List.lookup x M).toList) bs
bindList : (b : β) → ℕ → List β :=
  fun (b : β) (n : ℕ) ↦ Nat.rec (motive := fun (x : ℕ) ↦ List β) [b] (fun (x : ℕ) (bs : List β) ↦ List.flatMap l bs) n
graph : (b : β) → ℕ → List (β × σ) :=
  fun (b : β) (i : ℕ) ↦
    Nat.rec (motive := fun (x : ℕ) ↦ List (β × σ)) []
      (fun (i : ℕ) (ih : List (β × σ)) ↦
        List.filterMap (fun (b' : β) ↦ Option.map (fun (x : σ) ↦ (b', x)) (g b' (mapGraph ih (l b'))))
          (bindList b (m b - i)))
      i
⊢ Primrec₂ mapGraph

Tactic:
have mapGraph_primrec : Primrec₂ mapGraph :=
    to₂ <| list_flatMap snd <| optionToList.comp₂ <| listLookup.comp₂ .right (fst.comp₂ .left)
-- Module: Mathlib.Computability.Primrec.List
Goal:
β : Type u_2
σ : Type u_4
inst : Primcodable β
inst_1 : 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 : (M : List (β × σ)) → (bs : List β) → List σ :=
  fun (M : List (β × σ)) (bs : List β) ↦ List.flatMap (fun (x : β) ↦ (List.lookup x M).toList) bs
bindList : (b : β) → ℕ → List β :=
  fun (b : β) (n : ℕ) ↦ Nat.rec (motive := fun (x : ℕ) ↦ List β) [b] (fun (x : ℕ) (bs : List β) ↦ List.flatMap l bs) n
graph : (b : β) → ℕ → List (β × σ) :=
  fun (b : β) (i : ℕ) ↦
    Nat.rec (motive := fun (x : ℕ) ↦ List (β × σ)) []
      (fun (i : ℕ) (ih : List (β × σ)) ↦
        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
⊢ Primrec₂ bindList

Tactic:
have bindList_primrec : Primrec₂ (bindList) :=
    nat_rec' snd
      (list_cons.comp fst (const []))
      (to₂ <| list_flatMap (snd.comp snd) (hl.comp₂ .right))
-- Module: Mathlib.Computability.Primrec.List
Goal:
β : Type u_2
σ : Type u_4
inst : Primcodable β
inst_1 : 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 : (M : List (β × σ)) → (bs : List β) → List σ :=
  fun (M : List (β × σ)) (bs : List β) ↦ List.flatMap (fun (x : β) ↦ (List.lookup x M).toList) bs
bindList : (b : β) → ℕ → List β :=
  fun (b : β) (n : ℕ) ↦ Nat.rec (motive := fun (x : ℕ) ↦ List β) [b] (fun (x : ℕ) (bs : List β) ↦ List.flatMap l bs) n
graph : (b : β) → ℕ → List (β × σ) :=
  fun (b : β) (i : ℕ) ↦
    Nat.rec (motive := fun (x : ℕ) ↦ List (β × σ)) []
      (fun (i : ℕ) (ih : List (β × σ)) ↦
        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
⊢ Primrec₂ graph

Tactic:
have graph_primrec : Primrec₂ (graph) :=
    to₂ <| nat_rec' snd (const []) <|
      to₂ <| listFilterMap
        (bindList_primrec.comp
          (fst.comp fst)
          (nat_sub.comp (hm.comp <| fst.comp fst) (fst.comp snd))) <|
            to₂ <| option_map
              (hg.comp snd (mapGraph_primrec.comp (snd.comp <| snd.comp fst) (hl.comp snd)))
              (Primrec₂.pair.comp₂ (snd.comp₂ .left) .right)
-- Module: Mathlib.Computability.Primrec.List
Goal:
β : Type u_2
σ : Type u_4
inst : Primcodable β
inst_1 : 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 : (M : List (β × σ)) → (bs : List β) → List σ :=
  fun (M : List (β × σ)) (bs : List β) ↦ List.flatMap (fun (x : β) ↦ (List.lookup x M).toList) bs
bindList : (b : β) → ℕ → List β :=
  fun (b : β) (n : ℕ) ↦ Nat.rec (motive := fun (x : ℕ) ↦ List β) [b] (fun (x : ℕ) (bs : List β) ↦ List.flatMap l bs) n
graph : (b : β) → ℕ → List (β × σ) :=
  fun (b : β) (i : ℕ) ↦
    Nat.rec (motive := fun (x : ℕ) ↦ List (β × σ)) []
      (fun (i : ℕ) (ih : List (β × σ)) ↦
        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
⊢ Primrec.{u_2, u_4} (β := Option σ) fun (b : β) ↦
    Option.map Prod.snd (getElem? (valid := fun (as : List (β × σ)) (i : ℕ) ↦ i < as.length) (graph b (m b + 1)) 0)

Tactic:
have : Primrec (fun b => (graph b (m b + 1))[0]?.map Prod.snd) :=
    option_map (list_getElem?.comp (graph_primrec.comp Primrec.id (succ.comp hm)) (const 0))
      (snd.comp₂ Primrec₂.right)
-- Module: Mathlib.Computability.Primrec.List
Goal:
β : Type u_2
σ : Type u_4
inst : Primcodable β
inst_1 : 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_1 : DecidableEq β
mapGraph : (M : List (β × σ)) → (bs : List β) → List σ :=
  fun (M : List (β × σ)) (bs : List β) ↦ List.flatMap (fun (x : β) ↦ (List.lookup x M).toList) bs
bindList : (b : β) → ℕ → List β :=
  fun (b : β) (n : ℕ) ↦ Nat.rec (motive := fun (x : ℕ) ↦ List β) [b] (fun (x : ℕ) (bs : List β) ↦ List.flatMap l bs) n
graph : (b : β) → ℕ → List (β × σ) :=
  fun (b : β) (i : ℕ) ↦
    Nat.rec (motive := fun (x : ℕ) ↦ List (β × σ)) []
      (fun (i : ℕ) (ih : List (β × σ)) ↦
        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.{u_2, u_4} (β := Option σ) fun (b : β) ↦
    Option.map Prod.snd (getElem? (valid := fun (as : List (β × σ)) (i : ℕ) ↦ i < as.length) (graph b (m b + 1)) 0)
b : β
i : ℕ
hi : i ≤ m b + 1
k : ℕ
ih : ∀ b' ∈ bindList b k, m b' < m b + 1 - k
succ :
  ∀ (b' x : β),
    Membership.mem (γ := List β)
        (Nat.rec (motive := fun (x : ℕ) ↦ List β) [b] (fun (x : ℕ) (bs : List β) ↦ List.flatMap l bs) k : List β) x →
      b' ∈ l x → m b' < m b - k
⊢ ∀ b' ∈ bindList b (k + 1), m b' < m b + 1 - (k + 1)

Tactic:
simp [bindList]
-- Module: Mathlib.Computability.Primrec.List
Goal:
β : Type u_2
σ : Type u_4
inst : Primcodable β
inst_1 : 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_1 : DecidableEq β
mapGraph : (M : List (β × σ)) → (bs : List β) → List σ :=
  fun (M : List (β × σ)) (bs : List β) ↦ List.flatMap (fun (x : β) ↦ (List.lookup x M).toList) bs
bindList : (b : β) → ℕ → List β :=
  fun (b : β) (n : ℕ) ↦ Nat.rec (motive := fun (x : ℕ) ↦ List β) [b] (fun (x : ℕ) (bs : List β) ↦ List.flatMap l bs) n
graph : (b : β) → ℕ → List (β × σ) :=
  fun (b : β) (i : ℕ) ↦
    Nat.rec (motive := fun (x : ℕ) ↦ List (β × σ)) []
      (fun (i : ℕ) (ih : List (β × σ)) ↦
        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.{u_2, u_4} (β := Option σ) fun (b : β) ↦
    Option.map Prod.snd (getElem? (valid := fun (as : List (β × σ)) (i : ℕ) ↦ i < as.length) (graph b (m b + 1)) 0)
b : β
i : ℕ
hi : i ≤ m b + 1
k : ℕ
ih : ∀ b' ∈ bindList b k, m b' < m b + 1 - k
⊢ ∀ (b' x : β),
    Membership.mem (γ := List β)
        (Nat.rec (motive := fun (x : ℕ) ↦ List β) [b] (fun (x : ℕ) (bs : List β) ↦ List.flatMap l bs) k : List β) x →
      b' ∈ l x → m b' < m b - k

Tactic:
grind
-- Module: Mathlib.Computability.Primrec.List
Goal:
β : Type u_2
σ : Type u_4
inst : Primcodable β
inst_1 : 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_1 : DecidableEq β
mapGraph : (M : List (β × σ)) → (bs : List β) → List σ :=
  fun (M : List (β × σ)) (bs : List β) ↦ List.flatMap (fun (x : β) ↦ (List.lookup x M).toList) bs
bindList : (b : β) → ℕ → List β :=
  fun (b : β) (n : ℕ) ↦ Nat.rec (motive := fun (x : ℕ) ↦ List β) [b] (fun (x : ℕ) (bs : List β) ↦ List.flatMap l bs) n
graph : (b : β) → ℕ → List (β × σ) :=
  fun (b : β) (i : ℕ) ↦
    Nat.rec (motive := fun (x : ℕ) ↦ List (β × σ)) []
      (fun (i : ℕ) (ih : List (β × σ)) ↦
        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.{u_2, u_4} (β := Option σ) fun (b : β) ↦
    Option.map Prod.snd (getElem? (valid := fun (as : List (β × σ)) (i : ℕ) ↦ i < as.length) (graph b (m b + 1)) 0)
b : β
i : ℕ
hi : i ≤ m b + 1
⊢ ∀ b' ∈ bindList b 0, m b' < m b + 1 - 0

Tactic:
simp [bindList]
-- Module: Mathlib.Computability.Primrec.List
Goal:
β : Type u_2
σ : Type u_4
inst : Primcodable β
inst_1 : 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_1 : DecidableEq β
mapGraph : (M : List (β × σ)) → (bs : List β) → List σ :=
  fun (M : List (β × σ)) (bs : List β) ↦ List.flatMap (fun (x : β) ↦ (List.lookup x M).toList) bs
bindList : (b : β) → ℕ → List β :=
  fun (b : β) (n : ℕ) ↦ Nat.rec (motive := fun (x : ℕ) ↦ List β) [b] (fun (x : ℕ) (bs : List β) ↦ List.flatMap l bs) n
graph : (b : β) → ℕ → List (β × σ) :=
  fun (b : β) (i : ℕ) ↦
    Nat.rec (motive := fun (x : ℕ) ↦ List (β × σ)) []
      (fun (i : ℕ) (ih : List (β × σ)) ↦
        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.{u_2, u_4} (β := Option σ) fun (b : β) ↦
    Option.map Prod.snd (getElem? (valid := fun (as : List (β × σ)) (i : ℕ) ↦ i < as.length) (graph b (m b + 1)) 0)
b : β
i : ℕ
hi : i ≤ m b + 1
k : ℕ
succ : ∀ (k : ℕ) (ih : ∀ b' ∈ bindList b k, m b' < m b + 1 - k), ∀ b' ∈ bindList b (k + 1), m b' < m b + 1 - (k + 1)
succ₁ :
  ∀ (k : ℕ) (ih : ∀ b' ∈ bindList b k, m b' < m b + 1 - k) (b' x : β),
    Membership.mem (γ := List β)
        (Nat.rec (motive := fun (x : ℕ) ↦ List β) [b] (fun (x : ℕ) (bs : List β) ↦ List.flatMap l bs) k : List β) x →
      b' ∈ l x → m b' < m b - k
zero : ∀ b' ∈ bindList b 0, m b' < m b + 1 - 0
⊢ ∀ b' ∈ bindList b k, m b' < m b + 1 - k

Tactic:
induction k with simp [bindList]
          | succ k ih =>
            grind

Premises used: Primrec.succ