Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: case zero
k n x : ℕ
left✝ : n ≤ k
h : 0 = x
⊢ x ∈ pure 0 n

pp: case succ
k n x : ℕ
left✝ : n ≤ k
h : n + 1 = x
⊢ x = n + 1

pp: case left
k n x : ℕ
left✝ : n ≤ k
h : (unpair n).1 = x
⊢ x = (unpair n).1

pp: case right
k n x : ℕ
left✝ : n ≤ k
h : (unpair n).2 = x
⊢ x = (unpair n).2

pp: case pair
k : ℕ
a✝¹ a✝ : Code
a_ih✝¹ : ∀ (n x : ℕ), x ∈ evaln (k + 1) a✝¹ n → x ∈ a✝¹.eval n
a_ih✝ : ∀ (n x : ℕ), x ∈ evaln (k + 1) a✝ n → x ∈ a✝.eval n
n x : ℕ
left✝ : n ≤ k
h : ∃ a, evaln (k + 1) a✝¹ n = some a ∧ ∃ a_1, evaln (k + 1) a✝ n = some a_1 ∧ Nat.pair a a_1 = x
⊢ ∃ a ∈ a✝¹.eval n, ∃ a_1 ∈ a✝.eval n, Nat.pair a a_1 = x

pp: case comp
k : ℕ
a✝¹ a✝ : Code
a_ih✝¹ : ∀ (n x : ℕ), x ∈ evaln (k + 1) a✝¹ n → x ∈ a✝¹.eval n
a_ih✝ : ∀ (n x : ℕ), x ∈ evaln (k + 1) a✝ n → x ∈ a✝.eval n
n x : ℕ
left✝ : n ≤ k
h : ∃ a, evaln (k + 1) a✝ n = some a ∧ evaln (k + 1) a✝¹ a = some x
⊢ ∃ a ∈ a✝.eval n, x ∈ a✝¹.eval a

pp: case prec
k : ℕ
a✝¹ a✝ : Code
a_ih✝¹ : ∀ (n x : ℕ), x ∈ evaln (k + 1) a✝¹ n → x ∈ a✝¹.eval n
a_ih✝ : ∀ (n x : ℕ), x ∈ evaln (k + 1) a✝ n → x ∈ a✝.eval n
n x : ℕ
left✝ : n ≤ k
h :
  Nat.rec (evaln (k + 1) a✝¹ (unpair n).1)
      (fun n_1 n_ih ↦
        (evaln k (a✝¹.prec a✝) (Nat.pair (unpair n).1 n_1)).bind fun i ↦
          evaln (k + 1) a✝ (Nat.pair (unpair n).1 (Nat.pair n_1 i)))
      (unpair n).2 =
    some x
⊢ x ∈
    Nat.rec (a✝¹.eval (unpair n).1) (fun y IH ↦ IH.bind fun i ↦ a✝.eval (Nat.pair (unpair n).1 (Nat.pair y i)))
      (unpair n).2

pp: case rfind'
k : ℕ
a✝ : Code
a_ih✝ : ∀ (n x : ℕ), x ∈ evaln (k + 1) a✝ n → x ∈ a✝.eval n
n x : ℕ
left✝ : n ≤ k
h :
  ∃ a,
    evaln (k + 1) a✝ n = some a ∧
      (if a = 0 then some (unpair n).2 else evaln k a✝.rfind' (Nat.pair (unpair n).1 ((unpair n).2 + 1))) = some x
⊢ ∃ a,
    (0 ∈ a✝.eval (Nat.pair (unpair n).1 (a + (unpair n).2)) ∧
        ∀ {m : ℕ}, m < a → ∃ a ∈ a✝.eval (Nat.pair (unpair n).1 (m + (unpair n).2)), ¬a = 0) ∧
      a + (unpair n).2 = x

Tactic:
iterate 4 simpa [pure, PFun.pure, eq_comm] using h

Goal state after:
case pair
k : ℕ
a✝¹ a✝ : Code
a_ih✝¹ : ∀ (n x : ℕ), x ∈ evaln (k + 1) a✝¹ n → x ∈ a✝¹.eval n
a_ih✝ : ∀ (n x : ℕ), x ∈ evaln (k + 1) a✝ n → x ∈ a✝.eval n
n x : ℕ
left✝ : n ≤ k
h : ∃ a, evaln (k + 1) a✝¹ n = some a ∧ ∃ a_1, evaln (k + 1) a✝ n = some a_1 ∧ Nat.pair a a_1 = x
⊢ ∃ a ∈ a✝¹.eval n, ∃ a_1 ∈ a✝.eval n, Nat.pair a a_1 = x

case comp
k : ℕ
a✝¹ a✝ : Code
a_ih✝¹ : ∀ (n x : ℕ), x ∈ evaln (k + 1) a✝¹ n → x ∈ a✝¹.eval n
a_ih✝ : ∀ (n x : ℕ), x ∈ evaln (k + 1) a✝ n → x ∈ a✝.eval n
n x : ℕ
left✝ : n ≤ k
h : ∃ a, evaln (k + 1) a✝ n = some a ∧ evaln (k + 1) a✝¹ a = some x
⊢ ∃ a ∈ a✝.eval n, x ∈ a✝¹.eval a

case prec
k : ℕ
a✝¹ a✝ : Code
a_ih✝¹ : ∀ (n x : ℕ), x ∈ evaln (k + 1) a✝¹ n → x ∈ a✝¹.eval n
a_ih✝ : ∀ (n x : ℕ), x ∈ evaln (k + 1) a✝ n → x ∈ a✝.eval n
n x : ℕ
left✝ : n ≤ k
h :
  Nat.rec (evaln (k + 1) a✝¹ (unpair n).1)
      (fun n_1 n_ih ↦
        (evaln k (a✝¹.prec a✝) (Nat.pair (unpair n).1 n_1)).bind fun i ↦
          evaln (k + 1) a✝ (Nat.pair (unpair n).1 (Nat.pair n_1 i)))
      (unpair n).2 =
    some x
⊢ x ∈
    Nat.rec (a✝¹.eval (unpair n).1) (fun y IH ↦ IH.bind fun i ↦ a✝.eval (Nat.pair (unpair n).1 (Nat.pair y i)))
      (unpair n).2

case rfind'
k : ℕ
a✝ : Code
a_ih✝ : ∀ (n x : ℕ), x ∈ evaln (k + 1) a✝ n → x ∈ a✝.eval n
n x : ℕ
left✝ : n ≤ k
h :
  ∃ a,
    evaln (k + 1) a✝ n = some a ∧
      (if a = 0 then some (unpair n).2 else evaln k a✝.rfind' (Nat.pair (unpair n).1 ((unpair n).2 + 1))) = some x
⊢ ∃ a,
    (0 ∈ a✝.eval (Nat.pair (unpair n).1 (a + (unpair n).2)) ∧
        ∀ {m : ℕ}, m < a → ∃ a ∈ a✝.eval (Nat.pair (unpair n).1 (m + (unpair n).2)), ¬a = 0) ∧
      a + (unpair n).2 = x