-- 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:
case intro.intro.inl.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 ∈ f a
hn : encode a' ∈ k (encode a)
hx : a' = x
⊢ x ∈ f a ∨ x ∈ g a

Tactic:
exact Or.inl 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
h : (f a).Dom ∨ (g a).Dom
⊢ ((↑(decode₂ α (encode a))).bind fun a => Part.map encode (f a)).Dom ∨
    ((↑(decode₂ α (encode a))).bind fun a => Part.map encode (g a)).Dom

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

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
h : (f a).Dom ∨ (g a).Dom
hk : (k (encode a)).Dom
⊢ ∃ (h : (k (encode a)).Dom), (↑(decode ((k (encode a)).get h))).Dom

Tactic:
exists hk

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
hk : (k (encode 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 : ℕ →. ℕ
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)
⊢ ∃ 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 => ?_⟩

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 ∈ k' a, x ∈ f a ∨ x ∈ g a) ∧ ((k' a).Dom ↔ (f a).Dom ∨ (g a).Dom)

Proof state:
case 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 : σ
n : ℕ
hn : n ∈ k (encode a)
hx : decode n = Option.some x
⊢ x ∈ f a ∨ x ∈ g a

Tactic:
have := (H _).1 _ hn

Result:
case 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 : σ
n : ℕ
hn : n ∈ k (encode a)
hx : decode n = Option.some x
this :
  (n ∈ (↑(decode₂ α (encode a))).bind fun a => Part.map encode (f a)) ∨
    n ∈ (↑(decode₂ α (encode a))).bind fun a => Part.map encode (g a)
⊢ x ∈ f a ∨ x ∈ g a

Proof state:
case 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 : σ
n : ℕ
hn : n ∈ k (encode a)
hx : decode n = Option.some x
this :
  (n ∈ (↑(decode₂ α (encode a))).bind fun a => Part.map encode (f a)) ∨
    n ∈ (↑(decode₂ α (encode a))).bind fun a => Part.map encode (g a)
⊢ x ∈ f a ∨ x ∈ g a

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

Result:
case 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 : σ
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
⊢ x ∈ f a ∨ x ∈ g a