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

Proof state:
case intro.some
cf : Code
hf : Partrec cf.eval
cg : Code
hg : Partrec cg.eval
this : Partrec fun n => rfindOpt fun k => Code.evaln k cf n <|> Code.evaln k cg n
n x : ℕ
h : x ∈ rfindOpt fun k => Code.evaln k cf n <|> Code.evaln k cg n
k y : ℕ
e' : Code.evaln k cf n = Option.some y
e : y = x
⊢ x ∈ cf.eval n ∨ x ∈ cg.eval n

Tactic:
subst y

Result:
case intro.some
cf : Code
hf : Partrec cf.eval
cg : Code
hg : Partrec cg.eval
this : Partrec fun n => rfindOpt fun k => Code.evaln k cf n <|> Code.evaln k cg n
n x : ℕ
h : x ∈ rfindOpt fun k => Code.evaln k cf n <|> Code.evaln k cg n
k : ℕ
e' : Code.evaln k cf n = Option.some x
⊢ x ∈ cf.eval n ∨ x ∈ cg.eval n

Proof state:
case intro
cf : Code
hf : Partrec cf.eval
cg : Code
hg : Partrec cg.eval
this : Partrec fun n => rfindOpt fun k => Code.evaln k cf n <|> Code.evaln k cg n
n x : ℕ
h : x ∈ rfindOpt fun k => Code.evaln k cf n <|> Code.evaln k cg n
k : ℕ
⊢ x ∈ (Code.evaln k cf n <|> Code.evaln k cg n) → x ∈ cf.eval n ∨ x ∈ cg.eval n

Tactic:
simp only [Option.mem_def]

Result:
case intro
cf : Code
hf : Partrec cf.eval
cg : Code
hg : Partrec cg.eval
this : Partrec fun n => rfindOpt fun k => Code.evaln k cf n <|> Code.evaln k cg n
n x : ℕ
h : x ∈ rfindOpt fun k => Code.evaln k cf n <|> Code.evaln k cg n
k : ℕ
⊢ (Code.evaln k cf n <|> Code.evaln k cg n) = Option.some x → x ∈ cf.eval n ∨ x ∈ cg.eval n

Proof state:
case intro.intro.inr.intro.intro.some
cf : Code
hf : Partrec cf.eval
cg : Code
hg : Partrec cg.eval
this✝ : Partrec fun n => rfindOpt fun k => Code.evaln k cf n <|> Code.evaln k cg n
n : ℕ
this : ∀ x ∈ rfindOpt fun k => Code.evaln k cf n <|> Code.evaln k cg n, 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 only [Option.some_orElse, Option.mem_def]⟩

Result:
no goals

Proof state:
case intro.intro.inr.intro.intro.none
cf : Code
hf : Partrec cf.eval
cg : Code
hg : Partrec cg.eval
this✝ : Partrec fun n => rfindOpt fun k => Code.evaln k cf n <|> Code.evaln k cg n
n : ℕ
this : ∀ x ∈ rfindOpt fun k => Code.evaln k cf n <|> Code.evaln k cg n, x ∈ cf.eval n ∨ x ∈ cg.eval n
x k : ℕ
e : Code.evaln k cg n = Option.some x
⊢ ∃ a, a ∈ (Option.none <|> Code.evaln k cg n)

Tactic:
exact ⟨x, by simp only [e, Option.mem_def, Option.none_orElse]⟩

Result:
no goals

Proof state:
case intro.intro.inl.intro.intro
cf : Code
hf : Partrec cf.eval
cg : Code
hg : Partrec cg.eval
this✝ : Partrec fun n => rfindOpt fun k => Code.evaln k cf n <|> Code.evaln k cg n
n : ℕ
this : ∀ x ∈ rfindOpt fun k => Code.evaln k cf n <|> Code.evaln k cg n, x ∈ cf.eval n ∨ x ∈ cg.eval n
x k : ℕ
e : Code.evaln k cf n = Option.some x
⊢ x ∈ (Code.evaln k cf n <|> Code.evaln k cg n)

Tactic:
simp only [e, Option.some_orElse, Option.mem_def]

Result:
no goals

Proof state:
case intro.some
cf : Code
hf : Partrec cf.eval
cg : Code
hg : Partrec cg.eval
this : Partrec fun n => rfindOpt fun k => Code.evaln k cf n <|> Code.evaln k cg n
n x : ℕ
h : x ∈ rfindOpt fun k => Code.evaln k cf n <|> Code.evaln k cg n
k : ℕ
e' : Code.evaln k cf n = Option.some x
⊢ x ∈ cf.eval n ∨ x ∈ cg.eval n

Tactic:
exact Or.inl (Code.evaln_sound e')

Result:
no goals

Proof state:
f g : ℕ →. ℕ
hf : Partrec f
hg : Partrec g
⊢ ∃ h, Partrec h ∧ ∀ (a : ℕ), (∀ x ∈ h a, x ∈ f a ∨ x ∈ g a) ∧ ((h a).Dom ↔ (f a).Dom ∨ (g a).Dom)

Tactic:
obtain ⟨cf, rfl⟩ := Code.exists_code.1 hf

Result:
case intro
g : ℕ →. ℕ
hg : Partrec g
cf : Code
hf : Partrec cf.eval
⊢ ∃ h, Partrec h ∧ ∀ (a : ℕ), (∀ x ∈ h a, x ∈ cf.eval a ∨ x ∈ g a) ∧ ((h a).Dom ↔ (cf.eval a).Dom ∨ (g a).Dom)

Proof state:
cf : Code
hf : Partrec cf.eval
cg : Code
hg : Partrec cg.eval
this✝ : Partrec fun n => rfindOpt fun k => Code.evaln k cf n <|> Code.evaln k cg n
n : ℕ
this : ∀ x ∈ rfindOpt fun k => Code.evaln k cf n <|> Code.evaln k cg n, x ∈ cf.eval n ∨ x ∈ cg.eval n
x k : ℕ
e : Code.evaln k cg n = Option.some x
⊢ x ∈ (Option.none <|> Code.evaln k cg n)

Tactic:
simp only [e, Option.mem_def, Option.none_orElse]

Result:
no goals

Proof state:
case intro.none
cf : Code
hf : Partrec cf.eval
cg : Code
hg : Partrec cg.eval
this : Partrec fun n => rfindOpt fun k => Code.evaln k cf n <|> Code.evaln k cg n
n x : ℕ
h : x ∈ rfindOpt fun k => Code.evaln k cf n <|> Code.evaln k cg n
k : ℕ
e' : Code.evaln k cf n = Option.none
e : Code.evaln k cg n = Option.some x
⊢ x ∈ cf.eval n ∨ x ∈ cg.eval n

Tactic:
exact Or.inr (Code.evaln_sound e)

Result:
no goals

Proof state:
cf : Code
hf : Partrec cf.eval
cg : Code
hg : Partrec cg.eval
this✝ : Partrec fun n => rfindOpt fun k => Code.evaln k cf n <|> Code.evaln k cg n
n : ℕ
this : ∀ x ∈ rfindOpt fun k => Code.evaln k cf n <|> Code.evaln k cg n, x ∈ cf.eval n ∨ x ∈ cg.eval n
x k : ℕ
e : Code.evaln k cg n = Option.some x
y : ℕ
⊢ y ∈ (Option.some y <|> Code.evaln k cg n)

Tactic:
simp only [Option.some_orElse, Option.mem_def]

Result:
no goals

Proof state:
case intro.intro
cf : Code
hf : Partrec cf.eval
cg : Code
hg : Partrec cg.eval
this✝ : Partrec fun n => rfindOpt fun k => Code.evaln k cf n <|> Code.evaln k cg n
n : ℕ
this : ∀ x ∈ rfindOpt fun k => Code.evaln k cf n <|> Code.evaln k cg n, x ∈ cf.eval n ∨ x ∈ cg.eval n
h : (∃ y k, Code.evaln k cf n = Option.some y) ∨ ∃ y k, Code.evaln k cg n = Option.some y
⊢ ∃ n_1 a, a ∈ (Code.evaln n_1 cf n <|> Code.evaln n_1 cg n)

Tactic:
obtain ⟨x, k, e⟩ | ⟨x, k, e⟩ := h

Result:
case intro.intro.inl.intro.intro
cf : Code
hf : Partrec cf.eval
cg : Code
hg : Partrec cg.eval
this✝ : Partrec fun n => rfindOpt fun k => Code.evaln k cf n <|> Code.evaln k cg n
n : ℕ
this : ∀ x ∈ rfindOpt fun k => Code.evaln k cf n <|> Code.evaln k cg n, x ∈ cf.eval n ∨ x ∈ cg.eval n
x k : ℕ
e : Code.evaln k cf n = Option.some x
⊢ ∃ n_1 a, a ∈ (Code.evaln n_1 cf n <|> Code.evaln n_1 cg n)

case intro.intro.inr.intro.intro
cf : Code
hf : Partrec cf.eval
cg : Code
hg : Partrec cg.eval
this✝ : Partrec fun n => rfindOpt fun k => Code.evaln k cf n <|> Code.evaln k cg n
n : ℕ
this : ∀ x ∈ rfindOpt fun k => Code.evaln k cf n <|> Code.evaln k cg n, x ∈ cf.eval n ∨ x ∈ cg.eval n
x k : ℕ
e : Code.evaln k cg n = Option.some x
⊢ ∃ n_1 a, a ∈ (Code.evaln n_1 cf n <|> Code.evaln n_1 cg n)

Proof state:
cf : Code
hf : Partrec cf.eval
cg : Code
hg : Partrec cg.eval
this : Partrec fun n => rfindOpt fun k => Code.evaln k cf n <|> Code.evaln k cg n
n : ℕ
⊢ ∀ x ∈ rfindOpt fun k => Code.evaln k cf n <|> Code.evaln k cg n, x ∈ cf.eval n ∨ x ∈ cg.eval n

Tactic:
intro x h

Result:
cf : Code
hf : Partrec cf.eval
cg : Code
hg : Partrec cg.eval
this : Partrec fun n => rfindOpt fun k => Code.evaln k cf n <|> Code.evaln k cg n
n x : ℕ
h : x ∈ rfindOpt fun k => Code.evaln k cf n <|> Code.evaln k cg n
⊢ x ∈ cf.eval n ∨ x ∈ cg.eval n

Proof state:
case intro.intro.inr.intro.intro
cf : Code
hf : Partrec cf.eval
cg : Code
hg : Partrec cg.eval
this✝ : Partrec fun n => rfindOpt fun k => Code.evaln k cf n <|> Code.evaln k cg n
n : ℕ
this : ∀ x ∈ rfindOpt fun k => Code.evaln k cf n <|> Code.evaln k cg n, x ∈ cf.eval n ∨ x ∈ cg.eval n
x k : ℕ
e : Code.evaln k cg n = Option.some x
⊢ ∃ n_1 a, a ∈ (Code.evaln n_1 cf n <|> Code.evaln n_1 cg n)

Tactic:
refine ⟨k, ?_⟩

Result:
case intro.intro.inr.intro.intro
cf : Code
hf : Partrec cf.eval
cg : Code
hg : Partrec cg.eval
this✝ : Partrec fun n => rfindOpt fun k => Code.evaln k cf n <|> Code.evaln k cg n
n : ℕ
this : ∀ x ∈ rfindOpt fun k => Code.evaln k cf n <|> Code.evaln k cg n, x ∈ cf.eval n ∨ x ∈ cg.eval n
x k : ℕ
e : Code.evaln k cg n = Option.some x
⊢ ∃ a, a ∈ (Code.evaln k cf n <|> Code.evaln k cg n)