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

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

Tactic:
suffices ∃ k, y + n.unpair.2 ∈ evaln (k + 1) (rfind' cf) (Nat.pair n.unpair.1 n.unpair.2) by
  simpa [evaln, Option.bind_eq_some]

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

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

Tactic:
revert hy₁ hy₂

Result:
case rfind'.intro.intro.intro
cf : Code
hf : ∀ {n x : ℕ}, x ∈ cf.eval n → ∃ k, x ∈ evaln (k + 1) cf n
n y : ℕ
⊢ 0 ∈ cf.eval (Nat.pair (unpair n).1 (y + (unpair n).2)) →
    (∀ {m : ℕ}, m < y → ∃ a ∈ cf.eval (Nat.pair (unpair n).1 (m + (unpair n).2)), ¬a = 0) →
      ∃ k, y + (unpair n).2 ∈ evaln (k + 1) cf.rfind' (Nat.pair (unpair n).1 (unpair n).2)

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 : ℕ
h :
  x ∈
    Nat.rec (cf.eval (unpair n).1) (fun y IH => IH.bind fun i => cg.eval (Nat.pair (unpair n).1 (Nat.pair y i)))
      (unpair n).2
⊢ ∃ k,
    n ≤ k ∧
      Nat.rec (evaln (k + 1) cf (unpair n).1)
          (fun n_1 n_ih =>
            (evaln k (cf.prec cg) (Nat.pair (unpair n).1 n_1)).bind fun i =>
              evaln (k + 1) cg (Nat.pair (unpair n).1 (Nat.pair n_1 i)))
          (unpair n).2 =
        some x

Tactic:
revert h

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 : ℕ
⊢ x ∈
      Nat.rec (cf.eval (unpair n).1) (fun y IH => IH.bind fun i => cg.eval (Nat.pair (unpair n).1 (Nat.pair y i)))
        (unpair n).2 →
    ∃ k,
      n ≤ k ∧
        Nat.rec (evaln (k + 1) cf (unpair n).1)
            (fun n_1 n_ih =>
              (evaln k (cf.prec cg) (Nat.pair (unpair n).1 n_1)).bind fun i =>
                evaln (k + 1) cg (Nat.pair (unpair n).1 (Nat.pair n_1 i)))
            (unpair n).2 =
          some x

Proof state:
case comp
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 ∈ cg.eval n, x ∈ cf.eval a
⊢ ∃ k, n ≤ k ∧ ∃ a, evaln (k + 1) cg n = some a ∧ evaln (k + 1) cf a = some x

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

Result:
case comp.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, n ≤ k ∧ ∃ a, evaln (k + 1) cg n = some a ∧ evaln (k + 1) cf 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₁ : 0 ∈ cf.eval (Nat.pair (unpair n).1 (0 + m))
hy₂ : ∀ {m_1 : ℕ}, m_1 < 0 → ∃ a ∈ cf.eval (Nat.pair (unpair n).1 (m_1 + m)), ¬a = 0
⊢ ∃ 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:
simp at hy₁

Result:
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)

Proof state:
case h
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 m)
k₂ : ℕ
hk₂ : y + m.succ ∈ evaln (k₂ + 1) cf.rfind' (Nat.pair (unpair n).1 m.succ)
⊢ Nat.pair (unpair n).1 m ≤ (k₁ ⊔ k₂).succ ∧
    ∃ a,
      evaln ((k₁ ⊔ k₂).succ + 1) cf (Nat.pair (unpair n).1 m) = some a ∧
        (if a = 0 then some m else evaln (k₁ ⊔ k₂).succ cf.rfind' (Nat.pair (unpair n).1 (m + 1))) = some (y + 1 + m)

Tactic:
use Nat.le_succ_of_le <| le_max_of_le_left <| Nat.le_of_lt_succ <| evaln_bound hk₁

Result:
case right
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 m)
k₂ : ℕ
hk₂ : y + m.succ ∈ evaln (k₂ + 1) cf.rfind' (Nat.pair (unpair n).1 m.succ)
⊢ ∃ a,
    evaln ((k₁ ⊔ k₂).succ + 1) cf (Nat.pair (unpair n).1 m) = some a ∧
      (if a = 0 then some m else evaln (k₁ ⊔ k₂).succ cf.rfind' (Nat.pair (unpair n).1 (m + 1))) = some (y + 1 + m)