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

Proof state:
case right
n x : ℕ
h : x = (unpair n).2
⊢ (∃ x, n ≤ x) ∧ (unpair n).2 = x

Tactic:
exact ⟨⟨_, le_rfl⟩, h.symm⟩

Result:
no goals

Proof state:
case prec.succ
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 : ℕ
⊢ ∀ x_1 ∈ Nat.rec (cf.eval n₁) (fun y IH => IH.bind fun i => cg.eval (Nat.pair n₁ (Nat.pair y i))) m,
    x ∈ cg.eval (Nat.pair n₁ (Nat.pair m x_1)) →
      ∃ 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:
intro y hy hx

Result:
case prec.succ
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,
    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 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

Tactic:
refine ⟨max k₁ k₂, ?_⟩

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
⊢ n ≤ k₁ ⊔ k₂ ∧ ∃ a, evaln (k₁ ⊔ k₂ + 1) cg n = some a ∧ evaln (k₁ ⊔ k₂ + 1) cf a = some x

Proof state:
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
this : ∃ k, y + (unpair n).2 ∈ evaln (k + 1) cf.rfind' (Nat.pair (unpair n).1 (unpair n).2)
⊢ ∃ 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:
simpa [evaln, Option.bind_eq_some]

Result:
no goals

Proof state:
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))
⊢ 0 ∈ cf.eval (Nat.pair (unpair n).1 (y + m.succ))

Tactic:
simpa [Nat.succ_eq_add_one, add_comm, add_left_comm] using hy₁

Result:
no goals

Proof state:
case rfind'.intro.intro.intro.succ.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,
    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 hf ha with ⟨k₁, hk₁⟩

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

Proof state:
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₁ : n ⊔ Nat.pair n₁ m ≤ 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))
⊢ Nat.pair n₁ m ≤ k₁ ∧
    Nat.rec (evaln (k₁ + 1) cf n₁)
        (fun n n_ih =>
          (evaln k₁ (cf.prec cg) (Nat.pair n₁ n)).bind fun a => evaln (k₁ + 1) cg (Nat.pair n₁ (Nat.pair n a)))
        m =
      some y

Tactic:
exact ⟨le_trans (le_max_right _ _) nk₁, hk₁⟩

Result:
no goals