awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
n_1 : ℕ
f_1 : List.Vector ℕ n_1 →. ℕ
n_2 : ℕ
f_2 : List.Vector ℕ n_2 → ℕ
n : ℕ
f : List.Vector ℕ n → ℕ
g : List.Vector ℕ (n + 2) → ℕ
h : Nat.Primrec' f
h_1 : Nat.Primrec' g
cf cg : Code
hf : ∀ (v : List.Vector ℕ n), cf.eval (↑v : List ℕ) = Part.some (pure (f v))
hg : ∀ (v : List.Vector ℕ (n + 2)), cg.eval (↑v : List ℕ) = Part.some (pure (g v))
⊢ ∃ (c : Code),
    ∀ (v : List.Vector ℕ (n + 1)),
      c.eval (↑v : List ℕ) =
        pure <$>
          (↑fun (v : List.Vector ℕ (n + 1)) ↦
                Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (f v.tail) (fun (y IH : ℕ) ↦ g (y ::ᵥ IH ::ᵥ v.tail)) v.head :
              List.Vector ℕ (n + 1) →. ℕ)
            v

Tactic:
⟨prec cf cg, fun v => ?_⟩

Premises used: Turing.ToPartrec.Code.prec, Exists.intro
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
n_1 : ℕ
f_1 : List.Vector ℕ n_1 →. ℕ
n_2 : ℕ
f_2 : List.Vector ℕ n_2 → ℕ
n : ℕ
f : List.Vector ℕ n → ℕ
g : List.Vector ℕ (n + 2) → ℕ
h : Nat.Primrec' f
h_1 : Nat.Primrec' g
cf cg : Code
hf : ∀ (v : List.Vector ℕ n), cf.eval (↑v : List ℕ) = Part.some (pure (f v))
hg : ∀ (v : List.Vector ℕ (n + 2)), cg.eval (↑v : List ℕ) = Part.some (pure (g v))
prim :
  ∀ (v : List.Vector ℕ (n + 1)),
    (cf.prec cg).eval (↑v : List ℕ) =
      pure <$>
        (↑fun (v : List.Vector ℕ (n + 1)) ↦
              Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (f v.tail) (fun (y IH : ℕ) ↦ g (y ::ᵥ IH ::ᵥ v.tail)) v.head :
            List.Vector ℕ (n + 1) →. ℕ)
          v
⊢ ∃ (c : Code),
    ∀ (v : List.Vector ℕ (n + 1)),
      c.eval (↑v : List ℕ) =
        pure <$>
          (↑fun (v : List.Vector ℕ (n + 1)) ↦
                Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (f v.tail) (fun (y IH : ℕ) ↦ g (y ::ᵥ IH ::ᵥ v.tail)) v.head :
              List.Vector ℕ (n + 1) →. ℕ)
            v

Tactic:
refine ⟨prec cf cg, fun v => ?_⟩
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
n_1 : ℕ
f_1 : List.Vector ℕ n_1 →. ℕ
n_2 : ℕ
f_2 : List.Vector ℕ n_2 → ℕ
n : ℕ
f : List.Vector ℕ n → ℕ
g : List.Vector ℕ (n + 2) → ℕ
h : Nat.Primrec' f
h_1 : Nat.Primrec' g
cf cg : Code
hf : ∀ (v : List.Vector ℕ n), cf.eval (↑v : List ℕ) = Part.some (pure (f v))
hg : ∀ (v : List.Vector ℕ (n + 2)), cg.eval (↑v : List ℕ) = Part.some (pure (g v))
v : List.Vector ℕ (n + 1)
prim :
  (cf.prec cg).eval (↑(v.head ::ᵥ v.tail) : List ℕ) =
    pure <$>
      (↑fun (v : List.Vector ℕ (n + 1)) ↦
            Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (f v.tail) (fun (y IH : ℕ) ↦ g (y ::ᵥ IH ::ᵥ v.tail)) v.head :
          List.Vector ℕ (n + 1) →. ℕ)
        (v.head ::ᵥ v.tail)
⊢ (cf.prec cg).eval (↑v : List ℕ) =
    pure <$>
      (↑fun (v : List.Vector ℕ (n + 1)) ↦
            Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (f v.tail) (fun (y IH : ℕ) ↦ g (y ::ᵥ IH ::ᵥ v.tail)) v.head :
          List.Vector ℕ (n + 1) →. ℕ)
        v

Tactic:
rw [← v.cons_head_tail]

Premises used: List.Vector.cons_head_tail
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
n_1 : ℕ
f_1 : List.Vector ℕ n_1 →. ℕ
n_2 : ℕ
f_2 : List.Vector ℕ n_2 → ℕ
n : ℕ
f : List.Vector ℕ n → ℕ
g : List.Vector ℕ (n + 2) → ℕ
h : Nat.Primrec' f
h_1 : Nat.Primrec' g
cf cg : Code
hf : ∀ (v : List.Vector ℕ n), cf.eval (↑v : List ℕ) = Part.some (pure (f v))
hg : ∀ (v : List.Vector ℕ (n + 2)), cg.eval (↑v : List ℕ) = Part.some (pure (g v))
v : List.Vector ℕ (n + 1)
⊢ cf.eval (↑v.tail : List ℕ) = Part.some (pure (f v.tail))

Tactic:
specialize hf v.tail

Premises used: List.Vector.tail
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
n_1 : ℕ
f_1 : List.Vector ℕ n_1 →. ℕ
n_2 : ℕ
f_2 : List.Vector ℕ n_2 → ℕ
n : ℕ
f : List.Vector ℕ n → ℕ
g : List.Vector ℕ (n + 2) → ℕ
h : Nat.Primrec' f
h_1 : Nat.Primrec' g
cf cg : Code
hg : ∀ (v : List.Vector ℕ (n + 2)), cg.eval (↑v : List ℕ) = Part.some (pure (g v))
v : List.Vector ℕ (n + 1)
hf : cf.eval (↑v.tail : List ℕ) = Part.some (pure (f v.tail))
⊢ ∀ (a b : ℕ), cg.eval (↑(a ::ᵥ b ::ᵥ v.tail) : List ℕ) = Part.some (pure (g (a ::ᵥ b ::ᵥ v.tail)))

Tactic:
replace hg := fun a b => hg (a ::ᵥ b ::ᵥ v.tail)
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
n_1 : ℕ
f_1 : List.Vector ℕ n_1 →. ℕ
n_2 : ℕ
f_2 : List.Vector ℕ n_2 → ℕ
n : ℕ
f : List.Vector ℕ n → ℕ
g : List.Vector ℕ (n + 2) → ℕ
h : Nat.Primrec' f
h_1 : Nat.Primrec' g
cf cg : Code
v : List.Vector ℕ (n + 1)
hf : cf.eval (↑v.tail : List ℕ) = Part.some (pure (f v.tail))
hg : ∀ (a b : ℕ), cg.eval (↑(a ::ᵥ b ::ᵥ v.tail) : List ℕ) = Part.some (pure (g (a ::ᵥ b ::ᵥ v.tail)))
⊢ cf.eval (↑v : List ℕ).tail = Part.some (pure (f v.tail))

Tactic:
simp only [Vector.cons_val, Vector.tail_val] at hf hg

Premises used: List.Vector.cons_val, List.Vector.tail_val
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
n_1 : ℕ
f_1 : List.Vector ℕ n_1 →. ℕ
n_2 : ℕ
f_2 : List.Vector ℕ n_2 → ℕ
n : ℕ
f : List.Vector ℕ n → ℕ
g : List.Vector ℕ (n + 2) → ℕ
h : Nat.Primrec' f
h_1 : Nat.Primrec' g
cf cg : Code
v : List.Vector ℕ (n + 1)
hf : cf.eval (↑v.tail : List ℕ) = Part.some (pure (f v.tail))
hg : ∀ (a b : ℕ), cg.eval (↑(a ::ᵥ b ::ᵥ v.tail) : List ℕ) = Part.some (pure (g (a ::ᵥ b ::ᵥ v.tail)))
hf₁ : cf.eval (↑v : List ℕ).tail = Part.some (pure (f v.tail))
⊢ ∀ (a b : ℕ), cg.eval (a :: b :: (↑v : List ℕ).tail) = Part.some (pure (g (a ::ᵥ b ::ᵥ v.tail)))

Tactic:
simp only [Vector.cons_val, Vector.tail_val] at hf hg

Premises used: List.Vector.cons_val, List.Vector.tail_val
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
n_1 : ℕ
f_1 : List.Vector ℕ n_1 →. ℕ
n_2 : ℕ
f_2 : List.Vector ℕ n_2 → ℕ
n : ℕ
f : List.Vector ℕ n → ℕ
g : List.Vector ℕ (n + 2) → ℕ
h : Nat.Primrec' f
h_1 : Nat.Primrec' g
cf cg : Code
v : List.Vector ℕ (n + 1)
hf : cf.eval (↑v : List ℕ).tail = Part.some (pure (f v.tail))
hg : ∀ (a b : ℕ), cg.eval (a :: b :: (↑v : List ℕ).tail) = Part.some (pure (g (a ::ᵥ b ::ᵥ v.tail)))
prim :
  (cf.prec cg).eval (v.head :: (↑v : List ℕ).tail) =
    Part.some (pure (Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (f v.tail) (fun (y IH : ℕ) ↦ g (y ::ᵥ IH ::ᵥ v.tail)) v.head))
⊢ (cf.prec cg).eval (↑(v.head ::ᵥ v.tail) : List ℕ) =
    pure <$>
      (↑fun (v : List.Vector ℕ (n + 1)) ↦
            Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (f v.tail) (fun (y IH : ℕ) ↦ g (y ::ᵥ IH ::ᵥ v.tail)) v.head :
          List.Vector ℕ (n + 1) →. ℕ)
        (v.head ::ᵥ v.tail)

Tactic:
simp only [Part.map_eq_map, Part.map_some, Vector.cons_val, Vector.tail_cons,
        Vector.head_cons, PFun.coe_val, Vector.tail_val]

Premises used: List.Vector.tail_cons, List.Vector.cons_val, PFun.coe_val, Part.map_eq_map, List.Vector.head_cons, Part.map_some, List.Vector.tail_val
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
n_1 : ℕ
f_1 : List.Vector ℕ n_1 →. ℕ
n_2 : ℕ
f_2 : List.Vector ℕ n_2 → ℕ
n_3 : ℕ
f : List.Vector ℕ n_3 → ℕ
g : List.Vector ℕ (n_3 + 2) → ℕ
h : Nat.Primrec' f
h_1 : Nat.Primrec' g
cf cg : Code
v : List.Vector ℕ (n_3 + 1)
hf : cf.eval (↑v : List ℕ).tail = pure (pure (f v.tail))
hg : ∀ (a b : ℕ), cg.eval (a :: b :: (↑v : List ℕ).tail) = pure (pure (g (a ::ᵥ b ::ᵥ v.tail)))
n : ℕ
h_2 :
  (cf.prec cg).eval (n :: (↑v : List ℕ).tail) =
    pure (pure (Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (f v.tail) (fun (y IH : ℕ) ↦ g (y ::ᵥ IH ::ᵥ v.tail)) n))
prim :
  (Part.bind
      (PFun.fix
        (fun (v : List ℕ) ↦
          (cg.eval (v.headI :: v.tail.tail)).bind fun (x : List ℕ) ↦
            Part.some
              (if v.tail.headI = 0 then Sum.inl ((v.headI + 1) :: (v.tail.headI - 1) :: x.headI :: v.tail.tail.tail)
              else Sum.inr ((v.headI + 1) :: (v.tail.headI - 1) :: x.headI :: v.tail.tail.tail)))
        (0 :: n :: f v.tail :: (↑v : List ℕ).tail))
      fun (x : List ℕ) ↦ Part.some [x.tail.tail.headI]) =
    Part.some
      [g (n ::ᵥ Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (f v.tail) (fun (y IH : ℕ) ↦ g (y ::ᵥ IH ::ᵥ v.tail)) n ::ᵥ v.tail)]
⊢ (cf.prec cg).eval ((n + 1) :: (↑v : List ℕ).tail) =
    pure (pure (Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (f v.tail) (fun (y IH : ℕ) ↦ g (y ::ᵥ IH ::ᵥ v.tail)) (n + 1)))

Tactic:
simp [prec, hf, Part.bind_assoc, ← Part.bind_some_eq_map, Part.bind_some, Bind.bind]

Premises used: Part.bind_some, Turing.ToPartrec.Code.prec, Part.bind_some_eq_map, Part.bind_assoc, Bind.bind
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
n_1 : ℕ
f_1 : List.Vector ℕ n_1 →. ℕ
n_2 : ℕ
f_2 : List.Vector ℕ n_2 → ℕ
n_3 : ℕ
f : List.Vector ℕ n_3 → ℕ
g : List.Vector ℕ (n_3 + 2) → ℕ
h : Nat.Primrec' f
h_1 : Nat.Primrec' g
cf cg : Code
v : List.Vector ℕ (n_3 + 1)
hf : cf.eval (↑v : List ℕ).tail = pure (pure (f v.tail))
hg : ∀ (a b : ℕ), cg.eval (a :: b :: (↑v : List ℕ).tail) = pure (pure (g (a ::ᵥ b ::ᵥ v.tail)))
n : ℕ
h_2 :
  (cf.prec cg).eval (n :: (↑v : List ℕ).tail) =
    pure (pure (Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (f v.tail) (fun (y IH : ℕ) ↦ g (y ::ᵥ IH ::ᵥ v.tail)) n))
this :
  ∀ (a b : ℕ),
    a + b = n →
      Membership.mem (γ := Part (List ℕ))
        (PFun.fix
          (fun (v : List ℕ) ↦
            (cg.eval (v.headI :: v.tail.tail)).bind fun (x : List ℕ) ↦
              Part.some
                (if v.tail.headI = 0 then Sum.inl (v.headI.succ :: v.tail.headI.pred :: x.headI :: v.tail.tail.tail)
                else Sum.inr (v.headI.succ :: v.tail.headI.pred :: x.headI :: v.tail.tail.tail)))
          (a ::
            b ::
              Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (f v.tail) (fun (y IH : ℕ) ↦ g (y ::ᵥ IH ::ᵥ v.tail)) a ::
                (↑v : List ℕ).tail))
        (n.succ ::
          0 ::
            g
                (n ::ᵥ
                  Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (f v.tail) (fun (y IH : ℕ) ↦ g (y ::ᵥ IH ::ᵥ v.tail)) n ::ᵥ
                    v.tail) ::
              (↑v : List ℕ).tail)
⊢ PFun.fix
      (fun (v : List ℕ) ↦
        (cg.eval (v.headI :: v.tail.tail)).bind fun (x : List ℕ) ↦
          Part.some
            (if v.tail.headI = 0 then Sum.inl (v.headI.succ :: v.tail.headI.pred :: x.headI :: v.tail.tail.tail)
            else Sum.inr (v.headI.succ :: v.tail.headI.pred :: x.headI :: v.tail.tail.tail)))
      (0 ::
        n ::
          Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (f v.tail) (fun (y IH : ℕ) ↦ g (y ::ᵥ IH ::ᵥ v.tail)) 0 ::
            (↑v : List ℕ).tail) =
    Part.some
      (n.succ ::
        0 ::
          g
              (n ::ᵥ
                Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (f v.tail) (fun (y IH : ℕ) ↦ g (y ::ᵥ IH ::ᵥ v.tail)) n ::ᵥ
                  v.tail) ::
            (↑v : List ℕ).tail)

Tactic:
have := Part.eq_some_iff.mpr (this _ _ (zero_add _))
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
n_1 : ℕ
f_1 : List.Vector ℕ n_1 →. ℕ
n_2 : ℕ
f_2 : List.Vector ℕ n_2 → ℕ
n_3 : ℕ
f : List.Vector ℕ n_3 → ℕ
g : List.Vector ℕ (n_3 + 2) → ℕ
h : Nat.Primrec' f
h_1 : Nat.Primrec' g
cf cg : Code
v : List.Vector ℕ (n_3 + 1)
hf : cf.eval (↑v : List ℕ).tail = pure (pure (f v.tail))
hg : ∀ (a b : ℕ), cg.eval (a :: b :: (↑v : List ℕ).tail) = pure (pure (g (a ::ᵥ b ::ᵥ v.tail)))
n : ℕ
h_2 :
  (cf.prec cg).eval (n :: (↑v : List ℕ).tail) =
    pure (pure (Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (f v.tail) (fun (y IH : ℕ) ↦ g (y ::ᵥ IH ::ᵥ v.tail)) n))
this_1 :
  ∀ (a b : ℕ),
    a + b = n →
      Membership.mem (γ := Part (List ℕ))
        (PFun.fix
          (fun (v : List ℕ) ↦
            (cg.eval (v.headI :: v.tail.tail)).bind fun (x : List ℕ) ↦
              Part.some
                (if v.tail.headI = 0 then Sum.inl (v.headI.succ :: v.tail.headI.pred :: x.headI :: v.tail.tail.tail)
                else Sum.inr (v.headI.succ :: v.tail.headI.pred :: x.headI :: v.tail.tail.tail)))
          (a ::
            b ::
              Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (f v.tail) (fun (y IH : ℕ) ↦ g (y ::ᵥ IH ::ᵥ v.tail)) a ::
                (↑v : List ℕ).tail))
        (n.succ ::
          0 ::
            g
                (n ::ᵥ
                  Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (f v.tail) (fun (y IH : ℕ) ↦ g (y ::ᵥ IH ::ᵥ v.tail)) n ::ᵥ
                    v.tail) ::
              (↑v : List ℕ).tail)
this :
  PFun.fix
      (fun (v : List ℕ) ↦
        (cg.eval (v.headI :: v.tail.tail)).bind fun (x : List ℕ) ↦
          Part.some
            (if v.tail.headI = 0 then Sum.inl (v.headI.succ :: v.tail.headI.pred :: x.headI :: v.tail.tail.tail)
            else Sum.inr (v.headI.succ :: v.tail.headI.pred :: x.headI :: v.tail.tail.tail)))
      (0 ::
        n ::
          Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (f v.tail) (fun (y IH : ℕ) ↦ g (y ::ᵥ IH ::ᵥ v.tail)) 0 ::
            (↑v : List ℕ).tail) =
    Part.some
      (n.succ ::
        0 ::
          g
              (n ::ᵥ
                Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (f v.tail) (fun (y IH : ℕ) ↦ g (y ::ᵥ IH ::ᵥ v.tail)) n ::ᵥ
                  v.tail) ::
            (↑v : List ℕ).tail)
⊢ (Part.bind
      (PFun.fix
        (fun (v : List ℕ) ↦
          (cg.eval (v.headI :: v.tail.tail)).bind fun (x : List ℕ) ↦
            Part.some
              (if v.tail.headI = 0 then Sum.inl ((v.headI + 1) :: (v.tail.headI - 1) :: x.headI :: v.tail.tail.tail)
              else Sum.inr ((v.headI + 1) :: (v.tail.headI - 1) :: x.headI :: v.tail.tail.tail)))
        (0 :: n :: f v.tail :: (↑v : List ℕ).tail))
      fun (x : List ℕ) ↦ Part.some [x.tail.tail.headI]) =
    Part.some
      [g (n ::ᵥ Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (f v.tail) (fun (y IH : ℕ) ↦ g (y ::ᵥ IH ::ᵥ v.tail)) n ::ᵥ v.tail)]

Tactic:
simp_all
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
n_1 : ℕ
f_1 : List.Vector ℕ n_1 →. ℕ
n_2 : ℕ
f_2 : List.Vector ℕ n_2 → ℕ
n_3 : ℕ
f : List.Vector ℕ n_3 → ℕ
g : List.Vector ℕ (n_3 + 2) → ℕ
h : Nat.Primrec' f
h_1 : Nat.Primrec' g
cf cg : Code
v : List.Vector ℕ (n_3 + 1)
hf : cf.eval (↑v : List ℕ).tail = pure (pure (f v.tail))
hg : ∀ (a b : ℕ), cg.eval (a :: b :: (↑v : List ℕ).tail) = pure (pure (g (a ::ᵥ b ::ᵥ v.tail)))
n : ℕ
h_2 :
  (cf.prec cg).eval (n :: (↑v : List ℕ).tail) =
    pure (pure (Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (f v.tail) (fun (y IH : ℕ) ↦ g (y ::ᵥ IH ::ᵥ v.tail)) n))
prim :
  ∀ (a b : ℕ),
    a + b = n →
      Membership.mem (γ := Part (List ℕ))
        (PFun.fix
          (fun (v : List ℕ) ↦
            (cg.eval (v.headI :: v.tail.tail)).bind fun (x : List ℕ) ↦
              Part.some
                (if v.tail.headI = 0 then Sum.inl (v.headI.succ :: v.tail.headI.pred :: x.headI :: v.tail.tail.tail)
                else Sum.inr (v.headI.succ :: v.tail.headI.pred :: x.headI :: v.tail.tail.tail)))
          (a ::
            b ::
              Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (f v.tail) (fun (y IH : ℕ) ↦ g (y ::ᵥ IH ::ᵥ v.tail)) a ::
                (↑v : List ℕ).tail))
        (n.succ ::
          0 ::
            g
                (n ::ᵥ
                  Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (f v.tail) (fun (y IH : ℕ) ↦ g (y ::ᵥ IH ::ᵥ v.tail)) n ::ᵥ
                    v.tail) ::
              (↑v : List ℕ).tail)
⊢ (Part.bind
      (PFun.fix
        (fun (v : List ℕ) ↦
          (cg.eval (v.headI :: v.tail.tail)).bind fun (x : List ℕ) ↦
            Part.some
              (if v.tail.headI = 0 then Sum.inl ((v.headI + 1) :: (v.tail.headI - 1) :: x.headI :: v.tail.tail.tail)
              else Sum.inr ((v.headI + 1) :: (v.tail.headI - 1) :: x.headI :: v.tail.tail.tail)))
        (0 :: n :: f v.tail :: (↑v : List ℕ).tail))
      fun (x : List ℕ) ↦ Part.some [x.tail.tail.headI]) =
    Part.some
      [g (n ::ᵥ Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (f v.tail) (fun (y IH : ℕ) ↦ g (y ::ᵥ IH ::ᵥ v.tail)) n ::ᵥ v.tail)]

Tactic:
suffices ∀ a b, a + b = n →
        (n.succ :: 0 ::
          g (n ::ᵥ Nat.rec (f v.tail) (fun y IH => g (y ::ᵥ IH ::ᵥ v.tail)) n ::ᵥ v.tail) ::
              v.val.tail : List ℕ) ∈
          PFun.fix
            (fun v : List ℕ => Part.bind (cg.eval (v.headI :: v.tail.tail))
              (fun x => Part.some (if v.tail.headI = 0
                then Sum.inl
                  (v.headI.succ :: v.tail.headI.pred :: x.headI :: v.tail.tail.tail : List ℕ)
                else Sum.inr
                  (v.headI.succ :: v.tail.headI.pred :: x.headI :: v.tail.tail.tail))))
            (a :: b :: Nat.rec (f v.tail) (fun y IH => g (y ::ᵥ IH ::ᵥ v.tail)) a :: v.val.tail) by
        have := Part.eq_some_iff.mpr (this _ _ (zero_add _))
        simp_all
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
n_1 : ℕ
f_1 : List.Vector ℕ n_1 →. ℕ
n_2 : ℕ
f_2 : List.Vector ℕ n_2 → ℕ
n_3 : ℕ
f : List.Vector ℕ n_3 → ℕ
g : List.Vector ℕ (n_3 + 2) → ℕ
h : Nat.Primrec' f
h_1 : Nat.Primrec' g
cf cg : Code
v : List.Vector ℕ (n_3 + 1)
hf : cf.eval (↑v : List ℕ).tail = pure (pure (f v.tail))
hg : ∀ (a b : ℕ), cg.eval (a :: b :: (↑v : List ℕ).tail) = pure (pure (g (a ::ᵥ b ::ᵥ v.tail)))
n : ℕ
h_2 :
  (cf.prec cg).eval (n :: (↑v : List ℕ).tail) =
    pure (pure (Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (f v.tail) (fun (y IH : ℕ) ↦ g (y ::ᵥ IH ::ᵥ v.tail)) n))
a : ℕ
e : a + 0 = n
⊢ Membership.mem (γ := Part (List ℕ))
    (PFun.fix
      (fun (v : List ℕ) ↦
        (cg.eval (v.headI :: v.tail.tail)).bind fun (x : List ℕ) ↦
          Part.some
            (if v.tail.headI = 0 then Sum.inl (v.headI.succ :: v.tail.headI.pred :: x.headI :: v.tail.tail.tail)
            else Sum.inr (v.headI.succ :: v.tail.headI.pred :: x.headI :: v.tail.tail.tail)))
      (a ::
        0 ::
          Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (f v.tail) (fun (y IH : ℕ) ↦ g (y ::ᵥ IH ::ᵥ v.tail)) a ::
            (↑v : List ℕ).tail))
    (n.succ ::
      0 ::
        g
            (n ::ᵥ
              Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (f v.tail) (fun (y IH : ℕ) ↦ g (y ::ᵥ IH ::ᵥ v.tail)) n ::ᵥ v.tail) ::
          (↑v : List ℕ).tail)

Tactic:
PFun.mem_fix_iff.2 (Or.inl <| Part.eq_some_iff.1 ?_)

Premises used: Iff.mpr, Part.eq_some_iff, Iff.mp, Or.inl, PFun.mem_fix_iff
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
n_1 : ℕ
f_1 : List.Vector ℕ n_1 →. ℕ
n_2 : ℕ
f_2 : List.Vector ℕ n_2 → ℕ
n_3 : ℕ
f : List.Vector ℕ n_3 → ℕ
g : List.Vector ℕ (n_3 + 2) → ℕ
h : Nat.Primrec' f
h_1 : Nat.Primrec' g
cf cg : Code
v : List.Vector ℕ (n_3 + 1)
hf : cf.eval (↑v : List ℕ).tail = pure (pure (f v.tail))
hg : ∀ (a b : ℕ), cg.eval (a :: b :: (↑v : List ℕ).tail) = pure (pure (g (a ::ᵥ b ::ᵥ v.tail)))
n : ℕ
h_2 :
  (cf.prec cg).eval (n :: (↑v : List ℕ).tail) =
    pure (pure (Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (f v.tail) (fun (y IH : ℕ) ↦ g (y ::ᵥ IH ::ᵥ v.tail)) n))
a : ℕ
e : a + 0 = n
⊢ Part.some
      (if
          Eq (α := ℕ)
            (List.headI
                (0 ::
                  Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (f v.tail) (fun (y IH : ℕ) ↦ g (y ::ᵥ IH ::ᵥ v.tail)) a ::
                    (↑v : List ℕ).tail) :
              ℕ)
            (0 : ℕ) then
        Sum.inl
          ((a ::
                  0 ::
                    Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (f v.tail) (fun (y IH : ℕ) ↦ g (y ::ᵥ IH ::ᵥ v.tail)) a ::
                      (↑v : List ℕ).tail).headI.succ ::
            Nat.pred
                (List.headI
                  (0 ::
                    Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (f v.tail) (fun (y IH : ℕ) ↦ g (y ::ᵥ IH ::ᵥ v.tail)) a ::
                      (↑v : List ℕ).tail)) ::
              [g
                      ((a ::
                            0 ::
                              Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (f v.tail) (fun (y IH : ℕ) ↦ g (y ::ᵥ IH ::ᵥ v.tail))
                                  a ::
                                (↑v : List ℕ).tail).headI ::ᵥ
                        Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (f v.tail) (fun (y IH : ℕ) ↦ g (y ::ᵥ IH ::ᵥ v.tail)) a ::ᵥ
                          v.tail)].headI ::
                (↑v : List ℕ).tail)
      else
        Sum.inr
          ((a ::
                  0 ::
                    Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (f v.tail) (fun (y IH : ℕ) ↦ g (y ::ᵥ IH ::ᵥ v.tail)) a ::
                      (↑v : List ℕ).tail).headI.succ ::
            Nat.pred
                (List.headI
                  (0 ::
                    Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (f v.tail) (fun (y IH : ℕ) ↦ g (y ::ᵥ IH ::ᵥ v.tail)) a ::
                      (↑v : List ℕ).tail)) ::
              [g
                      ((a ::
                            0 ::
                              Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (f v.tail) (fun (y IH : ℕ) ↦ g (y ::ᵥ IH ::ᵥ v.tail))
                                  a ::
                                (↑v : List ℕ).tail).headI ::ᵥ
                        Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (f v.tail) (fun (y IH : ℕ) ↦ g (y ::ᵥ IH ::ᵥ v.tail)) a ::ᵥ
                          v.tail)].headI ::
                (↑v : List ℕ).tail)) =
    Part.some
      (Sum.inl
        ((a + 0).succ ::
          0 ::
            g
                ((a + 0) ::ᵥ
                  Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (f v.tail) (fun (y IH : ℕ) ↦ g (y ::ᵥ IH ::ᵥ v.tail)) (a + 0) ::ᵥ
                    v.tail) ::
              (↑v : List ℕ).tail))

Tactic:
rfl
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
n_1 : ℕ
f_1 : List.Vector ℕ n_1 →. ℕ
n_2 : ℕ
f_2 : List.Vector ℕ n_2 → ℕ
n_3 : ℕ
f : List.Vector ℕ n_3 → ℕ
g : List.Vector ℕ (n_3 + 2) → ℕ
h : Nat.Primrec' f
h_1 : Nat.Primrec' g
cf cg : Code
v : List.Vector ℕ (n_3 + 1)
hf : cf.eval (↑v : List ℕ).tail = pure (pure (f v.tail))
hg : ∀ (a b : ℕ), cg.eval (a :: b :: (↑v : List ℕ).tail) = pure (pure (g (a ::ᵥ b ::ᵥ v.tail)))
n : ℕ
h_2 :
  (cf.prec cg).eval (n :: (↑v : List ℕ).tail) =
    pure (pure (Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (f v.tail) (fun (y IH : ℕ) ↦ g (y ::ᵥ IH ::ᵥ v.tail)) n))
b : ℕ
IH :
  ∀ (a : ℕ) (e : a + b = n),
    Membership.mem (γ := Part (List ℕ))
      (PFun.fix
        (fun (v : List ℕ) ↦
          (cg.eval (v.headI :: v.tail.tail)).bind fun (x : List ℕ) ↦
            Part.some
              (if v.tail.headI = 0 then Sum.inl (v.headI.succ :: v.tail.headI.pred :: x.headI :: v.tail.tail.tail)
              else Sum.inr (v.headI.succ :: v.tail.headI.pred :: x.headI :: v.tail.tail.tail)))
        (a ::
          b ::
            Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (f v.tail) (fun (y IH : ℕ) ↦ g (y ::ᵥ IH ::ᵥ v.tail)) a ::
              (↑v : List ℕ).tail))
      (n.succ ::
        0 ::
          g
              (n ::ᵥ
                Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (f v.tail) (fun (y IH : ℕ) ↦ g (y ::ᵥ IH ::ᵥ v.tail)) n ::ᵥ
                  v.tail) ::
            (↑v : List ℕ).tail)
a : ℕ
e : a + (b + 1) = n
rwa rwa₁ rwa₂ rwa₃ : a + b + 1 = n
⊢ a + 1 + b = n

Tactic:
rwa [add_right_comm]

Premises used: add_right_comm
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
n_1 : ℕ
f_1 : List.Vector ℕ n_1 →. ℕ
n_2 : ℕ
f_2 : List.Vector ℕ n_2 → ℕ
n : ℕ
f : List.Vector ℕ n → ℕ
g : List.Vector ℕ (n + 2) → ℕ
h : Nat.Primrec' f
h_1 : Nat.Primrec' g
cf cg : Code
v : List.Vector ℕ (n + 1)
hf : cf.eval (↑v : List ℕ).tail = pure (pure (f v.tail))
hg : ∀ (a b : ℕ), cg.eval (a :: b :: (↑v : List ℕ).tail) = pure (pure (g (a ::ᵥ b ::ᵥ v.tail)))
⊢ (cf.prec cg).eval (0 :: (↑v : List ℕ).tail) =
    pure (pure (Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (f v.tail) (fun (y IH : ℕ) ↦ g (y ::ᵥ IH ::ᵥ v.tail)) 0))

Tactic:
simp [prec, hf, Part.bind_assoc, ← Part.bind_some_eq_map, Part.bind_some, Bind.bind]

Premises used: Part.bind_some, Turing.ToPartrec.Code.prec, Part.bind_some_eq_map, Part.bind_assoc, Bind.bind