-- Mathlib/Computability/PartrecCode.lean
theorem evaln_complete {c n x} : x ∈ eval c n ↔ ∃ k, x ∈ evaln k c n

Proof state:
case pair
cf cg : Code
hf : ∀ {n x : ℕ}, x ∈ cf.eval n → ∃ k, x ∈ evaln (k + 1) cf n
hg : ∀ {n x : ℕ}, x ∈ cg.eval n → ∃ k, x ∈ evaln (k + 1) cg n
n x : ℕ
h : ∃ a ∈ cf.eval n, ∃ a_1 ∈ cg.eval n, Nat.pair a a_1 = x
⊢ ∃ k, n ≤ k ∧ ∃ a, evaln (k + 1) cf n = some a ∧ ∃ a_1, evaln (k + 1) cg n = some a_1 ∧ Nat.pair a a_1 = x

Tactic:
rcases h with ⟨x, hx, y, hy, rfl⟩

Result:
case pair.intro.intro.intro.intro
cf cg : Code
hf : ∀ {n x : ℕ}, x ∈ cf.eval n → ∃ k, x ∈ evaln (k + 1) cf n
hg : ∀ {n x : ℕ}, x ∈ cg.eval n → ∃ k, x ∈ evaln (k + 1) cg n
n x : ℕ
hx : x ∈ cf.eval n
y : ℕ
hy : y ∈ cg.eval n
⊢ ∃ k, n ≤ k ∧ ∃ a, evaln (k + 1) cf n = some a ∧ ∃ a_1, evaln (k + 1) cg n = some a_1 ∧ Nat.pair a a_1 = Nat.pair x y

Proof state:
case prec
cf cg : Code
hf : ∀ {n x : ℕ}, x ∈ cf.eval n → ∃ k, x ∈ evaln (k + 1) cf n
hg : ∀ {n x : ℕ}, x ∈ cg.eval n → ∃ k, x ∈ evaln (k + 1) cg n
n x n₁ : ℕ
⊢ x ∈ Nat.rec (cf.eval n₁) (fun y IH => IH.bind fun i => cg.eval (Nat.pair n₁ (Nat.pair y i))) (unpair n).2 →
    ∃ k,
      n ≤ k ∧
        Nat.rec (evaln (k + 1) cf n₁)
            (fun n n_ih =>
              (evaln k (cf.prec cg) (Nat.pair n₁ n)).bind fun i => evaln (k + 1) cg (Nat.pair n₁ (Nat.pair n i)))
            (unpair n).2 =
          some x

Tactic:
generalize n.unpair.2 = n₂

Result:
case prec
cf cg : Code
hf : ∀ {n x : ℕ}, x ∈ cf.eval n → ∃ k, x ∈ evaln (k + 1) cf n
hg : ∀ {n x : ℕ}, x ∈ cg.eval n → ∃ k, x ∈ evaln (k + 1) cg n
n x n₁ n₂ : ℕ
⊢ x ∈ Nat.rec (cf.eval n₁) (fun y IH => IH.bind fun i => cg.eval (Nat.pair n₁ (Nat.pair y i))) n₂ →
    ∃ k,
      n ≤ k ∧
        Nat.rec (evaln (k + 1) cf n₁)
            (fun n n_ih =>
              (evaln k (cf.prec cg) (Nat.pair n₁ n)).bind fun i => evaln (k + 1) cg (Nat.pair n₁ (Nat.pair n i)))
            n₂ =
          some x

Proof state:
case rfind'.intro.intro.intro.succ.intro.intro.intro
cf : Code
hf : ∀ {n x : ℕ}, x ∈ cf.eval n → ∃ k, x ∈ evaln (k + 1) cf n
n y : ℕ
IH :
  ∀ (m : ℕ),
    0 ∈ cf.eval (Nat.pair (unpair n).1 (y + m)) →
      (∀ {m_1 : ℕ}, m_1 < y → ∃ a ∈ cf.eval (Nat.pair (unpair n).1 (m_1 + m)), ¬a = 0) →
        ∃ k, y + m ∈ evaln (k + 1) cf.rfind' (Nat.pair (unpair n).1 m)
m : ℕ
hy₁ : 0 ∈ cf.eval (Nat.pair (unpair n).1 (y + 1 + m))
hy₂ : ∀ {m_1 : ℕ}, m_1 < y + 1 → ∃ a ∈ cf.eval (Nat.pair (unpair n).1 (m_1 + m)), ¬a = 0
a : ℕ
ha : a ∈ cf.eval (Nat.pair (unpair n).1 (0 + m))
a0 : ¬a = 0
k₁ : ℕ
hk₁ : a ∈ evaln (k₁ + 1) cf (Nat.pair (unpair n).1 (0 + m))
⊢ ∃ k,
    Nat.pair (unpair n).1 m ≤ k ∧
      ∃ a,
        evaln (k + 1) cf (Nat.pair (unpair n).1 m) = some a ∧
          (if a = 0 then some m else evaln k cf.rfind' (Nat.pair (unpair n).1 (m + 1))) = some (y + 1 + m)

Tactic:
rcases IH m.succ (by simpa [Nat.succ_eq_add_one, add_comm, add_left_comm] using hy₁)
    fun {i} hi => by
    simpa [Nat.succ_eq_add_one, add_comm, add_left_comm] using
      hy₂ (Nat.succ_lt_succ hi) with
  ⟨k₂, hk₂⟩

Result:
case rfind'.intro.intro.intro.succ.intro.intro.intro.intro
cf : Code
hf : ∀ {n x : ℕ}, x ∈ cf.eval n → ∃ k, x ∈ evaln (k + 1) cf n
n y : ℕ
IH :
  ∀ (m : ℕ),
    0 ∈ cf.eval (Nat.pair (unpair n).1 (y + m)) →
      (∀ {m_1 : ℕ}, m_1 < y → ∃ a ∈ cf.eval (Nat.pair (unpair n).1 (m_1 + m)), ¬a = 0) →
        ∃ k, y + m ∈ evaln (k + 1) cf.rfind' (Nat.pair (unpair n).1 m)
m : ℕ
hy₁ : 0 ∈ cf.eval (Nat.pair (unpair n).1 (y + 1 + m))
hy₂ : ∀ {m_1 : ℕ}, m_1 < y + 1 → ∃ a ∈ cf.eval (Nat.pair (unpair n).1 (m_1 + m)), ¬a = 0
a : ℕ
ha : a ∈ cf.eval (Nat.pair (unpair n).1 (0 + m))
a0 : ¬a = 0
k₁ : ℕ
hk₁ : a ∈ evaln (k₁ + 1) cf (Nat.pair (unpair n).1 (0 + m))
k₂ : ℕ
hk₂ : y + m.succ ∈ evaln (k₂ + 1) cf.rfind' (Nat.pair (unpair n).1 m.succ)
⊢ ∃ k,
    Nat.pair (unpair n).1 m ≤ k ∧
      ∃ a,
        evaln (k + 1) cf (Nat.pair (unpair n).1 m) = some a ∧
          (if a = 0 then some m else evaln k cf.rfind' (Nat.pair (unpair n).1 (m + 1))) = some (y + 1 + m)

Proof state:
case prec.succ.intro.intro
cf cg : Code
hf : ∀ {n x : ℕ}, x ∈ cf.eval n → ∃ k, x ∈ evaln (k + 1) cf n
hg : ∀ {n x : ℕ}, x ∈ cg.eval n → ∃ k, x ∈ evaln (k + 1) cg n
n₁ m : ℕ
IH :
  ∀ {n x : ℕ},
    x ∈ Nat.rec (cf.eval n₁) (fun y IH => IH.bind fun i => cg.eval (Nat.pair n₁ (Nat.pair y i))) m →
      ∃ k,
        n ≤ k ∧
          Nat.rec (evaln (k + 1) cf n₁)
              (fun n n_ih =>
                (evaln k (cf.prec cg) (Nat.pair n₁ n)).bind fun i => evaln (k + 1) cg (Nat.pair n₁ (Nat.pair n i)))
              m =
            some x
n x y : ℕ
hy : y ∈ Nat.rec (cf.eval n₁) (fun y IH => IH.bind fun i => cg.eval (Nat.pair n₁ (Nat.pair y i))) m
hx : x ∈ cg.eval (Nat.pair n₁ (Nat.pair m y))
k₁ : ℕ
nk₁ : ?m.364079 ≤ k₁
hk₁ :
  Nat.rec (evaln (k₁ + 1) cf n₁)
      (fun n n_ih =>
        (evaln k₁ (cf.prec cg) (Nat.pair n₁ n)).bind fun i => evaln (k₁ + 1) cg (Nat.pair n₁ (Nat.pair n i)))
      m =
    some y
⊢ ∃ k,
    n ≤ k ∧ ∃ a, evaln k (cf.prec cg) (Nat.pair n₁ m) = some a ∧ evaln (k + 1) cg (Nat.pair n₁ (Nat.pair m a)) = some x

Tactic:
rcases hg hx with ⟨k₂, hk₂⟩

Result:
case prec.succ.intro.intro.intro
cf cg : Code
hf : ∀ {n x : ℕ}, x ∈ cf.eval n → ∃ k, x ∈ evaln (k + 1) cf n
hg : ∀ {n x : ℕ}, x ∈ cg.eval n → ∃ k, x ∈ evaln (k + 1) cg n
n₁ m : ℕ
IH :
  ∀ {n x : ℕ},
    x ∈ Nat.rec (cf.eval n₁) (fun y IH => IH.bind fun i => cg.eval (Nat.pair n₁ (Nat.pair y i))) m →
      ∃ k,
        n ≤ k ∧
          Nat.rec (evaln (k + 1) cf n₁)
              (fun n n_ih =>
                (evaln k (cf.prec cg) (Nat.pair n₁ n)).bind fun i => evaln (k + 1) cg (Nat.pair n₁ (Nat.pair n i)))
              m =
            some x
n x y : ℕ
hy : y ∈ Nat.rec (cf.eval n₁) (fun y IH => IH.bind fun i => cg.eval (Nat.pair n₁ (Nat.pair y i))) m
hx : x ∈ cg.eval (Nat.pair n₁ (Nat.pair m y))
k₁ : ℕ
nk₁ : ?m.364079 ≤ k₁
hk₁ :
  Nat.rec (evaln (k₁ + 1) cf n₁)
      (fun n n_ih =>
        (evaln k₁ (cf.prec cg) (Nat.pair n₁ n)).bind fun i => evaln (k₁ + 1) cg (Nat.pair n₁ (Nat.pair n i)))
      m =
    some y
k₂ : ℕ
hk₂ : x ∈ evaln (k₂ + 1) cg (Nat.pair n₁ (Nat.pair m y))
⊢ ∃ k,
    n ≤ k ∧ ∃ a, evaln k (cf.prec cg) (Nat.pair n₁ m) = some a ∧ evaln (k + 1) cg (Nat.pair n₁ (Nat.pair m a)) = some x

Proof state:
case rfind'.intro.intro.intro.zero
cf : Code
hf : ∀ {n x : ℕ}, x ∈ cf.eval n → ∃ k, x ∈ evaln (k + 1) cf n
n m : ℕ
hy₂ : ∀ {m_1 : ℕ}, m_1 < 0 → ∃ a ∈ cf.eval (Nat.pair (unpair n).1 (m_1 + m)), ¬a = 0
hy₁ : 0 ∈ cf.eval (Nat.pair (unpair n).1 m)
⊢ ∃ k,
    Nat.pair (unpair n).1 m ≤ k ∧
      ∃ a,
        evaln (k + 1) cf (Nat.pair (unpair n).1 m) = some a ∧
          (¬a = 0 → evaln k cf.rfind' (Nat.pair (unpair n).1 (m + 1)) = some m)

Tactic:
rcases hf hy₁ with ⟨k, hk⟩

Result:
case rfind'.intro.intro.intro.zero.intro
cf : Code
hf : ∀ {n x : ℕ}, x ∈ cf.eval n → ∃ k, x ∈ evaln (k + 1) cf n
n m : ℕ
hy₂ : ∀ {m_1 : ℕ}, m_1 < 0 → ∃ a ∈ cf.eval (Nat.pair (unpair n).1 (m_1 + m)), ¬a = 0
hy₁ : 0 ∈ cf.eval (Nat.pair (unpair n).1 m)
k : ℕ
hk : 0 ∈ evaln (k + 1) cf (Nat.pair (unpair n).1 m)
⊢ ∃ k,
    Nat.pair (unpair n).1 m ≤ k ∧
      ∃ a,
        evaln (k + 1) cf (Nat.pair (unpair n).1 m) = some a ∧
          (¬a = 0 → evaln k cf.rfind' (Nat.pair (unpair n).1 (m + 1)) = some m)

Proof state:
case comp.intro.intro.intro
cf cg : Code
hf : ∀ {n x : ℕ}, x ∈ cf.eval n → ∃ k, x ∈ evaln (k + 1) cf n
hg : ∀ {n x : ℕ}, x ∈ cg.eval n → ∃ k, x ∈ evaln (k + 1) cg n
n x y : ℕ
hy : y ∈ cg.eval n
hx : x ∈ cf.eval y
k₁ : ℕ
hk₁ : y ∈ evaln (k₁ + 1) cg n
⊢ ∃ k, n ≤ k ∧ ∃ a, evaln (k + 1) cg n = some a ∧ evaln (k + 1) cf a = some x

Tactic:
rcases hf hx with ⟨k₂, hk₂⟩

Result:
case comp.intro.intro.intro.intro
cf cg : Code
hf : ∀ {n x : ℕ}, x ∈ cf.eval n → ∃ k, x ∈ evaln (k + 1) cf n
hg : ∀ {n x : ℕ}, x ∈ cg.eval n → ∃ k, x ∈ evaln (k + 1) cg n
n x y : ℕ
hy : y ∈ cg.eval n
hx : x ∈ cf.eval y
k₁ : ℕ
hk₁ : y ∈ evaln (k₁ + 1) cg n
k₂ : ℕ
hk₂ : x ∈ evaln (k₂ + 1) cf y
⊢ ∃ k, n ≤ k ∧ ∃ a, evaln (k + 1) cg n = some a ∧ evaln (k + 1) cf a = some x