awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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), 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
-- 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 : β
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))
⊢ Option.map Prod.snd (getElem? (valid := fun (as : List (β × σ)) (i : ℕ) ↦ i < as.length) (graph b (m b + 1)) 0) =
    some (f b)

Tactic:
simp [graph_eq_map_bindList (m b + 1) (Nat.le_refl _), bindList]

Premises used: Nat.le_refl, HAdd.hAdd, OfNat.ofNat
-- 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)
⊢ Primrec f

Tactic:
exact option_some_iff.mp <| this.of_eq <| fun b ↦ by
    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
    simp [graph_eq_map_bindList (m b + 1) (Nat.le_refl _), bindList]

Premises used: Primrec.of_eq, Primrec.option_some_iff, Iff.mp
-- Module: Mathlib.Computability.Primrec.List
Goal:
α : Type u_1
β : Type u_2
σ : Type u_4
inst : Primcodable α
inst_1 : Primcodable β
inst_2 : Primcodable σ
f : α → β → σ
m : α → β → ℕ
l : α → β → List β
g : α → Prod.{u_2, u_4} β (List σ) → Option σ
hm : Primrec₂ m
hl : Primrec₂ l
hg : Primrec₂ g
Ord : ∀ (a : α) (b b' : β), b' ∈ l a b → m a b' < m a b
H : ∀ (a : α) (b : β), g a (b, List.map (f a) (l a b)) = some (f a b)
⊢ ∀ (b b' : α × β),
    Membership.mem (γ := List (α × β)) (List.map (fun (b_1 : β) ↦ (b.1, b_1)) (l b.1 b.2)) b' →
      uncurry m b' < uncurry m b

Tactic:
simpa using Ord
-- Module: Mathlib.Computability.Primrec.List
Goal:
α : Type u_1
β : Type u_2
σ : Type u_4
inst : Primcodable α
inst_1 : Primcodable β
inst_2 : Primcodable σ
f : α → β → σ
m : α → β → ℕ
l : α → β → List β
g : α → Prod.{u_2, u_4} β (List σ) → Option σ
hm : Primrec₂ m
hl : Primrec₂ l
hg : Primrec₂ g
Ord : ∀ (a : α) (b b' : β), b' ∈ l a b → m a b' < m a b
H : ∀ (a : α) (b : β), g a (b, List.map (f a) (l a b)) = some (f a b)
⊢ ∀ (b : α × β),
    g b.1 (b.2, List.map (uncurry f) (List.map (fun (b_1 : β) ↦ (b.1, b_1)) (l b.1 b.2))) = some (uncurry f b)

Tactic:
simpa [Function.comp] using H

Premises used: Function.comp
-- Module: Mathlib.Computability.Primrec.List
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
rw₁ rw₂ :
  (List.drop ((n, l).2.length - (n, l).1) (n, l).2.reverse).reverse = (List.drop (l.length - 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

Tactic:
rw [← List.reverse_reverse (l.take n), List.reverse_take]

Premises used: List.reverse_take, List.reverse_reverse, List.take
-- Module: Mathlib.Computability.Primrec.List
Goal:
α : Type u_1
inst : Primcodable α
p : α → Bool
hp : Primrec p
⊢ Primrec (List.takeWhile p)

Tactic:
(list_take.comp (list_findIdx Primrec.id (Primrec.not.comp (hp.comp snd)).to₂)
    Primrec.id).of_eq fun _ => List.takeWhile_eq_take_findIdx_not.symm

Premises used: Primrec.of_eq, Primrec.snd, Primrec.comp, List.takeWhile_eq_take_findIdx_not, Primrec.not, Primrec.list_take, Primrec₂.comp, Eq.symm, Primrec.id, Primrec.to₂, Primrec.list_findIdx
-- Module: Mathlib.Computability.Primrec.List
Goal:
α : Type u_1
inst : Primcodable α
p : α → Bool
hp : Primrec p
⊢ Primrec (List.dropWhile p)

Tactic:
(list_drop.comp (list_findIdx Primrec.id (Primrec.not.comp (hp.comp snd)).to₂)
    Primrec.id).of_eq fun _ => List.dropWhile_eq_drop_findIdx_not.symm

Premises used: Primrec.of_eq, Primrec.snd, Primrec.list_drop, List.dropWhile_eq_drop_findIdx_not, Primrec.comp, Primrec.not, Primrec₂.comp, Eq.symm, Primrec.id, Primrec.to₂, Primrec.list_findIdx
-- Module: Mathlib.Computability.Primrec.List
Goal:
α : Type u_1
β : Type u_2
inst : Primcodable α
inst_1 : Primcodable β
g : β → α → α
hg : Primrec₂ g
l : List α
b : β
nil :
  (List.casesOn (motive := fun (x : List α) ↦ List α) ([], b).1 [] fun (b_1 : α) (l : List α) ↦
      g (([], b), b_1, l).1.2 (([], b), b_1, l).2.1 :: (([], b), b_1, l).2.2) =
    List.modifyHead (g b) []
cons :
  ∀ (head : α) (tail : List α),
    (List.casesOn (motive := fun (x : List α) ↦ List α) (head :: tail, b).1 [] fun (b_1 : α) (l : List α) ↦
        g ((head :: tail, b), b_1, l).1.2 ((head :: tail, b), b_1, l).2.1 :: ((head :: tail, b), b_1, l).2.2) =
      List.modifyHead (g b) (head :: tail)
⊢ (List.casesOn (motive := fun (x : List α) ↦ List α) (l, b).1 [] fun (b_1 : α) (l_1 : List α) ↦
      g ((l, b), b_1, l_1).1.2 ((l, b), b_1, l_1).2.1 :: ((l, b), b_1, l_1).2.2) =
    List.modifyHead (g b) l

Tactic:
cases l
-- Module: Mathlib.Computability.Primrec.List
Goal:
α : Type u_1
β : Type u_2
inst : Primcodable α
inst_1 : Primcodable β
g : β → α → α
hg : Primrec₂ g
b : β
⊢ (List.casesOn (motive := fun (x : List α) ↦ List α) ([], b).1 [] fun (b_1 : α) (l : List α) ↦
      g (([], b), b_1, l).1.2 (([], b), b_1, l).2.1 :: (([], b), b_1, l).2.2) =
    List.modifyHead (g b) []

Tactic:
rfl
-- Module: Mathlib.Computability.Primrec.List
Goal:
α : Type u_1
β : Type u_2
inst : Primcodable α
inst_1 : Primcodable β
g : β → α → α
hg : Primrec₂ g
b : β
head : α
tail : List α
⊢ (List.casesOn (motive := fun (x : List α) ↦ List α) (head :: tail, b).1 [] fun (b_1 : α) (l : List α) ↦
      g ((head :: tail, b), b_1, l).1.2 ((head :: tail, b), b_1, l).2.1 :: ((head :: tail, b), b_1, l).2.2) =
    List.modifyHead (g b) (head :: tail)

Tactic:
rfl
-- Module: Mathlib.Computability.Primrec.List
Goal:
α : Type u_1
inst : Primcodable α
f : α → α
hf : Primrec f
⊢ Primrec (List.modifyHead f)

Tactic:
(list_modifyHead' (hf.comp snd).to₂).comp Primrec.id (const ())

Premises used: Unit.unit, Primrec.snd, Primrec.const, Primrec.list_modifyHead', Primrec.comp, Primrec₂.comp, Primrec.id, Primrec.to₂
-- Module: Mathlib.Computability.Primrec.List
Goal:
α : Type u_1
β : Type u_2
inst : Primcodable α
inst_1 : Primcodable β
g : β → α → α
hg : Primrec₂ g
⊢ Primrec₂ (σ := List α) fun (l : List α) (p : ℕ × β) ↦ l.modify p.1 (g p.2)

Tactic:
(list_append.comp
    (list_take.comp (fst.comp snd) fst)
    ((list_modifyHead' hg).comp (list_drop.comp (fst.comp snd) fst) (snd.comp snd))).to₂.of_eq
  fun l ⟨n, b⟩ => (List.modify_eq_take_drop (g b) l n).symm

Premises used: Primrec.snd, List.modify, Primrec.fst, Prod.mk, List.modify_eq_take_drop, Prod.fst, Primrec.list_drop, List.drop, Primrec.list_modifyHead', Primrec.comp, List.modifyHead, Primrec.list_take, Primrec₂.comp, Eq.symm, Primrec₂.of_eq, Eq, Prod.snd, List.take, HAppend.hAppend, Primrec.to₂, _private.0.Primrec.list_modify'.match_1, Primrec.list_append
-- Module: Mathlib.Computability.Primrec.List
Goal:
α : Type u_1
inst : Primcodable α
f : α → α
hf : Primrec f
⊢ Primrec₂ (σ := List α) fun (l : List α) (n : ℕ) ↦ l.modify n f

Tactic:
((list_modify' (hf.comp snd).to₂).comp fst (pair snd (const ()))).to₂

Premises used: Unit.unit, Primrec.snd, Primrec.list_modify', Primrec.fst, Primrec.pair, Primrec.const, Primrec.comp, Primrec₂.comp, Primrec.to₂
-- Module: Mathlib.Computability.Primrec.List
Goal:
α : Type u_1
inst : Primcodable α
⊢ Primrec₂ (σ := List α) fun (l : List α) (p : ℕ × α) ↦ l.set p.1 p.2

Tactic:
(list_modify' fst.to₂).of_eq fun l ⟨n, v⟩ => (List.set_eq_modify v n l).symm

Premises used: List.set_eq_modify, Primrec.list_modify', List.modify, Primrec.fst, List.set, Prod.mk, Prod.fst, Eq.symm, Primrec₂.of_eq, Eq, Prod.snd, Primrec.to₂, _private.0.Primrec.list_modify'.match_1
-- Module: Mathlib.Computability.Primrec.List
Goal:
α : Type u_1
p : α → Prop
inst : Primcodable α
w : DecidablePred p
hf : Primrec (β := Bool) fun (a : α) ↦ decide (p a)
⊢ ∀ (a : List α), ¬(filter (fun (x : α) ↦ decide (p x)) a).length = 0 ↔ ∃ a_1 ∈ a, p a_1

Tactic:
simp
-- Module: Mathlib.Computability.Primrec.List
Goal:
α : Type u_1
p : α → Prop
inst : Primcodable α
w : DecidablePred p
hf : Primrec (β := Bool) fun (a : α) ↦ decide (p a)
⊢ ∀ (a : List α), (filter (fun (x : α) ↦ decide (p x)) a).length = a.length ↔ ∀ a_1 ∈ a, p a_1

Tactic:
simp
-- Module: Mathlib.Computability.Primrec.List
Goal:
p : ℕ → Prop
hf : PrimrecPred p
⊢ ∀ (a : ℕ), (∃ a_1 ∈ range a, p a_1) ↔ ∃ x < a, p x

Tactic:
simp
-- Module: Mathlib.Computability.Primrec.List
Goal:
p : ℕ → Prop
hf : PrimrecPred p
⊢ ∀ (a : ℕ), (∀ a_1 ∈ range a, p a_1) ↔ ∀ x < a, p x

Tactic:
simp
-- Module: Mathlib.Computability.Primrec.List
Goal:
R : ℕ → ℕ → Prop
s : ℕ
inst : DecidableRel R
hf : PrimrecRel R
simp : Primrec (β := List ℕ) fun (n : ℕ) ↦ filterMap (Option.guard fun (y : ℕ) ↦ decide (R y n)) (range s)
⊢ Primrec (β := List ℕ) fun (n : ℕ) ↦ filter (fun (y : ℕ) ↦ decide (R y n)) (range s)

Tactic:
simp only [← filterMap_eq_filter]

Premises used: List.filterMap_eq_filter
-- Module: Mathlib.Computability.Primrec.List
Goal:
R : ℕ → ℕ → Prop
s : ℕ
inst : DecidableRel R
hf : PrimrecRel R
⊢ Primrec (β := List ℕ) fun (n : ℕ) ↦ filterMap (Option.guard fun (y : ℕ) ↦ decide (R y n)) (range s)

Tactic:
listFilterMap (.const (range s)) ?_

Premises used: List.range, Primrec.const, Primrec.listFilterMap
-- Module: Mathlib.Computability.Primrec.List
Goal:
R : ℕ → ℕ → Prop
s : ℕ
inst : DecidableRel R
hf : PrimrecRel R
refine : Primrec₂ (β := ℕ) (σ := Option ℕ) fun (n : ℕ) ↦ Option.guard fun (y : ℕ) ↦ decide (R y n)
⊢ Primrec (β := List ℕ) fun (n : ℕ) ↦ filterMap (Option.guard fun (y : ℕ) ↦ decide (R y n)) (range s)

Tactic:
refine listFilterMap (.const (range s)) ?_

Premises used: List.range, Primrec.const, Primrec.listFilterMap
-- Module: Mathlib.Computability.Primrec.List
Goal:
R : ℕ → ℕ → Prop
s : ℕ
inst : DecidableRel R
hf : PrimrecRel R
⊢ Primrec₂ (β := ℕ) (σ := Option ℕ) fun (n : ℕ) ↦ Option.guard fun (y : ℕ) ↦ decide (R y n)

Tactic:
ite (Primrec.eq.comp ?_ (const true)) (option_some_iff.mpr snd) (.const Option.none)

Premises used: Iff.mpr, Primrec.snd, Primrec.eq, PrimrecRel.comp, Primrec.const, Bool.true, Option.none, Primrec.option_some_iff, Primrec.ite, Primrec₂
-- Module: Mathlib.Computability.Primrec.List
Goal:
R : ℕ → ℕ → Prop
s : ℕ
inst : DecidableRel R
hf : PrimrecRel R
refine : Primrec (β := Bool) fun (p : ℕ × ℕ) ↦ (fun (y : ℕ) ↦ decide (R y p.1)) p.2
⊢ Primrec₂ (β := ℕ) (σ := Option ℕ) fun (n : ℕ) ↦ Option.guard fun (y : ℕ) ↦ decide (R y n)

Tactic:
refine ite (Primrec.eq.comp ?_ (const true)) (option_some_iff.mpr snd) (.const Option.none)

Premises used: Iff.mpr, Primrec.snd, Primrec.eq, PrimrecRel.comp, Primrec.const, Bool.true, Option.none, Primrec.option_some_iff, Primrec.ite
-- Module: Mathlib.Computability.Primrec.List
Goal:
R : ℕ → ℕ → Prop
s : ℕ
inst : DecidableRel R
hf : PrimrecRel R
⊢ Primrec (β := Bool) fun (p : ℕ × ℕ) ↦ (fun (y : ℕ) ↦ decide (R y p.1)) p.2

Tactic:
hf.decide.comp snd fst

Premises used: Primrec.snd, Primrec.fst, Primrec₂.comp, PrimrecRel.decide
-- Module: Mathlib.Computability.Primrec.List
Goal:
R : ℕ → ℕ → Prop
s : ℕ
inst : DecidableRel R
hf : PrimrecRel R
⊢ Primrec (β := Bool) fun (p : ℕ × ℕ) ↦ (fun (y : ℕ) ↦ decide (R y p.1)) p.2

Tactic:
exact hf.decide.comp snd fst

Premises used: Primrec.snd, Primrec.fst, Primrec₂.comp, PrimrecRel.decide
-- Module: Mathlib.Computability.Primrec.List
Goal:
α : Type u_1
β : Type u_2
R : α → β → Prop
inst : Primcodable α
inst_1 : Primcodable β
hf : PrimrecRel R
inst_2 : DecidableRel R
simp : Primrec₂ (σ := List α) fun (L : List α) (b : β) ↦ filterMap (Option.guard fun (a : α) ↦ decide (R a b)) L
⊢ Primrec₂ (σ := List α) fun (L : List α) (b : β) ↦ filter (fun (a : α) ↦ decide (R a b)) L

Tactic:
simp only [← List.filterMap_eq_filter]

Premises used: List.filterMap_eq_filter
-- Module: Mathlib.Computability.Primrec.List
Goal:
α : Type u_1
β : Type u_2
R : α → β → Prop
inst : Primcodable α
inst_1 : Primcodable β
hf : PrimrecRel R
inst_2 : DecidableRel R
⊢ Primrec₂ (σ := List α) fun (L : List α) (b : β) ↦ filterMap (Option.guard fun (a : α) ↦ decide (R a b)) L

Tactic:
listFilterMap fst (Primrec.ite ?_ ?_ (Primrec.const Option.none))

Premises used: Primrec.fst, Primrec.const, Option.none, Primrec.ite, Primrec.listFilterMap, Primrec₂
-- Module: Mathlib.Computability.Primrec.List
Goal:
α : Type u_1
β : Type u_2
R : α → β → Prop
inst : Primcodable α
inst_1 : Primcodable β
hf : PrimrecRel R
inst_2 : DecidableRel R
refine_1 : PrimrecPred fun (p : Prod.{u_1, u_2} (List α) β × α) ↦ (fun (a : α) ↦ decide (R a p.1.2)) p.2 = true
refine_2 : Primrec (β := Option α) fun (p : Prod.{u_1, u_2} (List α) β × α) ↦ some p.2
⊢ Primrec₂ (σ := List α) fun (L : List α) (b : β) ↦ filterMap (Option.guard fun (a : α) ↦ decide (R a b)) L

Tactic:
refine listFilterMap fst (Primrec.ite ?_ ?_ (Primrec.const Option.none))
-- Module: Mathlib.Computability.Primrec.List
Goal:
α : Type u_1
β : Type u_2
R : α → β → Prop
inst : Primcodable α
inst_1 : Primcodable β
hf : PrimrecRel R
inst_2 : DecidableRel R
⊢ PrimrecPred fun (p : Prod.{u_1, u_2} (List α) β × α) ↦ (fun (a : α) ↦ decide (R a p.1.2)) p.2 = true

Tactic:
Primrec.eq.comp (hf.decide.comp snd (snd.comp fst)) (.const true)

Premises used: Primrec.snd, Primrec.fst, Primrec.eq, PrimrecRel.comp, Primrec.const, Bool.true, Primrec.comp, Primrec₂.comp, PrimrecRel.decide
-- Module: Mathlib.Computability.Primrec.List
Goal:
α : Type u_1
β : Type u_2
R : α → β → Prop
inst : Primcodable α
inst_1 : Primcodable β
hf : PrimrecRel R
inst_2 : DecidableRel R
⊢ PrimrecPred fun (p : Prod.{u_1, u_2} (List α) β × α) ↦ (fun (a : α) ↦ decide (R a p.1.2)) p.2 = true

Tactic:
exact Primrec.eq.comp (hf.decide.comp snd (snd.comp fst)) (.const true)

Premises used: Primrec.snd, Primrec.fst, Primrec.eq, PrimrecRel.comp, Primrec.const, Bool.true, Primrec.comp, Primrec₂.comp, PrimrecRel.decide
-- Module: Mathlib.Computability.Primrec.List
Goal:
α : Type u_1
β : Type u_2
R : α → β → Prop
inst : Primcodable α
inst_1 : Primcodable β
hf : PrimrecRel R
inst_2 : DecidableRel R
⊢ Primrec (β := Option α) fun (p : Prod.{u_1, u_2} (List α) β × α) ↦ some p.2

Tactic:
option_some.comp snd

Premises used: Primrec.snd, Primrec.option_some, Primrec.comp
-- Module: Mathlib.Computability.Primrec.List
Goal:
α : Type u_1
β : Type u_2
R : α → β → Prop
inst : Primcodable α
inst_1 : Primcodable β
hf : PrimrecRel R
inst_2 : DecidableRel R
⊢ Primrec (β := Option α) fun (p : Prod.{u_1, u_2} (List α) β × α) ↦ some p.2

Tactic:
exact option_some.comp snd

Premises used: Primrec.snd, Primrec.option_some, Primrec.comp
-- Module: Mathlib.Computability.Primrec.List
Goal:
α : Type u_1
β : Type u_2
R : α → β → Prop
inst : Primcodable α
inst_1 : Primcodable β
hf : PrimrecRel R
L : List α
b : β
⊢ (filter (fun (x : α) ↦ decide (R x b)) L).length ≠ 0 ↔ ∃ a ∈ L, R a b

Tactic:
simp
-- Module: Mathlib.Computability.Primrec.List
Goal:
α : Type u_1
β : Type u_2
R : α → β → Prop
inst : Primcodable α
inst_1 : Primcodable β
hf : PrimrecRel R
⊢ ∀ (L : List α) (b : β), (filter (fun (x : α) ↦ decide (R x b)) L).length ≠ 0 ↔ ∃ a ∈ L, R a b

Tactic:
have h (L) (b) : (List.filter (R · b) L).length ≠ 0 ↔ ∃ a ∈ L, R a b := by simp
-- Module: Mathlib.Computability.Primrec.List
Goal:
α : Type u_1
β : Type u_2
R : α → β → Prop
inst : Primcodable α
inst_1 : Primcodable β
hf : PrimrecRel R
h : ∀ (L : List α) (b : β), (filter (fun (x : α) ↦ decide (R x b)) L).length ≠ 0 ↔ ∃ a ∈ L, R a b
⊢ PrimrecRel fun (L : List α) (b : β) ↦ ∃ a ∈ L, R a b

Tactic:
.of_eq (.not ?_) h

Premises used: PrimrecRel.not, PrimrecRel.of_eq
-- Module: Mathlib.Computability.Primrec.List
Goal:
α : Type u_1
β : Type u_2
R : α → β → Prop
inst : Primcodable α
inst_1 : Primcodable β
hf : PrimrecRel R
h : ∀ (L : List α) (b : β), (filter (fun (x : α) ↦ decide (R x b)) L).length ≠ 0 ↔ ∃ a ∈ L, R a b
refine : PrimrecRel fun (a : List α) (b : β) ↦ (filter (fun (x : α) ↦ decide (R x b)) a).length = 0
⊢ PrimrecRel fun (L : List α) (b : β) ↦ ∃ a ∈ L, R a b

Tactic:
refine .of_eq (.not ?_) h
-- Module: Mathlib.Computability.Primrec.List
Goal:
α : Type u_1
β : Type u_2
R : α → β → Prop
inst : Primcodable α
inst_1 : Primcodable β
hf : PrimrecRel R
h : ∀ (L : List α) (b : β), (filter (fun (x : α) ↦ decide (R x b)) L).length ≠ 0 ↔ ∃ a ∈ L, R a b
⊢ PrimrecRel fun (a : List α) (b : β) ↦ (filter (fun (x : α) ↦ decide (R x b)) a).length = 0

Tactic:
Primrec.eq.comp (list_length.comp hf.listFilter) (const 0)

Premises used: PrimrecRel, Primrec.list_length, PrimrecRel.listFilter, Primrec.eq, PrimrecRel.comp, Primrec.const, Primrec.comp, OfNat.ofNat
-- Module: Mathlib.Computability.Primrec.List
Goal:
α : Type u_1
β : Type u_2
R : α → β → Prop
inst : Primcodable α
inst_1 : Primcodable β
hf : PrimrecRel R
h : ∀ (L : List α) (b : β), (filter (fun (x : α) ↦ decide (R x b)) L).length ≠ 0 ↔ ∃ a ∈ L, R a b
⊢ PrimrecRel fun (a : List α) (b : β) ↦ (filter (fun (x : α) ↦ decide (R x b)) a).length = 0

Tactic:
exact Primrec.eq.comp (list_length.comp hf.listFilter) (const 0)

Premises used: Primrec.list_length, PrimrecRel.listFilter, Primrec.eq, PrimrecRel.comp, Primrec.const, Primrec.comp, OfNat.ofNat