awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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_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
bindList_eq_nil : bindList b (m b + 1) = []
mapGraph_graph :
  ∀ {bs bs' : List β} (has : bs' ⊆ bs), mapGraph (List.map (fun (x : β) ↦ (x, f x)) bs) bs' = List.map f bs'
graph_succ :
  ∀ (i : ℕ),
    graph b (i + 1) =
      List.filterMap (fun (b' : β) ↦ Option.map (fun (x : σ) ↦ (b', x)) (g b' (mapGraph (graph b i) (l b'))))
        (bindList b (m b - i))
⊢ graph b i = List.map (fun (x : β) ↦ (x, f x)) (bindList b (m b + 1 - i))
have bindList_succ : ∀ (i : ℕ), bindList b (i + 1) = List.flatMap l (bindList b i)
Tactic: have bindList_succ : ∀ i, bindList b (i + 1) = (bindList b i).flatMap l := fun _ => rfl
-- 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 : β
bindList_eq_nil : bindList b (m b + 1) = []
mapGraph_graph :
  ∀ {bs bs' : List β} (has : bs' ⊆ bs), mapGraph (List.map (fun (x : β) ↦ (x, f x)) bs) bs' = List.map f bs'
graph_succ :
  ∀ (i : ℕ),
    graph b (i + 1) =
      List.filterMap (fun (b' : β) ↦ Option.map (fun (x : σ) ↦ (b', x)) (g b' (mapGraph (graph b i) (l b'))))
        (bindList b (m b - i))
bindList_succ : ∀ (i : ℕ), bindList b (i + 1) = List.flatMap l (bindList b i)
hi : 0 ≤ m b + 1
⊢ graph b 0 = List.map (fun (x : β) ↦ (x, f x)) (bindList b (m b + 1 - 0))
have zero : List.map (fun (x : β) ↦ (x, f x)) (bindList b (m b + 1 - 0)) = graph b 0
Tactic: symm
-- 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 : β
bindList_eq_nil : bindList b (m b + 1) = []
mapGraph_graph :
  ∀ {bs bs' : List β} (has : bs' ⊆ bs), mapGraph (List.map (fun (x : β) ↦ (x, f x)) bs) bs' = List.map f bs'
graph_succ :
  ∀ (i : ℕ),
    graph b (i + 1) =
      List.filterMap (fun (b' : β) ↦ Option.map (fun (x : σ) ↦ (b', x)) (g b' (mapGraph (graph b i) (l b'))))
        (bindList b (m b - i))
bindList_succ : ∀ (i : ℕ), bindList b (i + 1) = List.flatMap l (bindList b i)
i : ℕ
ih : ∀ (hi : i ≤ m b + 1), graph b i = List.map (fun (x : β) ↦ (x, f x)) (bindList b (m b + 1 - i))
hi : i + 1 ≤ m b + 1
⊢ graph b (i + 1) = List.map (fun (x : β) ↦ (x, f x)) (bindList b (m b + 1 - (i + 1)))
have succ : Eq (α := List (β × σ))
  (List.filterMap
    (fun (x : β) ↦
      Option.map (fun (x_1 : σ) ↦ (x, x_1))
        (g x (mapGraph (List.map (fun (x : β) ↦ (x, f x)) (List.flatMap l (bindList b (m b - i)))) (l x))))
    (bindList b (m b - i)))
  (List.map (fun (x : β) ↦ (x, f x)) (bindList b (m b - i)))
Tactic: simp only [graph_succ, ih (Nat.le_of_lt hi), Nat.succ_sub (Nat.le_of_lt_succ hi),
          Nat.succ_eq_add_one, bindList_succ, Nat.reduceSubDiff]
-- 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 : β
bindList_eq_nil : bindList b (m b + 1) = []
mapGraph_graph :
  ∀ {bs bs' : List β} (has : bs' ⊆ bs), mapGraph (List.map (fun (x : β) ↦ (x, f x)) bs) bs' = List.map f bs'
graph_succ :
  ∀ (i : ℕ),
    graph b (i + 1) =
      List.filterMap (fun (b' : β) ↦ Option.map (fun (x : σ) ↦ (b', x)) (g b' (mapGraph (graph b i) (l b'))))
        (bindList b (m b - i))
bindList_succ : ∀ (i : ℕ), bindList b (i + 1) = List.flatMap l (bindList b i)
i : ℕ
ih : ∀ (hi : i ≤ m b + 1), graph b i = List.map (fun (x : β) ↦ (x, f x)) (bindList b (m b + 1 - i))
hi : i + 1 ≤ m b + 1
⊢ Eq (α := List (β × σ))
    (List.filterMap
      (fun (x : β) ↦
        Option.map (fun (x_1 : σ) ↦ (x, x_1))
          (g x (mapGraph (List.map (fun (x : β) ↦ (x, f x)) (List.flatMap l (bindList b (m b - i)))) (l x))))
      (bindList b (m b - i)))
    (List.map (fun (x : β) ↦ (x, f x)) (bindList b (m b - i)))
have succ : ∀ x ∈ bindList b (m b - i),
  Option.map (fun (x_1 : σ) ↦ (x, x_1))
      (g x (mapGraph (List.map (fun (x : β) ↦ (x, f x)) (List.flatMap l (bindList b (m b - i)))) (l x))) =
    some (x, f x)
Tactic: apply List.filterMap_eq_map_iff_forall_eq_some.mpr
-- 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 : β
bindList_eq_nil : bindList b (m b + 1) = []
mapGraph_graph :
  ∀ {bs bs' : List β} (has : bs' ⊆ bs), mapGraph (List.map (fun (x : β) ↦ (x, f x)) bs) bs' = List.map f bs'
graph_succ :
  ∀ (i : ℕ),
    graph b (i + 1) =
      List.filterMap (fun (b' : β) ↦ Option.map (fun (x : σ) ↦ (b', x)) (g b' (mapGraph (graph b i) (l b'))))
        (bindList b (m b - i))
bindList_succ : ∀ (i : ℕ), bindList b (i + 1) = List.flatMap l (bindList b i)
i : ℕ
ih : ∀ (hi : i ≤ m b + 1), graph b i = List.map (fun (x : β) ↦ (x, f x)) (bindList b (m b + 1 - i))
hi : i + 1 ≤ m b + 1
b' : β
ha' : b' ∈ bindList b (m b - i)
⊢ Option.map (fun (x : σ) ↦ (b', x))
      (g b' (mapGraph (List.map (fun (x : β) ↦ (x, f x)) (List.flatMap l (bindList b (m b - i)))) (l b'))) =
    some (b', f b')
have succ : g b' (mapGraph (List.map (fun (x : β) ↦ (x, f x)) (List.flatMap l (bindList b (m b - i)))) (l b')) = some (f b')
Tactic: simp
-- 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 : β
bindList_eq_nil : bindList b (m b + 1) = []
mapGraph_graph :
  ∀ {bs bs' : List β} (has : bs' ⊆ bs), mapGraph (List.map (fun (x : β) ↦ (x, f x)) bs) bs' = List.map f bs'
graph_succ :
  ∀ (i : ℕ),
    graph b (i + 1) =
      List.filterMap (fun (b' : β) ↦ Option.map (fun (x : σ) ↦ (b', x)) (g b' (mapGraph (graph b i) (l b'))))
        (bindList b (m b - i))
bindList_succ : ∀ (i : ℕ), bindList b (i + 1) = List.flatMap l (bindList b i)
i : ℕ
ih : ∀ (hi : i ≤ m b + 1), graph b i = List.map (fun (x : β) ↦ (x, f x)) (bindList b (m b + 1 - i))
hi : i + 1 ≤ m b + 1
b' : β
ha' : b' ∈ bindList b (m b - i)
⊢ g b' (mapGraph (List.map (fun (x : β) ↦ (x, f x)) (List.flatMap l (bindList b (m b - i)))) (l b')) = some (f b')
have succ : g b' (List.map f (l b')) = some (f b')
Tactic: rw [mapGraph_graph]
-- 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 : β
bindList_eq_nil : bindList b (m b + 1) = []
mapGraph_graph :
  ∀ {bs bs' : List β} (has : bs' ⊆ bs), mapGraph (List.map (fun (x : β) ↦ (x, f x)) bs) bs' = List.map f bs'
graph_succ :
  ∀ (i : ℕ),
    graph b (i + 1) =
      List.filterMap (fun (b' : β) ↦ Option.map (fun (x : σ) ↦ (b', x)) (g b' (mapGraph (graph b i) (l b'))))
        (bindList b (m b - i))
bindList_succ : ∀ (i : ℕ), bindList b (i + 1) = List.flatMap l (bindList b i)
i : ℕ
ih : ∀ (hi : i ≤ m b + 1), graph b i = List.map (fun (x : β) ↦ (x, f x)) (bindList b (m b + 1 - i))
hi : i + 1 ≤ m b + 1
b' : β
ha' : b' ∈ bindList b (m b - i)
succ : g b' (List.map f (l b')) = some (f b')
⊢ g b' (mapGraph (List.map (fun (x : β) ↦ (x, f x)) (List.flatMap l (bindList b (m b - i)))) (l b')) = some (f b')
have succ₁ : l b' ⊆ List.flatMap l (bindList b (m b - i))
Tactic: rw [mapGraph_graph]
-- 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
bindList_eq_nil : bindList b (m b + 1) = []
mapGraph_graph :
  ∀ {bs bs' : List β} (has : bs' ⊆ bs), mapGraph (List.map (fun (x : β) ↦ (x, f x)) bs) bs' = List.map f bs'
graph_succ :
  ∀ (i : ℕ),
    graph b (i + 1) =
      List.filterMap (fun (b' : β) ↦ Option.map (fun (x : σ) ↦ (b', x)) (g b' (mapGraph (graph b i) (l b'))))
        (bindList b (m b - i))
bindList_succ : ∀ (i : ℕ), bindList b (i + 1) = List.flatMap l (bindList b i)
⊢ graph b i = List.map (fun (x : β) ↦ (x, f x)) (bindList b (m b + 1 - i))
have zero : ∀ (hi : 0 ≤ m b + 1), graph b 0 = List.map (fun (x : β) ↦ (x, f x)) (bindList b (m b + 1 - 0))
Tactic: induction i with
      | zero => symm; simpa [graph] using bindList_eq_nil
      | succ i ih =>
        simp only [graph_succ, ih (Nat.le_of_lt hi), Nat.succ_sub (Nat.le_of_lt_succ hi),
          Nat.succ_eq_add_one, bindList_succ, Nat.reduceSubDiff]
        apply List.filterMap_eq_map_iff_forall_eq_some.mpr
        intro b' ha'; simp; rw [mapGraph_graph]
        · exact H b'
        · exact (List.infix_flatMap_of_mem ha' l).subset
Cleared hypotheses: i, hi
-- 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
bindList_eq_nil : bindList b (m b + 1) = []
mapGraph_graph :
  ∀ {bs bs' : List β} (has : bs' ⊆ bs), mapGraph (List.map (fun (x : β) ↦ (x, f x)) bs) bs' = List.map f bs'
graph_succ :
  ∀ (i : ℕ),
    graph b (i + 1) =
      List.filterMap (fun (b' : β) ↦ Option.map (fun (x : σ) ↦ (b', x)) (g b' (mapGraph (graph b i) (l b'))))
        (bindList b (m b - i))
bindList_succ : ∀ (i : ℕ), bindList b (i + 1) = List.flatMap l (bindList b i)
zero : ∀ (hi : 0 ≤ m b + 1), graph b 0 = List.map (fun (x : β) ↦ (x, f x)) (bindList b (m b + 1 - 0))
⊢ graph b i = List.map (fun (x : β) ↦ (x, f x)) (bindList b (m b + 1 - i))
have succ : ∀ (i : ℕ) (ih : ∀ (hi : i ≤ m b + 1), graph b i = List.map (fun (x : β) ↦ (x, f x)) (bindList b (m b + 1 - i)))
  (hi : i + 1 ≤ m b + 1), graph b (i + 1) = List.map (fun (x : β) ↦ (x, f x)) (bindList b (m b + 1 - (i + 1)))
Tactic: induction i with
      | zero => symm; simpa [graph] using bindList_eq_nil
      | succ i ih =>
        simp only [graph_succ, ih (Nat.le_of_lt hi), Nat.succ_sub (Nat.le_of_lt_succ hi),
          Nat.succ_eq_add_one, bindList_succ, Nat.reduceSubDiff]
        apply List.filterMap_eq_map_iff_forall_eq_some.mpr
        intro b' ha'; simp; rw [mapGraph_graph]
        · exact H b'
        · exact (List.infix_flatMap_of_mem ha' l).subset
Cleared hypotheses: i, hi
-- 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_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 : β
⊢ Option.map Prod.snd (getElem? (valid := fun (as : List (β × σ)) (i : ℕ) ↦ i < as.length) (graph b (m b + 1)) 0) =
    some (f b)
have graph_eq_map_bindList : ∀ (i : ℕ) (hi : i ≤ m b + 1), graph b i = List.map (fun (x : β) ↦ (x, f x)) (bindList b (m b + 1 - i))
Tactic: have graph_eq_map_bindList (i : ℕ) (hi : i ≤ m b + 1) :
        graph b i = (bindList b (m b + 1 - i)).map fun x ↦ (x, f x) := by
      have bindList_eq_nil : bindList b (m b + 1) = [] :=
        have bindList_m_lt (k : ℕ) : ∀ b' ∈ bindList b k, m b' < m b + 1 - k := by
          induction k with simp [bindList]
          | succ k ih =>
            grind
        List.eq_nil_iff_forall_not_mem.mpr
          (by intro b' ha'; by_contra; simpa using bindList_m_lt (m b + 1) b' ha')
      have mapGraph_graph {bs bs' : List β} (has : bs' ⊆ bs) :
          mapGraph (bs.map <| fun x => (x, f x)) bs' = bs'.map f := by
        induction bs' with simp [mapGraph]
        | cons b bs' ih =>
          have : b ∈ bs ∧ bs' ⊆ bs := by simpa using has
          rcases this with ⟨ha, has'⟩
          simpa [List.lookup_graph f ha] using ih has'
      have graph_succ : ∀ i, graph b (i + 1) =
        (bindList b (m b - i)).filterMap fun b' =>
          (g b' <| mapGraph (graph b i) (l b')).map (b', ·) := fun _ => rfl
      have bindList_succ : ∀ i, bindList b (i + 1) = (bindList b i).flatMap l := fun _ => rfl
      induction i with
      | zero => symm; simpa [graph] using bindList_eq_nil
      | succ i ih =>
        simp only [graph_succ, ih (Nat.le_of_lt hi), Nat.succ_sub (Nat.le_of_lt_succ hi),
          Nat.succ_eq_add_one, bindList_succ, Nat.reduceSubDiff]
        apply List.filterMap_eq_map_iff_forall_eq_some.mpr
        intro b' ha'; simp; rw [mapGraph_graph]
        · exact H b'
        · exact (List.infix_flatMap_of_mem ha' l).subset
-- Lean 4 proof step from Mathlib.Computability.Primrec.List (goal)
Goal:
α : 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
have rw : (List.drop ((n, l).2.length - (n, l).1) (n, l).2.reverse).reverse = (List.take n l).reverse.reverse
Tactic: rw [← List.reverse_reverse (l.take n), List.reverse_take]
-- Lean 4 proof step from Mathlib.Computability.Primrec.List (goal)
Goal:
α : Type u_1
inst : Primcodable α
x : ℕ × List α
n : ℕ
l : List α
rw : (List.drop ((n, l).2.length - (n, l).1) (n, l).2.reverse).reverse = (List.take n l).reverse.reverse
⊢ (List.drop ((n, l).2.length - (n, l).1) (n, l).2.reverse).reverse = List.take (n, l).1 (n, l).2
have rw₁ : (List.drop ((n, l).2.length - (n, l).1) (n, l).2.reverse).reverse = (List.drop (l.length - n) l.reverse).reverse
Tactic: rw [← List.reverse_reverse (l.take n), List.reverse_take]