-- Module: Mathlib.Computability.PartrecCode
Goal:
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 n₁ n₂ : ℕ
prec :
  ∀ {n x : ℕ}
    (h :
      Membership.mem (γ := Part ℕ)
        (Nat.rec (motive := fun (x : ℕ) ↦ Part ℕ) (cf.eval n₁)
            (fun (y : ℕ) (IH : Part ℕ) ↦ IH.bind fun (i : ℕ) ↦ cg.eval (Nat.pair n₁ (Nat.pair y i))) 0 :
          Part ℕ)
        x),
    ∃ (k : ℕ),
      n ≤ k ∧
        Nat.rec (motive := fun (x : ℕ) ↦ Option ℕ) (evaln (k + 1) cf n₁)
            (fun (n : ℕ) (n_ih : Option ℕ) ↦
              (evaln k (cf.prec cg) (Nat.pair n₁ n)).bind fun (i : ℕ) ↦ evaln (k + 1) cg (Nat.pair n₁ (Nat.pair n i)))
            0 =
          some x
prec₁ : ∀ {n x : ℕ} (h : x ∈ cf.eval n₁), ∃ (k : ℕ), n ≤ k ∧ evaln (k + 1) cf n₁ = some x
prec₂ :
  ∀ (m : ℕ)
    (IH :
      ∀ {n x : ℕ}
        (h :
          Membership.mem (γ := Part ℕ)
            (Nat.rec (motive := fun (x : ℕ) ↦ Part ℕ) (cf.eval n₁)
                (fun (y : ℕ) (IH : Part ℕ) ↦ IH.bind fun (i : ℕ) ↦ cg.eval (Nat.pair n₁ (Nat.pair y i))) m :
              Part ℕ)
            x),
        ∃ (k : ℕ),
          n ≤ k ∧
            Nat.rec (motive := fun (x : ℕ) ↦ Option ℕ) (evaln (k + 1) cf n₁)
                (fun (n : ℕ) (n_ih : Option ℕ) ↦
                  (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 : ℕ}
    (h :
      Membership.mem (γ := Part ℕ)
        (Nat.rec (motive := fun (x : ℕ) ↦ Part ℕ) (cf.eval n₁)
            (fun (y : ℕ) (IH : Part ℕ) ↦ IH.bind fun (i : ℕ) ↦ cg.eval (Nat.pair n₁ (Nat.pair y i))) (m + 1) :
          Part ℕ)
        x),
    ∃ (k : ℕ),
      n ≤ k ∧
        Nat.rec (motive := fun (x : ℕ) ↦ Option ℕ) (evaln (k + 1) cf n₁)
            (fun (n : ℕ) (n_ih : Option ℕ) ↦
              (evaln k (cf.prec cg) (Nat.pair n₁ n)).bind fun (i : ℕ) ↦ evaln (k + 1) cg (Nat.pair n₁ (Nat.pair n i)))
            (m + 1) =
          some x
prec₃ :
  ∀ (m : ℕ)
    (IH :
      ∀ {n x : ℕ}
        (h :
          Membership.mem (γ := Part ℕ)
            (Nat.rec (motive := fun (x : ℕ) ↦ Part ℕ) (cf.eval n₁)
                (fun (y : ℕ) (IH : Part ℕ) ↦ IH.bind fun (i : ℕ) ↦ cg.eval (Nat.pair n₁ (Nat.pair y i))) m :
              Part ℕ)
            x),
        ∃ (k : ℕ),
          n ≤ k ∧
            Nat.rec (motive := fun (x : ℕ) ↦ Option ℕ) (evaln (k + 1) cf n₁)
                (fun (n : ℕ) (n_ih : Option ℕ) ↦
                  (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 : ℕ),
    Membership.mem (γ := Part ℕ)
        (Nat.rec (motive := fun (x : ℕ) ↦ Part ℕ) (cf.eval n₁)
            (fun (y : ℕ) (IH : Part ℕ) ↦ IH.bind fun (i : ℕ) ↦ cg.eval (Nat.pair n₁ (Nat.pair y i))) m :
          Part ℕ)
        x_1 →
      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
⊢ ∀
    (h :
      Membership.mem (γ := Part ℕ)
        (Nat.rec (motive := fun (x : ℕ) ↦ Part ℕ) (cf.eval n₁)
            (fun (y : ℕ) (IH : Part ℕ) ↦ IH.bind fun (i : ℕ) ↦ cg.eval (Nat.pair n₁ (Nat.pair y i))) n₂ :
          Part ℕ)
        x),
    ∃ (k : ℕ),
      n ≤ k ∧
        Nat.rec (motive := fun (x : ℕ) ↦ Option ℕ) (evaln (k + 1) cf n₁)
            (fun (n : ℕ) (n_ih : Option ℕ) ↦
              (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

Tactic:
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₁⟩

Premises used: Nat.Partrec.Code.evaln.eq_8, exists_and_left, Nat.Partrec.Code.succ, Option.guard_eq_some', Nat.unpaired, exists_const, Nat.Partrec.Code.zero, Bind.bind, Option.bind_eq_some_iff, Nat.unpair_pair, Option.mem_def