-- Mathlib/Computability/Halting.lean
theorem merge' {f g : α →. σ} (hf : Partrec f) (hg : Partrec g) :
    ∃ k : α →. σ,
      Partrec k ∧ ∀ a, (∀ x ∈ k a, x ∈ f a ∨ x ∈ g a) ∧ ((k a).Dom ↔ (f a).Dom ∨ (g a).Dom)

Proof state:
α : Type u_1
σ : Type u_4
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
k : ℕ →. ℕ
hk : Nat.Partrec k
H :
  ∀ (a : ℕ),
    (∀ x ∈ k a,
        (x ∈ (↑(decode₂ α a)).bind fun a => Part.map encode (f a)) ∨
          x ∈ (↑(decode₂ α a)).bind fun a => Part.map encode (g a)) ∧
      ((k a).Dom ↔
        ((↑(decode₂ α a)).bind fun a => Part.map encode (f a)).Dom ∨
          ((↑(decode₂ α a)).bind fun a => Part.map encode (g a)).Dom)
k' : α → Part σ := fun a => (k (encode a)).bind fun n => ↑(decode n)
a : α
x : σ
h' : x ∈ k' a
⊢ x ∈ f a ∨ x ∈ g a

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

Result:
α : Type u_1
σ : Type u_4
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
k : ℕ →. ℕ
hk : Nat.Partrec k
H :
  ∀ (a : ℕ),
    (∀ x ∈ k a,
        (x ∈ (↑(decode₂ α a)).bind fun a => Part.map encode (f a)) ∨
          x ∈ (↑(decode₂ α a)).bind fun a => Part.map encode (g a)) ∧
      ((k a).Dom ↔
        ((↑(decode₂ α a)).bind fun a => Part.map encode (f a)).Dom ∨
          ((↑(decode₂ α a)).bind fun a => Part.map encode (g a)).Dom)
k' : α → Part σ := fun a => (k (encode a)).bind fun n => ↑(decode n)
a : α
x : σ
h' : ∃ a_1 ∈ k (encode a), decode a_1 = Option.some x
⊢ x ∈ f a ∨ x ∈ g a

Proof state:
case intro.intro.inr.intro.intro
α : Type u_1
σ : Type u_4
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
k : ℕ →. ℕ
hk : Nat.Partrec k
H :
  ∀ (a : ℕ),
    (∀ x ∈ k a,
        (x ∈ (↑(decode₂ α a)).bind fun a => Part.map encode (f a)) ∨
          x ∈ (↑(decode₂ α a)).bind fun a => Part.map encode (g a)) ∧
      ((k a).Dom ↔
        ((↑(decode₂ α a)).bind fun a => Part.map encode (f a)).Dom ∨
          ((↑(decode₂ α a)).bind fun a => Part.map encode (g a)).Dom)
k' : α → Part σ := fun a => (k (encode a)).bind fun n => ↑(decode n)
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

Result:
no goals

Proof state:
α : Type u_1
σ : Type u_4
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
k : ℕ →. ℕ
hk : Nat.Partrec k
H :
  ∀ (a : ℕ),
    (∀ x ∈ k a,
        (x ∈ (↑(decode₂ α a)).bind fun a => Part.map encode (f a)) ∨
          x ∈ (↑(decode₂ α a)).bind fun a => Part.map encode (g a)) ∧
      ((k a).Dom ↔
        ((↑(decode₂ α a)).bind fun a => Part.map encode (f a)).Dom ∨
          ((↑(decode₂ α a)).bind fun a => Part.map encode (g a)).Dom)
k' : α → Part σ := fun a => (k (encode a)).bind fun n => ↑(decode n)
a : α
this : ∀ x ∈ k' a, x ∈ f a ∨ x ∈ g a
⊢ (f a).Dom ∨ (g a).Dom → (k' a).Dom

Tactic:
intro h

Result:
α : Type u_1
σ : Type u_4
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
k : ℕ →. ℕ
hk : Nat.Partrec k
H :
  ∀ (a : ℕ),
    (∀ x ∈ k a,
        (x ∈ (↑(decode₂ α a)).bind fun a => Part.map encode (f a)) ∨
          x ∈ (↑(decode₂ α a)).bind fun a => Part.map encode (g a)) ∧
      ((k a).Dom ↔
        ((↑(decode₂ α a)).bind fun a => Part.map encode (f a)).Dom ∨
          ((↑(decode₂ α a)).bind fun a => Part.map encode (g a)).Dom)
k' : α → Part σ := fun a => (k (encode a)).bind fun n => ↑(decode n)
a : α
this : ∀ x ∈ k' a, x ∈ f a ∨ x ∈ g a
h : (f a).Dom ∨ (g a).Dom
⊢ (k' a).Dom

Proof state:
α : Type u_1
σ : Type u_4
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
k : ℕ →. ℕ
hk✝ : Nat.Partrec k
H :
  ∀ (a : ℕ),
    (∀ x ∈ k a,
        (x ∈ (↑(decode₂ α a)).bind fun a => Part.map encode (f a)) ∨
          x ∈ (↑(decode₂ α a)).bind fun a => Part.map encode (g a)) ∧
      ((k a).Dom ↔
        ((↑(decode₂ α a)).bind fun a => Part.map encode (f a)).Dom ∨
          ((↑(decode₂ α a)).bind fun a => Part.map encode (g a)).Dom)
k' : α → Part σ := fun a => (k (encode a)).bind fun n => ↑(decode n)
a : α
this : ∀ x ∈ k' a, x ∈ f a ∨ x ∈ g a
h : (f a).Dom ∨ (g a).Dom
hk : (k (encode a)).Dom
⊢ (↑(decode ((k (encode a)).get hk))).Dom

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

Result:
α : Type u_1
σ : Type u_4
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
k : ℕ →. ℕ
hk✝ : Nat.Partrec k
k' : α → Part σ := fun a => (k (encode a)).bind fun n => ↑(decode n)
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 ↔
        ((↑(decode₂ α a)).bind fun a => Part.map encode (f a)).Dom ∨
          ((↑(decode₂ α a)).bind fun a => Part.map encode (g a)).Dom)
⊢ (↑(decode ((k (encode a)).get hk))).Dom

Proof state:
α : Type u_1
σ : Type u_4
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
⊢ ∃ 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)

Result:
α : Type u_1
σ : Type u_4
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
k : ℕ →. ℕ
hk : Nat.Partrec k
H :
  ∀ (a : ℕ),
    (∀ x ∈ k a,
        (x ∈ (↑(decode₂ α a)).bind fun a => Part.map encode (f a)) ∨
          x ∈ (↑(decode₂ α a)).bind fun a => Part.map encode (g a)) ∧
      ((k a).Dom ↔
        ((↑(decode₂ α a)).bind fun a => Part.map encode (f a)).Dom ∨
          ((↑(decode₂ α a)).bind fun a => Part.map encode (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)

Proof state:
α : Type u_1
σ : Type u_4
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
k : ℕ →. ℕ
hk : Nat.Partrec k
H :
  ∀ (a : ℕ),
    (∀ x ∈ k a,
        (x ∈ (↑(decode₂ α a)).bind fun a => Part.map encode (f a)) ∨
          x ∈ (↑(decode₂ α a)).bind fun a => Part.map encode (g a)) ∧
      ((k a).Dom ↔
        ((↑(decode₂ α a)).bind fun a => Part.map encode (f a)).Dom ∨
          ((↑(decode₂ α a)).bind fun a => Part.map encode (g a)).Dom)
k' : α → Part σ := fun a => (k (encode a)).bind fun n => ↑(decode n)
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:
refine ⟨this, ⟨fun h => (this _ ⟨h, rfl⟩).imp Exists.fst Exists.fst, ?_⟩⟩

Result:
α : Type u_1
σ : Type u_4
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f g : α →. σ
hf : Partrec f
hg : Partrec g
k : ℕ →. ℕ
hk : Nat.Partrec k
H :
  ∀ (a : ℕ),
    (∀ x ∈ k a,
        (x ∈ (↑(decode₂ α a)).bind fun a => Part.map encode (f a)) ∨
          x ∈ (↑(decode₂ α a)).bind fun a => Part.map encode (g a)) ∧
      ((k a).Dom ↔
        ((↑(decode₂ α a)).bind fun a => Part.map encode (f a)).Dom ∨
          ((↑(decode₂ α a)).bind fun a => Part.map encode (g a)).Dom)
k' : α → Part σ := fun a => (k (encode a)).bind fun n => ↑(decode n)
a : α
this : ∀ x ∈ k' a, x ∈ f a ∨ x ∈ g a
⊢ (f a).Dom ∨ (g a).Dom → (k' a).Dom