awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Computability.Partrec
Goal:
α : Type u_1
σ : Type u_3
inst : Primcodable α
inst_1 : Primcodable σ
s : Part σ
inst_2 : Decidable s.Dom
⊢ Partrec.{u_1, u_3} (α := α) (σ := σ) fun (x : α) ↦ s

Tactic:
(Computable.ofOption (const (toOption s))).of_eq fun _ => of_toOption s

Premises used: Computable.ofOption, Partrec.of_eq, Computable.const, Part.of_toOption, Part.toOption
-- Module: Mathlib.Computability.Partrec
Goal:
α : Type u_1
σ : Type u_3
inst : Primcodable α
inst_1 : Primcodable σ
s : Part σ
⊢ Partrec.{u_1, u_3} (α := α) (σ := σ) fun (x : α) ↦ s

Tactic:
haveI := Classical.dec s.Dom
  Decidable.Partrec.const' s

Premises used: Decidable.Partrec.const'
-- 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 : Partrec f
hg : Partrec₂ g
n : ℕ
none :
  ∀ (e : Eq.{u_1 + 1} (α := Option α) (decode n) Option.none),
    Eq (α := Part ℕ)
      (do
        let n ← Nat.pair <$> Part.some n <*> Part.bind (↑Option.none : Part α) fun (a : α) ↦ map encode (f a)
        Part.bind (↑(decode n) : Part (α × β)) fun (a : α × β) ↦
            map.{u_3, 0} (α := σ) encode ((fun (p : α × β) ↦ g p.1 p.2) a))
      (Part.bind (↑Option.none : Part α) fun (a : α) ↦
        map.{u_3, 0} (α := σ) encode ((fun (a : α) ↦ (f a).bind (g a)) a))
some :
  ∀ (val : α) (e : decode n = Option.some val),
    Eq (α := Part ℕ)
      (do
        let n ← Nat.pair <$> Part.some n <*> (↑(Option.some val) : Part α).bind fun (a : α) ↦ map encode (f a)
        Part.bind (↑(decode n) : Part (α × β)) fun (a : α × β) ↦
            map.{u_3, 0} (α := σ) encode ((fun (p : α × β) ↦ g p.1 p.2) a))
      ((↑(Option.some val) : Part α).bind fun (a : α) ↦
        map.{u_3, 0} (α := σ) encode ((fun (a : α) ↦ (f a).bind (g a)) a))
⊢ Eq (α := Part ℕ)
    (do
      let n ← Nat.pair <$> Part.some n <*> Part.bind (↑(decode n) : Part α) fun (a : α) ↦ map encode (f a)
      Part.bind (↑(decode n) : Part (α × β)) fun (a : α × β) ↦
          map.{u_3, 0} (α := σ) encode ((fun (p : α × β) ↦ g p.1 p.2) a))
    (Part.bind (↑(decode n) : Part α) fun (a : α) ↦ map.{u_3, 0} (α := σ) encode ((fun (a : α) ↦ (f a).bind (g a)) a))

Tactic:
rcases e : 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 : Partrec f
hg : Partrec₂ g
n : ℕ
e : Eq.{u_1 + 1} (α := Option α) (decode n) Option.none
⊢ Eq (α := Part ℕ)
    (do
      let n ← Nat.pair <$> Part.some n <*> Part.bind (↑Option.none : Part α) fun (a : α) ↦ map encode (f a)
      Part.bind (↑(decode n) : Part (α × β)) fun (a : α × β) ↦
          map.{u_3, 0} (α := σ) encode ((fun (p : α × β) ↦ g p.1 p.2) a))
    (Part.bind (↑Option.none : Part α) fun (a : α) ↦ map.{u_3, 0} (α := σ) encode ((fun (a : α) ↦ (f a).bind (g a)) a))

Tactic:
simp [Seq.seq, e, encodek]

Premises used: Seq.seq, Encodable.encodek
-- 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 : Partrec f
hg : Partrec₂ g
n : ℕ
val : α
e : decode n = Option.some val
⊢ Eq (α := Part ℕ)
    (do
      let n ← Nat.pair <$> Part.some n <*> (↑(Option.some val) : Part α).bind fun (a : α) ↦ map encode (f a)
      Part.bind (↑(decode n) : Part (α × β)) fun (a : α × β) ↦
          map.{u_3, 0} (α := σ) encode ((fun (p : α × β) ↦ g p.1 p.2) a))
    ((↑(Option.some val) : Part α).bind fun (a : α) ↦ map.{u_3, 0} (α := σ) encode ((fun (a : α) ↦ (f a).bind (g a)) a))

Tactic:
simp [Seq.seq, e, encodek]

Premises used: Seq.seq, Encodable.encodek
-- 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 : Partrec f
hg : Computable₂ g
⊢ Partrec.{u_1, u_3} (α := α) (σ := σ) fun (a : α) ↦ Part.map (g a) (f a)

Tactic:
simpa [bind_some_eq_map] using Partrec.bind (g := fun a x => some (g a x)) hf hg

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

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

Premises used: Prod.mk, Prod.fst, Partrec.of_eq, _private.0.Computable.to₂.match_1, Eq, Prod.snd, Partrec₂, rfl
-- Module: Mathlib.Computability.Partrec
Goal:
α : Type u_1
σ : Type u_3
inst : Primcodable α
inst_1 : Primcodable σ
f : α → ℕ
g : α →. σ
h : α → ℕ × σ →. σ
hf : Computable f
hg : Partrec g
hh : Partrec₂ h
n : ℕ
none :
  ∀ (e : Eq.{u_1 + 1} (α := Option α) (decode n) Option.none),
    Eq (α := Part ℕ)
      (Part.bind (Part.bind (↑Option.none : Part α) fun (a : α) ↦ Part.map encode ((↑f : α →. ℕ) a)) fun (n_1 : ℕ) ↦
        Nat.rec (motive := fun (x : ℕ) ↦ Part ℕ) (Part.bind (↑Option.none : Part α) fun (a : α) ↦ Part.map encode (g a))
          (fun (y : ℕ) (IH : Part ℕ) ↦ do
            let i ← IH
            Part.bind (↑(decode (Nat.pair n (Nat.pair y i))) : Part (α × ℕ × σ)) fun (a : Prod.{u_1, u_3} α (ℕ × σ)) ↦
                Part.map.{u_3, 0} (α := σ) encode ((fun (p : Prod.{u_1, u_3} α (ℕ × σ)) ↦ h p.1 p.2) a))
          n_1)
      (Part.bind (↑Option.none : Part α) fun (a : α) ↦
        Part.map.{u_3, 0} (α := σ) encode
          ((fun (a : α) ↦
              (Nat.rec (motive := fun (x : ℕ) ↦ Part σ) (g a)
                  (fun (y : ℕ) (IH : Part σ) ↦ IH.bind fun (i : σ) ↦ h a (y, i)) (f a) :
                Part σ))
            a))
some :
  ∀ (a : α) (e : decode n = Option.some a),
    Eq (α := Part ℕ)
      (Part.bind ((↑(Option.some a) : Part α).bind fun (a : α) ↦ Part.map encode ((↑f : α →. ℕ) a)) fun (n_1 : ℕ) ↦
        Nat.rec (motive := fun (x : ℕ) ↦ Part ℕ) ((↑(Option.some a) : Part α).bind fun (a : α) ↦ Part.map encode (g a))
          (fun (y : ℕ) (IH : Part ℕ) ↦ do
            let i ← IH
            Part.bind (↑(decode (Nat.pair n (Nat.pair y i))) : Part (α × ℕ × σ)) fun (a : Prod.{u_1, u_3} α (ℕ × σ)) ↦
                Part.map.{u_3, 0} (α := σ) encode ((fun (p : Prod.{u_1, u_3} α (ℕ × σ)) ↦ h p.1 p.2) a))
          n_1)
      ((↑(Option.some a) : Part α).bind fun (a : α) ↦
        Part.map.{u_3, 0} (α := σ) encode
          ((fun (a : α) ↦
              (Nat.rec (motive := fun (x : ℕ) ↦ Part σ) (g a)
                  (fun (y : ℕ) (IH : Part σ) ↦ IH.bind fun (i : σ) ↦ h a (y, i)) (f a) :
                Part σ))
            a))
⊢ Eq (α := Part ℕ)
    (Part.bind (Part.bind (↑(decode n) : Part α) fun (a : α) ↦ Part.map encode ((↑f : α →. ℕ) a)) fun (n_1 : ℕ) ↦
      Nat.rec (motive := fun (x : ℕ) ↦ Part ℕ) (Part.bind (↑(decode n) : Part α) fun (a : α) ↦ Part.map encode (g a))
        (fun (y : ℕ) (IH : Part ℕ) ↦ do
          let i ← IH
          Part.bind (↑(decode (Nat.pair n (Nat.pair y i))) : Part (α × ℕ × σ)) fun (a : Prod.{u_1, u_3} α (ℕ × σ)) ↦
              Part.map.{u_3, 0} (α := σ) encode ((fun (p : Prod.{u_1, u_3} α (ℕ × σ)) ↦ h p.1 p.2) a))
        n_1)
    (Part.bind (↑(decode n) : Part α) fun (a : α) ↦
      Part.map.{u_3, 0} (α := σ) encode
        ((fun (a : α) ↦
            (Nat.rec (motive := fun (x : ℕ) ↦ Part σ) (g a)
                (fun (y : ℕ) (IH : Part σ) ↦ IH.bind fun (i : σ) ↦ h a (y, i)) (f a) :
              Part σ))
          a))

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

Premises used: Encodable.decode
-- Module: Mathlib.Computability.Partrec
Goal:
α : Type u_1
σ : Type u_3
inst : Primcodable α
inst_1 : Primcodable σ
f : α → ℕ
g : α →. σ
h : α → ℕ × σ →. σ
hf : Computable f
hg : Partrec g
hh : Partrec₂ h
n : ℕ
e : Eq.{u_1 + 1} (α := Option α) (decode n) Option.none
⊢ Eq (α := Part ℕ)
    (Part.bind (Part.bind (↑Option.none : Part α) fun (a : α) ↦ Part.map encode ((↑f : α →. ℕ) a)) fun (n_1 : ℕ) ↦
      Nat.rec (motive := fun (x : ℕ) ↦ Part ℕ) (Part.bind (↑Option.none : Part α) fun (a : α) ↦ Part.map encode (g a))
        (fun (y : ℕ) (IH : Part ℕ) ↦ do
          let i ← IH
          Part.bind (↑(decode (Nat.pair n (Nat.pair y i))) : Part (α × ℕ × σ)) fun (a : Prod.{u_1, u_3} α (ℕ × σ)) ↦
              Part.map.{u_3, 0} (α := σ) encode ((fun (p : Prod.{u_1, u_3} α (ℕ × σ)) ↦ h p.1 p.2) a))
        n_1)
    (Part.bind (↑Option.none : Part α) fun (a : α) ↦
      Part.map.{u_3, 0} (α := σ) encode
        ((fun (a : α) ↦
            (Nat.rec (motive := fun (x : ℕ) ↦ Part σ) (g a)
                (fun (y : ℕ) (IH : Part σ) ↦ IH.bind fun (i : σ) ↦ h a (y, i)) (f a) :
              Part σ))
          a))

Tactic:
simp
-- Module: Mathlib.Computability.Partrec
Goal:
α : Type u_1
σ : Type u_3
inst : Primcodable α
inst_1 : Primcodable σ
f : α → ℕ
g : α →. σ
h : α → ℕ × σ →. σ
hf : Computable f
hg : Partrec g
hh : Partrec₂ h
n : ℕ
a : α
e : decode n = Option.some a
some :
  ((Part.map encode (Part.some (f a))).bind fun (n_1 : ℕ) ↦
      Nat.rec (motive := fun (x : ℕ) ↦ Part ℕ) (Part.map encode (g a))
        (fun (y : ℕ) (IH : Part ℕ) ↦ do
          let i ← IH
          Part.bind (↑(decode (Nat.pair n (Nat.pair y i))) : Part (α × ℕ × σ)) fun (a : Prod.{u_1, u_3} α (ℕ × σ)) ↦
              Part.map encode (h a.1 a.2))
        n_1) =
    Part.map.{u_3, 0} (α := σ) encode
      (Nat.rec (motive := fun (x : ℕ) ↦ Part σ) (g a) (fun (y : ℕ) (IH : Part σ) ↦ IH.bind fun (i : σ) ↦ h a (y, i))
        (f a))
⊢ Eq (α := Part ℕ)
    (Part.bind ((↑(Option.some a) : Part α).bind fun (a : α) ↦ Part.map encode ((↑f : α →. ℕ) a)) fun (n_1 : ℕ) ↦
      Nat.rec (motive := fun (x : ℕ) ↦ Part ℕ) ((↑(Option.some a) : Part α).bind fun (a : α) ↦ Part.map encode (g a))
        (fun (y : ℕ) (IH : Part ℕ) ↦ do
          let i ← IH
          Part.bind (↑(decode (Nat.pair n (Nat.pair y i))) : Part (α × ℕ × σ)) fun (a : Prod.{u_1, u_3} α (ℕ × σ)) ↦
              Part.map.{u_3, 0} (α := σ) encode ((fun (p : Prod.{u_1, u_3} α (ℕ × σ)) ↦ h p.1 p.2) a))
        n_1)
    ((↑(Option.some a) : Part α).bind fun (a : α) ↦
      Part.map.{u_3, 0} (α := σ) encode
        ((fun (a : α) ↦
            (Nat.rec (motive := fun (x : ℕ) ↦ Part σ) (g a)
                (fun (y : ℕ) (IH : Part σ) ↦ IH.bind fun (i : σ) ↦ h a (y, i)) (f a) :
              Part σ))
          a))

Tactic:
simp only [coe_some, PFun.coe_val, bind_some]

Premises used: Part.bind_some, Part.coe_some, PFun.coe_val
-- Module: Mathlib.Computability.Partrec
Goal:
α : Type u_1
σ : Type u_3
inst : Primcodable α
inst_1 : Primcodable σ
f : α → ℕ
g : α →. σ
h : α → ℕ × σ →. σ
hf : Computable f
hg : Partrec g
hh : Partrec₂ h
n : ℕ
a : α
e : decode n = Option.some a
some :
  ((Part.map (α := ℕ) encode (Part.some 0)).bind fun (n_1 : ℕ) ↦
      Nat.rec (motive := fun (x : ℕ) ↦ Part ℕ) (Part.map encode (g a))
        (fun (y : ℕ) (IH : Part ℕ) ↦ do
          let i ← IH
          Part.bind (↑(decode (Nat.pair n (Nat.pair y i))) : Part (α × ℕ × σ)) fun (a : Prod.{u_1, u_3} α (ℕ × σ)) ↦
              Part.map encode (h a.1 a.2))
        n_1) =
    Part.map.{u_3, 0} (α := σ) encode
      (Nat.rec (motive := fun (x : ℕ) ↦ Part σ) (g a) (fun (y : ℕ) (IH : Part σ) ↦ IH.bind fun (i : σ) ↦ h a (y, i)) 0)
some₁ :
  ∀ (n_1 : ℕ),
    ((Part.map encode (Part.some n_1)).bind fun (n_2 : ℕ) ↦
          Nat.rec (motive := fun (x : ℕ) ↦ Part ℕ) (Part.map encode (g a))
            (fun (y : ℕ) (IH : Part ℕ) ↦ do
              let i ← IH
              Part.bind (↑(decode (Nat.pair n (Nat.pair y i))) : Part (α × ℕ × σ)) fun (a : Prod.{u_1, u_3} α (ℕ × σ)) ↦
                  Part.map encode (h a.1 a.2))
            n_2) =
        Part.map.{u_3, 0} (α := σ) encode
          (Nat.rec (motive := fun (x : ℕ) ↦ Part σ) (g a) (fun (y : ℕ) (IH : Part σ) ↦ IH.bind fun (i : σ) ↦ h a (y, i))
            n_1) →
      ((Part.map encode (Part.some (n_1 + 1))).bind fun (n_2 : ℕ) ↦
          Nat.rec (motive := fun (x : ℕ) ↦ Part ℕ) (Part.map encode (g a))
            (fun (y : ℕ) (IH : Part ℕ) ↦ do
              let i ← IH
              Part.bind (↑(decode (Nat.pair n (Nat.pair y i))) : Part (α × ℕ × σ)) fun (a : Prod.{u_1, u_3} α (ℕ × σ)) ↦
                  Part.map encode (h a.1 a.2))
            n_2) =
        Part.map.{u_3, 0} (α := σ) encode
          (Nat.rec (motive := fun (x : ℕ) ↦ Part σ) (g a) (fun (y : ℕ) (IH : Part σ) ↦ IH.bind fun (i : σ) ↦ h a (y, i))
            (n_1 + 1))
⊢ ((Part.map encode (Part.some (f a))).bind fun (n_1 : ℕ) ↦
      Nat.rec (motive := fun (x : ℕ) ↦ Part ℕ) (Part.map encode (g a))
        (fun (y : ℕ) (IH : Part ℕ) ↦ do
          let i ← IH
          Part.bind (↑(decode (Nat.pair n (Nat.pair y i))) : Part (α × ℕ × σ)) fun (a : Prod.{u_1, u_3} α (ℕ × σ)) ↦
              Part.map encode (h a.1 a.2))
        n_1) =
    Part.map.{u_3, 0} (α := σ) encode
      (Nat.rec (motive := fun (x : ℕ) ↦ Part σ) (g a) (fun (y : ℕ) (IH : Part σ) ↦ IH.bind fun (i : σ) ↦ h a (y, i))
        (f a))

Tactic:
induction f a
-- Module: Mathlib.Computability.Partrec
Goal:
α : Type u_1
σ : Type u_3
inst : Primcodable α
inst_1 : Primcodable σ
f : α → ℕ
g : α →. σ
h : α → ℕ × σ →. σ
hf : Computable f
hg : Partrec g
hh : Partrec₂ h
n : ℕ
a : α
e : decode n = Option.some a
⊢ ((Part.map (α := ℕ) encode (Part.some 0)).bind fun (n_1 : ℕ) ↦
      Nat.rec (motive := fun (x : ℕ) ↦ Part ℕ) (Part.map encode (g a))
        (fun (y : ℕ) (IH : Part ℕ) ↦ do
          let i ← IH
          Part.bind (↑(decode (Nat.pair n (Nat.pair y i))) : Part (α × ℕ × σ)) fun (a : Prod.{u_1, u_3} α (ℕ × σ)) ↦
              Part.map encode (h a.1 a.2))
        n_1) =
    Part.map.{u_3, 0} (α := σ) encode
      (Nat.rec (motive := fun (x : ℕ) ↦ Part σ) (g a) (fun (y : ℕ) (IH : Part σ) ↦ IH.bind fun (i : σ) ↦ h a (y, i)) 0)

Tactic:
simp_all
-- Module: Mathlib.Computability.Partrec
Goal:
α : Type u_1
σ : Type u_3
inst : Primcodable α
inst_1 : Primcodable σ
f : α → ℕ
g : α →. σ
h : α → ℕ × σ →. σ
hf : Computable f
hg : Partrec g
hh : Partrec₂ h
n : ℕ
a : α
e : decode n = Option.some a
n_1 : ℕ
h_1 :
  ((Part.map encode (Part.some n_1)).bind fun (n_2 : ℕ) ↦
      Nat.rec (motive := fun (x : ℕ) ↦ Part ℕ) (Part.map encode (g a))
        (fun (y : ℕ) (IH : Part ℕ) ↦ do
          let i ← IH
          Part.bind (↑(decode (Nat.pair n (Nat.pair y i))) : Part (α × ℕ × σ)) fun (a : Prod.{u_1, u_3} α (ℕ × σ)) ↦
              Part.map encode (h a.1 a.2))
        n_2) =
    Part.map.{u_3, 0} (α := σ) encode
      (Nat.rec (motive := fun (x : ℕ) ↦ Part σ) (g a) (fun (y : ℕ) (IH : Part σ) ↦ IH.bind fun (i : σ) ↦ h a (y, i))
        n_1)
⊢ ((Part.map encode (Part.some (n_1 + 1))).bind fun (n_2 : ℕ) ↦
      Nat.rec (motive := fun (x : ℕ) ↦ Part ℕ) (Part.map encode (g a))
        (fun (y : ℕ) (IH : Part ℕ) ↦ do
          let i ← IH
          Part.bind (↑(decode (Nat.pair n (Nat.pair y i))) : Part (α × ℕ × σ)) fun (a : Prod.{u_1, u_3} α (ℕ × σ)) ↦
              Part.map encode (h a.1 a.2))
        n_2) =
    Part.map.{u_3, 0} (α := σ) encode
      (Nat.rec (motive := fun (x : ℕ) ↦ Part σ) (g a) (fun (y : ℕ) (IH : Part σ) ↦ IH.bind fun (i : σ) ↦ h a (y, i))
        (n_1 + 1))

Tactic:
simp_all
-- 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 : Partrec f
hg : Computable g
n : ℕ
simp :
  Eq (α := Part ℕ)
    (Part.bind (Part.bind (↑(decode n) : Part α) fun (a : α) ↦ Part.some (encode (g a))) fun (n : ℕ) ↦
      Part.bind (↑(decode n) : Part β) fun (a : β) ↦ Part.map encode (f a))
    (Part.bind (↑(decode n) : Part α) fun (a : α) ↦ Part.map encode (f (g a)))
⊢ Eq (α := Part ℕ)
    (do
      let n ← Part.bind (↑(decode n) : Part α) fun (a : α) ↦ Part.map encode ((↑g : α →. β) a)
      Part.bind (↑(decode n) : Part β) fun (a : β) ↦ Part.map encode (f a))
    (Part.bind (↑(decode n) : Part α) fun (a : α) ↦ Part.map.{u_3, 0} (α := σ) encode ((fun (a : α) ↦ f (g a)) a))

Tactic:
simp only [PFun.coe_val, map_some, bind_eq_bind]

Premises used: PFun.coe_val, Part.map_some, Part.bind_eq_bind
-- 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 : Partrec f
hg : Computable g
n : ℕ
none :
  ∀ (e : Eq.{u_1 + 1} (α := Option α) (decode n) Option.none),
    Eq (α := Part ℕ)
      (Part.bind (Part.bind (↑Option.none : Part α) fun (a : α) ↦ Part.some (encode (g a))) fun (n : ℕ) ↦
        Part.bind (↑(decode n) : Part β) fun (a : β) ↦ Part.map encode (f a))
      (Part.bind (↑Option.none : Part α) fun (a : α) ↦ Part.map encode (f (g a)))
some :
  ∀ (a : α) (e : decode n = Option.some a),
    Eq (α := Part ℕ)
      (Part.bind ((↑(Option.some a) : Part α).bind fun (a : α) ↦ Part.some (encode (g a))) fun (n : ℕ) ↦
        Part.bind (↑(decode n) : Part β) fun (a : β) ↦ Part.map encode (f a))
      ((↑(Option.some a) : Part α).bind fun (a : α) ↦ Part.map encode (f (g a)))
⊢ Eq (α := Part ℕ)
    (Part.bind (Part.bind (↑(decode n) : Part α) fun (a : α) ↦ Part.some (encode (g a))) fun (n : ℕ) ↦
      Part.bind (↑(decode n) : Part β) fun (a : β) ↦ Part.map encode (f a))
    (Part.bind (↑(decode n) : Part α) fun (a : α) ↦ Part.map encode (f (g a)))

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

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 : Partrec f
hg : Computable g
n : ℕ
e : Eq.{u_1 + 1} (α := Option α) (decode n) Option.none
⊢ Eq (α := Part ℕ)
    (Part.bind (Part.bind (↑Option.none : Part α) fun (a : α) ↦ Part.some (encode (g a))) fun (n : ℕ) ↦
      Part.bind (↑(decode n) : Part β) fun (a : β) ↦ Part.map encode (f a))
    (Part.bind (↑Option.none : Part α) fun (a : α) ↦ Part.map encode (f (g a)))

Tactic:
simp [encodek]

Premises used: Encodable.encodek
-- 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 : Partrec f
hg : Computable g
n : ℕ
a : α
e : decode n = Option.some a
⊢ Eq (α := Part ℕ)
    (Part.bind ((↑(Option.some a) : Part α).bind fun (a : α) ↦ Part.some (encode (g a))) fun (n : ℕ) ↦
      Part.bind (↑(decode n) : Part β) fun (a : β) ↦ Part.map encode (f a))
    ((↑(Option.some a) : Part α).bind fun (a : α) ↦ Part.map encode (f (g a)))

Tactic:
simp [encodek]

Premises used: Encodable.encodek
-- Module: Mathlib.Computability.Partrec
Goal:
f : ℕ →. ℕ
⊢ Partrec f ↔ Nat.Partrec f

Tactic:
simp [Partrec, map_id']

Premises used: Part.map_id', Partrec
-- Module: Mathlib.Computability.Partrec
Goal:
α : Type u_1
σ : Type u_3
inst : Primcodable α
inst_1 : Primcodable σ
f : α →. σ
⊢ (Partrec.{u_1, 0} (α := α) (σ := ℕ) fun (a : α) ↦ Part.map encode (f a)) ↔ Partrec f

Tactic:
Iff.rfl

Premises used: Iff.rfl, Partrec, Part.map
-- Module: Mathlib.Computability.Partrec
Goal:
α : Type u_1
inst : Primcodable α
f : ℕ → ℕ →. α
h : Partrec (Nat.unpaired f)
⊢ Partrec₂ f

Tactic:
simpa using Partrec.comp (g := fun p : ℕ × ℕ => (p.1, p.2)) h Primrec₂.pair.to_comp

Premises used: Primrec₂.pair, Partrec.comp, Primrec₂.to_comp
-- Module: Mathlib.Computability.Partrec
Goal:
f : ℕ → ℕ →. ℕ
⊢ Nat.Partrec (Nat.unpaired f) ↔ Partrec₂ f

Tactic:
Partrec.nat_iff.symm.trans unpaired

Premises used: Partrec.nat_iff, Iff.trans, Partrec₂.unpaired, Iff.symm
-- Module: Mathlib.Computability.Partrec
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_5
inst : Primcodable α
inst_1 : Primcodable β
inst_2 : Primcodable γ
inst_3 : Primcodable σ
f : β → γ →. σ
g : α → β
h : α → γ
hf : Partrec₂ f
hg : Computable g
hh : Computable h
⊢ Partrec.{u_1, u_5} (α := α) (σ := σ) fun (a : α) ↦ f (g a) (h a)

Tactic:
hf.comp (hg.pair hh)

Premises used: Computable.pair, Partrec.comp
-- Module: Mathlib.Computability.Partrec
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
σ : Type u_5
inst : Primcodable α
inst_1 : Primcodable β
inst_2 : Primcodable γ
inst_3 : Primcodable δ
inst_4 : Primcodable σ
f : γ → δ →. σ
g : α → β → γ
h : α → β → δ
hf : Partrec₂ f
hg : Computable₂ g
hh : Computable₂ h
⊢ Partrec₂.{u_1, u_2, u_5} (β := β) (σ := σ) fun (a : α) (b : β) ↦ f (g a b) (h a b)

Tactic:
hf.comp hg hh

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

Tactic:
hf.comp hg

Premises used: PFun.lift, Computable, Partrec.comp
-- Module: Mathlib.Computability.Partrec
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst : Primcodable α
inst_1 : Primcodable β
inst_2 : Primcodable γ
inst_3 : Primcodable σ
f : γ → σ
g : α → β → γ
hf : Computable f
hg : Computable₂ g
⊢ Computable₂.{u_1, u_2, u_4} (σ := σ) fun (a : α) (b : β) ↦ f (g a b)

Tactic:
hf.comp hg

Premises used: Computable.comp, Computable₂
-- Module: Mathlib.Computability.Partrec
Goal:
α : Type u_1
β : Type u_2
σ : Type u_5
inst : Primcodable α
inst_1 : Primcodable β
inst_2 : Primcodable σ
f : α → β → σ
hf : Computable (σ := σ) fun (p : α × β) ↦ f p.1 p.2
⊢ Computable₂ f

Tactic:
hf

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

Tactic:
hf.comp (hg.pair hh)

Premises used: Computable.comp, Computable.pair
-- Module: Mathlib.Computability.Partrec
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
σ : Type u_5
inst : Primcodable α
inst_1 : Primcodable β
inst_2 : Primcodable γ
inst_3 : Primcodable δ
inst_4 : Primcodable σ
f : γ → δ → σ
g : α → β → γ
h : α → β → δ
hf : Computable₂ f
hg : Computable₂ g
hh : Computable₂ h
⊢ Computable₂.{u_1, u_2, u_5} (σ := σ) fun (a : α) (b : β) ↦ f (g a b) (h a b)

Tactic:
hf.comp hg hh

Premises used: Computable₂.comp, Computable₂
-- Module: Mathlib.Computability.Partrec
Goal:
α : Type u_1
inst : Primcodable α
p : α → ℕ →. Bool
hp : Partrec₂ p
n : ℕ
none :
  ∀ (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)
some :
  ∀ (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)
⊢ (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 (↑(decode n) : Part α) fun (a : α) ↦ Part.map (α := ℕ) encode ((fun (a : α) ↦ Nat.rfind (p a)) a)

Tactic:
rcases e : decode (α := α) n

Premises used: Encodable.decode