awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Computability.Partrec
Goal:
α : Type u_1
σ : Type u_4
inst : Primcodable α
inst_1 : Primcodable σ
f : α →. σ ⊕ α
hf : Partrec f
F : α → ℕ →. σ ⊕ α :=
  fun (a : α) (n : ℕ) ↦
    Nat.rec (motive := fun (x : ℕ) ↦ Part (σ ⊕ α)) (Part.some (Sum.inr a))
      (fun (x : ℕ) (IH : Part (σ ⊕ α)) ↦
        IH.bind fun (s : σ ⊕ α) ↦
          Sum.casesOn (motive := fun (x : σ ⊕ α) ↦ Part (σ ⊕ α)) s (fun (x : σ) ↦ Part.some s) f)
      n
⊢ Partrec₂ F

Tactic:
have hF : Partrec₂ F :=
    Partrec.nat_rec snd (sumInr.comp fst).partrec
      (sumCasesOn_right (snd.comp snd) (snd.comp <| snd.comp fst).to₂ (hf.comp snd).to₂).to₂
-- Module: Mathlib.Computability.Partrec
Goal:
α : Type u_1
σ : Type u_4
inst : Primcodable α
inst_1 : Primcodable σ
f : α →. σ ⊕ α
hf : Partrec f
F : α → ℕ →. σ ⊕ α :=
  fun (a : α) (n : ℕ) ↦
    Nat.rec (motive := fun (x : ℕ) ↦ Part (σ ⊕ α)) (Part.some (Sum.inr a))
      (fun (x : ℕ) (IH : Part (σ ⊕ α)) ↦
        IH.bind fun (s : σ ⊕ α) ↦
          Sum.casesOn (motive := fun (x : σ ⊕ α) ↦ Part (σ ⊕ α)) s (fun (x : σ) ↦ Part.some s) f)
      n
hF : Partrec₂ F
p : (a : α) → (n : ℕ) → Part Bool :=
  fun (a : α) (n : ℕ) ↦
    Part.map
      (fun (s : σ ⊕ α) ↦ Sum.casesOn (motive := fun (x : σ ⊕ α) ↦ Bool) s (fun (x : σ) ↦ true) fun (x : α) ↦ false)
      (F a n)
⊢ Partrec₂ p

Tactic:
have hp : Partrec₂ p :=
    hF.map ((sumCasesOn Computable.id (const true).to₂ (const false).to₂).comp snd).to₂
-- Module: Mathlib.Computability.Partrec
Goal:
α : Type u_1
σ : Type u_4
inst : Primcodable α
inst_1 : Primcodable σ
f : α →. σ ⊕ α
hf : Partrec f
F : α → ℕ →. σ ⊕ α :=
  fun (a : α) (n : ℕ) ↦
    Nat.rec (motive := fun (x : ℕ) ↦ Part (σ ⊕ α)) (Part.some (Sum.inr a))
      (fun (x : ℕ) (IH : Part (σ ⊕ α)) ↦
        IH.bind fun (s : σ ⊕ α) ↦
          Sum.casesOn (motive := fun (x : σ ⊕ α) ↦ Part (σ ⊕ α)) s (fun (x : σ) ↦ Part.some s) f)
      n
hF : Partrec₂ F
p : (a : α) → (n : ℕ) → Part Bool :=
  fun (a : α) (n : ℕ) ↦
    Part.map
      (fun (s : σ ⊕ α) ↦ Sum.casesOn (motive := fun (x : σ ⊕ α) ↦ Bool) s (fun (x : σ) ↦ true) fun (x : α) ↦ false)
      (F a n)
hp : Partrec₂ p
a : α
b : σ
⊢ Membership.mem (γ := Part σ)
      ((Nat.rfind (p a)).bind fun (b : ℕ) ↦
        (F (a, b).1 (a, b).2).bind fun (b_1 : σ ⊕ α) ↦
          Sum.casesOn (motive := fun (x : σ ⊕ α) ↦ Part σ) ((a, b), b_1).2
            (fun (b_2 : σ) ↦ Part.some (((a, b), b_1), b_2).2) fun (b : α) ↦ Part.none)
      b ↔
    b ∈ f.fix a

Tactic:
simpa [p] using fix_aux f _ _

Premises used: Partrec.fix_aux
-- Module: Mathlib.Computability.Partrec
Goal:
α : Type u_1
σ : Type u_4
inst : Primcodable α
inst_1 : Primcodable σ
f : α →. σ ⊕ α
hf : Partrec f
F : α → ℕ →. σ ⊕ α :=
  fun (a : α) (n : ℕ) ↦
    Nat.rec (motive := fun (x : ℕ) ↦ Part (σ ⊕ α)) (Part.some (Sum.inr a))
      (fun (x : ℕ) (IH : Part (σ ⊕ α)) ↦
        IH.bind fun (s : σ ⊕ α) ↦
          Sum.casesOn (motive := fun (x : σ ⊕ α) ↦ Part (σ ⊕ α)) s (fun (x : σ) ↦ Part.some s) f)
      n
hF : Partrec₂ F
p : (a : α) → (n : ℕ) → Part Bool :=
  fun (a : α) (n : ℕ) ↦
    Part.map
      (fun (s : σ ⊕ α) ↦ Sum.casesOn (motive := fun (x : σ ⊕ α) ↦ Bool) s (fun (x : σ) ↦ true) fun (x : α) ↦ false)
      (F a n)
hp : Partrec₂ p
⊢ Partrec f.fix

Tactic:
exact ((Partrec.rfind hp).bind (hF.bind (sumCasesOn_right snd snd.to₂ none.to₂).to₂).to₂).of_eq
    fun a => ext fun b => by simpa [p] using fix_aux f _ _

Premises used: Partrec.sumCasesOn_right, Partrec.bind, Computable.snd, Part.ext, Partrec.to₂, Partrec.none, Partrec.of_eq, Partrec.rfind, Computable.to₂
-- Module: Mathlib.Computability.PartrecBasis
Goal:
n : ℕ
f : List.Vector ℕ n →. ℕ
n_1 : ℕ
f_1 : List.Vector ℕ n_1 → ℕ
hf : Primrec' f_1
⊢ Partrec (↑f_1 : List.Vector ℕ n_1 →. ℕ)

Tactic:
hf.to_prim.to_comp

Premises used: Primrec.to_comp, Nat.Primrec'.to_prim, Computable
-- Module: Mathlib.Computability.PartrecBasis
Goal:
n : ℕ
f : List.Vector ℕ n →. ℕ
n_1 : ℕ
f_1 : List.Vector ℕ n_1 → ℕ
hf : Primrec' f_1
⊢ Partrec (↑f_1 : List.Vector ℕ n_1 →. ℕ)

Tactic:
exact hf.to_prim.to_comp

Premises used: Primrec.to_comp, Nat.Primrec'.to_prim
-- Module: Mathlib.Computability.PartrecBasis
Goal:
n : ℕ
f : List.Vector ℕ n →. ℕ
m n_1 : ℕ
f_1 : List.Vector ℕ n_1 →. ℕ
g : Fin n_1 → List.Vector ℕ m →. ℕ
h : Partrec' f_1
h_1 : ∀ (i : Fin n_1), Partrec' (g i)
hf : Partrec f_1
hg : ∀ (i : Fin n_1), Partrec (g i)
⊢ Partrec (α := List.Vector ℕ m) (σ := ℕ) fun (v : List.Vector ℕ m) ↦ (mOfFn fun (i : Fin n_1) ↦ g i v) >>= f_1

Tactic:
(Partrec.vector_mOfFn hg).bind (hf.comp snd)

Premises used: Partrec.bind, Partrec.vector_mOfFn, Computable.snd, Partrec.comp
-- Module: Mathlib.Computability.PartrecBasis
Goal:
n : ℕ
f : List.Vector ℕ n →. ℕ
m n_1 : ℕ
f_1 : List.Vector ℕ n_1 →. ℕ
g : Fin n_1 → List.Vector ℕ m →. ℕ
h : Partrec' f_1
h_1 : ∀ (i : Fin n_1), Partrec' (g i)
hf : Partrec f_1
hg : ∀ (i : Fin n_1), Partrec (g i)
⊢ Partrec (α := List.Vector ℕ m) (σ := ℕ) fun (v : List.Vector ℕ m) ↦ (mOfFn fun (i : Fin n_1) ↦ g i v) >>= f_1

Tactic:
exact (Partrec.vector_mOfFn hg).bind (hf.comp snd)
-- Module: Mathlib.Computability.PartrecBasis
Goal:
n : ℕ
f : List.Vector ℕ n →. ℕ
n_1 : ℕ
f_1 : List.Vector ℕ (n_1 + 1) → ℕ
h : Partrec' (↑f_1 : List.Vector ℕ (n_1 + 1) →. ℕ)
hf : Partrec (↑f_1 : List.Vector ℕ (n_1 + 1) →. ℕ)
⊢ Partrec (α := List.Vector ℕ n_1 × ℕ) (σ := ℕ) fun (a : List.Vector ℕ n_1 × ℕ) ↦
    (↑f_1 : List.Vector ℕ (n_1 + 1) →. ℕ) (a.2 ::ᵥ a.1)

Tactic:
have := hf.comp (vector_cons.comp snd fst)
-- Module: Mathlib.Computability.PartrecBasis
Goal:
n : ℕ
f : List.Vector ℕ n →. ℕ
n_1 : ℕ
f_1 : List.Vector ℕ (n_1 + 1) → ℕ
h : Partrec' (↑f_1 : List.Vector ℕ (n_1 + 1) →. ℕ)
hf : Partrec (↑f_1 : List.Vector ℕ (n_1 + 1) →. ℕ)
this :
  Partrec (α := List.Vector ℕ n_1 × ℕ) (σ := ℕ) fun (a : List.Vector ℕ n_1 × ℕ) ↦
    (↑f_1 : List.Vector ℕ (n_1 + 1) →. ℕ) (a.2 ::ᵥ a.1)
⊢ Partrec₂ (β := ℕ) (σ := Bool) fun (a : List.Vector ℕ n_1) ↦
    (↑fun (b : ℕ) ↦ decide (id (f_1 ((a, b).2 ::ᵥ (a, b).1)) = 0) : ℕ →. Bool)

Tactic:
have :=
      ((Primrec.eq.decide.comp _root_.Primrec.id (_root_.Primrec.const 0)).to_comp.comp
        this).to₂.partrec₂
-- Module: Mathlib.Computability.PartrecBasis
Goal:
n : ℕ
f : List.Vector ℕ n →. ℕ
n_1 : ℕ
f_1 : List.Vector ℕ (n_1 + 1) → ℕ
h : Partrec' (↑f_1 : List.Vector ℕ (n_1 + 1) →. ℕ)
hf : Partrec (↑f_1 : List.Vector ℕ (n_1 + 1) →. ℕ)
this_1 :
  Partrec (α := List.Vector ℕ n_1 × ℕ) (σ := ℕ) fun (a : List.Vector ℕ n_1 × ℕ) ↦
    (↑f_1 : List.Vector ℕ (n_1 + 1) →. ℕ) (a.2 ::ᵥ a.1)
this :
  Partrec₂ (β := ℕ) (σ := Bool) fun (a : List.Vector ℕ n_1) ↦
    (↑fun (b : ℕ) ↦ decide (id (f_1 ((a, b).2 ::ᵥ (a, b).1)) = 0) : ℕ →. Bool)
⊢ Partrec (α := List.Vector ℕ n_1) (σ := ℕ) fun (v : List.Vector ℕ n_1) ↦
    Nat.rfind fun (n : ℕ) ↦ Part.some (decide (f_1 (n ::ᵥ v) = 0))

Tactic:
_root_.Partrec.rfind this

Premises used: Partrec.rfind
-- Module: Mathlib.Computability.PartrecBasis
Goal:
n : ℕ
f : List.Vector ℕ n →. ℕ
n_1 : ℕ
f_1 : List.Vector ℕ (n_1 + 1) → ℕ
h : Partrec' (↑f_1 : List.Vector ℕ (n_1 + 1) →. ℕ)
hf : Partrec (↑f_1 : List.Vector ℕ (n_1 + 1) →. ℕ)
this_1 :
  Partrec (α := List.Vector ℕ n_1 × ℕ) (σ := ℕ) fun (a : List.Vector ℕ n_1 × ℕ) ↦
    (↑f_1 : List.Vector ℕ (n_1 + 1) →. ℕ) (a.2 ::ᵥ a.1)
this :
  Partrec₂ (β := ℕ) (σ := Bool) fun (a : List.Vector ℕ n_1) ↦
    (↑fun (b : ℕ) ↦ decide (id (f_1 ((a, b).2 ::ᵥ (a, b).1)) = 0) : ℕ →. Bool)
⊢ Partrec (α := List.Vector ℕ n_1) (σ := ℕ) fun (v : List.Vector ℕ n_1) ↦
    Nat.rfind fun (n : ℕ) ↦ Part.some (decide (f_1 (n ::ᵥ v) = 0))

Tactic:
exact _root_.Partrec.rfind this

Premises used: Partrec.rfind
-- Module: Mathlib.Computability.PartrecBasis
Goal:
n : ℕ
f : List.Vector ℕ n →. ℕ
pf : Partrec' f
prim : ∀ {n : ℕ} {f : List.Vector ℕ n → ℕ} (hf : Primrec' f), Partrec (↑f : List.Vector ℕ n →. ℕ)
comp :
  ∀ {m n : ℕ} {f : List.Vector ℕ n →. ℕ} (g : Fin n → List.Vector ℕ m →. ℕ),
    Partrec' f →
      (∀ (i : Fin n), Partrec' (g i)) →
        ∀ (hf : Partrec f) (hg : ∀ (i : Fin n), Partrec (g i)),
          Partrec (α := List.Vector ℕ m) (σ := ℕ) fun (v : List.Vector ℕ m) ↦ (mOfFn fun (i : Fin n) ↦ g i v) >>= f
rfind :
  ∀ {n : ℕ} {f : List.Vector ℕ (n + 1) → ℕ},
    Partrec' (↑f : List.Vector ℕ (n + 1) →. ℕ) →
      ∀ (hf : Partrec (↑f : List.Vector ℕ (n + 1) →. ℕ)),
        Partrec (α := List.Vector ℕ n) (σ := ℕ) fun (v : List.Vector ℕ n) ↦
          Nat.rfind fun (n_1 : ℕ) ↦ Part.some (decide (f (n_1 ::ᵥ v) = 0))
⊢ Partrec f

Tactic:
induction pf with
  | prim hf => exact hf.to_prim.to_comp
  | comp _ _ _ hf hg => exact (Partrec.vector_mOfFn hg).bind (hf.comp snd)
  | rfind _ hf =>
    have := hf.comp (vector_cons.comp snd fst)
    have :=
      ((Primrec.eq.decide.comp _root_.Primrec.id (_root_.Primrec.const 0)).to_comp.comp
        this).to₂.partrec₂
    exact _root_.Partrec.rfind this

Premises used: Nat.Partrec'.comp, Nat.Partrec'.prim, Nat.Partrec'.rfind
-- Module: Mathlib.Computability.PartrecBasis
Goal:
n : ℕ
f g : List.Vector ℕ n →. ℕ
hf : Partrec' f
H : ∀ (i : List.Vector ℕ n), f i = g i
⊢ Partrec' g

Tactic:
(funext H : f = g) ▸ hf

Premises used: Eq.rec, funext
-- Module: Mathlib.Computability.PartrecBasis
Goal:
n : ℕ
f : List.Vector ℕ n → ℕ
hf : Primrec f
⊢ Partrec' (↑f : List.Vector ℕ n →. ℕ)

Tactic:
prim (Nat.Primrec'.of_prim hf)

Premises used: Nat.Primrec'.of_prim, Nat.Partrec'.prim
-- Module: Mathlib.Computability.PartrecBasis
Goal:
n : ℕ
⊢ Partrec' (n := n.succ) (↑List.Vector.head : List.Vector ℕ n.succ →. ℕ)

Tactic:
prim Nat.Primrec'.head

Premises used: Nat.Primrec'.head, Nat.Partrec'.prim
-- Module: Mathlib.Computability.PartrecBasis
Goal:
n : ℕ
f : List.Vector ℕ n →. ℕ
hf : Partrec' f
v : List.Vector ℕ (n + 1)
rw :
  (mOfFn fun (i : Fin n) ↦ (↑fun (v : List.Vector ℕ (n + 1)) ↦ v.get i.succ : List.Vector ℕ (n + 1) →. ℕ) v) >>= f =
    f (ofFn fun (x : Fin n) ↦ v.get x.succ)
⊢ (mOfFn fun (i : Fin n) ↦ (↑fun (v : List.Vector ℕ (n + 1)) ↦ v.get i.succ : List.Vector ℕ (n + 1) →. ℕ) v) >>= f =
    f v.tail

Tactic:
rw [← ofFn_get v.tail, funext (get_tail_succ v)]

Premises used: List.Vector.get_tail_succ, List.Vector.ofFn_get, funext, List.Vector.tail
-- Module: Mathlib.Computability.PartrecBasis
Goal:
n : ℕ
f : List.Vector ℕ n →. ℕ
hf : Partrec' f
v : List.Vector ℕ (n + 1)
⊢ (mOfFn fun (i : Fin n) ↦ (↑fun (v : List.Vector ℕ (n + 1)) ↦ v.get i.succ : List.Vector ℕ (n + 1) →. ℕ) v) >>= f =
    f (ofFn fun (x : Fin n) ↦ v.get x.succ)

Tactic:
simp
-- Module: Mathlib.Computability.PartrecBasis
Goal:
n : ℕ
f : List.Vector ℕ n →. ℕ
g : List.Vector ℕ (n + 1) →. ℕ
hf : Partrec' f
hg : Partrec' g
⊢ Partrec' (n := n)
    ((fun (i : Fin (n + 1)) ↦
        (Fin.cases (motive := fun (x : Fin (n + 1)) ↦ List.Vector ℕ n →. ℕ) f
            (fun (i : Fin n) (v : List.Vector ℕ n) ↦ (↑(some (v.get i)) : Part ℕ)) i :
          List.Vector ℕ n →. ℕ))
      0)

Tactic:
simpa using hf
-- Module: Mathlib.Computability.PartrecBasis
Goal:
n : ℕ
f : List.Vector ℕ n →. ℕ
g : List.Vector ℕ (n + 1) →. ℕ
hf : Partrec' f
hg : Partrec' g
i : Fin n
⊢ Partrec' (n := n)
    ((fun (i : Fin (n + 1)) ↦
        (Fin.cases (motive := fun (x : Fin (n + 1)) ↦ List.Vector ℕ n →. ℕ) f
            (fun (i : Fin n) (v : List.Vector ℕ n) ↦ (↑(some (v.get i)) : Part ℕ)) i :
          List.Vector ℕ n →. ℕ))
      i.succ)

Tactic:
simpa using prim (Nat.Primrec'.get i)

Premises used: Nat.Primrec'.get, Nat.Partrec'.prim
-- Module: Mathlib.Computability.PartrecBasis
Goal:
n : ℕ
f : List.Vector ℕ n →. ℕ
g : List.Vector ℕ (n + 1) →. ℕ
hf : Partrec' f
hg : Partrec' g
v : List.Vector ℕ n
⊢ (mOfFn fun (i : Fin (n + 1)) ↦
        Fin.cases (motive := fun (x : Fin (n + 1)) ↦ List.Vector ℕ n →. ℕ) f
          (fun (i : Fin n) (v : List.Vector ℕ n) ↦ (↑(some (v.get i)) : Part ℕ)) i v) >>=
      g =
    (f v).bind fun (a : ℕ) ↦ g (a ::ᵥ v)

Tactic:
simp [mOfFn, Part.bind_assoc, pure]

Premises used: Pure.pure, Part.bind_assoc, List.Vector.mOfFn
-- Module: Mathlib.Computability.PartrecBasis
Goal:
n : ℕ
f : List.Vector ℕ n →. ℕ
g : List.Vector ℕ (n + 1) → ℕ
hf : Partrec' f
hg : Partrec' (↑g : List.Vector ℕ (n + 1) →. ℕ)
⊢ Partrec' (n := n) fun (v : List.Vector ℕ n) ↦ Part.map (fun (a : ℕ) ↦ g (a ::ᵥ v)) (f v)

Tactic:
simpa [(Part.bind_some_eq_map _ _).symm] using hf.bind hg

Premises used: Part.bind_some_eq_map, Nat.Partrec'.bind, Eq.symm
-- Module: Mathlib.Computability.PartrecBasis
Goal:
n m : ℕ
f : List.Vector ℕ n → List.Vector ℕ m
hf : Primrec'.Vec f
⊢ Vec f

Tactic:
fun i => prim <| hf i

Premises used: Nat.Partrec'.Vec, Nat.Partrec'.prim, Part.ofOption
-- Module: Mathlib.Computability.PartrecBasis
Goal:
n : ℕ
⊢ Vec (n := n) (m := 0) fun (x : List.Vector ℕ n) ↦ nil

Tactic:
fun i => i.elim0

Premises used: Nat.Partrec'.Vec, Fin.elim0
-- Module: Mathlib.Computability.PartrecBasis
Goal:
n m : ℕ
f : List.Vector ℕ n → ℕ
g : List.Vector ℕ n → List.Vector ℕ m
hf : Partrec' (↑f : List.Vector ℕ n →. ℕ)
hg : Vec g
i : Fin m.succ
⊢ Partrec' (n := n) fun (v : List.Vector ℕ n) ↦
    (↑(some (List.Vector.get (n := m.succ) ((fun (v : List.Vector ℕ n) ↦ f v ::ᵥ g v) v) 0)) : Part ℕ)

Tactic:
simpa using hf
-- Module: Mathlib.Computability.PartrecBasis
Goal:
n m : ℕ
f : List.Vector ℕ n → ℕ
g : List.Vector ℕ n → List.Vector ℕ m
hf : Partrec' (↑f : List.Vector ℕ n →. ℕ)
hg : Vec g
i_1 : Fin m.succ
i : Fin m
⊢ Partrec' (n := n) fun (v : List.Vector ℕ n) ↦
    (↑(some (List.Vector.get ((fun (v : List.Vector ℕ n) ↦ f v ::ᵥ g v) v) i.succ)) : Part ℕ)

Tactic:
simp only [hg i, get_cons_succ]

Premises used: List.Vector.get_cons_succ
-- Module: Mathlib.Computability.PartrecBasis
Goal:
n : ℕ
⊢ Vec (n := n) id

Tactic:
Vec.prim Nat.Primrec'.idv

Premises used: Nat.Partrec'.Vec.prim, Nat.Primrec'.idv
-- Module: Mathlib.Computability.PartrecBasis
Goal:
n m : ℕ
f : List.Vector ℕ m →. ℕ
g : List.Vector ℕ n → List.Vector ℕ m
hf : Partrec' f
hg : Vec g
v : List.Vector ℕ n
⊢ (mOfFn fun (i : Fin m) ↦ (↑(some ((g v).get i)) : Part ℕ)) >>= f = f (g v)

Tactic:
simp
-- Module: Mathlib.Computability.PartrecBasis
Goal:
n : ℕ
f : ℕ →. ℕ
g : List.Vector ℕ n → ℕ
hf : Partrec' (n := 1) fun (v : List.Vector ℕ 1) ↦ f v.head
hg : Partrec' (↑g : List.Vector ℕ n →. ℕ)
⊢ Partrec' (n := n) fun (v : List.Vector ℕ n) ↦ f (g v)

Tactic:
simpa using hf.comp' (Partrec'.cons hg Partrec'.nil)

Premises used: Nat.Partrec'.nil, Nat.Partrec'.comp', Nat.Partrec'.cons
-- Module: Mathlib.Computability.PartrecBasis
Goal:
n : ℕ
f : List.Vector ℕ (n + 1) → ℕ
hf : Partrec' (↑f : List.Vector ℕ (n + 1) →. ℕ)
v : List.Vector ℕ n
b : ℕ
simp :
  (∃ a ∈ Nat.rfind fun (n_1 : ℕ) ↦ Part.some (decide (1 ≤ f (n_1 ::ᵥ v))), b = (f (a ::ᵥ v)).pred) ↔
    ∃ a ∈ Nat.rfind fun (n_1 : ℕ) ↦ (↑(some (Option.isSome (α := ℕ) (ofNat (Option ℕ) (f (n_1 ::ᵥ v))))) : Part Bool),
      ofNat (Option ℕ) (f (a ::ᵥ v)) = some b
⊢ Membership.mem (γ := Part ℕ)
      ((Nat.rfind fun (n_1 : ℕ) ↦ Part.some (decide (1 - f (n_1 ::ᵥ v) = 0))).bind fun (a : ℕ) ↦
        (↑pred : ℕ →. ℕ) (f (a ::ᵥ v)))
      b ↔
    Membership.mem (γ := Part ℕ) (Nat.rfindOpt fun (a : ℕ) ↦ ofNat (Option ℕ) (f (a ::ᵥ v))) b

Tactic:
simp only [Nat.rfindOpt, Nat.sub_eq_zero_iff_le, PFun.coe_val, Part.mem_bind_iff,
        Part.mem_some_iff, Option.mem_def, Part.mem_coe]

Premises used: Part.mem_bind_iff, Part.mem_some_iff, PFun.coe_val, Nat.sub_eq_zero_iff_le, Part.mem_coe, Nat.rfindOpt, Option.mem_def
-- Module: Mathlib.Computability.PartrecBasis
Goal:
n : ℕ
f : List.Vector ℕ (n + 1) → ℕ
hf : Partrec' (↑f : List.Vector ℕ (n + 1) →. ℕ)
v : List.Vector ℕ n
b : ℕ
⊢ (∃ a ∈ Nat.rfind fun (n_1 : ℕ) ↦ Part.some (decide (1 ≤ f (n_1 ::ᵥ v))), b = (f (a ::ᵥ v)).pred) ↔
    ∃ a ∈ Nat.rfind fun (n_1 : ℕ) ↦ (↑(some (Option.isSome (α := ℕ) (ofNat (Option ℕ) (f (n_1 ::ᵥ v))))) : Part Bool),
      ofNat (Option ℕ) (f (a ::ᵥ v)) = some b

Tactic:
exists_congr fun a => (and_congr (iff_of_eq ?_) Iff.rfl).trans (and_congr_right fun h => ?_)

Premises used: Iff.rfl, and_congr_right, exists_congr, Iff.trans, and_congr, iff_of_eq
-- Module: Mathlib.Computability.PartrecBasis
Goal:
n : ℕ
f : List.Vector ℕ (n + 1) → ℕ
hf : Partrec' (↑f : List.Vector ℕ (n + 1) →. ℕ)
v : List.Vector ℕ n
b : ℕ
refine_1 :
  ∀ (a : ℕ),
    (a ∈ Nat.rfind fun (n_1 : ℕ) ↦ Part.some (decide (1 ≤ f (n_1 ::ᵥ v)))) =
      (a ∈ Nat.rfind fun (n_1 : ℕ) ↦ (↑(some (Option.isSome (α := ℕ) (ofNat (Option ℕ) (f (n_1 ::ᵥ v))))) : Part Bool))
refine_2 :
  ∀ (a : ℕ)
    (h :
      a ∈ Nat.rfind fun (n_1 : ℕ) ↦ (↑(some (Option.isSome (α := ℕ) (ofNat (Option ℕ) (f (n_1 ::ᵥ v))))) : Part Bool)),
    b = (f (a ::ᵥ v)).pred ↔ ofNat (Option ℕ) (f (a ::ᵥ v)) = some b
⊢ (∃ a ∈ Nat.rfind fun (n_1 : ℕ) ↦ Part.some (decide (1 ≤ f (n_1 ::ᵥ v))), b = (f (a ::ᵥ v)).pred) ↔
    ∃ a ∈ Nat.rfind fun (n_1 : ℕ) ↦ (↑(some (Option.isSome (α := ℕ) (ofNat (Option ℕ) (f (n_1 ::ᵥ v))))) : Part Bool),
      ofNat (Option ℕ) (f (a ::ᵥ v)) = some b

Tactic:
refine
        exists_congr fun a => (and_congr (iff_of_eq ?_) Iff.rfl).trans (and_congr_right fun h => ?_)

Premises used: Iff.rfl, and_congr_right, exists_congr, Iff.trans, and_congr, iff_of_eq
-- Module: Mathlib.Computability.PartrecBasis
Goal:
n : ℕ
f : List.Vector ℕ (n + 1) → ℕ
hf : Partrec' (↑f : List.Vector ℕ (n + 1) →. ℕ)
v : List.Vector ℕ n
b a : ℕ
refine_1 :
  Eq (α := ℕ →. Bool) (fun (n_1 : ℕ) ↦ Part.some (decide (1 ≤ f (n_1 ::ᵥ v)))) fun (n_1 : ℕ) ↦
    (↑(some (Option.isSome (α := ℕ) (ofNat (Option ℕ) (f (n_1 ::ᵥ v))))) : Part Bool)
⊢ (a ∈ Nat.rfind fun (n_1 : ℕ) ↦ Part.some (decide (1 ≤ f (n_1 ::ᵥ v)))) =
    (a ∈ Nat.rfind fun (n_1 : ℕ) ↦ (↑(some (Option.isSome (α := ℕ) (ofNat (Option ℕ) (f (n_1 ::ᵥ v))))) : Part Bool))

Tactic:
congr
-- Module: Mathlib.Computability.PartrecBasis
Goal:
n : ℕ
f : List.Vector ℕ (n + 1) → ℕ
hf : Partrec' (↑f : List.Vector ℕ (n + 1) →. ℕ)
v : List.Vector ℕ n
b a : ℕ
refine_1 :
  ∀ (n_1 : ℕ),
    Part.some (decide (1 ≤ f (n_1 ::ᵥ v))) =
      (↑(some (Option.isSome (α := ℕ) (ofNat (Option ℕ) (f (n_1 ::ᵥ v))))) : Part Bool)
⊢ Eq (α := ℕ →. Bool) (fun (n_1 : ℕ) ↦ Part.some (decide (1 ≤ f (n_1 ::ᵥ v)))) fun (n_1 : ℕ) ↦
    (↑(some (Option.isSome (α := ℕ) (ofNat (Option ℕ) (f (n_1 ::ᵥ v))))) : Part Bool)

Tactic:
funext n
-- Module: Mathlib.Computability.PartrecBasis
Goal:
n_1 : ℕ
f : List.Vector ℕ (n_1 + 1) → ℕ
hf : Partrec' (↑f : List.Vector ℕ (n_1 + 1) →. ℕ)
v : List.Vector ℕ n_1
b a n : ℕ
refine_1 : Part.some (decide (LE.le (α := ℕ) 1 0)) = (↑(some (Option.isSome (α := ℕ) (ofNat (Option ℕ) 0))) : Part Bool)
refine_1₁ :
  ∀ (n : ℕ), Part.some (decide (1 ≤ n + 1)) = (↑(some (Option.isSome (α := ℕ) (ofNat (Option ℕ) (n + 1)))) : Part Bool)
⊢ Part.some (decide (1 ≤ f (n ::ᵥ v))) = (↑(some (Option.isSome (α := ℕ) (ofNat (Option ℕ) (f (n ::ᵥ v))))) : Part Bool)

Tactic:
cases f (n ::ᵥ v)

Premises used: List.Vector.cons
-- Module: Mathlib.Computability.PartrecBasis
Goal:
n_1 : ℕ
f : List.Vector ℕ (n_1 + 1) → ℕ
hf : Partrec' (↑f : List.Vector ℕ (n_1 + 1) →. ℕ)
v : List.Vector ℕ n_1
b a n : ℕ
refine_1 : Eq (α := Option ℕ) (ofNat (Option ℕ) 0) Option.none
⊢ Part.some (decide (LE.le (α := ℕ) 1 0)) = (↑(some (Option.isSome (α := ℕ) (ofNat (Option ℕ) 0))) : Part Bool)

Tactic:
simp
-- Module: Mathlib.Computability.PartrecBasis
Goal:
n_1 : ℕ
f : List.Vector ℕ (n_1 + 1) → ℕ
hf : Partrec' (↑f : List.Vector ℕ (n_1 + 1) →. ℕ)
v : List.Vector ℕ n_1
b a n n_2 : ℕ
refine_1 : Option.isSome (α := ℕ) (ofNat (Option ℕ) (n_2 + 1)) = true
⊢ Part.some (decide (1 ≤ n_2 + 1)) = (↑(some (Option.isSome (α := ℕ) (ofNat (Option ℕ) (n_2 + 1)))) : Part Bool)

Tactic:
simp
-- Module: Mathlib.Computability.PartrecBasis
Goal:
n_1 : ℕ
f : List.Vector ℕ (n_1 + 1) → ℕ
hf : Partrec' (↑f : List.Vector ℕ (n_1 + 1) →. ℕ)
v : List.Vector ℕ n_1
b a n : ℕ
⊢ Eq (α := Option ℕ) (ofNat (Option ℕ) 0) Option.none

Tactic:
rfl
-- Module: Mathlib.Computability.PartrecBasis
Goal:
n_1 : ℕ
f : List.Vector ℕ (n_1 + 1) → ℕ
hf : Partrec' (↑f : List.Vector ℕ (n_1 + 1) →. ℕ)
v : List.Vector ℕ n_1
b a n n_2 : ℕ
⊢ Option.isSome (α := ℕ) (ofNat (Option ℕ) (n_2 + 1)) = true

Tactic:
rfl
-- Module: Mathlib.Computability.PartrecBasis
Goal:
n : ℕ
f : List.Vector ℕ (n + 1) → ℕ
hf : Partrec' (↑f : List.Vector ℕ (n + 1) →. ℕ)
v : List.Vector ℕ n
b a : ℕ
h : a ∈ Nat.rfind fun (n_1 : ℕ) ↦ (↑(some (Option.isSome (α := ℕ) (ofNat (Option ℕ) (f (n_1 ::ᵥ v))))) : Part Bool)
⊢ true ∈ (↑(some (Option.isSome (α := ℕ) (ofNat (Option ℕ) (f (a ::ᵥ v))))) : Part Bool)

Tactic:
have := Nat.rfind_spec h
-- Module: Mathlib.Computability.PartrecBasis
Goal:
n : ℕ
f : List.Vector ℕ (n + 1) → ℕ
hf : Partrec' (↑f : List.Vector ℕ (n + 1) →. ℕ)
v : List.Vector ℕ n
b a : ℕ
h : a ∈ Nat.rfind fun (n_1 : ℕ) ↦ (↑(some (Option.isSome (α := ℕ) (ofNat (Option ℕ) (f (n_1 ::ᵥ v))))) : Part Bool)
this : true ∈ (↑(some (Option.isSome (α := ℕ) (ofNat (Option ℕ) (f (a ::ᵥ v))))) : Part Bool)
⊢ true = Option.isSome (α := ℕ) (ofNat (Option ℕ) (f (a ::ᵥ v)))

Tactic:
simp only [Part.coe_some, Part.mem_some_iff] at this

Premises used: Part.mem_some_iff, Part.coe_some
-- Module: Mathlib.Computability.PartrecBasis
Goal:
n : ℕ
f : List.Vector ℕ (n + 1) → ℕ
hf : Partrec' (↑f : List.Vector ℕ (n + 1) →. ℕ)
v : List.Vector ℕ n
b a : ℕ
h : a ∈ Nat.rfind fun (n_1 : ℕ) ↦ (↑(some (Option.isSome (α := ℕ) (ofNat (Option ℕ) (f (n_1 ::ᵥ v))))) : Part Bool)
this : true = Option.isSome (α := ℕ) (ofNat (Option ℕ) (f (a ::ᵥ v)))
refine_2 :
  ∀ (this : true = Option.isSome (α := ℕ) (ofNat (Option ℕ) (f (a ::ᵥ v)))),
    b = (f (a ::ᵥ v)).pred ↔ ofNat (Option ℕ) (f (a ::ᵥ v)) = some b
⊢ b = (f (a ::ᵥ v)).pred ↔ ofNat (Option ℕ) (f (a ::ᵥ v)) = some b

Tactic:
revert this
-- Module: Mathlib.Computability.PartrecBasis
Goal:
n : ℕ
f : List.Vector ℕ (n + 1) → ℕ
hf : Partrec' (↑f : List.Vector ℕ (n + 1) →. ℕ)
v : List.Vector ℕ n
b a : ℕ
h : a ∈ Nat.rfind fun (n_1 : ℕ) ↦ (↑(some (Option.isSome (α := ℕ) (ofNat (Option ℕ) (f (n_1 ::ᵥ v))))) : Part Bool)
refine_2 : ∀ (this : true = Option.isSome (α := ℕ) (ofNat (Option ℕ) 0)), b = pred 0 ↔ ofNat (Option ℕ) 0 = some b
refine_2₁ :
  ∀ (c : ℕ) (this : true = Option.isSome (α := ℕ) (ofNat (Option ℕ) (c + 1))),
    b = (c + 1).pred ↔ ofNat (Option ℕ) (c + 1) = some b
⊢ ∀ (this : true = Option.isSome (α := ℕ) (ofNat (Option ℕ) (f (a ::ᵥ v)))),
    b = (f (a ::ᵥ v)).pred ↔ ofNat (Option ℕ) (f (a ::ᵥ v)) = some b

Tactic:
rcases f (a ::ᵥ v) with - | c

Premises used: List.Vector.cons
-- Module: Mathlib.Computability.PartrecBasis
Goal:
n : ℕ
f : List.Vector ℕ (n + 1) → ℕ
hf : Partrec' (↑f : List.Vector ℕ (n + 1) →. ℕ)
v : List.Vector ℕ n
b a : ℕ
h : a ∈ Nat.rfind fun (n_1 : ℕ) ↦ (↑(some (Option.isSome (α := ℕ) (ofNat (Option ℕ) (f (n_1 ::ᵥ v))))) : Part Bool)
this : true = Option.isSome (α := ℕ) (ofNat (Option ℕ) 0)
⊢ b = pred 0 ↔ ofNat (Option ℕ) 0 = some b

Tactic:
cases this
-- Module: Mathlib.Computability.PartrecBasis
Goal:
n : ℕ
f : List.Vector ℕ (n + 1) → ℕ
hf : Partrec' (↑f : List.Vector ℕ (n + 1) →. ℕ)
v : List.Vector ℕ n
b a : ℕ
h : a ∈ Nat.rfind fun (n_1 : ℕ) ↦ (↑(some (Option.isSome (α := ℕ) (ofNat (Option ℕ) (f (n_1 ::ᵥ v))))) : Part Bool)
c : ℕ
this : true = Option.isSome (α := ℕ) (ofNat (Option ℕ) (c + 1))
refine_2 : some (c + 1).pred = some b ↔ ofNat (Option ℕ) (c + 1) = some b
⊢ b = (c + 1).pred ↔ ofNat (Option ℕ) (c + 1) = some b

Tactic:
rw [← Option.some_inj, eq_comm]

Premises used: eq_comm, Option.some_inj
-- Module: Mathlib.Computability.PartrecBasis
Goal:
n : ℕ
f : List.Vector ℕ (n + 1) → ℕ
hf : Partrec' (↑f : List.Vector ℕ (n + 1) →. ℕ)
v : List.Vector ℕ n
b a : ℕ
h : a ∈ Nat.rfind fun (n_1 : ℕ) ↦ (↑(some (Option.isSome (α := ℕ) (ofNat (Option ℕ) (f (n_1 ::ᵥ v))))) : Part Bool)
c : ℕ
this : true = Option.isSome (α := ℕ) (ofNat (Option ℕ) (c + 1))
⊢ some (c + 1).pred = some b ↔ ofNat (Option ℕ) (c + 1) = some b

Tactic:
rfl
-- Module: Mathlib.Computability.PartrecBasis
Goal:
f : ℕ →. ℕ
hf : Nat.Partrec f
obtain : ∀ (c : Code) (hf : Nat.Partrec c.eval), Partrec' (n := 1) fun (v : List.Vector ℕ 1) ↦ c.eval v.head
⊢ Partrec' (n := 1) fun (v : List.Vector ℕ 1) ↦ f v.head

Tactic:
obtain ⟨c, rfl⟩ := exists_code.1 hf

Premises used: Iff.mp, Nat.Partrec.Code.exists_code, rfl