-- Mathlib/Computability/PartrecCode.lean
theorem evaln_mono : ∀ {k₁ k₂ c n x}, k₁ ≤ k₂ → x ∈ evaln k₁ c n → x ∈ evaln k₂ c n
  | 0, k₂, c, n, x, _, h => by simp [evaln] at h
  | k + 1, k₂ + 1, c, n, x, hl, h => by
    have hl' := Nat.le_of_succ_le_succ hl
    have :
      ∀ {k k₂ n x : ℕ} {o₁ o₂ : Option ℕ},
        k ≤ k₂ → (x ∈ o₁ → x ∈ o₂) →
          x ∈ do { guard (n ≤ k); o₁ } → x ∈ do { guard (n ≤ k₂); o₂ }

Proof state:
case rfind'
k k₂ : ℕ
hl : k + 1 ≤ k₂ + 1
hl' : k ≤ k₂
this :
  ∀ {k k₂ n x : ℕ} {o₁ o₂ : Option ℕ},
    k ≤ k₂ →
      (x ∈ o₁ → x ∈ o₂) →
        (x ∈ do
            guard (n ≤ k)
            o₁) →
          x ∈ do
            guard (n ≤ k₂)
            o₂
cf : Code
hf : ∀ (n x : ℕ), evaln (k + 1) cf n = some x → evaln (k₂ + 1) cf n = some x
n x : ℕ
h✝ :
  (fun n => do
        guard (n ≤ k)
        unpaired
            (fun a m => do
              let x ← evaln (k + 1) cf (Nat.pair a m)
              if x = 0 then pure m else evaln k cf.rfind' (Nat.pair a (m + 1)))
            n)
      n =
    some x
h :
  ∃ 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
⊢ ∃ 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

Tactic:
refine h.imp fun x => And.imp (hf _ _) ?_

Result:
case rfind'
k k₂ : ℕ
hl : k + 1 ≤ k₂ + 1
hl' : k ≤ k₂
this :
  ∀ {k k₂ n x : ℕ} {o₁ o₂ : Option ℕ},
    k ≤ k₂ →
      (x ∈ o₁ → x ∈ o₂) →
        (x ∈ do
            guard (n ≤ k)
            o₁) →
          x ∈ do
            guard (n ≤ k₂)
            o₂
cf : Code
hf : ∀ (n x : ℕ), evaln (k + 1) cf n = some x → evaln (k₂ + 1) cf n = some x
n x✝ : ℕ
h✝ :
  (fun n => do
        guard (n ≤ k)
        unpaired
            (fun a m => do
              let x ← evaln (k + 1) cf (Nat.pair a m)
              if x = 0 then pure m else evaln k cf.rfind' (Nat.pair a (m + 1)))
            n)
      n =
    some x✝
h :
  ∃ 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✝
x : ℕ
⊢ (if x = 0 then some (unpair n).2 else evaln k cf.rfind' (Nat.pair (unpair n).1 ((unpair n).2 + 1))) = some x✝ →
    (if x = 0 then some (unpair n).2 else evaln k₂ cf.rfind' (Nat.pair (unpair n).1 ((unpair n).2 + 1))) = some x✝

Proof state:
k✝ k₂✝ : ℕ
c : Code
n✝ x✝ : ℕ
hl : k✝ + 1 ≤ k₂✝ + 1
h✝ : x✝ ∈ evaln (k✝ + 1) c n✝
hl' : k✝ ≤ k₂✝
k k₂ n x : ℕ
o₁ o₂ : Option ℕ
h : k ≤ k₂
h₁ : o₁ = some x → o₂ = some x
h₂ : n ≤ k
h₃ : o₁ = some x
⊢ n ≤ k₂ ∧ o₂ = some x

Tactic:
exact ⟨le_trans h₂ h, h₁ h₃⟩

Result:
no goals

Proof state:
case prec
k k₂ : ℕ
hl : k + 1 ≤ k₂ + 1
hl' : k ≤ k₂
this :
  ∀ {k k₂ n x : ℕ} {o₁ o₂ : Option ℕ},
    k ≤ k₂ →
      (x ∈ o₁ → x ∈ o₂) →
        (x ∈ do
            guard (n ≤ k)
            o₁) →
          x ∈ do
            guard (n ≤ k₂)
            o₂
cf cg : Code
hf : ∀ (n x : ℕ), evaln (k + 1) cf n = some x → evaln (k₂ + 1) cf n = some x
hg : ∀ (n x : ℕ), evaln (k + 1) cg n = some x → evaln (k₂ + 1) cg n = some x
n x : ℕ
h :
  (fun n => do
        guard (n ≤ k)
        unpaired
            (fun a n =>
              Nat.casesOn n (evaln (k + 1) cf a) fun y => do
                let i ← evaln k (cf.prec cg) (Nat.pair a y)
                evaln (k + 1) cg (Nat.pair a (Nat.pair y i)))
            n)
      n =
    some x
⊢ Nat.rec (evaln (k + 1) cf (unpair n).1)
        (fun n_1 n_ih =>
          (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 →
    Nat.rec (evaln (k₂ + 1) cf (unpair n).1)
        (fun n_1 n_ih =>
          (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

Tactic:
induction n.unpair.2 <;> simp [Option.bind_eq_some]

Result:
case prec.zero
k k₂ : ℕ
hl : k + 1 ≤ k₂ + 1
hl' : k ≤ k₂
this :
  ∀ {k k₂ n x : ℕ} {o₁ o₂ : Option ℕ},
    k ≤ k₂ →
      (x ∈ o₁ → x ∈ o₂) →
        (x ∈ do
            guard (n ≤ k)
            o₁) →
          x ∈ do
            guard (n ≤ k₂)
            o₂
cf cg : Code
hf : ∀ (n x : ℕ), evaln (k + 1) cf n = some x → evaln (k₂ + 1) cf n = some x
hg : ∀ (n x : ℕ), evaln (k + 1) cg n = some x → evaln (k₂ + 1) cg n = some x
n x : ℕ
h :
  (fun n => do
        guard (n ≤ k)
        unpaired
            (fun a n =>
              Nat.casesOn n (evaln (k + 1) cf a) fun y => do
                let i ← evaln k (cf.prec cg) (Nat.pair a y)
                evaln (k + 1) cg (Nat.pair a (Nat.pair y i)))
            n)
      n =
    some x
⊢ evaln (k + 1) cf (unpair n).1 = some x → evaln (k₂ + 1) cf (unpair n).1 = some x

case prec.succ
k k₂ : ℕ
hl : k + 1 ≤ k₂ + 1
hl' : k ≤ k₂
this :
  ∀ {k k₂ n x : ℕ} {o₁ o₂ : Option ℕ},
    k ≤ k₂ →
      (x ∈ o₁ → x ∈ o₂) →
        (x ∈ do
            guard (n ≤ k)
            o₁) →
          x ∈ do
            guard (n ≤ k₂)
            o₂
cf cg : Code
hf : ∀ (n x : ℕ), evaln (k + 1) cf n = some x → evaln (k₂ + 1) cf n = some x
hg : ∀ (n x : ℕ), evaln (k + 1) cg n = some x → evaln (k₂ + 1) cg n = some x
n x : ℕ
h :
  (fun n => do
        guard (n ≤ k)
        unpaired
            (fun a n =>
              Nat.casesOn n (evaln (k + 1) cf a) fun y => do
                let i ← evaln k (cf.prec cg) (Nat.pair a y)
                evaln (k + 1) cg (Nat.pair a (Nat.pair y i)))
            n)
      n =
    some x
n✝ : ℕ
a✝ :
  Nat.rec (evaln (k + 1) cf (unpair n).1)
        (fun n_1 n_ih =>
          (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)))
        n✝ =
      some x →
    Nat.rec (evaln (k₂ + 1) cf (unpair n).1)
        (fun n_1 n_ih =>
          (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)))
        n✝ =
      some x
⊢ ∀ (x_1 : ℕ),
    evaln k (cf.prec cg) (Nat.pair (unpair n).1 n✝) = some x_1 →
      evaln (k + 1) cg (Nat.pair (unpair n).1 (Nat.pair n✝ x_1)) = some x →
        ∃ a,
          evaln k₂ (cf.prec cg) (Nat.pair (unpair n).1 n✝) = some a ∧
            evaln (k₂ + 1) cg (Nat.pair (unpair n).1 (Nat.pair n✝ a)) = some x