-- Lean 4 proof step from Mathlib.Computability.PartrecCode (goal)
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
⊢ ∀
    (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
have 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
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₁⟩
Cleared hypotheses: n, x, n₂