awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Computability.Partrec
Goal:
α : Type u_1
inst : Primcodable α
p : α → ℕ →. Bool
hp : Partrec₂ p
n : ℕ
e : Eq.{u_1 + 1} (α := Option α) (decode n) Option.none
⊢ (Nat.rfind fun (n_1 : ℕ) ↦
      (fun (m : ℕ) ↦ decide (m = 0)) <$>
        Part.bind (↑(decode (Nat.pair n n_1)) : Part (α × ℕ)) fun (a : α × ℕ) ↦
          Part.map (α := ℕ) encode
            ((fun (a : α × ℕ) ↦ (Part.map (fun (b : Bool) ↦ bif (a, b).2 then 0 else 1) (p a.1 a.2) : Part ℕ)) a)) =
    Part.bind (↑Option.none : Part α) fun (a : α) ↦ Part.map (α := ℕ) encode ((fun (a : α) ↦ Nat.rfind (p a)) a)

Tactic:
simp [e, Nat.rfind_zero_none, map_map, map_id']

Premises used: Nat.rfind_zero_none, Part.map_map, Part.map_id'
-- Module: Mathlib.Computability.Partrec
Goal:
α : Type u_1
inst : Primcodable α
p : α → ℕ →. Bool
hp : Partrec₂ p
n : ℕ
val : α
e : decode n = Option.some val
⊢ (Nat.rfind fun (n_1 : ℕ) ↦
      (fun (m : ℕ) ↦ decide (m = 0)) <$>
        Part.bind (↑(decode (Nat.pair n n_1)) : Part (α × ℕ)) fun (a : α × ℕ) ↦
          Part.map (α := ℕ) encode
            ((fun (a : α × ℕ) ↦ (Part.map (fun (b : Bool) ↦ bif (a, b).2 then 0 else 1) (p a.1 a.2) : Part ℕ)) a)) =
    (↑(Option.some val) : Part α).bind fun (a : α) ↦ Part.map (α := ℕ) encode ((fun (a : α) ↦ Nat.rfind (p a)) a)

Tactic:
simp [e, Nat.rfind_zero_none, map_map, map_id']

Premises used: Nat.rfind_zero_none, Part.map_map, Part.map_id'
-- Module: Mathlib.Computability.Partrec
Goal:
α : Type u_1
σ : Type u_2
inst : Primcodable α
inst_1 : Primcodable σ
f : α → ℕ → Option σ
hf : Computable₂ f
⊢ Partrec.{u_1, u_2} (α := α) (σ := σ) fun (a : α) ↦ Nat.rfindOpt (f a)

Tactic:
(rfind (Primrec.option_isSome.to_comp.comp hf).partrec.to₂).bind (ofOption hf)

Premises used: Partrec.bind, Primrec.to_comp, Primrec.option_isSome, Computable.ofOption, Computable.comp, Computable.partrec, Partrec.to₂, Nat.rfindOpt, Partrec.rfind, Part.ofOption
-- Module: Mathlib.Computability.Partrec
Goal:
α : Type u_1
σ : Type u_2
inst : Primcodable α
inst_1 : Primcodable σ
f : α → ℕ
g : α → σ
h : α → ℕ →. σ
hf : Computable f
hg : Computable g
hh : Partrec₂ h
a : α
simp :
  Eq.{u_2 + 1} (α := Part σ)
    (Nat.rec (motive := fun (x : ℕ) ↦ Part σ) (Part.some (g a))
        (fun (y : ℕ) (IH : Part σ) ↦ IH.bind fun (i : σ) ↦ h a (f a - 1)) (f a) :
      Part σ)
    (Nat.rec (motive := fun (x : ℕ) ↦ Part σ) (Part.some (g a)) (fun (n : ℕ) (n_ih : Part σ) ↦ h a n) (f a) : Part σ)
⊢ Eq.{u_2 + 1} (α := Part σ)
    (Nat.rec (motive := fun (x : ℕ) ↦ Part σ) ((↑g : α →. σ) a)
        (fun (y : ℕ) (IH : Part σ) ↦ IH.bind fun (i : σ) ↦ h (a, y, i).1 (f (a, y, i).1).pred) (f a) :
      Part σ)
    (Nat.casesOn (motive := fun (x : ℕ) ↦ Part σ) (f a) (Part.some (g a)) (h a) : Part σ)

Tactic:
simp only [PFun.coe_val, Nat.pred_eq_sub_one]

Premises used: PFun.coe_val, Nat.pred_eq_sub_one
-- Module: Mathlib.Computability.Partrec
Goal:
α : Type u_1
σ : Type u_2
inst : Primcodable α
inst_1 : Primcodable σ
f : α → ℕ
g : α → σ
h : α → ℕ →. σ
hf : Computable f
hg : Computable g
hh : Partrec₂ h
a : α
zero :
  Eq.{u_2 + 1} (α := Part σ)
    (Nat.rec (motive := fun (x : ℕ) ↦ Part σ) (Part.some (g a))
        (fun (y : ℕ) (IH : Part σ) ↦ IH.bind fun (i : σ) ↦ h a (HSub.hSub (α := ℕ) 0 1)) 0 :
      Part σ)
    (Nat.rec (motive := fun (x : ℕ) ↦ Part σ) (Part.some (g a)) (fun (n : ℕ) (n_ih : Part σ) ↦ h a n) 0 : Part σ)
succ :
  ∀ (n : ℕ),
    Eq.{u_2 + 1} (α := Part σ)
      (Nat.rec (motive := fun (x : ℕ) ↦ Part σ) (Part.some (g a))
          (fun (y : ℕ) (IH : Part σ) ↦ IH.bind fun (i : σ) ↦ h a (n + 1 - 1)) (n + 1) :
        Part σ)
      (Nat.rec (motive := fun (x : ℕ) ↦ Part σ) (Part.some (g a)) (fun (n : ℕ) (n_ih : Part σ) ↦ h a n) (n + 1) :
        Part σ)
⊢ Eq.{u_2 + 1} (α := Part σ)
    (Nat.rec (motive := fun (x : ℕ) ↦ Part σ) (Part.some (g a))
        (fun (y : ℕ) (IH : Part σ) ↦ IH.bind fun (i : σ) ↦ h a (f a - 1)) (f a) :
      Part σ)
    (Nat.rec (motive := fun (x : ℕ) ↦ Part σ) (Part.some (g a)) (fun (n : ℕ) (n_ih : Part σ) ↦ h a n) (f a) : Part σ)

Tactic:
rcases f a with - | n
-- Module: Mathlib.Computability.Partrec
Goal:
α : Type u_1
σ : Type u_2
inst : Primcodable α
inst_1 : Primcodable σ
f : α → ℕ
g : α → σ
h : α → ℕ →. σ
hf : Computable f
hg : Computable g
hh : Partrec₂ h
a : α
⊢ Eq.{u_2 + 1} (α := Part σ)
    (Nat.rec (motive := fun (x : ℕ) ↦ Part σ) (Part.some (g a))
        (fun (y : ℕ) (IH : Part σ) ↦ IH.bind fun (i : σ) ↦ h a (HSub.hSub (α := ℕ) 0 1)) 0 :
      Part σ)
    (Nat.rec (motive := fun (x : ℕ) ↦ Part σ) (Part.some (g a)) (fun (n : ℕ) (n_ih : Part σ) ↦ h a n) 0 : Part σ)

Tactic:
simp
-- Module: Mathlib.Computability.Partrec
Goal:
α : Type u_1
σ : Type u_2
inst : Primcodable α
inst_1 : Primcodable σ
f : α → ℕ
g : α → σ
h : α → ℕ →. σ
hf : Computable f
hg : Computable g
hh : Partrec₂ h
a : α
n : ℕ
⊢ Eq.{u_2 + 1} (α := Part σ)
    (Nat.rec (motive := fun (x : ℕ) ↦ Part σ) (Part.some (g a))
        (fun (y : ℕ) (IH : Part σ) ↦ IH.bind fun (i : σ) ↦ h a (n + 1 - 1)) (n + 1) :
      Part σ)
    (Nat.rec (motive := fun (x : ℕ) ↦ Part σ) (Part.some (g a)) (fun (n : ℕ) (n_ih : Part σ) ↦ h a n) (n + 1) : Part σ)

Tactic:
ext fun b => ⟨fun H => ?_, fun H => ?_⟩

Premises used: Part.ext, Iff.intro
-- Module: Mathlib.Computability.Partrec
Goal:
α : Type u_1
σ : Type u_2
inst : Primcodable α
inst_1 : Primcodable σ
f : α → ℕ
g : α → σ
h : α → ℕ →. σ
hf : Computable f
hg : Computable g
hh : Partrec₂ h
a : α
n : ℕ
succ :
  ∀ (b : σ)
    (H :
      Membership.mem (γ := Part σ)
        (Nat.rec (motive := fun (x : ℕ) ↦ Part σ) (Part.some (g a))
            (fun (y : ℕ) (IH : Part σ) ↦ IH.bind fun (i : σ) ↦ h a (n + 1 - 1)) (n + 1) :
          Part σ)
        b),
    Membership.mem (γ := Part σ)
      (Nat.rec (motive := fun (x : ℕ) ↦ Part σ) (Part.some (g a)) (fun (n : ℕ) (n_ih : Part σ) ↦ h a n) (n + 1) :
        Part σ)
      b
succ₁ :
  ∀ (b : σ)
    (H :
      Membership.mem (γ := Part σ)
        (Nat.rec (motive := fun (x : ℕ) ↦ Part σ) (Part.some (g a)) (fun (n : ℕ) (n_ih : Part σ) ↦ h a n) (n + 1) :
          Part σ)
        b),
    Membership.mem (γ := Part σ)
      (Nat.rec (motive := fun (x : ℕ) ↦ Part σ) (Part.some (g a))
          (fun (y : ℕ) (IH : Part σ) ↦ IH.bind fun (i : σ) ↦ h a (n + 1 - 1)) (n + 1) :
        Part σ)
      b
⊢ Eq.{u_2 + 1} (α := Part σ)
    (Nat.rec (motive := fun (x : ℕ) ↦ Part σ) (Part.some (g a))
        (fun (y : ℕ) (IH : Part σ) ↦ IH.bind fun (i : σ) ↦ h a (n + 1 - 1)) (n + 1) :
      Part σ)
    (Nat.rec (motive := fun (x : ℕ) ↦ Part σ) (Part.some (g a)) (fun (n : ℕ) (n_ih : Part σ) ↦ h a n) (n + 1) : Part σ)

Tactic:
refine ext fun b => ⟨fun H => ?_, fun H => ?_⟩

Premises used: Part.ext, Iff.intro
-- Module: Mathlib.Computability.Partrec
Goal:
α : Type u_1
σ : Type u_2
inst : Primcodable α
inst_1 : Primcodable σ
f : α → ℕ
g : α → σ
h : α → ℕ →. σ
hf : Computable f
hg : Computable g
hh : Partrec₂ h
a : α
n : ℕ
b : σ
H :
  Membership.mem (γ := Part σ)
    (Nat.rec (motive := fun (x : ℕ) ↦ Part σ) (Part.some (g a))
        (fun (y : ℕ) (IH : Part σ) ↦ IH.bind fun (i : σ) ↦ h a (n + 1 - 1)) (n + 1) :
      Part σ)
    b
succ :
  ∀ (c : σ),
    Membership.mem (γ := Part σ)
        (Nat.rec (motive := fun (x : ℕ) ↦ Part σ) (Part.some (g a))
            (fun (y : ℕ) (IH : Part σ) ↦ IH.bind fun (i : σ) ↦ h a (n + 1 - 1)) n :
          Part σ)
        c →
      ∀ (h₂ : b ∈ h a (n + 1 - 1)),
        Membership.mem (γ := Part σ)
          (Nat.rec (motive := fun (x : ℕ) ↦ Part σ) (Part.some (g a)) (fun (n : ℕ) (n_ih : Part σ) ↦ h a n) (n + 1) :
            Part σ)
          b
⊢ Membership.mem (γ := Part σ)
    (Nat.rec (motive := fun (x : ℕ) ↦ Part σ) (Part.some (g a)) (fun (n : ℕ) (n_ih : Part σ) ↦ h a n) (n + 1) : Part σ)
    b

Tactic:
rcases mem_bind_iff.1 H with ⟨c, _, h₂⟩

Premises used: Part.mem_bind_iff, Iff.mp
-- Module: Mathlib.Computability.Partrec
Goal:
α : Type u_1
σ : Type u_2
inst : Primcodable α
inst_1 : Primcodable σ
f : α → ℕ
g : α → σ
h : α → ℕ →. σ
hf : Computable f
hg : Computable g
hh : Partrec₂ h
a : α
n : ℕ
b : σ
H :
  Membership.mem (γ := Part σ)
    (Nat.rec (motive := fun (x : ℕ) ↦ Part σ) (Part.some (g a))
        (fun (y : ℕ) (IH : Part σ) ↦ IH.bind fun (i : σ) ↦ h a (n + 1 - 1)) (n + 1) :
      Part σ)
    b
c : σ
left :
  Membership.mem (γ := Part σ)
    (Nat.rec (motive := fun (x : ℕ) ↦ Part σ) (Part.some (g a))
        (fun (y : ℕ) (IH : Part σ) ↦ IH.bind fun (i : σ) ↦ h a (n + 1 - 1)) n :
      Part σ)
    c
h₂ : b ∈ h a (n + 1 - 1)
⊢ Membership.mem (γ := Part σ)
    (Nat.rec (motive := fun (x : ℕ) ↦ Part σ) (Part.some (g a)) (fun (n : ℕ) (n_ih : Part σ) ↦ h a n) (n + 1) : Part σ)
    b

Tactic:
h₂

Premises used: Nat.pred
-- Module: Mathlib.Computability.Partrec
Goal:
α : Type u_1
σ : Type u_2
inst : Primcodable α
inst_1 : Primcodable σ
f : α → ℕ
g : α → σ
h : α → ℕ →. σ
hf : Computable f
hg : Computable g
hh : Partrec₂ h
a : α
n : ℕ
b : σ
H :
  Membership.mem (γ := Part σ)
    (Nat.rec (motive := fun (x : ℕ) ↦ Part σ) (Part.some (g a))
        (fun (y : ℕ) (IH : Part σ) ↦ IH.bind fun (i : σ) ↦ h a (n + 1 - 1)) (n + 1) :
      Part σ)
    b
c : σ
left :
  Membership.mem (γ := Part σ)
    (Nat.rec (motive := fun (x : ℕ) ↦ Part σ) (Part.some (g a))
        (fun (y : ℕ) (IH : Part σ) ↦ IH.bind fun (i : σ) ↦ h a (n + 1 - 1)) n :
      Part σ)
    c
h₂ : b ∈ h a (n + 1 - 1)
⊢ Membership.mem (γ := Part σ)
    (Nat.rec (motive := fun (x : ℕ) ↦ Part σ) (Part.some (g a)) (fun (n : ℕ) (n_ih : Part σ) ↦ h a n) (n + 1) : Part σ)
    b

Tactic:
exact h₂
-- Module: Mathlib.Computability.Partrec
Goal:
α : Type u_1
σ : Type u_2
inst : Primcodable α
inst_1 : Primcodable σ
f : α → ℕ
g : α → σ
h : α → ℕ →. σ
hf : Computable f
hg : Computable g
hh : Partrec₂ h
a : α
n : ℕ
b : σ
H :
  Membership.mem (γ := Part σ)
    (Nat.rec (motive := fun (x : ℕ) ↦ Part σ) (Part.some (g a)) (fun (n : ℕ) (n_ih : Part σ) ↦ h a n) (n + 1) : Part σ)
    b
m : ℕ
zero :
  Dom.{u_2} (α := σ)
    (Nat.rec (motive := fun (x : ℕ) ↦ Part σ) (Part.some (g a))
      (fun (y : ℕ) (IH : (fun (x : ℕ) ↦ Part σ) y) ↦ Part.bind IH fun (x : σ) ↦ h a n) 0)
succ :
  ∀ (n_1 : ℕ),
    Dom.{u_2} (α := σ)
        (Nat.rec (motive := fun (x : ℕ) ↦ Part σ) (Part.some (g a))
          (fun (y : ℕ) (IH : (fun (x : ℕ) ↦ Part σ) y) ↦ Part.bind IH fun (x : σ) ↦ h a n) n_1) →
      Dom.{u_2} (α := σ)
        (Nat.rec (motive := fun (x : ℕ) ↦ Part σ) (Part.some (g a))
          (fun (y : ℕ) (IH : (fun (x : ℕ) ↦ Part σ) y) ↦ Part.bind IH fun (x : σ) ↦ h a n) (n_1 + 1))
⊢ Dom.{u_2} (α := σ)
    (Nat.rec (motive := fun (x : ℕ) ↦ Part σ) (Part.some (g a))
      (fun (y : ℕ) (IH : (fun (x : ℕ) ↦ Part σ) y) ↦ Part.bind IH fun (x : σ) ↦ h a n) m)

Tactic:
induction m
-- Module: Mathlib.Computability.Partrec
Goal:
α : Type u_1
σ : Type u_2
inst : Primcodable α
inst_1 : Primcodable σ
f : α → ℕ
g : α → σ
h : α → ℕ →. σ
hf : Computable f
hg : Computable g
hh : Partrec₂ h
a : α
n : ℕ
b : σ
H :
  Membership.mem (γ := Part σ)
    (Nat.rec (motive := fun (x : ℕ) ↦ Part σ) (Part.some (g a)) (fun (n : ℕ) (n_ih : Part σ) ↦ h a n) (n + 1) : Part σ)
    b
⊢ Dom.{u_2} (α := σ)
    (Nat.rec (motive := fun (x : ℕ) ↦ Part σ) (Part.some (g a))
      (fun (y : ℕ) (IH : (fun (x : ℕ) ↦ Part σ) y) ↦ Part.bind IH fun (x : σ) ↦ h a n) 0)

Tactic:
simp [*, H.fst]

Premises used: Exists.fst
-- Module: Mathlib.Computability.Partrec
Goal:
α : Type u_1
σ : Type u_2
inst : Primcodable α
inst_1 : Primcodable σ
f : α → ℕ
g : α → σ
h : α → ℕ →. σ
hf : Computable f
hg : Computable g
hh : Partrec₂ h
a : α
n : ℕ
b : σ
H :
  Membership.mem (γ := Part σ)
    (Nat.rec (motive := fun (x : ℕ) ↦ Part σ) (Part.some (g a)) (fun (n : ℕ) (n_ih : Part σ) ↦ h a n) (n + 1) : Part σ)
    b
n_1 : ℕ
h_1 :
  Dom.{u_2} (α := σ)
    (Nat.rec (motive := fun (x : ℕ) ↦ Part σ) (Part.some (g a))
      (fun (y : ℕ) (IH : (fun (x : ℕ) ↦ Part σ) y) ↦ Part.bind IH fun (x : σ) ↦ h a n) n_1)
⊢ Dom.{u_2} (α := σ)
    (Nat.rec (motive := fun (x : ℕ) ↦ Part σ) (Part.some (g a))
      (fun (y : ℕ) (IH : (fun (x : ℕ) ↦ Part σ) y) ↦ Part.bind IH fun (x : σ) ↦ h a n) (n_1 + 1))

Tactic:
simp [*, H.fst]

Premises used: Exists.fst
-- Module: Mathlib.Computability.Partrec
Goal:
α : Type u_1
σ : Type u_2
inst : Primcodable α
inst_1 : Primcodable σ
f : α → ℕ
g : α → σ
h : α → ℕ →. σ
hf : Computable f
hg : Computable g
hh : Partrec₂ h
a : α
n : ℕ
b : σ
H :
  Membership.mem (γ := Part σ)
    (Nat.rec (motive := fun (x : ℕ) ↦ Part σ) (Part.some (g a)) (fun (n : ℕ) (n_ih : Part σ) ↦ h a n) (n + 1) : Part σ)
    b
⊢ ∀ (m : ℕ),
    Dom.{u_2} (α := σ)
      (Nat.rec (motive := fun (x : ℕ) ↦ Part σ) (Part.some (g a))
        (fun (y : ℕ) (IH : (fun (x : ℕ) ↦ Part σ) y) ↦ Part.bind IH fun (x : σ) ↦ h a n) m)

Tactic:
have : ∀ m, (Nat.rec (motive := fun _ => Part σ)
            (Part.some (g a)) (fun y IH => IH.bind fun _ => h a n) m).Dom := by
          intro m
          induction m <;> simp [*, H.fst]
-- Module: Mathlib.Computability.Partrec
Goal:
α : Type u_1
σ : Type u_2
inst : Primcodable α
inst_1 : Primcodable σ
f : α → ℕ
g : α → σ
h : α → ℕ →. σ
hf : Computable f
hg : Computable g
hh : Partrec₂ h
a : α
n : ℕ
b : σ
H :
  Membership.mem (γ := Part σ)
    (Nat.rec (motive := fun (x : ℕ) ↦ Part σ) (Part.some (g a)) (fun (n : ℕ) (n_ih : Part σ) ↦ h a n) (n + 1) : Part σ)
    b
this :
  ∀ (m : ℕ),
    Dom.{u_2} (α := σ)
      (Nat.rec (motive := fun (x : ℕ) ↦ Part σ) (Part.some (g a))
        (fun (y : ℕ) (IH : (fun (x : ℕ) ↦ Part σ) y) ↦ Part.bind IH fun (x : σ) ↦ h a n) m)
⊢ Membership.mem (γ := Part σ)
    (Nat.rec (motive := fun (x : ℕ) ↦ Part σ) (Part.some (g a))
        (fun (y : ℕ) (IH : Part σ) ↦ IH.bind fun (i : σ) ↦ h a (n + 1 - 1)) (n + 1) :
      Part σ)
    b

Tactic:
⟨⟨this n, H.fst⟩, H.snd⟩

Premises used: Part.Mem, Exists.fst, Exists.snd, Exists.intro
-- Module: Mathlib.Computability.Partrec
Goal:
α : Type u_1
σ : Type u_2
inst : Primcodable α
inst_1 : Primcodable σ
f : α → ℕ
g : α → σ
h : α → ℕ →. σ
hf : Computable f
hg : Computable g
hh : Partrec₂ h
a : α
n : ℕ
b : σ
H :
  Membership.mem (γ := Part σ)
    (Nat.rec (motive := fun (x : ℕ) ↦ Part σ) (Part.some (g a)) (fun (n : ℕ) (n_ih : Part σ) ↦ h a n) (n + 1) : Part σ)
    b
this :
  ∀ (m : ℕ),
    Dom.{u_2} (α := σ)
      (Nat.rec (motive := fun (x : ℕ) ↦ Part σ) (Part.some (g a))
        (fun (y : ℕ) (IH : (fun (x : ℕ) ↦ Part σ) y) ↦ Part.bind IH fun (x : σ) ↦ h a n) m)
⊢ Membership.mem (γ := Part σ)
    (Nat.rec (motive := fun (x : ℕ) ↦ Part σ) (Part.some (g a))
        (fun (y : ℕ) (IH : Part σ) ↦ IH.bind fun (i : σ) ↦ h a (n + 1 - 1)) (n + 1) :
      Part σ)
    b

Tactic:
exact ⟨⟨this n, H.fst⟩, H.snd⟩
-- Module: Mathlib.Computability.Partrec
Goal:
α : Type u_1
σ : Type u_2
inst : Primcodable α
inst_1 : Primcodable σ
f : α →. σ
h : Nat.Partrec fun (n : ℕ) ↦ (↑(decode₂ α n) : Part α).bind fun (a : α) ↦ Part.map encode (f a)
⊢ Partrec.{u_1, 0} (α := α) (σ := ℕ) fun (a : α) ↦ Part.map encode (f a)

Tactic:
simpa [encodek₂] using (nat_iff.2 h).comp (@Computable.encode α _)

Premises used: Iff.mpr, Computable.encode, Partrec.nat_iff, Encodable.encodek₂, Partrec.comp
-- Module: Mathlib.Computability.Partrec
Goal:
α : Type u_1
σ : Type u_2
inst : Primcodable α
inst_1 : Primcodable σ
n : ℕ
f : Fin (n + 1) → α →. σ
hf : ∀ (i : Fin (n + 1)), Partrec (f i)
simp :
  Partrec.{u_1, u_2} (α := α) (σ := List.Vector σ (n + 1)) fun (a : α) ↦
    (f 0 a).bind fun (a_1 : σ) ↦
      Part.bind (Vector.mOfFn fun (i : Fin n) ↦ f i.succ a) fun (v : List.Vector σ n) ↦ Part.some (a_1 ::ᵥ v)
⊢ Partrec.{u_1, u_2} (α := α) (σ := List.Vector σ (n + 1)) fun (a : α) ↦ Vector.mOfFn fun (i : Fin (n + 1)) ↦ f i a

Tactic:
simp only [Vector.mOfFn, pure_eq_some, bind_eq_bind]

Premises used: Part.pure_eq_some, Part.bind_eq_bind, List.Vector.mOfFn
-- Module: Mathlib.Computability.Partrec
Goal:
α : Type u_1
σ : Type u_2
inst : Primcodable α
inst_1 : Primcodable σ
n : ℕ
f : Fin (n + 1) → α →. σ
hf : ∀ (i : Fin (n + 1)), Partrec (f i)
⊢ Partrec.{u_1, u_2} (α := α) (σ := List.Vector σ (n + 1)) fun (a : α) ↦
    (f 0 a).bind fun (a_1 : σ) ↦
      Part.bind (Vector.mOfFn fun (i : Fin n) ↦ f i.succ a) fun (v : List.Vector σ n) ↦ Part.some (a_1 ::ᵥ v)

Tactic:
(hf 0).bind
        (Partrec.bind ((vector_mOfFn fun i => hf i.succ).comp fst)
          (Primrec.vector_cons.to_comp.comp (snd.comp fst) snd))

Premises used: Fin.succ, Partrec.bind, Computable.snd, Computable₂.comp, Computable.comp, Primrec.vector_cons, Computable.fst, OfNat.ofNat, Partrec.comp, Primrec₂.to_comp
-- Module: Mathlib.Computability.Partrec
Goal:
α : Type u_1
σ : Type u_2
inst : Primcodable α
inst_1 : Primcodable σ
n : ℕ
f : Fin (n + 1) → α →. σ
hf : ∀ (i : Fin (n + 1)), Partrec (f i)
⊢ Partrec.{u_1, u_2} (α := α) (σ := List.Vector σ (n + 1)) fun (a : α) ↦
    (f 0 a).bind fun (a_1 : σ) ↦
      Part.bind (Vector.mOfFn fun (i : Fin n) ↦ f i.succ a) fun (v : List.Vector σ n) ↦ Part.some (a_1 ::ᵥ v)

Tactic:
exact
      (hf 0).bind
        (Partrec.bind ((vector_mOfFn fun i => hf i.succ).comp fst)
          (Primrec.vector_cons.to_comp.comp (snd.comp fst) snd))
-- Module: Mathlib.Computability.Partrec
Goal:
α : Type u_1
n : ℕ
⊢ ∀ (f : Fin n → α), (Vector.mOfFn fun (i : Fin n) ↦ Part.some (f i)) = Part.some (List.Vector.ofFn f)

Tactic:
Vector.mOfFn_pure

Premises used: List.Vector.mOfFn_pure
-- Module: Mathlib.Computability.Partrec
Goal:
α : Type u_1
σ : Type u_4
inst : Primcodable α
inst_1 : Primcodable σ
f : α → σ
⊢ (Computable.{u_1, u_4} (σ := Option σ) fun (a : α) ↦ Option.some (f a)) ↔ Computable f

Tactic:
⟨fun h => encode_iff.1 <| Primrec.pred.to_comp.comp <| encode_iff.2 h, option_some.comp⟩

Premises used: Iff.mpr, Computable.encode_iff, Primrec.to_comp, Computable.comp, Computable.option_some, Iff.intro, Iff.mp, Primrec.pred
-- Module: Mathlib.Computability.Partrec
Goal:
α : Type u_1
β : Type u_2
σ : Type u_4
inst : Primcodable α
inst_1 : Primcodable β
inst_2 : Primcodable σ
f : α → β → Option σ
hf : Computable₂.{u_1, 0, u_4} (σ := Option σ) fun (a : α) (n : ℕ) ↦ Option.bind (decode n) (f a)
n : ℕ
simp :
  Eq (α := Part ℕ)
    (Part.bind (↑(Option.bind (decode (Nat.unpair n).1) fun (a : α) ↦ Option.some (a, (Nat.unpair n).2)) : Part (α × ℕ))
      fun (a : α × ℕ) ↦
      (↑(encode.{u_2} (α := Option β) (decode a.2)).ppred : Part ℕ).bind fun (y : ℕ) ↦
        Part.some (encode.{u_4} (α := Option σ) (Option.bind (decode a.2) fun (a_1 : β) ↦ f a.1 a_1)))
    (Part.bind
      (↑(Option.bind (decode (Nat.unpair n).1) fun (a : α) ↦ Option.map (Prod.mk a) (decode (Nat.unpair n).2)) :
        Part (α × β))
      fun (a : α × β) ↦ Part.some (encode (f a.1 a.2)))
⊢ Eq (α := Part ℕ)
    (Part.bind (↑(decode n) : Part (α × ℕ)) fun (a : α × ℕ) ↦
      map.{u_4, 0} (α := Option σ) encode
        ((fun (a : α × ℕ) ↦
            (Part.bind (α := ℕ)
                (do
                  let n ← (↑fun (n : ℕ) ↦ encode.{u_2} (α := Option β) (decode n) : ℕ →. ℕ) a.2
                  (↑n.ppred : Part ℕ))
                (↑fun (b : ℕ) ↦ (fun (a : α) (n : ℕ) ↦ Option.bind (decode n) (f a)) (a, b).1.1 (a, b).1.2 :
                  ℕ →. Option σ) :
              Part (Option σ)))
          a))
    (Part.bind (↑(decode n) : Part (α × β)) fun (a : α × β) ↦
      map.{u_4, 0} (α := Option σ) encode ((↑fun (p : α × β) ↦ f p.1 p.2 : α × β →. Option σ) a))

Tactic:
simp only [decode_prod_val, decode_nat, Option.map_some, PFun.coe_val, bind_eq_bind,
          bind_some, Part.map_bind, map_some]

Premises used: Part.map_bind, Part.bind_some, PFun.coe_val, Part.map_some, Option.map_some, Encodable.decode_prod_val, Encodable.decode_nat, Part.bind_eq_bind
-- Module: Mathlib.Computability.Partrec
Goal:
α : Type u_1
β : Type u_2
σ : Type u_4
inst : Primcodable α
inst_1 : Primcodable β
inst_2 : Primcodable σ
f : α → β → Option σ
hf : Computable₂.{u_1, 0, u_4} (σ := Option σ) fun (a : α) (n : ℕ) ↦ Option.bind (decode n) (f a)
n : ℕ
none :
  Eq (α := Part ℕ)
    (Part.bind (↑(Option.bind Option.none fun (a : α) ↦ Option.some (a, (Nat.unpair n).2)) : Part (α × ℕ))
      fun (a : α × ℕ) ↦
      (↑(encode.{u_2} (α := Option β) (decode a.2)).ppred : Part ℕ).bind fun (y : ℕ) ↦
        Part.some (encode.{u_4} (α := Option σ) (Option.bind (decode a.2) fun (a_1 : β) ↦ f a.1 a_1)))
    (Part.bind
      (↑(Option.bind Option.none fun (a : α) ↦ Option.map (Prod.mk a) (decode (Nat.unpair n).2)) : Part (α × β))
      fun (a : α × β) ↦ Part.some (encode (f a.1 a.2)))
some :
  ∀ (val : α),
    Eq (α := Part ℕ)
      (Part.bind (↑((Option.some val).bind fun (a : α) ↦ Option.some (a, (Nat.unpair n).2)) : Part (α × ℕ))
        fun (a : α × ℕ) ↦
        (↑(encode.{u_2} (α := Option β) (decode a.2)).ppred : Part ℕ).bind fun (y : ℕ) ↦
          Part.some (encode.{u_4} (α := Option σ) (Option.bind (decode a.2) fun (a_1 : β) ↦ f a.1 a_1)))
      (Part.bind
        (↑((Option.some val).bind fun (a : α) ↦ Option.map (Prod.mk a) (decode (Nat.unpair n).2)) : Part (α × β))
        fun (a : α × β) ↦ Part.some (encode (f a.1 a.2)))
⊢ Eq (α := Part ℕ)
    (Part.bind (↑(Option.bind (decode (Nat.unpair n).1) fun (a : α) ↦ Option.some (a, (Nat.unpair n).2)) : Part (α × ℕ))
      fun (a : α × ℕ) ↦
      (↑(encode.{u_2} (α := Option β) (decode a.2)).ppred : Part ℕ).bind fun (y : ℕ) ↦
        Part.some (encode.{u_4} (α := Option σ) (Option.bind (decode a.2) fun (a_1 : β) ↦ f a.1 a_1)))
    (Part.bind
      (↑(Option.bind (decode (Nat.unpair n).1) fun (a : α) ↦ Option.map (Prod.mk a) (decode (Nat.unpair n).2)) :
        Part (α × β))
      fun (a : α × β) ↦ Part.some (encode (f a.1 a.2)))

Tactic:
cases decode (α := α) n.unpair.1

Premises used: Nat.unpair, Prod.fst, Encodable.decode
-- Module: Mathlib.Computability.Partrec
Goal:
α : Type u_1
β : Type u_2
σ : Type u_4
inst : Primcodable α
inst_1 : Primcodable β
inst_2 : Primcodable σ
f : α → β → Option σ
hf : Computable₂.{u_1, 0, u_4} (σ := Option σ) fun (a : α) (n : ℕ) ↦ Option.bind (decode n) (f a)
n : ℕ
⊢ Eq (α := Part ℕ)
    (Part.bind (↑(Option.bind Option.none fun (a : α) ↦ Option.some (a, (Nat.unpair n).2)) : Part (α × ℕ))
      fun (a : α × ℕ) ↦
      (↑(encode.{u_2} (α := Option β) (decode a.2)).ppred : Part ℕ).bind fun (y : ℕ) ↦
        Part.some (encode.{u_4} (α := Option σ) (Option.bind (decode a.2) fun (a_1 : β) ↦ f a.1 a_1)))
    (Part.bind
      (↑(Option.bind Option.none fun (a : α) ↦ Option.map (Prod.mk a) (decode (Nat.unpair n).2)) : Part (α × β))
      fun (a : α × β) ↦ Part.some (encode (f a.1 a.2)))

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 : α → β → Option σ
hf : Computable₂.{u_1, 0, u_4} (σ := Option σ) fun (a : α) (n : ℕ) ↦ Option.bind (decode n) (f a)
n : ℕ
val : α
some :
  Eq (α := Part ℕ)
    ((↑(encode.{u_2} (α := Option β) (decode (Nat.unpair n).2)).ppred : Part ℕ).bind fun (y : ℕ) ↦
      Part.some (encode.{u_4} (α := Option σ) (Option.bind (decode (Nat.unpair n).2) fun (a : β) ↦ f val a)))
    (Part.bind (↑(Option.map (Prod.mk val) (decode (Nat.unpair n).2)) : Part (α × β)) fun (a : α × β) ↦
      Part.some (encode (f a.1 a.2)))
⊢ Eq (α := Part ℕ)
    (Part.bind (↑((Option.some val).bind fun (a : α) ↦ Option.some (a, (Nat.unpair n).2)) : Part (α × ℕ))
      fun (a : α × ℕ) ↦
      (↑(encode.{u_2} (α := Option β) (decode a.2)).ppred : Part ℕ).bind fun (y : ℕ) ↦
        Part.some (encode.{u_4} (α := Option σ) (Option.bind (decode a.2) fun (a_1 : β) ↦ f a.1 a_1)))
    (Part.bind (↑((Option.some val).bind fun (a : α) ↦ Option.map (Prod.mk a) (decode (Nat.unpair n).2)) : Part (α × β))
      fun (a : α × β) ↦ Part.some (encode (f a.1 a.2)))

Tactic:
simp