-- 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 :
  x ∈
    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
⊢ x ∈
    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

Tactic:
simp? [Bind.bind, Option.bind_eq_some] at h ⊢ says
  simp only [unpaired, bind, pair_unpair, Option.pure_def, Option.mem_def,
    Option.bind_eq_some] at h ⊢

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
⊢ ∃ 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

Proof state:
case pair
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)
        Nat.pair <$> evaln (k + 1) cf n <*> evaln (k + 1) cg n)
      n =
    some x
h : ∃ a, evaln (k + 1) cf n = some a ∧ ∃ a_1, evaln (k + 1) cg n = some a_1 ∧ Nat.pair a a_1 = x
⊢ ∃ a, evaln (k₂ + 1) cf n = some a ∧ ∃ a_1, evaln (k₂ + 1) cg n = some a_1 ∧ Nat.pair a a_1 = x

Tactic:
exact h.imp fun a => And.imp (hf _ _) <| Exists.imp fun b => And.imp_left (hg _ _)

Result:
no goals

Proof state:
case pair
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)
        Nat.pair <$> evaln (k + 1) cf n <*> evaln (k + 1) cg n)
      n =
    some x
h : x ∈ Nat.pair <$> evaln (k + 1) cf n <*> evaln (k + 1) cg n
⊢ x ∈ Nat.pair <$> evaln (k₂ + 1) cf n <*> evaln (k₂ + 1) cg n

Tactic:
simp? [Seq.seq, Option.bind_eq_some] at h ⊢ says
  simp only [Seq.seq, Option.map_eq_map, Option.mem_def, Option.bind_eq_some,
    Option.map_eq_some', exists_exists_and_eq_and] at h ⊢

Result:
case pair
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)
        Nat.pair <$> evaln (k + 1) cf n <*> evaln (k + 1) cg n)
      n =
    some x
h : ∃ a, evaln (k + 1) cf n = some a ∧ ∃ a_1, evaln (k + 1) cg n = some a_1 ∧ Nat.pair a a_1 = x
⊢ ∃ a, evaln (k₂ + 1) cf n = some a ∧ ∃ a_1, evaln (k₂ + 1) cg n = some a_1 ∧ Nat.pair a a_1 = x

Proof state:
case comp
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)
        let x ← evaln (k + 1) cg n
        evaln (k + 1) cf x)
      n =
    some x
h : ∃ a, evaln (k + 1) cg n = some a ∧ evaln (k + 1) cf a = some x
⊢ ∃ a, evaln (k₂ + 1) cg n = some a ∧ evaln (k₂ + 1) cf a = some x

Tactic:
exact h.imp fun a => And.imp (hg _ _) (hf _ _)

Result:
no goals

Proof state:
k k₂ : ℕ
c : Code
n x : ℕ
hl : k + 1 ≤ k₂ + 1
h : x ∈ evaln (k + 1) c n
⊢ x ∈ evaln (k₂ + 1) c n

Tactic:
have hl' := Nat.le_of_succ_le_succ hl

Result:
k k₂ : ℕ
c : Code
n x : ℕ
hl : k + 1 ≤ k₂ + 1
h : x ∈ evaln (k + 1) c n
hl' : k ≤ k₂
⊢ x ∈ evaln (k₂ + 1) c n