awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Computability.Primrec.List (goal)
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, 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)
have dsimp : List.foldr (fun (b : β) (s : ℕ) ↦ bif p a b then 0 else s + 1) 0 (f a) = List.findIdx (p a) (f a)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Computability.Primrec.List (goal)
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 (f a) = List.findIdx (p a) (f a)
have nil : List.foldr (fun (b : β) (s : ℕ) ↦ bif p a b then 0 else s + 1) 0 [] = List.findIdx (p a) []
Tactic: induction f a
-- Lean 4 proof step from Mathlib.Computability.Primrec.List (goal)
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) []
⊢ List.foldr (fun (b : β) (s : ℕ) ↦ bif p a b then 0 else s + 1) 0 (f a) = List.findIdx (p a) (f a)
have 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)
Tactic: induction f a
-- Lean 4 proof step from Mathlib.Computability.Primrec.List (goal)
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 : ℕ
⊢ 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))
have 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))
Tactic: induction n with
      | zero => rfl
      | succ n IH => simp [IH, H, List.range_succ]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Computability.Primrec.List (goal)
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))
⊢ 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))
have 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)))
Tactic: induction n with
      | zero => rfl
      | succ n IH => simp [IH, H, List.range_succ]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Computability.Primrec.List (goal)
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
⊢ (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)
have 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
Tactic: simp [List.lookup, *]
-- Lean 4 proof step from Mathlib.Computability.Primrec.List (goal)
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
⊢ (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
have 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
Tactic: cases ha : a == p.1
-- Lean 4 proof step from Mathlib.Computability.Primrec.List (goal)
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
⊢ (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
have 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
Tactic: cases ha : a == p.1
-- Lean 4 proof step from Mathlib.Computability.Primrec.List (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Primcodable α
inst_1 : Primcodable β
inst_2 : DecidableEq α
a : α
ps : List (α × β)
⊢ (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
have 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)
Tactic: induction ps with simp [List.lookup, *]
  | cons p ps ih => cases ha : a == p.1 <;> simp
Cleared hypotheses: ps
-- Lean 4 proof step from Mathlib.Computability.Primrec.List (goal)
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)
⊢ (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
have 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
Tactic: induction ps with simp [List.lookup, *]
  | cons p ps ih => cases ha : a == p.1 <;> simp
Cleared hypotheses: ps
-- Lean 4 proof step from Mathlib.Computability.Primrec.List (goal)
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
⊢ (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
have 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 β)
Tactic: induction ps with simp [List.lookup, *]
  | cons p ps ih => cases ha : a == p.1 <;> simp
Cleared hypotheses: ps
-- Lean 4 proof step from Mathlib.Computability.Primrec.List (goal)
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)
⊢ Primrec f
have haveI : ∀ (this : DecidableEq β), Primrec f
Tactic: haveI : DecidableEq β := Encodable.decidableEqOfEncodable β
-- Lean 4 proof step from Mathlib.Computability.Primrec.List (hypothesis)
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 f
have mapGraph_primrec : Primrec₂ mapGraph
Tactic: have mapGraph_primrec : Primrec₂ mapGraph :=
    to₂ <| list_flatMap snd <| optionToList.comp₂ <| listLookup.comp₂ .right (fst.comp₂ .left)
-- Lean 4 proof step from Mathlib.Computability.Primrec.List (hypothesis)
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 f
have bindList_primrec : 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))
-- Lean 4 proof step from Mathlib.Computability.Primrec.List (hypothesis)
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 f
have graph_primrec : 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)
-- Lean 4 proof step from Mathlib.Computability.Primrec.List (hypothesis)
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 f
have 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)
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)
-- Lean 4 proof step from Mathlib.Computability.Primrec.List (goal)
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' ∈ bindList b (k + 1), m b' < m b + 1 - (k + 1)
have 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
Tactic: simp [bindList]
-- Lean 4 proof step from Mathlib.Computability.Primrec.List (goal)
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 : ℕ
⊢ ∀ b' ∈ bindList b k, m b' < m b + 1 - k
have 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)
Tactic: induction k with simp [bindList]
          | succ k ih =>
            grind
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.Computability.Primrec.List (goal)
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)
⊢ ∀ b' ∈ bindList b k, m b' < m b + 1 - k
have 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
Tactic: induction k with simp [bindList]
          | succ k ih =>
            grind
Cleared hypotheses: k