-- Module: Mathlib.Computability.PartrecCode
Goal:
c : Code
n x : ℕ
h : x ∈ c.eval n
pair :
  ∀ (cf cg : Code) (hf : ∀ {n x : ℕ} (h : x ∈ cf.eval n), ∃ (k : ℕ), x ∈ evaln (k + 1) cf n)
    (hg : ∀ {n x : ℕ} (h : x ∈ cg.eval n), ∃ (k : ℕ), x ∈ evaln (k + 1) cg n) {n x : ℕ} (h : x ∈ (cf.pair cg).eval n),
    ∃ (k : ℕ), x ∈ evaln (k + 1) (cf.pair cg) n
pair₁ :
  ∀ (cf cg : Code) (hf : ∀ {n x : ℕ} (h : x ∈ cf.eval n), ∃ (k : ℕ), x ∈ evaln (k + 1) cf n)
    (hg : ∀ {n x : ℕ} (h : 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
comp :
  ∀ (cf cg : Code) (hf : ∀ {n x : ℕ} (h : x ∈ cf.eval n), ∃ (k : ℕ), x ∈ evaln (k + 1) cf n)
    (hg : ∀ {n x : ℕ} (h : x ∈ cg.eval n), ∃ (k : ℕ), x ∈ evaln (k + 1) cg n) {n x : ℕ} (h : x ∈ (cf.comp cg).eval n),
    ∃ (k : ℕ), x ∈ evaln (k + 1) (cf.comp cg) n
comp₁ :
  ∀ (cf cg : Code) (hf : ∀ {n x : ℕ} (h : x ∈ cf.eval n), ∃ (k : ℕ), x ∈ evaln (k + 1) cf n)
    (hg : ∀ {n x : ℕ} (h : 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
prec :
  ∀ (cf cg : Code) (hf : ∀ {n x : ℕ} (h : x ∈ cf.eval n), ∃ (k : ℕ), x ∈ evaln (k + 1) cf n)
    (hg : ∀ {n x : ℕ} (h : x ∈ cg.eval n), ∃ (k : ℕ), x ∈ evaln (k + 1) cg n) {n x : ℕ} (h : x ∈ (cf.prec cg).eval n),
    ∃ (k : ℕ), x ∈ evaln (k + 1) (cf.prec cg) n
prec₁ :
  ∀ (cf cg : Code) (hf : ∀ {n x : ℕ} (h : x ∈ cf.eval n), ∃ (k : ℕ), x ∈ evaln (k + 1) cf n)
    (hg : ∀ {n x : ℕ} (h : x ∈ cg.eval n), ∃ (k : ℕ), x ∈ evaln (k + 1) cg n) {n x : ℕ}
    (h :
      Membership.mem (γ := Part ℕ)
        (Nat.rec (motive := fun (x : ℕ) ↦ Part ℕ) (cf.eval (unpair n).1)
            (fun (y : ℕ) (IH : Part ℕ) ↦ IH.bind fun (i : ℕ) ↦ cg.eval (Nat.pair (unpair n).1 (Nat.pair y i)))
            (unpair n).2 :
          Part ℕ)
        x),
    ∃ (k : ℕ),
      n ≤ k ∧
        Nat.rec (motive := fun (x : ℕ) ↦ Option ℕ) (evaln (k + 1) cf (unpair n).1)
            (fun (n_1 : ℕ) (n_ih : Option ℕ) ↦
              (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
rfind' :
  ∀ (cf : Code) (hf : ∀ {n x : ℕ} (h : x ∈ cf.eval n), ∃ (k : ℕ), x ∈ evaln (k + 1) cf n) {n x : ℕ}
    (h : x ∈ cf.rfind'.eval n), ∃ (k : ℕ), x ∈ evaln (k + 1) cf.rfind' n
rfind'₁ :
  ∀ (cf : Code) (hf : ∀ {n x : ℕ} (h : x ∈ cf.eval n), ∃ (k : ℕ), x ∈ evaln (k + 1) cf n) {n x : ℕ}
    (h :
      ∃ (a : ℕ),
        (0 ∈ cf.eval (Nat.pair (unpair n).1 (a + (unpair n).2)) ∧
            ∀ {m : ℕ}, m < a → ∃ a ∈ cf.eval (Nat.pair (unpair n).1 (m + (unpair n).2)), ¬a = 0) ∧
          a + (unpair n).2 = x),
    ∃ (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 x
zero : ∀ {n x : ℕ} (h : x ∈ Code.zero.eval n), ∃ (k : ℕ), x ∈ evaln (k + 1) Code.zero n
zero₁ : ∀ {n x : ℕ} (h : x = 0), (∃ (x : ℕ), n ≤ x) ∧ 0 = x
succ : ∀ {n x : ℕ} (h : x ∈ Code.succ.eval n), ∃ (k : ℕ), x ∈ evaln (k + 1) Code.succ n
succ₁ : ∀ {n x : ℕ} (h : x = n + 1), (∃ (x : ℕ), n ≤ x) ∧ n + 1 = x
left : ∀ {n x : ℕ} (h : x ∈ Code.left.eval n), ∃ (k : ℕ), x ∈ evaln (k + 1) Code.left n
left₁ : ∀ {n x : ℕ} (h : x = (unpair n).1), (∃ (x : ℕ), n ≤ x) ∧ (unpair n).1 = x
right : ∀ {n x : ℕ} (h : x ∈ Code.right.eval n), ∃ (k : ℕ), x ∈ evaln (k + 1) Code.right n
right₁ : ∀ {n x : ℕ} (h : x = (unpair n).2), (∃ (x : ℕ), n ≤ x) ∧ (unpair n).2 = x
⊢ ∃ (k : ℕ), x ∈ evaln (k + 1) c n

Tactic:
induction c generalizing n x with
      simp [eval, evaln, pure, PFun.pure, Seq.seq, Option.bind_eq_some_iff] at h ⊢
  | pair cf cg hf hg =>
    rcases h with ⟨x, hx, y, hy, rfl⟩
    rcases hf hx with ⟨k₁, hk₁⟩; rcases hg hy with ⟨k₂, hk₂⟩
    refine ⟨max k₁ k₂, ?_⟩
    refine
      ⟨le_max_of_le_left <| Nat.le_of_lt_succ <| evaln_bound hk₁, _,
        evaln_mono (Nat.succ_le_succ <| le_max_left _ _) hk₁, _,
        evaln_mono (Nat.succ_le_succ <| le_max_right _ _) hk₂, rfl⟩
  | comp cf cg hf hg =>
    rcases h with ⟨y, hy, hx⟩
    rcases hg hy with ⟨k₁, hk₁⟩; rcases hf hx with ⟨k₂, hk₂⟩
    refine ⟨max k₁ k₂, ?_⟩
    exact
      ⟨le_max_of_le_left <| Nat.le_of_lt_succ <| evaln_bound hk₁, _,
        evaln_mono (Nat.succ_le_succ <| le_max_left _ _) hk₁,
        evaln_mono (Nat.succ_le_succ <| le_max_right _ _) hk₂⟩
  | prec cf cg hf hg =>
    revert h
    generalize n.unpair.1 = n₁; generalize n.unpair.2 = n₂
    induction n₂ generalizing x n with simp [Option.bind_eq_some_iff]
    | zero =>
      intro h
      rcases hf h with ⟨k, hk⟩
      exact ⟨_, le_max_left _ _, evaln_mono (Nat.succ_le_succ <| le_max_right _ _) hk⟩
    | succ m IH =>
      intro y hy hx
      rcases IH hy with ⟨k₁, nk₁, hk₁⟩
      rcases hg hx with ⟨k₂, hk₂⟩
      refine
        ⟨(max k₁ k₂).succ,
          Nat.le_succ_of_le <| le_max_of_le_left <|
            le_trans (le_max_left _ (Nat.pair n₁ m)) nk₁, y,
          evaln_mono (Nat.succ_le_succ <| le_max_left _ _) ?_,
          evaln_mono (Nat.succ_le_succ <| Nat.le_succ_of_le <| le_max_right _ _) hk₂⟩
      simp only [evaln.eq_8, bind, unpaired, unpair_pair, Option.mem_def, Option.bind_eq_some_iff,
        Option.guard_eq_some', exists_and_left, exists_const]
      exact ⟨le_trans (le_max_right _ _) nk₁, hk₁⟩
  | rfind' cf hf =>
    rcases h with ⟨y, ⟨hy₁, hy₂⟩, rfl⟩
    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_iff]
    revert hy₁ hy₂
    generalize n.unpair.2 = m
    intro hy₁ hy₂
    induction y generalizing m with simp [evaln, Option.bind_eq_some_iff]
    | zero =>
      simp at hy₁
      rcases hf hy₁ with ⟨k, hk⟩
      exact ⟨_, Nat.le_of_lt_succ <| evaln_bound hk, _, hk, by simp⟩
    | succ y IH =>
      rcases hy₂ (Nat.succ_pos _) with ⟨a, ha, a0⟩
      rcases hf ha with ⟨k₁, hk₁⟩
      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₂⟩
      use (max k₁ k₂).succ
      rw [zero_add] at hk₁
      use Nat.le_succ_of_le <| le_max_of_le_left <| Nat.le_of_lt_succ <| evaln_bound hk₁
      use a
      use evaln_mono (Nat.succ_le_succ <| Nat.le_succ_of_le <| le_max_left _ _) hk₁
      simpa [a0, add_comm, add_left_comm] using
        evaln_mono (Nat.succ_le_succ <| le_max_right _ _) hk₂
  | _ => exact ⟨⟨_, le_rfl⟩, h.symm⟩

Premises used: Pure.pure, Nat.Partrec.Code.evaln.eq_8, Nat.Partrec.Code.evaln, Nat.Partrec.Code.rfind', add_left_comm, Nat.unpair, exists_and_left, Nat.Partrec.Code.prec, Nat.Partrec.Code.succ, Seq.seq, zero_add, add_comm, Prod.fst, Option.guard_eq_some', Nat.Partrec.Code.comp, Nat.le_of_lt_succ, le_max_of_le_left, Nat.unpaired, exists_const, Nat.Partrec.Code.zero, PFun.pure, Nat.Partrec.Code.eval, Bind.bind, Option.bind_eq_some_iff, Nat.Partrec.Code.pair, Nat.le_succ_of_le, Nat.unpair_pair, Prod.snd, rfl, Option.mem_def