awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Computability.RE
Goal:
α : Type u_1
σ : Type u_4
inst : Primcodable α
inst_1 : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
k : ℕ →. ℕ
hk : Nat.Partrec k
H :
  ∀ (a : ℕ),
    (∀ x ∈ k a,
        Membership.mem (γ := Part ℕ) ((↑(decode₂ α a) : Part α).bind fun (a : α) ↦ Part.map encode (f a)) x ∨
          Membership.mem (γ := Part ℕ) ((↑(decode₂ α a) : Part α).bind fun (a : α) ↦ Part.map encode (g a)) x) ∧
      ((k a).Dom ↔
        Dom (α := ℕ) ((↑(decode₂ α a) : Part α).bind fun (a : α) ↦ Part.map encode (f a)) ∨
          Dom (α := ℕ) ((↑(decode₂ α a) : Part α).bind fun (a : α) ↦ Part.map encode (g a)))
k' : (a : α) → Part σ := fun (a : α) ↦ (k (encode a)).bind fun (n : ℕ) ↦ (↑(decode n) : Part σ)
a : α
this : ∀ x ∈ k' a, x ∈ f a ∨ x ∈ g a
h : (f a).Dom ∨ (g a).Dom
⊢ Dom (α := ℕ) ((↑(decode₂ α (encode a)) : Part α).bind fun (a : α) ↦ Part.map encode (f a)) ∨
    Dom (α := ℕ) ((↑(decode₂ α (encode a)) : Part α).bind fun (a : α) ↦ Part.map encode (g a))

Tactic:
simpa only [encodek₂, bind_some, coe_some] using h

Premises used: Part.bind_some, Part.coe_some, Encodable.encodek₂
-- Module: Mathlib.Computability.RE
Goal:
α : Type u_1
σ : Type u_4
inst : Primcodable α
inst_1 : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
k : ℕ →. ℕ
hk : Nat.Partrec k
H :
  ∀ (a : ℕ),
    (∀ x ∈ k a,
        Membership.mem (γ := Part ℕ) ((↑(decode₂ α a) : Part α).bind fun (a : α) ↦ Part.map encode (f a)) x ∨
          Membership.mem (γ := Part ℕ) ((↑(decode₂ α a) : Part α).bind fun (a : α) ↦ Part.map encode (g a)) x) ∧
      ((k a).Dom ↔
        Dom (α := ℕ) ((↑(decode₂ α a) : Part α).bind fun (a : α) ↦ Part.map encode (f a)) ∨
          Dom (α := ℕ) ((↑(decode₂ α a) : Part α).bind fun (a : α) ↦ Part.map encode (g a)))
k' : (a : α) → Part σ := fun (a : α) ↦ (k (encode a)).bind fun (n : ℕ) ↦ (↑(decode n) : Part σ)
a : α
this : ∀ x ∈ k' a, x ∈ f a ∨ x ∈ g a
h : (f a).Dom ∨ (g a).Dom
⊢ (k (encode a)).Dom

Tactic:
have hk : (k (encode a)).Dom :=
    (H _).2.2 (by simpa only [encodek₂, bind_some, coe_some] using h)
-- Module: Mathlib.Computability.RE
Goal:
α : Type u_1
σ : Type u_4
inst : Primcodable α
inst_1 : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
k : ℕ →. ℕ
hk_1 : Nat.Partrec k
H :
  ∀ (a : ℕ),
    (∀ x ∈ k a,
        Membership.mem (γ := Part ℕ) ((↑(decode₂ α a) : Part α).bind fun (a : α) ↦ Part.map encode (f a)) x ∨
          Membership.mem (γ := Part ℕ) ((↑(decode₂ α a) : Part α).bind fun (a : α) ↦ Part.map encode (g a)) x) ∧
      ((k a).Dom ↔
        Dom (α := ℕ) ((↑(decode₂ α a) : Part α).bind fun (a : α) ↦ Part.map encode (f a)) ∨
          Dom (α := ℕ) ((↑(decode₂ α a) : Part α).bind fun (a : α) ↦ Part.map encode (g a)))
k' : (a : α) → Part σ := fun (a : α) ↦ (k (encode a)).bind fun (n : ℕ) ↦ (↑(decode n) : Part σ)
a : α
this : ∀ x ∈ k' a, x ∈ f a ∨ x ∈ g a
h : (f a).Dom ∨ (g a).Dom
hk : (k (encode a)).Dom
exists : Dom.{u_4} (α := σ) (↑(decode ((k (encode a)).get hk)) : Part σ)
⊢ ∃ (h : (k (encode a)).Dom), Dom.{u_4} (α := σ) (↑(decode ((k (encode a)).get h)) : Part σ)

Tactic:
exists hk
-- Module: Mathlib.Computability.RE
Goal:
α : Type u_1
σ : Type u_4
inst : Primcodable α
inst_1 : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
k : ℕ →. ℕ
hk_1 : Nat.Partrec k
H :
  ∀ (a : ℕ),
    (∀ x ∈ k a,
        Membership.mem (γ := Part ℕ) ((↑(decode₂ α a) : Part α).bind fun (a : α) ↦ Part.map encode (f a)) x ∨
          Membership.mem (γ := Part ℕ) ((↑(decode₂ α a) : Part α).bind fun (a : α) ↦ Part.map encode (g a)) x) ∧
      ((k a).Dom ↔
        Dom (α := ℕ) ((↑(decode₂ α a) : Part α).bind fun (a : α) ↦ Part.map encode (f a)) ∨
          Dom (α := ℕ) ((↑(decode₂ α a) : Part α).bind fun (a : α) ↦ Part.map encode (g a)))
k' : (a : α) → Part σ := fun (a : α) ↦ (k (encode a)).bind fun (n : ℕ) ↦ (↑(decode n) : Part σ)
a : α
this : ∀ x ∈ k' a, x ∈ f a ∨ x ∈ g a
h : (f a).Dom ∨ (g a).Dom
hk : (k (encode a)).Dom
⊢ ∀ (a : ℕ),
    (∀ x ∈ k a,
        (∃ (a_2 : α), decode₂ α a = Option.some a_2 ∧ ∃ a ∈ f a_2, encode a = x) ∨
          ∃ (a_2 : α), decode₂ α a = Option.some a_2 ∧ ∃ a ∈ g a_2, encode a = x) ∧
      ((k a).Dom ↔
        Dom (α := ℕ) ((↑(decode₂ α a) : Part α).bind fun (a : α) ↦ Part.map encode (f a)) ∨
          Dom (α := ℕ) ((↑(decode₂ α a) : Part α).bind fun (a : α) ↦ Part.map encode (g a)))

Tactic:
simp only [mem_map_iff, mem_coe, mem_bind_iff, Option.mem_def] at H

Premises used: Part.mem_bind_iff, Part.mem_coe, Part.mem_map_iff, Option.mem_def
-- Module: Mathlib.Computability.RE
Goal:
α : Type u_1
σ : Type u_4
inst : Primcodable α
inst_1 : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
k : ℕ →. ℕ
hk_1 : Nat.Partrec k
k' : (a : α) → Part σ := fun (a : α) ↦ (k (encode a)).bind fun (n : ℕ) ↦ (↑(decode n) : Part σ)
a : α
this : ∀ x ∈ k' a, x ∈ f a ∨ x ∈ g a
h : (f a).Dom ∨ (g a).Dom
hk : (k (encode a)).Dom
H :
  ∀ (a : ℕ),
    (∀ x ∈ k a,
        (∃ (a_2 : α), decode₂ α a = Option.some a_2 ∧ ∃ a ∈ f a_2, encode a = x) ∨
          ∃ (a_2 : α), decode₂ α a = Option.some a_2 ∧ ∃ a ∈ g a_2, encode a = x) ∧
      ((k a).Dom ↔
        Dom (α := ℕ) ((↑(decode₂ α a) : Part α).bind fun (a : α) ↦ Part.map encode (f a)) ∨
          Dom (α := ℕ) ((↑(decode₂ α a) : Part α).bind fun (a : α) ↦ Part.map encode (g a)))
inl :
  ∀ (a' : α),
    decode₂ α (encode a) = Option.some a' →
      ∀ y ∈ f a',
        ∀ (e : encode y = (k (encode a)).get hk), Dom.{u_4} (α := σ) (↑(decode ((k (encode a)).get hk)) : Part σ)
inr :
  ∀ (a' : α),
    decode₂ α (encode a) = Option.some a' →
      ∀ y ∈ g a',
        ∀ (e : encode y = (k (encode a)).get hk), Dom.{u_4} (α := σ) (↑(decode ((k (encode a)).get hk)) : Part σ)
⊢ Dom.{u_4} (α := σ) (↑(decode ((k (encode a)).get hk)) : Part σ)

Tactic:
obtain ⟨a', _, y, _, e⟩ | ⟨a', _, y, _, e⟩ := (H _).1 _ ⟨hk, rfl⟩

Premises used: And.left, Exists.intro, rfl
-- Module: Mathlib.Computability.RE
Goal:
α : Type u_1
σ : Type u_4
inst : Primcodable α
inst_1 : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
k : ℕ →. ℕ
hk_1 : Nat.Partrec k
k' : (a : α) → Part σ := fun (a : α) ↦ (k (encode a)).bind fun (n : ℕ) ↦ (↑(decode n) : Part σ)
a : α
this : ∀ x ∈ k' a, x ∈ f a ∨ x ∈ g a
h : (f a).Dom ∨ (g a).Dom
hk : (k (encode a)).Dom
H :
  ∀ (a : ℕ),
    (∀ x ∈ k a,
        (∃ (a_2 : α), decode₂ α a = Option.some a_2 ∧ ∃ a ∈ f a_2, encode a = x) ∨
          ∃ (a_2 : α), decode₂ α a = Option.some a_2 ∧ ∃ a ∈ g a_2, encode a = x) ∧
      ((k a).Dom ↔
        Dom (α := ℕ) ((↑(decode₂ α a) : Part α).bind fun (a : α) ↦ Part.map encode (f a)) ∨
          Dom (α := ℕ) ((↑(decode₂ α a) : Part α).bind fun (a : α) ↦ Part.map encode (g a)))
a' : α
left : decode₂ α (encode a) = Option.some a'
y : σ
left_1 : y ∈ f a'
e : encode y = (k (encode a)).get hk
⊢ Dom.{u_4} (α := σ) (↑(decode ((k (encode a)).get hk)) : Part σ)

Tactic:
simp only [e.symm, encodek, coe_some, some_dom]

Premises used: Part.coe_some, Encodable.encodek, Eq.symm, Part.some_dom
-- Module: Mathlib.Computability.RE
Goal:
α : Type u_1
σ : Type u_4
inst : Primcodable α
inst_1 : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
k : ℕ →. ℕ
hk_1 : Nat.Partrec k
k' : (a : α) → Part σ := fun (a : α) ↦ (k (encode a)).bind fun (n : ℕ) ↦ (↑(decode n) : Part σ)
a : α
this : ∀ x ∈ k' a, x ∈ f a ∨ x ∈ g a
h : (f a).Dom ∨ (g a).Dom
hk : (k (encode a)).Dom
H :
  ∀ (a : ℕ),
    (∀ x ∈ k a,
        (∃ (a_2 : α), decode₂ α a = Option.some a_2 ∧ ∃ a ∈ f a_2, encode a = x) ∨
          ∃ (a_2 : α), decode₂ α a = Option.some a_2 ∧ ∃ a ∈ g a_2, encode a = x) ∧
      ((k a).Dom ↔
        Dom (α := ℕ) ((↑(decode₂ α a) : Part α).bind fun (a : α) ↦ Part.map encode (f a)) ∨
          Dom (α := ℕ) ((↑(decode₂ α a) : Part α).bind fun (a : α) ↦ Part.map encode (g a)))
a' : α
left : decode₂ α (encode a) = Option.some a'
y : σ
left_1 : y ∈ g a'
e : encode y = (k (encode a)).get hk
⊢ Dom.{u_4} (α := σ) (↑(decode ((k (encode a)).get hk)) : Part σ)

Tactic:
simp only [e.symm, encodek, coe_some, some_dom]

Premises used: Part.coe_some, Encodable.encodek, Eq.symm, Part.some_dom
-- Module: Mathlib.Computability.RE
Goal:
α : Type u_1
σ : Type u_4
inst : Primcodable α
inst_1 : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
H : ∀ (a : α), ∀ x ∈ f a, ∀ y ∈ g a, x = y
k : α →. σ
hk : Partrec k
K : ∀ (a : α), (∀ x ∈ k a, x ∈ f a ∨ x ∈ g a) ∧ ((k a).Dom ↔ (f a).Dom ∨ (g a).Dom)
a : α
x : σ
h : x ∈ f a ∨ x ∈ g a
⊢ (k a).Dom

Tactic:
have : (k a).Dom := (K _).2.2 (h.imp Exists.fst Exists.fst)
-- Module: Mathlib.Computability.RE
Goal:
α : Type u_1
σ : Type u_4
inst : Primcodable α
inst_1 : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
H : ∀ (a : α), ∀ x ∈ f a, ∀ y ∈ g a, x = y
k : α →. σ
hk : Partrec k
K : ∀ (a : α), (∀ x ∈ k a, x ∈ f a ∨ x ∈ g a) ∧ ((k a).Dom ↔ (f a).Dom ∨ (g a).Dom)
a : α
x : σ
h : x ∈ f a ∨ x ∈ g a
this : (k a).Dom
⊢ x ∈ k a

Tactic:
⟨this, ?_⟩

Premises used: Part.Mem, Exists.intro
-- Module: Mathlib.Computability.RE
Goal:
α : Type u_1
σ : Type u_4
inst : Primcodable α
inst_1 : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
H : ∀ (a : α), ∀ x ∈ f a, ∀ y ∈ g a, x = y
k : α →. σ
hk : Partrec k
K : ∀ (a : α), (∀ x ∈ k a, x ∈ f a ∨ x ∈ g a) ∧ ((k a).Dom ↔ (f a).Dom ∨ (g a).Dom)
a : α
x : σ
h : x ∈ f a ∨ x ∈ g a
this : (k a).Dom
refine : (k a).get this = x
⊢ x ∈ k a

Tactic:
refine ⟨this, ?_⟩
-- Module: Mathlib.Computability.RE
Goal:
α : Type u_1
σ : Type u_4
inst : Primcodable α
inst_1 : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
H : ∀ (a : α), ∀ x ∈ f a, ∀ y ∈ g a, x = y
k : α →. σ
hk : Partrec k
K : ∀ (a : α), (∀ x ∈ k a, x ∈ f a ∨ x ∈ g a) ∧ ((k a).Dom ↔ (f a).Dom ∨ (g a).Dom)
a : α
x : σ
h : x ∈ f a ∨ x ∈ g a
this : (k a).Dom
inl : ∀ (h : x ∈ f a), (k a).get this = x
inr : ∀ (h : x ∈ g a), (k a).get this = x
⊢ (k a).get this = x

Tactic:
rcases h with h | h
-- Module: Mathlib.Computability.RE
Goal:
α : Type u_1
σ : Type u_4
inst : Primcodable α
inst_1 : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
H : ∀ (a : α), ∀ x ∈ f a, ∀ y ∈ g a, x = y
k : α →. σ
hk : Partrec k
K : ∀ (a : α), (∀ x ∈ k a, x ∈ f a ∨ x ∈ g a) ∧ ((k a).Dom ↔ (f a).Dom ∨ (g a).Dom)
a : α
x : σ
this : (k a).Dom
h : x ∈ f a
inl : ∀ (h' : (k a).get this ∈ f a), (k a).get this = x
inl₁ : ∀ (h' : (k a).get this ∈ g a), (k a).get this = x
⊢ (k a).get this = x

Tactic:
rcases (K _).1 _ ⟨this, rfl⟩ with h' | h'

Premises used: And.left, Exists.intro, rfl
-- Module: Mathlib.Computability.RE
Goal:
α : Type u_1
σ : Type u_4
inst : Primcodable α
inst_1 : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
H : ∀ (a : α), ∀ x ∈ f a, ∀ y ∈ g a, x = y
k : α →. σ
hk : Partrec k
K : ∀ (a : α), (∀ x ∈ k a, x ∈ f a ∨ x ∈ g a) ∧ ((k a).Dom ↔ (f a).Dom ∨ (g a).Dom)
a : α
x : σ
this : (k a).Dom
h : x ∈ g a
inr : ∀ (h' : (k a).get this ∈ f a), (k a).get this = x
inr₁ : ∀ (h' : (k a).get this ∈ g a), (k a).get this = x
⊢ (k a).get this = x

Tactic:
rcases (K _).1 _ ⟨this, rfl⟩ with h' | h'

Premises used: And.left, Exists.intro, rfl
-- Module: Mathlib.Computability.RE
Goal:
α : Type u_1
σ : Type u_4
inst : Primcodable α
inst_1 : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
H : ∀ (a : α), ∀ x ∈ f a, ∀ y ∈ g a, x = y
k : α →. σ
hk : Partrec k
K : ∀ (a : α), (∀ x ∈ k a, x ∈ f a ∨ x ∈ g a) ∧ ((k a).Dom ↔ (f a).Dom ∨ (g a).Dom)
a : α
x : σ
this : (k a).Dom
h : x ∈ f a
h' : (k a).get this ∈ f a
⊢ (k a).get this = x

Tactic:
mem_unique h' h

Premises used: Part.mem_unique
-- Module: Mathlib.Computability.RE
Goal:
α : Type u_1
σ : Type u_4
inst : Primcodable α
inst_1 : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
H : ∀ (a : α), ∀ x ∈ f a, ∀ y ∈ g a, x = y
k : α →. σ
hk : Partrec k
K : ∀ (a : α), (∀ x ∈ k a, x ∈ f a ∨ x ∈ g a) ∧ ((k a).Dom ↔ (f a).Dom ∨ (g a).Dom)
a : α
x : σ
this : (k a).Dom
h : x ∈ f a
h' : (k a).get this ∈ f a
⊢ (k a).get this = x

Tactic:
exact mem_unique h' h

Premises used: Part.mem_unique
-- Module: Mathlib.Computability.RE
Goal:
α : Type u_1
σ : Type u_4
inst : Primcodable α
inst_1 : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
H : ∀ (a : α), ∀ x ∈ f a, ∀ y ∈ g a, x = y
k : α →. σ
hk : Partrec k
K : ∀ (a : α), (∀ x ∈ k a, x ∈ f a ∨ x ∈ g a) ∧ ((k a).Dom ↔ (f a).Dom ∨ (g a).Dom)
a : α
x : σ
this : (k a).Dom
h : x ∈ f a
h' : (k a).get this ∈ g a
⊢ (k a).get this = x

Tactic:
(H _ _ h _ h').symm

Premises used: Eq.symm
-- Module: Mathlib.Computability.RE
Goal:
α : Type u_1
σ : Type u_4
inst : Primcodable α
inst_1 : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
H : ∀ (a : α), ∀ x ∈ f a, ∀ y ∈ g a, x = y
k : α →. σ
hk : Partrec k
K : ∀ (a : α), (∀ x ∈ k a, x ∈ f a ∨ x ∈ g a) ∧ ((k a).Dom ↔ (f a).Dom ∨ (g a).Dom)
a : α
x : σ
this : (k a).Dom
h : x ∈ f a
h' : (k a).get this ∈ g a
⊢ (k a).get this = x

Tactic:
exact (H _ _ h _ h').symm

Premises used: Eq.symm
-- Module: Mathlib.Computability.RE
Goal:
α : Type u_1
σ : Type u_4
inst : Primcodable α
inst_1 : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
H : ∀ (a : α), ∀ x ∈ f a, ∀ y ∈ g a, x = y
k : α →. σ
hk : Partrec k
K : ∀ (a : α), (∀ x ∈ k a, x ∈ f a ∨ x ∈ g a) ∧ ((k a).Dom ↔ (f a).Dom ∨ (g a).Dom)
a : α
x : σ
this : (k a).Dom
h : x ∈ g a
h' : (k a).get this ∈ f a
⊢ (k a).get this = x

Tactic:
H _ _ h' _ h
-- Module: Mathlib.Computability.RE
Goal:
α : Type u_1
σ : Type u_4
inst : Primcodable α
inst_1 : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
H : ∀ (a : α), ∀ x ∈ f a, ∀ y ∈ g a, x = y
k : α →. σ
hk : Partrec k
K : ∀ (a : α), (∀ x ∈ k a, x ∈ f a ∨ x ∈ g a) ∧ ((k a).Dom ↔ (f a).Dom ∨ (g a).Dom)
a : α
x : σ
this : (k a).Dom
h : x ∈ g a
h' : (k a).get this ∈ f a
⊢ (k a).get this = x

Tactic:
exact H _ _ h' _ h
-- Module: Mathlib.Computability.RE
Goal:
α : Type u_1
σ : Type u_4
inst : Primcodable α
inst_1 : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
H : ∀ (a : α), ∀ x ∈ f a, ∀ y ∈ g a, x = y
k : α →. σ
hk : Partrec k
K : ∀ (a : α), (∀ x ∈ k a, x ∈ f a ∨ x ∈ g a) ∧ ((k a).Dom ↔ (f a).Dom ∨ (g a).Dom)
a : α
x : σ
this : (k a).Dom
h : x ∈ g a
h' : (k a).get this ∈ g a
⊢ (k a).get this = x

Tactic:
mem_unique h' h

Premises used: Part.mem_unique
-- Module: Mathlib.Computability.RE
Goal:
α : Type u_1
σ : Type u_4
inst : Primcodable α
inst_1 : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
H : ∀ (a : α), ∀ x ∈ f a, ∀ y ∈ g a, x = y
k : α →. σ
hk : Partrec k
K : ∀ (a : α), (∀ x ∈ k a, x ∈ f a ∨ x ∈ g a) ∧ ((k a).Dom ↔ (f a).Dom ∨ (g a).Dom)
a : α
x : σ
this : (k a).Dom
h : x ∈ g a
h' : (k a).get this ∈ g a
⊢ (k a).get this = x

Tactic:
exact mem_unique h' h

Premises used: Part.mem_unique
-- Module: Mathlib.Computability.RE
Goal:
α : Type u_1
σ : Type u_4
inst : Primcodable α
inst_1 : Primcodable σ
c : α → Bool
f g : α →. σ
hc : Computable c
hf : Partrec f
hg : Partrec g
cf : Code
ef : cf.eval = fun (n : ℕ) ↦ Part.bind (↑(decode n) : Part α) fun (a : α) ↦ Part.map encode (f a)
cg : Code
eg : cg.eval = fun (n : ℕ) ↦ Part.bind (↑(decode n) : Part α) fun (a : α) ↦ Part.map encode (g a)
a : α
false :
  (((bif Bool.false then cf else cg).eval (encode a)).bind fun (b : ℕ) ↦ (↑(decode (a, b).2) : Part σ)) =
    bif Bool.false then f a else g a
true :
  (((bif Bool.true then cf else cg).eval (encode a)).bind fun (b : ℕ) ↦ (↑(decode (a, b).2) : Part σ)) =
    bif Bool.true then f a else g a
⊢ (((bif c a then cf else cg).eval (encode a)).bind fun (b : ℕ) ↦ (↑(decode (a, b).2) : Part σ)) =
    bif c a then f a else g a

Tactic:
cases c a
-- Module: Mathlib.Computability.RE
Goal:
α : Type u_1
σ : Type u_4
inst : Primcodable α
inst_1 : Primcodable σ
c : α → Bool
f g : α →. σ
hc : Computable c
hf : Partrec f
hg : Partrec g
cf : Code
ef : cf.eval = fun (n : ℕ) ↦ Part.bind (↑(decode n) : Part α) fun (a : α) ↦ Part.map encode (f a)
cg : Code
eg : cg.eval = fun (n : ℕ) ↦ Part.bind (↑(decode n) : Part α) fun (a : α) ↦ Part.map encode (g a)
a : α
⊢ (((bif false then cf else cg).eval (encode a)).bind fun (b : ℕ) ↦ (↑(decode (a, b).2) : Part σ)) =
    bif false then f a else g a

Tactic:
simp [ef, eg, encodek]

Premises used: Encodable.encodek
-- Module: Mathlib.Computability.RE
Goal:
α : Type u_1
σ : Type u_4
inst : Primcodable α
inst_1 : Primcodable σ
c : α → Bool
f g : α →. σ
hc : Computable c
hf : Partrec f
hg : Partrec g
cf : Code
ef : cf.eval = fun (n : ℕ) ↦ Part.bind (↑(decode n) : Part α) fun (a : α) ↦ Part.map encode (f a)
cg : Code
eg : cg.eval = fun (n : ℕ) ↦ Part.bind (↑(decode n) : Part α) fun (a : α) ↦ Part.map encode (g a)
a : α
⊢ (((bif true then cf else cg).eval (encode a)).bind fun (b : ℕ) ↦ (↑(decode (a, b).2) : Part σ)) =
    bif true then f a else g a

Tactic:
simp [ef, eg, encodek]

Premises used: Encodable.encodek
-- Module: Mathlib.Computability.RE
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 : α → β →. σ
h : α → γ →. σ
hf : Computable f
hg : Partrec₂ g
hh : Partrec₂ h
a : α
inl :
  ∀ (val : β),
    Eq.{u_4 + 1} (α := Part (Option σ))
      (bif Sum.casesOn (motive := fun (x : β ⊕ γ) ↦ Bool) (Sum.inl val) (fun (b : β) ↦ true) fun (b : γ) ↦ false then
          Sum.casesOn (motive := fun (x : β ⊕ γ) ↦ Part (Option σ)) (Sum.inl val)
            (fun (b : β) ↦ Part.map Option.some (g (a, b).1 (a, b).2)) fun (c : γ) ↦ Part.some Option.none
        else
          Sum.casesOn (motive := fun (x : β ⊕ γ) ↦ Part (Option σ)) (Sum.inl val) (fun (b : β) ↦ Part.some Option.none)
            fun (b : γ) ↦ Part.map Option.some (h (a, b).1 (a, b).2) :
        Part (Option σ))
      (Part.map Option.some (Sum.casesOn (motive := fun (x : β ⊕ γ) ↦ Part σ) (Sum.inl val) (g a) (h a)) :
        Part (Option σ))
inr :
  ∀ (val : γ),
    Eq.{u_4 + 1} (α := Part (Option σ))
      (bif Sum.casesOn (motive := fun (x : β ⊕ γ) ↦ Bool) (Sum.inr val) (fun (b : β) ↦ true) fun (b : γ) ↦ false then
          Sum.casesOn (motive := fun (x : β ⊕ γ) ↦ Part (Option σ)) (Sum.inr val)
            (fun (b : β) ↦ Part.map Option.some (g (a, b).1 (a, b).2)) fun (c : γ) ↦ Part.some Option.none
        else
          Sum.casesOn (motive := fun (x : β ⊕ γ) ↦ Part (Option σ)) (Sum.inr val) (fun (b : β) ↦ Part.some Option.none)
            fun (b : γ) ↦ Part.map Option.some (h (a, b).1 (a, b).2) :
        Part (Option σ))
      (Part.map Option.some (Sum.casesOn (motive := fun (x : β ⊕ γ) ↦ Part σ) (Sum.inr val) (g a) (h a)) :
        Part (Option σ))
⊢ Eq.{u_4 + 1} (α := Part (Option σ))
    (bif Sum.casesOn (motive := fun (x : β ⊕ γ) ↦ Bool) (f a) (fun (b : β) ↦ true) fun (b : γ) ↦ false then
        Sum.casesOn (motive := fun (x : β ⊕ γ) ↦ Part (Option σ)) (f a)
          (fun (b : β) ↦ Part.map Option.some (g (a, b).1 (a, b).2)) fun (c : γ) ↦ Part.some Option.none
      else
        Sum.casesOn (motive := fun (x : β ⊕ γ) ↦ Part (Option σ)) (f a) (fun (b : β) ↦ Part.some Option.none)
          fun (b : γ) ↦ Part.map Option.some (h (a, b).1 (a, b).2) :
      Part (Option σ))
    (Part.map Option.some (Sum.casesOn (motive := fun (x : β ⊕ γ) ↦ Part σ) (f a) (g a) (h a)) : Part (Option σ))

Tactic:
cases f a
-- Module: Mathlib.Computability.RE
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 : α → β →. σ
h : α → γ →. σ
hf : Computable f
hg : Partrec₂ g
hh : Partrec₂ h
a : α
val : β
⊢ Eq.{u_4 + 1} (α := Part (Option σ))
    (bif Sum.casesOn (motive := fun (x : β ⊕ γ) ↦ Bool) (Sum.inl val) (fun (b : β) ↦ true) fun (b : γ) ↦ false then
        Sum.casesOn (motive := fun (x : β ⊕ γ) ↦ Part (Option σ)) (Sum.inl val)
          (fun (b : β) ↦ Part.map Option.some (g (a, b).1 (a, b).2)) fun (c : γ) ↦ Part.some Option.none
      else
        Sum.casesOn (motive := fun (x : β ⊕ γ) ↦ Part (Option σ)) (Sum.inl val) (fun (b : β) ↦ Part.some Option.none)
          fun (b : γ) ↦ Part.map Option.some (h (a, b).1 (a, b).2) :
      Part (Option σ))
    (Part.map Option.some (Sum.casesOn (motive := fun (x : β ⊕ γ) ↦ Part σ) (Sum.inl val) (g a) (h a)) :
      Part (Option σ))

Tactic:
simp only [Bool.cond_true, Bool.cond_false]

Premises used: Bool.cond_true, Bool.cond_false
-- Module: Mathlib.Computability.RE
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 : α → β →. σ
h : α → γ →. σ
hf : Computable f
hg : Partrec₂ g
hh : Partrec₂ h
a : α
val : γ
⊢ Eq.{u_4 + 1} (α := Part (Option σ))
    (bif Sum.casesOn (motive := fun (x : β ⊕ γ) ↦ Bool) (Sum.inr val) (fun (b : β) ↦ true) fun (b : γ) ↦ false then
        Sum.casesOn (motive := fun (x : β ⊕ γ) ↦ Part (Option σ)) (Sum.inr val)
          (fun (b : β) ↦ Part.map Option.some (g (a, b).1 (a, b).2)) fun (c : γ) ↦ Part.some Option.none
      else
        Sum.casesOn (motive := fun (x : β ⊕ γ) ↦ Part (Option σ)) (Sum.inr val) (fun (b : β) ↦ Part.some Option.none)
          fun (b : γ) ↦ Part.map Option.some (h (a, b).1 (a, b).2) :
      Part (Option σ))
    (Part.map Option.some (Sum.casesOn (motive := fun (x : β ⊕ γ) ↦ Part σ) (Sum.inr val) (g a) (h a)) :
      Part (Option σ))

Tactic:
simp only [Bool.cond_true, Bool.cond_false]

Premises used: Bool.cond_true, Bool.cond_false
-- Module: Mathlib.Computability.RE
Goal:
α : Type u_1
inst : Primcodable α
p : α → Prop
inst_1 : DecidablePred p
hp : ComputablePred p
⊢ Computable (σ := Bool) fun (a : α) ↦ decide (p a)

Tactic:
hp.choose_spec

Premises used: Exists.choose_spec
-- Module: Mathlib.Computability.RE
Goal:
α : Type u_1
inst : Primcodable α
p : α → Prop
inst_1 : DecidablePred p
hp : ComputablePred p
⊢ Computable (σ := Bool) fun (a : α) ↦ decide (p a)

Tactic:
convert! hp.choose_spec

Premises used: Exists.choose_spec
-- Module: Mathlib.Computability.RE
Goal:
α : Type u_1
inst : Primcodable α
p : α → Prop
inst_1 : DecidablePred p
hp : Computable (σ := Bool) fun (a : α) ↦ decide (p a)
⊢ ComputablePred p

Tactic:
⟨inferInstance, hp⟩

Premises used: inferInstance, Exists.intro, ComputablePred
-- Module: Mathlib.Computability.RE
Goal:
α : Type u_1
inst : Primcodable α
p q : α → Prop
hp : REPred p
H : ∀ (a : α), p a ↔ q a
⊢ REPred q

Tactic:
(funext fun a => propext (H a) : p = q) ▸ hp

Premises used: Eq.rec, funext, propext
-- Module: Mathlib.Computability.RE
Goal:
α : Type u_1
β : Type u_2
inst : Primcodable α
inst_1 : Primcodable β
f : α →. β
h : Partrec f
n : α
x : Unit
⊢ Membership.mem (γ := Part Unit) (Part.map (fun (b : β) ↦ ()) (f n)) x ↔
    Membership.mem (γ := Part Unit)
      (Part.assert ((fun (a : α) ↦ (f a).Dom) n) fun (x : (fun (a : α) ↦ (f a).Dom) n) ↦ Part.some ()) x

Tactic:
simp [Part.dom_iff_mem]

Premises used: Part.dom_iff_mem
-- Module: Mathlib.Computability.RE
Goal:
α : Type u_1
inst : Primcodable α
p q : α → Prop
hp : ComputablePred p
H : ∀ (a : α), p a ↔ q a
⊢ ComputablePred q

Tactic:
(funext fun a => propext (H a) : p = q) ▸ hp

Premises used: Eq.rec, funext, propext
-- Module: Mathlib.Computability.RE
Goal:
α : Type u_1
inst : Primcodable α
P : α → ℕ → Prop
inst_1 : DecidableRel P
hP_comp : ComputablePred fun (p : α × ℕ) ↦ P p.1 p.2
hP_ex : ∀ (x : α), ∃ (n : ℕ), P x n
⊢ Partrec.{u_1, 0} (α := α) (σ := ℕ) fun (x : α) ↦ Nat.rfind fun (n : ℕ) ↦ Part.some (decide (P x n))

Tactic:
have h : Partrec (fun x ↦ Nat.rfind fun n => Part.some (decide (P x n))) :=
    Partrec.rfind hP_comp.decide.partrec
-- Module: Mathlib.Computability.RE
Goal:
α : Type u_1
inst : Primcodable α
P : α → ℕ → Prop
inst_1 : DecidableRel P
hP_comp : ComputablePred fun (p : α × ℕ) ↦ P p.1 p.2
hP_ex : ∀ (x : α), ∃ (n : ℕ), P x n
h : Partrec.{u_1, 0} (α := α) (σ := ℕ) fun (x : α) ↦ Nat.rfind fun (n : ℕ) ↦ Part.some (decide (P x n))
⊢ Computable (σ := ℕ) fun (x : α) ↦ Nat.find (p := P x) ⋯

Tactic:
h.of_eq_tot fun x ↦ ?_

Premises used: Partrec.of_eq_tot
-- Module: Mathlib.Computability.RE
Goal:
α : Type u_1
inst : Primcodable α
P : α → ℕ → Prop
inst_1 : DecidableRel P
hP_comp : ComputablePred fun (p : α × ℕ) ↦ P p.1 p.2
hP_ex : ∀ (x : α), ∃ (n : ℕ), P x n
h : Partrec.{u_1, 0} (α := α) (σ := ℕ) fun (x : α) ↦ Nat.rfind fun (n : ℕ) ↦ Part.some (decide (P x n))
refine : ∀ (x : α), Nat.find (p := P x) ⋯ ∈ Nat.rfind fun (n : ℕ) ↦ Part.some (decide (P x n))
⊢ Computable (σ := ℕ) fun (x : α) ↦ Nat.find (p := P x) ⋯

Tactic:
refine h.of_eq_tot fun x ↦ ?_

Premises used: Partrec.of_eq_tot