awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Computability.Partrec
Goal:
f f_1 g : ℕ → ℕ
h : Nat.Primrec f_1
h_1 : Nat.Primrec g
pf : Nat.Partrec (↑f_1 : ℕ →. ℕ)
pg : Nat.Partrec (↑g : ℕ →. ℕ)
n : ℕ
prec :
  ∀ (x : ℕ),
    Membership.mem (α := ℕ) (γ := Part ℕ)
      (Nat.rec (motive := fun (x : ℕ) ↦ Part ℕ) (Part.some (f_1 (unpair n).1))
          (fun (y : ℕ) (IH : Part ℕ) ↦ IH.bind fun (i : ℕ) ↦ Part.some (g (Nat.pair (unpair n).1 (Nat.pair y i)))) x :
        Part ℕ)
      (Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (f_1 (unpair n).1)
          (fun (y IH : ℕ) ↦ g (Nat.pair (unpair n).1 (Nat.pair y IH))) x :
        ℕ)
⊢ Membership.mem (α := ℕ) (γ := Part ℕ)
    (Nat.rec (motive := fun (x : ℕ) ↦ Part ℕ) (Part.some (f_1 (unpair n).1))
        (fun (y : ℕ) (IH : Part ℕ) ↦ IH.bind fun (i : ℕ) ↦ Part.some (g (Nat.pair (unpair n).1 (Nat.pair y i))))
        (unpair n).2 :
      Part ℕ)
    (Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (f_1 (unpair n).1) (fun (y IH : ℕ) ↦ g (Nat.pair (unpair n).1 (Nat.pair y IH)))
        (unpair n).2 :
      ℕ)

Tactic:
induction n.unpair.2 with
    | zero => simp
    | succ m IH =>
      simp only [mem_bind_iff, mem_some_iff]
      exact ⟨_, IH, rfl⟩

Premises used: Part.mem_bind_iff, Nat.unpair, Part.mem_some_iff, Nat.Partrec.zero, Nat.Partrec.succ, Prod.snd
-- Module: Mathlib.Computability.Partrec
Goal:
f : ℕ → ℕ
hf : Nat.Primrec f
zero : Nat.Partrec (↑fun (x : ℕ) ↦ 0 : ℕ →. ℕ)
succ : Nat.Partrec (↑Nat.succ : ℕ →. ℕ)
left : Nat.Partrec (↑fun (n : ℕ) ↦ (unpair n).1 : ℕ →. ℕ)
right : Nat.Partrec (↑fun (n : ℕ) ↦ (unpair n).2 : ℕ →. ℕ)
pair :
  ∀ {f g : ℕ → ℕ},
    Nat.Primrec f →
      Nat.Primrec g →
        ∀ (pf : Nat.Partrec (↑f : ℕ →. ℕ)) (pg : Nat.Partrec (↑g : ℕ →. ℕ)),
          Nat.Partrec (↑fun (n : ℕ) ↦ Nat.pair (f n) (g n) : ℕ →. ℕ)
comp :
  ∀ {f g : ℕ → ℕ},
    Nat.Primrec f →
      Nat.Primrec g →
        ∀ (pf : Nat.Partrec (↑f : ℕ →. ℕ)) (pg : Nat.Partrec (↑g : ℕ →. ℕ)),
          Nat.Partrec (↑fun (n : ℕ) ↦ f (g n) : ℕ →. ℕ)
prec :
  ∀ {f g : ℕ → ℕ},
    Nat.Primrec f →
      Nat.Primrec g →
        ∀ (pf : Nat.Partrec (↑f : ℕ →. ℕ)) (pg : Nat.Partrec (↑g : ℕ →. ℕ)),
          Nat.Partrec
            (↑(unpaired fun (z n : ℕ) ↦
                  Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (f z) (fun (y IH : ℕ) ↦ g (Nat.pair z (Nat.pair y IH))) n) :
              ℕ →. ℕ)
⊢ Nat.Partrec (↑f : ℕ →. ℕ)

Tactic:
induction hf with
  | zero => exact zero
  | succ => exact succ
  | left => exact left
  | right => exact right
  | pair _ _ pf pg =>
    refine (pf.pair pg).of_eq_tot fun n => ?_
    simp [Seq.seq]
  | comp _ _ pf pg =>
    refine (pf.comp pg).of_eq_tot fun n => (by simp)
  | prec _ _ pf pg =>
    refine (pf.prec pg).of_eq_tot fun n => ?_
    simp only [unpaired, PFun.coe_val, bind_eq_bind]
    induction n.unpair.2 with
    | zero => simp
    | succ m IH =>
      simp only [mem_bind_iff, mem_some_iff]
      exact ⟨_, IH, rfl⟩

Premises used: Part.mem_bind_iff, Nat.Partrec.comp, Nat.Partrec.prec, Part.mem_some_iff, PFun.coe_val, Nat.Partrec.zero, Nat.Partrec.right, Nat.Partrec.pair, Seq.seq, Nat.Partrec.succ, Nat.Partrec.left, Nat.unpaired, Part.bind_eq_bind
-- Module: Mathlib.Computability.Partrec
Goal:
⊢ Nat.Partrec Part.some

Tactic:
of_primrec Primrec.id

Premises used: Nat.Primrec.id, PFun.lift, Nat.Partrec.of_primrec
-- Module: Mathlib.Computability.Partrec
Goal:
x x_1 : ℕ
h_1 : x_1 ∈ Nat.rfind fun (n : ℕ) ↦ (fun (m : ℕ) ↦ decide (m = 0)) <$> (↑fun (x : ℕ) ↦ 1 : ℕ →. ℕ) (Nat.pair x n)
h : (Nat.rfind fun (n : ℕ) ↦ (fun (m : ℕ) ↦ decide (m = 0)) <$> (↑fun (x : ℕ) ↦ 1 : ℕ →. ℕ) (Nat.pair x n)).Dom
h_2 :
  (Nat.rfind fun (n : ℕ) ↦ (fun (m : ℕ) ↦ decide (m = 0)) <$> (↑fun (x : ℕ) ↦ 1 : ℕ →. ℕ) (Nat.pair x n)).get h = x_1
⊢ False

Tactic:
simp at h
-- Module: Mathlib.Computability.Partrec
Goal:
f g h : ℕ →. ℕ
hf : Nat.Partrec f
hg : Nat.Partrec g
hh : Nat.Partrec h
a s : ℕ
⊢ Membership.mem (γ := Part ℕ)
      (Nat.pair <$> Part.some a <*> f a >>=
        unpaired fun (a n : ℕ) ↦
          Nat.rec (motive := fun (x : ℕ) ↦ Part ℕ) (g a)
            (fun (y : ℕ) (IH : Part ℕ) ↦ do
              let i ← IH
              h (Nat.pair a (Nat.pair y i)))
            n)
      s ↔
    Membership.mem (γ := Part ℕ)
      ((f a).bind fun (n : ℕ) ↦
        Nat.rec (motive := fun (x : ℕ) ↦ Part ℕ) (g a)
          (fun (y : ℕ) (IH : Part ℕ) ↦ do
            let i ← IH
            h (Nat.pair a (Nat.pair y i)))
          n)
      s

Tactic:
simp [Seq.seq]

Premises used: Seq.seq
-- Module: Mathlib.Computability.Partrec
Goal:
this : Primrec₂ (σ := ℕ) fun (n m : ℕ) ↦ if n = m.succ then 0 else 1
n : ℕ
zero :
  (Nat.rfind fun (n : ℕ) ↦
      (fun (m : ℕ) ↦ decide (m = 0)) <$>
        (↑(unpaired fun (n m : ℕ) ↦ if n = m.succ then 0 else 1) : ℕ →. ℕ) (Nat.pair 0 n)) =
    (↑(Nat.ppred 0) : Part ℕ)
succ :
  ∀ (n : ℕ),
    (Nat.rfind fun (n_1 : ℕ) ↦
        (fun (m : ℕ) ↦ decide (m = 0)) <$>
          (↑(unpaired fun (n m : ℕ) ↦ if n = m.succ then 0 else 1) : ℕ →. ℕ) (Nat.pair (n + 1) n_1)) =
      (↑(n + 1).ppred : Part ℕ)
⊢ (Nat.rfind fun (n_1 : ℕ) ↦
      (fun (m : ℕ) ↦ decide (m = 0)) <$>
        (↑(unpaired fun (n m : ℕ) ↦ if n = m.succ then 0 else 1) : ℕ →. ℕ) (Nat.pair n n_1)) =
    (↑n.ppred : Part ℕ)

Tactic:
cases n
-- Module: Mathlib.Computability.Partrec
Goal:
this : Primrec₂ (σ := ℕ) fun (n m : ℕ) ↦ if n = m.succ then 0 else 1
⊢ ∀ (a : ℕ),
    a ∉
      Nat.rfind fun (n : ℕ) ↦
        (fun (m : ℕ) ↦ decide (m = 0)) <$>
          (↑(unpaired fun (n m : ℕ) ↦ if n = m.succ then 0 else 1) : ℕ →. ℕ) (Nat.pair 0 n)

Tactic:
simp
-- Module: Mathlib.Computability.Partrec
Goal:
this : Primrec₂ (σ := ℕ) fun (n m : ℕ) ↦ if n = m.succ then 0 else 1
⊢ (Nat.rfind fun (n : ℕ) ↦
      (fun (m : ℕ) ↦ decide (m = 0)) <$>
        (↑(unpaired fun (n m : ℕ) ↦ if n = m.succ then 0 else 1) : ℕ →. ℕ) (Nat.pair 0 n)) =
    (↑(Nat.ppred 0) : Part ℕ)

Tactic:
exact eq_none_iff.2 (by simp)

Premises used: Iff.mpr, Part.eq_none_iff
-- Module: Mathlib.Computability.Partrec
Goal:
this : Primrec₂ (σ := ℕ) fun (n m : ℕ) ↦ if n = m.succ then 0 else 1
n : ℕ
simp : ∀ {m : ℕ}, m < n → ¬n = m
⊢ n ∈
    Nat.rfind fun (n_1 : ℕ) ↦
      (fun (m : ℕ) ↦ decide (m = 0)) <$>
        (↑(unpaired fun (n m : ℕ) ↦ if n = m.succ then 0 else 1) : ℕ →. ℕ) (Nat.pair (n + 1) n_1)

Tactic:
simp
-- Module: Mathlib.Computability.Partrec
Goal:
this : Primrec₂ (σ := ℕ) fun (n m : ℕ) ↦ if n = m.succ then 0 else 1
n : ℕ
⊢ ∀ {m : ℕ}, m < n → ¬n = m

Tactic:
lia
-- Module: Mathlib.Computability.Partrec
Goal:
this : Primrec₂ (σ := ℕ) fun (n m : ℕ) ↦ if n = m.succ then 0 else 1
n : ℕ
⊢ (Nat.rfind fun (n_1 : ℕ) ↦
      (fun (m : ℕ) ↦ decide (m = 0)) <$>
        (↑(unpaired fun (n m : ℕ) ↦ if n = m.succ then 0 else 1) : ℕ →. ℕ) (Nat.pair (n + 1) n_1)) =
    (↑(n + 1).ppred : Part ℕ)

Tactic:
exact eq_some_iff.2 (by simp; lia)

Premises used: Iff.mpr, Part.eq_some_iff
-- Module: Mathlib.Computability.Partrec
Goal:
α : Type u_1
σ : Type u_2
inst : Primcodable α
inst_1 : Primcodable σ
f : α → σ
hf : Primrec f
n : ℕ
simp :
  (↑(encode (Option.map f (decode n))).ppred : Part ℕ) =
    Part.bind (↑(decode n) : Part α) fun (a : α) ↦ Part.some (encode (f a))
⊢ Eq (α := Part ℕ)
    (do
      let n ← (↑fun (n : ℕ) ↦ encode (Option.map f (decode n)) : ℕ →. ℕ) n
      (↑n.ppred : Part ℕ))
    (Part.bind (↑(decode n) : Part α) fun (a : α) ↦ map encode ((↑f : α →. σ) a))

Tactic:
simp
-- Module: Mathlib.Computability.Partrec
Goal:
α : Type u_1
σ : Type u_2
inst : Primcodable α
inst_1 : Primcodable σ
f : α → σ
hf : Primrec f
n : ℕ
none :
  (↑(encode (Option.map f Option.none)).ppred : Part ℕ) =
    Part.bind (↑Option.none : Part α) fun (a : α) ↦ Part.some (encode (f a))
some :
  ∀ (val : α),
    (↑(encode (Option.map f (Option.some val))).ppred : Part ℕ) =
      (↑(Option.some val) : Part α).bind fun (a : α) ↦ Part.some (encode (f a))
⊢ (↑(encode (Option.map f (decode n))).ppred : Part ℕ) =
    Part.bind (↑(decode n) : Part α) fun (a : α) ↦ Part.some (encode (f a))

Tactic:
cases decode (α := α) n

Premises used: Encodable.decode
-- Module: Mathlib.Computability.Partrec
Goal:
α : Type u_1
σ : Type u_2
inst : Primcodable α
inst_1 : Primcodable σ
f : α → σ
hf : Primrec f
n : ℕ
⊢ (↑(encode (Option.map f Option.none)).ppred : Part ℕ) =
    Part.bind (↑Option.none : Part α) fun (a : α) ↦ Part.some (encode (f a))

Tactic:
simp
-- Module: Mathlib.Computability.Partrec
Goal:
α : Type u_1
σ : Type u_2
inst : Primcodable α
inst_1 : Primcodable σ
f : α → σ
hf : Primrec f
n : ℕ
val : α
⊢ (↑(encode (Option.map f (Option.some val))).ppred : Part ℕ) =
    (↑(Option.some val) : Part α).bind fun (a : α) ↦ Part.some (encode (f a))

Tactic:
simp
-- Module: Mathlib.Computability.Partrec
Goal:
α : Type u_1
β : Type u_2
σ : Type u_3
inst : Primcodable α
inst_1 : Primcodable β
inst_2 : Primcodable σ
f : α → β → σ
hf : Primrec₂ f
⊢ Computable₂ f

Tactic:
hf.to_comp

Premises used: Primrec.to_comp, Computable₂
-- Module: Mathlib.Computability.Partrec
Goal:
α : Type u_1
σ : Type u_2
inst : Primcodable α
inst_1 : Primcodable σ
f : α → σ
hf : Computable f
⊢ Partrec (↑f : α →. σ)

Tactic:
hf

Premises used: Computable
-- Module: Mathlib.Computability.Partrec
Goal:
α : Type u_1
β : Type u_2
σ : Type u_3
inst : Primcodable α
inst_1 : Primcodable β
inst_2 : Primcodable σ
f : α → β → σ
hf : Computable₂ f
⊢ Partrec₂.{u_1, u_2, u_3} (β := β) (σ := σ) fun (a : α) ↦ (↑(f a) : β →. σ)

Tactic:
hf

Premises used: PFun.lift, Computable, Partrec₂
-- Module: Mathlib.Computability.Partrec
Goal:
α : Type u_1
σ : Type u_4
inst : Primcodable α
inst_1 : Primcodable σ
f g : α → σ
hf : Computable f
H : ∀ (n : α), f n = g n
⊢ Computable g

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

Premises used: Eq.rec, funext
-- Module: Mathlib.Computability.Partrec
Goal:
α : Type u_1
σ : Type u_4
inst : Primcodable α
inst_1 : Primcodable σ
s : σ
⊢ Computable.{u_1, u_4} (σ := σ) fun (x : α) ↦ s

Tactic:
(Primrec.const _).to_comp

Premises used: Primrec.to_comp, Primrec.const
-- Module: Mathlib.Computability.Partrec
Goal:
α : Type u_1
β : Type u_2
inst : Primcodable α
inst_1 : Primcodable β
f : α → Option β
hf : Computable f
n : ℕ
none :
  Eq (α := Part ℕ)
    (do
      let n ← Part.bind (↑Option.none : Part α) fun (a : α) ↦ map encode ((↑f : α →. Option β) a)
      (↑n.ppred : Part ℕ))
    (Part.bind (↑Option.none : Part α) fun (a : α) ↦ map.{u_2, 0} (α := β) encode ((fun (a : α) ↦ (↑(f a) : Part β)) a))
some :
  ∀ (a : α),
    Eq (α := Part ℕ)
      (do
        let n ← (↑(Option.some a) : Part α).bind fun (a : α) ↦ map encode ((↑f : α →. Option β) a)
        (↑n.ppred : Part ℕ))
      ((↑(Option.some a) : Part α).bind fun (a : α) ↦
        map.{u_2, 0} (α := β) encode ((fun (a : α) ↦ (↑(f a) : Part β)) a))
⊢ Eq (α := Part ℕ)
    (do
      let n ← Part.bind (↑(decode n) : Part α) fun (a : α) ↦ map encode ((↑f : α →. Option β) a)
      (↑n.ppred : Part ℕ))
    (Part.bind (↑(decode n) : Part α) fun (a : α) ↦ map.{u_2, 0} (α := β) encode ((fun (a : α) ↦ (↑(f a) : Part β)) a))

Tactic:
rcases decode (α := α) n with - | a

Premises used: Encodable.decode
-- Module: Mathlib.Computability.Partrec
Goal:
α : Type u_1
β : Type u_2
inst : Primcodable α
inst_1 : Primcodable β
f : α → Option β
hf : Computable f
n : ℕ
⊢ Eq (α := Part ℕ)
    (do
      let n ← Part.bind (↑Option.none : Part α) fun (a : α) ↦ map encode ((↑f : α →. Option β) a)
      (↑n.ppred : Part ℕ))
    (Part.bind (↑Option.none : Part α) fun (a : α) ↦ map.{u_2, 0} (α := β) encode ((fun (a : α) ↦ (↑(f a) : Part β)) a))

Tactic:
simp
-- Module: Mathlib.Computability.Partrec
Goal:
α : Type u_1
β : Type u_2
inst : Primcodable α
inst_1 : Primcodable β
f : α → Option β
hf : Computable f
n : ℕ
a : α
some : (↑(encode (f a)).ppred : Part ℕ) = map encode (↑(f a) : Part β)
⊢ Eq (α := Part ℕ)
    (do
      let n ← (↑(Option.some a) : Part α).bind fun (a : α) ↦ map encode ((↑f : α →. Option β) a)
      (↑n.ppred : Part ℕ))
    ((↑(Option.some a) : Part α).bind fun (a : α) ↦ map.{u_2, 0} (α := β) encode ((fun (a : α) ↦ (↑(f a) : Part β)) a))

Tactic:
simp
-- Module: Mathlib.Computability.Partrec
Goal:
α : Type u_1
β : Type u_2
inst : Primcodable α
inst_1 : Primcodable β
f : α → Option β
hf : Computable f
n : ℕ
a : α
some :
  (↑(encode.{u_2} (α := Option β) Option.none).ppred : Part ℕ) = map.{u_2, 0} (α := β) encode (↑Option.none : Part β)
some₁ : ∀ (val : β), (↑(encode (Option.some val)).ppred : Part ℕ) = map encode (↑(Option.some val) : Part β)
⊢ (↑(encode (f a)).ppred : Part ℕ) = map encode (↑(f a) : Part β)

Tactic:
cases f a
-- Module: Mathlib.Computability.Partrec
Goal:
α : Type u_1
β : Type u_2
inst : Primcodable α
inst_1 : Primcodable β
f : α → Option β
hf : Computable f
n : ℕ
a : α
⊢ (↑(encode.{u_2} (α := Option β) Option.none).ppred : Part ℕ) = map.{u_2, 0} (α := β) encode (↑Option.none : Part β)

Tactic:
simp
-- Module: Mathlib.Computability.Partrec
Goal:
α : Type u_1
β : Type u_2
inst : Primcodable α
inst_1 : Primcodable β
f : α → Option β
hf : Computable f
n : ℕ
a : α
val : β
⊢ (↑(encode (Option.some val)).ppred : Part ℕ) = map encode (↑(Option.some val) : Part β)

Tactic:
simp
-- Module: Mathlib.Computability.Partrec
Goal:
α : Type u_1
β : Type u_2
σ : Type u_4
inst : Primcodable α
inst_1 : Primcodable β
inst_2 : Primcodable σ
f : α × β → σ
hf : Computable f
⊢ Computable₂.{u_1, u_2, u_4} (σ := σ) fun (a : α) (b : β) ↦ f (a, b)

Tactic:
hf.of_eq fun ⟨_, _⟩ => rfl

Premises used: Computable.of_eq, Prod.mk, Prod.fst, Computable₂, _private.0.Computable.to₂.match_1, Eq, Prod.snd, rfl
-- Module: Mathlib.Computability.Partrec
Goal:
α : Type u_1
inst : Primcodable α
⊢ Computable.{u_1, u_1} (α := α) id

Tactic:
Primrec.id.to_comp

Premises used: Primrec.to_comp, Primrec.id
-- Module: Mathlib.Computability.Partrec
Goal:
α : Type u_1
β : Type u_2
inst : Primcodable α
inst_1 : Primcodable β
⊢ Computable (α := α × β) Prod.fst

Tactic:
Primrec.fst.to_comp

Premises used: Primrec.to_comp, Primrec.fst
-- Module: Mathlib.Computability.Partrec
Goal:
α : Type u_1
β : Type u_2
inst : Primcodable α
inst_1 : Primcodable β
⊢ Computable (α := α × β) Prod.snd

Tactic:
Primrec.snd.to_comp

Premises used: Primrec.snd, Primrec.to_comp
-- Module: Mathlib.Computability.Partrec
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Primcodable α
inst_1 : Primcodable β
inst_2 : Primcodable γ
f : α → β
g : α → γ
hf : Computable f
hg : Computable g
n : ℕ
none :
  ((Nat.pair <$> Part.bind (↑Option.none : Part α) fun (a : α) ↦ map encode ((↑f : α →. β) a)) <*>
      Part.bind (↑Option.none : Part α) fun (a : α) ↦ map encode ((↑g : α →. γ) a)) =
    Part.bind (↑Option.none : Part α) fun (a : α) ↦ map (α := β × γ) encode ((↑fun (a : α) ↦ (f a, g a) : α →. β × γ) a)
some :
  ∀ (val : α),
    ((Nat.pair <$> (↑(Option.some val) : Part α).bind fun (a : α) ↦ map encode ((↑f : α →. β) a)) <*>
        (↑(Option.some val) : Part α).bind fun (a : α) ↦ map encode ((↑g : α →. γ) a)) =
      (↑(Option.some val) : Part α).bind fun (a : α) ↦
        map (α := β × γ) encode ((↑fun (a : α) ↦ (f a, g a) : α →. β × γ) a)
⊢ ((Nat.pair <$> Part.bind (↑(decode n) : Part α) fun (a : α) ↦ map encode ((↑f : α →. β) a)) <*>
      Part.bind (↑(decode n) : Part α) fun (a : α) ↦ map encode ((↑g : α →. γ) a)) =
    Part.bind (↑(decode n) : Part α) fun (a : α) ↦ map (α := β × γ) encode ((↑fun (a : α) ↦ (f a, g a) : α →. β × γ) a)

Tactic:
cases decode (α := α) n

Premises used: Encodable.decode
-- Module: Mathlib.Computability.Partrec
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Primcodable α
inst_1 : Primcodable β
inst_2 : Primcodable γ
f : α → β
g : α → γ
hf : Computable f
hg : Computable g
n : ℕ
⊢ ((Nat.pair <$> Part.bind (↑Option.none : Part α) fun (a : α) ↦ map encode ((↑f : α →. β) a)) <*>
      Part.bind (↑Option.none : Part α) fun (a : α) ↦ map encode ((↑g : α →. γ) a)) =
    Part.bind (↑Option.none : Part α) fun (a : α) ↦ map (α := β × γ) encode ((↑fun (a : α) ↦ (f a, g a) : α →. β × γ) a)

Tactic:
simp [Seq.seq]

Premises used: Seq.seq
-- Module: Mathlib.Computability.Partrec
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Primcodable α
inst_1 : Primcodable β
inst_2 : Primcodable γ
f : α → β
g : α → γ
hf : Computable f
hg : Computable g
n : ℕ
val : α
⊢ ((Nat.pair <$> (↑(Option.some val) : Part α).bind fun (a : α) ↦ map encode ((↑f : α →. β) a)) <*>
      (↑(Option.some val) : Part α).bind fun (a : α) ↦ map encode ((↑g : α →. γ) a)) =
    (↑(Option.some val) : Part α).bind fun (a : α) ↦
      map (α := β × γ) encode ((↑fun (a : α) ↦ (f a, g a) : α →. β × γ) a)

Tactic:
simp [Seq.seq]

Premises used: Seq.seq
-- Module: Mathlib.Computability.Partrec
Goal:
⊢ Computable Nat.unpair

Tactic:
Primrec.unpair.to_comp

Premises used: Primrec.to_comp, Primrec.unpair
-- Module: Mathlib.Computability.Partrec
Goal:
⊢ Computable Nat.succ

Tactic:
Primrec.succ.to_comp

Premises used: Primrec.to_comp, Primrec.succ
-- Module: Mathlib.Computability.Partrec
Goal:
⊢ Computable Nat.pred

Tactic:
Primrec.pred.to_comp

Premises used: Primrec.to_comp, Primrec.pred
-- Module: Mathlib.Computability.Partrec
Goal:
⊢ Computable Nat.bodd

Tactic:
Primrec.nat_bodd.to_comp

Premises used: Primrec.to_comp, Primrec.nat_bodd
-- Module: Mathlib.Computability.Partrec
Goal:
⊢ Computable Nat.div2

Tactic:
Primrec.nat_div2.to_comp

Premises used: Primrec.to_comp, Primrec.nat_div2
-- Module: Mathlib.Computability.Partrec
Goal:
α : Type u_1
β : Type u_2
inst : Primcodable α
inst_1 : Primcodable β
⊢ Computable (α := α) (σ := α ⊕ β) Sum.inl

Tactic:
Primrec.sumInl.to_comp

Premises used: Primrec.to_comp, Primrec.sumInl
-- Module: Mathlib.Computability.Partrec
Goal:
α : Type u_1
β : Type u_2
inst : Primcodable α
inst_1 : Primcodable β
⊢ Computable (α := β) (σ := α ⊕ β) Sum.inr

Tactic:
Primrec.sumInr.to_comp

Premises used: Primrec.to_comp, Primrec.sumInr
-- Module: Mathlib.Computability.Partrec
Goal:
α : Type u_1
inst : Primcodable α
⊢ Computable₂.{u_1, u_1, u_1} (α := α) List.cons

Tactic:
Primrec.list_cons.to_comp

Premises used: Primrec.list_cons, Primrec₂.to_comp
-- Module: Mathlib.Computability.Partrec
Goal:
α : Type u_1
inst : Primcodable α
⊢ Computable.{u_1, u_1} (α := List α) List.reverse

Tactic:
Primrec.list_reverse.to_comp

Premises used: Primrec.to_comp, Primrec.list_reverse
-- Module: Mathlib.Computability.Partrec
Goal:
α : Type u_1
inst : Primcodable α
⊢ Computable₂ (σ := Option α) fun (x1 : List α) (x2 : ℕ) ↦
    getElem? (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) x1 x2

Tactic:
Primrec.list_getElem?.to_comp

Premises used: Primrec.list_getElem?, Primrec₂.to_comp
-- Module: Mathlib.Computability.Partrec
Goal:
α : Type u_1
inst : Primcodable α
⊢ Computable₂ (σ := List α) fun (x1 x2 : List α) ↦ x1 ++ x2

Tactic:
Primrec.list_append.to_comp

Premises used: Primrec₂.to_comp, Primrec.list_append
-- Module: Mathlib.Computability.Partrec
Goal:
α : Type u_1
inst : Primcodable α
⊢ Computable₂ (σ := List α) fun (l : List α) (a : α) ↦ l ++ [a]

Tactic:
Primrec.list_concat.to_comp

Premises used: Primrec.list_concat, Primrec₂.to_comp
-- Module: Mathlib.Computability.Partrec
Goal:
α : Type u_1
inst : Primcodable α
⊢ Computable.{u_1, 0} (α := List α) List.length

Tactic:
Primrec.list_length.to_comp

Premises used: Primrec.list_length, Primrec.to_comp
-- Module: Mathlib.Computability.Partrec
Goal:
α : Type u_1
inst : Primcodable α
n : ℕ
⊢ Computable₂.{u_1, u_1, u_1} (α := α) (β := List.Vector α n) Vector.cons

Tactic:
Primrec.vector_cons.to_comp

Premises used: Primrec.vector_cons, Primrec₂.to_comp
-- Module: Mathlib.Computability.Partrec
Goal:
α : Type u_1
inst : Primcodable α
n : ℕ
⊢ Computable.{u_1, u_1} (α := List.Vector α n) List.Vector.toList

Tactic:
Primrec.vector_toList.to_comp

Premises used: Primrec.to_comp, Primrec.vector_toList
-- Module: Mathlib.Computability.Partrec
Goal:
α : Type u_1
inst : Primcodable α
n : ℕ
⊢ Computable.{u_1, 0} (α := List.Vector α n) Vector.length

Tactic:
Primrec.vector_length.to_comp

Premises used: Primrec.to_comp, Primrec.vector_length
-- Module: Mathlib.Computability.Partrec
Goal:
α : Type u_1
inst : Primcodable α
n : ℕ
⊢ Computable.{u_1, u_1} (α := List.Vector α n.succ) List.Vector.head

Tactic:
Primrec.vector_head.to_comp

Premises used: Primrec.to_comp, Primrec.vector_head
-- Module: Mathlib.Computability.Partrec
Goal:
α : Type u_1
inst : Primcodable α
n : ℕ
⊢ Computable.{u_1, u_1} (α := List.Vector α n) List.Vector.tail

Tactic:
Primrec.vector_tail.to_comp

Premises used: Primrec.to_comp, Primrec.vector_tail
-- Module: Mathlib.Computability.Partrec
Goal:
α : Type u_1
inst : Primcodable α
n : ℕ
⊢ Computable₂.{u_1, 0, u_1} (α := List.Vector α n) List.Vector.get

Tactic:
Primrec.vector_get.to_comp

Premises used: Primrec.vector_get, Primrec₂.to_comp
-- Module: Mathlib.Computability.Partrec
Goal:
α : Type u_1
inst : Primcodable α
n : ℕ
⊢ Computable.{u_1, u_1} (α := Fin n → α) List.Vector.ofFn

Tactic:
Primrec.vector_ofFn'.to_comp

Premises used: Primrec.to_comp, Primrec.vector_ofFn'
-- Module: Mathlib.Computability.Partrec
Goal:
σ : Type u_4
inst : Primcodable σ
n : ℕ
⊢ Computable₂.{u_4, 0, u_4} (α := Fin n → σ) id

Tactic:
Primrec.fin_app.to_comp

Premises used: Primrec.fin_app, Primrec₂.to_comp
-- Module: Mathlib.Computability.Partrec
Goal:
α : Type u_1
inst : Primcodable α
⊢ Computable.{u_1, 0} (α := α) encode

Tactic:
Primrec.encode.to_comp

Premises used: Primrec.to_comp, Primrec.encode
-- Module: Mathlib.Computability.Partrec
Goal:
α : Type u_1
inst : Primcodable α
⊢ Computable.{0, u_1} (σ := Option α) decode

Tactic:
Primrec.decode.to_comp

Premises used: Primrec.to_comp, Primrec.decode
-- Module: Mathlib.Computability.Partrec
Goal:
α : Type u_5
inst : Denumerable α
⊢ Computable (ofNat α)

Tactic:
(Primrec.ofNat _).to_comp

Premises used: Primrec.to_comp, Primrec.ofNat
-- Module: Mathlib.Computability.Partrec
Goal:
α : Type u_1
σ : Type u_4
inst : Primcodable α
inst_1 : Primcodable σ
f : α → σ
⊢ (Computable (σ := ℕ) fun (a : α) ↦ encode (f a)) ↔ Computable f

Tactic:
Iff.rfl

Premises used: Part.some, Iff.rfl, PFun.lift, Computable, Partrec, Part.map
-- Module: Mathlib.Computability.Partrec
Goal:
α : Type u_1
inst : Primcodable α
⊢ Computable.{u_1, u_1} (α := α) Option.some

Tactic:
Primrec.option_some.to_comp

Premises used: Primrec.to_comp, Primrec.option_some
-- Module: Mathlib.Computability.Partrec
Goal:
α : Type u_1
σ : Type u_3
inst : Primcodable α
inst_1 : Primcodable σ
f g : α →. σ
hf : Partrec f
H : ∀ (n : α), f n = g n
⊢ Partrec g

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

Premises used: Eq.rec, funext
-- Module: Mathlib.Computability.Partrec
Goal:
α : Type u_1
σ : Type u_3
inst : Primcodable α
inst_1 : Primcodable σ
f : α →. σ
g : α → σ
hf : Partrec f
H : ∀ (n : α), g n ∈ f n
⊢ Computable g

Tactic:
hf.of_eq fun a => eq_some_iff.2 (H a)

Premises used: Iff.mpr, Part.eq_some_iff, Partrec.of_eq, Computable
-- Module: Mathlib.Computability.Partrec
Goal:
α : Type u_1
σ : Type u_3
inst : Primcodable α
inst_1 : Primcodable σ
n : ℕ
none₁ :
  Eq (α := Part ℕ) Part.none
    (Part.bind (↑Option.none : Part α) fun (a : α) ↦
      map.{u_3, 0} (α := σ) encode ((fun (x : α) ↦ (Part.none : Part σ)) a))
some :
  ∀ (val : α),
    Eq (α := Part ℕ) Part.none
      ((↑(Option.some val) : Part α).bind fun (a : α) ↦
        map.{u_3, 0} (α := σ) encode ((fun (x : α) ↦ (Part.none : Part σ)) a))
⊢ Eq (α := Part ℕ) Part.none
    (Part.bind (↑(decode n) : Part α) fun (a : α) ↦
      map.{u_3, 0} (α := σ) encode ((fun (x : α) ↦ (Part.none : Part σ)) a))

Tactic:
cases decode (α := α) n

Premises used: Encodable.decode
-- Module: Mathlib.Computability.Partrec
Goal:
α : Type u_1
σ : Type u_3
inst : Primcodable α
inst_1 : Primcodable σ
n : ℕ
⊢ Eq (α := Part ℕ) Part.none
    (Part.bind (↑Option.none : Part α) fun (a : α) ↦
      map.{u_3, 0} (α := σ) encode ((fun (x : α) ↦ (Part.none : Part σ)) a))

Tactic:
simp
-- Module: Mathlib.Computability.Partrec
Goal:
α : Type u_1
σ : Type u_3
inst : Primcodable α
inst_1 : Primcodable σ
n : ℕ
val : α
⊢ Eq (α := Part ℕ) Part.none
    ((↑(Option.some val) : Part α).bind fun (a : α) ↦
      map.{u_3, 0} (α := σ) encode ((fun (x : α) ↦ (Part.none : Part σ)) a))

Tactic:
simp
-- Module: Mathlib.Computability.Partrec
Goal:
α : Type u_1
inst : Primcodable α
⊢ Partrec.{u_1, u_1} (α := α) Part.some

Tactic:
Computable.id

Premises used: PFun.lift, Computable, Computable.id