Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: k k₂ : ℕ
c : Code
n x : ℕ
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₂
h : evaln (k + 1) c n = some x
⊢ evaln (k₂ + 1) c n = some x

Tactic:
induction c generalizing x n <;> rw [evaln] at h ⊢

Goal state after:
case 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₂
n x : ℕ
h :
  (fun n ↦ do
        guard (n ≤ k)
        pure 0)
      n =
    some x
⊢ (fun n ↦ do
        guard (n ≤ k₂)
        pure 0)
      n =
    some x

case 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₂
n x : ℕ
h :
  (fun n ↦ do
        guard (n ≤ k)
        pure n.succ)
      n =
    some x
⊢ (fun n ↦ do
        guard (n ≤ k₂)
        pure n.succ)
      n =
    some x

case left
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₂
n x : ℕ
h :
  (fun n ↦ do
        guard (n ≤ k)
        pure (unpair n).1)
      n =
    some x
⊢ (fun n ↦ do
        guard (n ≤ k₂)
        pure (unpair n).1)
      n =
    some x

case right
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₂
n x : ℕ
h :
  (fun n ↦ do
        guard (n ≤ k)
        pure (unpair n).2)
      n =
    some x
⊢ (fun n ↦ do
        guard (n ≤ k₂)
        pure (unpair n).2)
      n =
    some x

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₂
a✝¹ a✝ : Code
a_ih✝¹ : ∀ (n x : ℕ), evaln (k + 1) a✝¹ n = some x → evaln (k₂ + 1) a✝¹ n = some x
a_ih✝ : ∀ (n x : ℕ), evaln (k + 1) a✝ n = some x → evaln (k₂ + 1) a✝ n = some x
n x : ℕ
h :
  (fun n ↦ do
        guard (n ≤ k)
        Nat.pair <$> evaln (k + 1) a✝¹ n <*> evaln (k + 1) a✝ n)
      n =
    some x
⊢ (fun n ↦ do
        guard (n ≤ k₂)
        Nat.pair <$> evaln (k₂ + 1) a✝¹ n <*> evaln (k₂ + 1) a✝ n)
      n =
    some x

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₂
a✝¹ a✝ : Code
a_ih✝¹ : ∀ (n x : ℕ), evaln (k + 1) a✝¹ n = some x → evaln (k₂ + 1) a✝¹ n = some x
a_ih✝ : ∀ (n x : ℕ), evaln (k + 1) a✝ n = some x → evaln (k₂ + 1) a✝ n = some x
n x : ℕ
h :
  (fun n ↦ do
        guard (n ≤ k)
        let x ← evaln (k + 1) a✝ n
        evaln (k + 1) a✝¹ x)
      n =
    some x
⊢ (fun n ↦ do
        guard (n ≤ k₂)
        let x ← evaln (k₂ + 1) a✝ n
        evaln (k₂ + 1) a✝¹ x)
      n =
    some x

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₂
a✝¹ a✝ : Code
a_ih✝¹ : ∀ (n x : ℕ), evaln (k + 1) a✝¹ n = some x → evaln (k₂ + 1) a✝¹ n = some x
a_ih✝ : ∀ (n x : ℕ), evaln (k + 1) a✝ n = some x → evaln (k₂ + 1) a✝ n = some x
n x : ℕ
h :
  (fun n ↦ do
        guard (n ≤ k)
        unpaired
            (fun a n ↦
              Nat.casesOn n (evaln (k + 1) a✝¹ a) fun y ↦ do
                let i ← evaln k (a✝¹.prec a✝) (Nat.pair a y)
                evaln (k + 1) a✝ (Nat.pair a (Nat.pair y i)))
            n)
      n =
    some x
⊢ (fun n ↦ do
        guard (n ≤ k₂)
        unpaired
            (fun a n ↦
              Nat.casesOn n (evaln (k₂ + 1) a✝¹ a) fun y ↦ do
                let i ← evaln k₂ (a✝¹.prec a✝) (Nat.pair a y)
                evaln (k₂ + 1) a✝ (Nat.pair a (Nat.pair y i)))
            n)
      n =
    some x

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₂
a✝ : Code
a_ih✝ : ∀ (n x : ℕ), evaln (k + 1) a✝ n = some x → evaln (k₂ + 1) a✝ n = some x
n x : ℕ
h :
  (fun n ↦ do
        guard (n ≤ k)
        unpaired
            (fun a m ↦ do
              let x ← evaln (k + 1) a✝ (Nat.pair a m)
              if x = 0 then pure m else evaln k a✝.rfind' (Nat.pair a (m + 1)))
            n)
      n =
    some x
⊢ (fun n ↦ do
        guard (n ≤ k₂)
        unpaired
            (fun a m ↦ do
              let x ← evaln (k₂ + 1) a✝ (Nat.pair a m)
              if x = 0 then pure m else evaln k₂ a✝.rfind' (Nat.pair a (m + 1)))
            n)
      n =
    some x