-- Module: Mathlib.Computability.PartrecCode
Goal:
cf : Code
hf : ∀ {n x : ℕ} (h : x ∈ cf.eval n), ∃ (k : ℕ), x ∈ evaln (k + 1) cf n
n y m : ℕ
hy₁ : 0 ∈ cf.eval (Nat.pair (unpair n).1 (y + m))
hy₂ : ∀ {m_1 : ℕ}, m_1 < y → ∃ a ∈ cf.eval (Nat.pair (unpair n).1 (m_1 + m)), ¬a = 0
rfind' :
  ∀ (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 : ℕ), 0 + m ∈ evaln (k + 1) cf.rfind' (Nat.pair (unpair n).1 m)
rfind'₁ :
  ∀ (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)
rfind'₂ :
  ∀ (y : ℕ)
    (IH :
      ∀ (m : ℕ) (hy₁ : 0 ∈ cf.eval (Nat.pair (unpair n).1 (y + m)))
        (hy₂ : ∀ {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),
    ∃ (k : ℕ), y + 1 + m ∈ evaln (k + 1) cf.rfind' (Nat.pair (unpair n).1 m)
rfind'₃ :
  ∀ (y : ℕ)
    (IH :
      ∀ (m : ℕ) (hy₁ : 0 ∈ cf.eval (Nat.pair (unpair n).1 (y + m)))
        (hy₂ : ∀ {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),
    ∃ (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)
⊢ ∃ (k : ℕ), y + m ∈ evaln (k + 1) cf.rfind' (Nat.pair (unpair n).1 m)

Tactic:
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₂

Premises used: Nat.Partrec.Code.evaln, add_left_comm, Nat.Partrec.Code.succ, zero_add, add_comm, Nat.le_of_lt_succ, le_max_of_le_left, Nat.Partrec.Code.zero, Option.bind_eq_some_iff, Nat.le_succ_of_le