-- Module: Mathlib.Computability.PartrecCode
Goal:
k k₂ : ℕ
hl : k + 1 ≤ k₂ + 1
hl' : k ≤ k₂
this :
  ∀ {k k₂ n x : ℕ} {o₁ o₂ : Option ℕ},
    k ≤ k₂ →
      (x ∈ o₁ → x ∈ o₂) →
        Membership.mem (γ := Option ℕ)
            (do
              guard (n ≤ k)
              o₁)
            x →
          Membership.mem (γ := Option ℕ)
            (do
              guard (n ≤ k₂)
              o₂)
            x
cf cg : Code
hf : ∀ (n x : ℕ) (h : evaln (k + 1) cf n = some x), evaln (k₂ + 1) cf n = some x
hg : ∀ (n x : ℕ) (h : 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 (motive := fun (x : ℕ) ↦ Option ℕ) 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 :
          Option ℕ))
      n =
    some x
zero :
  ∀
    (h :
      Nat.rec (motive := fun (x : ℕ) ↦ Option ℕ) (evaln (k + 1) cf (unpair n).1)
          (fun (n_1 : ℕ) (n_ih : Option ℕ) ↦
            (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)))
          0 =
        some x),
    Nat.rec (motive := fun (x : ℕ) ↦ Option ℕ) (evaln (k₂ + 1) cf (unpair n).1)
        (fun (n_1 : ℕ) (n_ih : Option ℕ) ↦
          (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)))
        0 =
      some x
succ :
  ∀ (n_1 : ℕ),
    (∀
        (h :
          Nat.rec (motive := fun (x : ℕ) ↦ Option ℕ) (evaln (k + 1) cf (unpair n).1)
              (fun (n_2 : ℕ) (n_ih : Option ℕ) ↦
                (evaln k (cf.prec cg) (Nat.pair (unpair n).1 n_2)).bind fun (i : ℕ) ↦
                  evaln (k + 1) cg (Nat.pair (unpair n).1 (Nat.pair n_2 i)))
              n_1 =
            some x),
        Nat.rec (motive := fun (x : ℕ) ↦ Option ℕ) (evaln (k₂ + 1) cf (unpair n).1)
            (fun (n_2 : ℕ) (n_ih : Option ℕ) ↦
              (evaln k₂ (cf.prec cg) (Nat.pair (unpair n).1 n_2)).bind fun (i : ℕ) ↦
                evaln (k₂ + 1) cg (Nat.pair (unpair n).1 (Nat.pair n_2 i)))
            n_1 =
          some x) →
      ∀
        (h :
          Nat.rec (motive := fun (x : ℕ) ↦ Option ℕ) (evaln (k + 1) cf (unpair n).1)
              (fun (n_2 : ℕ) (n_ih : Option ℕ) ↦
                (evaln k (cf.prec cg) (Nat.pair (unpair n).1 n_2)).bind fun (i : ℕ) ↦
                  evaln (k + 1) cg (Nat.pair (unpair n).1 (Nat.pair n_2 i)))
              (n_1 + 1) =
            some x),
        Nat.rec (motive := fun (x : ℕ) ↦ Option ℕ) (evaln (k₂ + 1) cf (unpair n).1)
            (fun (n_2 : ℕ) (n_ih : Option ℕ) ↦
              (evaln k₂ (cf.prec cg) (Nat.pair (unpair n).1 n_2)).bind fun (i : ℕ) ↦
                evaln (k₂ + 1) cg (Nat.pair (unpair n).1 (Nat.pair n_2 i)))
            (n_1 + 1) =
          some x
⊢ ∀
    (h :
      Nat.rec (motive := fun (x : ℕ) ↦ Option ℕ) (evaln (k + 1) cf (unpair n).1)
          (fun (n_1 : ℕ) (n_ih : Option ℕ) ↦
            (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 (motive := fun (x : ℕ) ↦ Option ℕ) (evaln (k₂ + 1) cf (unpair n).1)
        (fun (n_1 : ℕ) (n_ih : Option ℕ) ↦
          (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

Premises used: Nat.unpair, Prod.snd