awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
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
⊢ ∀ b' ∈ bindList b k, m b' < m b + 1 - k
have zero : ∀ b' ∈ bindList b 0, m b' < m b + 1 - 0
Tactic: induction k with simp [bindList]
          | succ k ih =>
            grind
Cleared hypotheses: k
-- 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_m_lt : ∀ (k : ℕ), ∀ b' ∈ bindList b k, m b' < m b + 1 - k
b' : β
ha' : b' ∈ bindList b (m b + 1)
⊢ False
have this₁ : ¬False
Tactic: by_contra
-- 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
⊢ graph b i = List.map (fun (x : β) ↦ (x, f x)) (bindList b (m b + 1 - i))
have bindList_eq_nil : bindList b (m b + 1) = []
Tactic: 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')
-- 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_1 : β
i : ℕ
hi : i ≤ m b_1 + 1
bindList_eq_nil : bindList b_1 (m b_1 + 1) = []
bs : List β
b : β
bs' : List β
ih : ∀ (has : bs' ⊆ bs), mapGraph (List.map (fun (x : β) ↦ (x, f x)) bs) bs' = List.map f bs'
has : b :: bs' ⊆ bs
⊢ mapGraph (List.map (fun (x : β) ↦ (x, f x)) bs) (b :: bs') = List.map f (b :: bs')
have cons : HAppend.hAppend (α := List σ) (Option.toList (List.lookup b (List.map (fun (x : β) ↦ (x, f x)) bs)))
    (List.flatMap (fun (x : β) ↦ Option.toList (List.lookup x (List.map (fun (x : β) ↦ (x, f x)) bs))) bs') =
  f b :: List.map f bs'
Tactic: simp [mapGraph]
-- 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_1 : β
i : ℕ
hi : i ≤ m b_1 + 1
bindList_eq_nil : bindList b_1 (m b_1 + 1) = []
bs : List β
b : β
bs' : List β
ih : ∀ (has : bs' ⊆ bs), mapGraph (List.map (fun (x : β) ↦ (x, f x)) bs) bs' = List.map f bs'
has : b :: bs' ⊆ bs
⊢ HAppend.hAppend (α := List σ) (Option.toList (List.lookup b (List.map (fun (x : β) ↦ (x, f x)) bs)))
      (List.flatMap (fun (x : β) ↦ Option.toList (List.lookup x (List.map (fun (x : β) ↦ (x, f x)) bs))) bs') =
    f b :: List.map f bs'
have this₁ : b ∈ bs ∧ bs' ⊆ bs
Tactic: have : b ∈ bs ∧ bs' ⊆ bs := by simpa using has
-- 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_2 :
  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_1 : β
i : ℕ
hi : i ≤ m b_1 + 1
bindList_eq_nil : bindList b_1 (m b_1 + 1) = []
bs : List β
b : β
bs' : List β
ih : ∀ (has : bs' ⊆ bs), mapGraph (List.map (fun (x : β) ↦ (x, f x)) bs) bs' = List.map f bs'
has : b :: bs' ⊆ bs
this : b ∈ bs ∧ bs' ⊆ bs
⊢ HAppend.hAppend (α := List σ) (Option.toList (List.lookup b (List.map (fun (x : β) ↦ (x, f x)) bs)))
      (List.flatMap (fun (x : β) ↦ Option.toList (List.lookup x (List.map (fun (x : β) ↦ (x, f x)) bs))) bs') =
    f b :: List.map f bs'
have ha : b ∈ bs
Tactic: rcases this with ⟨ha, has'⟩
Cleared hypotheses: this
-- 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_2 :
  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_1 : β
i : ℕ
hi : i ≤ m b_1 + 1
bindList_eq_nil : bindList b_1 (m b_1 + 1) = []
bs : List β
b : β
bs' : List β
ih : ∀ (has : bs' ⊆ bs), mapGraph (List.map (fun (x : β) ↦ (x, f x)) bs) bs' = List.map f bs'
has : b :: bs' ⊆ bs
this : b ∈ bs ∧ bs' ⊆ bs
ha : b ∈ bs
⊢ HAppend.hAppend (α := List σ) (Option.toList (List.lookup b (List.map (fun (x : β) ↦ (x, f x)) bs)))
      (List.flatMap (fun (x : β) ↦ Option.toList (List.lookup x (List.map (fun (x : β) ↦ (x, f x)) bs))) bs') =
    f b :: List.map f bs'
have has' : bs' ⊆ bs
Tactic: rcases this with ⟨ha, has'⟩
Cleared hypotheses: this
-- 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) = []
bs bs' : List β
has : bs' ⊆ bs
⊢ mapGraph (List.map (fun (x : β) ↦ (x, f x)) bs) bs' = List.map f bs'
have cons : ∀ (b : β) (bs' : List β) (ih : ∀ (has : bs' ⊆ bs), mapGraph (List.map (fun (x : β) ↦ (x, f x)) bs) bs' = List.map f bs')
  (has : b :: bs' ⊆ bs), mapGraph (List.map (fun (x : β) ↦ (x, f x)) bs) (b :: bs') = List.map f (b :: bs')
Tactic: 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'
Cleared hypotheses: bs', has
-- 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) = []
bs bs' : List β
has : bs' ⊆ bs
cons :
  ∀ (b : β) (bs' : List β)
    (ih : ∀ (has : bs' ⊆ bs), mapGraph (List.map (fun (x : β) ↦ (x, f x)) bs) bs' = List.map f bs')
    (has : b :: bs' ⊆ bs), mapGraph (List.map (fun (x : β) ↦ (x, f x)) bs) (b :: bs') = List.map f (b :: bs')
⊢ mapGraph (List.map (fun (x : β) ↦ (x, f x)) bs) bs' = List.map f bs'
have cons₁ : ∀ (b : β) (bs' : List β) (ih : ∀ (has : bs' ⊆ bs), mapGraph (List.map (fun (x : β) ↦ (x, f x)) bs) bs' = List.map f bs')
  (has : b :: bs' ⊆ bs),
  HAppend.hAppend (α := List σ) (Option.toList (List.lookup b (List.map (fun (x : β) ↦ (x, f x)) bs)))
      (List.flatMap (fun (x : β) ↦ Option.toList (List.lookup x (List.map (fun (x : β) ↦ (x, f x)) bs))) bs') =
    f b :: List.map f bs'
Tactic: 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'
Cleared hypotheses: bs', has
-- 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) = []
bs bs' : List β
has : bs' ⊆ bs
cons :
  ∀ (b : β) (bs' : List β)
    (ih : ∀ (has : bs' ⊆ bs), mapGraph (List.map (fun (x : β) ↦ (x, f x)) bs) bs' = List.map f bs')
    (has : b :: bs' ⊆ bs), mapGraph (List.map (fun (x : β) ↦ (x, f x)) bs) (b :: bs') = List.map f (b :: bs')
cons₁ :
  ∀ (b : β) (bs' : List β)
    (ih : ∀ (has : bs' ⊆ bs), mapGraph (List.map (fun (x : β) ↦ (x, f x)) bs) bs' = List.map f bs')
    (has : b :: bs' ⊆ bs),
    HAppend.hAppend (α := List σ) (Option.toList (List.lookup b (List.map (fun (x : β) ↦ (x, f x)) bs)))
        (List.flatMap (fun (x : β) ↦ Option.toList (List.lookup x (List.map (fun (x : β) ↦ (x, f x)) bs))) bs') =
      f b :: List.map f bs'
⊢ mapGraph (List.map (fun (x : β) ↦ (x, f x)) bs) bs' = List.map f bs'
have nil : ∀ (has : [] ⊆ bs), mapGraph (List.map (fun (x : β) ↦ (x, f x)) bs) [] = List.map f []
Tactic: 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'
Cleared hypotheses: bs', has
-- 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) = []
⊢ graph b i = List.map (fun (x : β) ↦ (x, f x)) (bindList b (m b + 1 - i))
have mapGraph_graph : ∀ {bs bs' : List β} (has : bs' ⊆ bs), mapGraph (List.map (fun (x : β) ↦ (x, f x)) bs) bs' = List.map f bs'
Tactic: 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'
-- 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 b i = List.map (fun (x : β) ↦ (x, f x)) (bindList b (m b + 1 - i))
have 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))
Tactic: 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