awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
m n : ℕ
f : List.Vector ℕ n →. ℕ
g : Fin n → List.Vector ℕ m →. ℕ
hg_1 : ∀ (i : Fin n), ∃ (c : Code), ∀ (v : List.Vector ℕ m), c.eval (↑v : List ℕ) = pure <$> g i v
cg : Code
hg :
  ∀ (v : List.Vector ℕ m),
    cg.eval (↑v : List ℕ) =
      Functor.map (α := { l : List ℕ // l.length = n }) (Subtype.val (p := fun (l : List ℕ) ↦ l.length = n))
        (Vector.mOfFn fun (i : Fin n) ↦ g i v)
cf : Code
hf : ∀ (v : List.Vector ℕ n), cf.eval (↑v : List ℕ) = pure <$> f v
v : List.Vector ℕ m
simp :
  Eq (α := Part (List ℕ))
    (do
      let a ← Vector.mOfFn fun (i : Fin n) ↦ g i v
      pure <$> f a)
    do
    let a ← Vector.mOfFn fun (i : Fin n) ↦ g i v
    pure <$> f a
⊢ (cf.comp cg).eval (↑v : List ℕ) = pure <$> ((Vector.mOfFn fun (i : Fin n) ↦ g i v) >>= f)

Tactic:
simp [hg, hf, map_bind]

Premises used: map_bind
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
m n : ℕ
f : List.Vector ℕ n →. ℕ
g : Fin n → List.Vector ℕ m →. ℕ
hg_1 : ∀ (i : Fin n), ∃ (c : Code), ∀ (v : List.Vector ℕ m), c.eval (↑v : List ℕ) = pure <$> g i v
cg : Code
hg :
  ∀ (v : List.Vector ℕ m),
    cg.eval (↑v : List ℕ) =
      Functor.map (α := { l : List ℕ // l.length = n }) (Subtype.val (p := fun (l : List ℕ) ↦ l.length = n))
        (Vector.mOfFn fun (i : Fin n) ↦ g i v)
cf : Code
hf : ∀ (v : List.Vector ℕ n), cf.eval (↑v : List ℕ) = pure <$> f v
v : List.Vector ℕ m
⊢ Eq (α := Part (List ℕ))
    (do
      let a ← Vector.mOfFn fun (i : Fin n) ↦ g i v
      pure <$> f a)
    do
    let a ← Vector.mOfFn fun (i : Fin n) ↦ g i v
    pure <$> f a

Tactic:
rfl
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
m n : ℕ
f : List.Vector ℕ n →. ℕ
g : Fin n → List.Vector ℕ m →. ℕ
hg_1 : ∀ (i : Fin n), ∃ (c : Code), ∀ (v : List.Vector ℕ m), c.eval (↑v : List ℕ) = pure <$> g i v
cg : Code
hg :
  ∀ (v : List.Vector ℕ m),
    cg.eval (↑v : List ℕ) =
      Functor.map (α := { l : List ℕ // l.length = n }) (Subtype.val (p := fun (l : List ℕ) ↦ l.length = n))
        (Vector.mOfFn fun (i : Fin n) ↦ g i v)
cf : Code
hf : ∀ (v : List.Vector ℕ n), cf.eval (↑v : List ℕ) = pure <$> f v
⊢ ∃ (c : Code), ∀ (v : List.Vector ℕ m), c.eval (↑v : List ℕ) = pure <$> ((Vector.mOfFn fun (i : Fin n) ↦ g i v) >>= f)

Tactic:
exact
      ⟨cf.comp cg, fun v => by
        simp [hg, hf, map_bind]
        rfl⟩
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
m : ℕ
g : Fin 0 → List.Vector ℕ m →. ℕ
hg : ∀ (i : Fin 0), ∃ (c : Code), ∀ (v : List.Vector ℕ m), c.eval (↑v : List ℕ) = pure <$> g i v
v : List.Vector ℕ m
simp :
  Eq (α := Part (List ℕ)) (Part.some []) (Subtype.val (p := fun (l : List ℕ) ↦ l.length = 0) <$> Part.some Vector.nil)
⊢ nil.eval (↑v : List ℕ) =
    Functor.map (α := { l : List ℕ // l.length = 0 }) (Subtype.val (p := fun (l : List ℕ) ↦ l.length = 0))
      (Vector.mOfFn fun (i : Fin 0) ↦ g i v)

Tactic:
simp [Vector.mOfFn]

Premises used: List.Vector.mOfFn
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
m : ℕ
g : Fin 0 → List.Vector ℕ m →. ℕ
hg : ∀ (i : Fin 0), ∃ (c : Code), ∀ (v : List.Vector ℕ m), c.eval (↑v : List ℕ) = pure <$> g i v
v : List.Vector ℕ m
⊢ Eq (α := Part (List ℕ)) (Part.some []) (Subtype.val (p := fun (l : List ℕ) ↦ l.length = 0) <$> Part.some Vector.nil)

Tactic:
rfl
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
m : ℕ
g : Fin 0 → List.Vector ℕ m →. ℕ
hg : ∀ (i : Fin 0), ∃ (c : Code), ∀ (v : List.Vector ℕ m), c.eval (↑v : List ℕ) = pure <$> g i v
⊢ ∃ (c : Code),
    ∀ (v : List.Vector ℕ m),
      c.eval (↑v : List ℕ) =
        Functor.map (α := { l : List ℕ // l.length = 0 }) (Subtype.val (p := fun (l : List ℕ) ↦ l.length = 0))
          (Vector.mOfFn fun (i : Fin 0) ↦ g i v)

Tactic:
exact ⟨nil, fun v => by simp [Vector.mOfFn]; rfl⟩
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
m n : ℕ
IH :
  ∀ {g : Fin n → List.Vector ℕ m →. ℕ}
    (hg : ∀ (i : Fin n), ∃ (c : Code), ∀ (v : List.Vector ℕ m), c.eval (↑v : List ℕ) = pure <$> g i v),
    ∃ (c : Code),
      ∀ (v : List.Vector ℕ m),
        c.eval (↑v : List ℕ) =
          Functor.map (α := { l : List ℕ // l.length = n }) (Subtype.val (p := fun (l : List ℕ) ↦ l.length = n))
            (Vector.mOfFn fun (i : Fin n) ↦ g i v)
g : Fin (n + 1) → List.Vector ℕ m →. ℕ
hg : ∀ (i : Fin (n + 1)), ∃ (c : Code), ∀ (v : List.Vector ℕ m), c.eval (↑v : List ℕ) = pure <$> g i v
succ :
  ∀ (cg : Code) (hg₁ : ∀ (v : List.Vector ℕ m), cg.eval (↑v : List ℕ) = pure <$> g 0 v),
    ∃ (c : Code),
      ∀ (v : List.Vector ℕ m),
        c.eval (↑v : List ℕ) =
          Functor.map (α := { l : List ℕ // l.length = n + 1 }) (Subtype.val (p := fun (l : List ℕ) ↦ l.length = n + 1))
            (Vector.mOfFn fun (i : Fin (n + 1)) ↦ g i v)
⊢ ∃ (c : Code),
    ∀ (v : List.Vector ℕ m),
      c.eval (↑v : List ℕ) =
        Functor.map (α := { l : List ℕ // l.length = n + 1 }) (Subtype.val (p := fun (l : List ℕ) ↦ l.length = n + 1))
          (Vector.mOfFn fun (i : Fin (n + 1)) ↦ g i v)

Tactic:
obtain ⟨cg, hg₁⟩ := hg 0

Premises used: OfNat.ofNat
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
m n : ℕ
IH :
  ∀ {g : Fin n → List.Vector ℕ m →. ℕ}
    (hg : ∀ (i : Fin n), ∃ (c : Code), ∀ (v : List.Vector ℕ m), c.eval (↑v : List ℕ) = pure <$> g i v),
    ∃ (c : Code),
      ∀ (v : List.Vector ℕ m),
        c.eval (↑v : List ℕ) =
          Functor.map (α := { l : List ℕ // l.length = n }) (Subtype.val (p := fun (l : List ℕ) ↦ l.length = n))
            (Vector.mOfFn fun (i : Fin n) ↦ g i v)
g : Fin (n + 1) → List.Vector ℕ m →. ℕ
hg : ∀ (i : Fin (n + 1)), ∃ (c : Code), ∀ (v : List.Vector ℕ m), c.eval (↑v : List ℕ) = pure <$> g i v
cg : Code
hg₁ : ∀ (v : List.Vector ℕ m), cg.eval (↑v : List ℕ) = pure <$> g 0 v
succ :
  ∀ (cl : Code)
    (hl :
      ∀ (v : List.Vector ℕ m),
        cl.eval (↑v : List ℕ) =
          Functor.map (α := { l : List ℕ // l.length = n }) (Subtype.val (p := fun (l : List ℕ) ↦ l.length = n))
            (Vector.mOfFn fun (i : Fin n) ↦ g i.succ v)),
    ∃ (c : Code),
      ∀ (v : List.Vector ℕ m),
        c.eval (↑v : List ℕ) =
          Functor.map (α := { l : List ℕ // l.length = n + 1 }) (Subtype.val (p := fun (l : List ℕ) ↦ l.length = n + 1))
            (Vector.mOfFn fun (i : Fin (n + 1)) ↦ g i v)
⊢ ∃ (c : Code),
    ∀ (v : List.Vector ℕ m),
      c.eval (↑v : List ℕ) =
        Functor.map (α := { l : List ℕ // l.length = n + 1 }) (Subtype.val (p := fun (l : List ℕ) ↦ l.length = n + 1))
          (Vector.mOfFn fun (i : Fin (n + 1)) ↦ g i v)

Tactic:
obtain ⟨cl, hl⟩ := IH fun i => hg i.succ

Premises used: Fin.succ
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
m n : ℕ
IH :
  ∀ {g : Fin n → List.Vector ℕ m →. ℕ}
    (hg : ∀ (i : Fin n), ∃ (c : Code), ∀ (v : List.Vector ℕ m), c.eval (↑v : List ℕ) = pure <$> g i v),
    ∃ (c : Code),
      ∀ (v : List.Vector ℕ m),
        c.eval (↑v : List ℕ) =
          Functor.map (α := { l : List ℕ // l.length = n }) (Subtype.val (p := fun (l : List ℕ) ↦ l.length = n))
            (Vector.mOfFn fun (i : Fin n) ↦ g i v)
g : Fin (n + 1) → List.Vector ℕ m →. ℕ
hg : ∀ (i : Fin (n + 1)), ∃ (c : Code), ∀ (v : List.Vector ℕ m), c.eval (↑v : List ℕ) = pure <$> g i v
cg : Code
hg₁ : ∀ (v : List.Vector ℕ m), cg.eval (↑v : List ℕ) = pure <$> g 0 v
cl : Code
hl :
  ∀ (v : List.Vector ℕ m),
    cl.eval (↑v : List ℕ) =
      Functor.map (α := { l : List ℕ // l.length = n }) (Subtype.val (p := fun (l : List ℕ) ↦ l.length = n))
        (Vector.mOfFn fun (i : Fin n) ↦ g i.succ v)
v : List.Vector ℕ m
simp :
  Eq (α := Part (List ℕ))
    (do
      let a ← g 0 v
      let a_1 ← Vector.mOfFn fun (i : Fin n) ↦ g i.succ v
      Part.some (a :: (↑a_1 : List ℕ)))
    (Functor.map (α := { l : List ℕ // l.length = n + 1 }) (Subtype.val (p := fun (l : List ℕ) ↦ l.length = n + 1)) do
      let a ← g 0 v
      let v ← Vector.mOfFn fun (i : Fin n) ↦ g i.succ v
      Part.some (a ::ᵥ v))
⊢ (cg.cons cl).eval (↑v : List ℕ) =
    Functor.map (α := { l : List ℕ // l.length = n + 1 }) (Subtype.val (p := fun (l : List ℕ) ↦ l.length = n + 1))
      (Vector.mOfFn fun (i : Fin (n + 1)) ↦ g i v)

Tactic:
simp [Vector.mOfFn, hg₁, hl]

Premises used: List.Vector.mOfFn
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
m n : ℕ
IH :
  ∀ {g : Fin n → List.Vector ℕ m →. ℕ}
    (hg : ∀ (i : Fin n), ∃ (c : Code), ∀ (v : List.Vector ℕ m), c.eval (↑v : List ℕ) = pure <$> g i v),
    ∃ (c : Code),
      ∀ (v : List.Vector ℕ m),
        c.eval (↑v : List ℕ) =
          Functor.map (α := { l : List ℕ // l.length = n }) (Subtype.val (p := fun (l : List ℕ) ↦ l.length = n))
            (Vector.mOfFn fun (i : Fin n) ↦ g i v)
g : Fin (n + 1) → List.Vector ℕ m →. ℕ
hg : ∀ (i : Fin (n + 1)), ∃ (c : Code), ∀ (v : List.Vector ℕ m), c.eval (↑v : List ℕ) = pure <$> g i v
cg : Code
hg₁ : ∀ (v : List.Vector ℕ m), cg.eval (↑v : List ℕ) = pure <$> g 0 v
cl : Code
hl :
  ∀ (v : List.Vector ℕ m),
    cl.eval (↑v : List ℕ) =
      Functor.map (α := { l : List ℕ // l.length = n }) (Subtype.val (p := fun (l : List ℕ) ↦ l.length = n))
        (Vector.mOfFn fun (i : Fin n) ↦ g i.succ v)
v : List.Vector ℕ m
⊢ Eq (α := Part (List ℕ))
    (do
      let a ← g 0 v
      let a_1 ← Vector.mOfFn fun (i : Fin n) ↦ g i.succ v
      Part.some (a :: (↑a_1 : List ℕ)))
    (Functor.map (α := { l : List ℕ // l.length = n + 1 }) (Subtype.val (p := fun (l : List ℕ) ↦ l.length = n + 1)) do
      let a ← g 0 v
      let v ← Vector.mOfFn fun (i : Fin n) ↦ g i.succ v
      Part.some (a ::ᵥ v))

Tactic:
rfl
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
m n : ℕ
IH :
  ∀ {g : Fin n → List.Vector ℕ m →. ℕ}
    (hg : ∀ (i : Fin n), ∃ (c : Code), ∀ (v : List.Vector ℕ m), c.eval (↑v : List ℕ) = pure <$> g i v),
    ∃ (c : Code),
      ∀ (v : List.Vector ℕ m),
        c.eval (↑v : List ℕ) =
          Functor.map (α := { l : List ℕ // l.length = n }) (Subtype.val (p := fun (l : List ℕ) ↦ l.length = n))
            (Vector.mOfFn fun (i : Fin n) ↦ g i v)
g : Fin (n + 1) → List.Vector ℕ m →. ℕ
hg : ∀ (i : Fin (n + 1)), ∃ (c : Code), ∀ (v : List.Vector ℕ m), c.eval (↑v : List ℕ) = pure <$> g i v
cg : Code
hg₁ : ∀ (v : List.Vector ℕ m), cg.eval (↑v : List ℕ) = pure <$> g 0 v
cl : Code
hl :
  ∀ (v : List.Vector ℕ m),
    cl.eval (↑v : List ℕ) =
      Functor.map (α := { l : List ℕ // l.length = n }) (Subtype.val (p := fun (l : List ℕ) ↦ l.length = n))
        (Vector.mOfFn fun (i : Fin n) ↦ g i.succ v)
⊢ ∃ (c : Code),
    ∀ (v : List.Vector ℕ m),
      c.eval (↑v : List ℕ) =
        Functor.map (α := { l : List ℕ // l.length = n + 1 }) (Subtype.val (p := fun (l : List ℕ) ↦ l.length = n + 1))
          (Vector.mOfFn fun (i : Fin (n + 1)) ↦ g i v)

Tactic:
exact
      ⟨cons cg cl, fun v => by
        simp [Vector.mOfFn, hg₁, hl]
        rfl⟩
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
m n : ℕ
g : Fin n → List.Vector ℕ m →. ℕ
hg : ∀ (i : Fin n), ∃ (c : Code), ∀ (v : List.Vector ℕ m), c.eval (↑v : List ℕ) = pure <$> g i v
zero :
  ∀ {g : Fin 0 → List.Vector ℕ m →. ℕ}
    (hg : ∀ (i : Fin 0), ∃ (c : Code), ∀ (v : List.Vector ℕ m), c.eval (↑v : List ℕ) = pure <$> g i v),
    ∃ (c : Code),
      ∀ (v : List.Vector ℕ m),
        c.eval (↑v : List ℕ) =
          Functor.map (α := { l : List ℕ // l.length = 0 }) (Subtype.val (p := fun (l : List ℕ) ↦ l.length = 0))
            (Vector.mOfFn fun (i : Fin 0) ↦ g i v)
succ :
  ∀ (n : ℕ)
    (IH :
      ∀ {g : Fin n → List.Vector ℕ m →. ℕ}
        (hg : ∀ (i : Fin n), ∃ (c : Code), ∀ (v : List.Vector ℕ m), c.eval (↑v : List ℕ) = pure <$> g i v),
        ∃ (c : Code),
          ∀ (v : List.Vector ℕ m),
            c.eval (↑v : List ℕ) =
              Functor.map (α := { l : List ℕ // l.length = n }) (Subtype.val (p := fun (l : List ℕ) ↦ l.length = n))
                (Vector.mOfFn fun (i : Fin n) ↦ g i v))
    {g : Fin (n + 1) → List.Vector ℕ m →. ℕ}
    (hg : ∀ (i : Fin (n + 1)), ∃ (c : Code), ∀ (v : List.Vector ℕ m), c.eval (↑v : List ℕ) = pure <$> g i v),
    ∃ (c : Code),
      ∀ (v : List.Vector ℕ m),
        c.eval (↑v : List ℕ) =
          Functor.map (α := { l : List ℕ // l.length = n + 1 }) (Subtype.val (p := fun (l : List ℕ) ↦ l.length = n + 1))
            (Vector.mOfFn fun (i : Fin (n + 1)) ↦ g i v)
⊢ ∃ (c : Code),
    ∀ (v : List.Vector ℕ m),
      c.eval (↑v : List ℕ) =
        Functor.map (α := { l : List ℕ // l.length = n }) (Subtype.val (p := fun (l : List ℕ) ↦ l.length = n))
          (Vector.mOfFn fun (i : Fin n) ↦ g i v)

Tactic:
induction n with
  | zero => exact ⟨nil, fun v => by simp [Vector.mOfFn]; rfl⟩
  | succ n IH =>
    obtain ⟨cg, hg₁⟩ := hg 0
    obtain ⟨cl, hl⟩ := IH fun i => hg i.succ
    exact
      ⟨cons cg cl, fun v => by
        simp [Vector.mOfFn, hg₁, hl]
        rfl⟩

Premises used: Turing.ToPartrec.Code.succ, Turing.ToPartrec.Code.zero
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
n : ℕ
f : List.Vector ℕ n →. ℕ
n_1 : ℕ
f_1 : List.Vector ℕ n_1 → ℕ
⊢ ∃ (c : Code),
    ∀ (v : List.Vector ℕ 0), c.eval (↑v : List ℕ) = pure <$> (↑fun (x : List.Vector ℕ 0) ↦ 0 : List.Vector ℕ 0 →. ℕ) v

Tactic:
⟨zero', fun ⟨[], _⟩ => rfl⟩

Premises used: Pure.pure, Turing.ToPartrec.Code.eval, Exists.intro, Turing.ToPartrec.Code.zero', PFun.lift, _private.0.Turing.ToPartrec.Code.exists_code.match_1, OfNat.ofNat, Subtype.val, Eq, Functor.map, rfl
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
n : ℕ
f : List.Vector ℕ n →. ℕ
n_1 : ℕ
f_1 : List.Vector ℕ n_1 → ℕ
⊢ ∃ (c : Code),
    ∀ (v : List.Vector ℕ 0), c.eval (↑v : List ℕ) = pure <$> (↑fun (x : List.Vector ℕ 0) ↦ 0 : List.Vector ℕ 0 →. ℕ) v

Tactic:
exact ⟨zero', fun ⟨[], _⟩ => rfl⟩
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
n : ℕ
f : List.Vector ℕ n →. ℕ
n_1 : ℕ
f_1 : List.Vector ℕ n_1 → ℕ
⊢ ∃ (c : Code),
    ∀ (v : List.Vector ℕ 1),
      c.eval (↑v : List ℕ) = pure <$> (↑fun (v : List.Vector ℕ 1) ↦ v.head.succ : List.Vector ℕ 1 →. ℕ) v

Tactic:
⟨succ, fun ⟨[v], _⟩ => rfl⟩

Premises used: Pure.pure, List.Vector.head, Turing.ToPartrec.Code.eval, Turing.ToPartrec.Code.succ, _private.0.Turing.ToPartrec.Code.exists_code.match_2, Exists.intro, PFun.lift, Subtype.val, Nat.succ, Eq, Functor.map, rfl
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
n : ℕ
f : List.Vector ℕ n →. ℕ
n_1 : ℕ
f_1 : List.Vector ℕ n_1 → ℕ
⊢ ∃ (c : Code),
    ∀ (v : List.Vector ℕ 1),
      c.eval (↑v : List ℕ) = pure <$> (↑fun (v : List.Vector ℕ 1) ↦ v.head.succ : List.Vector ℕ 1 →. ℕ) v

Tactic:
exact ⟨succ, fun ⟨[v], _⟩ => rfl⟩
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
n : ℕ
f : List.Vector ℕ n →. ℕ
n_1 : ℕ
f_1 : List.Vector ℕ n_1 → ℕ
n_2 : ℕ
i : Fin n_2
⊢ ∃ (c : Code),
    ∀ (v : List.Vector ℕ n_2),
      c.eval (↑v : List ℕ) = pure <$> (↑fun (v : List.Vector ℕ n_2) ↦ v.get i : List.Vector ℕ n_2 →. ℕ) v

Tactic:
Fin.succRec (fun n => ?_) (fun n i IH => ?_) i

Premises used: Fin.succRec
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
n : ℕ
f : List.Vector ℕ n →. ℕ
n_1 : ℕ
f_1 : List.Vector ℕ n_1 → ℕ
n_2 : ℕ
i : Fin n_2
prim :
  ∀ (n : ℕ),
    ∃ (c : Code),
      ∀ (v : List.Vector ℕ n.succ),
        c.eval (↑v : List ℕ) = pure <$> (↑fun (v : List.Vector ℕ n.succ) ↦ v.get 0 : List.Vector ℕ n.succ →. ℕ) v
prim₁ :
  ∀ (n : ℕ) (i : Fin n)
    (IH :
      ∃ (c : Code),
        ∀ (v : List.Vector ℕ n),
          c.eval (↑v : List ℕ) = pure <$> (↑fun (v : List.Vector ℕ n) ↦ v.get i : List.Vector ℕ n →. ℕ) v),
    ∃ (c : Code),
      ∀ (v : List.Vector ℕ n.succ),
        c.eval (↑v : List ℕ) = pure <$> (↑fun (v : List.Vector ℕ n.succ) ↦ v.get i.succ : List.Vector ℕ n.succ →. ℕ) v
⊢ ∃ (c : Code),
    ∀ (v : List.Vector ℕ n_2),
      c.eval (↑v : List ℕ) = pure <$> (↑fun (v : List.Vector ℕ n_2) ↦ v.get i : List.Vector ℕ n_2 →. ℕ) v

Tactic:
refine Fin.succRec (fun n => ?_) (fun n i IH => ?_) i
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
n_1 : ℕ
f : List.Vector ℕ n_1 →. ℕ
n_2 : ℕ
f_1 : List.Vector ℕ n_2 → ℕ
n_3 : ℕ
i : Fin n_3
n : ℕ
x : List.Vector ℕ n.succ
a : ℕ
as : List ℕ
property : (a :: as).length = n.succ
simp :
  Part.some [a] =
    pure <$>
      Part.some (List.Vector.head (n := n) (Subtype.mk (p := fun (l : List ℕ) ↦ l.length = n + 1) (a :: as) property))
⊢ head.eval (↑(Subtype.mk (p := fun (l : List ℕ) ↦ l.length = n.succ) (a :: as) property) : List ℕ) =
    pure <$>
      (↑fun (v : List.Vector ℕ n.succ) ↦ v.get 0 : List.Vector ℕ n.succ →. ℕ)
        (Subtype.mk (p := fun (l : List ℕ) ↦ l.length = n.succ) (a :: as) property)

Tactic:
simp
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
n_1 : ℕ
f : List.Vector ℕ n_1 →. ℕ
n_2 : ℕ
f_1 : List.Vector ℕ n_2 → ℕ
n_3 : ℕ
i : Fin n_3
n : ℕ
x : List.Vector ℕ n.succ
a : ℕ
as : List ℕ
property : (a :: as).length = n.succ
⊢ Part.some [a] =
    pure <$>
      Part.some (List.Vector.head (n := n) (Subtype.mk (p := fun (l : List ℕ) ↦ l.length = n + 1) (a :: as) property))

Tactic:
rfl
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
n_1 : ℕ
f : List.Vector ℕ n_1 →. ℕ
n_2 : ℕ
f_1 : List.Vector ℕ n_2 → ℕ
n_3 : ℕ
i : Fin n_3
n : ℕ
⊢ ∃ (c : Code),
    ∀ (v : List.Vector ℕ n.succ),
      c.eval (↑v : List ℕ) = pure <$> (↑fun (v : List.Vector ℕ n.succ) ↦ v.get 0 : List.Vector ℕ n.succ →. ℕ) v

Tactic:
exact ⟨head, fun ⟨List.cons a as, _⟩ => by simp; rfl⟩
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
n_1 : ℕ
f : List.Vector ℕ n_1 →. ℕ
n_2 : ℕ
f_1 : List.Vector ℕ n_2 → ℕ
n_3 : ℕ
i_1 : Fin n_3
n : ℕ
i : Fin n
IH :
  ∃ (c : Code),
    ∀ (v : List.Vector ℕ n),
      c.eval (↑v : List ℕ) = pure <$> (↑fun (v : List.Vector ℕ n) ↦ v.get i : List.Vector ℕ n →. ℕ) v
prim :
  ∀ (c : Code)
    (h :
      ∀ (v : List.Vector ℕ n),
        c.eval (↑v : List ℕ) = pure <$> (↑fun (v : List.Vector ℕ n) ↦ v.get i : List.Vector ℕ n →. ℕ) v),
    ∃ (c : Code),
      ∀ (v : List.Vector ℕ n.succ),
        c.eval (↑v : List ℕ) = pure <$> (↑fun (v : List.Vector ℕ n.succ) ↦ v.get i.succ : List.Vector ℕ n.succ →. ℕ) v
⊢ ∃ (c : Code),
    ∀ (v : List.Vector ℕ n.succ),
      c.eval (↑v : List ℕ) = pure <$> (↑fun (v : List.Vector ℕ n.succ) ↦ v.get i.succ : List.Vector ℕ n.succ →. ℕ) v

Tactic:
obtain ⟨c, h⟩ := IH
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
n_1 : ℕ
f : List.Vector ℕ n_1 →. ℕ
n_2 : ℕ
f_1 : List.Vector ℕ n_2 → ℕ
n_3 : ℕ
i_1 : Fin n_3
n : ℕ
i : Fin n
c : Code
h :
  ∀ (v : List.Vector ℕ n),
    c.eval (↑v : List ℕ) = pure <$> (↑fun (v : List.Vector ℕ n) ↦ v.get i : List.Vector ℕ n →. ℕ) v
v : List.Vector ℕ n.succ
⊢ (c.comp tail).eval (↑v : List ℕ) =
    pure <$> (↑fun (v : List.Vector ℕ n.succ) ↦ v.get i.succ : List.Vector ℕ n.succ →. ℕ) v

Tactic:
simpa [← Vector.get_tail, Bind.bind] using h v.tail

Premises used: List.Vector.get_tail, Bind.bind, List.Vector.tail
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
n_1 : ℕ
f : List.Vector ℕ n_1 →. ℕ
n_2 : ℕ
f_1 : List.Vector ℕ n_2 → ℕ
n_3 : ℕ
i_1 : Fin n_3
n : ℕ
i : Fin n
c : Code
h :
  ∀ (v : List.Vector ℕ n),
    c.eval (↑v : List ℕ) = pure <$> (↑fun (v : List.Vector ℕ n) ↦ v.get i : List.Vector ℕ n →. ℕ) v
⊢ ∃ (c : Code),
    ∀ (v : List.Vector ℕ n.succ),
      c.eval (↑v : List ℕ) = pure <$> (↑fun (v : List.Vector ℕ n.succ) ↦ v.get i.succ : List.Vector ℕ n.succ →. ℕ) v

Tactic:
exact ⟨c.comp tail, fun v => by simpa [← Vector.get_tail, Bind.bind] using h v.tail⟩
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
n : ℕ
f : List.Vector ℕ n →. ℕ
n_1 : ℕ
f_1 : List.Vector ℕ n_1 → ℕ
m n_2 : ℕ
f_2 : List.Vector ℕ n_2 → ℕ
g : Fin n_2 → List.Vector ℕ m → ℕ
hf : Nat.Primrec' f_2
hg : ∀ (i : Fin n_2), Nat.Primrec' (g i)
IHf : ∃ (c : Code), ∀ (v : List.Vector ℕ n_2), c.eval (↑v : List ℕ) = pure <$> (↑f_2 : List.Vector ℕ n_2 →. ℕ) v
IHg :
  ∀ (i : Fin n_2),
    ∃ (c : Code), ∀ (v : List.Vector ℕ m), c.eval (↑v : List ℕ) = pure <$> (↑(g i) : List.Vector ℕ m →. ℕ) v
⊢ ∃ (c : Code),
    ∀ (v : List.Vector ℕ m),
      c.eval (↑v : List ℕ) =
        pure <$>
          (↑fun (a : List.Vector ℕ m) ↦ f_2 (List.Vector.ofFn fun (i : Fin n_2) ↦ g i a) : List.Vector ℕ m →. ℕ) v

Tactic:
simpa [Part.bind_eq_bind] using exists_code.comp IHf IHg

Premises used: Turing.ToPartrec.Code.exists_code.comp, Part.bind_eq_bind
-- 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
IHf : ∃ (c : Code), ∀ (v : List.Vector ℕ n), c.eval (↑v : List ℕ) = pure <$> (↑f : List.Vector ℕ n →. ℕ) v
IHg : ∃ (c : Code), ∀ (v : List.Vector ℕ (n + 2)), c.eval (↑v : List ℕ) = pure <$> (↑g : List.Vector ℕ (n + 2) →. ℕ) v
prim :
  ∀ (cf : Code) (hf : ∀ (v : List.Vector ℕ n), cf.eval (↑v : List ℕ) = pure <$> (↑f : List.Vector ℕ n →. ℕ) 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
⊢ ∃ (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:
obtain ⟨cf, hf⟩ := IHf
-- 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
IHg : ∃ (c : Code), ∀ (v : List.Vector ℕ (n + 2)), c.eval (↑v : List ℕ) = pure <$> (↑g : List.Vector ℕ (n + 2) →. ℕ) v
cf : Code
hf : ∀ (v : List.Vector ℕ n), cf.eval (↑v : List ℕ) = pure <$> (↑f : List.Vector ℕ n →. ℕ) v
prim :
  ∀ (cg : Code)
    (hg : ∀ (v : List.Vector ℕ (n + 2)), cg.eval (↑v : List ℕ) = pure <$> (↑g : List.Vector ℕ (n + 2) →. ℕ) 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
⊢ ∃ (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:
obtain ⟨cg, hg⟩ := IHg
-- 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 : Code
hf : ∀ (v : List.Vector ℕ n), cf.eval (↑v : List ℕ) = pure <$> (↑f : List.Vector ℕ n →. ℕ) v
cg : Code
hg : ∀ (v : List.Vector ℕ (n + 2)), cg.eval (↑v : List ℕ) = pure <$> (↑g : List.Vector ℕ (n + 2) →. ℕ) v
⊢ ∀ (v : List.Vector ℕ n), cf.eval (↑v : List ℕ) = Part.some (pure (f v))

Tactic:
simp only [Part.map_eq_map, Part.map_some, PFun.coe_val] at hf hg

Premises used: PFun.coe_val, Part.map_eq_map, Part.map_some
-- 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 : Code
hf : ∀ (v : List.Vector ℕ n), cf.eval (↑v : List ℕ) = pure <$> (↑f : List.Vector ℕ n →. ℕ) v
cg : Code
hg : ∀ (v : List.Vector ℕ (n + 2)), cg.eval (↑v : List ℕ) = pure <$> (↑g : List.Vector ℕ (n + 2) →. ℕ) v
hf₁ : ∀ (v : List.Vector ℕ n), cf.eval (↑v : List ℕ) = Part.some (pure (f v))
⊢ ∀ (v : List.Vector ℕ (n + 2)), cg.eval (↑v : List ℕ) = Part.some (pure (g v))

Tactic:
simp only [Part.map_eq_map, Part.map_some, PFun.coe_val] at hf hg

Premises used: PFun.coe_val, Part.map_eq_map, Part.map_some