awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Computability.RE
Goal:
cf : Code
hf : Nat.Partrec cf.eval
cg : Code
hg : Nat.Partrec cg.eval
this_1 : Nat.Partrec fun (n : ℕ) ↦ rfindOpt fun (k : ℕ) ↦ Code.evaln k cf n <|> Code.evaln k cg n
n : ℕ
this :
  ∀ (x : ℕ),
    Membership.mem (γ := Part ℕ) (rfindOpt fun (k : ℕ) ↦ Code.evaln k cf n <|> Code.evaln k cg n) x →
      x ∈ cf.eval n ∨ x ∈ cg.eval n
x k : ℕ
e : Code.evaln k cg n = Option.some x
y : ℕ
⊢ ∃ (a : ℕ), a ∈ (Option.some y <|> Code.evaln k cg n)

Tactic:
exact ⟨y, by simp⟩
-- Module: Mathlib.Computability.RE
Goal:
α : Type u_1
σ : Type u_4
inst : Primcodable α
inst_1 : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
let :
  ∀ (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 : α →. σ), Partrec k ∧ ∀ (a : α), (∀ x ∈ k a, x ∈ f a ∨ x ∈ g a) ∧ ((k a).Dom ↔ (f a).Dom ∨ (g a).Dom)
⊢ ∃ (k : α →. σ), Partrec k ∧ ∀ (a : α), (∀ x ∈ k a, x ∈ f a ∨ x ∈ g a) ∧ ((k a).Dom ↔ (f a).Dom ∨ (g a).Dom)

Tactic:
let ⟨k, hk, H⟩ := Nat.Partrec.merge' (bind_decode₂_iff.1 hf) (bind_decode₂_iff.1 hg)
-- 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 σ)
⊢ ∃ (k : α →. σ), Partrec k ∧ ∀ (a : α), (∀ x ∈ k a, x ∈ f a ∨ x ∈ g a) ∧ ((k a).Dom ↔ (f a).Dom ∨ (g a).Dom)

Tactic:
⟨k', ((nat_iff.2 hk).comp Computable.encode).bind (Computable.decode.ofOption.comp snd).to₂,
      fun a => ?_⟩

Premises used: Iff.mpr, Computable.encode, Computable.decode, Partrec.bind, Computable.snd, Computable.ofOption, Partrec.nat_iff, Partrec.to₂, And.intro, Exists.intro, Partrec.comp
-- 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 σ)
fun : ∀ (a : α), (∀ x ∈ k' a, x ∈ f a ∨ x ∈ g a) ∧ ((k' a).Dom ↔ (f a).Dom ∨ (g a).Dom)
⊢ ∃ (k : α →. σ), Partrec k ∧ ∀ (a : α), (∀ x ∈ k a, x ∈ f a ∨ x ∈ g a) ∧ ((k a).Dom ↔ (f a).Dom ∨ (g a).Dom)

Tactic:
refine
    ⟨k', ((nat_iff.2 hk).comp Computable.encode).bind (Computable.decode.ofOption.comp snd).to₂,
      fun a => ?_⟩
-- 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 : α
x : σ
h' : x ∈ k' a
⊢ ∃ a_1 ∈ k (encode a), decode a_1 = Option.some x

Tactic:
simp only [k', mem_coe, mem_bind_iff, Option.mem_def] at h'

Premises used: Part.mem_bind_iff, Part.mem_coe, 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 : 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 : α
x : σ
h' : ∃ a_1 ∈ k (encode a), decode a_1 = Option.some x
obtain : ∀ (n : ℕ) (hn : n ∈ k (encode a)) (hx : decode n = Option.some x), x ∈ f a ∨ x ∈ g a
⊢ x ∈ f a ∨ x ∈ g a

Tactic:
obtain ⟨n, hn, hx⟩ := 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 : 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 : α
x : σ
n : ℕ
hn : n ∈ k (encode a)
hx : decode n = Option.some x
⊢ Membership.mem (γ := Part ℕ) ((↑(decode₂ α (encode a)) : Part α).bind fun (a : α) ↦ Part.map encode (f a)) n ∨
    Membership.mem (γ := Part ℕ) ((↑(decode₂ α (encode a)) : Part α).bind fun (a : α) ↦ Part.map encode (g a)) n

Tactic:
have := (H _).1 _ hn
-- 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 : α
x : σ
n : ℕ
hn : n ∈ k (encode a)
hx : decode n = Option.some x
this :
  Membership.mem (γ := Part ℕ) ((↑(decode₂ α (encode a)) : Part α).bind fun (a : α) ↦ Part.map encode (f a)) n ∨
    Membership.mem (γ := Part ℕ) ((↑(decode₂ α (encode a)) : Part α).bind fun (a : α) ↦ Part.map encode (g a)) n
⊢ (∃ a_1 ∈ f a, encode a_1 = n) ∨ ∃ a_1 ∈ g a, encode a_1 = n

Tactic:
simp only [decode₂_encode, coe_some, bind_some, mem_map_iff] at this

Premises used: Part.bind_some, Part.coe_some, Encodable.decode₂_encode, Part.mem_map_iff
-- 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 : α
x : σ
n : ℕ
hn : n ∈ k (encode a)
hx : decode n = Option.some x
this : (∃ a_1 ∈ f a, encode a_1 = n) ∨ ∃ a_1 ∈ g a, encode a_1 = n
inl :
  ∀ (a' : σ) (ha : a' ∈ f a) (hn : encode a' ∈ k (encode a)) (hx : decode (encode a') = Option.some x),
    x ∈ f a ∨ x ∈ g a
inr :
  ∀ (a' : σ) (ha : a' ∈ g a) (hn : encode a' ∈ k (encode a)) (hx : decode (encode a') = Option.some x),
    x ∈ f a ∨ x ∈ g a
⊢ x ∈ f a ∨ x ∈ g a

Tactic:
obtain ⟨a', ha, rfl⟩ | ⟨a', ha, rfl⟩ := this

Premises used: 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 : 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 : α
x a' : σ
ha : a' ∈ f a
hn : encode a' ∈ k (encode a)
hx : decode (encode a') = Option.some x
⊢ a' = x

Tactic:
simp only [encodek, Option.some_inj] at hx

Premises used: Encodable.encodek, Option.some_inj
-- 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 : α
x a' : σ
ha : a' ∈ g a
hn : encode a' ∈ k (encode a)
hx : decode (encode a') = Option.some x
⊢ a' = x

Tactic:
simp only [encodek, Option.some_inj] at hx

Premises used: Encodable.encodek, Option.some_inj
-- 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 : α
x a' : σ
ha : a' ∈ f a
hn : encode a' ∈ k (encode a)
hx : a' = x
⊢ x ∈ f a

Tactic:
rw [hx] at ha
-- 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 : α
x a' : σ
ha : a' ∈ f a
hn : encode a' ∈ k (encode a)
hx : a' = x
ha₁ : x ∈ f a
⊢ encode a' ∈ k (encode a)

Tactic:
rw [hx] at ha
-- 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 : α
x a' : σ
ha : a' ∈ f a
hn : encode a' ∈ k (encode a)
hx : a' = x
ha₁ : x ∈ f a
hn₁ : encode a' ∈ k (encode a)
⊢ a' = x

Tactic:
rw [hx] at ha
-- 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 : α
x a' : σ
ha : a' ∈ g a
hn : encode a' ∈ k (encode a)
hx : a' = x
⊢ x ∈ g a

Tactic:
rw [hx] at ha
-- 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 : α
x a' : σ
ha : a' ∈ g a
hn : encode a' ∈ k (encode a)
hx : a' = x
ha₁ : x ∈ g a
⊢ encode a' ∈ k (encode a)

Tactic:
rw [hx] at ha
-- 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 : α
x a' : σ
ha : a' ∈ g a
hn : encode a' ∈ k (encode a)
hx : a' = x
ha₁ : x ∈ g a
hn₁ : encode a' ∈ k (encode a)
⊢ a' = x

Tactic:
rw [hx] at ha
-- 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 : α
x a' : σ
ha : x ∈ f a
hn : encode a' ∈ k (encode a)
hx : a' = x
⊢ x ∈ f a ∨ x ∈ g a

Tactic:
Or.inl ha

Premises used: Or.inl
-- 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 : α
x a' : σ
ha : x ∈ f a
hn : encode a' ∈ k (encode a)
hx : a' = x
⊢ x ∈ f a ∨ x ∈ g a

Tactic:
exact Or.inl ha

Premises used: Or.inl
-- 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 : α
x a' : σ
ha : x ∈ g a
hn : encode a' ∈ k (encode a)
hx : a' = x
⊢ x ∈ f a ∨ x ∈ g a

Tactic:
Or.inr ha

Premises used: Or.inr
-- 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 : α
x a' : σ
ha : x ∈ g a
hn : encode a' ∈ k (encode a)
hx : a' = x
⊢ x ∈ f a ∨ x ∈ g a

Tactic:
exact Or.inr ha

Premises used: Or.inr
-- 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 : α
⊢ ∀ x ∈ k' a, x ∈ f a ∨ x ∈ g a

Tactic:
have : ∀ x ∈ k' a, x ∈ f a ∨ x ∈ g a := by
    intro x h'
    simp only [k', mem_coe, mem_bind_iff, Option.mem_def] at h'
    obtain ⟨n, hn, hx⟩ := h'
    have := (H _).1 _ hn
    simp only [decode₂_encode, coe_some, bind_some, mem_map_iff] at this
    obtain ⟨a', ha, rfl⟩ | ⟨a', ha, rfl⟩ := this <;> simp only [encodek, Option.some_inj] at hx <;>
      rw [hx] at ha
    · exact Or.inl ha
    · exact Or.inr ha
-- 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
⊢ (∀ x ∈ k' a, x ∈ f a ∨ x ∈ g a) ∧ ((k' a).Dom ↔ (f a).Dom ∨ (g a).Dom)

Tactic:
⟨this, ⟨fun h => (this _ ⟨h, rfl⟩).imp Exists.fst Exists.fst, ?_⟩⟩

Premises used: Exists.fst, Part.get, And.intro, Iff.intro, Exists.intro, Or.imp, 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 : 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
refine : (f a).Dom ∨ (g a).Dom → (k' a).Dom
⊢ (∀ x ∈ k' a, x ∈ f a ∨ x ∈ g a) ∧ ((k' a).Dom ↔ (f a).Dom ∨ (g a).Dom)

Tactic:
refine ⟨this, ⟨fun h => (this _ ⟨h, rfl⟩).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
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
rw : ∃ (h : (k (encode a)).Dom), Dom.{u_4} (α := σ) (↑(decode ((k (encode a)).get h)) : Part σ)
⊢ (k' a).Dom

Tactic:
rw [bind_dom]

Premises used: Part.bind_dom